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.

3 files changed, 73 insertions, 14 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 */