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.

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<bool> DebugValidateSolver;
   
 extern llvm::cl::opt<int> MinQueryTimeToLog;
 
-extern llvm::cl::opt<double> MaxSTPTime;
+extern llvm::cl::opt<double> MaxCoreSolverTime;
+
+extern llvm::cl::opt<bool> UseForkedCoreSolver;
+
+extern llvm::cl::opt<bool> 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<double>
-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<bool>
+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<bool>
+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<double>
   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<double>
@@ -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<bool>
-  UseForkedSTP("use-forked-stp",
-	       cl::desc("Run STP in a forked process (default=off)"));
-
-  cl::opt<bool>
-  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 &current, ref<Expr> condition, bool isInternal) {
     }
   }
 
-  double timeout = stpTimeout;
+  double timeout = coreSolverTimeout;
   if (isSeeding)
     timeout *= it->second.size();
   solver->setTimeout(timeout);
@@ -982,7 +972,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
     ref<ConstantExpr> 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<ConstantExpr>(address), op);
@@ -2996,7 +2986,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     ref<Expr> 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<std::string,
                                    std::vector<unsigned char> > >
                                    &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<bool>
   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<bool>
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 <stdio.h>
 
 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;
   }