Merge pull request #7493 from zhassan-aws/cadical-option

Allow building CBMC with multiple backend SAT solvers that can be selected at runtime via a new `--sat-solver` option

Author: zhassan-aws

.github/workflows/pull-request-checks.yaml

@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download
+          make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -118,7 +118,7 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src       -j2
+          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C unit      -j2
           make -C jbmc/src  -j2
           make -C jbmc/unit -j2
@@ -223,7 +223,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Check that doc task works
         run: ninja -C build doc
       - name: Zero ccache stats and limit in size
@@ -260,7 +260,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download
+          make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -290,7 +290,7 @@ jobs:
           make -C src/cpp library_check
       - name: Build with make
         run: |
-          make -C src       -j2
+          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C unit      -j2
           make -C jbmc/src  -j2
           make -C jbmc/unit -j2
@@ -348,7 +348,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Check that doc task works
         run: ninja -C build doc
       - name: Zero ccache stats and limit in size
@@ -439,7 +439,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
@@ -482,8 +482,8 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build using Make
         run: |
-          make -C src minisat2-download
-          make -C src -j3 CXX="ccache clang++"
+          make -C src minisat2-download cadical-download
+          make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
           make -C jbmc/src -j3 CXX="ccache clang++"
           make -C unit "CXX=ccache clang++"
           make -C jbmc/unit "CXX=ccache clang++"

.github/workflows/release-packages.yaml

@@ -39,7 +39,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build using Ninja
@@ -112,7 +112,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical"
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build using Ninja
@@ -198,7 +198,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical"
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build using Ninja

.gitignore

@@ -74,6 +74,7 @@ jbmc/regression/**/tests-symex-driven-loading.log
 
 # libs downloaded by make [name]-download
 minisat*/
+cadical*/
 glucose-syrup/
 
 # flex/bison generated files

CMakeLists.txt

@@ -273,7 +273,8 @@ else()
     FetchContent_MakeAvailable(Corrosion)
 
     corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
-    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} SAT_IMPL=${sat_impl})
+    list(JOIN sat_impl " " sat_impl_str)
+    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} "SAT_IMPL=${sat_impl_str}")
     corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
     install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
     # NOTE: We want to rename to a name consistent with the name of the

COMPILING.md

@@ -82,7 +82,7 @@ files.
    to generate IDE projects by supplying the `-G` flag.  Run `cmake -G` for a
    comprehensive list of supported back-ends.
 
-   As part of this step, CMake will download the back-end solver (see Section
+   As part of this step, CMake will download the back-end solvers (see Section
    "Compiling with alternative SAT solvers" in this document for configuration
    options). Should it be necessary to perform this step without network access,
    a solver can be downloaded ahead of the above `cmake` invocation as follows:
@@ -371,28 +371,40 @@ compilation flag:
 ## Compiling with alternative SAT solvers
 
 For the packaged builds of CBMC on our release page we currently build CBMC
-with the MiniSat2 SAT solver statically linked at compile time. However it is
-also possible to build CBMC using alternative SAT solvers.
+with the MiniSat2 and CaDiCaL SAT solvers statically linked at compile time.
+However it is also possible to build CBMC using alternative SAT solvers.
 
 ### Compiling CBMC Using Solver Native Interfaces
 
 The following solvers are supported by CBMC using custom interfaces and can
-by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
+be downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
 
-For `make` alternatives to the default (i.e. not MiniSAT) can be built with the
-following commands for CaDiCaL:
-```
-make -C src cadical-download
-make -C src CADICAL=../../cadical
-```
-and for glucose
+For `make`, alternatives to the default (i.e. not MiniSAT and CaDiCaL) can be
+built with the following commands for glucose:
 ```
 make -C src glucose-download
 make -C src GLUCOSE=../../glucose-syrup
 ```
+CBMC can be built with multiple solvers, which can then be selected at runtime
+using the `--sat-solver` option.
+For example, to build CBMC with MiniSAT2 and Glucose, do:
+```
+make -C src minisat2-download glucose-download
+make -C src MINISAT2=../../minisat-2.2.1 GLUCOSE=../../glucose-syrup
+```
+The build sets the default solver based on the priority defined by the
+`#if/#elif` tree defined at the end of
+[`src/solvers/sat/satcheck.h`](https://github.com/diffblue/cbmc/blob/develop/src/solvers/sat/satcheck.h).
+In the above example, MiniSAT2 will be set as the default solver because it is
+listed before Glucose. To switch to glucose at runtime, run CBMC with
+`--sat-solver glucose`.
 
 For CMake the alternatives can be built with the following arguments to `cmake`
-for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`.
+for glucose `-Dsat_impl=glucose`.
+To build CBMC with multiple solvers, specify the solvers in a semicolon-separated list to `-Dsat_impl`, e.g.:
+```
+cmake -S . -Bbuild -Dsat_impl="minisat2;glucose"
+```
 
 
 ### Compiling with IPASIR Interface
@@ -520,7 +532,7 @@ successfully on Windows or macOS.
 This document assumes you have already been able to build CPROVER on
 your chosen architecture.
 
-#RUNNING REGRESSION AND UNIT TESTS
+# RUNNING REGRESSION AND UNIT TESTS
 
 Regression and unit tests can be run using cmake or make. Your choice here
 should be the same as the compiling of the project itself.

Dockerfile

@@ -10,6 +10,7 @@ RUN echo 'tzdata tzdata/Areas select Etc' | debconf-set-selections; \
     echo 'tzdata tzdata/Zones/Etc select UTC' | debconf-set-selections; \
     apt-get update && apt-get upgrade -y && apt-get install --no-install-recommends -y \
     cmake \
+    make \
     ninja-build \
     gcc \
     g++ \

doc/man/cbmc.1

@@ -388,6 +388,9 @@ enable caching of repeated dereferences
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
 .TP
+\fB\-\-sat\-solver\fR solver
+use specified SAT solver
+.TP
 \fB\-\-external\-sat\-solver\fR cmd
 command to invoke SAT solver process
 .TP

doc/man/jbmc.1

@@ -382,6 +382,9 @@ enable caching of repeated dereferences
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
 .TP
+\fB\-\-sat\-solver\fR solver
+use specified SAT solver
+.TP
 \fB\-\-external\-sat\-solver\fR \fIcmd\fR
 command to invoke SAT solver process
 .TP

regression/cbmc/sat-solver-error/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = 0;
+  assert(x * y == y);
+  return 0;
+}

regression/cbmc/sat-solver-error/test.desc

@@ -0,0 +1,7 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend paths-lifo-expected-failure
+test.c
+--sat-solver non-existing-solver
+^EXIT=1$
+^SIGNAL=0$
+unknown solver 'non-existing-solver'
+--

regression/cbmc/sat-solver-warning/test.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = x;
+  x /= 2;
+  y /= 2;
+  assert(x == y);
+  return 0;
+}

regression/cbmc/sat-solver-warning/test.desc

@@ -0,0 +1,9 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend 
+test.c
+--sat-solver lingeling
+^EXIT=0$
+^SIGNAL=0$
+The specified solver, 'lingeling', is not available\. The default solver will be used instead\.
+\[main\.assertion\.1] line \d+ assertion x == y: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/sat-solver/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = x / 2;
+  assert(y != x);
+  assert(y <= x);
+  return 0;
+}

regression/cbmc/sat-solver/test.desc

@@ -0,0 +1,10 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend 
+test.c
+--sat-solver cadical
+^EXIT=10$
+^SIGNAL=0$
+Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
+\[main\.assertion\.1] line \d+ assertion y != x: FAILURE
+\[main\.assertion\.2] line \d+ assertion y <= x: SUCCESS
+^VERIFICATION FAILED$
+--

regression/validate-trace-xml-schema/check.py

@@ -42,6 +42,7 @@
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],
     ['unknown-argument-suggestion', 'test.desc'],
+    ['sat-solver-error', 'test.desc'],
     # this one produces XML intermingled with main XML output when used with --xml-ui
     ['graphml_witness2', 'test.desc'],
     # these are producing coverage goals which aren't included in the schema

scripts/cadical-1.4.1-patch

@@ -0,0 +1,34 @@
+diff --git a/scripts/make-build-header.sh b/scripts/make-build-header.sh
+index e8f6746..1290024 100755
+--- a/scripts/make-build-header.sh
++++ b/scripts/make-build-header.sh
+@@ -20,7 +20,7 @@ warning () {
+ 
+ #--------------------------------------------------------------------------#
+ 
+-[ ! -f VERSION -a ! -f ../VERSION ] && \
++[ ! -f VERSION.txt -a ! -f ../VERSION.txt ] && \
+ die "needs to be called from build sub-directory"
+ 
+ [ -f makefile ] || \
+@@ -29,7 +29,7 @@ warning "could not find 'makefile'"
+ #--------------------------------------------------------------------------#
+ # The version.
+ #
+-VERSION="`cat ../VERSION`"
++VERSION="`cat ../VERSION.txt`"
+ if [ x"$VERSION" = x ]
+ then
+   warning "could not determine 'VERSION'"
+diff --git a/src/lookahead.cpp b/src/lookahead.cpp
+index 9e8a16b..3d5721a 100644
+--- a/src/lookahead.cpp
++++ b/src/lookahead.cpp
+@@ -390,6 +390,7 @@ int Internal::lookahead_probing() {
+ CubesWithStatus Internal::generate_cubes(int depth, int min_depth) {
+   if (!active() || depth == 0) {
+     CubesWithStatus cubes;
++    cubes.status = 0;
+     cubes.cubes.push_back(std::vector<int>());
+     return cubes;
+   }

scripts/cadical_CMakeLists.txt

@@ -0,0 +1,27 @@
+file(GLOB sources "src/*.cpp" "src/*.hpp" "src/*.h")
+# Remove "app" sources from list
+list(REMOVE_ITEM sources
+    "${CMAKE_CURRENT_SOURCE_DIR}/src/cadical.cpp"
+    "${CMAKE_CURRENT_SOURCE_DIR}/src/mobical.cpp"
+)
+
+add_library(cadical ${sources})
+
+# Pass -DNBUILD to disable including the version information, which is not
+# needed since cbmc doesn't run the cadical binary
+target_compile_options(cadical PUBLIC -DNBUILD)
+
+set_target_properties(
+    cadical
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)
+
+target_include_directories(cadical
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}/src
+)
+
+target_link_libraries(cadical util)

src/Makefile

@@ -177,7 +177,11 @@ cadical-download:
 	@$(TAR) xfz $(cadical_release).tar.gz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@cd ../cadical && CXX=$(CXX) ./configure -O3 -s && make -j
+	@(cd ../cadical; patch -p1 < ../scripts/cadical-1.4.1-patch)
+	@(cd ../cadical && ./configure)
+  # Need to rename VERSION so that it isn't picked up by `#include<version>` on
+  # macOS which is case insensitive
+	@(cd ../cadical && mv VERSION VERSION.txt)
 	@$(RM) $(cadical_release).tar.gz
 
 doc :