diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:07:30 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:07:30 +0000 |
commit | 7c27c8a6a7c233c3c6162d9b86942351fe5f42b3 (patch) | |
tree | 876b610183e2e4d470139b8544cd6cdbf22a6982 /lib/Core | |
parent | d15a30cc0ce2579747ae4c2e919af54c6b06af70 (diff) | |
download | klee-7c27c8a6a7c233c3c6162d9b86942351fe5f42b3.tar.gz |
Add ConstantExpr::{getLimitedValue,getZExtValue}.
- For use in situations where the range of the constant is known to fit in a uint64 (or smaller), or the extra bits don't matter. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73326 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 13 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 4 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 10 |
3 files changed, 13 insertions, 14 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index f12aec08..5b22b782 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Somewhat gross to create these all the time, but fine till we // switch to an internal rep. ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(), - CE->getConstantValue()); + CE->getZExtValue()); unsigned index = si->findCaseValue(ci); transferToBasicBlock(si->getSuccessor(index), si->getParent(), state); } else { @@ -2688,11 +2688,10 @@ void Executor::executeAlloc(ExecutionState &state, assert(success && "FIXME: Unhandled solver failure"); (void) success; - // Try and start with a small example - while (example->getConstantValue() > 128) { - ref<ConstantExpr> tmp = - ConstantExpr::alloc(example->getConstantValue() >> 1, - example->getWidth()); + // Try and start with a small example. + Expr::Width W = example->getWidth(); + while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) { + ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W)); bool res; bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res); assert(success && "FIXME: Unhandled solver failure"); @@ -3225,7 +3224,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, assert(!os->readOnly && "not possible? read only object with static read?"); ObjectState *wos = state.addressSpace.getWriteable(mo, os); - wos->write(CE->getConstantValue(), it->second); + wos->write(CE, it->second); } } } diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index d8cf0bdb..49198df8 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -187,7 +187,7 @@ const UpdateList &ObjectState::getUpdates() const { if (!Value) break; - Contents[Index->getConstantValue()] = Value; + Contents[Index->getZExtValue()] = Value; } // FIXME: We should unique these, there is no good reason to create multiple @@ -400,7 +400,7 @@ void ObjectState::write8(unsigned offset, uint8_t value) { void ObjectState::write8(unsigned offset, ref<Expr> value) { // can happen when ExtractExpr special cases if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { - write8(offset, (uint8_t) CE->getConstantValue()); + write8(offset, (uint8_t) CE->getZExtValue(8)); } else { setKnownSymbolic(offset, value.get()); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 2ee73457..d2c68b77 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -198,7 +198,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, cur = executor.toUnique(state, cur); assert(isa<ConstantExpr>(cur) && "hit symbolic char while reading concrete string"); - buf[i] = cast<ConstantExpr>(cur)->getConstantValue(); + buf[i] = cast<ConstantExpr>(cur)->getZExtValue(8); } buf[i] = 0; @@ -441,7 +441,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, ref<Expr> value = executor.toUnique(state, arguments[0]); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { - state.forkDisabled = !CE->getConstantValue(); + state.forkDisabled = CE->isZero(); } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", @@ -607,7 +607,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, } else { ref<Expr> chk = op.first->getBoundsCheckPointer(address, cast<ConstantExpr>(size)->getConstantValue()); - if (!cast<ConstantExpr>(chk)->getConstantValue()) { + if (!chk->isTrue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", "ptr.err", @@ -636,8 +636,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state, assert(isa<ConstantExpr>(arguments[1]) && "expect constant size argument to klee_define_fixed_object"); - uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue(); - uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue(); + uint64_t address = cast<ConstantExpr>(arguments[0])->getZExtValue(); + uint64_t size = cast<ConstantExpr>(arguments[1])->getZExtValue(); MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst); executor.bindObjectInState(state, mo, false); mo->isUserSpecified = true; // XXX hack; |