Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that...

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

include/klee/IncompleteSolver.h

@@ -101,6 +101,7 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
+  bool hasTimeoutOccurred();
 };
 
 }

include/klee/Solver.h

@@ -216,7 +216,8 @@ namespace klee {
   
   /// createPCLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .pc format.
-  Solver *createPCLoggingSolver(Solver *s, std::string path);
+  Solver *createPCLoggingSolver(Solver *s, std::string path,
+                                int minQueryTimeToLog);
 
   /// createFPRewritingSolver - Create a solver which rewrites queries that
   /// involve FP comparisons.
@@ -229,6 +230,13 @@ namespace klee {
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
   Solver *createDummySolver();
+  
+  enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS, 
+                         SOLVER_RUN_STATUS_TIMEOUT,
+                         SOLVER_RUN_STATUS_FORK_FAILED,
+                         SOLVER_RUN_STATUS_INTERRUPTED,
+                         SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE,
+                         SOLVER_RUN_STATUS_WAITPID_FAILED };
 }
 
 #endif

include/klee/SolverImpl.h

@@ -55,7 +55,10 @@ namespace klee {
                                         &objects,
                                       std::vector< std::vector<unsigned char> > 
                                         &values,
-                                      bool &hasSolution) = 0;  
+                                      bool &hasSolution) = 0;
+    
+    /// haveTimeOutOccurred - retrieve timeout status for the last query.
+    virtual bool hasTimeoutOccurred() = 0;
 };
 
 }

lib/Core/Executor.cpp

@@ -172,6 +172,15 @@ namespace {
   UseFPRewriter("use-fp-rewriter",
                 cl::init(false));
 
+  // 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 functin calls"));
@@ -316,7 +325,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());
   }
 
@@ -347,7 +357,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());
   }
   

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) {

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) {

lib/Solver/FPRewritingSolver.cpp

@@ -57,6 +57,8 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
+
+  virtual bool hasTimeoutOccurred() { return solver->impl->hasTimeoutOccurred(); }
 };
 
 enum MinMax { mmUnknown, mmMin, mmMax };

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();
+}

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));
 }

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));
 }

lib/Solver/SMTLIBLoggingSolver.cpp

@@ -158,6 +158,11 @@ class SMTLIBLoggingSolver : public SolverImpl
 			os << "\n";
 			return success;
 		}
+                
+                bool hasTimeoutOccurred() 
+                {
+                        return solver->impl->hasTimeoutOccurred();
+                }
 };
 
 

lib/Solver/Solver.cpp

@@ -282,6 +282,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,
@@ -379,6 +380,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));
 }
@@ -412,6 +417,10 @@ public:
     ++stats::queryCounterexamples;
     return false; 
   }
+  bool hasTimeoutOccurred() {
+      return false;
+  }
+  
 };
 
 Solver *klee::createDummySolver() {
@@ -428,6 +437,7 @@ private:
   STPBuilder *builder;
   double timeout;
   bool useForkedSTP;
+  bool timeoutOccurred;
 
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
@@ -442,6 +452,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;
@@ -458,7 +469,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");
@@ -586,14 +598,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
@@ -606,11 +618,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));
@@ -638,7 +650,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
@@ -646,7 +658,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);
@@ -656,10 +668,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) {
@@ -674,7 +687,7 @@ static bool runAndGetCexForked(::VC vc,
       }
     }
 
-    return true;
+    return SOLVER_RUN_STATUS_SUCCESS;
   }
 }
 
@@ -685,6 +698,8 @@ STPSolverImpl::computeInitialValues(const Query &query,
                                     std::vector< std::vector<unsigned char> > 
                                       &values,
                                     bool &hasSolution) {
+  timeoutOccurred = false;
+    
   TimerStatIncrementer t(stats::queryTime);
 
   vc_push(vc);
@@ -707,8 +722,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;
@@ -725,3 +742,7 @@ STPSolverImpl::computeInitialValues(const Query &query,
   
   return success;
 }
+
+bool STPSolverImpl::hasTimeoutOccurred() {
+    return timeoutOccurred;
+}

tools/kleaver/main.cpp

@@ -87,9 +87,20 @@ namespace {
   UseFastCexSolver("use-fast-cex-solver",
 		   cl::init(false));
   
+  // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different
+  // output file name used.
   cl::opt<bool>
   UseSTPQueryPCLog("use-stp-query-pc-log",
                    cl::init(false));
+   
+  // FIXME: Command line argument duplicated in Executor.cpp of Klee
+  cl::opt<unsigned 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)"));
+  
 }
 
 static std::string escapedString(const char *start, unsigned length) {
@@ -180,7 +191,7 @@ static bool EvaluateInputAST(const char *Filename,
   Solver *S, *STP = S = 
     UseDummySolver ? createDummySolver() : new STPSolver(true);
   if (UseSTPQueryPCLog)
-    S = createPCLoggingSolver(S, "stp-queries.pc");
+    S = createPCLoggingSolver(S, "stp-queries.pc", MinQueryTimeToLog);
   if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);