From bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 22 Apr 2010 16:14:41 +0000 Subject: 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 --- lib/Core/Executor.cpp | 7 ++++++- lib/Solver/Solver.cpp | 10 +++++----- 2 files changed, 11 insertions(+), 6 deletions(-) (limited to 'lib') 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 UseForkedSTP("use-forked-stp", cl::desc("Run STP in forked process")); + + cl::opt + 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)) { } -- cgit 1.4.1