Improve IndependentConstraintSetUnion

include/klee/ADT/DisjointSetUnion.h

@@ -1,14 +1,27 @@
 #ifndef KLEE_DISJOINEDSETUNION_H
 #define KLEE_DISJOINEDSETUNION_H
+
+#include "klee/ADT/Either.h"
 #include "klee/ADT/PersistentMap.h"
 #include "klee/ADT/PersistentSet.h"
 #include "klee/ADT/Ref.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/Symcrete.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
+
+#include <map>
 #include <set>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
 
 namespace klee {
+using ExprEitherSymcrete = either<Expr, Symcrete>;
 
 template <typename ValueType, typename SetType,
           typename CMP = std::less<ValueType>>
@@ -55,7 +68,7 @@ class DisjointSetUnion {
     roots.remove(b);
     disjointSets.replace(
         {a, SetType::merge(disjointSets.at(a), disjointSets.at(b))});
-    disjointSets.replace({b, nullptr});
+    disjointSets.remove(b);
   }
 
   bool areJoined(const ValueType &i, const ValueType &j) const {
@@ -109,6 +122,8 @@ class DisjointSetUnion {
   }
 
   void add(const DisjointSetUnion &b) {
+    internalStorage_ty oldRoots = roots;
+    internalStorage_ty newRoots = b.roots;
     for (auto it : b.parent) {
       parent.insert(it);
     }
@@ -124,6 +139,15 @@ class DisjointSetUnion {
     for (auto it : b.disjointSets) {
       disjointSets.insert(it);
     }
+    for (ValueType nv : newRoots) {
+      for (ValueType ov : oldRoots) {
+        if (!areJoined(ov, nv) &&
+            SetType::intersects(disjointSets.at(find(ov)),
+                                disjointSets.at(find(nv)))) {
+          merge(ov, nv);
+        }
+      }
+    }
   }
 
   DisjointSetUnion() {}
@@ -140,4 +164,5 @@ class DisjointSetUnion {
   disjointSets_ty ds() const { return disjointSets; }
 };
 } // namespace klee
-#endif
+
+#endif /* KLEE_DISJOINEDSETUNION_H */

include/klee/ADT/Either.h

@@ -0,0 +1,142 @@
+//===-- Either.h ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EITHER_H
+#define KLEE_EITHER_H
+
+#include "klee/ADT/Ref.h"
+
+#include "klee/Support/Casting.h"
+
+#include <cassert>
+
+namespace llvm {
+class raw_ostream;
+} // namespace llvm
+
+namespace klee {
+
+template <class T1, class T2> class either_left;
+template <class T1, class T2> class either_right;
+
+template <class T1, class T2> class either {
+protected:
+  friend class ref<either<T1, T2>>;
+  friend class ref<const either<T1, T2>>;
+
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
+
+public:
+  using left = either_left<T1, T2>;
+  using right = either_right<T1, T2>;
+
+  enum class EitherKind { Left, Right };
+
+  virtual ~either() {}
+  virtual EitherKind getKind() const = 0;
+
+  static bool classof(const either<T1, T2> *) { return true; }
+  // virtual unsigned hash() = 0;
+  virtual int compare(const either<T1, T2> &b) = 0;
+  virtual bool equals(const either<T1, T2> &b) = 0;
+};
+
+template <class T1, class T2> class either_left : public either<T1, T2> {
+protected:
+  friend class ref<either_left<T1, T2>>;
+  friend class ref<const either_left<T1, T2>>;
+
+private:
+  ref<T1> value_;
+
+public:
+  either_left(ref<T1> leftValue) : value_(leftValue){};
+
+  ref<T1> value() const { return value_; }
+  operator ref<T1> const() { return value_; }
+
+  virtual typename either<T1, T2>::EitherKind getKind() const override {
+    return either<T1, T2>::EitherKind::Left;
+  }
+
+  static bool classof(const either<T1, T2> *S) {
+    return S->getKind() == either<T1, T2>::EitherKind::Left;
+  }
+  static bool classof(const either_left<T1, T2> *) { return true; }
+
+  // virtual unsigned hash() override { return value_->hash(); };
+  virtual int compare(const either<T1, T2> &b) override {
+    if (b.getKind() != getKind()) {
+      return b.getKind() < getKind() ? -1 : 1;
+    }
+    const either_left<T1, T2> &el = static_cast<const either_left<T1, T2> &>(b);
+    if (el.value() != value()) {
+      return el.value() < value() ? -1 : 1;
+    }
+    return 0;
+  }
+
+  virtual bool equals(const either<T1, T2> &b) override {
+    if (b.getKind() != getKind()) {
+      return false;
+    }
+    const either_left<T1, T2> &el = static_cast<const either_left<T1, T2> &>(b);
+    return el.value() == value();
+  }
+};
+
+template <class T1, class T2> class either_right : public either<T1, T2> {
+protected:
+  friend class ref<either_right<T1, T2>>;
+  friend class ref<const either_right<T1, T2>>;
+
+private:
+  ref<T2> value_;
+
+public:
+  either_right(ref<T2> rightValue) : value_(rightValue){};
+
+  ref<T2> value() const { return value_; }
+  operator ref<T2> const() { return value_; }
+
+  virtual typename either<T1, T2>::EitherKind getKind() const override {
+    return either<T1, T2>::EitherKind::Right;
+  }
+
+  static bool classof(const either<T1, T2> *S) {
+    return S->getKind() == either<T1, T2>::EitherKind::Right;
+  }
+  static bool classof(const either_right<T1, T2> *) { return true; }
+
+  // virtual unsigned hash() override { return value_->hash(); };
+  virtual int compare(const either<T1, T2> &b) override {
+    if (b.getKind() != getKind()) {
+      return b.getKind() < getKind() ? -1 : 1;
+    }
+    const either_right<T1, T2> &el =
+        static_cast<const either_right<T1, T2> &>(b);
+    if (el.value() != value()) {
+      return el.value() < value() ? -1 : 1;
+    }
+    return 0;
+  }
+
+  virtual bool equals(const either<T1, T2> &b) override {
+    if (b.getKind() != getKind()) {
+      return false;
+    }
+    const either_right<T1, T2> &el =
+        static_cast<const either_right<T1, T2> &>(b);
+    return el.value() == value();
+  }
+};
+} // end namespace klee
+
+#endif /* KLEE_EITHER_H */

include/klee/Expr/Constraints.h

@@ -152,6 +152,7 @@ class Simplificator {
   struct SetResult {
     constraints_ty simplified;
     ExprHashMap<ExprHashSet> dependency;
+    bool wasSimplified;
   };
 
 public:

include/klee/Expr/IndependentConstraintSetUnion.h

@@ -1,12 +1,15 @@
 #ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H
 #define KLEE_INDEPENDENTCONSTRAINTSETUNION_H
 
+#include "klee/ADT/Either.h"
+
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/IndependentSet.h"
 
 namespace klee {
 class IndependentConstraintSetUnion
-    : public DisjointSetUnion<ref<Expr>, IndependentConstraintSet> {
+    : public DisjointSetUnion<ref<ExprEitherSymcrete>,
+                              IndependentConstraintSet> {
 public:
   Assignment concretization;
 
@@ -43,4 +46,4 @@ class IndependentConstraintSetUnion
 };
 } // namespace klee
 
-#endif
+#endif /* KLEE_INDEPENDENTCONSTRAINTSETUNION_H */

include/klee/Expr/IndependentSet.h

@@ -2,6 +2,7 @@
 #define KLEE_INDEPENDENTSET_H
 
 #include "klee/ADT/DisjointSetUnion.h"
+#include "klee/ADT/Either.h"
 #include "klee/ADT/PersistentMap.h"
 #include "klee/ADT/PersistentSet.h"
 #include "klee/Expr/Assignment.h"
@@ -21,6 +22,7 @@ DISABLE_WARNING_POP
 #include <vector>
 
 namespace klee {
+using ExprEitherSymcrete = either<Expr, Symcrete>;
 
 template <class T> class DenseSet {
   typedef std::set<T> set_ty;
@@ -84,7 +86,11 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
 
 class IndependentConstraintSet {
 private:
-  using InnerSetUnion = DisjointSetUnion<ref<Expr>, IndependentConstraintSet>;
+  using InnerSetUnion =
+      DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet>;
+
+  void initIndependentConstraintSet(ref<Expr> e);
+  void initIndependentConstraintSet(ref<Symcrete> s);
 
 public:
   // All containers need to become persistent to make fast copy and faster
@@ -117,11 +123,8 @@ class IndependentConstraintSet {
                         Assignment &assign) const;
 
   IndependentConstraintSet();
-  IndependentConstraintSet(ref<Expr> e);
-  IndependentConstraintSet(ref<Symcrete> s);
-  IndependentConstraintSet(const ref<const IndependentConstraintSet> &ics);
-
-  IndependentConstraintSet &operator=(const IndependentConstraintSet &ies);
+  explicit IndependentConstraintSet(ref<ExprEitherSymcrete> v);
+  IndependentConstraintSet(const IndependentConstraintSet &ics);
 
   void print(llvm::raw_ostream &os) const;
 

lib/Core/CXXTypeSystem/CXXTypeManager.cpp

@@ -201,8 +201,10 @@ static ref<Expr> getComplexPointerRestrictions(
     restrictions.addConstraint(innerAlignmentRequirement, {});
   }
 
-  auto simplified = Simplificator::simplify(restrictions.cs()).simplified;
-  restrictions.changeCS(simplified);
+  auto simplified = Simplificator::simplify(restrictions.cs());
+  if (simplified.wasSimplified) {
+    restrictions.changeCS(simplified.simplified);
+  }
   for (auto restriction : restrictions.cs()) {
     if (resultCondition.isNull()) {
       resultCondition = restriction;

lib/Core/ExecutionState.h

@@ -228,9 +228,8 @@ struct Symbolic {
 struct MemorySubobject {
   ref<Expr> address;
   unsigned size;
-  MemorySubobject(ref<Expr> address, unsigned size)
+  explicit MemorySubobject(ref<Expr> address, unsigned size)
       : address(address), size(size) {}
-  MemorySubobject &operator=(const MemorySubobject &other) = default;
 };
 
 struct MemorySubobjectHash {