aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/ExecutionState.h4
-rw-r--r--lib/Core/Executor.cpp180
2 files changed, 133 insertions, 51 deletions
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 20187166..833537f2 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -248,6 +248,10 @@ public:
/// @brief Disables forking for this state. Set by user code
bool forkDisabled = false;
+ /// @brief Mapping symbolic address expressions to concrete base addresses
+ typedef std::map<ref<Expr>, ref<ConstantExpr>> base_addrs_t;
+ base_addrs_t base_addrs;
+
public:
#ifdef KLEE_UNITTEST
// provide this function only in the context of unittests
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index cf6ce777..b96ea843 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -466,6 +466,12 @@ cl::opt<bool> DebugCheckForImpliedValues(
cl::desc("Debug the implied value optimization"),
cl::cat(DebugCat));
+/*** Misc options ***/
+cl::opt<bool> SingleObjectResolution(
+ "single-object-resolution",
+ cl::desc("Try to resolve memory reads/writes to single objects "
+ "when offsets are symbolic (default=false)"),
+ cl::init(false), cl::cat(MiscCat));
} // namespace
// XXX hack
@@ -2784,6 +2790,26 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
ref<Expr> base = eval(ki, 0, state).value;
+ bool const_base = isa<ConstantExpr>(base);
+ bool update = false;
+ ref<ConstantExpr> original_base = 0;
+ ref<Expr> key = 0;
+ ref<ConstantExpr> value = 0;
+
+ if (SingleObjectResolution) {
+ ExecutionState::base_addrs_t::iterator base_it;
+ if (!const_base) {
+ base_it = state.base_addrs.find(base);
+ if (base_it != state.base_addrs.end()) {
+ update = true;
+ key = base_it->first;
+ value = base_it->second;
+ }
+ } else {
+ original_base = dyn_cast<ConstantExpr>(base);
+ }
+ }
+
for (std::vector< std::pair<unsigned, uint64_t> >::iterator
it = kgepi->indices.begin(), ie = kgepi->indices.end();
it != ie; ++it) {
@@ -2796,6 +2822,22 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
if (kgepi->offset)
base = AddExpr::create(base,
Expr::createPointer(kgepi->offset));
+
+ if (SingleObjectResolution) {
+ if (const_base && !isa<ConstantExpr>(base)) {
+ // the initial base address was a constant expression, the final is not:
+ // store the mapping between constant address and the non-const
+ // reference in the state
+ state.base_addrs[base] = original_base;
+ }
+
+ if (update) {
+ // we need to update the current entry with a new value
+ state.base_addrs[base] = value;
+ state.base_addrs.erase(key);
+ }
+ }
+
bindLocal(ki, state, base);
break;
}
@@ -4305,71 +4347,107 @@ void Executor::executeMemoryOperation(ExecutionState &state,
address = optimizer.optimizeExpr(address, true);
- // fast path: single in-bounds resolution
ObjectPair op;
bool success;
solver->setTimeout(coreSolverTimeout);
- if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) {
- address = toConstant(state, address, "resolveOne failure");
- success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
- }
- solver->setTimeout(time::Span());
-
- if (success) {
- const MemoryObject *mo = op.first;
- if (MaxSymArraySize && mo->size >= MaxSymArraySize) {
- address = toConstant(state, address, "max-sym-array-size");
+ bool resolveSingleObject = SingleObjectResolution;
+
+ if (resolveSingleObject && !isa<ConstantExpr>(address)) {
+ // Address is symbolic
+
+ resolveSingleObject = false;
+ ExecutionState::base_addrs_t::iterator base_it =
+ state.base_addrs.find(address);
+ if (base_it != state.base_addrs.end()) {
+ // Concrete address found in the map, now find the associated memory
+ // object
+ if (!state.addressSpace.resolveOne(state, solver.get(), base_it->second, op,
+ success) ||
+ !success) {
+ klee_warning("Failed to resolve concrete address from the base_addrs "
+ "map to a memory object");
+ } else {
+ // We have resolved the stored concrete address to a memory object.
+ // Now let's see if we can prove an overflow - we are only interested in
+ // two cases: either we overflow and it's a bug or we don't and we carry
+ // on; in this mode we are not interested in trying out other memory
+ // objects
+ resolveSingleObject = true;
+ }
}
-
- ref<Expr> offset = mo->getOffsetExpr(address);
- ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes);
- check = optimizer.optimizeExpr(check, true);
+ } else {
+ resolveSingleObject = false;
+ }
- bool inBounds;
- solver->setTimeout(coreSolverTimeout);
- bool success = solver->mustBeTrue(state.constraints, check, inBounds,
- state.queryMetaData);
- solver->setTimeout(time::Span());
- if (!success) {
- state.pc = state.prevPC;
- terminateStateOnSolverError(state, "Query timed out (bounds check).");
- return;
+ if (!resolveSingleObject) {
+ if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) {
+ address = toConstant(state, address, "resolveOne failure");
+ success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
}
+ solver->setTimeout(time::Span());
- if (inBounds) {
- const ObjectState *os = op.second;
- if (isWrite) {
- if (os->readOnly) {
- terminateStateOnProgramError(state, "memory error: object read only",
- StateTerminationType::ReadOnly);
- } else {
- ObjectState *wos = state.addressSpace.getWriteable(mo, os);
- wos->write(offset, value);
- }
- } else {
- ref<Expr> result = os->read(offset, type);
-
- if (interpreterOpts.MakeConcreteSymbolic)
- result = replaceReadWithSymbolic(state, result);
-
- bindLocal(target, state, result);
+ if (success) {
+ const MemoryObject *mo = op.first;
+
+ if (MaxSymArraySize && mo->size >= MaxSymArraySize) {
+ address = toConstant(state, address, "max-sym-array-size");
}
- return;
+ ref<Expr> offset = mo->getOffsetExpr(address);
+ ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes);
+ check = optimizer.optimizeExpr(check, true);
+
+ bool inBounds;
+ solver->setTimeout(coreSolverTimeout);
+ bool success = solver->mustBeTrue(state.constraints, check, inBounds,
+ state.queryMetaData);
+ solver->setTimeout(time::Span());
+ if (!success) {
+ state.pc = state.prevPC;
+ terminateStateOnSolverError(state, "Query timed out (bounds check).");
+ return;
+ }
+
+ if (inBounds) {
+ const ObjectState *os = op.second;
+ if (isWrite) {
+ if (os->readOnly) {
+ terminateStateOnProgramError(state, "memory error: object read only",
+ StateTerminationType::ReadOnly);
+ } else {
+ ObjectState *wos = state.addressSpace.getWriteable(mo, os);
+ wos->write(offset, value);
+ }
+ } else {
+ ref<Expr> result = os->read(offset, type);
+
+ if (interpreterOpts.MakeConcreteSymbolic)
+ result = replaceReadWithSymbolic(state, result);
+
+ bindLocal(target, state, result);
+ }
+
+ return;
+ }
}
- }
+ }
// we are on an error path (no resolution, multiple resolution, one
- // resolution with out of bounds)
+ // resolution with out of bounds), or we do a single object resolution
address = optimizer.optimizeExpr(address, true);
- ResolutionList rl;
- solver->setTimeout(coreSolverTimeout);
- bool incomplete = state.addressSpace.resolve(state, solver.get(), address, rl,
- 0, coreSolverTimeout);
- solver->setTimeout(time::Span());
-
+ ResolutionList rl;
+ bool incomplete = false;
+
+ if (!resolveSingleObject) {
+ solver->setTimeout(coreSolverTimeout);
+ incomplete = state.addressSpace.resolve(state, solver.get(), address, rl, 0,
+ coreSolverTimeout);
+ solver->setTimeout(time::Span());
+ } else {
+ rl.push_back(op); // we already have the object pair, no need to look for it
+ }
// XXX there is some query wasteage here. who cares?
ExecutionState *unbound = &state;
@@ -4401,7 +4479,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
if (!unbound)
break;
}
-
+
// XXX should we distinguish out of bounds and overlapped cases?
if (unbound) {
if (incomplete) {
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-20 22:47:43 +0000