diff options
| -rw-r--r-- | lib/Solver/STPSolver.cpp | 65 | ||||
| -rw-r--r-- | test/Solver/STPswitchSAT.c | 31 |
2 files changed, 94 insertions, 2 deletions
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 95728cde..13536910 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -16,13 +16,14 @@ #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/ExprUtil.h" -#include "klee/Support/OptionCategories.h" #include "klee/Solver/SolverImpl.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/OptionCategories.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" +#include <array> #include <csignal> #include <sys/ipc.h> #include <sys/shm.h> @@ -40,7 +41,24 @@ llvm::cl::opt<bool> IgnoreSolverFailures( "ignore-solver-failures", llvm::cl::init(false), llvm::cl::desc("Ignore any STP solver failures (default=false)"), llvm::cl::cat(klee::SolvingCat)); -} + +enum SAT { MINISAT, SIMPLEMINISAT, CRYPTOMINISAT, RISS }; +const std::array<std::string, 4> SATNames{"MiniSat", "simplifying MiniSat", + "CryptoMiniSat", "RISS"}; + +llvm::cl::opt<SAT> SATSolver( + "stp-sat-solver", + llvm::cl::desc( + "Set the underlying SAT solver for STP (default=cryptominisat)"), + llvm::cl::values(clEnumValN(SAT::MINISAT, "minisat", + SATNames[SAT::MINISAT]), + clEnumValN(SAT::SIMPLEMINISAT, "simpleminisat", + SATNames[SAT::SIMPLEMINISAT]), + clEnumValN(SAT::CRYPTOMINISAT, "cryptominisat", + SATNames[SAT::CRYPTOMINISAT]), + clEnumValN(SAT::RISS, "riss", SATNames[SAT::RISS])), + llvm::cl::init(CRYPTOMINISAT), llvm::cl::cat(klee::SolvingCat)); +} // namespace #define vc_bvBoolExtract IAMTHESPAWNOFSATAN @@ -103,6 +121,49 @@ STPSolverImpl::STPSolverImpl(bool useForkedSTP, bool optimizeDivides) // we restore the old behaviour. vc_setInterfaceFlags(vc, EXPRDELETE, 0); + // set SAT solver + bool SATSolverAvailable = false; + bool specifiedOnCommandLine = SATSolver.getNumOccurrences() > 0; + switch (SATSolver) { + case SAT::MINISAT: { + SATSolverAvailable = vc_useMinisat(vc); + break; + } + case SAT::SIMPLEMINISAT: { + SATSolverAvailable = vc_useSimplifyingMinisat(vc); + break; + } + case SAT::CRYPTOMINISAT: { + SATSolverAvailable = vc_useCryptominisat(vc); + break; + } + case SAT::RISS: { + SATSolverAvailable = vc_useRiss(vc); + break; + } + default: + assert(false && "Illegal SAT solver value."); + } + + // print SMT/SAT status + const auto expectedSATName = SATNames[SATSolver.getValue()]; + std::string SATName{"unknown"}; + if (vc_isUsingMinisat(vc)) + SATName = SATNames[SAT::MINISAT]; + else if (vc_isUsingSimplifyingMinisat(vc)) + SATName = SATNames[SAT::SIMPLEMINISAT]; + else if (vc_isUsingCryptominisat(vc)) + SATName = SATNames[SAT::CRYPTOMINISAT]; + else if (vc_isUsingRiss(vc)) + SATName = SATNames[SAT::RISS]; + + if (!specifiedOnCommandLine || SATSolverAvailable) { + klee_message("SAT solver: %s", SATName.c_str()); + } else { + klee_warning("%s not supported by STP", expectedSATName.c_str()); + klee_message("Fallback SAT solver: %s", SATName.c_str()); + } + make_division_total(vc); vc_registerErrorHandler(::stp_error_handler); diff --git a/test/Solver/STPswitchSAT.c b/test/Solver/STPswitchSAT.c new file mode 100644 index 00000000..f205aca7 --- /dev/null +++ b/test/Solver/STPswitchSAT.c @@ -0,0 +1,31 @@ +// REQUIRES: stp +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// +// RUN: rm -rf %t.klee-out-minisat +// RUN: %klee --output-dir=%t.klee-out-minisat -solver-backend=stp --stp-sat-solver=minisat %t1.bc +// RUN: cat %t.klee-out-minisat/messages.txt %t.klee-out-minisat/warnings.txt > %t.klee-out-minisat/all.txt +// RUN: FileCheck --input-file=%t.klee-out-minisat/all.txt --check-prefix=MINISAT %s +// +// RUN: rm -rf %t.klee-out-riss +// RUN: %klee --output-dir=%t.klee-out-riss -solver-backend=stp --stp-sat-solver=riss %t1.bc +// RUN: cat %t.klee-out-riss/messages.txt %t.klee-out-riss/warnings.txt > %t.klee-out-riss/all.txt +// RUN: FileCheck --input-file=%t.klee-out-riss/all.txt --check-prefix=RISS %s + +#include "klee/klee.h" + +int main(void) { + int foo; + int bar = 42; + klee_make_symbolic(&foo, sizeof(foo), "foo"); + + if (foo) bar -= 17; + else bar += 5; + + return bar; +} + +// MINISAT: KLEE: Using STP solver backend +// MINISAT: {{KLEE: SAT solver: MiniSat|KLEE: Fallback SAT solver}} + +// RISS: KLEE: Using STP solver backend +// RISS: {{KLEE: SAT solver: RISS|KLEE: Fallback SAT solver}} |