From b084092bcc2e5cb69e80a9a0ecd9340ec4c4458c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 15 Aug 2019 22:29:59 +0100 Subject: Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated header SolverCmdLine.h) and moved it to the Solver library. --- lib/Basic/CMakeLists.txt | 1 - lib/Basic/CmdLineOptions.cpp | 220 ------------------------------------------- lib/Solver/CMakeLists.txt | 1 + lib/Solver/SolverCmdLine.cpp | 220 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 221 insertions(+), 221 deletions(-) delete mode 100644 lib/Basic/CmdLineOptions.cpp create mode 100644 lib/Solver/SolverCmdLine.cpp diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt index d0a309c9..78890ea6 100644 --- a/lib/Basic/CMakeLists.txt +++ b/lib/Basic/CMakeLists.txt @@ -7,7 +7,6 @@ # #===------------------------------------------------------------------------===# klee_add_component(kleeBasic - CmdLineOptions.cpp ConstructSolverChain.cpp KTest.cpp Statistics.cpp diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp deleted file mode 100644 index 9e190840..00000000 --- a/lib/Basic/CmdLineOptions.cpp +++ /dev/null @@ -1,220 +0,0 @@ -//===-- 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/Config/Version.h" -#include "klee/SolverCmdLine.h" -#include "klee/OptionCategories.h" - -#include "llvm/ADT/ArrayRef.h" -#include "llvm/ADT/StringMap.h" -#include "llvm/Support/CommandLine.h" - -using namespace llvm; - -namespace klee { - -cl::extrahelp TimeFormatInfo( - "\nTime format used by KLEE's options\n" - "\n" - " Time spans can be specified in two ways:\n" - " 1. As positive real numbers representing seconds, e.g. '10', '3.5' " - "but not 'INF', 'NaN', '1e3', '-4.5s'\n" - " 2. As a sequence of natural numbers with specified units, e.g. " - "'1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n" - " 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("Enable an experimental range-based solver (default=false)"), - cl::cat(SolvingCat)); - -cl::opt UseCexCache("use-cex-cache", cl::init(true), - cl::desc("Use the counterexample cache (default=true)"), - cl::cat(SolvingCat)); - -cl::opt UseBranchCache("use-branch-cache", cl::init(true), - cl::desc("Use the branch cache (default=true)"), - cl::cat(SolvingCat)); - -cl::opt - UseIndependentSolver("use-independent-solver", cl::init(true), - cl::desc("Use constraint independence (default=true)"), - cl::cat(SolvingCat)); - -cl::opt DebugValidateSolver( - "debug-validate-solver", cl::init(false), - cl::desc("Crosscheck the results of the solver chain above the core solver " - "with the results of the core solver (default=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)"), - cl::cat(SolvingCat)); - -cl::opt - LogTimedOutQueries("log-timed-out-queries", cl::init(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::cat(SolvingCat)); - -cl::opt UseForkedCoreSolver( - "use-forked-solver", - cl::desc("Run the core SMT solver in a forked process (default=true)"), - cl::init(true), cl::cat(SolvingCat)); - -cl::opt CoreSolverOptimizeDivides( - "solver-optimize-divides", - cl::desc("Optimize constant divides into add/shift/multiplies before " - "passing them to the core SMT solver (default=false)"), - cl::init(false), cl::cat(SolvingCat)); - -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::cat(SolvingCat)); - -cl::opt UseAssignmentValidatingSolver( - "debug-assignment-validating-solver", cl::init(false), - cl::desc("Debug the correctness of generated assignments (default=false)"), - cl::cat(SolvingCat)); - - -void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) { - StringMap &map = cl::getRegisteredOptions(); - - for (auto &elem : map) { - if (elem.second->Category == &Category) { - elem.second->setHiddenFlag(cl::Hidden); - } - } -} - -void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { - StringMap &map = cl::getRegisteredOptions(); - for (StringMap::iterator i = map.begin(), e = map.end(); i != e; - i++) { - if (i->second->Category != &Category) { - i->second->setHiddenFlag(cl::Hidden); - } - } -} - -#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), - cl::cat(SolvingCat)); - -#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::cat(SolvingCat)); - -cl::opt DebugCrossCheckCoreSolverWith( - "debug-crosscheck-core-solver", - cl::desc( - "Specifiy a solver to use for crosschecking the results of 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 crosscheck (default)") - KLEE_LLVM_CL_VAL_END), - cl::init(NO_SOLVER), cl::cat(SolvingCat)); -} // namespace klee - -#undef STP_IS_DEFAULT_STR -#undef METASMT_IS_DEFAULT_STR -#undef Z3_IS_DEFAULT_STR -#undef DEFAULT_CORE_SOLVER diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index d9c393fb..f4cfa738 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -21,6 +21,7 @@ klee_add_component(kleaverSolver QueryLoggingSolver.cpp SMTLIBLoggingSolver.cpp Solver.cpp + SolverCmdLine.cpp SolverImpl.cpp SolverStats.cpp STPBuilder.cpp diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp new file mode 100644 index 00000000..9e190840 --- /dev/null +++ b/lib/Solver/SolverCmdLine.cpp @@ -0,0 +1,220 @@ +//===-- 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/Config/Version.h" +#include "klee/SolverCmdLine.h" +#include "klee/OptionCategories.h" + +#include "llvm/ADT/ArrayRef.h" +#include "llvm/ADT/StringMap.h" +#include "llvm/Support/CommandLine.h" + +using namespace llvm; + +namespace klee { + +cl::extrahelp TimeFormatInfo( + "\nTime format used by KLEE's options\n" + "\n" + " Time spans can be specified in two ways:\n" + " 1. As positive real numbers representing seconds, e.g. '10', '3.5' " + "but not 'INF', 'NaN', '1e3', '-4.5s'\n" + " 2. As a sequence of natural numbers with specified units, e.g. " + "'1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n" + " 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("Enable an experimental range-based solver (default=false)"), + cl::cat(SolvingCat)); + +cl::opt UseCexCache("use-cex-cache", cl::init(true), + cl::desc("Use the counterexample cache (default=true)"), + cl::cat(SolvingCat)); + +cl::opt UseBranchCache("use-branch-cache", cl::init(true), + cl::desc("Use the branch cache (default=true)"), + cl::cat(SolvingCat)); + +cl::opt + UseIndependentSolver("use-independent-solver", cl::init(true), + cl::desc("Use constraint independence (default=true)"), + cl::cat(SolvingCat)); + +cl::opt DebugValidateSolver( + "debug-validate-solver", cl::init(false), + cl::desc("Crosscheck the results of the solver chain above the core solver " + "with the results of the core solver (default=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)"), + cl::cat(SolvingCat)); + +cl::opt + LogTimedOutQueries("log-timed-out-queries", cl::init(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::cat(SolvingCat)); + +cl::opt UseForkedCoreSolver( + "use-forked-solver", + cl::desc("Run the core SMT solver in a forked process (default=true)"), + cl::init(true), cl::cat(SolvingCat)); + +cl::opt CoreSolverOptimizeDivides( + "solver-optimize-divides", + cl::desc("Optimize constant divides into add/shift/multiplies before " + "passing them to the core SMT solver (default=false)"), + cl::init(false), cl::cat(SolvingCat)); + +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::cat(SolvingCat)); + +cl::opt UseAssignmentValidatingSolver( + "debug-assignment-validating-solver", cl::init(false), + cl::desc("Debug the correctness of generated assignments (default=false)"), + cl::cat(SolvingCat)); + + +void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) { + StringMap &map = cl::getRegisteredOptions(); + + for (auto &elem : map) { + if (elem.second->Category == &Category) { + elem.second->setHiddenFlag(cl::Hidden); + } + } +} + +void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { + StringMap &map = cl::getRegisteredOptions(); + for (StringMap::iterator i = map.begin(), e = map.end(); i != e; + i++) { + if (i->second->Category != &Category) { + i->second->setHiddenFlag(cl::Hidden); + } + } +} + +#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), + cl::cat(SolvingCat)); + +#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::cat(SolvingCat)); + +cl::opt DebugCrossCheckCoreSolverWith( + "debug-crosscheck-core-solver", + cl::desc( + "Specifiy a solver to use for crosschecking the results of 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 crosscheck (default)") + KLEE_LLVM_CL_VAL_END), + cl::init(NO_SOLVER), cl::cat(SolvingCat)); +} // namespace klee + +#undef STP_IS_DEFAULT_STR +#undef METASMT_IS_DEFAULT_STR +#undef Z3_IS_DEFAULT_STR +#undef DEFAULT_CORE_SOLVER -- cgit 1.4.1