Use `ref<>` for MemoryObject handling

This uses the `ref<>`-based memory handling of MemoryObjects.
This makes it explicit that references are held in:
 - ExecutionState::symbolics
 - ObjectState

6 files changed, 40 insertions, 49 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 95808be1..e647d0ab 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -132,7 +132,7 @@ public:
   /// @brief Ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
+  std::vector<std::pair<ref<const MemoryObject>, const Array *>> symbolics;
 
   /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 78aa8f67..eadf7e11 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -83,20 +83,10 @@ ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
     : constraints(assumptions), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
-  for (unsigned int i=0; i<symbolics.size(); i++)
-  {
-    const MemoryObject *mo = symbolics[i].first;
-    assert(mo->refCount > 0);
-    mo->refCount--;
-    if (mo->refCount == 0)
-      delete mo;
-  }
-
   for (auto cur_mergehandler: openMergeStack){
     cur_mergehandler->removeOpenState(this);
   }
 
-
   while (!stack.empty()) popFrame();
 }
 
@@ -123,11 +113,7 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     symbolics(state.symbolics),
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
-    steppedInstructions(state.steppedInstructions)
-{
-  for (unsigned int i=0; i<symbolics.size(); i++)
-    symbolics[i].first->refCount++;
-
+    steppedInstructions(state.steppedInstructions) {
   for (auto cur_mergehandler: openMergeStack)
     cur_mergehandler->addOpenState(this);
 }
@@ -154,9 +140,8 @@ void ExecutionState::popFrame() {
   stack.pop_back();
 }
 
-void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) { 
-  mo->refCount++;
-  symbolics.push_back(std::make_pair(mo, array));
+void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) {
+  symbolics.emplace_back(std::make_pair(ref<const MemoryObject>(mo), array));
 }
 
 /**/
@@ -183,7 +168,8 @@ bool ExecutionState::merge(const ExecutionState &b) {
 
   // XXX is it even possible for these to differ? does it matter? probably
   // implies difference in object states?
-  if (symbolics!=b.symbolics)
+
+  if (symbolics != b.symbolics)
     return false;
 
   {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b10a8850..8845f11d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3894,7 +3894,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   // an example) While this process can be very expensive, it can
   // also make understanding individual test cases much easier.
   for (unsigned i = 0; i != state.symbolics.size(); ++i) {
-    const MemoryObject *mo = state.symbolics[i].first;
+    const auto &mo = state.symbolics[i].first;
     std::vector< ref<Expr> >::const_iterator pi = 
       mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
     for (; pi != pie; ++pi) {
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 37e6646b..ce537a4c 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -82,7 +82,6 @@ ObjectState::ObjectState(const MemoryObject *mo)
     updates(0, 0),
     size(mo->size),
     readOnly(false) {
-  mo->refCount++;
   if (!UseConstantArrays) {
     static unsigned id = 0;
     const Array *array =
@@ -103,7 +102,6 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
     updates(array, 0),
     size(mo->size),
     readOnly(false) {
-  mo->refCount++;
   makeSymbolic();
   memset(concreteStore, 0, size);
 }
@@ -119,9 +117,6 @@ ObjectState::ObjectState(const ObjectState &os)
     size(os.size),
     readOnly(false) {
   assert(!os.readOnly && "no need to copy read only object?");
-  if (object)
-    object->refCount++;
-
   if (os.knownSymbolics) {
     knownSymbolics = new ref<Expr>[size];
     for (unsigned i=0; i<size; i++)
@@ -136,20 +131,10 @@ ObjectState::~ObjectState() {
   delete flushMask;
   delete[] knownSymbolics;
   delete[] concreteStore;
-
-  if (object)
-  {
-    assert(object->refCount > 0);
-    object->refCount--;
-    if (object->refCount == 0)
-    {
-      delete object;
-    }
-  }
 }
 
 ArrayCache *ObjectState::getArrayCache() const {
-  assert(object && "object was NULL");
+  assert(!object.isNull() && "object was NULL");
   return object->parent->getArrayCache();
 }
 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index e4260c55..2ab7cd22 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -35,10 +35,13 @@ class MemoryObject {
   friend class STPBuilder;
   friend class ObjectState;
   friend class ExecutionState;
+  friend class ref<MemoryObject>;
+  friend class ref<const MemoryObject>;
 
 private:
   static int counter;
-  mutable unsigned refCount;
+  /// @brief Required by klee::ref-managed objects
+  mutable class ReferenceCounter _refCount;
 
 public:
   unsigned id;
@@ -75,8 +78,7 @@ public:
   // XXX this is just a temp hack, should be removed
   explicit
   MemoryObject(uint64_t _address) 
-    : refCount(0),
-      id(counter++), 
+    : id(counter++),
       address(_address),
       size(0),
       isFixed(true),
@@ -88,8 +90,7 @@ public:
                bool _isLocal, bool _isGlobal, bool _isFixed,
                const llvm::Value *_allocSite,
                MemoryManager *_parent)
-    : refCount(0), 
-      id(counter++),
+    : id(counter++),
       address(_address),
       size(_size),
       name("unnamed"),
@@ -143,6 +144,25 @@ public:
       return ConstantExpr::alloc(0, Expr::Bool);
     }
   }
+
+  /// Compare this object with memory object b.
+  /// \param b memory object to compare with
+  /// \return <0 if this is smaller, 0 if both are equal, >0 if b is smaller
+  int compare(const MemoryObject &b) const {
+    // Short-cut with id
+    if (id == b.id)
+      return 0;
+    if (address != b.address)
+      return (address < b.address ? -1 : 1);
+
+    if (size != b.size)
+      return (size < b.size ? -1 : 1);
+
+    if (allocSite != b.allocSite)
+      return (allocSite < b.allocSite ? -1 : 1);
+
+    return 0;
+  }
 };
 
 class ObjectState {
@@ -155,7 +175,7 @@ private:
   /// @brief Required by klee::ref-managed objects
   class ReferenceCounter _refCount;
 
-  const MemoryObject *object;
+  ref<const MemoryObject> object;
 
   uint8_t *concreteStore;
 
@@ -188,7 +208,7 @@ public:
   ObjectState(const ObjectState &os);
   ~ObjectState();
 
-  const MemoryObject *getObject() const { return object; }
+  const MemoryObject *getObject() const { return object.get(); }
 
   void setReadOnly(bool ro) { readOnly = ro; }
 
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 3112495d..376ffe25 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -182,7 +182,7 @@ MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root,
     if (!hashed) {
       un_expr = evaluate(_solver,
                          metaSMT::logic::Array::store(
-                             getArrayForUpdate(root, un->next),
+                             getArrayForUpdate(root, un->next.get()),
                              construct(un->index, 0), construct(un->value, 0)));
       _arr_hash.hashUpdateNodeExpr(un, un_expr);
     }
@@ -680,10 +680,10 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
     assert(re && re->updates.root);
     *width_out = re->updates.root->getRange();
     // FixMe call method of Array
-    res = evaluate(_solver,
-                   metaSMT::logic::Array::select(
-                       getArrayForUpdate(re->updates.root, re->updates.head),
-                       construct(re->index, 0)));
+    res = evaluate(_solver, metaSMT::logic::Array::select(
+                                getArrayForUpdate(re->updates.root,
+                                                  re->updates.head.get()),
+                                construct(re->index, 0)));
     break;
   }