Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing

a ``createCoreSolver()`` function. The solver used is set by the new
``--solver-backend`` command line argument. The default is STP.

This change necessitated refactoring the MetaSMT stuff. That clearly
didn't belong in the Executor! The MetaSMT command line option is
now ``--metasmt-backend`` as this only picks the MetaSMT backend.

In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed.

Note I don't have MetaSMT built on my development machine so I don't
know if the MetaSMT stuff even compiles...

8 files changed, 130 insertions, 120 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index c4c70069..44f1afd4 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -44,17 +44,19 @@ enum QueryLoggingSolverType
  */
 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
+enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER };
+extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
+
 #ifdef SUPPORT_METASMT
 
 enum MetaSMTBackendType
 {
-    METASMT_BACKEND_NONE,
     METASMT_BACKEND_STP,
     METASMT_BACKEND_Z3,
     METASMT_BACKEND_BOOLECTOR
 };
 
-extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT;
+extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
 #endif /* SUPPORT_METASMT */
 
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 906309d2..e3adac6a 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
+#include "klee/CommandLine.h" // FIXME: This is just for CoreSolverType
 #include "klee/Expr.h"
 
 #include <vector>
@@ -290,7 +291,9 @@ namespace klee {
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
   Solver *createDummySolver();
-  
+
+  // Create a solver based on the supplied ``CoreSolverType``.
+  Solver *createCoreSolver(CoreSolverType cst);
 }
 
 #endif
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index eac54141..d7157b25 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -75,18 +75,26 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 #ifdef SUPPORT_METASMT
 
-llvm::cl::opt<klee::MetaSMTBackendType>
-UseMetaSMT("use-metasmt",
-           llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."),
-           llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"),
-                      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"),
-                      clEnumValEnd),  
-           llvm::cl::init(METASMT_BACKEND_NONE));
+llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
+    "metasmt-backend",
+    llvm::cl::desc("Specify the MetaSMT solver backend type."),
+    llvm::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"),
+        clEnumValEnd),
+    llvm::cl::init(METASMT_BACKEND_STP));
 
 #endif /* SUPPORT_METASMT */
 
+llvm::cl::opt<CoreSolverType> CoreSolverToUse(
+    "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"),
+    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"),
+                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
+                     clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
+                     clEnumValEnd),
+    llvm::cl::init(STP_SOLVER));
 }
 
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9211f485..854754b0 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -107,29 +107,6 @@ using namespace llvm;
 using namespace klee;
 
 
-#ifdef SUPPORT_METASMT
-
-#include <metaSMT/frontend/Array.hpp>
-#include <metaSMT/backend/Z3_Backend.hpp>
-#include <metaSMT/backend/Boolector.hpp>
-#include <metaSMT/backend/MiniSAT.hpp>
-#include <metaSMT/DirectSolver_Context.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-#include <metaSMT/API/Stack.hpp>
-#include <metaSMT/API/Group.hpp>
-
-#define Expr VCExpr
-#define Type VCType
-#define STP STP_Backend
-#include <metaSMT/backend/STP.hpp>
-#undef Expr
-#undef Type
-#undef STP
-
-using namespace metaSMT;
-using namespace metaSMT::solver;
-
-#endif /* SUPPORT_METASMT */
 
 
 
@@ -293,50 +270,19 @@ Executor::Executor(const InterpreterOptions &opts,
       : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
       
   if (coreSolverTimeout) UseForkedCoreSolver = true;
-  
-  Solver *coreSolver = NULL;
-  
-#ifdef SUPPORT_METASMT
-  if (UseMetaSMT != METASMT_BACKEND_NONE) {
-    
-    std::string backend;
-    
-    switch (UseMetaSMT) {
-          case METASMT_BACKEND_STP:
-              backend = "STP"; 
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          case METASMT_BACKEND_Z3:
-              backend = "Z3";
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          case METASMT_BACKEND_BOOLECTOR:
-              backend = "Boolector";
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          default:
-              assert(false);
-              break;
-    };
-    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
-  }
-  else {
-    coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-  }
-#else
-  coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-#endif /* SUPPORT_METASMT */
-  
-   
-  Solver *solver = 
-    constructSolverChain(coreSolver,
-                         interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
-                         interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
-                         interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
-                         interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
-  
-  this->solver = new TimingSolver(solver, EqualitySubstitution);
+  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+  if (!coreSolver) {
+    llvm::errs() << "Failed to create core solver\n";
+    exit(1);
+  }
+  Solver *solver = constructSolverChain(
+      coreSolver,
+      interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
+      interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
+      interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
+      interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
 
+  this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
 }
 
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
new file mode 100644
index 00000000..9d21931d
--- /dev/null
+++ b/lib/Solver/CoreSolver.cpp
@@ -0,0 +1,87 @@
+//===-- CoreSolver.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/CommandLine.h"
+#include "klee/Solver.h"
+#include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/raw_ostream.h"
+#include <string>
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+static Solver *handleMetaSMT() {
+  Solver *coreSolver = NULL;
+  std::string backend;
+  switch (MetaSMTBackend) {
+  case METASMT_BACKEND_STP:
+    backend = "STP";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_Z3:
+    backend = "Z3";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_BOOLECTOR:
+    backend = "Boolector";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  default:
+    llvm_unreachable("Unrecognised metasmt backend");
+    break;
+  };
+  llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  return coreSolver;
+}
+#endif /* SUPPORT_METASMT */
+
+namespace klee {
+
+Solver *createCoreSolver(CoreSolverType cst) {
+  switch (cst) {
+  case STP_SOLVER:
+    llvm::errs() << "Using STP solver backend\n";
+    return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+  case METASMT_SOLVER:
+#ifdef SUPPORT_METASMT
+    llvm::errs() << "Using MetaSMT solver backend\n";
+    return handleMetaSMT();
+#else
+    llvm::errs() << "Not compiled with MetaSMT support\n";
+    return NULL;
+#endif
+  case DUMMY_SOLVER:
+    return createDummySolver();
+  default:
+    llvm_unreachable("Unsupported CoreSolverType");
+  }
+}
+}
diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.pc
index b8f839c3..b3ec63e3 100644
--- a/test/Solver/FastCexSolver.pc
+++ b/test/Solver/FastCexSolver.pc
@@ -1,4 +1,4 @@
-# RUN: %kleaver --use-fast-cex-solver --use-dummy-solver %s > %t
+# RUN: %kleaver --use-fast-cex-solver --solver-backend=dummy %s > %t
 # RUN: not grep FAIL %t
 
 array arr1[4] : w32 -> w8 = symbolic
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index af337abe..f91693c5 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -104,9 +104,6 @@ namespace {
                          "Fold constants and simplify expressions."),
               clEnumValEnd));
 
-  cl::opt<bool>
-  UseDummySolver("use-dummy-solver",
-		   cl::init(false));
 
   llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."),
 		                                               llvm::cl::init("."));
@@ -224,42 +221,9 @@ static bool EvaluateInputAST(const char *Filename,
   if (!success)
     return false;
 
-  // FIXME: Support choice of solver.
-  Solver *coreSolver = NULL; // 
-  
-#ifdef SUPPORT_METASMT
-  if (UseMetaSMT != METASMT_BACKEND_NONE) {
-    
-    std::string backend;
-    
-    switch (UseMetaSMT) {
-          case METASMT_BACKEND_STP:
-              backend = "STP"; 
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          case METASMT_BACKEND_Z3:
-              backend = "Z3";
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          case METASMT_BACKEND_BOOLECTOR:
-              backend = "Boolector";
-              coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
-              break;
-          default:
-              assert(false);
-              break;
-    };
-    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
-  }
-  else {
-    coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
-  }
-#else
-  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
-#endif /* SUPPORT_METASMT */
-  
-  
-  if (!UseDummySolver) {
+  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+
+  if (CoreSolverToUse != DUMMY_SOLVER) {
     if (0 != MaxCoreSolverTime) {
       coreSolver->setCoreSolverTimeout(MaxCoreSolverTime);
     }
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index 16bd3ce4..38e055cd 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -10,6 +10,7 @@
 #include <iostream>
 #include "gtest/gtest.h"
 
+#include "klee/CommandLine.h"
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Solver.h"
@@ -127,8 +128,7 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true,
 }
 
 TEST(SolverTest, Evaluation) {
-  STPSolver *stpSolver = new STPSolver(true); 
-  Solver *solver = stpSolver;
+  Solver *solver = klee::createCoreSolver(CoreSolverToUse);
 
   solver = createCexCachingSolver(solver);
   solver = createCachingSolver(solver);