Allow to use SAT Solvers with IPASIR interface#552
Closed
nmanthey wants to merge 4 commits intodiffblue:developfrom
Closed
Allow to use SAT Solvers with IPASIR interface#552nmanthey wants to merge 4 commits intodiffblue:developfrom
nmanthey wants to merge 4 commits intodiffblue:developfrom
Conversation
1881203 to
ac2ea5c
Compare
Member
|
@nmanthey, this does not compile at the moment: https://travis-ci.org/diffblue/cbmc/jobs/202519720 |
Closed
Collaborator
|
@nmanthey could you have a look at the merge conflicts on this? It looks to be mostly Makefiles so should be pretty straight forward. |
added 4 commits
March 22, 2017 21:45
When building solvers.a while aiming at building CBMC with support for
IPASIR solvers, all projects that need SAT checkers would require to
link against the provided libipasir.a library. To make this library
visible for all subprojects at the same time, but furthermore allow the
user to choose which library to pick, the variable LIBSOLVER was
introduced, which is set to an empty value by default.
To compile while using IPASIR solvers, use for example:
IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
CFLAGS="-DSATCHECK_IPSAIR" make -j 7 -C src
Add the necessary source changes to allow CBMC to use IPASIR solvers.
Add necessary steps to set variables for IPASIR Furthermore, allow to select SAT solver from make command line, for example by calling IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a make Not, to compile with a different SAT solver, e.g. GLUCOSE=../../glucose-syrup make it has to be ensured, that the solvers.a library is rebuild, and all components that link against this library are renewed as well. This can be achieved by touching the satcheck.h flie, i.e.: touch src/solvers/sat/satcheck.h
Besides the usual test with Minisat, also compile with glucose, and test whether compilation with IPASIR works. Perform tests and regression testing for the two variants as well. Furthermore, if libzip and zlib and not inizialized properly, any build will fail. Hence, these targets are added as well.
Contributor
Author
|
at least one of the checks fails because the glucose variant of CBMC does not compile. I believe this should still be in the CI checks. I will not fix the glucose based build. |
Closed
Contributor
|
@nmanthey I started fixing the bugs, there's a bit more to do, the glucose bug was due to us using Alpine Linux with musl, while |
Contributor
Author
|
Closed as PR 884 has been accepted. |
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
…goat-use-xxe-library SEC-633: Make WebGoat.sh run XXE lessons
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Modern SAT solvers implement an interface for incremental SAT solving, IPASIR. To allow CPROVER tools to use more recent SAT solvers than Minisat or the installed Glucose, SAT solvers can be linked to CBMC by specifying the introduced "LIBSOLVER" make variable during build, which needs to point to a library of such a SAT solver.