Exact abstract types

[jakobkummerow]

I'd like to reopen the discussion about exact abstract types (such as (ref null? exact any)).

Motivation: I've thought about computing type unions today. By that I mean specifically: when an optimizing compiler encounters a control flow merge, it'll want to compute the type of any merged values as accurately as possible, because having an accurate type might unlock further optimization opportunities in the subsequent code (such as: eliminating casts and branches), whereas on the flip side having inaccurate, overly-generic types might rule out optimizations that would otherwise be applicable. So, just to be extra clear about it, I'm not talking about spec-level union types. I'm aware that as far as the spec is concerned, any control flow merge point will have explicit type annotations, and a validator only needs to check whether the "incoming" types are subtypes of the merged type. But these merged types are often rather loose upper bounds for the values that will actually be seen there, and optimizing engines want to do better.

I'm also well aware that folks tend to say "we must have regularity!!!" as a reflex. In this particular case, I think the "regularity" idea is that the nullability, exactness, and heaptype dimensions of a reference type can be considered orthogonally to each other, so the hope is that if each of these is "regular" on its own, then their composition will also be "regular". On closer inspection, that is not the case: uninhabited types are noise/pollution, and having to filter them out makes implementations overly complex and irregular.

To illustrate, I think this is the behavior an optimizing compiler would want to implement for computing type unions at control flow merge points (assuming a module that has types $sub <: $super <: eq):

Two indexed types: union is exact if both inputs are exact and have
equivalent indices.
(ref $sub), (ref exact $super) -> (ref $super)
(ref exact $sub), (ref $super) -> (ref $super)
(ref exact $sub), (ref exact $super) -> (ref $super)
(ref exact $sub), (ref exact $sub) -> (ref exact $sub)

An indexed type and a non-bottom abstract type: union is exact if the
indexed type is exact and the abstract supertype is uninhabited.
(ref exact $sub), (ref eq) -> (ref eq)
(ref $sub), (ref exact eq) -> (ref $sub) [!!!]
(ref exact $sub), (ref exact eq) -> (ref exact $sub) [!!!]
(ref exact $sub), (ref null exact eq) -> (ref null exact $sub) [!!!]

An indexed type and a none-type: union is exact if the indexed type is exact.
(ref exact $sub), (ref null none) -> (ref null exact $sub)
(ref $sub), (ref null exact none) -> (ref null $sub)
(ref exact $sub), (ref null exact none) -> (ref null exact $sub)

Two abstract types: union is exact if both inputs are exact, even if their
heap types are different:
(ref null exact none), (ref eq) -> (ref null eq)
(ref null none), (ref exact eq) -> (ref null none) [!!!]
(ref null exact none), (ref exact eq) -> (ref null exact none) [!!!]
(ref null exact none), (ref null exact eq) -> (ref null exact none) [!!!]

Note in particular the lines annotated with [!!!], indicating results that may be surprising. I find them surprising too: they violate the rule that union(a, b) == b if a <: b, at least in the heaptype dimension. But we wouldn't want the union of (ref null none) and (ref exact any) to be (ref null any): that would destroy the highly valuable information that the value described by this type is guaranteed to always be null (on all reachable control flow paths)!
Then note that these [!!!] lines are precisely those where exact eq occurs as an input.

This is a new issue with this proposal because previously, only none/bottom types were uninhabited, so handling them fit well into algorithms because they were subtypes of everything else anyway. But now we have "uninhabited supertypes", which are just weird.

Obviously, the behavior above can be implemented, and after shipping a few security vulnerabilities caused by type confusions to their users, most implementations will probably even get it right eventually. But what's the benefit? Previous conversations have agreed that uninhabitable exact abstract types are useless. They may be harmless on the spec level, but they're harmful for implementations.

Spec regularity causes implementation irregularity in this case.

I'm sympathetic to the desire to keep the spec simple. But a few restrictions can hardly be considered excessive complexity. And they're not painting us into a corner either: restrictions can always be lifted if a need for that is discovered.

So, I have two suggestions:

(1) Let's please allow exact only for indexed reference types. IOW, (ref null? exact X) only validates if X is a type index.

(2) Ideally we'd even go one step further and also disallow the combination null+exact, since it's a bit of a contradiction (if the thing with type (ref null exact $x) can be null, then it's not "exactly $x"), and not needed for the primary use case. The recent discussion about shorthands already hinted in the direction that null exact is likely to be far less useful in practice than non-nullable exact. Perhaps we can get by without it entirely? That would turn the two dimensions nullability×exactness into a 3-level scale: in increasing order of strictness, a reference can be nullable, non-nullable, or exact.

[tlively]

The operation you're describing here is not a plain union (or lattice join) operation because it does not maintain key properties such as a <: union(a, b). This operation is instead union(filter(a), filter(b)), where filter maps uninhabitable types to (ref exact bot) and types inhabited only by null values to (ref null exact bot). If you refactor the implementation to separate union and filter (but still use their combination when optimizing, of course), then I hope you would find that the implementation is simpler overall and easier to property test (or fuzz) for correctness because the union operation will have all the properties you would expect of a union.

Since you care about maximizing your optimizing power, I would expect you to prefer allowing more uninhabitable types, though. If, through some sequence of optimizations, wasm-opt produces a block (for example) with result type (ref exact eq), then the engine would be able to use that information to optimize out all the code dominated by that block. If wasm-opt had to generalize that type to (ref eq) because exact references to eq were disallowed, then the engine would not be able to optimize just by looking at the type.

That being said, we could still disallow exact references to abstract heap types if we wanted to. To keep each type hierarchy a lattice, we would need to special-case (ref none) to be a subtype of (ref exact x) and (ref null none) to be a subtype of (ref null exact x). This doesn't seem better or worse than our current special casing of bottom types.

I would expect that Binaryen would continue to internally allow all exact references for the additional follow-on optimization power in case any optimizations are able to produce an exact reference to an abstract type. We would just erase the exactness as necessary in our binary writer.

Ideally we'd even go one step further and also disallow the combination null+exact...

I would strongly prefer we not do this. Binaryen depends on being able to make non-nullable locals nullable as a fixup whenever an optimization changes control flow so a local.get of the local is no longer structurally dominated by a local.set. If we had to do this for a local that happened to hold the descriptor operand for a struct.new, the fixup would have to introduce a new exactness cast as well.

after shipping a few security vulnerabilities caused by type confusions to their users, most implementations will probably even get it right eventually

I know this is tongue-in-cheek, but I strongly believe that targeted property fuzzing of the type system implementation can help avoid this, no matter what particular rules we choose for typing.

[tlively]

OTOH, Binaryen can and should do the filter operation itself to emit (ref null exact? none) and (ref exact? none) instead of arbitrary other uninhabitable or null-only types. And with #16, we have a clear rule that exact non-nullable references to abstract types are uninhabitable, making them categorically useless. I would be happy to disallow exact references to abstract heap types if we can figure out a sensible story for how to allow ref.null none to appear where (ref null exact $some_struct) is expected.

I can see two options:

• Make an exception for bottom types and allow (ref null exact none) and (ref exact none).
• Update the special subtyping rules for bottom types to be (ref null? none) <: (ref null? exact x).

I would probably lean toward the second. If we ever allow exact references to abstract heap types in the future, (ref null? none) and (ref null? exact none) would be identical, but that doesn't seem like the end of the world.

@jakobkummerow, does one of those options sound nicer to you? @rossberg, what would you think of this change?

[rossberg]

Hm, my vague concern with disallowing exact abstract types is that it appears to introduce a discontinuity in the type algebra. Those generally have a strong tendency to mess things up. Maybe that's not a problem in this particular case, at least I can't think of an immediate issue, but I wouldn't bet on it either. Perhaps it makes sense if we view the exact as an attribute on the type index inside a heap type, not outside heap types, but that is a slightly more complex algebra.

Note however that uninhabited types are a pretty normal thing in any sufficiently expressive type system, and cannot generally be avoided. Ruling them out just for its own sake is a weak motivation.

[rossberg]

Thinking through this some more, I’ve just convinced myself that making it part of heap types actually is the right way to skin the game. That is, instead of extending the syntax of reference types, we merely

• introduce one new heap type constructor of the form exact $t,
• with a single subtyping rule exact $t <: $t (in addition to the generic reflexivity & transitivity rules).

Relative to Wasm 3.0 nothing else changes. In particular, nothing new needs to be specified for the bottom type, since the existing rule none <: ht covers the case where ht is an exact type, and likewise all supertypes follow from the transitivity rule.

The consequence of course is that we now need to allow exact in all other places where heap types occur. But the only other place in the entire Wasm syntax currently is ref.null, where @tlively already requested that. So with this factorisation that case follows naturally as well, i.e., (ref.null (exact $t)) : (ref null (exact $t)).

[tlively]

Sounds good to me. @rossberg, are you thinking that we need encodings for both (ref.null (exact $t))) and (ref.null $t), or will we just reinterpret the current encoding as always being exact in that context?

[rossberg]

@tlively, exact being a type constructor for heap types implies that it is represented by a heap type code. Consequently, we automatically get both forms of ref.null. AFAICS, it would be both extra work and irregular to reinterpret or restrict that, with no particular benefit.

[tlively]

Oh, I see. Currently in the binary format we have exact as a prefix for the entire reference type, so we would have to change that. Once we have it as a prefix for just the heap type, everything falls out correctly.

[tlively]

#18 implements this change. PTAL!

[jakobkummerow]

We can consider this fixed by #18. Thanks!