Added --stp-optimize-divides flag. Patch submitted by Peter

Collingbourne: "This flag controls whether constant divides are
optimized into add/shift/multiplies before passing to STP, and is set
by default.  In some circumstances the use of this optimisation can
actually slow the solver down, so it is best to allow the user to
disable it."



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102069 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 11 insertions, 6 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index fd6cf441..17b87873 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -249,6 +249,11 @@ namespace {
   cl::opt<bool>
   UseForkedSTP("use-forked-stp", 
                  cl::desc("Run STP in forked process"));
+
+  cl::opt<bool>
+  STPOptimizeDivides("stp-optimize-divides", 
+                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP"),
+                 cl::init(true));
 }
 
 
@@ -314,7 +319,7 @@ Executor::Executor(const InterpreterOptions &opts,
     stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
       ? std::min(MaxSTPTime,MaxInstructionTime)
       : std::max(MaxSTPTime,MaxInstructionTime)) {
-  STPSolver *stpSolver = new STPSolver(UseForkedSTP);
+  STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
   Solver *solver = 
     constructSolverChain(stpSolver,
                          interpreterHandler->getOutputFilename("queries.qlog"),
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 5dd24273..1d13a11d 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -420,7 +420,7 @@ private:
   bool useForkedSTP;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP);
+  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
 
   char *getConstraintLog(const Query&);
@@ -443,10 +443,10 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP) 
+STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
   : solver(_solver),
     vc(vc_createValidityChecker()),
-    builder(new STPBuilder(vc)),
+    builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP)
 {
@@ -472,8 +472,8 @@ STPSolverImpl::~STPSolverImpl() {
 
 /***/
 
-STPSolver::STPSolver(bool useForkedSTP) 
-  : Solver(new STPSolverImpl(this, useForkedSTP))
+STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
+  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
 {
 }