From 8a0f1af7500e10dadd97300f242424917d2e9902 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 1 Apr 2019 14:08:43 +0100 Subject: Use constraint sets and separate metadata for timing solver invocation Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints) --- lib/Core/TimingSolver.cpp | 81 ++++++++++++++++++++++++----------------------- 1 file changed, 42 insertions(+), 39 deletions(-) (limited to 'lib/Core/TimingSolver.cpp') diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index cc0afff8..fc31e72d 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -23,8 +23,9 @@ using namespace llvm; /***/ -bool TimingSolver::evaluate(const ExecutionState& state, ref expr, - Solver::Validity &result) { +bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, + Solver::Validity &result, + SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? Solver::True : Solver::False; @@ -34,17 +35,17 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->evaluate(Query(state.constraints, expr), result); + bool success = solver->evaluate(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? true : false; @@ -54,40 +55,41 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->mustBeTrue(Query(state.constraints, expr), result); + bool success = solver->mustBeTrue(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool TimingSolver::mustBeFalse(const ExecutionState& state, ref expr, - bool &result) { - return mustBeTrue(state, Expr::createIsZero(expr), result); +bool TimingSolver::mustBeFalse(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { + return mustBeTrue(constraints, Expr::createIsZero(expr), result, metaData); } -bool TimingSolver::mayBeTrue(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mayBeTrue(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { bool res; - if (!mustBeFalse(state, expr, res)) + if (!mustBeFalse(constraints, expr, res, metaData)) return false; result = !res; return true; } -bool TimingSolver::mayBeFalse(const ExecutionState& state, ref expr, - bool &result) { +bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref expr, + bool &result, SolverQueryMetaData &metaData) { bool res; - if (!mustBeTrue(state, expr, res)) + if (!mustBeTrue(constraints, expr, res, metaData)) return false; result = !res; return true; } -bool TimingSolver::getValue(const ExecutionState& state, ref expr, - ref &result) { +bool TimingSolver::getValue(const ConstraintSet &constraints, ref expr, + ref &result, + SolverQueryMetaData &metaData) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE; @@ -97,36 +99,37 @@ bool TimingSolver::getValue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = ConstraintManager::simplifyExpr(state.constraints, expr); + expr = ConstraintManager::simplifyExpr(constraints, expr); - bool success = solver->getValue(Query(state.constraints, expr), result); + bool success = solver->getValue(Query(constraints, expr), result); - state.queryCost += timer.delta(); + metaData.queryCost += timer.delta(); return success; } -bool -TimingSolver::getInitialValues(const ExecutionState& state, - const std::vector - &objects, - std::vector< std::vector > - &result) { +bool TimingSolver::getInitialValues( + const ConstraintSet &constraints, const std::vector &objects, + std::vector> &result, + SolverQueryMetaData &metaData) { if (objects.empty()) return true; TimerStatIncrementer timer(stats::solverTime); - bool success = solver->getInitialValues(Query(state.constraints, - ConstantExpr::alloc(0, Expr::Bool)), - objects, result); - - state.queryCost += timer.delta(); - + bool success = solver->getInitialValues( + Query(constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result); + + metaData.queryCost += timer.delta(); + return success; } -std::pair< ref, ref > -TimingSolver::getRange(const ExecutionState& state, ref expr) { - return solver->getRange(Query(state.constraints, expr)); +std::pair, ref> +TimingSolver::getRange(const ConstraintSet &constraints, ref expr, + SolverQueryMetaData &metaData) { + TimerStatIncrementer timer(stats::solverTime); + auto result = solver->getRange(Query(constraints, expr)); + metaData.queryCost += timer.delta(); + return result; } -- cgit 1.4.1