From a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 27 Mar 2019 11:33:07 +0000 Subject: Separate constraint set and constraint manager --- lib/Core/ExecutionState.cpp | 16 +++++++++++----- lib/Core/ExecutionState.h | 5 +++-- lib/Core/Executor.cpp | 8 ++++---- lib/Core/ImpliedValue.cpp | 23 ++++++++++------------- lib/Core/TimingSolver.cpp | 6 +++--- lib/Core/TimingSolver.h | 1 + 6 files changed, 32 insertions(+), 27 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 14d596fc..0b848f41 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -310,11 +310,12 @@ bool ExecutionState::merge(const ExecutionState &b) { } } - constraints = ConstraintManager(); - for (std::set< ref >::iterator it = commonConstraints.begin(), - ie = commonConstraints.end(); it != ie; ++it) - constraints.addConstraint(*it); - constraints.addConstraint(OrExpr::create(inA, inB)); + constraints = ConstraintSet(); + + ConstraintManager m(constraints); + for (const auto &constraint : commonConstraints) + m.addConstraint(constraint); + m.addConstraint(OrExpr::create(inA, inB)); return true; } @@ -352,3 +353,8 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const { target = sf.caller; } } + +void ExecutionState::addConstraint(ref e) { + ConstraintManager c(constraints); + c.addConstraint(e); +} diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index f1b09644..397b2364 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -92,7 +92,7 @@ public: AddressSpace addressSpace; /// @brief Constraints collected so far - ConstraintManager constraints; + ConstraintSet constraints; /// Statistics and information @@ -171,7 +171,8 @@ public: void popFrame(); void addSymbolic(const MemoryObject *mo, const Array *array); - void addConstraint(ref e) { constraints.addConstraint(std::move(e)); } + + void addConstraint(ref e); bool merge(const ExecutionState &b); void dumpStack(llvm::raw_ostream &out) const; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index af376755..39de6e8d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1252,7 +1252,7 @@ ref Executor::toConstant(ExecutionState &state, ref e, const char *reason) { - e = state.constraints.simplifyExpr(e); + e = ConstraintManager::simplifyExpr(state.constraints, e); if (ConstantExpr *CE = dyn_cast(e)) return CE; @@ -1280,7 +1280,7 @@ Executor::toConstant(ExecutionState &state, void Executor::executeGetValue(ExecutionState &state, ref e, KInstruction *target) { - e = state.constraints.simplifyExpr(e); + e = ConstraintManager::simplifyExpr(state.constraints, e); std::map< ExecutionState*, std::vector >::iterator it = seedMap.find(&state); if (it==seedMap.end() || isa(e)) { @@ -3651,9 +3651,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (SimplifySymIndices) { if (!isa(address)) - address = state.constraints.simplifyExpr(address); + address = ConstraintManager::simplifyExpr(state.constraints, address); if (isWrite && !isa(value)) - value = state.constraints.simplifyExpr(value); + value = ConstraintManager::simplifyExpr(state.constraints, value); } address = optimizer.optimizeExpr(address, true); diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index a09e4b7c..4baec512 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -193,14 +193,12 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref e, getImpliedValues(e, value, results); - for (ImpliedValueList::iterator i = results.begin(), ie = results.end(); - i != ie; ++i) { - std::map, ref >::iterator it = - found.find(i->first); + for (auto &i : results) { + auto it = found.find(i.first); if (it != found.end()) { - assert(it->second == i->second && "Invalid ImpliedValue!"); + assert(it->second == i.second && "Invalid ImpliedValue!"); } else { - found.insert(std::make_pair(i->first, i->second)); + found.insert(std::make_pair(i.first, i.second)); } } @@ -208,7 +206,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref e, std::set< ref > readsSet(reads.begin(), reads.end()); reads = std::vector< ref >(readsSet.begin(), readsSet.end()); - std::vector > assumption; + ConstraintSet assumption; assumption.push_back(EqExpr::create(e, value)); // obscure... we need to make sure that all the read indices are @@ -225,16 +223,15 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref e, Context::get().getPointerWidth()))); } - ConstraintManager assume(assumption); - for (std::vector< ref >::iterator i = reads.begin(), - ie = reads.end(); i != ie; ++i) { - ref var = *i; + for (const auto &var : reads) { ref possible; - bool success = S->getValue(Query(assume, var), possible); (void) success; + bool success = S->getValue(Query(assumption, var), possible); + (void)success; assert(success && "FIXME: Unhandled solver failure"); std::map, ref >::iterator it = found.find(var); bool res; - success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res); + success = + S->mustBeTrue(Query(assumption, EqExpr::create(var, possible)), res); assert(success && "FIXME: Unhandled solver failure"); if (res) { if (it != found.end()) { diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index d525a9db..cc0afff8 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -34,7 +34,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = state.constraints.simplifyExpr(expr); + expr = ConstraintManager::simplifyExpr(state.constraints, expr); bool success = solver->evaluate(Query(state.constraints, expr), result); @@ -54,7 +54,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = state.constraints.simplifyExpr(expr); + expr = ConstraintManager::simplifyExpr(state.constraints, expr); bool success = solver->mustBeTrue(Query(state.constraints, expr), result); @@ -97,7 +97,7 @@ bool TimingSolver::getValue(const ExecutionState& state, ref expr, TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) - expr = state.constraints.simplifyExpr(expr); + expr = ConstraintManager::simplifyExpr(state.constraints, expr); bool success = solver->getValue(Query(state.constraints, expr), result); diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index f6dfd5b9..8e25b21c 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -10,6 +10,7 @@ #ifndef KLEE_TIMINGSOLVER_H #define KLEE_TIMINGSOLVER_H +#include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Solver/Solver.h" #include "klee/System/Time.h" -- cgit 1.4.1