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. --- include/klee/CommandLine.h | 6 +++++- lib/Basic/CmdLineOptions.cpp | 17 ++++++++++++++--- lib/Core/Executor.cpp | 36 +++++++++++++----------------------- lib/Core/Executor.h | 5 +++-- lib/Solver/CexCachingSolver.cpp | 2 +- test/Feature/SolverTimeout.c | 2 +- tools/kleaver/main.cpp | 6 +++--- 7 files changed, 40 insertions(+), 34 deletions(-) diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index f303ae6c..38b22c6f 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -22,7 +22,11 @@ extern llvm::cl::opt DebugValidateSolver; extern llvm::cl::opt MinQueryTimeToLog; -extern llvm::cl::opt MaxSTPTime; +extern llvm::cl::opt MaxCoreSolverTime; + +extern llvm::cl::opt UseForkedCoreSolver; + +extern llvm::cl::opt CoreSolverOptimizeDivides; ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 6fe20b7e..ac0474fb 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -40,9 +40,20 @@ MinQueryTimeToLog("min-query-time-to-log", "Set this param to a negative value to log timeouts only.")); llvm::cl::opt -MaxSTPTime("max-stp-time", - llvm::cl::desc("Maximum amount of time for a single query (default=0s (off)). Enables --use-forked-stp"), - llvm::cl::init(0.0)); +MaxCoreSolverTime("max-solver-time", + llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), + llvm::cl::init(0.0), + llvm::cl::value_desc("seconds")); + +llvm::cl::opt +UseForkedCoreSolver("use-forked-solver", + llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"), + llvm::cl::init(true)); + +llvm::cl::opt +CoreSolverOptimizeDivides("solver-optimize-divides", + llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), + llvm::cl::init(true)); /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking 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) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c434c34c..a9d6b791 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -173,8 +173,9 @@ private: /// false, it is buggy (it needs to validate its writes). bool ivcEnabled; - /// The maximum time to allow for a single stp query. - double stpTimeout; + /// The maximum time to allow for a single core solver query. + /// (e.g. for a single STP query) + double coreSolverTimeout; llvm::Function* getTargetFunction(llvm::Value *calledVal, ExecutionState &state); diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 497ccb4a..b38df672 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -31,7 +31,7 @@ namespace { cl::opt CexCacheTryAll("cex-cache-try-all", - cl::desc("try substituting all counterexamples before asking STP"), + cl::desc("try substituting all counterexamples before asking the SMT solver"), cl::init(false)); cl::opt diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index 96f75cd7..34405c1f 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,5 +1,5 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc -// RUN: %klee --max-stp-time=1 %t1.bc +// RUN: %klee --max-solver-time=1 %t1.bc #include int main() { diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 5b9e43a6..47c4f07f 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -214,9 +214,9 @@ static bool EvaluateInputAST(const char *Filename, Solver *S = 0; Solver *STP = 0; if (!UseDummySolver) { - STPSolver* stpSolver = new STPSolver(true); - if (0 != MaxSTPTime) { - stpSolver->setTimeout(MaxSTPTime); + STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver); + if (0 != MaxCoreSolverTime) { + stpSolver->setTimeout(MaxCoreSolverTime); } STP = S = stpSolver; } -- cgit 1.4.1