diff options
| -rw-r--r-- | include/klee/CommandLine.h | 70 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 49 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 8 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 27 |
4 files changed, 79 insertions, 75 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h new file mode 100644 index 00000000..4b537174 --- /dev/null +++ b/include/klee/CommandLine.h @@ -0,0 +1,70 @@ +/* + * FIXME: This is a temporary solution. + * This header groups command line options and associated data that is common + * for klee and kleaver. + */ + +#ifndef COMMANDLINE_H +#define COMMANDLINE_H + +#include "llvm/Support/CommandLine.h" + +namespace { + +#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" + +llvm::cl::opt<bool> +UseFastCexSolver("use-fast-cex-solver", + llvm::cl::init(false), + llvm::cl::desc("(default=off)")); + +llvm::cl::opt<int> +MinQueryTimeToLog("min-query-time-to-log", + llvm::cl::init(0), + llvm::cl::value_desc("milliseconds"), + llvm::cl::desc("Set time threshold (in ms) for queries logged in files. " + "Only queries longer than threshold will be logged. (default=0). " + "Set this param to a negative value to log timeouts only.")); + +///The different query logging solvers that can switched on/off +enum QueryLoggingSolverType +{ + 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 +}; + +/* 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. + */ +llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( + "use-query-log", + llvm::cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."), + llvm::cl::values( + clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"), + clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), + clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), + clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"), + clEnumValEnd + ), + llvm::cl::CommaSeparated +); + +} + +namespace klee { + //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions + template <typename T> + static bool optionIsSet(llvm::cl::list<T> list, T option) + { + return std::find(list.begin(), list.end(), option) != list.end(); + } +} + +#endif /* COMMANDLINE_H */ + diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 5803e6ff..f3278c89 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -30,6 +30,7 @@ #include "klee/Expr.h" #include "klee/Interpreter.h" #include "klee/TimerStatIncrementer.h" +#include "klee/CommandLine.h" #include "klee/util/Assignment.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprSMTLIBLetPrinter.h" @@ -144,11 +145,6 @@ namespace { cl::desc("Only output test cases covering new code.")); cl::opt<bool> - UseFastCexSolver("use-fast-cex-solver", - cl::init(false), - cl::desc("(default=off")); - - cl::opt<bool> UseIndependentSolver("use-independent-solver", cl::init(true), cl::desc("Use constraint independence (default=on)")); @@ -163,15 +159,6 @@ namespace { UseCexCache("use-cex-cache", cl::init(true), cl::desc("Use counterexample caching (default=on)")); - - // FIXME: Command line argument duplicated in main.cpp of Kleaver - cl::opt<int> - MinQueryTimeToLog("min-query-time-to-log", - cl::init(0), - cl::value_desc("milliseconds"), - cl::desc("Set time threshold (in ms) for queries logged in files. " - "Only queries longer than threshold will be logged. (default=0). " - "Set this param to a negative value to log timeouts only.")); cl::opt<bool> NoExternals("no-externals", @@ -267,37 +254,11 @@ namespace { 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, @@ -381,10 +342,10 @@ Executor::Executor(const InterpreterOptions &opts, STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides); Solver *solver = constructSolverChain(stpSolver, - interpreterHandler->getOutputFilename("all-queries.smt2"), - interpreterHandler->getOutputFilename("solver-queries.smt2"), - interpreterHandler->getOutputFilename("all-queries.pc"), - interpreterHandler->getOutputFilename("solver-queries.pc")); + interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), + interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), + interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), + interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); this->solver = new TimingSolver(solver, stpSolver); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c86fe6ab..c434c34c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -70,14 +70,6 @@ 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 diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 1a4663a1..00034eb1 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -10,6 +10,7 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/Statistics.h" +#include "klee/CommandLine.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" @@ -90,24 +91,6 @@ namespace { UseDummySolver("use-dummy-solver", cl::init(false)); - cl::opt<bool> - UseFastCexSolver("use-fast-cex-solver", - cl::init(false)); - - // FIXME: Command line argument modified in Executor.cpp of Klee. Different - // output file name used. - cl::opt<bool> - UseSTPQueryPCLog("use-stp-query-pc-log", - cl::init(false)); - - // FIXME: Command line argument duplicated in Executor.cpp of Klee - cl::opt<unsigned int> - MinQueryTimeToLog("min-query-time-to-log", - cl::init(0), - cl::value_desc("milliseconds"), - cl::desc("Set time threshold (in ms) for queries logged in files. " - "Only queries longer than threshold will be logged. (default=0)")); - } static std::string escapedString(const char *start, unsigned length) { @@ -197,8 +180,8 @@ static bool EvaluateInputAST(const char *Filename, // FIXME: Support choice of solver. Solver *S, *STP = S = UseDummySolver ? createDummySolver() : new STPSolver(true); - if (UseSTPQueryPCLog) - S = createPCLoggingSolver(S, "stp-queries.pc", MinQueryTimeToLog); + if (true == optionIsSet(queryLoggingOptions, SOLVER_PC)) + S = createPCLoggingSolver(S, SOLVER_QUERIES_PC_FILE_NAME, MinQueryTimeToLog); if (UseFastCexSolver) S = createFastCexSolver(S); S = createCexCachingSolver(S); @@ -265,9 +248,7 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "\n"; } } else { - std::cout << "FAIL (reason: " - << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) - << ")"; + std::cout << "VALID (counterexample request ignored)"; } } |