diff options
| -rw-r--r-- | include/klee/CommandLine.h | 78 | ||||
| -rw-r--r-- | include/klee/Common.h | 27 | ||||
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 57 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 1 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 1 |
5 files changed, 107 insertions, 57 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index c8397cf1..39290e7b 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -1,55 +1,31 @@ /* - * FIXME: This is a temporary solution. - * This header groups command line options and associated data that is common - * for klee and kleaver. + * This header groups command line options declarations and associated data + * that is common for klee and kleaver. */ -#ifndef COMMANDLINE_H -#define COMMANDLINE_H +#ifndef KLEE_COMMANDLINE_H +#define KLEE_COMMANDLINE_H #include "llvm/Support/CommandLine.h" -namespace { +namespace klee { -#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)")); +extern llvm::cl::opt<bool> UseFastCexSolver; -llvm::cl::opt<bool> -UseCexCache("use-cex-cache", - llvm::cl::init(true), - llvm::cl::desc("Use counterexample caching (default=on)")); +extern llvm::cl::opt<bool> UseCexCache; -llvm::cl::opt<bool> -UseCache("use-cache", - llvm::cl::init(true), - llvm::cl::desc("Use validity caching (default=on)")); +extern llvm::cl::opt<bool> UseCache; -llvm::cl::opt<bool> -UseIndependentSolver("use-independent-solver", - llvm::cl::init(true), - llvm::cl::desc("Use constraint independence (default=on)")); +extern llvm::cl::opt<bool> UseIndependentSolver; -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.")); +extern llvm::cl::opt<int> MinQueryTimeToLog; ///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 + 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 }; @@ -57,29 +33,17 @@ enum QueryLoggingSolverType * 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 -); +extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; + +//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(); } -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 */ +#endif /* KLEE_COMMANDLINE_H */ diff --git a/include/klee/Common.h b/include/klee/Common.h new file mode 100644 index 00000000..657b9341 --- /dev/null +++ b/include/klee/Common.h @@ -0,0 +1,27 @@ +//===-- Common.h ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/* + * This file groups declarations that are common to both KLEE and Kleaver. + */ + +#ifndef KLEE_COMMON_H +#define KLEE_COMMON_H + +namespace klee { + +#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" + +} + +#endif /* KLEE_COMMON_H */ + diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp new file mode 100644 index 00000000..f14b813a --- /dev/null +++ b/lib/Basic/CmdLineOptions.cpp @@ -0,0 +1,57 @@ +/* + * This file groups command line options definitions and associated + * data that are common to both KLEE and Kleaver. + */ + +#include "klee/CommandLine.h" + +namespace klee { + +llvm::cl::opt<bool> +UseFastCexSolver("use-fast-cex-solver", + llvm::cl::init(false), + llvm::cl::desc("(default=off)")); + +llvm::cl::opt<bool> +UseCexCache("use-cex-cache", + llvm::cl::init(true), + llvm::cl::desc("Use counterexample caching (default=on)")); + +llvm::cl::opt<bool> +UseCache("use-cache", + llvm::cl::init(true), + llvm::cl::desc("Use validity caching (default=on)")); + +llvm::cl::opt<bool> +UseIndependentSolver("use-independent-solver", + llvm::cl::init(true), + llvm::cl::desc("Use constraint independence (default=on)")); + +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.")); + + +/* 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 +); + +} + diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a0c4de1c..b2ddb9b1 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -31,6 +31,7 @@ #include "klee/Interpreter.h" #include "klee/TimerStatIncrementer.h" #include "klee/CommandLine.h" +#include "klee/Common.h" #include "klee/util/Assignment.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprSMTLIBLetPrinter.h" diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 00ffc92f..6b0008db 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -11,6 +11,7 @@ #include "klee/SolverImpl.h" #include "klee/Statistics.h" #include "klee/CommandLine.h" +#include "klee/Common.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" |