Patch by Dan Liew: "Added support for generating .smt2 files when

writing out test cases (option --write-smt2s) in KLEE."



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

2 files changed, 41 insertions, 11 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 74769aa1..968283b7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -32,6 +32,7 @@
 #include "klee/TimerStatIncrementer.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprPPrinter.h"
+#include "klee/util/ExprSMTLIBLetPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
 #include "klee/Config/Version.h"
@@ -3373,17 +3374,46 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
 
 void Executor::getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC) {
-  if (asCVC) {
-    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-    char *log = solver->stpSolver->getConstraintLog(query);
-    res = std::string(log);
-    free(log);
-  } else {
-    std::ostringstream info;
-    ExprPPrinter::printConstraints(info, state.constraints);
-    res = info.str();    
+                                Interpreter::LogType logFormat) {
+
+  std::ostringstream info;
+
+  switch(logFormat)
+  {
+  case STP:
+  {
+	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+	  char *log = solver->stpSolver->getConstraintLog(query);
+	  res = std::string(log);
+	  free(log);
+  }
+	  break;
+
+  case KQUERY:
+  {
+	  std::ostringstream info;
+	  ExprPPrinter::printConstraints(info, state.constraints);
+	  res = info.str();
+  }
+	  break;
+
+  case SMTLIB2:
+  {
+	  std::ostringstream info;
+	  ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
+	  printer->setOutput(info);
+	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+	  printer->setQuery(query);
+	  printer->generateOutput();
+	  res = info.str();
+	  delete printer;
   }
+	  break;
+
+  default:
+	  klee_warning("Executor::getConstraintLog() : Log format not supported!");
+  }
+
 }
 
 bool Executor::getSymbolicSolution(const ExecutionState &state,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index f0c9f576..c86fe6ab 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -456,7 +456,7 @@ public:
 
   virtual void getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC = false);
+                                Interpreter::LogType logFormat = Interpreter::STP);
 
   virtual bool getSymbolicSolution(const ExecutionState &state, 
                                    std::vector<