Patch by Dan Liew which unifies the solver construction between KLEE

and Kleaver and fixes --use-query-log in Kleaver.



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

3 files changed, 41 insertions, 14 deletions

diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 3973a2e6..b6ccc91f 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -14,7 +14,7 @@ include $(LEVEL)/Makefile.config
 
 # FIXME: Ideally we wouldn't have any LLVM dependencies here, which
 # means kicking out klee's Support.
-USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+USEDLIBS = kleeBasic.a kleaverSolver.a kleaverExpr.a kleeSupport.a 
 LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 48c24257..5b9e43a6 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -24,6 +24,9 @@
 #include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/raw_ostream.h"
 
+#include <sys/stat.h>
+#include <unistd.h>
+
 // FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
 #undef PACKAGE_BUGREPORT
 #undef PACKAGE_NAME
@@ -92,6 +95,35 @@ namespace {
   UseDummySolver("use-dummy-solver",
 		   cl::init(false));
 
+  llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."),
+		                                               llvm::cl::init("."));
+
+}
+
+static std::string getQueryLogPath(const char filename[])
+{
+	//check directoryToWriteLogs exists
+	struct stat s;
+	if( !(stat(directoryToWriteQueryLogs.c_str(),&s) == 0 && S_ISDIR(s.st_mode)) )
+	{
+		std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" does not exist!" << std::endl;
+		exit(1);
+	}
+
+	//check permissions okay
+	if( !( (s.st_mode & S_IWUSR) && getuid() == s.st_uid) &&
+	    !( (s.st_mode & S_IWGRP) && getgid() == s.st_gid) &&
+	    !( s.st_mode & S_IWOTH)
+	)
+	{
+		std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" is not writable!" << std::endl;
+		exit(1);
+	}
+
+	std::string path=directoryToWriteQueryLogs;
+	path+="/";
+	path+=filename;
+	return path;
 }
 
 static std::string escapedString(const char *start, unsigned length) {
@@ -191,18 +223,13 @@ static bool EvaluateInputAST(const char *Filename,
   else {
     STP = S = createDummySolver(); 
   }
-  if (true == optionIsSet(queryLoggingOptions, SOLVER_PC))
-    S = createPCLoggingSolver(S, SOLVER_QUERIES_PC_FILE_NAME, MinQueryTimeToLog);
-  if (UseFastCexSolver)
-    S = createFastCexSolver(S);  
-  if (UseCexCache)
-    S = createCexCachingSolver(S);
-  if (UseCache)
-    S = createCachingSolver(S);
-  if (UseIndependentSolver)
-    S = createIndependentSolver(S);
-  if (0)
-    S = createValidatingSolver(S, STP);
+
+  S= constructSolverChain((STPSolver*) STP,
+		  	  	  	      getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
+		  	  	  	      getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
+		  	  	  	      getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
+		  	  	  	      getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
+
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 6e05a5a9..01486fef 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -12,7 +12,7 @@ TOOLNAME = klee
 
 include $(LEVEL)/Makefile.config
 
-USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a  kleaverSolver.a kleaverExpr.a kleeSupport.a 
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
 include $(LEVEL)/Makefile.common