Patch by Dan Liew which improves the logging options: "Removed

-use-query-pc-log and -use-stp-query-pc-log and replaced with better
command line option -use-query-log=option.  Multiple comma seperated
options can be specified after -use-query-log=.  In addition queries
can now be logged in SMT-LIBv2 format as well as KQuery format. The
names of logging files has changed and also KLEE now informs users
which files are being written to.

Because of the changes the test/Feature/ExprLogging.c test broke so it
was necessary to fix it."



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

3 files changed, 67 insertions, 22 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8478ea67..74769aa1 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -164,16 +164,6 @@ namespace {
 	      cl::desc("Use counterexample caching (default=on)"));
 
   cl::opt<bool>
-  UseQueryPCLog("use-query-pc-log",
-                cl::init(false),
-		cl::desc("Log all queries into queries.pc (default=off)"));
-  
-  cl::opt<bool>
-  UseSTPQueryPCLog("use-stp-query-pc-log",
-                   cl::init(false),
-		   cl::desc("Log all queries sent to STP into queries.pc (default=off)"));
-
-  cl::opt<bool>
   NoExternals("no-externals", 
            cl::desc("Do not allow external function calls (default=off)"));
 
@@ -266,23 +256,59 @@ namespace {
   STPOptimizeDivides("stp-optimize-divides", 
                  cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"),
                  cl::init(true));
+
+
+  /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
+   * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
+   * wants to patch their copy of LLVM just for these options.
+   */
+  cl::list<klee::QueryLoggingSolver> queryLoggingOptions("use-query-log",
+		  cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."),
+		  cl::values(
+					  clEnumValN(klee::ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
+					  clEnumValN(klee::ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
+					  clEnumValN(klee::SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
+					  clEnumValN(klee::SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"),
+					  clEnumValEnd
+		             ), cl::CommaSeparated
+  );
+
+
 }
 
 
 namespace klee {
   RNG theRNG;
+
+  //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
+  template <typename T>
+  static bool optionIsSet(cl::list<T> list, T option)
+  {
+	  return std::find(list.begin(), list.end(), option) != list.end();
+  }
+
+
 }
 
 Solver *constructSolverChain(STPSolver *stpSolver,
-                             std::string queryLogPath,
-                             std::string stpQueryLogPath,
+                             std::string querySMT2LogPath,
+                             std::string baseSolverQuerySMT2LogPath,
                              std::string queryPCLogPath,
-                             std::string stpQueryPCLogPath) {
+                             std::string baseSolverQueryPCLogPath) {
   Solver *solver = stpSolver;
 
-  if (UseSTPQueryPCLog)
+  if (optionIsSet(queryLoggingOptions,SOLVER_PC))
+  {
     solver = createPCLoggingSolver(solver, 
-                                   stpQueryLogPath);
+                                   baseSolverQueryPCLogPath);
+    klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
+  }
+
+  if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
+  {
+    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath);
+    klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
+  }
 
   if (UseFastCexSolver)
     solver = createFastCexSolver(solver);
@@ -299,10 +325,19 @@ Solver *constructSolverChain(STPSolver *stpSolver,
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, stpSolver);
 
-  if (UseQueryPCLog)
+  if (optionIsSet(queryLoggingOptions,ALL_PC))
+  {
     solver = createPCLoggingSolver(solver, 
                                    queryPCLogPath);
+    klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
+  }
   
+  if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
+  {
+    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath);
+    klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
+  }
+
   return solver;
 }
 
@@ -332,10 +367,10 @@ Executor::Executor(const InterpreterOptions &opts,
   STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
   Solver *solver = 
     constructSolverChain(stpSolver,
-                         interpreterHandler->getOutputFilename("queries.qlog"),
-                         interpreterHandler->getOutputFilename("stp-queries.qlog"),
-                         interpreterHandler->getOutputFilename("queries.pc"),
-                         interpreterHandler->getOutputFilename("stp-queries.pc"));
+                         interpreterHandler->getOutputFilename("all-queries.smt2"),
+                         interpreterHandler->getOutputFilename("solver-queries.smt2"),
+                         interpreterHandler->getOutputFilename("all-queries.pc"),
+                         interpreterHandler->getOutputFilename("solver-queries.pc"));
   
   this->solver = new TimingSolver(solver, stpSolver);
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 7e6b79cd..f0c9f576 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -70,6 +70,16 @@ namespace klee {
   class TreeStreamWriter;
   template<class T> class ref;
 
+  ///The different query logging solvers that can switched on/off
+  enum QueryLoggingSolver
+  {
+	  ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format
+	  ALL_SMTLIB, ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
+	  SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format
+	  SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
+  };
+
+
   /// \todo Add a context object to keep track of data only live
   /// during an instruction step. Should contain addedStates,
   /// removedStates, and haltExecution, among others.
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 2329279d..6a996d38 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
-// RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log
-// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log
+// RUN: %klee --use-query-log=all:pc --write-pcs --write-cvcs %t1.bc 2> %t2.log
+// RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log