symex: Add cadical

src/patches/cadical-shared-library.patch

@@ -0,0 +1,82 @@
+Taken from Fedora: https://src.fedoraproject.org/rpms/cadical/blob/rawhide/f/cadical-shared.patch
+
+See also: https://github.com/arminbiere/cadical/issues/40
+
+diff --git a/makefile.in b/makefile.in
+index 1a21bff..ba07560 100644
+--- a/makefile.in
++++ b/makefile.in
+@@ -9,6 +9,7 @@
+
+ CXX=@CXX@
+ CXXFLAGS=@CXXFLAGS@
++CXXFLAGS+=-fPIC
+
+ LIBS=@LIBS@
+
+@@ -26,7 +27,7 @@ COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR)
+
+ #--------------------------------------------------------------------------#
+
+-all: libcadical.a cadical mobical
++all: libcadical.so cadical mobical
+
+ #--------------------------------------------------------------------------#
+
+@@ -40,11 +41,17 @@ all: libcadical.a cadical mobical
+ # Application binaries (the stand alone solver 'cadical' and the model based
+ # tester 'mobical') and the library are the main build targets.
+
+-cadical: cadical.o libcadical.a makefile
+-	$(COMPILE) -o $@ $< -L. -lcadical $(LIBS)
++cadical: cadical.o libcadical.so makefile
++	$(COMPILE) -o $@ $< $(LDFLAGS) -L. -lcadical $(LIBS)
+
+-mobical: mobical.o libcadical.a makefile $(LIBS)
+-	$(COMPILE) -o $@ $< -L. -lcadical
++mobical: mobical.o libcadical.so makefile $(LIBS)
++	$(COMPILE) -o $@ $< $(LDFLAGS) -L. -lcadical
++
++libcadical.so: $(OBJ) makefile
++	rm -f $@
++	$(COMPILE) -shared -Wl,-h,libcadical.so.0 -o libcadical.so.0.0.0 $(LDFLAGS) $(OBJ)
++	ln -s libcadical.so.0.0.0 libcadical.so.0
++	ln -s libcadical.so.0 $@
+
+ libcadical.a: $(OBJ) makefile
+ 	ar rc $@ $(OBJ)
+@@ -53,7 +60,7 @@ libcadical.a: $(OBJ) makefile
+
+ # Note that 'build.hpp' is generated and resides in the build directory.
+
+-build.hpp: always
++build.hpp:
+ 	../scripts/make-build-header.sh > build.hpp
+
+ version.o: build.hpp
+@@ -85,8 +92,8 @@ clean:
+ 	rm -f *.gcda *.gcno *.gcov gmon.out
+
+ test: all
+-	CADICALBUILD="$(DIR)" $(MAKE) -j1 -C ../test
++	LD_LIBRARY_PATH=$(shell pwd) CADICALBUILD="$(DIR)" $(MAKE) -j1 -C ../test
+
+ #--------------------------------------------------------------------------#
+
+-.PHONY: all always analyze clean test update format
++.PHONY: all analyze clean test update format
+diff --git a/test/api/run.sh b/test/api/run.sh
+index 2f5df1d..70687af 100755
+--- a/test/api/run.sh
++++ b/test/api/run.sh
+@@ -28,8 +28,8 @@ die "needs to be called from a top-level sub-directory of CaDiCaL"
+ [ -f "$CADICALBUILD/makefile" ] || \
+   die "can not find '$CADICALBUILD/makefile' (run 'configure' first)"
+
+-[ -f "$CADICALBUILD/libcadical.a" ] || \
+-  die "can not find '$CADICALBUILD/libcadical.a' (run 'make' first)"
++[ -f "$CADICALBUILD/libcadical.so" ] || \
++  die "can not find '$CADICALBUILD/libcadical.so' (run 'make' first)"
+
+ cecho -n "$HILITE"
+ cecho "---------------------------------------------------------"

src/symex/packages/binsec.scm

@@ -2,10 +2,20 @@
   #:use-module (guix packages)
   #:use-module (guix download)
   #:use-module (guix gexp)
+  #:use-module (guix utils)
   #:use-module ((guix licenses) #:prefix license:)
   #:use-module (guix git-download)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix build-system copy)
   #:use-module (guix build-system dune)
   #:use-module (guix build-system ocaml)
+  #:use-module (guix build-system meson)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages check)
+  #:use-module (gnu packages version-control)
+  #:use-module (gnu packages maths)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages pkg-config)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ocaml))
 
@@ -221,3 +231,52 @@ at the intersection of formal methods, program analysis security and
 software engineering.")
     (home-page "https://binsec.github.io/")
     (license license:lgpl2.1)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-public cadical
+  (package
+    (name "cadical")
+    (version "1.9.5")
+    (source
+     (origin
+       (method git-fetch)
+       (patches (search-patches "patches/cadical-shared-library.patch"))
+       (uri (git-reference
+             (url "https://github.com/arminbiere/cadical")
+             (commit (string-append "rel-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "0vxky42s6md6ys85jkm5p1nnryrx9hafdc5l8fqfqpx3qp7sw0lq"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list
+      #:test-target "test"
+      #:make-flags #~(list (string-append "CXX="
+                                          #$(cxx-for-target))
+                           (string-append "LDFLAGS=-Wl,-rpath="
+                                          (assoc-ref %outputs "out") "/lib"))
+      #:phases #~(modify-phases %standard-phases
+                   (replace 'configure
+                     (lambda _
+                       (invoke "./configure")))
+                   (replace 'install
+                     (lambda* (#:key outputs #:allow-other-keys)
+                       (let* ((outdir (assoc-ref outputs "out"))
+                              (incdir (string-append outdir "/include"))
+                              (libdir (string-append outdir "/lib"))
+                              (bindir (string-append outdir "/bin")))
+                         (install-file "build/cadical" bindir)
+                         (install-file "build/mobical" bindir)
+                         (install-file "src/ccadical.h" incdir)
+                         (install-file "src/cadical.hpp" incdir)
+                         (install-file "build/libcadical.so" libdir)
+                         (install-file "build/libcadical.so.0" libdir)
+                         (install-file "build/libcadical.so.0.0.0" libdir)))))))
+    (synopsis "A simplified satisfiability solver")
+    (description
+     "CaDiCaL is a solver for the boolean satisfiability problem which utilizes
+@acronym{CDCL, Conflict-driven clause learning}. In comparison to existing solvers,
+it supposed to be easy to modify and extend.")
+    (home-page "https://github.com/arminbiere/cadical")
+    (license license:expat)))