Patch by Tomasz Kuchta that refactors the logging code, by introducing a new logging class hierarchy.

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

1 files changed, 38 insertions, 173 deletions

diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index 0b31182e..67e9be45 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -7,192 +7,57 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
+#include "QueryLoggingSolver.h"
 
 #include "klee/Expr.h"
-#include "klee/SolverImpl.h"
-#include "klee/Statistics.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/Internal/Support/QueryLog.h"
-#include "klee/Internal/System/Time.h"
 
-#include "llvm/Support/CommandLine.h"
-
-#include <fstream>
-#include <sstream>
-#include <iostream>
 using namespace klee;
-using namespace llvm;
-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,
-                  const ref<Expr> *evalExprsEnd = 0,
-                  const Array * const* evalArraysBegin = 0,
-                  const Array * const* evalArraysEnd = 0) {
-    Statistic *S = theStatisticManager->getStatisticByName("Instructions");
-    uint64_t instructions = S ? S->getValue() : 0;
-
-    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) {
-    lastQueryTime = getWallTime() - startTime;
-    logBuffer << "#   " << (success ? "OK" : "FAIL") << " -- "
-              << "Elapsed: " << lastQueryTime << "\n";
-    
-    if (true == solver->impl->hasTimeoutOccurred()) {
-        logBuffer << "\nSolver TIMEOUT detected\n";
+class PCLoggingSolver : public QueryLoggingSolver {
+
+private :
+    ExprPPrinter *printer;
+        
+    virtual void printQuery(const Query& query,
+                            const Query* falseQuery = 0,
+                            const std::vector<const Array*>* objects = 0) {
+        
+        const ref<Expr>* evalExprsBegin = 0;
+        const ref<Expr>* evalExprsEnd = 0;
+        
+        if (0 != falseQuery) {
+            evalExprsBegin = &query.expr;
+            evalExprsEnd = &query.expr + 1;
+        }
+        
+        const Array* const *evalArraysBegin = 0;
+        const Array* const *evalArraysEnd = 0;
+        
+        if ((0 != objects) && (false == objects->empty())) {
+            evalArraysBegin = &((*objects)[0]);
+            evalArraysEnd = &((*objects)[0]) + objects->size();            
+        }
+        
+        const Query* q = (0 == falseQuery) ? &query : falseQuery;
+        
+        printer->printQuery(logBuffer, q->constraints, q->expr,
+                            evalExprsBegin, evalExprsEnd,
+                            evalArraysBegin, evalArraysEnd);
     }
-  }
-  
-  /// 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, int queryTimeToLog) 
-  : solver(_solver),
-    os(path.c_str(), std::ios::trunc),
-    logBuffer(""),
-    printer(ExprPPrinter::create(logBuffer)),
-    queryCount(0),    
-    minQueryTimeToLog(queryTimeToLog),
-    startTime(0.0f),
-    lastQueryTime(0.0f) {
-  }                                                      
-  ~PCLoggingSolver() {    
-    delete printer;
-    delete solver;
-  }
-  
-  bool computeTruth(const Query& query, bool &isValid) {
-    startQuery(query, "Truth");
-    bool success = solver->impl->computeTruth(query, isValid);
-    finishQuery(success);
-    if (success)
-      logBuffer << "#   Is Valid: " << (isValid ? "true" : "false") << "\n";
-    logBuffer << "\n";
-    
-    flushBuffer();
+    PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) 
+    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),    
+    printer(ExprPPrinter::create(logBuffer)) {
+    }                                                      
     
-    return success;
-  }
-
-  bool computeValidity(const Query& query, Solver::Validity &result) {
-    startQuery(query, "Validity");
-    bool success = solver->impl->computeValidity(query, result);
-    finishQuery(success);
-    if (success)
-      logBuffer << "#   Validity: " << result << "\n";
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
-  }
-
-  bool computeValue(const Query& query, ref<Expr> &result) {
-    startQuery(query.withFalse(), "Value", 
-               &query.expr, &query.expr + 1);
-    bool success = solver->impl->computeValue(query, result);
-    finishQuery(success);
-    if (success)
-      logBuffer << "#   Result: " << result << "\n";
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
-  }
-
-  bool computeInitialValues(const Query& query,
-                            const std::vector<const Array*> &objects,
-                            std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution) {
-    if (objects.empty()) {
-      startQuery(query, "InitialValues",
-                 0, 0);
-    } else {
-      startQuery(query, "InitialValues",
-                 0, 0,
-                 &objects[0], &objects[0] + objects.size());
-    }
-    bool success = solver->impl->computeInitialValues(query, objects, 
-                                                      values, hasSolution);
-    finishQuery(success);
-    if (success) {
-      logBuffer << "#   Solvable: " << (hasSolution ? "true" : "false") << "\n";
-      if (hasSolution) {
-        std::vector< std::vector<unsigned char> >::iterator
-          values_it = values.begin();
-        for (std::vector<const Array*>::const_iterator i = objects.begin(),
-               e = objects.end(); i != e; ++i, ++values_it) {
-          const Array *array = *i;
-          std::vector<unsigned char> &data = *values_it;
-          logBuffer << "#     " << array->name << " = [";
-          for (unsigned j = 0; j < array->size; j++) {
-            logBuffer << (int) data[j];
-            if (j+1 < array->size)
-              logBuffer << ",";
-          }
-          logBuffer << "]\n";
-        }
-      }
-    }
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
-  }
-  
-  bool hasTimeoutOccurred() {
-    return solver->impl->hasTimeoutOccurred();
-  }
+    virtual ~PCLoggingSolver() {    
+        delete printer;
+    }    
 };
 
 ///