[analysis] Add a ConeType lattice #8050
Conversation
ConeType is an important part of PossibleContents. Implement it as a standalone lattice that can be combined into a larger lattice if we rewrite PossibleContents in terms of the lattice framework.
|
|
||
| namespace wasm::analysis { | ||
|
|
||
| struct ConeType { |
There was a problem hiding this comment.
A comment describing this could be good.
src/analysis/lattices/conetype.h
Outdated
| if (auto it = typeDepths.find(type.getHeapType()); it != typeDepths.end()) { | ||
| return Element{type, it->second}; | ||
| } | ||
| return Element{type, 0}; |
There was a problem hiding this comment.
Shouldn't this be an encoding of infinity?
There was a problem hiding this comment.
This should only be reached in practice for bottom types. I can add an assertion.
There was a problem hiding this comment.
In that case, can check type.isBottom on line 44?
src/analysis/lattices/conetype.h
Outdated
| bool isTop() const { return type == Type::none; } | ||
| }; | ||
|
|
||
| std::unordered_map<HeapType, Index> typeDepths; |
There was a problem hiding this comment.
Is this a cache (it isn't const which suggests that)? What is the meaning of a missing entry?
There was a problem hiding this comment.
No, it only used to create new elements in get. I can make it const.
| CHECK_MEET(a, b, meet); | ||
| switch (lattice.compare(a, b)) { | ||
| case analysis::NO_RELATION: | ||
| CHECK_UNRELATED(a, b); |
There was a problem hiding this comment.
This is identical to what the switch is branching on, i.e., this adds nothing? It reads as
if (x == 1) {
assert(x == 1);
} else ..There was a problem hiding this comment.
The check also tests the opposite direction.
| Element top; | ||
| Element i32; | ||
| Element i64; | ||
| Element eqNull3; |
There was a problem hiding this comment.
A note to the reader about the depth.
src/analysis/lattices/conetype.h
Outdated
| return changed; | ||
| } | ||
| Index joineeToLub = 0, joinerToLub = 0; | ||
| if (!joinee.isBottom() && !joinee.type.getHeapType().isBottom()) { |
There was a problem hiding this comment.
Is this distinction necessary? That is, do we need to differentiate the case of A being bottom from A's type being bottom?
It seems the difference only arises for non-refs, and the bottom has no more depth below it, so it seems this only applies to the top?
(In PossibleContents, we didn't have cones of the top type - the top type always means "anything" anyhow, so I hope we don't need it here either?)
There was a problem hiding this comment.
The lattice's bottom is {unreachable, 0}, but we also allow elements like {(ref none), 0}. Right now we don't do any kind of canonicalization, so these are considered separate elements. (Similarly, {(ref foo), 0} and {(ref (exact foo)), 0} are currently considered separate elements.)
We could add canonicalization to avoid having multiple elements that are "morally" equivalent like this, but I'm not sure it's necessary, and it makes the lattice properties harder to reason about.
There was a problem hiding this comment.
But do we allow {(ref none), 1)? If not, then why is this line not condensable to a single check?
There was a problem hiding this comment.
No, we have an invariant that bottom heap types always have a depth of 0. This can't be a single check because joinee.isBottom() is checking the unreachable case and joinee.type.isNull() (previously joinee.getHeapType().isBottom()) is checking the none case. There's not a good way to check both at once.
| return changed; | ||
| } | ||
| Index joineeToLub = 0, joinerToLub = 0; | ||
| if (!joinee.isBottom() && !joinee.type.isNull()) { |
There was a problem hiding this comment.
I'm still fuzzy on why nulls are special here. Perhaps add a comment, as it seems nonobvious?
There was a problem hiding this comment.
The top comment already mentions the invariant that bottom heap types always have a depth of zero.
There was a problem hiding this comment.
As for why this is: If we did support arbitrary depths on bottom types, we would have no way to compare the depths with the depths on concrete types. What would the join of {(ref null none), 5} and {(ref null $sub1), 2} be? {(ref null $sub1), 2}? {(ref null $sub1), 1000}? Without an encoding for infinite depth, there's no way to reason about the gap between bottom types and defined types. Since we don't need an encoding of infinite depth for anything else, it's easier to just define the problem away.
| top = lattice.getTop(); | ||
| i32 = lattice.get(Type::i32); | ||
| i64 = lattice.get(Type::i64); | ||
| eqNull3 = lattice.get(Type(HeapType::eq, Nullable)); |
There was a problem hiding this comment.
What makes this have a depth of 3?
There was a problem hiding this comment.
eq -> struct -> $super -> $sub1/2
There was a problem hiding this comment.
I see, thanks. Then this differs from PossibleContents, where depth is only for user types, not basic ones.
There was a problem hiding this comment.
This makes it depend on the set of types given to the lattice to begin with, which PC does not do. I'm not sure which is better.
There was a problem hiding this comment.
Oh, interesting. This just uses the depths provided by SubTypes, so I'm surprised PossibleContents doesn't do the same. I doubt this difference will cause problems, though.
ConeType is an important part of PossibleContents. Implement it as a
standalone lattice that can be combined into a larger lattice if we
rewrite PossibleContents in terms of the lattice framework.