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

@@ -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

Makefile

@@ -1,42 +1,43 @@
 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
 
 # rudimentary
 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)

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

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]]]]]].
+  @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