Skip to content

Commit

Permalink
Explicitly expose the default value kind (top, bottom or value)
Browse files Browse the repository at this point in the history 
Summary:
This diff requires users implementing the `ValueType` interface to explicitly expose whether the default value is top, bottom or value, as a `constexpr AbstractValueKind`.
This usually allows optimizations in the `leq` implementation, which can now always be inlined.

Reviewed By: arnaudvenet

Differential Revision: D49639410

fbshipit-source-id: 246e6d6e80d1fa407b42481409ff3abadb91ba16
  • Loading branch information
@arthaud @facebook-github-bot
arthaud authored and facebook-github-bot committed Sep 27, 2023
1 parent ecd559b commit 1320616
Show file tree
Hide file tree
Showing 8 changed files with 67 additions and 33 deletions.
10 changes: 7 additions & 3 deletions include/sparta/FlatMap.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -199,12 +199,16 @@ class FlatMap final {
"leq can only be used when Value implements AbstractDomain");

// Assumes Value::default_value() is either Top or Bottom.
if (Value::default_value().is_top()) {
if constexpr (Value::default_value_kind == AbstractValueKind::Top) {
return this->leq_when_default_is_top(other);
} else if (Value::default_value().is_bottom()) {
} else if constexpr (Value::default_value_kind ==
AbstractValueKind::Bottom) {
return this->leq_when_default_is_bottom(other);
} else {
RUNTIME_CHECK(false, undefined_operation());
static_assert(
Value::default_value_kind == AbstractValueKind::Top ||
Value::default_value_kind == AbstractValueKind::Bottom,
"leq can only be used when Value::default_value() is top or bottom");
}
}

Expand Down
12 changes: 8 additions & 4 deletions include/sparta/HashMap.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,13 +174,17 @@ class HashMap final {
static_assert(std::is_base_of_v<AbstractDomain<ValueType>, ValueType>,
"leq can only be used when Value implements AbstractDomain");

// Assumes Value::default_value() is either Top or Bottom.
if (Value::default_value().is_top()) {
// Assumes Value::default_value_kind is either Top or Bottom.
if constexpr (Value::default_value_kind == AbstractValueKind::Top) {
return this->leq_when_default_is_top(other);
} else if (Value::default_value().is_bottom()) {
} else if constexpr (Value::default_value_kind ==
AbstractValueKind::Bottom) {
return this->leq_when_default_is_bottom(other);
} else {
RUNTIME_CHECK(false, undefined_operation());
static_assert(
Value::default_value_kind == AbstractValueKind::Top ||
Value::default_value_kind == AbstractValueKind::Bottom,
"leq can only be used when Value::default_value() is top or bottom");
}
}

Expand Down
3 changes: 3 additions & 0 deletions include/sparta/HashedAbstractEnvironment.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,9 @@ class MapValue final
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Top;
};

using MapType =
Expand Down
3 changes: 3 additions & 0 deletions include/sparta/HashedAbstractPartition.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,9 @@ class HashedAbstractPartition final
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Bottom;
};

using MapType = HashMap<Label, Domain, ValueInterface, LabelHash, LabelEqual>;
Expand Down
28 changes: 18 additions & 10 deletions include/sparta/PatriciaTreeCore.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,9 @@ struct SimpleValue {
static bool is_default_value(const T& t) { return t == T(); }

static bool equals(const T& a, const T& b) { return a == b; }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Value;
};

/*
Expand All @@ -83,6 +86,9 @@ struct EmptyValue {
static bool is_default_value(const type&) { return true; }

static bool equals(const type&, const type&) { return true; }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Value;
};

template <typename IntegerType, typename Value>
Expand Down Expand Up @@ -590,7 +596,7 @@ inline bool is_tree_subset_of(
return false;
}

/* Assumes Value::default_value() is either Top or Bottom */
/* Assumes Value::default_value_kind is either Top or Bottom */
template <typename IntegerType, typename Value>
inline bool is_tree_leq(
const intrusive_ptr<PatriciaTreeNode<IntegerType, Value>>& s,
Expand All @@ -606,18 +612,17 @@ inline bool is_tree_leq(
"Value::leq() is defined, but Value::type is not an "
"implementation of AbstractDomain");

RUNTIME_CHECK(Value::default_value().is_top() ||
Value::default_value().is_bottom(),
undefined_operation());
static_assert(Value::default_value_kind == AbstractValueKind::Top ||
Value::default_value_kind == AbstractValueKind::Bottom);

if (s == t) {
// This condition allows the leq operation to run in sublinear time when
// comparing Patricia trees that share some structure.
return true;
} else if (s == nullptr) {
return Value::default_value().is_bottom();
return Value::default_value_kind == AbstractValueKind::Bottom;
} else if (t == nullptr) {
return Value::default_value().is_top();
return Value::default_value_kind == AbstractValueKind::Top;
}

const auto* s_leaf = s->as_leaf();
Expand All @@ -629,7 +634,7 @@ inline bool is_tree_leq(
Value::leq(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().is_top()) {
if (Value::default_value_kind == AbstractValueKind::Top) {
// The non-default binding in t can never be <= Top.
return false;
}
Expand All @@ -648,7 +653,7 @@ inline bool is_tree_leq(
}
} else if (t_leaf) {
// s has at least one non-default binding that t doesn't have.
if (Value::default_value().is_bottom()) {
if (Value::default_value_kind == AbstractValueKind::Bottom) {
// There exists a key such that s[key] != Bottom and t[key] == Bottom.
return false;
}
Expand Down Expand Up @@ -678,12 +683,12 @@ inline bool is_tree_leq(
} 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().is_top() &&
return Value::default_value_kind == AbstractValueKind::Top &&
is_tree_leq(is_zero_bit(q, m) ? s0 : s1, t);
} 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().is_bottom() &&
return Value::default_value_kind == AbstractValueKind::Bottom &&
is_tree_leq(s, is_zero_bit(p, n) ? t0 : t1);
} else {
// s and t both have bindings that are not present in the other tree.
Expand Down Expand Up @@ -1317,6 +1322,9 @@ class PatriciaTreeCore {
std::declval<ValueType>())),
bool>,
"Value::equals() does not exist");
static_assert(std::is_same_v<decltype(Value::default_value_kind),
const AbstractValueKind>,
"Value::default_value_kind does not exist");

inline bool empty() const { return m_tree == nullptr; }

Expand Down
3 changes: 3 additions & 0 deletions include/sparta/PatriciaTreeMapAbstractEnvironment.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,6 +235,9 @@ class MapValue final : public AbstractValue<MapValue<Variable, Domain>> {
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Top;
};

MapValue() = default;
Expand Down
3 changes: 3 additions & 0 deletions include/sparta/PatriciaTreeMapAbstractPartition.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ class PatriciaTreeMapAbstractPartition final
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }

constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Bottom;
};

using MapType = PatriciaTreeMap<Label, Domain, ValueInterface>;
Expand Down
38 changes: 22 additions & 16 deletions test/FlatMapTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,19 +116,22 @@ TEST_F(FlatMapTest, updates) {
EXPECT_EQ(0, m1.at(20));
}

TEST_F(FlatMapTest, partitionLeq) {
struct StringSetPartitionInterface {
using type = StringAbstractSet;
struct StringSetPartitionInterface {
using type = StringAbstractSet;

static type default_value() { return type::bottom(); }

static type default_value() { return type::bottom(); }
static bool is_default_value(const type& x) { return x.is_bottom(); }

static bool is_default_value(const type& x) { return x.is_bottom(); }
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool equals(const type& x, const type& y) { return x.equals(y); }
static bool leq(const type& x, const type& y) { return x.leq(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }
};
constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Bottom;
};

TEST_F(FlatMapTest, partitionLeq) {
using Partition =
FlatMap<uint32_t, StringAbstractSet, StringSetPartitionInterface>;

Expand Down Expand Up @@ -222,19 +225,22 @@ TEST_F(FlatMapTest, partitionLeq) {
}
}

TEST_F(FlatMapTest, environmentLeq) {
struct StringSetEnvironmentInterface {
using type = StringAbstractSet;
struct StringSetEnvironmentInterface {
using type = StringAbstractSet;

static type default_value() { return type::top(); }

static type default_value() { return type::top(); }
static bool is_default_value(const type& x) { return x.is_top(); }

static bool is_default_value(const type& x) { return x.is_top(); }
static bool equals(const type& x, const type& y) { return x.equals(y); }

static bool equals(const type& x, const type& y) { return x.equals(y); }
static bool leq(const type& x, const type& y) { return x.leq(y); }

static bool leq(const type& x, const type& y) { return x.leq(y); }
};
constexpr static AbstractValueKind default_value_kind =
AbstractValueKind::Top;
};

TEST_F(FlatMapTest, environmentLeq) {
using Environment =
FlatMap<uint32_t, StringAbstractSet, StringSetEnvironmentInterface>;

Expand Down

0 comments on commit 1320616

Please sign in to comment.