diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-04-03 16:01:36 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-02-19 12:05:22 +0000 |
commit | 288e3110e5df232ab471db705371d818605b4ae4 (patch) | |
tree | 0d36b9dc49581b9b335cc962f0896c13e2756993 /include | |
parent | b723470d00f80ad5620b27e81f2afa9efdd95135 (diff) | |
download | klee-288e3110e5df232ab471db705371d818605b4ae4.tar.gz |
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.
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Expr/Expr.h | 5 | ||||
-rw-r--r-- | include/klee/MergeHandler.h | 10 | ||||
-rw-r--r-- | include/klee/util/Ref.h | 72 |
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 */ |