5 files changed, 29 insertions, 18 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 0b34c357..4a21be3e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -337,7 +337,7 @@ Executor::Executor(const InterpreterOptions &opts,
   
   this->solver = new TimingSolver(solver, EqualitySubstitution);
 
-  memory = new MemoryManager();
+  memory = new MemoryManager(&arrayCache);
 }
 
 
@@ -2918,8 +2918,9 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   // and return it.
   
   static unsigned id;
-  const Array *array = Array::CreateArray("rrws_arr" + llvm::utostr(++id),
-					  Expr::getMinBytesForWidth(e->getWidth()));
+  const Array *array =
+      arrayCache.CreateArray("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::errs() << "Making symbolic: " << eq << "\n";
@@ -3257,7 +3258,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     while (!state.arrayNames.insert(uniqueName).second) {
       uniqueName = name + "_" + llvm::utostr(++id);
     }
-    const Array *array = Array::CreateArray(uniqueName, mo->size);
+    const Array *array = arrayCache.CreateArray(uniqueName, mo->size);
     bindObjectInState(state, mo, false, array);
     state.addSymbolic(mo, array);
     
@@ -3415,8 +3416,8 @@ void Executor::runFunctionAsMain(Function *f,
 
   // hack to clear memory objects
   delete memory;
-  memory = new MemoryManager();
-  
+  memory = new MemoryManager(NULL);
+
   globalObjects.clear();
   globalAddresses.clear();
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 523b3648..919d2124 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -20,6 +20,7 @@
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
+#include "klee/util/ArrayCache.h"
 
 #include "llvm/ADT/Twine.h"
 
@@ -177,7 +178,10 @@ private:
 
   /// The maximum time to allow for a single core solver query.
   /// (e.g. for a single STP query)
-  double coreSolverTimeout; 
+  double coreSolverTimeout;
+
+  /// Assumes ownership of the created array objects
+  ArrayCache arrayCache;
 
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 12ca7104..72f0a1fb 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -14,6 +14,7 @@
 #include "klee/Solver.h"
 #include "klee/util/BitArray.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/util/ArrayCache.h"
 
 #include "ObjectHolder.h"
 #include "MemoryManager.h"
@@ -110,9 +111,9 @@ ObjectState::ObjectState(const MemoryObject *mo)
     readOnly(false) {
   mo->refCount++;
   if (!UseConstantArrays) {
-    // FIXME: Leaked.
     static unsigned id = 0;
-    const Array *array = Array::CreateArray("tmp_arr" + llvm::utostr(++id), size);
+    const Array *array =
+        getArrayCache()->CreateArray("tmp_arr" + llvm::utostr(++id), size);
     updates = UpdateList(array, 0);
   }
   memset(concreteStore, 0, size);
@@ -176,6 +177,11 @@ ObjectState::~ObjectState() {
   }
 }
 
+ArrayCache *ObjectState::getArrayCache() const {
+  assert(object && "object was NULL");
+  return object->parent->getArrayCache();
+}
+
 /***/
 
 const UpdateList &ObjectState::getUpdates() const {
@@ -215,15 +221,10 @@ const UpdateList &ObjectState::getUpdates() const {
       Contents[Index->getZExtValue()] = Value;
     }
 
-    // FIXME: We should unique these, there is no good reason to create multiple
-    // ones.
-
-    // Start a new update list.
-    // FIXME: Leaked.
     static unsigned id = 0;
-    const Array *array = Array::CreateArray("const_arr" + llvm::utostr(++id), size,
-					    &Contents[0],
-					    &Contents[0] + Contents.size());
+    const Array *array = getArrayCache()->CreateArray(
+        "const_arr" + llvm::utostr(++id), size, &Contents[0],
+        &Contents[0] + Contents.size());
     updates = UpdateList(array, 0);
 
     // Apply the remaining (non-constant) writes.
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 637f8772..d08bfb0c 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -27,6 +27,7 @@ namespace klee {
 class BitArray;
 class MemoryManager;
 class Solver;
+class ArrayCache;
 
 class MemoryObject {
   friend class STPBuilder;
@@ -234,6 +235,7 @@ private:
   void setKnownSymbolic(unsigned offset, Expr *value);
 
   void print();
+  ArrayCache *getArrayCache() const;
 };
   
 } // End klee namespace
diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h
index f398db62..01683443 100644
--- a/lib/Core/MemoryManager.h
+++ b/lib/Core/MemoryManager.h
@@ -19,14 +19,16 @@ namespace llvm {
 
 namespace klee {
   class MemoryObject;
+  class ArrayCache;
 
   class MemoryManager {
   private:
     typedef std::set<MemoryObject*> objects_ty;
     objects_ty objects;
+    ArrayCache *const arrayCache;
 
   public:
-    MemoryManager() {}
+    MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {}
     ~MemoryManager();
 
     MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal,
@@ -35,6 +37,7 @@ namespace klee {
                                 const llvm::Value *allocSite);
     void deallocate(const MemoryObject *mo);
     void markFreed(MemoryObject *mo);
+    ArrayCache *getArrayCache() const { return arrayCache; }
   };
 
 } // End klee namespace