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

3 files changed, 14 insertions, 7 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index dc787ad6..09cf4b47 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -157,7 +157,9 @@ namespace klee {
     ///
     /// \param useForkedSTP - Whether STP should be run in a separate process
     /// (required for using timeouts).
-    STPSolver(bool useForkedSTP);
+    /// \param optimizeDivides - Whether constant division operations should
+    /// be optimized into add/shift/multiply operations.
+    STPSolver(bool useForkedSTP, bool optimizeDivides = true);
 
     
     
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))
 {
 }