Use Arrays instead of MemoryObject where possible.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73160 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 9 insertions, 10 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e47dcfc0..4c5f9511 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -50,6 +50,7 @@
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
 #include "llvm/Module.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/GetElementPtrTypeIterator.h"
@@ -2606,11 +2607,10 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   // create a new fresh location, assert it is equal to concrete value in e
   // and return it.
   
-  const MemoryObject *mo =
-    memory->allocate(Expr::getMinBytesForWidth(e->getWidth()), false, false,
-                     state.prevPC->inst);
-  assert(mo && "out of memory");
-  ref<Expr> res = Expr::createTempRead(mo->array, e->getWidth());
+  static unsigned id;
+  const Array *array = new Array("rrws_arr" + llvm::utostr(++id), 
+                                 Expr::getMinBytesForWidth(e->getWidth()));
+  ref<Expr> res = Expr::createTempRead(array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
   llvm::cerr << "Making symbolic: " << eq << "\n";
   state.addConstraint(eq);
@@ -2943,6 +2943,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     os->makeSymbolic();
     state.addSymbolic(mo);
     
+    const Array *array = os->updates.root;
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
       seedMap.find(&state);
     if (it!=seedMap.end()) { // In seed mode we need to add this as a
@@ -2955,8 +2956,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
 
         if (!obj) {
           if (ZeroSeedExtension) {
-            std::vector<unsigned char> &values = 
-              si.assignment.bindings[mo->array];
+            std::vector<unsigned char> &values = si.assignment.bindings[array];
             values = std::vector<unsigned char>(mo->size, '\0');
           } else if (!AllowSeedExtension) {
             terminateStateOnError(state, 
@@ -2980,10 +2980,9 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
                                   "user.err");
             break;
           } else {
-            std::vector<unsigned char> &values = 
-              si.assignment.bindings[mo->array];
+            std::vector<unsigned char> &values = si.assignment.bindings[array];
             values.insert(values.begin(), obj->bytes, 
-                          obj->bytes + std::min(obj->numBytes, mo->size));            
+                          obj->bytes + std::min(obj->numBytes, mo->size));
             if (ZeroSeedExtension) {
               for (unsigned i=obj->numBytes; i<mo->size; ++i)
                 values.push_back('\0');