From 8c9c1681155812a27b46ba131c44a5737afe67c3 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 1 Nov 2018 17:50:42 +0000 Subject: Introduced a constraint solving option category to which all the options in CmdLineOptions.cpp are currently added. --- lib/Basic/CmdLineOptions.cpp | 53 ++++++++++++++++++++++++++++++-------------- 1 file changed, 36 insertions(+), 17 deletions(-) (limited to 'lib/Basic') 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 UseFastCexSolver("use-fast-cex-solver", - cl::init(false), - cl::desc("(default=off)")); + cl::init(false), + cl::desc("(default=off)"), + cl::cat(SolvingCat)); cl::opt 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 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 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 DebugValidateSolver("debug-validate-solver", - cl::init(false)); + cl::init(false), + cl::cat(SolvingCat)); cl::opt 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 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 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 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 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 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 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 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 -- cgit 1.4.1