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

5 files changed, 84 insertions, 321 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index db14f003..94e7d477 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -218,7 +218,8 @@ namespace klee {
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .smt2 format.
-  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path);
+  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
+                                    int minQueryTimeToLog);
 
 
   /// createDummySolver - Create a dummy solver implementation which always
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b8db18fe..5803e6ff 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -317,7 +317,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
 
   if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
   {
-    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath);
+    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath,
+                                       MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
   }
 
@@ -346,7 +347,8 @@ Solver *constructSolverChain(STPSolver *stpSolver,
   
   if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
   {
-    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath);
+    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
+                                       MinQueryTimeToLog);
     klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
   }
 
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;
+    }    
 };
 
 ///
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index b3f7eb3b..f64e11e0 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -1,4 +1,4 @@
-//===-- SMTLIBLoggingSolver.cpp -----------------------------------------------===//
+//===-- SMTLIBLoggingSolver.cpp -------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,166 +7,61 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
-
-#include "klee/Expr.h"
-#include "klee/SolverImpl.h"
-#include "klee/Statistics.h"
-
+#include "QueryLoggingSolver.h"
 #include "klee/util/ExprSMTLIBLetPrinter.h"
 
-#include "klee/Internal/Support/QueryLog.h"
-#include "klee/Internal/System/Time.h"
-
-#include "llvm/Support/CommandLine.h"
-
-#include <fstream>
-
 using namespace klee;
-using namespace llvm;
-using namespace klee::util;
 
-///This SolverImpl will log queries to a file in the SMTLIBv2 format
-///and pass the query down to the underlying solver.
-///
-///This is basically just a "copy" of PCLoggingSolver with a few modifications.
-class SMTLIBLoggingSolver : public SolverImpl
+/// This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format
+/// and pass the query down to the underlying solver.
+class SMTLIBLoggingSolver : public QueryLoggingSolver
 {
-	Solver *solver;
-	std::ofstream os;
-	ExprSMTLIBPrinter* printer;
-	unsigned queryCount;
-	double startTime;
-
-	void startQuery(const Query& query, const char *typeName, const std::vector<const Array*>* objects=NULL)
-	{
-		Statistic *S = theStatisticManager->getStatisticByName("Instructions");
-		uint64_t instructions = S ? S->getValue() : 0;
-		os << ";SMTLIBv2 Query " << queryCount++ << " -- "
-		   << "Type: " << typeName << ", "
-		   << "Instructions: " << instructions << "\n";
-		printer->setQuery(query);
-
-		if(objects!=NULL)
-			printer->setArrayValuesToGet(*objects);
-
-		printer->generateOutput();
-		os << "\n";
-
-		startTime = getWallTime();
-	}
-
-	void finishQuery(bool success)
-	{
-		double delta = getWallTime() - startTime;
-		os << ";   " << (success ? "OK" : "FAIL") << " -- "
-		   << "Elapsed: " << delta << "\n";
-	}
+        private:
+    
+                ExprSMTLIBPrinter* printer;
 
+                virtual void printQuery(const Query& query,
+                                        const Query* falseQuery = 0,
+                                        const std::vector<const Array*>* objects = 0) 
+                {
+                        if (0 == falseQuery) 
+                        {
+                                printer->setQuery(query);
+                        }
+                        else
+                        {
+                                printer->setQuery(*falseQuery);                
+                        }
+
+                        if (0 != objects)
+                        {
+                                printer->setArrayValuesToGet(*objects);
+                        }
+
+                        printer->generateOutput();
+                }    
+        
 	public:
-		SMTLIBLoggingSolver(Solver *_solver, std::string path)
-		: solver(_solver),
-		os(path.c_str(), std::ios::trunc),
-		printer(),
-		queryCount(0),
-		startTime(0)
+		SMTLIBLoggingSolver(Solver *_solver,
+                                    std::string path,
+                                    int queryTimeToLog)                
+		: QueryLoggingSolver(_solver, path, ";", queryTimeToLog),
+		printer()
 		{
 		  //Setup the printer
 		  printer = createSMTLIBPrinter();
-		  printer->setOutput(os);
+		  printer->setOutput(logBuffer);
 		}
 
 		~SMTLIBLoggingSolver()
 		{
 			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)
-			  os << ";   Is Valid: " << (isValid ? "true" : "false") << "\n";
-			os << "\n";
-			return success;
-		}
-
-		bool computeValidity(const Query& query, Solver::Validity &result)
-		{
-			startQuery(query, "Validity");
-			bool success = solver->impl->computeValidity(query, result);
-			finishQuery(success);
-			if (success)
-			  os << ";   Validity: " << result << "\n";
-			os << "\n";
-			return success;
-		}
-
-		bool computeValue(const Query& query, ref<Expr> &result)
-		{
-			startQuery(query.withFalse(), "Value");
-
-			bool success = solver->impl->computeValue(query, result);
-			finishQuery(success);
-			if (success)
-			  os << ";   Result: " << result << "\n";
-			os << "\n";
-			return success;
-		}
-
-		bool computeInitialValues(const Query& query,
-								const std::vector<const Array*> &objects,
-								std::vector< std::vector<unsigned char> > &values,
-								bool &hasSolution)
-		{
-
-		  startQuery(query, "InitialValues", &objects);
-
-
-			bool success = solver->impl->computeInitialValues(query, objects,
-															  values, hasSolution);
-			finishQuery(success);
-			if (success)
-			{
-				os << ";   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;
-						os << ";     " << array->name << " = [";
-
-						for (unsigned j = 0; j < array->size; j++)
-						{
-							os << (int) data[j];
-							if (j+1 < array->size)
-							  os << ",";
-						}
-
-						os << "]\n";
-					}
-				}
-			}
-
-			os << "\n";
-			return success;
 		}
-                
-                bool hasTimeoutOccurred() 
-                {
-                        return solver->impl->hasTimeoutOccurred();
-                }
 };
 
 
-Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path)
+Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path,
+                                        int minQueryTimeToLog)
 {
-  return new Solver(new SMTLIBLoggingSolver(_solver, path));
+  return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog));
 }
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index d8dfe4b4..ad671a5e 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -6,8 +6,8 @@
 // RUN: %kleaver -print-ast klee-last/solver-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
-// RUN: grep "^;SMTLIBv2 Query" klee-last/all-queries.smt2 | wc -l | grep -q 17
-// RUN: grep "^;SMTLIBv2 Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10
+// RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17
+// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10
 
 #include <assert.h>