-
Notifications
You must be signed in to change notification settings - Fork 825
[analysis] Add an abstraction lattice #8036
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
7b596ad
a5ebc6b
d8da812
b9a05f2
44b8a23
5d97ed2
6b13aa3
aaf853b
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,227 @@ | ||
| /* | ||
| * Copyright 2025 WebAssembly Community Group participants | ||
| * | ||
| * Licensed under the Apache License, Version 2.0 (the "License"); | ||
| * you may not use this file except in compliance with the License. | ||
| * You may obtain a copy of the License at | ||
| * | ||
| * http://www.apache.org/licenses/LICENSE-2.0 | ||
| * | ||
| * Unless required by applicable law or agreed to in writing, software | ||
| * distributed under the License is distributed on an "AS IS" BASIS, | ||
| * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| * See the License for the specific language governing permissions and | ||
| * limitations under the License. | ||
| */ | ||
|
|
||
| #include <array> | ||
| #include <tuple> | ||
| #include <utility> | ||
| #include <variant> | ||
|
|
||
| #include "../lattice.h" | ||
| #include "support/utilities.h" | ||
|
|
||
| #if __cplusplus >= 202002L | ||
| #include "analysis/lattices/bool.h" | ||
| #endif | ||
|
|
||
| #ifndef wasm_analysis_lattices_abstraction_h | ||
| #define wasm_analysis_lattices_abstraction_h | ||
|
|
||
| namespace wasm::analysis { | ||
|
|
||
| // CRTP lattice composed of increasingly abstract sub-lattices. The subclass is | ||
| // responsible for providing two method templates. The first abstracts an | ||
| // element of one sub-lattice into an element of the next sub-lattice: | ||
| // | ||
| // template<size_t I, typename E1, typename E2> | ||
| // E2 abstract(const E1&) const | ||
| // | ||
| // The template method should be specialized for each sub-lattice index I, its | ||
| // element type E1, and the next element type E2. | ||
| // | ||
| // The `abstract` method is used to abstract elements of the more specific | ||
| // lattice whenever elements from different lattices are compared or joined. It | ||
| // may also be used to abstract two joined elements from the same lattice when | ||
| // those elements are unrelated and the second method returns true: | ||
| // | ||
| // template<size_t I, typename E> | ||
| // bool shouldAbstract(const E&. const E&) const | ||
| // | ||
| // shouldAbstract is only queried for unrelated elements. Related elements of | ||
| // the same sub-lattice are always joined as normal. | ||
| // | ||
| // `abstract` should be monotonic. Making its input more general should either | ||
| // not change its output or make its output more general. | ||
| // | ||
| // `shouldAbstract` should return true only when no upper bound of its arguments | ||
| // in their original sub-lattice is used. If such an upper bound is used in a | ||
| // comparison or join, the operation may fail to uphold the properties of a | ||
| // lattice. | ||
| template<typename Self, typename... Ls> struct Abstraction { | ||
| using Element = std::variant<typename Ls::Element...>; | ||
|
|
||
| std::tuple<Ls...> lattices; | ||
|
|
||
| Abstraction(Ls&&... lattices) : lattices({std::move(lattices)...}) {} | ||
|
|
||
| Element getBottom() const noexcept { | ||
| return std::get<0>(lattices).getBottom(); | ||
| } | ||
|
|
||
| LatticeComparison compare(const Element& a, const Element& b) const noexcept { | ||
| if (a.index() < b.index()) { | ||
| auto abstractedA = a; | ||
| abstractToIndex(abstractedA, b.index()); | ||
| switch (compare()[b.index()](lattices, abstractedA, b)) { | ||
| case EQUAL: | ||
| case LESS: | ||
| return LESS; | ||
| case NO_RELATION: | ||
| case GREATER: | ||
| return NO_RELATION; | ||
| } | ||
| WASM_UNREACHABLE("unexpected comparison"); | ||
| } | ||
| if (a.index() > b.index()) { | ||
| auto abstractedB = b; | ||
| abstractToIndex(abstractedB, a.index()); | ||
| switch (compare()[a.index()](lattices, a, abstractedB)) { | ||
| case EQUAL: | ||
| case GREATER: | ||
| return GREATER; | ||
| case NO_RELATION: | ||
| case LESS: | ||
| return NO_RELATION; | ||
| } | ||
| WASM_UNREACHABLE("unexpected comparison"); | ||
| } | ||
| return compare()[a.index()](lattices, a, b); | ||
| } | ||
|
|
||
| bool join(Element& joinee, const Element& _joiner) const noexcept { | ||
| Element joiner = _joiner; | ||
| bool changed = false; | ||
| if (joinee.index() < joiner.index()) { | ||
| abstractToIndex(joinee, joiner.index()); | ||
| changed = true; | ||
| } else if (joinee.index() > joiner.index()) { | ||
| abstractToIndex(joiner, joinee.index()); | ||
| } | ||
| while (true) { | ||
| assert(joinee.index() == joiner.index()); | ||
| if (joiner.index() == sizeof...(Ls) - 1) { | ||
| // Cannot abstract further, so we must join no matter what. | ||
| break; | ||
| } | ||
| switch (compare()[joiner.index()](lattices, joinee, joiner)) { | ||
| case NO_RELATION: | ||
| if (shouldAbstract()[joiner.index()](self(), joinee, joiner)) { | ||
| // Try abstracting further. | ||
| joinee = abstract()[joinee.index()](self(), joinee); | ||
| joiner = abstract()[joiner.index()](self(), joiner); | ||
| changed = true; | ||
| continue; | ||
| } | ||
| break; | ||
| case EQUAL: | ||
| case LESS: | ||
| case GREATER: | ||
| break; | ||
| } | ||
| break; | ||
| } | ||
| return join()[joiner.index()](lattices, joinee, joiner) || changed; | ||
| } | ||
|
|
||
| private: | ||
| const Self& self() const noexcept { return *static_cast<const Self*>(this); } | ||
|
|
||
| // TODO: Use C++26 pack indexing. | ||
| template<std::size_t I> using L = std::tuple_element_t<I, std::tuple<Ls...>>; | ||
|
|
||
| // Compute tables of functions that forward operations to the CRTP subtype or | ||
| // the lattices. These tables map the dynamic variant indices to compile-time | ||
| // lattice indices. | ||
|
|
||
| template<std::size_t... I> | ||
| static constexpr auto makeAbstractFuncs(std::index_sequence<I...>) noexcept { | ||
| using F = Element (*)(const Self&, const Element& elem); | ||
| return std::array<F, sizeof...(I)>{ | ||
| [](const Self& self, const Element& elem) -> Element { | ||
| if constexpr (I < sizeof...(Ls) - 1) { | ||
| using E1 = typename L<I>::Element; | ||
| using E2 = typename L<I + 1>::Element; | ||
| return Element(std::in_place_index_t<I + 1>{}, | ||
| self.template abstract<I, E1, E2>(std::get<I>(elem))); | ||
| } else { | ||
| WASM_UNREACHABLE("unexpected abstraction"); | ||
| } | ||
| }...}; | ||
| } | ||
| static constexpr auto abstract() noexcept { | ||
| return makeAbstractFuncs(std::make_index_sequence<sizeof...(Ls)>{}); | ||
| } | ||
|
|
||
| void abstractToIndex(Element& elem, std::size_t index) const noexcept { | ||
| while (elem.index() < index) { | ||
| elem = abstract()[elem.index()](self(), elem); | ||
| } | ||
| } | ||
|
|
||
| template<std::size_t... I> | ||
| static constexpr auto | ||
| makeShouldAbstractFuncs(std::index_sequence<I...>) noexcept { | ||
| using F = bool (*)(const Self&, const Element&, const Element&); | ||
| return std::array<F, sizeof...(I)>{ | ||
| [](const Self& self, const Element& a, const Element& b) -> bool { | ||
| if constexpr (I < sizeof...(Ls) - 1) { | ||
| return self.template shouldAbstract<I>(std::get<I>(a), | ||
| std::get<I>(b)); | ||
| } else { | ||
| WASM_UNREACHABLE("unexpected abstraction check"); | ||
| } | ||
| }...}; | ||
| } | ||
| static constexpr auto shouldAbstract() noexcept { | ||
| return makeShouldAbstractFuncs(std::make_index_sequence<sizeof...(Ls)>{}); | ||
| } | ||
|
|
||
| template<std::size_t... I> | ||
| static constexpr auto makeCompareFuncs(std::index_sequence<I...>) noexcept { | ||
| using F = LatticeComparison (*)( | ||
| const std::tuple<Ls...>&, const Element&, const Element&); | ||
| return std::array<F, sizeof...(I)>{ | ||
| [](const std::tuple<Ls...>& lattices, | ||
| const Element& a, | ||
| const Element& b) -> LatticeComparison { | ||
| return std::get<I>(lattices).compare(std::get<I>(a), std::get<I>(b)); | ||
| }...}; | ||
| } | ||
| static constexpr auto compare() noexcept { | ||
| return makeCompareFuncs(std::make_index_sequence<sizeof...(Ls)>{}); | ||
| } | ||
|
|
||
| template<std::size_t... I> | ||
| static constexpr auto makeJoinFuncs(std::index_sequence<I...>) noexcept { | ||
| using F = bool (*)(const std::tuple<Ls...>&, Element&, const Element&); | ||
| return std::array<F, sizeof...(I)>{[](const std::tuple<Ls...>& lattices, | ||
| Element& joinee, | ||
| const Element& joiner) { | ||
| return std::get<I>(lattices).join(std::get<I>(joinee), | ||
| std::get<I>(joiner)); | ||
| }...}; | ||
| } | ||
| static constexpr auto join() noexcept { | ||
| return makeJoinFuncs(std::make_index_sequence<sizeof...(Ls)>{}); | ||
| } | ||
| }; | ||
|
|
||
| #if __cplusplus >= 202002L | ||
| static_assert(Lattice<Abstraction<Bool, Bool, Bool>>); | ||
| #endif | ||
|
|
||
| } // namespace wasm::analysis | ||
|
|
||
| #endif // wasm_analysis_lattices_abstraction_h | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -14,6 +14,8 @@ | |
| * limitations under the License. | ||
| */ | ||
|
|
||
| #include "analysis/lattice.h" | ||
| #include "analysis/lattices/abstraction.h" | ||
| #include "analysis/lattices/array.h" | ||
| #include "analysis/lattices/bool.h" | ||
| #include "analysis/lattices/flat.h" | ||
|
|
@@ -723,3 +725,130 @@ TEST(StackLattice, Join) { | |
| {flat.get(0), flat.get(1)}, | ||
| {flat.get(0), flat.getTop()}); | ||
| } | ||
|
|
||
| using OddEvenInt = analysis::Flat<uint32_t>; | ||
| using OddEvenBool = analysis::Flat<bool>; | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What does "odd even int" mean? Every integer is already even or odd. This seems like just an integer? "odd even bool" I can see as being interpreted as "a boolean saying whether it is even or odd"- is that right?
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, this is just an integer. I could use a namespace instead of the |
||
| struct OddEvenAbstraction | ||
| : analysis::Abstraction<OddEvenAbstraction, OddEvenInt, OddEvenBool> { | ||
| OddEvenAbstraction() | ||
| : analysis::Abstraction<OddEvenAbstraction, OddEvenInt, OddEvenBool>( | ||
| OddEvenInt{}, OddEvenBool{}) {} | ||
|
|
||
| template<size_t I, typename E1, typename E2> E2 abstract(const E1&) const; | ||
|
|
||
| template<std::size_t I, typename E> | ||
| bool shouldAbstract(const E&, const E&) const; | ||
| }; | ||
|
|
||
| template<> | ||
| OddEvenBool::Element | ||
| OddEvenAbstraction::abstract<0>(const OddEvenInt::Element& elem) const { | ||
| if (elem.isTop()) { | ||
| return OddEvenBool{}.getTop(); | ||
| } | ||
| if (elem.isBottom()) { | ||
| return OddEvenBool{}.getBottom(); | ||
| } | ||
| return OddEvenBool{}.get((*elem.getVal() & 1) == 0); | ||
| } | ||
|
|
||
| template<> | ||
| bool OddEvenAbstraction::shouldAbstract<0>(const OddEvenInt::Element&, | ||
| const OddEvenInt::Element&) const { | ||
| // Since the elements are not related, they must be different integers. | ||
| // Always abstract them. | ||
| return true; | ||
| } | ||
|
|
||
| TEST(AbstractionLattice, GetBottom) { | ||
| OddEvenAbstraction abstraction; | ||
| auto expected = OddEvenAbstraction::Element(OddEvenInt{}.getBottom()); | ||
| EXPECT_EQ(abstraction.getBottom(), expected); | ||
| } | ||
|
|
||
| TEST(AbstractionLattice, Join) { | ||
| OddEvenAbstraction abstraction; | ||
|
|
||
| auto expectJoin = [&](const char* file, | ||
| int line, | ||
| const auto& joinee, | ||
| const auto& joiner, | ||
| const auto& expected) { | ||
| testing::ScopedTrace trace(file, line, ""); | ||
| switch (abstraction.compare(joinee, joiner)) { | ||
| case analysis::NO_RELATION: | ||
| EXPECT_NE(joinee, joiner); | ||
| EXPECT_EQ(abstraction.compare(joiner, joinee), analysis::NO_RELATION); | ||
| EXPECT_EQ(abstraction.compare(joinee, expected), analysis::LESS); | ||
| EXPECT_EQ(abstraction.compare(joiner, expected), analysis::LESS); | ||
| break; | ||
| case analysis::EQUAL: | ||
| EXPECT_EQ(joinee, joiner); | ||
| EXPECT_EQ(abstraction.compare(joiner, joinee), analysis::EQUAL); | ||
| EXPECT_EQ(abstraction.compare(joinee, expected), analysis::EQUAL); | ||
| EXPECT_EQ(abstraction.compare(joiner, expected), analysis::EQUAL); | ||
| break; | ||
| case analysis::LESS: | ||
| EXPECT_EQ(joiner, expected); | ||
| EXPECT_EQ(abstraction.compare(joiner, joinee), analysis::GREATER); | ||
| EXPECT_EQ(abstraction.compare(joinee, expected), analysis::LESS); | ||
| EXPECT_EQ(abstraction.compare(joiner, expected), analysis::EQUAL); | ||
| break; | ||
| case analysis::GREATER: | ||
| EXPECT_EQ(joinee, expected); | ||
| EXPECT_EQ(abstraction.compare(joiner, joinee), analysis::LESS); | ||
| EXPECT_EQ(abstraction.compare(joinee, expected), analysis::EQUAL); | ||
| EXPECT_EQ(abstraction.compare(joiner, expected), analysis::LESS); | ||
| } | ||
| { | ||
| auto copy = joinee; | ||
| EXPECT_EQ(abstraction.join(copy, joiner), joinee != expected); | ||
| EXPECT_EQ(copy, expected); | ||
| } | ||
| { | ||
| auto copy = joiner; | ||
| EXPECT_EQ(abstraction.join(copy, joinee), joiner != expected); | ||
| EXPECT_EQ(copy, expected); | ||
| } | ||
| }; | ||
|
|
||
| #define JOIN(a, b, c) expectJoin(__FILE__, __LINE__, a, b, c) | ||
|
|
||
| auto bot = abstraction.getBottom(); | ||
| auto one = OddEvenAbstraction::Element(OddEvenInt{}.get(1)); | ||
| auto two = OddEvenAbstraction::Element(OddEvenInt{}.get(2)); | ||
| auto three = OddEvenAbstraction::Element(OddEvenInt{}.get(3)); | ||
| auto four = OddEvenAbstraction::Element(OddEvenInt{}.get(4)); | ||
| auto even = OddEvenAbstraction::Element(OddEvenBool{}.get(true)); | ||
| auto odd = OddEvenAbstraction::Element(OddEvenBool{}.get(false)); | ||
| auto top = OddEvenAbstraction::Element(OddEvenBool{}.getTop()); | ||
|
|
||
| JOIN(bot, bot, bot); | ||
| JOIN(bot, one, one); | ||
| JOIN(bot, two, two); | ||
| JOIN(bot, even, even); | ||
| JOIN(bot, odd, odd); | ||
| JOIN(bot, top, top); | ||
|
|
||
| JOIN(one, one, one); | ||
| JOIN(one, two, top); | ||
| JOIN(one, three, odd); | ||
| JOIN(one, even, top); | ||
| JOIN(one, odd, odd); | ||
|
|
||
| JOIN(two, two, two); | ||
| JOIN(two, three, top); | ||
| JOIN(two, four, even); | ||
| JOIN(two, even, even); | ||
| JOIN(two, odd, top); | ||
| JOIN(two, top, top); | ||
|
|
||
| JOIN(even, even, even); | ||
| JOIN(even, odd, top); | ||
| JOIN(even, top, top); | ||
|
|
||
| JOIN(odd, odd, odd); | ||
| JOIN(odd, top, top); | ||
|
|
||
| #undef JOIN | ||
| } | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't follow this. We abstract
a, then compare - but we turn that outcome into either "less" or "no"? Why can't we return "greater"or "equal"?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The element
acame from a more concrete lattice than elementb, soacannot possibly be equal to or greater thanb, even if its abstracted version is.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, then my mental model is all wrong here.
I was thinking "an abstraction lattice has items from a tower of types. when it needs to, it abstracts - moves a type up the tower. but otherwise it works normally, i.e., when it has two values to compare, it abstracts the ones it needs to, then compares - and that result can be anything at all".
From what you are saying, it seems there is a ordering of some kind in the tower... is that right? How precisely?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(My mental model is based on the example test, where it seems it abstracts an int to an even/odd as needed, and after such abstraction, the result can be anything... so I may have misunderstood that too.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, there's a tower of sub-lattices. But elements from a lower sub-lattice are always less than elements from higher sub-lattices. Otherwise the user would have to provide complete implementations of comparisons and joins across sub-lattices, so the user code would become quadratic in the number of sub-lattices rather than linear.
The test lattice looks like this:
All the integer elements are less than the even/odd bool elements.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, for sure. But
abstract(X)is a different lattice element thanX, soabstract(X) > Ydoes not imply thatX > Y. And indeed we know that eitherX < YorX <> YifXhad to be abstracted to be in the same sub-lattice asY.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Then I do not understand the motivation for this lattice.
My sense was "abstract as you need, until you can compare things." So if my lattice has integers and even/odd, then given 42 and odd, I must abstract the 42 - but after doing so, I then compare it. And, if even/odd was not flat, that outcome could go either way.
That seems obviously useful in practice - when given 42,1337, the comparison just works; when given even,odd, the same; when given a mix like 42/odd, we abstract "just enough", looking at a higher level, which misses details but at least we get some useful abstraction out of our abstract interpretation.
Put another way, given 42,1337, we could also abstract them both before comparing. Maybe that makes sense for some reason, like distilling them to the core information we care about. We abstract to the properties we care about, then compare/operate.
If, instead, abstract(X) > Y does not imply that X > Y, then I'm not sure how this would be used in practice - can you please elaborate?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The elements 42 and 1337 are not related, but when they are joined they are both abstracted, becoming
evenandodd, which are still not related. But there is no further abstraction possible, so they are then joined to becometop.To take another example, 42 and
evenare related. 42 is less thaneven. When 42 andevenare joined, the 42 is abstracted toevenand then joined with the othereven, producingeven.For yet another example, 42 and 2 are not related. When they are joined, they are both abstracted to
evenand the result iseven. If I understand the way you are thinking we should do things, then to compare 42 and 2 we would first abstract them and then compare. But that would give EQUALS, and 42 is clearly not equal to 2.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And if the even/odd lattice was not flat? Say
odd < even. What happens then?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We figured out offline that the issue is that the abstraction transformation must be monotonic. With that in place, the weird situations I was envisioning are ruled out.