bt_table validation

[manoskouk]

TL;DR: I suggest dropping the check that all br_table targets have equal types (which will become more complicated in the presence of subtyping), and instead check that stack values are compatible with every target.

First of all, thanks for this proposal. As an engine implementor, I think it will make decoding simpler, especially given the upcoming proposals which complicate the type system.

To the matter at hand: the br_table typing rule states that label_types(ctrls[n]) != label_types(ctrls[m]). This is chosen over typechecking against each label to cover the following situation in unreachable code: (block i32 (block i64 (unreachable) (i32.const 42) (br_table 0 1 0))) should not validate, because, even though every individual label would be fine in a polymorphic stack environment, there is no value that could simultaneously type check against all labels. However, given upcoming proposals which introduce subtyping, this computation is not as simple as checking for label type equality. Instead we need to compute that the greatest common subtype (GCS) of all label types is not bottom. This, however is not as simple: In the GC proposal, consider the types (ref null t1) and (ref t2) where t1 <: t2. Their GCS is (ref t1) which is neither of these types. Implementing the GCS algorithm correctly will take a few hundreds of lines of code, and will be only useful for technicality in unreachable code. Therefore, I suggest to switch to checking that stack values typecheck against the type of each individual label (which is trivially true in unreachable code).

[rossberg]

He he, this is actually the intended semantics right now, see e.g. the changed algorithm in the current draft. The current test suite also matches this. However, there is an oversight wrt the spec rule, and waiting for a review of WebAssembly/spec#1305 which fixes it.

See also my presentation from a 2019 F2F meeting, where I brought up the exact problem you are describing. Back then, the CG already agreed to avoid the need for computing glbs and lubs.

[conrad-watt]

Yes, with @rossberg's bottom value type change, most of the worst cases are avoided independent of this proposal. In fact, the more I think about the implications of his bottom value type change, the more marginal I feel this proposal is :)

The main value of this proposal would be in

1. avoiding the need for a polymorphic stack base that's already present in the MVP and hopefully not made worse by any post-MVP extensions (although if it were made worse, that would be a strong motivation for this proposal)
2. avoiding some ugly looking "if bottom then skip-check" tests when implementing type-checking for certain post-MVP instructions, although potentially trading this off against more "if dead then skip-check" tests, depending on the implementation strategy.

[manoskouk]

Thank you for your responses!

[rossberg]

WebAssembly/spec#1305 has landed, so I guess we can close this particular issue.

@conrad-watt, I agree it's probably a wash for the time being. But as you observed at some point, the situation will become a bit more complicated with typed references (as in the function-types proposal). That requires introducing a bottom heap type as well. In most places that merely amounts to skipping more checks.

However, there is one case in the GC proposal which is problematic, namely rtt.sub. Its declarative type is:

ref.sub : [(ref (rtt $t n?))] -> [(ref (rtt $t (n+1)?)]

Here, n is the (optional) depth of the subtyping chain. If known for the operand, then the result has to be +1. But if the operand is bottom, then any n would be possible, and there is no principal type that can be derived (unless we introduce a bottom depth, which seems excessive).

It's not clear whether we want to keep the depth in the types anyway, so maybe this case becomes moot. But we might introduce similar ones in the future. At that point, it may be more attractive to introduce a bottom stack type instead.