From a0df8836d01840303d8d70e5ad4d9045827cba7c Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Fri, 30 Aug 2024 12:46:52 +0300 Subject: [PATCH] Fix compilation for 64bit souffle wordsizes, add build and test action (#3) * Add build and test action * Enhance new action * Build and test with souffle package from apt * Try different souffle version * Try different ubuntu image * Try to get correct z3 package * another try * Add example in lists_test.dl that breaks locally * Download souffle 2.4.1 deb file as it's missing in apt. Remove useless installs. * Compile functors with -fopenmp * Run souffle --version in both configs * Parametrize Makefile to work for 32 or 64 bit souffle word sizes. * Polish gh action jobs * try to get action to run * minor --- .github/workflows/build-and-test.yml | 57 ++++++++++++++++++++++++++++ Makefile | 17 +++++---- README.md | 5 ++- lists_test.dl | 8 +++- 4 files changed, 77 insertions(+), 10 deletions(-) create mode 100644 .github/workflows/build-and-test.yml diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml new file mode 100644 index 0000000..3e23b22 --- /dev/null +++ b/.github/workflows/build-and-test.yml @@ -0,0 +1,57 @@ +name: Build and Test Functors + +on: + push: + branches: [ "master" ] + pull_request: + branches: [ "master" ] + +jobs: + build-and-test-32bit-wordsize: + # Souffle with a 32bit word size is built inside our "Gigahorse dependencies" docker image + runs-on: ubuntu-22.04 + + container: + image: ghcr.io/nevillegrech/gigahorse-toolchain-deps-souffle24:latest + + steps: + - uses: actions/checkout@v4 + + - name: Test Souffle + run: souffle --version + + - name: Build + run: make libsoufflenum.so WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13) + - name: Test + run: make WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13) + - name: Run lists_test.dl + run: souffle lists_test.dl + - name: Run smt-testing.dl + run: souffle smt-testing.dl + + build-and-test-64bit-wordsize: + # Souffle with a 64bit word size is installed on the runner via the provided .deb files + runs-on: ubuntu-22.04 + + steps: + - uses: actions/checkout@v4 + + - name: Download souffle + run: wget -O souffle.deb https://github.com/souffle-lang/souffle/releases/download/2.4.1/x86_64-ubuntu-2004-souffle-2.4.1-Linux.deb + - name: Install souffle + run: sudo apt-get install ./souffle.deb -y + + - name: Test Souffle + run: souffle --version + + - name: Install Boost + run: sudo apt install libboost-all-dev + + - name: Build + run: make libsoufflenum.so WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13) + - name: Test + run: make WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13) + - name: Run lists_test.dl + run: souffle lists_test.dl + - name: Run smt-testing.dl + run: souffle smt-testing.dl \ No newline at end of file diff --git a/Makefile b/Makefile index 6d12712..c5c4e81 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,7 @@ KECCAK_DIR := keccak KECCAK_SRC := $(wildcard $(KECCAK_DIR)/*.c) KECCAK_OBJ := $(patsubst $(KECCAK_DIR)/%.c,$(KECCAK_DIR)/%.o, $(KECCAK_SRC)) +WORD_SIZE=32 .PHONY: clean softclean @@ -8,35 +9,35 @@ KECCAK_OBJ := $(patsubst $(KECCAK_DIR)/%.c,$(KECCAK_DIR)/%.o, $(KECCAK_SRC)) all: libsoufflenum.so num_tests mappings_tests keccak256_tests libsoufflenum.so: $(KECCAK_OBJ) num256.o mappings.o keccak256.o lists.o smt-api.o - g++ -std=c++17 -shared -o libsoufflenum.so $(KECCAK_OBJ) smt-api.o num256.o mappings.o keccak256.o lists.o -march=native -lz3 - ln -sf libsoufflenum.so libfunctors.so + g++ -std=c++17 -shared -o libsoufflenum.so $(KECCAK_OBJ) smt-api.o num256.o mappings.o keccak256.o lists.o -march=native -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) + ln -sf libsoufflenum.so libfunctors.so smt-api.o: smt-api.cpp - g++ -std=c++17 smt-api.cpp -lz3 -c -fPIC -o smt-api.o + g++ -std=c++17 smt-api.cpp -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) -c -fPIC -o smt-api.o num256.o: num256.cpp - g++ -std=c++17 -O2 num256.cpp -c -fPIC -o num256.o -lz3 + g++ -std=c++17 -O2 num256.cpp -c -fPIC -o num256.o -lz3 -fopenmp num_tests: num256.cpp num256_test.cpp g++ -std=c++17 -o num_tests num256_test.cpp ./num_tests mappings.o: mappings.cpp - g++ -std=c++17 -O2 mappings.cpp -c -fPIC -o mappings.o -lz3 + g++ -std=c++17 -O2 mappings.cpp -c -fPIC -o mappings.o -lz3 -fopenmp mappings_tests: mappings.cpp mappings_test.cpp g++ -std=c++17 -o mappings_tests mappings_test.cpp ./mappings_tests lists.o: lists.cpp - g++ -std=c++17 -O2 lists.cpp -c -fPIC -o lists.o -lz3 + g++ -std=c++17 -O2 lists.cpp -c -fPIC -o lists.o -lz3 -fopenmp -DRAM_DOMAIN_SIZE=$(WORD_SIZE) lists_tests: lists.cpp lists_test.cpp g++ -std=c++17 -o lists_tests lists_test.cpp ./lists_tests keccak256.o: keccak256.cpp - g++ -std=c++17 -O2 keccak256.cpp -c -fPIC -o keccak256.o + g++ -std=c++17 -O2 keccak256.cpp -c -fPIC -o keccak256.o -fopenmp keccak256_test.o: keccak256_test.cpp keccak256.cpp g++ -std=c++17 -O2 -c -o keccak256_test.o keccak256_test.cpp @@ -46,7 +47,7 @@ keccak256_tests: keccak256_test.o $(KECCAK_OBJ) ./keccak256_tests $(KECCAK_DIR)/%.o: $(KECCAK_DIR)/%.c $(KECCAK_SRC) - gcc -O2 -c -fPIC -o $@ $< + gcc -O2 -fopenmp -c -fPIC -o $@ $< softclean: rm -f $(KECCAK_OBJ) diff --git a/README.md b/README.md index 078eff7..8d3702c 100644 --- a/README.md +++ b/README.md @@ -9,9 +9,12 @@ Dependencies: - Boost libraries - Z3: https://github.com/Z3Prover/z3 +Functor compilation is rellying on the underlying word size of the installed `souffle` binary. +Due to that, our Makefile is parametrized via its `WORD_SIZE` parameter. +The `make WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13)` command will build the functor with the correct word size (for latest `souffle` versions). Usage: - $ make # builds all, sets libfunctors.so as a link to libsoufflenum.so + $ make WORD_SIZE=32|64 # builds all, sets libfunctors.so as a link to libsoufflenum.so $ export LD_LIBRARY_PATH=`pwd` # or wherever you want to put the resulting libfunctors.so and use a Souffle program with the num256functors.dl definitions. For compiled execution, libfunctors.so (i.e., at least a diff --git a/lists_test.dl b/lists_test.dl index 16906ea..322caaa 100644 --- a/lists_test.dl +++ b/lists_test.dl @@ -36,4 +36,10 @@ TestCat(a, b, @list_concat(a, b)):- TestAppend(a, b, @list_append(a, b)):- a = ["0x8d8", ["0xf48", ["0xd05", ["0xd4b", ["0x91d", nil]]]]], b = "0x1457", - @list_append(a, b) = ["0x8d8", ["0xf48", ["0xd05", ["0xd4b", ["0x91d", ["0x1457", nil]]]]]]. \ No newline at end of file + @list_append(a, b) = ["0x8d8", ["0xf48", ["0xd05", ["0xd4b", ["0x91d", ["0x1457", nil]]]]]]. + +.decl BreakSouffle(x:StringList) +BreakSouffle(["ddd", nil]). +BreakSouffle(@list_append(["ddd", nil], "ddd")) :- BreakSouffle(["ddd", nil]). + +.output BreakSouffle