Patch by Dan Liew: "Added -print-smtlib option to kleaver tool that

allows .pc files to be printed as SMT-LIBv2 queries."



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

1 files changed, 86 insertions, 0 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 0c4a78f7..077de3ed 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -12,6 +12,8 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
 
+#include "klee/util/ExprSMTLIBLetPrinter.h"
+
 #include "llvm/ADT/OwningPtr.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
@@ -45,6 +47,7 @@ namespace {
   enum ToolActions {
     PrintTokens,
     PrintAST,
+    PrintSMTLIBv2,
     Evaluate
   };
 
@@ -54,12 +57,15 @@ namespace {
              llvm::cl::values(
              clEnumValN(PrintTokens, "print-tokens",
                         "Print tokens from the input file."),
+			clEnumValN(PrintSMTLIBv2, "print-smtlib",
+					   "Print parsed input file as SMT-LIBv2 query."),
              clEnumValN(PrintAST, "print-ast",
                         "Print parsed AST nodes from the input file."),
              clEnumValN(Evaluate, "evaluate",
                         "Print parsed AST nodes from the input file."),
              clEnumValEnd));
 
+
   enum BuilderKinds {
     DefaultBuilder,
     ConstantFoldingBuilder,
@@ -276,6 +282,79 @@ static bool EvaluateInputAST(const char *Filename,
   return success;
 }
 
+static bool printInputAsSMTLIBv2(const char *Filename,
+                             const MemoryBuffer *MB,
+                             ExprBuilder *Builder)
+{
+	//Parse the input file
+	std::vector<Decl*> Decls;
+	Parser *P = Parser::Create(Filename, MB, Builder);
+	P->SetMaxErrors(20);
+	while (Decl *D = P->ParseTopLevelDecl())
+	{
+		Decls.push_back(D);
+	}
+
+	bool success = true;
+	if (unsigned N = P->GetNumErrors())
+	{
+		std::cerr << Filename << ": parse failure: "
+				   << N << " errors.\n";
+		success = false;
+	}
+
+	if (!success)
+	return false;
+
+	ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
+	printer->setOutput(std::cout);
+
+	unsigned int queryNumber = 0;
+	//Loop over the declarations
+	for (std::vector<Decl*>::iterator it = Decls.begin(), ie = Decls.end(); it != ie; ++it)
+	{
+		Decl *D = *it;
+		if (QueryCommand *QC = dyn_cast<QueryCommand>(D))
+		{
+			//print line break to separate from previous query
+			if(queryNumber!=0) 	std::cout << std::endl;
+
+			//Output header for this query as a SMT-LIBv2 comment
+			std::cout << ";SMTLIBv2 Query " << queryNumber << std::endl;
+
+			/* Can't pass ConstraintManager constructor directly
+			 * as argument to Query object. Like...
+			 * query(ConstraintManager(QC->Constraints),QC->Query);
+			 *
+			 * For some reason if constructed this way the first
+			 * constraint in the constraint set is set to NULL and
+			 * will later cause a NULL pointer dereference.
+			 */
+			ConstraintManager constraintM(QC->Constraints);
+			Query query(constraintM,QC->Query);
+			printer->setQuery(query);
+
+			if(!QC->Objects.empty())
+				printer->setArrayValuesToGet(QC->Objects);
+
+			printer->generateOutput();
+
+
+			queryNumber++;
+		}
+	}
+
+	//Clean up
+	for (std::vector<Decl*>::iterator it = Decls.begin(),
+			ie = Decls.end(); it != ie; ++it)
+		delete *it;
+	delete P;
+
+	delete printer;
+
+	return true;
+}
+
 int main(int argc, char **argv) {
   bool success = true;
 
@@ -341,6 +420,13 @@ int main(int argc, char **argv) {
                                MB.get(), Builder);
 #endif
     break;
+  case PrintSMTLIBv2:
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
+    success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB,Builder);
+#else
+    success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder);
+#endif
+    break;
   default:
     std::cerr << argv[0] << ": error: Unknown program action!\n";
   }