diff options
| -rw-r--r-- | include/klee/Solver.h | 4 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 7 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 10 |
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)) { } |