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

4 files changed, 63 insertions, 14 deletions

diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 8640869a..e29db411 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -58,6 +58,13 @@ public:
         CheckDivZero(_CheckDivZero) {}
   };
 
+  enum LogType
+  {
+	  STP, //.CVC (STP's native language)
+	  KQUERY, //.PC files (kQuery native language)
+	  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
+  };
+
   /// InterpreterOptions - Options varying the runtime behavior during
   /// interpretation.
   struct InterpreterOptions {
@@ -132,7 +139,7 @@ public:
   
   virtual void getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC = false) = 0;
+                                LogType logFormat = STP) = 0;
 
   virtual bool getSymbolicSolution(const ExecutionState &state, 
                                    std::vector< 
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< 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index dc335cd0..d28356bd 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -96,6 +96,10 @@ namespace {
             cl::desc("Write .pc files for each test case"));
   
   cl::opt<bool>
+  WriteSMT2s("write-smt2s",
+            cl::desc("Write .smt2 (SMT-LIBv2) files for each test case"));
+
+  cl::opt<bool>
   WriteCov("write-cov", 
            cl::desc("Write coverage information for each test case"));
   
@@ -448,7 +452,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
    
     if (errorMessage || WritePCs) {
       std::string constraints;
-      m_interpreter->getConstraintLog(state, constraints);
+      m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
       std::ostream *f = openTestFile("pc", id);
       *f << constraints;
       delete f;
@@ -456,12 +460,20 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 
     if (WriteCVCs) {
       std::string constraints;
-      m_interpreter->getConstraintLog(state, constraints, true);
+      m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
       std::ostream *f = openTestFile("cvc", id);
       *f << constraints;
       delete f;
     }
     
+    if(WriteSMT2s) {
+    	std::string constraints;
+        m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
+        std::ostream *f = openTestFile("smt2", id);
+        *f << constraints;
+        delete f;
+    }
+
     if (m_symPathWriter) {
       std::vector<unsigned char> symbolicBranches;
       m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state),