diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-03-11 17:11:06 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-03-11 17:11:06 +0000 |
commit | fd3c6fc92af004cd4e0b6bacb549566df5db8470 (patch) | |
tree | feb58aa16b77632274d4316f90a1e1ae0e5cb2b8 /klee/tools | |
parent | 0b4c143df1441aec21e4c22c6327e0bb92d200bb (diff) |
Patch by Dan Liew which unifies the solver construction between KLEE
and Kleaver and fixes --use-query-log in Kleaver.
Diffstat (limited to 'klee/tools')
-rw-r--r-- | klee/tools/kleaver/Makefile | 2 | ||||
-rw-r--r-- | klee/tools/kleaver/main.cpp | 51 | ||||
-rw-r--r-- | klee/tools/klee/Makefile | 2 |
3 files changed, 41 insertions, 14 deletions
diff --git a/klee/tools/kleaver/Makefile b/klee/tools/kleaver/Makefile index 3973a2e6905..b6ccc91fe3d 100644 --- a/klee/tools/kleaver/Makefile +++ b/klee/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/klee/tools/kleaver/main.cpp b/klee/tools/kleaver/main.cpp index 48c24257c50..5b9e43a6350 100644 --- a/klee/tools/kleaver/main.cpp +++ b/klee/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/klee/tools/klee/Makefile b/klee/tools/klee/Makefile index 6e05a5a9bd5..01486feff97 100644 --- a/klee/tools/klee/Makefile +++ b/klee/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 |