diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-07 12:00:25 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-12 11:40:39 +0000 |
commit | e81f5ceed580d4d267e3c857b47637d6bd065499 (patch) | |
tree | eb9f3b74b036a59edd1164bc68e9e00d5156936d | |
parent | 9da07ca0ccc58286f8247bc2e7d7745abfa0cc54 (diff) | |
download | klee-e81f5ceed580d4d267e3c857b47637d6bd065499.tar.gz |
Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing
a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...
-rw-r--r-- | include/klee/CommandLine.h | 6 | ||||
-rw-r--r-- | include/klee/Solver.h | 5 | ||||
-rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 26 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 78 | ||||
-rw-r--r-- | lib/Solver/CoreSolver.cpp | 87 | ||||
-rw-r--r-- | test/Solver/FastCexSolver.pc | 2 | ||||
-rw-r--r-- | tools/kleaver/main.cpp | 42 | ||||
-rw-r--r-- | unittests/Solver/SolverTest.cpp | 4 |
8 files changed, 130 insertions, 120 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index c4c70069..44f1afd4 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -44,17 +44,19 @@ enum QueryLoggingSolverType */ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; +enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER }; +extern llvm::cl::opt<CoreSolverType> CoreSolverToUse; + #ifdef SUPPORT_METASMT enum MetaSMTBackendType { - METASMT_BACKEND_NONE, METASMT_BACKEND_STP, METASMT_BACKEND_Z3, METASMT_BACKEND_BOOLECTOR }; -extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT; +extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend; #endif /* SUPPORT_METASMT */ diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 906309d2..e3adac6a 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -10,6 +10,7 @@ #ifndef KLEE_SOLVER_H #define KLEE_SOLVER_H +#include "klee/CommandLine.h" // FIXME: This is just for CoreSolverType #include "klee/Expr.h" #include <vector> @@ -290,7 +291,9 @@ namespace klee { /// createDummySolver - Create a dummy solver implementation which always /// fails. Solver *createDummySolver(); - + + // Create a solver based on the supplied ``CoreSolverType``. + Solver *createCoreSolver(CoreSolverType cst); } #endif diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index eac54141..d7157b25 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -75,18 +75,26 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( #ifdef SUPPORT_METASMT -llvm::cl::opt<klee::MetaSMTBackendType> -UseMetaSMT("use-metasmt", - llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."), - llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"), - clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), - clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), - clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), - clEnumValEnd), - llvm::cl::init(METASMT_BACKEND_NONE)); +llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend( + "metasmt-backend", + llvm::cl::desc("Specify the MetaSMT solver backend type."), + llvm::cl::values( + clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), + clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), + clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", + "Use metaSMT with Boolector"), + clEnumValEnd), + llvm::cl::init(METASMT_BACKEND_STP)); #endif /* SUPPORT_METASMT */ +llvm::cl::opt<CoreSolverType> CoreSolverToUse( + "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"), + llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"), + clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), + clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), + clEnumValEnd), + llvm::cl::init(STP_SOLVER)); } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9211f485..854754b0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -107,29 +107,6 @@ using namespace llvm; using namespace klee; -#ifdef SUPPORT_METASMT - -#include <metaSMT/frontend/Array.hpp> -#include <metaSMT/backend/Z3_Backend.hpp> -#include <metaSMT/backend/Boolector.hpp> -#include <metaSMT/backend/MiniSAT.hpp> -#include <metaSMT/DirectSolver_Context.hpp> -#include <metaSMT/support/run_algorithm.hpp> -#include <metaSMT/API/Stack.hpp> -#include <metaSMT/API/Group.hpp> - -#define Expr VCExpr -#define Type VCType -#define STP STP_Backend -#include <metaSMT/backend/STP.hpp> -#undef Expr -#undef Type -#undef STP - -using namespace metaSMT; -using namespace metaSMT::solver; - -#endif /* SUPPORT_METASMT */ @@ -293,50 +270,19 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - - Solver *coreSolver = NULL; - -#ifdef SUPPORT_METASMT - if (UseMetaSMT != METASMT_BACKEND_NONE) { - - std::string backend; - - switch (UseMetaSMT) { - case METASMT_BACKEND_STP: - backend = "STP"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_Z3: - backend = "Z3"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_BOOLECTOR: - backend = "Boolector"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - default: - assert(false); - break; - }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; - } - else { - coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); - } -#else - coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); -#endif /* SUPPORT_METASMT */ - - - Solver *solver = - constructSolverChain(coreSolver, - interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), - interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), - interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), - interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - - this->solver = new TimingSolver(solver, EqualitySubstitution); + Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); + if (!coreSolver) { + llvm::errs() << "Failed to create core solver\n"; + exit(1); + } + Solver *solver = constructSolverChain( + coreSolver, + interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), + interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), + interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), + interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); + this->solver = new TimingSolver(solver, EqualitySubstitution); memory = new MemoryManager(&arrayCache); } diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp new file mode 100644 index 00000000..9d21931d --- /dev/null +++ b/lib/Solver/CoreSolver.cpp @@ -0,0 +1,87 @@ +//===-- CoreSolver.cpp ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/CommandLine.h" +#include "klee/Solver.h" +#include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/raw_ostream.h" +#include <string> + +#ifdef SUPPORT_METASMT + +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +static Solver *handleMetaSMT() { + Solver *coreSolver = NULL; + std::string backend; + switch (MetaSMTBackend) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + llvm_unreachable("Unrecognised metasmt backend"); + break; + }; + llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; + return coreSolver; +} +#endif /* SUPPORT_METASMT */ + +namespace klee { + +Solver *createCoreSolver(CoreSolverType cst) { + switch (cst) { + case STP_SOLVER: + llvm::errs() << "Using STP solver backend\n"; + return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + case METASMT_SOLVER: +#ifdef SUPPORT_METASMT + llvm::errs() << "Using MetaSMT solver backend\n"; + return handleMetaSMT(); +#else + llvm::errs() << "Not compiled with MetaSMT support\n"; + return NULL; +#endif + case DUMMY_SOLVER: + return createDummySolver(); + default: + llvm_unreachable("Unsupported CoreSolverType"); + } +} +} diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.pc index b8f839c3..b3ec63e3 100644 --- a/test/Solver/FastCexSolver.pc +++ b/test/Solver/FastCexSolver.pc @@ -1,4 +1,4 @@ -# RUN: %kleaver --use-fast-cex-solver --use-dummy-solver %s > %t +# RUN: %kleaver --use-fast-cex-solver --solver-backend=dummy %s > %t # RUN: not grep FAIL %t array arr1[4] : w32 -> w8 = symbolic diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index af337abe..f91693c5 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -104,9 +104,6 @@ namespace { "Fold constants and simplify expressions."), clEnumValEnd)); - cl::opt<bool> - UseDummySolver("use-dummy-solver", - cl::init(false)); llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."), llvm::cl::init(".")); @@ -224,42 +221,9 @@ static bool EvaluateInputAST(const char *Filename, if (!success) return false; - // FIXME: Support choice of solver. - Solver *coreSolver = NULL; // - -#ifdef SUPPORT_METASMT - if (UseMetaSMT != METASMT_BACKEND_NONE) { - - std::string backend; - - switch (UseMetaSMT) { - case METASMT_BACKEND_STP: - backend = "STP"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_Z3: - backend = "Z3"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_BOOLECTOR: - backend = "Boolector"; - coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - default: - assert(false); - break; - }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; - } - else { - coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); - } -#else - coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); -#endif /* SUPPORT_METASMT */ - - - if (!UseDummySolver) { + Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); + + if (CoreSolverToUse != DUMMY_SOLVER) { if (0 != MaxCoreSolverTime) { coreSolver->setCoreSolverTimeout(MaxCoreSolverTime); } diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 16bd3ce4..38e055cd 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -10,6 +10,7 @@ #include <iostream> #include "gtest/gtest.h" +#include "klee/CommandLine.h" #include "klee/Constraints.h" #include "klee/Expr.h" #include "klee/Solver.h" @@ -127,8 +128,7 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, } TEST(SolverTest, Evaluation) { - STPSolver *stpSolver = new STPSolver(true); - Solver *solver = stpSolver; + Solver *solver = klee::createCoreSolver(CoreSolverToUse); solver = createCexCachingSolver(solver); solver = createCachingSolver(solver); |