Fixed --max-stp-time, which wasn't working unless --use-forked-stp was

also used.  Thanks to Paul Marinescu for reporting and debugging this.
The patch also disables the STP timeout by default.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 20 insertions, 4 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 462db18b..917a746d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -209,7 +209,7 @@ namespace {
 
   cl::opt<double>
   MaxInstructionTime("max-instruction-time",
-                     cl::desc("Only allow a single instruction to take this much time (default=0 (off))"),
+                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-stp"),
                      cl::init(0));
   
   cl::opt<double>
@@ -219,8 +219,8 @@ namespace {
   
   cl::opt<double>
   MaxSTPTime("max-stp-time",
-             cl::desc("Maximum amount of time for a single query (default=120s)"),
-             cl::init(120.0));
+             cl::desc("Maximum amount of time for a single query (default=0s (off)). Enables --use-forked-stp"),
+             cl::init(0.0));
   
   cl::opt<unsigned int>
   StopAfterNInstructions("stop-after-n-instructions",
@@ -249,7 +249,7 @@ namespace {
 
   cl::opt<bool>
   UseForkedSTP("use-forked-stp", 
-                 cl::desc("Run STP in forked process"));
+                 cl::desc("Run STP in a forked process (default=off)"));
 
   cl::opt<bool>
   STPOptimizeDivides("stp-optimize-divides", 
@@ -317,6 +317,7 @@ Executor::Executor(const InterpreterOptions &opts,
     stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
       ? std::min(MaxSTPTime,MaxInstructionTime)
       : std::max(MaxSTPTime,MaxInstructionTime)) {
+  if (stpTimeout) UseForkedSTP = true;
   STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
   Solver *solver = 
     constructSolverChain(stpSolver,
diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c
new file mode 100644
index 00000000..96f75cd7
--- /dev/null
+++ b/test/Feature/SolverTimeout.c
@@ -0,0 +1,15 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --max-stp-time=1 %t1.bc
+#include <stdio.h>
+
+int main() {
+  long long int x, y = 102*75678 + 78, i = 101;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  if (x*x*x*x*x*x*x*x*x*x*x*x*x*x*x*x + (x*x % (x+12)) == y*y*y*y*y*y*y*y*y*y*y*y*y*y*y*y % i)
+    printf("Yes\n");
+  else printf("No\n");
+  
+  return 0;
+}