diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/ExecutionState.h | 4 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 180 |
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) { |