diff options
| -rw-r--r-- | include/klee/OptionCategories.h | 23 | ||||
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 53 |
2 files changed, 59 insertions, 17 deletions
diff --git a/include/klee/OptionCategories.h b/include/klee/OptionCategories.h new file mode 100644 index 00000000..34783d77 --- /dev/null +++ b/include/klee/OptionCategories.h @@ -0,0 +1,23 @@ +//===-- OptionCategories.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 header defines the option categories used in KLEE. + */ + +#ifndef KLEE_SOLVERCOMMANDLINE_H +#define KLEE_SOLVERCOMMANDLINE_H + +#include "llvm/Support/CommandLine.h" + +namespace klee { + extern cl::OptionCategory SolvingCat; +} + +#endif diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index b071eab6..fc856096 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -12,8 +12,9 @@ * data that are common to both KLEE and Kleaver. */ -#include "klee/SolverCmdLine.h" #include "klee/Config/Version.h" +#include "klee/SolverCmdLine.h" +#include "klee/OptionCategories.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/StringMap.h" @@ -32,53 +33,66 @@ cl::extrahelp TimeFormatInfo( " The following units are supported: h, min, s, ms, us, ns.\n" ); +cl::OptionCategory SolvingCat("Constraint solving options", + "These options impact constraint solving."); + cl::opt<bool> UseFastCexSolver("use-fast-cex-solver", - cl::init(false), - cl::desc("(default=off)")); + cl::init(false), + cl::desc("(default=off)"), + cl::cat(SolvingCat)); cl::opt<bool> UseCexCache("use-cex-cache", cl::init(true), - cl::desc("Use counterexample caching (default=on)")); + cl::desc("Use counterexample caching (default=on)"), + cl::cat(SolvingCat)); cl::opt<bool> UseCache("use-cache", cl::init(true), - cl::desc("Use validity caching (default=on)")); + cl::desc("Use validity caching (default=on)"), + cl::cat(SolvingCat)); cl::opt<bool> UseIndependentSolver("use-independent-solver", cl::init(true), - cl::desc("Use constraint independence (default=on)")); + cl::desc("Use constraint independence (default=on)"), + cl::cat(SolvingCat)); cl::opt<bool> DebugValidateSolver("debug-validate-solver", - cl::init(false)); + cl::init(false), + cl::cat(SolvingCat)); cl::opt<std::string> MinQueryTimeToLog("min-query-time-to-log", cl::desc("Set time threshold for queries logged in files. " - "Only queries longer than threshold will be logged. (default=0s)")); + "Only queries longer than threshold will be logged. (default=0s)"), + cl::cat(SolvingCat)); cl::opt<bool> LogTimedOutQueries("log-timed-out-queries", cl::init(true), - cl::desc("Log queries that timed out. (default=true).")); + cl::desc("Log queries that timed out. (default=true)."), + cl::cat(SolvingCat)); cl::opt<std::string> MaxCoreSolverTime("max-solver-time", - cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver")); + cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), + cl::cat(SolvingCat)); cl::opt<bool> UseForkedCoreSolver("use-forked-solver", cl::desc("Run the core SMT solver in a forked process (default=on)"), - cl::init(true)); + cl::init(true), + cl::cat(SolvingCat)); cl::opt<bool> CoreSolverOptimizeDivides("solver-optimize-divides", cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"), - cl::init(false)); + cl::init(false), + cl::cat(SolvingCat)); cl::bits<QueryLoggingSolverType> queryLoggingOptions("use-query-log", @@ -88,11 +102,13 @@ queryLoggingOptions("use-query-log", clEnumValN(SOLVER_KQUERY,"solver:kquery","All queries reaching the solver in .kquery (KQuery) format"), clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format") KLEE_LLVM_CL_VAL_END), - cl::CommaSeparated); + cl::CommaSeparated, + cl::cat(SolvingCat)); cl::opt<bool> UseAssignmentValidatingSolver("debug-assignment-validating-solver", - cl::init(false)); + cl::init(false), + cl::cat(SolvingCat)); void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7) @@ -146,7 +162,8 @@ MetaSMTBackend("metasmt-backend", clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"), clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2") KLEE_LLVM_CL_VAL_END), - cl::init(METASMT_DEFAULT_BACKEND)); + cl::init(METASMT_DEFAULT_BACKEND), + cl::cat(SolvingCat)); #undef METASMT_DEFAULT_BACKEND #undef METASMT_DEFAULT_BACKEND_STR @@ -181,7 +198,8 @@ CoreSolverToUse("solver-backend", cl::desc("Specifiy the core solver backend to clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR) KLEE_LLVM_CL_VAL_END), - cl::init(DEFAULT_CORE_SOLVER)); + cl::init(DEFAULT_CORE_SOLVER), + cl::cat(SolvingCat)); cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith("debug-crosscheck-core-solver", @@ -193,7 +211,8 @@ DebugCrossCheckCoreSolverWith("debug-crosscheck-core-solver", clEnumValN(NO_SOLVER, "none", "Do not cross check (default)") KLEE_LLVM_CL_VAL_END), - cl::init(NO_SOLVER)); + cl::init(NO_SOLVER), + cl::cat(SolvingCat)); } #undef STP_IS_DEFAULT_STR |