From 132061636a524b232a4fea949745e83fad30eb56 Mon Sep 17 00:00:00 2001 From: Maxime Arthaud Date: Wed, 27 Sep 2023 03:34:57 -0700 Subject: [PATCH] Explicitly expose the default value kind (top, bottom or value) 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 --- include/sparta/FlatMap.h | 10 +++-- include/sparta/HashMap.h | 12 ++++-- include/sparta/HashedAbstractEnvironment.h | 3 ++ include/sparta/HashedAbstractPartition.h | 3 ++ include/sparta/PatriciaTreeCore.h | 28 +++++++++----- .../PatriciaTreeMapAbstractEnvironment.h | 3 ++ .../sparta/PatriciaTreeMapAbstractPartition.h | 3 ++ test/FlatMapTest.cpp | 38 +++++++++++-------- 8 files changed, 67 insertions(+), 33 deletions(-) diff --git a/include/sparta/FlatMap.h b/include/sparta/FlatMap.h index 8be5f30..1143c49 100644 --- a/include/sparta/FlatMap.h +++ b/include/sparta/FlatMap.h @@ -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"); } } diff --git a/include/sparta/HashMap.h b/include/sparta/HashMap.h index 445b8d3..45f2764 100644 --- a/include/sparta/HashMap.h +++ b/include/sparta/HashMap.h @@ -174,13 +174,17 @@ class HashMap final { static_assert(std::is_base_of_v, 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"); } } diff --git a/include/sparta/HashedAbstractEnvironment.h b/include/sparta/HashedAbstractEnvironment.h index 82a96f4..c62cd3f 100644 --- a/include/sparta/HashedAbstractEnvironment.h +++ b/include/sparta/HashedAbstractEnvironment.h @@ -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 = diff --git a/include/sparta/HashedAbstractPartition.h b/include/sparta/HashedAbstractPartition.h index 689dce6..f707a27 100644 --- a/include/sparta/HashedAbstractPartition.h +++ b/include/sparta/HashedAbstractPartition.h @@ -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; diff --git a/include/sparta/PatriciaTreeCore.h b/include/sparta/PatriciaTreeCore.h index a25a6ea..8636973 100644 --- a/include/sparta/PatriciaTreeCore.h +++ b/include/sparta/PatriciaTreeCore.h @@ -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; }; /* @@ -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 @@ -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 inline bool is_tree_leq( const intrusive_ptr>& s, @@ -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(); @@ -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; } @@ -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; } @@ -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. @@ -1317,6 +1322,9 @@ class PatriciaTreeCore { std::declval())), bool>, "Value::equals() does not exist"); + static_assert(std::is_same_v, + "Value::default_value_kind does not exist"); inline bool empty() const { return m_tree == nullptr; } diff --git a/include/sparta/PatriciaTreeMapAbstractEnvironment.h b/include/sparta/PatriciaTreeMapAbstractEnvironment.h index 85740fe..076cacc 100644 --- a/include/sparta/PatriciaTreeMapAbstractEnvironment.h +++ b/include/sparta/PatriciaTreeMapAbstractEnvironment.h @@ -235,6 +235,9 @@ class MapValue final : public AbstractValue> { 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; diff --git a/include/sparta/PatriciaTreeMapAbstractPartition.h b/include/sparta/PatriciaTreeMapAbstractPartition.h index 52103ca..9b9ba13 100644 --- a/include/sparta/PatriciaTreeMapAbstractPartition.h +++ b/include/sparta/PatriciaTreeMapAbstractPartition.h @@ -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; diff --git a/test/FlatMapTest.cpp b/test/FlatMapTest.cpp index 83313cb..1e64e1b 100644 --- a/test/FlatMapTest.cpp +++ b/test/FlatMapTest.cpp @@ -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; @@ -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;