//===-- CmdLineOptions.cpp --------------------------------------*- 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 command line options definitions and associated * data that are common to both KLEE and Kleaver. */ #include "klee/SolverCmdLine.h" #include "klee/Config/Version.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/StringMap.h" #include "llvm/Support/CommandLine.h" using namespace llvm; namespace klee { cl::opt UseFastCexSolver("use-fast-cex-solver", cl::init(false), cl::desc("(default=off)")); cl::opt UseCexCache("use-cex-cache", cl::init(true), cl::desc("Use counterexample caching (default=on)")); cl::opt UseCache("use-cache", cl::init(true), cl::desc("Use validity caching (default=on)")); cl::opt UseIndependentSolver("use-independent-solver", cl::init(true), cl::desc("Use constraint independence (default=on)")); cl::opt DebugValidateSolver("debug-validate-solver", cl::init(false)); cl::opt 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 MaxCoreSolverTime("max-solver-time", cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), cl::init(0.0), cl::value_desc("seconds")); cl::opt UseForkedCoreSolver("use-forked-solver", cl::desc("Run the core SMT solver in a forked process (default=on)"), cl::init(true)); 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::bits queryLoggingOptions("use-query-log", cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."), cl::values(clEnumValN(ALL_KQUERY,"all:kquery","All queries in .kquery (KQuery) format"), clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), 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::opt UseAssignmentValidatingSolver("debug-assignment-validating-solver", cl::init(false)); void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7) StringMap &map = cl::getRegisteredOptions(); #else StringMap map; cl::getRegisteredOptions(map); #endif for (StringMap::iterator i = map.begin(), e = map.end(); i != e; i++) { if (i->second->Category != &Category) { i->second->setHiddenFlag(cl::Hidden); } } } void KCommandLine::HideUnrelatedOptions( ArrayRef Categories) { for (ArrayRef::iterator i = Categories.begin(), e = Categories.end(); i != e; i++) HideUnrelatedOptions(*i); } #ifdef ENABLE_METASMT #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR #define METASMT_DEFAULT_BACKEND_STR "(default = btor)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR #elif METASMT_DEFAULT_BACKEND_IS_Z3 #define METASMT_DEFAULT_BACKEND_STR "(default = z3)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3 #elif METASMT_DEFAULT_BACKEND_IS_CVC4 #define METASMT_DEFAULT_BACKEND_STR "(default = cvc4)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_CVC4 #elif METASMT_DEFAULT_BACKEND_IS_YICES2 #define METASMT_DEFAULT_BACKEND_STR "(default = yices2)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_YICES2 #else #define METASMT_DEFAULT_BACKEND_STR "(default = stp)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP #endif cl::opt MetaSMTBackend("metasmt-backend", cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR), cl::values(clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), 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)); #undef METASMT_DEFAULT_BACKEND #undef METASMT_DEFAULT_BACKEND_STR #endif /* ENABLE_METASMT */ // Pick the default core solver based on configuration #ifdef ENABLE_STP #define STP_IS_DEFAULT_STR " (default)" #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER STP_SOLVER #elif ENABLE_Z3 #define STP_IS_DEFAULT_STR "" #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR " (default)" #define DEFAULT_CORE_SOLVER Z3_SOLVER #elif ENABLE_METASMT #define STP_IS_DEFAULT_STR "" #define METASMT_IS_DEFAULT_STR " (default)" #define Z3_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER METASMT_SOLVER #define Z3_IS_DEFAULT_STR "" #else #error "Unsupported solver configuration" #endif cl::opt CoreSolverToUse("solver-backend", cl::desc("Specifiy the core solver backend to use"), cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), 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::opt DebugCrossCheckCoreSolverWith("debug-crosscheck-core-solver", cl::desc("Specifiy a solver to use for cross checking with the core solver"), cl::values(clEnumValN(STP_SOLVER, "stp", "stp"), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), clEnumValN(NO_SOLVER, "none", "Do not cross check (default)") KLEE_LLVM_CL_VAL_END), cl::init(NO_SOLVER)); } #undef STP_IS_DEFAULT_STR #undef METASMT_IS_DEFAULT_STR #undef Z3_IS_DEFAULT_STR #undef DEFAULT_CORE_SOLVER