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

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",