Use `ref<>` for UpdateNode

Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.

19 files changed, 111 insertions, 256 deletions

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 12e74c77..e006d4d0 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -30,23 +30,23 @@ void AddressSpace::unbindObject(const MemoryObject *mo) {
 }
 
 const ObjectState *AddressSpace::findObject(const MemoryObject *mo) const {
-  const MemoryMap::value_type *res = objects.lookup(mo);
-  
-  return res ? res->second : 0;
+  const auto res = objects.lookup(mo);
+  return res ? res->second.get() : nullptr;
 }
 
 ObjectState *AddressSpace::getWriteable(const MemoryObject *mo,
                                         const ObjectState *os) {
   assert(!os->readOnly);
 
-  if (cowKey==os->copyOnWriteOwner) {
+  // If this address space owns they object, return it
+  if (cowKey == os->copyOnWriteOwner)
     return const_cast<ObjectState*>(os);
-  } else {
-    ObjectState *n = new ObjectState(*os);
-    n->copyOnWriteOwner = cowKey;
-    objects = objects.replace(std::make_pair(mo, n));
-    return n;    
-  }
+
+  // Add a copy of this object state that can be updated
+  ref<ObjectState> newObjectState(new ObjectState(*os));
+  newObjectState->copyOnWriteOwner = cowKey;
+  objects = objects.replace(std::make_pair(mo, newObjectState));
+  return newObjectState.get();
 }
 
 /// 
@@ -56,13 +56,14 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr,
   uint64_t address = addr->getZExtValue();
   MemoryObject hack(address);
 
-  if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) {
-    const MemoryObject *mo = res->first;
+  if (const auto res = objects.lookup_previous(&hack)) {
+    const auto &mo = res->first;
     // Check if the provided address is between start and end of the object
     // [mo->address, mo->address + mo->size) or the object is a 0-sized object.
     if ((mo->size==0 && address==mo->address) ||
         (address - mo->address < mo->size)) {
-      result = *res;
+      result.first = res->first;
+      result.second = res->second.get();
       return true;
     }
   }
@@ -88,12 +89,13 @@ bool AddressSpace::resolveOne(ExecutionState &state,
       return false;
     uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
-    const MemoryMap::value_type *res = objects.lookup_previous(&hack);
-    
+    const auto res = objects.lookup_previous(&hack);
+
     if (res) {
       const MemoryObject *mo = res->first;
       if (example - mo->address < mo->size) {
-        result = *res;
+        result.first = res->first;
+        result.second = res->second.get();
         success = true;
         return true;
       }
@@ -108,14 +110,15 @@ bool AddressSpace::resolveOne(ExecutionState &state,
     MemoryMap::iterator start = oi;
     while (oi!=begin) {
       --oi;
-      const MemoryObject *mo = oi->first;
-        
+      const auto &mo = oi->first;
+
       bool mayBeTrue;
       if (!solver->mayBeTrue(state, 
                              mo->getBoundsCheckPointer(address), mayBeTrue))
         return false;
       if (mayBeTrue) {
-        result = *oi;
+        result.first = oi->first;
+        result.second = oi->second.get();
         success = true;
         return true;
       } else {
@@ -131,7 +134,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
 
     // search forwards
     for (oi=start; oi!=end; ++oi) {
-      const MemoryObject *mo = oi->first;
+      const auto &mo = oi->first;
 
       bool mustBeTrue;
       if (!solver->mustBeTrue(state, 
@@ -148,7 +151,8 @@ bool AddressSpace::resolveOne(ExecutionState &state,
                                mayBeTrue))
           return false;
         if (mayBeTrue) {
-          result = *oi;
+          result.first = oi->first;
+          result.second = oi->second.get();
           success = true;
           return true;
         }
@@ -240,8 +244,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
       if (timeout && timeout < timer.delta())
         return true;
 
+      auto op = std::make_pair<>(mo, oi->second.get());
+
       int incomplete =
-          checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+          checkPointerInObject(state, solver, p, op, rl, maxResolutions);
       if (incomplete != 2)
         return incomplete ? true : false;
 
@@ -265,9 +271,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
         return true;
       if (mustBeTrue)
         break;
+      auto op = std::make_pair<>(mo, oi->second.get());
 
       int incomplete =
-          checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+          checkPointerInObject(state, solver, p, op, rl, maxResolutions);
       if (incomplete != 2)
         return incomplete ? true : false;
     }
@@ -288,7 +295,7 @@ void AddressSpace::copyOutConcretes() {
     const MemoryObject *mo = it->first;
 
     if (!mo->isUserSpecified) {
-      ObjectState *os = it->second;
+      const auto &os = it->second;
       auto address = reinterpret_cast<std::uint8_t*>(mo->address);
 
       if (!os->readOnly)
@@ -298,14 +305,13 @@ void AddressSpace::copyOutConcretes() {
 }
 
 bool AddressSpace::copyInConcretes() {
-  for (MemoryMap::iterator it = objects.begin(), ie = objects.end(); 
-       it != ie; ++it) {
-    const MemoryObject *mo = it->first;
+  for (auto &obj : objects) {
+    const MemoryObject *mo = obj.first;
 
     if (!mo->isUserSpecified) {
-      const ObjectState *os = it->second;
+      const auto &os = obj.second;
 
-      if (!copyInConcrete(mo, os, mo->address))
+      if (!copyInConcrete(mo, os.get(), mo->address))
         return false;
     }
   }
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 9e7e414a..10310a1e 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -10,8 +10,7 @@
 #ifndef KLEE_ADDRESSSPACE_H
 #define KLEE_ADDRESSSPACE_H
 
-#include "ObjectHolder.h"
-
+#include "Memory.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
 #include "klee/Internal/System/Time.h"
@@ -31,8 +30,9 @@ namespace klee {
   struct MemoryObjectLT {
     bool operator()(const MemoryObject *a, const MemoryObject *b) const;
   };
-  
-  typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
+
+  typedef ImmutableMap<const MemoryObject *, ref<ObjectState>, MemoryObjectLT>
+      MemoryMap;
 
   class AddressSpace {
   private:
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 60715b33..78aa8f67 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -166,9 +166,9 @@ llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
   MemoryMap::iterator it = mm.begin();
   MemoryMap::iterator ie = mm.end();
   if (it!=ie) {
-    os << "MO" << it->first->id << ":" << it->second;
+    os << "MO" << it->first->id << ":" << it->second.get();
     for (++it; it!=ie; ++it)
-      os << ", MO" << it->first->id << ":" << it->second;
+      os << ", MO" << it->first->id << ":" << it->second.get();
   }
   os << "}";
   return os;
@@ -265,7 +265,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
       }
       return false;
     }
-    if (ai->second != bi->second) {
+    if (ai->second.get() != bi->second.get()) {
       if (DebugLogStateMerge)
         llvm::errs() << "\t\tmutated: " << ai->first->id << "\n";
       mutated.insert(ai->first);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index c7e7a928..37e6646b 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -11,7 +11,6 @@
 
 #include "Context.h"
 #include "MemoryManager.h"
-#include "ObjectHolder.h"
 
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/Expr.h"
@@ -42,27 +41,6 @@ namespace {
 
 /***/
 
-ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) { 
-  if (os) ++os->refCount; 
-}
-
-ObjectHolder::ObjectHolder(ObjectState *_os) : os(_os) { 
-  if (os) ++os->refCount; 
-}
-
-ObjectHolder::~ObjectHolder() { 
-  if (os && --os->refCount==0) delete os; 
-}
-  
-ObjectHolder &ObjectHolder::operator=(const ObjectHolder &b) {
-  if (b.os) ++b.os->refCount;
-  if (os && --os->refCount==0) delete os;
-  os = b.os;
-  return *this;
-}
-
-/***/
-
 int MemoryObject::counter = 0;
 
 MemoryObject::~MemoryObject() {
@@ -96,7 +74,6 @@ void MemoryObject::getAllocInfo(std::string &result) const {
 
 ObjectState::ObjectState(const MemoryObject *mo)
   : copyOnWriteOwner(0),
-    refCount(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
     concreteMask(0),
@@ -118,7 +95,6 @@ ObjectState::ObjectState(const MemoryObject *mo)
 
 ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
   : copyOnWriteOwner(0),
-    refCount(0),
     object(mo),
     concreteStore(new uint8_t[mo->size]),
     concreteMask(0),
@@ -134,7 +110,6 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
 
 ObjectState::ObjectState(const ObjectState &os) 
   : copyOnWriteOwner(0),
-    refCount(0),
     object(os.object),
     concreteStore(new uint8_t[os.size]),
     concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
@@ -188,10 +163,10 @@ const UpdateList &ObjectState::getUpdates() const {
     // FIXME: We should be able to do this more efficiently, we just need to be
     // careful to get the interaction with the cache right. In particular we
     // should avoid creating UpdateNode instances we never use.
-    unsigned NumWrites = updates.head ? updates.head->getSize() : 0;
+    unsigned NumWrites = updates.head.isNull() ? 0 : updates.head->getSize();
     std::vector< std::pair< ref<Expr>, ref<Expr> > > Writes(NumWrites);
-    const UpdateNode *un = updates.head;
-    for (unsigned i = NumWrites; i != 0; un = un->next) {
+    const auto *un = updates.head.get();
+    for (unsigned i = NumWrites; i != 0; un = un->next.get()) {
       --i;
       Writes[i] = std::make_pair(un->index, un->value);
     }
@@ -257,7 +232,7 @@ void ObjectState::makeConcrete() {
 }
 
 void ObjectState::makeSymbolic() {
-  assert(!updates.head &&
+  assert(updates.head.isNull() &&
          "XXX makeSymbolic of objects with symbolic values is unsupported");
 
   // XXX simplify this, can just delete various arrays I guess
@@ -612,7 +587,7 @@ void ObjectState::print() const {
   }
 
   llvm::errs() << "\tUpdates:\n";
-  for (const UpdateNode *un=updates.head; un; un=un->next) {
+  for (const auto *un = updates.head.get(); un; un = un->next.get()) {
     llvm::errs() << "\t\t[" << un->index << "] = " << un->value << "\n";
   }
 }
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index dfda433c..e4260c55 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -148,10 +148,12 @@ public:
 class ObjectState {
 private:
   friend class AddressSpace;
+  friend class ref<ObjectState>;
+
   unsigned copyOnWriteOwner; // exclusively for AddressSpace
 
-  friend class ObjectHolder;
-  unsigned refCount;
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
 
   const MemoryObject *object;
 
diff --git a/lib/Core/ObjectHolder.h b/lib/Core/ObjectHolder.h
deleted file mode 100644
index cd6c6281..00000000
--- a/lib/Core/ObjectHolder.h
+++ /dev/null
@@ -1,32 +0,0 @@
-//===-- ObjectHolder.h ------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_OBJECTHOLDER_H
-#define KLEE_OBJECTHOLDER_H
-
-namespace klee {
-  class ObjectState;
-
-  class ObjectHolder {
-    ObjectState *os;
-    
-  public:
-    ObjectHolder() : os(0) {}
-    ObjectHolder(ObjectState *_os);
-    ObjectHolder(const ObjectHolder &b);
-    ~ObjectHolder(); 
-    
-    ObjectHolder &operator=(const ObjectHolder &b);
-
-    operator class ObjectState *() { return os; }
-    operator class ObjectState *() const { return (ObjectState*) os; }
-  };
-}
-
-#endif /* KLEE_OBJECTHOLDER_H */
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 60f2ca6e..d80cc3bc 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -284,7 +284,8 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
       // reverse the list
       std::vector<const UpdateNode *> us;
       us.reserve(read->updates.getSize());
-      for (const UpdateNode *un = read->updates.head; un; un = un->next)
+      for (const UpdateNode *un = read->updates.head.get(); un;
+           un = un->next.get())
         us.push_back(un);
 
       auto arrayConstValues = read->updates.root->constantValues;
@@ -366,7 +367,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
       // reverse the list
       std::vector<const UpdateNode *> us;
       us.reserve(read->updates.getSize());
-      for (const UpdateNode *un = read->updates.head; un; un = un->next)
+      for (const UpdateNode *un = read->updates.head.get(); un; un = un->next.get())
         us.push_back(un);
 
       for (auto it = us.rbegin(); it != us.rend(); it++) {
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index cada7867..986360f7 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -63,7 +63,7 @@ ConstantArrayExprVisitor::visitConcat(const ConcatExpr &ce) {
     // that is read at a symbolic index
     if (base->updates.root->isConstantArray() &&
         !isa<ConstantExpr>(base->index)) {
-      for (const UpdateNode *un = base->updates.head; un; un = un->next) {
+      for (const auto *un = base->updates.head.get(); un; un = un->next.get()) {
         if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) {
           incompatible = true;
           return Action::skipChildren();
@@ -97,7 +97,7 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
   // It is an interesting ReadExpr if it contains a concrete array
   // that is read at a symbolic index
   if (re.updates.root->isConstantArray() && !isa<ConstantExpr>(re.index)) {
-    for (const UpdateNode *un = re.updates.head; un; un = un->next) {
+    for (const auto *un = re.updates.head.get(); un; un = un->next.get()) {
       if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) {
         incompatible = true;
         return Action::skipChildren();
@@ -132,7 +132,7 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
 
 ExprVisitor::Action
 IndexCompatibilityExprVisitor::visitRead(const ReadExpr &re) {
-  if (re.updates.head) {
+  if (!re.updates.head.isNull()) {
     compatible = false;
     return Action::skipChildren();
   } else if (re.updates.root->isConstantArray() &&
@@ -198,13 +198,13 @@ ExprVisitor::Action ArrayReadExprVisitor::inspectRead(ref<Expr> hash,
   // pre(*): index is symbolic
   if (!isa<ConstantExpr>(re.index)) {
     if (readInfo.find(&re) == readInfo.end()) {
-      if (re.updates.root->isSymbolicArray() && !re.updates.head) {
+      if (re.updates.root->isSymbolicArray() && re.updates.head.isNull()) {
         return Action::doChildren();
       }
-      if (re.updates.head) {
+      if (!re.updates.head.isNull()) {
         // Check preconditions on UpdateList nodes
         bool hasConcreteValues = false;
-        for (const UpdateNode *un = re.updates.head; un; un = un->next) {
+        for (const auto *un = re.updates.head.get(); un; un = un->next.get()) {
           // Symbolic case - \inv(update): index is concrete
           if (!isa<ConstantExpr>(un->index)) {
             incompatible = true;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 6b8dc95f..b798bc37 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -537,10 +537,9 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
   // least recent to find a potential written value for a concrete index;
   // stop if an update with symbolic has been found as we don't know which
   // array element has been updated
-  const UpdateNode *un = ul.head;
+  auto un = ul.head.get();
   bool updateListHasSymbolicWrites = false;
-  for (; un; un=un->next) {
-    // Check if we have an equivalent concrete index
+  for (; un; un = un->next.get()) {
     ref<Expr> cond = EqExpr::create(index, un->index);
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
       if (CE->isTrue())
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index e1cfa2d2..f8f57d35 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -326,8 +326,8 @@ namespace {
     virtual ref<Expr> Read(const UpdateList &Updates,
                            const ref<Expr> &Index) {
       // Roll back through writes when possible.
-      const UpdateNode *UN = Updates.head;
-      while (UN && Eq(Index, UN->index)->isFalse())
+      auto UN = Updates.head;
+      while (!UN.isNull() && Eq(Index, UN->index)->isFalse())
         UN = UN->next;
 
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Index))
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index f03d7669..afd5d641 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -13,7 +13,7 @@ using namespace klee;
 
 ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
                                             unsigned index) {
-  for (const UpdateNode *un=ul.head; un; un=un->next) {
+  for (auto un = ul.head; !un.isNull(); un = un->next) {
     ref<Expr> ui = visit(un->index);
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 2ccd7262..9d34e356 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -92,7 +92,8 @@ private:
     if (isVerySimple(e)) {
       return true;
     } else if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
-      return isVerySimple(re->index) && isVerySimpleUpdate(re->updates.head);
+      return isVerySimple(re->index) &&
+             isVerySimpleUpdate(re->updates.head.get());
     } else {
       Expr *ep = e.get();
       for (unsigned i=0; i<ep->getNumKids(); i++)
@@ -113,7 +114,7 @@ private:
     // FIXME: This needs to be non-recursive.
     if (un) {
       if (couldPrintUpdates.insert(un).second) {
-        scanUpdate(un->next);
+        scanUpdate(un->next.get());
         scan1(un->index);
         scan1(un->value);
       } else {
@@ -130,7 +131,7 @@ private:
           scan1(ep->getKid(i));
         if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
           usedArrays.insert(re->updates.root);
-          scanUpdate(re->updates.head);
+          scanUpdate(re->updates.head.get());
         }
       } else {
         shouldPrint.insert(e);
@@ -139,10 +140,10 @@ private:
   }
 
   void printUpdateList(const UpdateList &updates, PrintContext &PC) {
-    const UpdateNode *head = updates.head;
+    auto head = updates.head;
 
     // Special case empty list.
-    if (!head) {
+    if (head.isNull()) {
       // FIXME: We need to do something (assert, mangle, etc.) so that printing
       // distinct arrays with the same name doesn't fail.
       PC << updates.root->name;
@@ -153,22 +154,22 @@ private:
     bool openedList = false, nextShouldBreak = false;
     unsigned outerIndent = PC.pos;
     unsigned middleIndent = 0;
-    for (const UpdateNode *un = head; un; un = un->next) {      
+    for (auto un = head; !un.isNull(); un = un->next) {
       // We are done if we hit the cache.
-      std::map<const UpdateNode*, unsigned>::iterator it = 
-        updateBindings.find(un);
+      std::map<const UpdateNode *, unsigned>::iterator it =
+          updateBindings.find(un.get());
       if (it!=updateBindings.end()) {
         if (openedList)
           PC << "] @ ";
         PC << "U" << it->second;
         return;
-      } else if (!hasScan || shouldPrintUpdates.count(un)) {
+      } else if (!hasScan || shouldPrintUpdates.count(un.get())) {
         if (openedList)
           PC << "] @";
         if (un != head)
           PC.breakLine(outerIndent);
-        PC << "U" << updateCounter << ":"; 
-        updateBindings.insert(std::make_pair(un, updateCounter++));
+        PC << "U" << updateCounter << ":";
+        updateBindings.insert(std::make_pair(un.get(), updateCounter++));
         openedList = nextShouldBreak = false;
      }
     
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index b83a6af4..069eb32f 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -279,7 +279,7 @@ void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr> &e) {
   printSeperator();
 
   // print array with updates recursively
-  printUpdatesAndArray(e->updates.head, e->updates.root);
+  printUpdatesAndArray(e->updates.head.get(), e->updates.root);
 
   // print index
   printSeperator();
@@ -483,7 +483,7 @@ void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode *un,
     printSeperator();
 
     // recurse to get the array or update that this store operations applies to
-    printUpdatesAndArray(un->next, root);
+    printUpdatesAndArray(un->next.get(), root);
 
     printSeperator();
 
@@ -713,7 +713,7 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
           haveConstantArray = true;
 
         // scan the update list
-        scanUpdates(re->updates.head);
+        scanUpdates(re->updates.head.get());
       }
     }
 
@@ -824,7 +824,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
   while (un != NULL) {
     scan(un->index);
     scan(un->value);
-    un = un->next;
+    un = un->next.get();
   }
 }
 
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 911366f3..3819e3a2 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -49,8 +49,9 @@ void klee::findReads(ref<Expr> e,
         // especially since we memoize all the expr results anyway. So
         // we take a simple approach of memoizing the results for the
         // head, which often will be shared among multiple nodes.
-        if (updates.insert(re->updates.head).second) {
-          for (const UpdateNode *un=re->updates.head; un; un=un->next) {
+        if (updates.insert(re->updates.head.get()).second) {
+          for (const auto *un = re->updates.head.get(); un;
+               un = un->next.get()) {
             if (!isa<ConstantExpr>(un->index) &&
                 visited.insert(un->index).second)
               stack.push_back(un->index);
@@ -82,7 +83,7 @@ protected:
     const UpdateList &ul = re.updates;
 
     // XXX should we memo better than what ExprVisitor is doing for us?
-    for (const UpdateNode *un=ul.head; un; un=un->next) {
+    for (const auto *un = ul.head.get(); un; un = un->next.get()) {
       visit(un->index);
       visit(un->value);
     }
@@ -106,7 +107,7 @@ ExprVisitor::Action ConstantArrayFinder::visitRead(const ReadExpr &re) {
   const UpdateList &ul = re.updates;
 
   // FIXME should we memo better than what ExprVisitor is doing for us?
-  for (const UpdateNode *un = ul.head; un; un = un->next) {
+  for (const auto *un = ul.head.get(); un; un = un->next.get()) {
     visit(un->index);
     visit(un->value);
   }
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;
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 3e1162fd..722f624f 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -804,8 +804,8 @@ public:
       const Array *array = re->updates.root;
       CexObjectData &cod = getObjectData(array);
       CexValueData index = evalRangeForExpr(re->index);
-        
-      for (const UpdateNode *un = re->updates.head; un; un = un->next) {
+
+      for (const auto *un = re->updates.head.get(); un; un = un->next.get()) {
         CexValueData ui = evalRangeForExpr(un->index);
 
         // If these indices can't alias, continue propogation
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 7beb1a7c..cd59c741 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -120,8 +120,7 @@ public:
       const Array *array = re->updates.root;
       
       // Reads of a constant array don't alias.
-      if (re->updates.root->isConstantArray() &&
-          !re->updates.head)
+      if (re->updates.root->isConstantArray() && re->updates.head.isNull())
         continue;
 
       if (!wholeObjects.count(array)) {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ef6697ef..5857e6f0 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -480,12 +480,11 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
       bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
       
       if (!hashed) {
-	un_expr = vc_writeExpr(vc,
-                               getArrayForUpdate(root, un->next),
-                               construct(un->index, 0),
-                               construct(un->value, 0));
-	
-	_arr_hash.hashUpdateNodeExpr(un, un_expr);
+        un_expr =
+            vc_writeExpr(vc, getArrayForUpdate(root, un->next.get()),
+                         construct(un->index, 0), construct(un->value, 0));
+
+        _arr_hash.hashUpdateNodeExpr(un, un_expr);
       }
       
       return un_expr;
@@ -560,9 +559,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ReadExpr *re = cast<ReadExpr>(e);
     assert(re && re->updates.root);
     *width_out = re->updates.root->getRange();
-    return vc_readExpr(vc,
-                       getArrayForUpdate(re->updates.root, re->updates.head),
-                       construct(re->index, 0));
+    return vc_readExpr(
+        vc, getArrayForUpdate(re->updates.root, re->updates.head.get()),
+        construct(re->index, 0));
   }
     
   case Expr::Select: {
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 43440fa7..29f55b31 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -439,7 +439,7 @@ Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root,
     bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
 
     if (!hashed) {
-      un_expr = writeExpr(getArrayForUpdate(root, un->next),
+      un_expr = writeExpr(getArrayForUpdate(root, un->next.get()),
                           construct(un->index, 0), construct(un->value, 0));
 
       _arr_hash.hashUpdateNodeExpr(un, un_expr);
@@ -522,7 +522,7 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) {
     ReadExpr *re = cast<ReadExpr>(e);
     assert(re && re->updates.root);
     *width_out = re->updates.root->getRange();
-    return readExpr(getArrayForUpdate(re->updates.root, re->updates.head),
+    return readExpr(getArrayForUpdate(re->updates.root, re->updates.head.get()),
                     construct(re->index, 0));
   }