Implement a generic set abstract domain on top of a given set

Summary: This implements a similar design as D50054646 but for sets. Users can provide set implementations by implementing `AbstractSet`. Then, a new class `SetAbstractDomain` can turn it into a powerset with a top and bottom element. For now, this is only used to implement `PatriciaTreeSetAbstractDomain`, but we will use it for hash set and sparse set in a follow-up. Reviewed By: arnaudvenet Differential Revision: D50054946 fbshipit-source-id: 756a5b5a3b66b7525e8e06b6d5b0046daab8d07a
facebook · Oct 9, 2023 · afa37f8 · afa37f8
1 parent 028d60b
commit afa37f8
Show file tree

Hide file tree

Showing 2 changed files with 146 additions and 120 deletions.
diff --git a/include/sparta/PatriciaTreeSetAbstractDomain.h b/include/sparta/PatriciaTreeSetAbstractDomain.h
@@ -7,90 +7,11 @@
 
 #pragma once
 
-#include <cstddef>
-#include <initializer_list>
-#include <unordered_set>
-
 #include <sparta/PatriciaTreeSet.h>
-#include <sparta/PowersetAbstractDomain.h>
+#include <sparta/SetAbstractDomain.h>
 
 namespace sparta {
 
-template <typename Element>
-class PatriciaTreeSetAbstractDomain;
-
-namespace ptsad_impl {
-
-/*
- * An abstract value from a powerset is implemented as a Patricia tree.
- */
-template <typename Element>
-class SetValue final
-    : public PowersetImplementation<Element,
-                                    const PatriciaTreeSet<Element>&,
-                                    SetValue<Element>> {
- public:
-  SetValue() = default;
-
-  explicit SetValue(Element e) : m_set(std::move(e)) {}
-
-  explicit SetValue(std::initializer_list<Element> l)
-      : m_set(l.begin(), l.end()) {}
-
-  explicit SetValue(PatriciaTreeSet<Element> set) : m_set(std::move(set)) {}
-
-  const PatriciaTreeSet<Element>& elements() const { return m_set; }
-
-  size_t size() const { return m_set.size(); }
-
-  bool contains(const Element& e) const { return m_set.contains(e); }
-
-  void add(const Element& e) { m_set.insert(e); }
-
-  void add(Element&& e) { m_set.insert(std::move(e)); }
-
-  void remove(const Element& e) { m_set.remove(e); }
-
-  void clear() { m_set.clear(); }
-
-  AbstractValueKind kind() const { return AbstractValueKind::Value; }
-
-  bool leq(const SetValue& other) const {
-    return m_set.is_subset_of(other.m_set);
-  }
-
-  bool equals(const SetValue& other) const { return m_set.equals(other.m_set); }
-
-  AbstractValueKind join_with(const SetValue& other) {
-    m_set.union_with(other.m_set);
-    return AbstractValueKind::Value;
-  }
-
-  AbstractValueKind meet_with(const SetValue& other) {
-    m_set.intersection_with(other.m_set);
-    return AbstractValueKind::Value;
-  }
-
-  AbstractValueKind difference_with(const SetValue& other) {
-    m_set.difference_with(other.m_set);
-    return AbstractValueKind::Value;
-  }
-
-  friend std::ostream& operator<<(std::ostream& o, const SetValue& value) {
-    o << "[#" << value.size() << "]";
-    o << value.m_set;
-    return o;
-  }
-
- private:
-  PatriciaTreeSet<Element> m_set;
-
-  template <typename T>
-  friend class sparta::PatriciaTreeSetAbstractDomain;
-};
-
-} // namespace ptsad_impl
-
 /*
  * An implementation of powerset abstract domains using Patricia trees. This
  * implementation should be used for analyses that create large numbers of
@@ -116,45 +37,7 @@ class SetValue final
  *
  */
 template <typename Element>
-class PatriciaTreeSetAbstractDomain final
-    : public PowersetAbstractDomain<Element,
-                                    ptsad_impl::SetValue<Element>,
-                                    const PatriciaTreeSet<Element>&,
-                                    PatriciaTreeSetAbstractDomain<Element>> {
- public:
-  using Value = ptsad_impl::SetValue<Element>;
-
-  PatriciaTreeSetAbstractDomain()
-      : PowersetAbstractDomain<Element,
-                               Value,
-                               const PatriciaTreeSet<Element>&,
-                               PatriciaTreeSetAbstractDomain>() {}
-
-  explicit PatriciaTreeSetAbstractDomain(AbstractValueKind kind)
-      : PowersetAbstractDomain<Element,
-                               Value,
-                               const PatriciaTreeSet<Element>&,
-                               PatriciaTreeSetAbstractDomain>(kind) {}
-
-  explicit PatriciaTreeSetAbstractDomain(Element e) {
-    this->set_to_value(Value(std::move(e)));
-  }
-
-  explicit PatriciaTreeSetAbstractDomain(std::initializer_list<Element> l) {
-    this->set_to_value(Value(l));
-  }
-
-  explicit PatriciaTreeSetAbstractDomain(PatriciaTreeSet<Element> set) {
-    this->set_to_value(Value(std::move(set)));
-  }
-
-  static PatriciaTreeSetAbstractDomain bottom() {
-    return PatriciaTreeSetAbstractDomain(AbstractValueKind::Bottom);
-  }
-
-  static PatriciaTreeSetAbstractDomain top() {
-    return PatriciaTreeSetAbstractDomain(AbstractValueKind::Top);
-  }
-};
+using PatriciaTreeSetAbstractDomain =
+    SetAbstractDomain<PatriciaTreeSet<Element>>;
 
 } // namespace sparta
diff --git a/include/sparta/SetAbstractDomain.h b/include/sparta/SetAbstractDomain.h
@@ -0,0 +1,143 @@
+/*
+ * Copyright (c) Meta Platforms, Inc. and affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#pragma once
+
+#include <cstddef>
+#include <initializer_list>
+
+#include <sparta/AbstractSet.h>
+#include <sparta/PowersetAbstractDomain.h>
+
+namespace sparta {
+
+namespace set_impl {
+
+template <typename Set>
+class SetValue;
+
+} // namespace set_impl
+
+/*
+ * An implementation of powerset abstract domains based on the given set.
+ */
+template <typename Set>
+class SetAbstractDomain final
+    : public PowersetAbstractDomain<typename Set::value_type,
+                                    set_impl::SetValue<Set>,
+                                    const Set&,
+                                    SetAbstractDomain<Set>> {
+ public:
+  using Value = set_impl::SetValue<Set>;
+  using Element = typename Set::value_type;
+
+  ~SetAbstractDomain() {
+    static_assert(std::is_base_of<AbstractSet<Set>, Set>::value,
+                  "Set doesn't inherit from AbstractSet");
+  }
+
+  SetAbstractDomain()
+      : PowersetAbstractDomain<Element,
+                               Value,
+                               const Set&,
+                               SetAbstractDomain>() {}
+
+  explicit SetAbstractDomain(AbstractValueKind kind)
+      : PowersetAbstractDomain<Element, Value, const Set&, SetAbstractDomain>(
+            kind) {}
+
+  explicit SetAbstractDomain(Element e) {
+    this->set_to_value(Value(std::move(e)));
+  }
+
+  explicit SetAbstractDomain(std::initializer_list<Element> l) {
+    this->set_to_value(Value(l));
+  }
+
+  explicit SetAbstractDomain(Set set) {
+    this->set_to_value(Value(std::move(set)));
+  }
+
+  static SetAbstractDomain bottom() {
+    return SetAbstractDomain(AbstractValueKind::Bottom);
+  }
+
+  static SetAbstractDomain top() {
+    return SetAbstractDomain(AbstractValueKind::Top);
+  }
+};
+
+namespace set_impl {
+
+template <typename Set>
+class SetValue final : public PowersetImplementation<typename Set::value_type,
+                                                     const Set&,
+                                                     SetValue<Set>> {
+ public:
+  using Element = typename Set::value_type;
+
+  SetValue() = default;
+
+  explicit SetValue(Element e) : m_set(std::move(e)) {}
+
+  explicit SetValue(std::initializer_list<Element> l)
+      : m_set(l.begin(), l.end()) {}
+
+  explicit SetValue(Set set) : m_set(std::move(set)) {}
+
+  const Set& elements() const { return m_set; }
+
+  size_t size() const { return m_set.size(); }
+
+  bool contains(const Element& e) const { return m_set.contains(e); }
+
+  void add(const Element& e) { m_set.insert(e); }
+
+  void add(Element&& e) { m_set.insert(std::move(e)); }
+
+  void remove(const Element& e) { m_set.remove(e); }
+
+  void clear() { m_set.clear(); }
+
+  AbstractValueKind kind() const { return AbstractValueKind::Value; }
+
+  bool leq(const SetValue& other) const {
+    return m_set.is_subset_of(other.m_set);
+  }
+
+  bool equals(const SetValue& other) const { return m_set.equals(other.m_set); }
+
+  AbstractValueKind join_with(const SetValue& other) {
+    m_set.union_with(other.m_set);
+    return AbstractValueKind::Value;
+  }
+
+  AbstractValueKind meet_with(const SetValue& other) {
+    m_set.intersection_with(other.m_set);
+    return AbstractValueKind::Value;
+  }
+
+  AbstractValueKind difference_with(const SetValue& other) {
+    m_set.difference_with(other.m_set);
+    return AbstractValueKind::Value;
+  }
+
+  friend std::ostream& operator<<(std::ostream& o, const SetValue& value) {
+    o << "[#" << value.size() << "]";
+    o << value.m_set;
+    return o;
+  }
+
+ private:
+  Set m_set;
+
+  friend class sparta::SetAbstractDomain<Set>;
+};
+
+} // namespace set_impl
+
+} // namespace sparta