Add `ReferenceCounter` struct utilized by ref<>

Using KLEE's `ref<>` shared ptr requires the referenced object
to contain a reference counter to be added and initialised to 0
as part of the constructor.

To support better reuse of the `ref<>` ptr add a `ReferenceCounter`
struct.

Just adding this struct to a new class/struct as member enables
reference counting with `ref<>` - no additional counter management
needed.

5 files changed, 111 insertions, 41 deletions

diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index d4e4f7fa..b979596a 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -174,7 +174,8 @@ public:
     CmpKindLast=Sge
   };
 
-  unsigned refCount;
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
 
 protected:  
   unsigned hashValue;
@@ -204,7 +205,7 @@ protected:
   virtual int compareContents(const Expr &b) const = 0;
 
 public:
-  Expr() : refCount(0) { Expr::count++; }
+  Expr() { Expr::count++; }
   virtual ~Expr() { Expr::count--; } 
 
   virtual Kind getKind() const = 0;
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h
index d189e46f..48b67467 100644
--- a/include/klee/MergeHandler.h
+++ b/include/klee/MergeHandler.h
@@ -69,10 +69,11 @@
 #ifndef KLEE_MERGEHANDLER_H
 #define KLEE_MERGEHANDLER_H
 
-#include <vector>
+#include "klee/util/Ref.h"
+#include "llvm/Support/CommandLine.h"
 #include <map>
 #include <stdint.h>
-#include "llvm/Support/CommandLine.h"
+#include <vector>
 
 namespace llvm {
 class Instruction;
@@ -143,9 +144,8 @@ public:
   // klee_close_merge
   double getMean();
 
-  /// @brief Required by klee::ref objects
-  unsigned refCount;
-
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
 
   MergeHandler(Executor *_executor, ExecutionState *es);
   ~MergeHandler();
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index 44f3f49e..f6d66d16 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -7,6 +7,25 @@
 //
 //===----------------------------------------------------------------------===//
 
+/**
+ * @file Ref.h
+ * @brief Implements smart-pointer ref<> used by KLEE.
+ *
+ * ## Basic usage:
+ *
+ * Add the following to your struct/class to enable ref<> pointer usage
+ * @code{.cpp}
+ *
+ * struct MyStruct{
+ *   ...
+ *   /// @brief Required by klee::ref-managed objects
+ *   class ReferenceCounter _refCount;
+ *   ...
+ * }
+ * @endcode
+ *
+ */
+
 #ifndef KLEE_REF_H
 #define KLEE_REF_H
 
@@ -22,27 +41,66 @@ using llvm::dyn_cast_or_null;
 
 namespace llvm {
   class raw_ostream;
-}
+} // namespace llvm
 
 namespace klee {
 
 template<class T>
+class ref;
+
+/// Reference counter to be used as part of a ref-managed struct or class
+class ReferenceCounter {
+  template<class T>
+  friend class ref;
+
+  /// Count how often the object has been referenced.
+  unsigned refCount = 0;
+
+public:
+  ReferenceCounter() = default;
+  ~ReferenceCounter() = default;
+
+  // Explicitly initialise reference counter with 0 again
+  // As this object is part of another object, the copy-constructor
+  // might be invoked as part of the other one.
+  ReferenceCounter(const ReferenceCounter& ) {}
+
+  /// Returns the number of parallel references of this objects
+  /// \return number of references on this object
+  unsigned getCount() {return refCount;}
+
+  // Copy assignment operator
+  ReferenceCounter &operator=(const ReferenceCounter &a) {
+    if (this == &a)
+      return *this;
+    // The new copy won't be referenced
+    refCount = 0;
+    return *this;
+  }
+
+  // Do not allow move operations for the reference counter
+  // as otherwise, references become incorrect.
+  ReferenceCounter(ReferenceCounter &&r) noexcept = delete;
+  ReferenceCounter &operator=(ReferenceCounter &&other) noexcept = delete;
+};
+
+template<class T>
 class ref {
   T *ptr;
 
 public:
   // default constructor: create a NULL reference
-  ref() : ptr(0) { }
+  ref() : ptr(nullptr) {}
   ~ref () { dec (); }
 
 private:
   void inc() const {
     if (ptr)
-      ++ptr->refCount;
+      ++ptr->_refCount.refCount;
   }
 
   void dec() const {
-    if (ptr && --ptr->refCount == 0)
+    if (ptr && --ptr->_refCount.refCount == 0)
       delete ptr;
   }
 
@@ -121,7 +179,7 @@ public:
     return ptr;
   }
 
-  bool isNull() const { return ptr == 0; }
+  bool isNull() const { return ptr == nullptr; }
 
   // assumes non-null arguments
   int compare(const ref &rhs) const {
@@ -158,7 +216,7 @@ namespace llvm {
   // isNull semantics, which doesn't seem like a good idea.
 template<typename T>
 struct simplify_type<const ::klee::ref<T> > {
-  typedef T* SimpleType;
+  using SimpleType = T *;
   static SimpleType getSimplifiedValue(const ::klee::ref<T> &Ref) {
     return Ref.get();
   }
@@ -167,6 +225,6 @@ struct simplify_type<const ::klee::ref<T> > {
 template<typename T>
 struct simplify_type< ::klee::ref<T> >
   : public simplify_type<const ::klee::ref<T> > {};
-}
+}  // namespace llvm
 
 #endif /* KLEE_REF_H */
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
index 5764b5a1..7a683e84 100644
--- a/lib/Core/MergeHandler.cpp
+++ b/lib/Core/MergeHandler.cpp
@@ -135,8 +135,8 @@ bool MergeHandler::hasMergedStates() {
 
 MergeHandler::MergeHandler(Executor *_executor, ExecutionState *es)
     : executor(_executor), openInstruction(es->steppedInstructions),
-      closedMean(0), closedStateCount(0), refCount(0) {
-  executor->mergingSearcher->mergeGroups.push_back(this);
+      closedMean(0), closedStateCount(0) {
+    executor->mergingSearcher->mergeGroups.push_back(this);
   addOpenState(es);
 }
 
diff --git a/unittests/Ref/RefTest.cpp b/unittests/Ref/RefTest.cpp
index 7d587f69..3548da85 100644
--- a/unittests/Ref/RefTest.cpp
+++ b/unittests/Ref/RefTest.cpp
@@ -8,40 +8,35 @@
 //===----------------------------------------------------------------------===//
 
 /* Regression test for a bug caused by assigning a ref to itself.
-   More details at http://keeda.stanford.edu/pipermail/klee-commits/2012-February/000904.html */
+   More details at
+   http://keeda.stanford.edu/pipermail/klee-commits/2012-February/000904.html */
 
+#include "klee/util/Ref.h"
 #include "gtest/gtest.h"
 #include <iostream>
-#include "klee/util/Ref.h"
 using klee::ref;
 
 int finished = 0;
 int finished_counter = 0;
 
-struct Expr
-{
-  int refCount;
-  Expr() : refCount(0) { 
-    //std::cout << "Expr(" << this << ") created\n"; 
-  }
-  ~Expr() { 
-    //std::cout << "Expr(" << this << ") destroyed\n"; 
+struct Expr {
+  /// @brief Required by klee::ref-managed objects
+  class klee::ReferenceCounter _refCount;
+  Expr() = default;
+
+  Expr(const Expr &) = delete;
+  Expr &operator=(const Expr &) = delete;
+
+  ~Expr() {
+    // std::cout << "Expr(" << this << ") destroyed\n";
     EXPECT_EQ(finished, 1);
+    finished_counter++;
   }
 };
 
-TEST(RefTest, SelfAssign) 
-{
-  struct Expr *r_e = new Expr();
-  ref<Expr> r(r_e);
-  EXPECT_EQ(r_e->refCount, 1);
-  r = r;
-  EXPECT_EQ(r_e->refCount, 1);
-  finished = 1;
-}
 struct SelfRefExpr {
   /// @brief Required by klee::ref-managed objects
-  struct klee::ReferenceCounter __refCount;
+  class klee::ReferenceCounter _refCount;
   ref<SelfRefExpr> next_;
 
   explicit SelfRefExpr(ref<SelfRefExpr> next) : next_(next) {}
@@ -50,21 +45,37 @@ struct SelfRefExpr {
 
   ~SelfRefExpr() { finished_counter++; }
 };
+
+TEST(RefTest, SelfAssign) {
+  finished = 0;
+  finished_counter = 0;
+  {
+
+    struct Expr *r_e = new Expr();
+    ref<Expr> r(r_e);
+    EXPECT_EQ(r_e->_refCount.getCount(), 1u);
+    r = r;
+    EXPECT_EQ(r_e->_refCount.getCount(), 1u);
+    finished = 1;
+  }
+  EXPECT_EQ(1, finished_counter);
+}
+
 TEST(RefTest, SelfRef) {
   struct SelfRefExpr *e_1 = new SelfRefExpr(nullptr);
   ref<SelfRefExpr> r_e_1(e_1);
-  EXPECT_EQ(1u, r_e_1->__refCount.refCount);
+  EXPECT_EQ(1u, r_e_1->_refCount.getCount());
   ref<SelfRefExpr> r_root = r_e_1;
-  EXPECT_EQ(2u, r_e_1->__refCount.refCount);
+  EXPECT_EQ(2u, r_e_1->_refCount.getCount());
 
   {
     ref<SelfRefExpr> r2(new SelfRefExpr(r_e_1));
-    EXPECT_EQ(3u, r_e_1->__refCount.refCount);
+    EXPECT_EQ(3u, r_e_1->_refCount.getCount());
 
     r_root = r2;
-    EXPECT_EQ(2u, r_e_1->__refCount.refCount);
+    EXPECT_EQ(2u, r_e_1->_refCount.getCount());
   }
 
   r_root = r_root->next_;
-  EXPECT_EQ(2u, r_e_1->__refCount.refCount);
+  EXPECT_EQ(2u, r_e_1->_refCount.getCount());
 }
\ No newline at end of file