Skip to content

Commit

Permalink
Take the less-equal binary function as a argument in PatriciaTreeCore…
Browse files Browse the repository at this point in the history
…::leq

Summary:
We want to use patricia trees in another tool internally, to improve performance.
That tool has an abstract domain interface that has an additional parameter for its `leq` operator.
Unfortunately, the `leq` operator in sparta is a static method in the `ValueInterface`, which cannot be adapted for that tool.

To unblock the situation, let's make `PatriciaTreeCore` (the internal class representing patricia tree) accept an arbitrary operator for its `leq` method.
Note that `PatriciaTreeMap`, `PatriciaTreeMapAbstractEnvironment` and `PatriciaTreeMapAbstractPartition` are unchanged.

We also expose a `find` method that returns nullptr when the key is not found. This will also be necessary.

Reviewed By: arnaudvenet

Differential Revision: D60052170

fbshipit-source-id: c27eeaef4872fe8d4b9b93409e5017622faf1952
  • Loading branch information
arthaud authored and facebook-github-bot committed Jul 23, 2024
1 parent 59322e0 commit 850b004
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 18 deletions.
35 changes: 18 additions & 17 deletions include/sparta/PatriciaTreeCore.h
Original file line number Diff line number Diff line change
Expand Up @@ -599,17 +599,11 @@ inline bool is_tree_subset_of(
}

/* Assumes Value::default_value_kind is either Top or Bottom */
template <typename IntegerType, typename Value>
template <typename IntegerType, typename Value, typename Compare>
inline bool is_tree_leq(
const intrusive_ptr<PatriciaTreeNode<IntegerType, Value>>& s,
const intrusive_ptr<PatriciaTreeNode<IntegerType, Value>>& t) {
using ValueType = typename Value::type;
constexpr bool kHasLeq =
std::is_same_v<decltype(Value::leq(std::declval<ValueType>(),
std::declval<ValueType>())),
bool>;
static_assert(kHasLeq, "Value::leq() is not defined");

const intrusive_ptr<PatriciaTreeNode<IntegerType, Value>>& t,
Compare&& compare) {
static_assert(Value::default_value_kind == AbstractValueKind::Top ||
Value::default_value_kind == AbstractValueKind::Bottom);

Expand All @@ -629,7 +623,7 @@ inline bool is_tree_leq(
// Both nodes are leaves. s leq to t iff
// key(s) == key(t) && value(s) <= value(t).
return s_leaf->key() == t_leaf->key() &&
Value::leq(s_leaf->value(), t_leaf->value());
compare(s_leaf->key(), s_leaf->value(), t_leaf->value());
} else if (s_leaf) {
// t has at least one non-default binding that s doesn't have.
if (Value::default_value_kind == AbstractValueKind::Top) {
Expand All @@ -647,7 +641,7 @@ inline bool is_tree_leq(
// Always false if default_value is Bottom, which we already assume.
return false;
} else {
return Value::leq(s_leaf->value(), *t_value);
return compare(s_leaf->key(), s_leaf->value(), *t_value);
}
} else if (t_leaf) {
// s has at least one non-default binding that t doesn't have.
Expand All @@ -661,7 +655,7 @@ inline bool is_tree_leq(
// Always false if default_value is Top, which we already assume.
return false;
} else {
return Value::leq(*s_value, t_leaf->value());
return compare(t_leaf->key(), *s_value, t_leaf->value());
}
}

Expand All @@ -677,17 +671,17 @@ inline bool is_tree_leq(
const auto& t0 = t_branch->left_tree();
const auto& t1 = t_branch->right_tree();
if (m == n && p == q) {
return is_tree_leq(s0, t0) && is_tree_leq(s1, t1);
return is_tree_leq(s0, t0, compare) && is_tree_leq(s1, t1, compare);
} else if (m < n && match_prefix(q, p, m)) {
// The tree t only contains bindings present in a subtree of s, and s has
// bindings not present in t.
return Value::default_value_kind == AbstractValueKind::Top &&
is_tree_leq(is_zero_bit(q, m) ? s0 : s1, t);
is_tree_leq(is_zero_bit(q, m) ? s0 : s1, t, compare);
} else if (m > n && match_prefix(p, q, n)) {
// The tree s only contains bindings present in a subtree of t, and t has
// bindings not present in s.
return Value::default_value_kind == AbstractValueKind::Bottom &&
is_tree_leq(s, is_zero_bit(p, n) ? t0 : t1);
is_tree_leq(s, is_zero_bit(p, n) ? t0 : t1, compare);
} else {
// s and t both have bindings that are not present in the other tree.
return false;
Expand Down Expand Up @@ -1371,6 +1365,11 @@ class PatriciaTreeCore {
return contains_leaf_with_key(Codec::encode(key), m_tree);
}

// Returns nullptr if the key is mapped to the default value.
inline const ValueType* find(Key key) const {
return find_value_by_key(Codec::encode(key), m_tree);
}

inline const ValueType& at(Key key) const {
if (const auto* value = find_value_by_key(Codec::encode(key), m_tree)) {
return *value;
Expand Down Expand Up @@ -1401,8 +1400,10 @@ class PatriciaTreeCore {
return pt_core::is_tree_subset_of(m_tree, other.m_tree);
}

inline bool leq(const PatriciaTreeCore& other) const {
return pt_core::is_tree_leq(m_tree, other.m_tree);
template <typename Compare>
inline bool leq(const PatriciaTreeCore& other, Compare compare) const {
return pt_core::is_tree_leq(
m_tree, other.m_tree, std::forward<Compare>(compare));
}

inline bool equals(const PatriciaTreeCore& other) const {
Expand Down
5 changes: 4 additions & 1 deletion include/sparta/PatriciaTreeMap.h
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,10 @@ class PatriciaTreeMap final
const mapped_type& at(Key key) const { return m_core.at(key); }

bool leq(const PatriciaTreeMap& other) const {
return m_core.leq(other.m_core);
return m_core.leq(other.m_core,
[](auto, const mapped_type& a, const mapped_type& b) {
return ValueInterface::leq(a, b);
});
}

bool equals(const PatriciaTreeMap& other) const {
Expand Down

0 comments on commit 850b004

Please sign in to comment.