2 files changed, 129 insertions, 0 deletions

diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index f6d66d16..4dafdf8e 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -123,6 +123,14 @@ public:
     inc();
   }
 
+  // normal move constructor: invoke the move assignment operator
+  ref(ref<T> &&r) noexcept : ptr(nullptr) { *this = std::move(r); }
+
+  // conversion move constructors: invoke the move assignment operator
+  template <class U> ref(ref<U> &&r) noexcept : ptr(nullptr) {
+    *this = std::move(r);
+  }
+
   // pointer operations
   T *get () const {
     return ptr;
@@ -171,6 +179,35 @@ public:
     return *this;
   }
 
+  // Move assignment operator
+  ref<T> &operator=(ref<T> &&r) noexcept {
+    if (this == &r)
+      return *this;
+    dec();
+    ptr = r.ptr;
+    r.ptr = nullptr;
+    return *this;
+  }
+
+  // Move assignment operator
+  template <class U> ref<T> &operator=(ref<U> &&r) noexcept {
+    if (static_cast<void *>(this) == static_cast<void *>(&r))
+      return *this;
+
+    // Do not swap as the types might be not compatible
+    // Decrement local counter to not hold reference anymore
+    dec();
+
+    // Assign to this ref
+    ptr = cast_or_null<T>(r.ptr);
+
+    // Invalidate old ptr
+    r.ptr = nullptr;
+
+    // Return this pointer
+    return *this;
+  }
+
   T& operator*() const {
     return *ptr;
   }
diff --git a/unittests/Ref/RefTest.cpp b/unittests/Ref/RefTest.cpp
index 3548da85..066ecc58 100644
--- a/unittests/Ref/RefTest.cpp
+++ b/unittests/Ref/RefTest.cpp
@@ -46,6 +46,32 @@ struct SelfRefExpr {
   ~SelfRefExpr() { finished_counter++; }
 };
 
+struct ParentExpr {
+  /// @brief Required by klee::ref-managed objects
+  class klee::ReferenceCounter _refCount;
+
+  enum ExprKind {
+    EK_Parent,
+    EK_Child,
+  };
+
+  const ExprKind Kind;
+  ExprKind getKind() const { return Kind; }
+
+  ParentExpr(ExprKind K) : Kind(K) {}
+
+  virtual ~ParentExpr() {
+    EXPECT_EQ(finished, 1);
+    finished_counter++;
+  }
+};
+
+struct ChildExpr : public ParentExpr {
+  ChildExpr() : ParentExpr(EK_Child) {}
+
+  static bool classof(const ParentExpr *S) { return S->getKind() == EK_Child; }
+};
+
 TEST(RefTest, SelfAssign) {
   finished = 0;
   finished_counter = 0;
@@ -61,6 +87,72 @@ TEST(RefTest, SelfAssign) {
   EXPECT_EQ(1, finished_counter);
 }
 
+TEST(RefTest, SelfMove) {
+  finished = 0;
+  finished_counter = 0;
+  {
+    struct Expr *r_e = new Expr();
+    ref<Expr> r(r_e);
+
+    // Check self move
+    r = std::move(r);
+    finished = 1;
+  }
+  EXPECT_EQ(1, finished_counter);
+}
+
+TEST(RefTest, MoveAssignment) {
+  finished = 0;
+  finished_counter = 0;
+  {
+    struct Expr *r_e = new Expr();
+    ref<Expr> r(r_e);
+
+    struct Expr *q_e = new Expr();
+    ref<Expr> q(q_e);
+
+    finished = 1;
+
+    // Move the object
+    q = std::move(r);
+
+    // Re-assign new object
+    r = new Expr();
+  }
+  EXPECT_EQ(3, finished_counter);
+}
+
+TEST(RefTest, MoveCastingAssignment) {
+  finished = 0;
+  finished_counter = 0;
+  {
+    ref<ParentExpr> r(new ChildExpr());
+
+    struct ChildExpr *child = new ChildExpr();
+    ref<ChildExpr> ce(child);
+
+    finished = 1;
+
+    // Move the object
+    r = std::move(child);
+  }
+  EXPECT_EQ(2, finished_counter);
+}
+
+TEST(RefTest, MoveConstructor) {
+  finished = 0;
+  finished_counter = 0;
+  {
+    struct Expr *r_e = new Expr();
+    ref<Expr> r(r_e);
+
+    ref<Expr> q(std::move(r_e));
+
+    finished = 1;
+  }
+  EXPECT_EQ(1, finished_counter);
+}
+
 TEST(RefTest, SelfRef) {
   struct SelfRefExpr *e_1 = new SelfRefExpr(nullptr);
   ref<SelfRefExpr> r_e_1(e_1);