Use `ref<>` for UpdateNode

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

9 files changed, 47 insertions, 141 deletions

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;
 }