aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp16
-rw-r--r--lib/Core/ExecutionState.h5
-rw-r--r--lib/Core/Executor.cpp8
-rw-r--r--lib/Core/ImpliedValue.cpp23
-rw-r--r--lib/Core/TimingSolver.cpp6
-rw-r--r--lib/Core/TimingSolver.h1
6 files changed, 32 insertions, 27 deletions
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<Expr> >::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<Expr> 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<Expr> e) { constraints.addConstraint(std::move(e)); }
+
+ void addConstraint(ref<Expr> 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<klee::ConstantExpr>
Executor::toConstant(ExecutionState &state,
ref<Expr> e,
const char *reason) {
- e = state.constraints.simplifyExpr(e);
+ e = ConstraintManager::simplifyExpr(state.constraints, e);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
return CE;
@@ -1280,7 +1280,7 @@ Executor::toConstant(ExecutionState &state,
void Executor::executeGetValue(ExecutionState &state,
ref<Expr> e,
KInstruction *target) {
- e = state.constraints.simplifyExpr(e);
+ e = ConstraintManager::simplifyExpr(state.constraints, e);
std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it =
seedMap.find(&state);
if (it==seedMap.end() || isa<ConstantExpr>(e)) {
@@ -3651,9 +3651,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
if (SimplifySymIndices) {
if (!isa<ConstantExpr>(address))
- address = state.constraints.simplifyExpr(address);
+ address = ConstraintManager::simplifyExpr(state.constraints, address);
if (isWrite && !isa<ConstantExpr>(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<Expr> e,
getImpliedValues(e, value, results);
- for (ImpliedValueList::iterator i = results.begin(), ie = results.end();
- i != ie; ++i) {
- std::map<ref<ReadExpr>, ref<ConstantExpr> >::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<Expr> e,
std::set< ref<ReadExpr> > readsSet(reads.begin(), reads.end());
reads = std::vector< ref<ReadExpr> >(readsSet.begin(), readsSet.end());
- std::vector<ref<Expr> > 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<Expr> e,
Context::get().getPointerWidth())));
}
- ConstraintManager assume(assumption);
- for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(),
- ie = reads.end(); i != ie; ++i) {
- ref<ReadExpr> var = *i;
+ for (const auto &var : reads) {
ref<ConstantExpr> 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<ReadExpr>, ref<ConstantExpr> >::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> 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> 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> 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"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-24 04:12:08 +0000