From 9abe9572e68748002d8bbb789587e2a036ff760d Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 16:15:56 +0100 Subject: Renaming solver-related command-line options in order to decouple them from STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well. --- lib/Core/Executor.cpp | 36 +++++++++++++----------------------- 1 file changed, 13 insertions(+), 23 deletions(-) (limited to 'lib/Core/Executor.cpp') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d0ad811d..309c5fd5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -189,7 +189,7 @@ namespace { cl::opt MaxInstructionTime("max-instruction-time", - cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-stp"), + cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"), cl::init(0)); cl::opt @@ -221,16 +221,6 @@ namespace { MaxMemoryInhibit("max-memory-inhibit", cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"), cl::init(true)); - - cl::opt - UseForkedSTP("use-forked-stp", - cl::desc("Run STP in a forked process (default=off)")); - - cl::opt - STPOptimizeDivides("stp-optimize-divides", - cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"), - cl::init(true)); - } @@ -258,11 +248,11 @@ Executor::Executor(const InterpreterOptions &opts, inhibitForking(false), haltExecution(false), ivcEnabled(false), - stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0 - ? std::min(MaxSTPTime,MaxInstructionTime) - : std::max(MaxSTPTime,MaxInstructionTime)) { - if (stpTimeout) UseForkedSTP = true; - STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides); + coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 + ? std::min(MaxCoreSolverTime,MaxInstructionTime) + : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; + STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = constructSolverChain(stpSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), @@ -666,7 +656,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { } } - double timeout = stpTimeout; + double timeout = coreSolverTimeout; if (isSeeding) timeout *= it->second.size(); solver->setTimeout(timeout); @@ -982,7 +972,7 @@ ref Executor::toUnique(const ExecutionState &state, ref value; bool isTrue = false; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); if (solver->getValue(state, e, value) && solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) && isTrue) @@ -2979,7 +2969,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, // fast path: single in-bounds resolution ObjectPair op; bool success; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); if (!state.addressSpace.resolveOne(state, solver, address, op, success)) { address = toConstant(state, address, "resolveOne failure"); success = state.addressSpace.resolveOne(cast(address), op); @@ -2996,7 +2986,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, ref offset = mo->getOffsetExpr(address); bool inBounds; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); bool success = solver->mustBeTrue(state, mo->getBoundsCheckOffset(offset, bytes), inBounds); @@ -3035,9 +3025,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, // resolution with out of bounds) ResolutionList rl; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); bool incomplete = state.addressSpace.resolve(state, solver, address, rl, - 0, stpTimeout); + 0, coreSolverTimeout); solver->setTimeout(0); // XXX there is some query wasteage here. who cares? @@ -3328,7 +3318,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, std::pair > > &res) { - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); if (!NoPreferCex) { -- cgit 1.4.1 From 4a426569a38760b9ecf34af46b4eeca76e21e8e6 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 18:25:16 +0100 Subject: TimingSolver and constructSolverChain() no longer coupled with pointers to STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver. --- include/klee/Common.h | 2 +- lib/Basic/ConstructSolverChain.cpp | 14 +++++++------- lib/Core/Executor.cpp | 9 +++++---- lib/Core/TimingSolver.h | 11 ++++------- tools/kleaver/main.cpp | 22 ++++++++-------------- 5 files changed, 25 insertions(+), 33 deletions(-) (limited to 'lib/Core/Executor.cpp') 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::iterator it = Decls.begin(), -- cgit 1.4.1