Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that enables KLEE to log only the queries exceeding a certain duration, or only those that time out.

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

8 files changed, 161 insertions, 47 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 968283b7..b8db18fe 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -164,6 +164,15 @@ namespace {
               cl::init(true),
 	      cl::desc("Use counterexample caching (default=on)"));
 
+  // FIXME: Command line argument duplicated in main.cpp of Kleaver
+  cl::opt<int>
+  MinQueryTimeToLog("min-query-time-to-log",
+                    cl::init(0),
+                    cl::value_desc("milliseconds"),
+                    cl::desc("Set time threshold (in ms) for queries logged in files. "
+                             "Only queries longer than threshold will be logged. (default=0). "
+                             "Set this param to a negative value to log timeouts only."));
+   
   cl::opt<bool>
   NoExternals("no-externals", 
            cl::desc("Do not allow external function calls (default=off)"));
@@ -301,7 +310,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
   if (optionIsSet(queryLoggingOptions,SOLVER_PC))
   {
     solver = createPCLoggingSolver(solver, 
-                                   baseSolverQueryPCLogPath);
+                                   baseSolverQueryPCLogPath,
+		                   MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
   }
 
@@ -329,7 +339,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
   if (optionIsSet(queryLoggingOptions,ALL_PC))
   {
     solver = createPCLoggingSolver(solver, 
-                                   queryPCLogPath);
+                                   queryPCLogPath,
+                                   MinQueryTimeToLog);
     klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
   }
   
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index c0b77429..f7b88855 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -82,6 +82,7 @@ public:
     return solver->impl->computeInitialValues(query, objects, values, 
                                               hasSolution);
   }
+  bool hasTimeoutOccurred();
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -234,6 +235,10 @@ bool CachingSolver::computeTruth(const Query& query,
   return true;
 }
 
+bool CachingSolver::hasTimeoutOccurred() {
+  return solver->impl->hasTimeoutOccurred();
+}
+
 ///
 
 Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 19f16821..c84ae409 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -82,6 +82,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
+  bool hasTimeoutOccurred();
 };
 
 ///
@@ -339,6 +340,10 @@ CexCachingSolver::computeInitialValues(const Query& query,
   return true;
 }
 
+bool CexCachingSolver::hasTimeoutOccurred() {
+  return solver->impl->hasTimeoutOccurred();
+}
+
 ///
 
 Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index a565bab2..45e2ea9b 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -134,3 +134,7 @@ StagedSolverImpl::computeInitialValues(const Query& query,
   return secondary->impl->computeInitialValues(query, objects, values,
                                                hasSolution);
 }
+
+bool StagedSolverImpl::hasTimeoutOccurred() {
+  return secondary->impl->hasTimeoutOccurred();
+}
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 70f3cab2..0eb86720 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -284,6 +284,7 @@ public:
     return solver->impl->computeInitialValues(query, objects, values,
                                               hasSolution);
   }
+  bool hasTimeoutOccurred();
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -313,6 +314,10 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
   return solver->impl->computeValue(Query(tmp, query.expr), result);
 }
 
+bool IndependentSolver::hasTimeoutOccurred() {
+  return solver->impl->hasTimeoutOccurred();
+}
+
 Solver *klee::createIndependentSolver(Solver *s) {
   return new Solver(new IndependentSolver(s));
 }
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index e7128982..0b31182e 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -19,7 +19,8 @@
 #include "llvm/Support/CommandLine.h"
 
 #include <fstream>
-
+#include <sstream>
+#include <iostream>
 using namespace klee;
 using namespace llvm;
 using namespace klee::util;
@@ -29,9 +30,17 @@ using namespace klee::util;
 class PCLoggingSolver : public SolverImpl {
   Solver *solver;
   std::ofstream os;
+  std::ostringstream logBuffer; // buffer to store logs before flushing to 
+                                // file
   ExprPPrinter *printer;
   unsigned queryCount;
+  int minQueryTimeToLog; // we log to file only those queries
+                         // which take longer than specified time (ms);
+                         // if this param is negative, log only those queries
+                         // on which solver's timed out
+  
   double startTime;
+  double lastQueryTime;
 
   void startQuery(const Query& query, const char *typeName,
                   const ref<Expr> *evalExprsBegin = 0,
@@ -40,30 +49,62 @@ class PCLoggingSolver : public SolverImpl {
                   const Array * const* evalArraysEnd = 0) {
     Statistic *S = theStatisticManager->getStatisticByName("Instructions");
     uint64_t instructions = S ? S->getValue() : 0;
-    os << "# Query " << queryCount++ << " -- "
-       << "Type: " << typeName << ", "
-       << "Instructions: " << instructions << "\n";
-    printer->printQuery(os, query.constraints, query.expr,
+
+    logBuffer << "# Query " << queryCount++ << " -- "
+              << "Type: " << typeName << ", "
+              << "Instructions: " << instructions << "\n";
+    printer->printQuery(logBuffer, query.constraints, query.expr,
                         evalExprsBegin, evalExprsEnd,
                         evalArraysBegin, evalArraysEnd);
-    
+
     startTime = getWallTime();
   }
 
   void finishQuery(bool success) {
-    double delta = getWallTime() - startTime;
-    os << "#   " << (success ? "OK" : "FAIL") << " -- "
-       << "Elapsed: " << delta << "\n";
+    lastQueryTime = getWallTime() - startTime;
+    logBuffer << "#   " << (success ? "OK" : "FAIL") << " -- "
+              << "Elapsed: " << lastQueryTime << "\n";
+    
+    if (true == solver->impl->hasTimeoutOccurred()) {
+        logBuffer << "\nSolver TIMEOUT detected\n";
+    }
+  }
+  
+  /// flushBuffer - flushes the temporary logs buffer. Depending on threshold
+  /// settings, contents of the buffer are either discarded or written to a file.  
+  void flushBuffer(void) {           
+      logBuffer.flush();            
+
+      if ((0 == minQueryTimeToLog) ||
+          (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
+          // we either do not limit logging queries or the query time
+          // is larger than threshold (in ms)
+          
+          if ((minQueryTimeToLog >= 0) || 
+              (true == (solver->impl->hasTimeoutOccurred()))) {
+              // we do additional check here to log only timeouts in case
+              // user specified negative value for minQueryTimeToLog param
+              os << logBuffer.str();
+          }                    
+      }
+      
+      // prepare the buffer for reuse
+      logBuffer.clear();
+      logBuffer.str("");
   }
   
 public:
-  PCLoggingSolver(Solver *_solver, std::string path) 
+  PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) 
   : solver(_solver),
     os(path.c_str(), std::ios::trunc),
-    printer(ExprPPrinter::create(os)),
-    queryCount(0) {
+    logBuffer(""),
+    printer(ExprPPrinter::create(logBuffer)),
+    queryCount(0),    
+    minQueryTimeToLog(queryTimeToLog),
+    startTime(0.0f),
+    lastQueryTime(0.0f) {
   }                                                      
-  ~PCLoggingSolver() {
+  ~PCLoggingSolver() {    
     delete printer;
     delete solver;
   }
@@ -73,8 +114,11 @@ public:
     bool success = solver->impl->computeTruth(query, isValid);
     finishQuery(success);
     if (success)
-      os << "#   Is Valid: " << (isValid ? "true" : "false") << "\n";
-    os << "\n";
+      logBuffer << "#   Is Valid: " << (isValid ? "true" : "false") << "\n";
+    logBuffer << "\n";
+    
+    flushBuffer();
+    
     return success;
   }
 
@@ -83,8 +127,11 @@ public:
     bool success = solver->impl->computeValidity(query, result);
     finishQuery(success);
     if (success)
-      os << "#   Validity: " << result << "\n";
-    os << "\n";
+      logBuffer << "#   Validity: " << result << "\n";
+    logBuffer << "\n";
+    
+    flushBuffer();
+    
     return success;
   }
 
@@ -94,8 +141,11 @@ public:
     bool success = solver->impl->computeValue(query, result);
     finishQuery(success);
     if (success)
-      os << "#   Result: " << result << "\n";
-    os << "\n";
+      logBuffer << "#   Result: " << result << "\n";
+    logBuffer << "\n";
+    
+    flushBuffer();
+    
     return success;
   }
 
@@ -115,7 +165,7 @@ public:
                                                       values, hasSolution);
     finishQuery(success);
     if (success) {
-      os << "#   Solvable: " << (hasSolution ? "true" : "false") << "\n";
+      logBuffer << "#   Solvable: " << (hasSolution ? "true" : "false") << "\n";
       if (hasSolution) {
         std::vector< std::vector<unsigned char> >::iterator
           values_it = values.begin();
@@ -123,23 +173,31 @@ public:
                e = objects.end(); i != e; ++i, ++values_it) {
           const Array *array = *i;
           std::vector<unsigned char> &data = *values_it;
-          os << "#     " << array->name << " = [";
+          logBuffer << "#     " << array->name << " = [";
           for (unsigned j = 0; j < array->size; j++) {
-            os << (int) data[j];
+            logBuffer << (int) data[j];
             if (j+1 < array->size)
-              os << ",";
+              logBuffer << ",";
           }
-          os << "]\n";
+          logBuffer << "]\n";
         }
       }
     }
-    os << "\n";
+    logBuffer << "\n";
+    
+    flushBuffer();
+    
     return success;
   }
+  
+  bool hasTimeoutOccurred() {
+    return solver->impl->hasTimeoutOccurred();
+  }
 };
 
 ///
 
-Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path) {
-  return new Solver(new PCLoggingSolver(_solver, path));
+Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path,
+                                    int minQueryTimeToLog) {
+  return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog));
 }
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index 0fb09424..b3f7eb3b 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -158,6 +158,11 @@ class SMTLIBLoggingSolver : public SolverImpl
 			os << "\n";
 			return success;
 		}
+                
+                bool hasTimeoutOccurred() 
+                {
+                        return solver->impl->hasTimeoutOccurred();
+                }
 };
 
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 7430a58b..366a7b05 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -273,6 +273,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
+  bool hasTimeoutOccurred();
 };
 
 bool ValidatingSolver::computeTruth(const Query& query,
@@ -370,6 +371,10 @@ ValidatingSolver::computeInitialValues(const Query& query,
   return true;
 }
 
+bool ValidatingSolver::hasTimeoutOccurred() {
+    return solver->impl->hasTimeoutOccurred();
+}
+
 Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
   return new Solver(new ValidatingSolver(s, oracle));
 }
@@ -403,6 +408,10 @@ public:
     ++stats::queryCounterexamples;
     return false; 
   }
+  bool hasTimeoutOccurred() {
+      return false;
+  }
+  
 };
 
 Solver *klee::createDummySolver() {
@@ -419,6 +428,7 @@ private:
   STPBuilder *builder;
   double timeout;
   bool useForkedSTP;
+  bool timeoutOccurred;
 
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
@@ -433,6 +443,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
+  bool hasTimeoutOccurred();
 };
 
 static unsigned char *shared_memory_ptr;
@@ -449,7 +460,8 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
     vc(vc_createValidityChecker()),
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
-    useForkedSTP(_useForkedSTP)
+    useForkedSTP(_useForkedSTP),
+    timeoutOccurred(false)
 {
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
@@ -577,14 +589,14 @@ static void stpTimeoutHandler(int x) {
   _exit(52);
 }
 
-static bool runAndGetCexForked(::VC vc, 
-                               STPBuilder *builder,
-                               ::VCExpr q,
-                               const std::vector<const Array*> &objects,
-                               std::vector< std::vector<unsigned char> >
-                                 &values,
-                               bool &hasSolution,
-                               double timeout) {
+static SolverRunStatus runAndGetCexForked(::VC vc, 
+                                          STPBuilder *builder,
+                                          ::VCExpr q,
+                                          const std::vector<const Array*> &objects,
+                                          std::vector< std::vector<unsigned char> >
+                                          &values,
+                                          bool &hasSolution,
+                                          double timeout) {
   unsigned char *pos = shared_memory_ptr;
   unsigned sum = 0;
   for (std::vector<const Array*>::const_iterator
@@ -597,11 +609,11 @@ static bool runAndGetCexForked(::VC vc,
   int pid = fork();
   if (pid==-1) {
     fprintf(stderr, "error: fork failed (for STP)");
-    return false;
+    return SOLVER_RUN_STATUS_FORK_FAILED;
   }
 
   if (pid == 0) {
-    if (timeout) {
+    if (timeout) {      
       ::alarm(0); /* Turn off alarm so we can safely set signal handler */
       ::signal(SIGALRM, stpTimeoutHandler);
       ::alarm(std::max(1, (int)timeout));
@@ -629,7 +641,7 @@ static bool runAndGetCexForked(::VC vc,
     
     if (res < 0) {
       fprintf(stderr, "error: waitpid() for STP failed");
-      return false;
+      return SOLVER_RUN_STATUS_WAITPID_FAILED;
     }
     
     // From timed_run.py: It appears that linux at least will on
@@ -637,7 +649,7 @@ static bool runAndGetCexForked(::VC vc,
     // signal, so test signal first.
     if (WIFSIGNALED(status) || !WIFEXITED(status)) {
       fprintf(stderr, "error: STP did not return successfully");
-      return false;
+      return SOLVER_RUN_STATUS_INTERRUPTED;
     }
 
     int exitcode = WEXITSTATUS(status);
@@ -647,10 +659,11 @@ static bool runAndGetCexForked(::VC vc,
       hasSolution = false;
     } else if (exitcode==52) {
       fprintf(stderr, "error: STP timed out");
-      return false;
+      // mark that a timeout occurred
+      return SOLVER_RUN_STATUS_TIMEOUT;
     } else {
       fprintf(stderr, "error: STP did not return a recognized code");
-      return false;
+      return SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
     }
     
     if (hasSolution) {
@@ -665,7 +678,7 @@ static bool runAndGetCexForked(::VC vc,
       }
     }
 
-    return true;
+    return SOLVER_RUN_STATUS_SUCCESS;
   }
 }
 
@@ -676,6 +689,8 @@ STPSolverImpl::computeInitialValues(const Query &query,
                                     std::vector< std::vector<unsigned char> > 
                                       &values,
                                     bool &hasSolution) {
+  timeoutOccurred = false;
+    
   TimerStatIncrementer t(stats::queryTime);
 
   vc_push(vc);
@@ -698,8 +713,10 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   bool success;
   if (useForkedSTP) {
-    success = runAndGetCexForked(vc, builder, stp_e, objects, values, 
-                                 hasSolution, timeout);
+    SolverRunStatus runStatus = runAndGetCexForked(vc, builder, stp_e, objects, values, 
+                                                   hasSolution, timeout);
+    success = (SOLVER_RUN_STATUS_SUCCESS == runStatus);
+    timeoutOccurred = (SOLVER_RUN_STATUS_TIMEOUT == runStatus);
   } else {
     runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
     success = true;
@@ -716,3 +733,7 @@ STPSolverImpl::computeInitialValues(const Query &query,
   
   return success;
 }
+
+bool STPSolverImpl::hasTimeoutOccurred() {
+    return timeoutOccurred;
+}