diff options
| -rw-r--r-- | include/klee/Common.h | 2 | ||||
| -rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 14 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 9 | ||||
| -rw-r--r-- | lib/Core/TimingSolver.h | 11 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 22 |
5 files changed, 25 insertions, 33 deletions
diff --git a/include/klee/Common.h b/include/klee/Common.h index 1418f1b6..7149708a 100644 --- a/include/klee/Common.h +++ b/include/klee/Common.h @@ -22,7 +22,7 @@ namespace klee { const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc"; const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc"; - Solver *constructSolverChain(STPSolver *stpSolver, + Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 70c728df..c0d0ef61 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -16,13 +16,13 @@ namespace klee { - Solver *constructSolverChain(STPSolver *stpSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryPCLogPath, - std::string baseSolverQueryPCLogPath) + Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryPCLogPath, + std::string baseSolverQueryPCLogPath) { - Solver *solver = stpSolver; + Solver *solver = coreSolver; if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { @@ -55,7 +55,7 @@ namespace klee solver = createIndependentSolver(solver); if (DebugValidateSolver) - solver = createValidatingSolver(solver, stpSolver); + solver = createValidatingSolver(solver, coreSolver); if (optionIsSet(queryLoggingOptions, ALL_PC)) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 309c5fd5..b57b1956 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -251,16 +251,17 @@ Executor::Executor(const InterpreterOptions &opts, coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 ? std::min(MaxCoreSolverTime,MaxInstructionTime) : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; - STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = - constructSolverChain(stpSolver, + 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, stpSolver); + this->solver = new TimingSolver(solver); memory = new MemoryManager(); } @@ -3280,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state, case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); + char *log = solver->getConstraintLog(query); res = std::string(log); free(log); } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 2684e071..c98dd881 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -17,15 +17,13 @@ namespace klee { class ExecutionState; - class Solver; - class STPSolver; + class Solver; /// TimingSolver - A simple class which wraps a solver and handles /// tracking the statistics that we care about. class TimingSolver { public: Solver *solver; - STPSolver *stpSolver; bool simplifyExprs; public: @@ -34,15 +32,14 @@ namespace klee { /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, STPSolver *_stpSolver, - bool _simplifyExprs = true) - : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {} + TimingSolver(Solver *_solver, bool _simplifyExprs = true) + : solver(_solver), simplifyExprs(_simplifyExprs) {} ~TimingSolver() { delete solver; } void setTimeout(double t) { - stpSolver->setCoreSolverTimeout(t); + solver->setCoreSolverTimeout(t); } char *getConstraintLog(const Query& query) { diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 6c2a29e5..accc48e4 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -211,25 +211,19 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *S = 0; - Solver *STP = 0; + Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + if (!UseDummySolver) { - STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver); if (0 != MaxCoreSolverTime) { - stpSolver->setCoreSolverTimeout(MaxCoreSolverTime); + coreSolver->setCoreSolverTimeout(MaxCoreSolverTime); } - STP = S = stpSolver; - } - else { - STP = S = createDummySolver(); } - S= constructSolverChain((STPSolver*) STP, - getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); - + Solver *S = constructSolverChain(coreSolver, + getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); unsigned Index = 0; for (std::vector<Decl*>::iterator it = Decls.begin(), |