diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 75 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 10 | ||||
| -rw-r--r-- | test/Feature/ExprLogging.c | 4 |
3 files changed, 67 insertions, 22 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8478ea67..74769aa1 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -164,16 +164,6 @@ namespace { cl::desc("Use counterexample caching (default=on)")); cl::opt<bool> - UseQueryPCLog("use-query-pc-log", - cl::init(false), - cl::desc("Log all queries into queries.pc (default=off)")); - - cl::opt<bool> - UseSTPQueryPCLog("use-stp-query-pc-log", - cl::init(false), - cl::desc("Log all queries sent to STP into queries.pc (default=off)")); - - cl::opt<bool> NoExternals("no-externals", cl::desc("Do not allow external function calls (default=off)")); @@ -266,23 +256,59 @@ namespace { STPOptimizeDivides("stp-optimize-divides", cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"), cl::init(true)); + + + /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking + * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone + * wants to patch their copy of LLVM just for these options. + */ + cl::list<klee::QueryLoggingSolver> queryLoggingOptions("use-query-log", + cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."), + cl::values( + clEnumValN(klee::ALL_PC,"all:pc","All queries in .pc (KQuery) format"), + clEnumValN(klee::ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), + clEnumValN(klee::SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), + clEnumValN(klee::SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"), + clEnumValEnd + ), cl::CommaSeparated + ); + + } namespace klee { RNG theRNG; + + //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions + template <typename T> + static bool optionIsSet(cl::list<T> list, T option) + { + return std::find(list.begin(), list.end(), option) != list.end(); + } + + } Solver *constructSolverChain(STPSolver *stpSolver, - std::string queryLogPath, - std::string stpQueryLogPath, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, - std::string stpQueryPCLogPath) { + std::string baseSolverQueryPCLogPath) { Solver *solver = stpSolver; - if (UseSTPQueryPCLog) + if (optionIsSet(queryLoggingOptions,SOLVER_PC)) + { solver = createPCLoggingSolver(solver, - stpQueryLogPath); + baseSolverQueryPCLogPath); + klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str()); + } + + if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB)) + { + solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath); + klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str()); + } if (UseFastCexSolver) solver = createFastCexSolver(solver); @@ -299,10 +325,19 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (DebugValidateSolver) solver = createValidatingSolver(solver, stpSolver); - if (UseQueryPCLog) + if (optionIsSet(queryLoggingOptions,ALL_PC)) + { solver = createPCLoggingSolver(solver, queryPCLogPath); + klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str()); + } + if (optionIsSet(queryLoggingOptions,ALL_SMTLIB)) + { + solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath); + klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str()); + } + return solver; } @@ -332,10 +367,10 @@ Executor::Executor(const InterpreterOptions &opts, STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides); Solver *solver = constructSolverChain(stpSolver, - interpreterHandler->getOutputFilename("queries.qlog"), - interpreterHandler->getOutputFilename("stp-queries.qlog"), - interpreterHandler->getOutputFilename("queries.pc"), - interpreterHandler->getOutputFilename("stp-queries.pc")); + interpreterHandler->getOutputFilename("all-queries.smt2"), + interpreterHandler->getOutputFilename("solver-queries.smt2"), + interpreterHandler->getOutputFilename("all-queries.pc"), + interpreterHandler->getOutputFilename("solver-queries.pc")); this->solver = new TimingSolver(solver, stpSolver); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7e6b79cd..f0c9f576 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -70,6 +70,16 @@ namespace klee { class TreeStreamWriter; template<class T> class ref; + ///The different query logging solvers that can switched on/off + enum QueryLoggingSolver + { + ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format + ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format + SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format + SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format + }; + + /// \todo Add a context object to keep track of data only live /// during an instruction step. Should contain addedStates, /// removedStates, and haltExecution, among others. diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index 2329279d..6a996d38 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc -// RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log -// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log +// RUN: %klee --use-query-log=all:pc --write-pcs --write-cvcs %t1.bc 2> %t2.log +// RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log |