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

7 files changed, 60 insertions, 77 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index bcb490cf..f303ae6c 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -17,6 +17,8 @@ extern llvm::cl::opt<bool> UseCexCache;
 extern llvm::cl::opt<bool> UseCache;
 
 extern llvm::cl::opt<bool> UseIndependentSolver; 
+
+extern llvm::cl::opt<bool> DebugValidateSolver;
   
 extern llvm::cl::opt<int> MinQueryTimeToLog;
 
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 657b9341..1418f1b6 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -13,15 +13,23 @@
 
 #ifndef KLEE_COMMON_H
 #define KLEE_COMMON_H
+#include "klee/Solver.h"
+#include <string>
 
 namespace klee {
+    const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2";
+    const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2";
+    const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
+    const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
 
-#define ALL_QUERIES_SMT2_FILE_NAME      "all-queries.smt2"
-#define SOLVER_QUERIES_SMT2_FILE_NAME   "solver-queries.smt2"
-#define ALL_QUERIES_PC_FILE_NAME        "all-queries.pc"
-#define SOLVER_QUERIES_PC_FILE_NAME     "solver-queries.pc"
-
+    Solver *constructSolverChain(STPSolver *stpSolver,
+                                 std::string querySMT2LogPath,
+                                 std::string baseSolverQuerySMT2LogPath,
+                                 std::string queryPCLogPath,
+                                 std::string baseSolverQueryPCLogPath);
 }
 
+
+
 #endif /* KLEE_COMMON_H */
 
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 714ae131..bc4c0023 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -26,6 +26,10 @@ llvm::cl::opt<bool>
 UseIndependentSolver("use-independent-solver",
                      llvm::cl::init(true),
                      llvm::cl::desc("Use constraint independence (default=on)"));
+
+llvm::cl::opt<bool>
+DebugValidateSolver("debug-validate-solver",
+		             llvm::cl::init(false));
   
 llvm::cl::opt<int>
 MinQueryTimeToLog("min-query-time-to-log",
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ec053597..3f90c426 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -131,10 +131,6 @@ namespace {
                   cl::init(0));
 
   cl::opt<bool>
-  DebugValidateSolver("debug-validate-solver",
-		      cl::init(false));
-
-  cl::opt<bool>
   SuppressExternalWarnings("suppress-external-warnings");
 
   cl::opt<bool>
@@ -242,60 +238,6 @@ namespace klee {
   RNG theRNG;
 }
 
-Solver *constructSolverChain(STPSolver *stpSolver,
-                             std::string querySMT2LogPath,
-                             std::string baseSolverQuerySMT2LogPath,
-                             std::string queryPCLogPath,
-                             std::string baseSolverQueryPCLogPath) {
-  Solver *solver = stpSolver;
-
-  if (optionIsSet(queryLoggingOptions,SOLVER_PC))
-  {
-    solver = createPCLoggingSolver(solver, 
-                                   baseSolverQueryPCLogPath,
-		                   MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
-  }
-
-  if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
-  {
-    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath,
-                                       MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
-  }
-
-  if (UseFastCexSolver)
-    solver = createFastCexSolver(solver);
-
-  if (UseCexCache)
-    solver = createCexCachingSolver(solver);
-
-  if (UseCache)
-    solver = createCachingSolver(solver);
-
-  if (UseIndependentSolver)
-    solver = createIndependentSolver(solver);
-
-  if (DebugValidateSolver)
-    solver = createValidatingSolver(solver, stpSolver);
-
-  if (optionIsSet(queryLoggingOptions,ALL_PC))
-  {
-    solver = createPCLoggingSolver(solver, 
-                                   queryPCLogPath,
-                                   MinQueryTimeToLog);
-    klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
-  }
-  
-  if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
-  {
-    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
-                                       MinQueryTimeToLog);
-    klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
-  }
-
-  return solver;
-}
 
 Executor::Executor(const InterpreterOptions &opts,
                    InterpreterHandler *ih) 
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