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

zhassan-aws · 2023-01-19T19:51:04Z

Allow building CBMC with multiple backend solvers that can be selected at runtime via the new --sat-solver option.

For example, if CBMC is built with cmake -S . -Bbuild -Dsat_impl="minisat2;cadical", then one can use cbmc --sat-solver cadical to use CaDiCaL instead of MiniSAT.

The release build now includes both MiniSAT2 and CaDiCaL.

Fixes: #7467

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2023-01-19T20:48:08Z

Codecov Report

Base: 78.49% // Head: 78.27% // Decreases project coverage by -0.22% ⚠️

Coverage data is based on head (85c6f6c) compared to base (eaae3b6).
Patch coverage: 75.00% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7493      +/-   ##
===========================================
- Coverage    78.49%   78.27%   -0.22%     
===========================================
  Files         1663     1667       +4     
  Lines       191339   191475     +136     
===========================================
- Hits        150186   149882     -304     
- Misses       41153    41593     +440

Impacted Files	Coverage Δ
src/goto-checker/solver_factory.h	`100.00% <ø> (ø)`
src/goto-checker/solver_factory.cpp	`80.16% <75.00%> (-1.07%)`	⬇️
src/util/validate_expressions.cpp	`31.25% <0.00%> (-62.50%)`	⬇️
src/util/cout_message.cpp	`33.33% <0.00%> (-51.86%)`	⬇️
src/util/timestamper.h	`16.66% <0.00%> (-50.00%)`	⬇️
src/util/type.cpp	`27.27% <0.00%> (-45.46%)`	⬇️
src/big-int/bigint.cc	`56.61% <0.00%> (-32.40%)`	⬇️
src/util/string_container.cpp	`24.07% <0.00%> (-27.78%)`	⬇️
src/util/symbol_table.cpp	`66.30% <0.00%> (-25.00%)`	⬇️
src/util/validate_types.cpp	`70.00% <0.00%> (-23.34%)`	⬇️
... and 59 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

TGWDB · 2023-01-20T10:13:11Z

Assigning myself to keep up to date on this. I've done a partial review, but will wait until all checks have passed.

NlightNFotis · 2023-01-20T10:31:51Z

CMakeLists.txt

@@ -91,7 +91,7 @@ set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")

 set(sat_impl "minisat2" CACHE STRING
    "This setting controls the SAT library which is used. Valid values are
-    'minisat2', 'glucose', 'cadical', 'ipasir-cadical' or 'ipasir-custom'"


Why was this deleted?

I removed cadical from the list, since the PR changes the build flow so that cadical is always included in the build, so there is no longer a reason to build with -Dsat_impl=cadical.

See my above comment: maybe there is, and even if it's only to run tests with CaDiCaL (without having to specify --cadical).

NlightNFotis · 2023-01-20T10:32:51Z

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

@@ -412,7 +412,7 @@ jobs:
        run: ccache -z --max-size=500M
      - name: Build using Make
        run: |
-          make -C src minisat2-download


Why add the download to all of the builds even to the ones not using cadical?

This seems to increase build times for no observable benefit (if it's not being used).

To support the new --cadical option, cadical now has to be always built (otherwise, the CBMC build will fail). Downloading and building it typically takes ~11 seconds, so hopefully this doesn't add too much overhead:

$ /usr/bin/time -p make -C src cadical-download ... real 11.28

Is this still the case? It would be good if it could be built without.

NlightNFotis · 2023-01-20T10:33:51Z

COMPILING.md

   ```
   mkdir -p build/minisat2-download/minisat2-download-prefix/src/
   wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz \
     -O build/minisat2-download/minisat2-download-prefix/src/minisat2_2.2.1.orig.tar.gz
+   mkdir -p build/cadical-download/cadical-download-prefix/src/
+   wget  https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz \
+     -O build/cadical-download/cadical-download-prefix/src/rel-1.4.1.tar.gz


Note to self: candidate for automation through the justfile? #7486

NlightNFotis · 2023-01-20T10:34:48Z

COMPILING.md

@@ -520,7 +520,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


I love little fixes to improve the docs 👍🏻

NlightNFotis · 2023-01-20T10:35:56Z

src/config.inc


 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)


Why did this need to be deleted?

It seems to also be containing minisat2 which is the default.

Since cadical is now always included, it was necessary to remove it from the list so that we don't prevent minisat from getting built by default as well. That way, if the build is done with -Dsat_impl=glucose for example, then glucose will be built in place of minisat (but cadical is always built regardless of the options).

tautschnig · 2023-01-23T11:22:43Z

We'll have to refrain from building CaDiCaL on Windows, unless we want to use the patched version from https://github.com/deiruch/cadical (which, arguably, we could - it seems it's being kept up to date; maybe we just use this version for Windows?).

martin-cs

It seems that this PR does a number of linked but different things.

A. Allow (limited) runtime switching of SAT solvers.
B. Remove the option to build without CaDiCaL.
C. Change the default solver to CaDiCaL.

A. is a good thing and long overdue. I would really support this, esp. if it worked for all solvers.
B. I am less sure about but I can see it is necessary for C.
C. Has some pretty far-reaching consequences and will change pretty much the entire performance profile of the tool. I suspect it will be for the better but it feels like the kind of change that should be profiled.

Can you explain a little more why you want this change and why it is important to do B and C? Is CADICAL=... make not a option?

zhassan-aws · 2023-01-24T00:32:50Z

Thanks for taking a look @martin-cs.

It seems that this PR does a number of linked but different things.

A. Allow (limited) runtime switching of SAT solvers. B. Remove the option to build without CaDiCaL. C. Change the default solver to CaDiCaL.

The PR does A and B, but not C. The default SAT solver remains minisat. I updated the PR description to clarify this.

Can you explain a little more why you want this change and why it is important to do B and C?

The point of this change is to include an option to run CBMC with cadical in CBMC releases going forward. This allows people using the CBMC binaries included in the releases to switch to cadical via an option instead of having to build CBMC from source.

martin-cs · 2023-01-24T11:56:54Z

> Can you explain a little more why you want this change and why it > is important to do B and C? The point of this change is to include an option to run CBMC with cadical in CBMC releases going forward. This allows people using the CBMC binaries included in the releases to switch to cadical via an option instead of having to build CBMC from source.

Why not just set `CADICAL = ../../cadical` before building in the part of the CI that builds the release binaries? That way it is in the release but is not added as a build dependency for everyone? We should also possibly use it in some of the CI jobs just so that we catch if it breaks.

zhassan-aws · 2023-01-24T15:56:40Z

Why not just set CADICAL = ../../cadical before building in the part of the CI that builds the release binaries?

Wouldn't that make CaDiCaL the only choice for released binaries? The point of the PR was to give users the option to switch to a different solver at runtime (cadical in this PR, but other solvers can be added later) as requested in #7467.

martin-cs · 2023-01-25T21:35:44Z

> Why not just set CADICAL = ../../cadical before building in the > part of the CI that builds the release binaries? Wouldn't that make CaDiCaL the only choice for released binaries? The point of the PR was to give users the option to switch to a different solver at runtime (cadical in this PR, but other solvers can be added later) as requested in #7467< #7467>.

Forgive me if I have confused matters, my position is: - I think the run-time switching is good. It would be great to have that for all of the solvers. Keeping minisat2 as the default is good too. - I think it would be good if CADICAL remains an optional part of the build. - Having it enabled for the release build and some of the CI jobs seems like a good way to get the functionality you need. Does that make sense?

zhassan-aws · 2023-01-25T22:24:02Z

I see. Thanks for clarifying. I'll see if I can keep cadical an optional part of the build. In that case, we can error out if --cadical is passed to cbmc?

jimgrundy · 2023-01-25T22:37:30Z

Does CaDiCaL need to be special? Could we let people build with any/multiple solvers and then run-time switch to any of the solvers they built with?

martin-cs · 2023-01-25T22:55:03Z

@zhassan-aws It should be possible to guard using HAVE_CADICAL so that you only have the flag when it has been built like that.

@jimgrundy That would be ideal!

zhassan-aws · 2023-01-25T22:59:12Z

Does CaDiCaL need to be special?

No, but CaDiCaL was explicitly requested in #7467.

Could we let people build with any/multiple solvers and then run-time switch to any of the solvers they built with?

That would be ideal. This PR was meant as a step in that direction.

jimgrundy · 2023-01-25T23:58:58Z

This is a response to a request, but it's our own request, so we have some flex here. Would it be a lot of work to do the more general thing? I mean if it is, then sure, let's do it later, but if it's not much it will be easiest to do it now while you have this in your head.

tautschnig · 2023-01-26T09:17:02Z

Could we let people build with any/multiple solvers and then run-time switch to any of the solvers they built with?

That would be ideal. This PR was meant as a step in that direction.

Should the user experience/command-line interface then perhaps be --sat-solver <name> with a runtime error when <name> is not among the solvers built with, and that same error then also listing what the valid choices are? Else I'm worried that we'll struggle to present coherent documentation (at all levels: HTML manuals and tutorials, man pages, help output).

…T solver

…ltiple backend solvers

peterschrammel

Have you tried to build with -Dsat_impl="minisat2;glucose"?

zhassan-aws · 2023-02-10T15:37:21Z

Have you tried to build with -Dsat_impl="minisat2;glucose"?

I don't recall if I did, but I just tried it now, and it behaves as expected:

$ ~/git/cbmc/build/bin/cbmc fail.c | grep Solving
Solving with MiniSAT 2.2.1 with simplifier
$ ~/git/cbmc/build/bin/cbmc fail.c --sat-solver glucose | grep Solving
Solving with Glucose Syrup with simplifier

src/goto-checker/solver_factory.cpp

martin-cs

Thanks for all of the reworking on this @zhassan-aws . I appreciate that it is tedious but I think it is really a better change because of it.

martin-cs · 2023-02-15T15:03:57Z

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

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


I am probably wrong about this but shouldn't the assignment of environmental variables be before the make, as in:

CXXFLAGS="-O0 -g" make -j4000

AFAIK, this is a standard way for passing variables from the command-line to make (e.g. see http://books.gigatux.nl/mirror/cinanutshell/0596006977/cinanut-CHP-19-SECT-5.html). In this form, the variables are not treated as environment variables, and they are parsed by the make command.

martin-cs · 2023-02-15T15:04:44Z

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

@@ -412,7 +412,7 @@ jobs:
        run: ccache -z --max-size=500M
      - name: Build using Make
        run: |
-          make -C src minisat2-download


Is this still the case? It would be good if it could be built without.

martin-cs · 2023-02-15T15:06:40Z

scripts/cadical-1.4.1-patch

+ # The version.
+ #
+-VERSION="`cat ../VERSION`"
+VERSION="`cat ../VERSION.txt`"


Ummm... why the rename?

I added a comment here that explains why the rename is necessary. In short, the build failed on macos-11 without this change:

https://github.com/diffblue/cbmc/actions/runs/4138376169/jobs/7154711888#step:9:782

because the used macos-11 image is case insensitive, and so it ends up using the VERSION file in cadical's root directory for an #include<version> directive, as opposed to using the system's version header file. See this thread for more details:

marian-nmt/marian-dev#871 (comment)

martin-cs · 2023-02-15T15:08:51Z

src/goto-checker/solver_factory.h

@@ -126,6 +130,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
  " --smt2                       use default SMT2 solver (Z3)\n"               \
  " --bitwuzla                   use Bitwuzla\n"                               \
  " --boolector                  use Boolector\n"                              \
+  " --sat-solver solver          use specified SAT solver\n"                   \


This is a terrible thing to request as it is so fiddly, so feel free to ignore BUT would it be possible to have the available solvers given here, so it prints "use specified SAT solver : minisat2, CaDiCaL" etc.

That's a good idea, but I'm not sure how easy it would be. I'll see if I can do this in a follow-up PR.

zhassan-aws · 2023-02-15T17:51:49Z

Is this still the case? It would be good if it could be built without.

CaDiCaL is optional in the build, but I added it to as many workflows as possible because @tautschnig mentioned that there are a few regression tests that would be significantly sped up by using cadical, so he plans on updating them to use cadical to reduce CI time.

thomasspriggs · 2023-02-15T18:58:03Z

This may be something of a moot point now the PR is merged, but I don't see the Windows release package being updated in this PR to be built with multiple SAT solvers like for the Ubuntu releases. Does this mean this new functionality doesn't work on Windows or just that we have moved further further from feature parity?

zhassan-aws · 2023-02-15T19:23:00Z

Does this mean this new functionality doesn't work on Windows or just that we have moved further further from feature parity?

The feature works on Windows as well, in the sense that the build can include multiple solvers. However, CaDiCaL cannot be built on Windows currently due to some platform-dependent code it uses, and thus, I haven't included it in the Windows release build. Perhaps we can try using the fork of CaDiCaL pointed out in this comment? We can also try patching it ourselves.

zhassan-aws requested review from a team, kroening, tautschnig, peterschrammel, chris-ryder, thomasspriggs, NlightNFotis, TGWDB and martin-cs as code owners January 19, 2023 19:51

zhassan-aws requested a review from jimgrundy as a code owner January 19, 2023 22:53

TGWDB self-assigned this Jan 20, 2023

NlightNFotis reviewed Jan 20, 2023

View reviewed changes

feliperodri added aws Bugs or features of importance to AWS CBMC users Kani Bugs or features of importance to Kani Rust Verifier labels Jan 23, 2023

martin-cs reviewed Jan 23, 2023

View reviewed changes

zhassan-aws force-pushed the cadical-option branch from fedd088 to f1dfc28 Compare January 31, 2023 01:10

zhassan-aws changed the title ~~Build CaDiCaL by default and allow invoking it via an option~~ Allow building CBMC with multiple backend solvers Feb 1, 2023

zhassan-aws added 4 commits February 9, 2023 17:04

Include cadical in some CI workflows

b1fb769

Include cadical in release packages

6bf4dad

Introduce a new --sat-solver option to allow selecting the backend SA…

d070932

…T solver

Update installation instructions to include how to build CBMC with mu…

4b17867

…ltiple backend solvers

zhassan-aws force-pushed the cadical-option branch from a355830 to 4b17867 Compare February 10, 2023 01:07

zhassan-aws changed the title ~~Allow building CBMC with multiple backend solvers~~ Allow building CBMC with multiple backend SAT solvers that can be selected at runtime via a new --sat-solver option Feb 10, 2023

zhassan-aws removed their assignment Feb 10, 2023

peterschrammel reviewed Feb 10, 2023

View reviewed changes

peterschrammel approved these changes Feb 10, 2023

View reviewed changes

peterschrammel removed their assignment Feb 10, 2023

zhassan-aws requested a review from kroening February 10, 2023 22:15

tautschnig assigned kroening Feb 13, 2023

TGWDB approved these changes Feb 15, 2023

View reviewed changes

kroening reviewed Feb 15, 2023

View reviewed changes

src/goto-checker/solver_factory.cpp Show resolved Hide resolved

kroening approved these changes Feb 15, 2023

View reviewed changes

tautschnig assigned zhassan-aws and unassigned kroening, NlightNFotis, thomasspriggs and TGWDB Feb 15, 2023

martin-cs approved these changes Feb 15, 2023

View reviewed changes

Undo renaming of function back to get_default

85c6f6c

zhassan-aws merged commit 42d5ce2 into diffblue:develop Feb 15, 2023

zhassan-aws deleted the cadical-option branch February 15, 2023 18:36

NlightNFotis mentioned this pull request Mar 1, 2023

cbmc: enable building CBMC with both minisat and cadical by default Homebrew/homebrew-core#124543

Closed

6 tasks

NlightNFotis mentioned this pull request Mar 9, 2023

Naming collisions prevent linking against libcprover.5.78.0.a #7586

Closed


		# select default solver to be minisat2 if no other is specified
		ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)

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

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

Uh oh!

Conversation

zhassan-aws commented Jan 19, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jan 19, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

TGWDB commented Jan 20, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 23, 2023

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

zhassan-aws commented Jan 24, 2023

Uh oh!

martin-cs commented Jan 24, 2023 via email

Uh oh!

zhassan-aws commented Jan 24, 2023

Uh oh!

martin-cs commented Jan 25, 2023 via email

Uh oh!

zhassan-aws commented Jan 25, 2023

Uh oh!

jimgrundy commented Jan 25, 2023

Uh oh!

martin-cs commented Jan 25, 2023

Uh oh!

zhassan-aws commented Jan 25, 2023

Uh oh!

jimgrundy commented Jan 25, 2023

Uh oh!

tautschnig commented Jan 26, 2023

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

zhassan-aws commented Feb 10, 2023

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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

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

zhassan-aws commented Jan 19, 2023 •

edited

Loading

codecov bot commented Jan 19, 2023 •

edited

Loading