1 files changed, 12 insertions, 108 deletions

diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 7264ca89..4734f592 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -13,13 +13,11 @@
 
 using namespace klee;
 
-UpdateNode::UpdateNode(const UpdateNode *_next, 
-                       const ref<Expr> &_index, 
-                       const ref<Expr> &_value) 
-  : refCount(0),    
-    next(_next),
-    index(_index),
-    value(_value) {
+///
+
+UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
+                       const ref<Expr> &_value)
+    : next(_next), index(_index), value(_value) {
   // FIXME: What we need to check here instead is that _value is of the same width 
   // as the range of the array that the update node is part of.
   /*
@@ -27,23 +25,11 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
          "Update value should be 8-bit wide.");
   */
   computeHash();
-  if (next) {
-    ++next->refCount;
-    size = 1 + next->size;
-  }
-  else size = 1;
+  size = next.isNull() ? 1 : 1 + next->size;
 }
 
 extern "C" void vc_DeleteExpr(void*);
 
-// This is deliberately empty to avoid recursively deleting UpdateNodes
-// (i.e. ``if (--next->refCount==0) delete next;``).
-// UpdateList manages the correct destruction of a chain UpdateNodes
-// non-recursively.
-UpdateNode::~UpdateNode() {
-    assert(refCount == 0 && "Deleted UpdateNode when a reference is still held");
-}
-
 int UpdateNode::compare(const UpdateNode &b) const {
   if (int i = index.compare(b.index)) 
     return i;
@@ -52,95 +38,15 @@ int UpdateNode::compare(const UpdateNode &b) const {
 
 unsigned UpdateNode::computeHash() {
   hashValue = index->hash() ^ value->hash();
-  if (next)
+  if (!next.isNull())
     hashValue ^= next->hash();
   return hashValue;
 }
 
 ///
 
-UpdateList::UpdateList(const Array *_root, const UpdateNode *_head)
-  : root(_root),
-    head(_head) {
-  if (head) ++head->refCount;
-}
-
-UpdateList::UpdateList(const UpdateList &b)
-  : root(b.root),
-    head(b.head) {
-  if (head) ++head->refCount;
-}
-
-UpdateList::~UpdateList() {
-    tryFreeNodes();
-}
-
-void UpdateList::tryFreeNodes() {
-  // We need to be careful and avoid having the UpdateNodes recursively deleting
-  // themselves. This is done in cooperation with the private dtor of UpdateNode
-  // which does nothing.
-  //
-  // This method will free UpdateNodes that only this instance has references
-  // to, i.e. it will delete a continguous chain of UpdateNodes that all have
-  // a ``refCount`` of 1 starting at the head.
-  //
-  // In the following examples the Head0 is the head of this UpdateList instance
-  // and Head1 is the head of some other instance of UpdateList.
-  //
-  // [x] represents an UpdateNode where the reference count for that node is x.
-  //
-  // Example: Simple chain.
-  //
-  // [1] -> [1] -> [1] -> nullptr
-  //  ^Head0
-  //
-  // Result: The entire chain is freed
-  //
-  // nullptr
-  // ^Head0
-  //
-  // Example: A chain where two UpdateLists share some nodes
-  //
-  // [1] -> [1] -> [2] -> [1] -> nullptr
-  //  ^Head0        ^Head1
-  //
-  // Result: Part of the chain is freed and the UpdateList with head Head1
-  //         is now the exclusive owner of the UpdateNodes.
-  //
-  // nullptr       [1] -> [1] -> nullptr
-  //  ^Head0        ^Head1
-  //
-  // Example: A chain where two UpdateLists point at the same head
-  //
-  // [2] -> [1] -> [1] -> [1] -> nullptr
-  //  ^Head0
-  //   Head1
-  //
-  // Result: No UpdateNodes are freed but now the UpdateList with head Head1
-  //         is now the exclusive owner of the UpdateNodes.
-  //
-  // [1] -> [1] -> [1] -> [1] -> nullptr
-  //  ^Head1
-  //
-  //  nullptr
-  //  ^Head0
-  //
-  while (head && --head->refCount==0) {
-    const UpdateNode *n = head->next;
-    delete head;
-    head = n;
-  }
-}
-
-UpdateList &UpdateList::operator=(const UpdateList &b) {
-  if (b.head) ++b.head->refCount;
-  // Drop reference to the current head and free a chain of nodes
-  // if we are the only UpdateList referencing them
-  tryFreeNodes();
-  root = b.root;
-  head = b.head;
-  return *this;
-}
+UpdateList::UpdateList(const Array *_root, const ref<UpdateNode> &_head)
+    : root(_root), head(_head) {}
 
 void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
   
@@ -149,9 +55,7 @@ void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
     assert(root->getRange() == value->getWidth());
   }
 
-  if (head) --head->refCount;
   head = new UpdateNode(head, index, value);
-  ++head->refCount;
 }
 
 int UpdateList::compare(const UpdateList &b) const {
@@ -167,8 +71,8 @@ int UpdateList::compare(const UpdateList &b) const {
   else if (getSize() > b.getSize()) return 1;    
 
   // XXX build comparison into update, make fast
-  const UpdateNode *an=head, *bn=b.head;
-  for (; an && bn; an=an->next,bn=bn->next) {
+  const auto *an = head.get(), *bn = b.head.get();
+  for (; an && bn; an = an->next.get(), bn = bn->next.get()) {
     if (an==bn) { // exploit shared list structure
       return 0;
     } else {
@@ -184,7 +88,7 @@ unsigned UpdateList::hash() const {
   unsigned res = 0;
   for (unsigned i = 0, e = root->name.size(); i != e; ++i)
     res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
-  if (head)
+  if (head.get())
     res ^= head->hash();
   return res;
 }