diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:16:49 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:16:49 +0000 |
commit | 171810d97c206c090ff588729f1ee16f9d47cbfb (patch) | |
tree | c3d9bafcd329cfca3293bc71cb4d5ead2512f043 | |
parent | 7c27c8a6a7c233c3c6162d9b86942351fe5f42b3 (diff) | |
download | klee-171810d97c206c090ff588729f1ee16f9d47cbfb.tar.gz |
Change AddressSpace::resolveOne to take a ConstantExpr directly (and to allow
64-bit addresses). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73327 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | lib/Core/AddressSpace.cpp | 9 | ||||
-rw-r--r-- | lib/Core/AddressSpace.h | 2 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 2 | ||||
-rw-r--r-- | lib/Core/MemoryManager.cpp | 3 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 4 |
5 files changed, 11 insertions, 9 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 5b73a6f6..1e683e34 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -51,8 +51,9 @@ ObjectState *AddressSpace::getWriteable(const MemoryObject *mo, /// -bool AddressSpace::resolveOne(uint64_t addr64, ObjectPair &result) { - unsigned address = (unsigned) addr64; +bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr, + ObjectPair &result) { + uint64_t address = addr->getZExtValue(); MemoryObject hack(address); if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) { @@ -73,7 +74,7 @@ bool AddressSpace::resolveOne(ExecutionState &state, ObjectPair &result, bool &success) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) { - success = resolveOne(CE->getConstantValue(), result); + success = resolveOne(CE, result); return true; } else { TimerStatIncrementer timer(stats::resolveTime); @@ -165,7 +166,7 @@ bool AddressSpace::resolve(ExecutionState &state, double timeout) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) { ObjectPair res; - if (resolveOne(CE->getConstantValue(), res)) + if (resolveOne(CE, res)) rl.push_back(res); return false; } else { diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index a281714c..079453b3 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -58,7 +58,7 @@ namespace klee { /// Resolve address to an ObjectPair in result. /// \return true iff an object was found. - bool resolveOne(uint64_t address, + bool resolveOne(const ref<ConstantExpr> &address, ObjectPair &result); /// Resolve address to an ObjectPair in result. diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 5b22b782..2be099bd 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2838,7 +2838,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, solver->setTimeout(stpTimeout); if (!state.addressSpace.resolveOne(state, solver, address, op, success)) { address = toConstant(state, address, "resolveOne failure"); - success = state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op); + success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op); } solver->setTimeout(0); diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index 72c1b67f..69bbd6e3 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -31,7 +31,8 @@ MemoryManager::~MemoryManager() { } } -MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, bool isGlobal, +MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, + bool isGlobal, const llvm::Value *allocSite) { if (size>10*1024*1024) { klee_warning_once(0, "failing large alloc: %u bytes", (unsigned) size); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index d2c68b77..11705722 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -178,7 +178,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ObjectPair op; addressExpr = executor.toUnique(state, addressExpr); ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr); - if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) + if (!state.addressSpace.resolveOne(address, op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); bool res; assert(executor.solver->mustBeTrue(state, @@ -599,7 +599,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, } else { ObjectPair op; - if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op)) { + if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) { executor.terminateStateOnError(state, "check_memory_access: memory error", "ptr.err", |