Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated header SolverCmdLine.h) and moved it to the Solver library.

1 files changed, 220 insertions, 0 deletions

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<bool> UseFastCexSolver(
+    "use-fast-cex-solver", cl::init(false),
+    cl::desc("Enable an experimental range-based solver (default=false)"),
+    cl::cat(SolvingCat));
+
+cl::opt<bool> UseCexCache("use-cex-cache", cl::init(true),
+                          cl::desc("Use the counterexample cache (default=true)"),
+                          cl::cat(SolvingCat));
+
+cl::opt<bool> UseBranchCache("use-branch-cache", cl::init(true),
+                             cl::desc("Use the branch cache (default=true)"),
+                             cl::cat(SolvingCat));
+
+cl::opt<bool>
+    UseIndependentSolver("use-independent-solver", cl::init(true),
+                         cl::desc("Use constraint independence (default=true)"),
+                         cl::cat(SolvingCat));
+
+cl::opt<bool> 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<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)"),
+    cl::cat(SolvingCat));
+
+cl::opt<bool>
+    LogTimedOutQueries("log-timed-out-queries", cl::init(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::cat(SolvingCat));
+
+cl::opt<bool> 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<bool> 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<QueryLoggingSolverType> 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<bool> 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<cl::Option *> &map = cl::getRegisteredOptions();
+
+  for (auto &elem : map) {
+    if (elem.second->Category == &Category) {
+      elem.second->setHiddenFlag(cl::Hidden);
+    }
+  }
+}
+
+void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
+  StringMap<cl::Option *> &map = cl::getRegisteredOptions();
+  for (StringMap<cl::Option *>::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<klee::MetaSMTBackendType>
+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<CoreSolverType> 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<CoreSolverType> 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