From 9cfa329a77d3dfec4746ca307c6da1b3e904cbfa Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Wed, 12 Sep 2018 14:58:11 +0000
Subject: Use `ref<>` for UpdateNode

Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.
---
 include/klee/Expr/Assignment.h         |  2 +-
 include/klee/Expr/Expr.h               | 40 +++++++++++++++++-----------------
 include/klee/Expr/ExprRangeEvaluator.h |  4 ++--
 3 files changed, 23 insertions(+), 23 deletions(-)

(limited to 'include')

diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
index ead459a9..395a3387 100644
--- a/include/klee/Expr/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -73,7 +73,7 @@ namespace klee {
       return ConstantExpr::alloc(it->second[index], array->getRange());
     } else {
       if (allowFreeValues) {
-        return ReadExpr::create(UpdateList(array, 0), 
+        return ReadExpr::create(UpdateList(array, ref<UpdateNode>(nullptr)),
                                 ConstantExpr::alloc(index, array->getDomain()));
       } else {
         return ConstantExpr::alloc(0, array->getRange());
diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index b979596a..374fc541 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -450,23 +450,24 @@ public:
 
 /// Class representing a byte update of an array.
 class UpdateNode {
-  friend class UpdateList;  
+  friend class UpdateList;
 
-  mutable unsigned refCount;
   // cache instead of recalc
   unsigned hashValue;
 
 public:
-  const UpdateNode *next;
+  const ref<UpdateNode> next;
   ref<Expr> index, value;
-  
+
+  /// @brief Required by klee::ref-managed objects
+  mutable class ReferenceCounter _refCount;
+
 private:
   /// size of this update sequence, including this update
   unsigned size;
   
 public:
-  UpdateNode(const UpdateNode *_next, 
-             const ref<Expr> &_index, 
+  UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
              const ref<Expr> &_value);
 
   unsigned getSize() const { return size; }
@@ -474,9 +475,8 @@ public:
   int compare(const UpdateNode &b) const;  
   unsigned hash() const { return hashValue; }
 
-private:
-  UpdateNode() : refCount(0) {}
-  ~UpdateNode();
+  UpdateNode() = delete;
+  ~UpdateNode() = default;
 
   unsigned computeHash();
 };
@@ -544,24 +544,24 @@ public:
   const Array *root;
   
   /// pointer to the most recent update node
-  const UpdateNode *head;
-  
+  ref<UpdateNode> head;
+
 public:
-  UpdateList(const Array *_root, const UpdateNode *_head);
-  UpdateList(const UpdateList &b);
-  ~UpdateList();
-  
-  UpdateList &operator=(const UpdateList &b);
+  UpdateList(const Array *_root, const ref<UpdateNode> &_head);
+  UpdateList(const UpdateList &b) = default;
+  ~UpdateList() = default;
+
+  UpdateList &operator=(const UpdateList &b) = default;
 
   /// size of this update list
-  unsigned getSize() const { return (head ? head->getSize() : 0); }
-  
+  unsigned getSize() const {
+    return (head.get() != nullptr ? head->getSize() : 0);
+  }
+
   void extend(const ref<Expr> &index, const ref<Expr> &value);
 
   int compare(const UpdateList &b) const;
   unsigned hash() const;
-private:
-  void tryFreeNodes();
 };
 
 /// Class representing a one byte read from an array. 
diff --git a/include/klee/Expr/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h
index 4d212764..540ccafd 100644
--- a/include/klee/Expr/ExprRangeEvaluator.h
+++ b/include/klee/Expr/ExprRangeEvaluator.h
@@ -73,7 +73,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
                                   T index) {
   T res;
 
-  for (const UpdateNode *un=ul.head; un; un=un->next) {
+  for (const UpdateNode *un = ul.head.get(); un; un = un->next.get()) {
     T ui = evaluate(un->index);
 
     if (ui.mustEqual(index)) {
@@ -85,7 +85,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
       } 
     }
   }
-  
+
   return res.set_union(getInitialReadRange(*ul.root, index));
 }
 
-- 
cgit 1.4.1