Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in SMT-LIBv2 format."

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

2 files changed, 172 insertions, 0 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index b87b6dc3..4cedf47d 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -215,6 +215,11 @@ namespace klee {
   /// after writing them to the given path in .pc format.
   Solver *createPCLoggingSolver(Solver *s, std::string path);
 
+  /// 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);
+
+
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
   Solver *createDummySolver();
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
new file mode 100644
index 00000000..0fb09424
--- /dev/null
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -0,0 +1,167 @@
+//===-- SMTLIBLoggingSolver.cpp -----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Solver.h"
+
+#include "klee/Expr.h"
+#include "klee/SolverImpl.h"
+#include "klee/Statistics.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
+{
+	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";
+	}
+
+	public:
+		SMTLIBLoggingSolver(Solver *_solver, std::string path)
+		: solver(_solver),
+		os(path.c_str(), std::ios::trunc),
+		printer(),
+		queryCount(0),
+		startTime(0)
+		{
+		  //Setup the printer
+		  printer = createSMTLIBPrinter();
+		  printer->setOutput(os);
+		}
+
+		~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;
+		}
+};
+
+
+Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path)
+{
+  return new Solver(new SMTLIBLoggingSolver(_solver, path));
+}