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

Conflicts:

	lib/Core/Executor.cpp
	tools/klee/main.cpp

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< 

lib/Core/Executor.cpp

@@ -43,6 +43,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"
@@ -3902,17 +3903,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,

lib/Core/Executor.h

@@ -528,7 +528,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< 

lib/Core/KleeHandler.cpp

@@ -69,6 +69,9 @@ cl::opt<bool> WriteCVCs("write-cvcs", cl::desc(
 cl::opt<bool> WritePCs("write-pcs", 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"));
 
@@ -294,7 +297,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);
 			if(f) {
 			  *f << constraints;
@@ -306,7 +309,7 @@ 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);
 			if(f) {
 			  *f << constraints;
@@ -316,6 +319,15 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 			}
 		}
 
+    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(