Incorrect implementations of unreachable `ref.as_non_null` validation

[tlively]

V8, SpiderMonkey, and JavaScriptCore all say this invalid module is valid:

(module
  (func $invalid
    (local $i32 i32)
    (unreachable)
    (ref.as_non_null)
    (local.set $i32)
  )
)

I guess production engines never bothered to implement (ref ⊥), so they just have the ref.as_non_null push ⊥ in this situation. The reference interpreter and wasm-tools get this right. WABT gets this wrong. Binaryen doesn't even try to validate unreachable code correctly.

We should probably add a spec test for this, but OTOH that would be really annoying for the engines for no real benefit.

Maybe it's time to revisit the relaxed dead code validation proposal 🤔

cc @conrad-watt

[tlively]

@titzer, Wizard also gets this wrong (not to suggest that you should do anything about it, though).

[tlively]

I expect to run into the same kind of problem with any.convert_extern and extern.convert_any once we have shared types because those will have to produce (ref (⊥-share any)) and (ref (⊥-share extern)), and that's going to be at least as gross to implement.

[titzer]

Confirmed. I think that regardless of whether we change dead code validation, we need better test coverage here. It's very tricky and there's a trickle of these bugs that I don't think will be fixed by spec changes, but can only be fixed by very thorough testing.

[eqrion]

Ah, gross. As a data point, I have spent a significant amount of time analyzing the spec rules for GC types to try and do dead code correctly and missed this. It is very difficult to derive an algorithm from the rules for dead code.

Choosing the valtype bottom is fine for the input, but the output fixes the form ref ht. I think this would also affect br_on_null/br_on_non_null which are the same operation.

[redianthus]

I tried in Owi and we are also accepting this module (cc @hra687261).

I agree with @tlively that it would be great to have the relaxed dead code validation proposal being revisited!

@titzer, are you talking about code coverage in the reference interpreter? If yes, it should be quite easy to generate one. It simply requires adding a single line to the dune file, and then it can be generated with a few commands, see for instance how the ouput looks like in Owi. It requires adding a dependency but it is fully optional and is only needed when actually trying to generate the report. If this is what you had in mind, I can make a PR and automatically deploy it using GH pages as I did in Owi.

[titzer]

@redianthus I meant general coverage of all the cases, but line coverage of the reference interpreter would be a really nice addition.

[tlively]

I posted WebAssembly/relaxed-dead-code-validation#6 to renew the discussion on relaxed dead code validation in light of this problem. Let's move discussion of relaxed dead code validation as a potential solution there, but keep this open to discuss the problem in existing implementations with the current spec rules.

[tlively]

FWIW, the validation algorithm in the appendix of the spec gets this right, and the spec itself mentions that bot needs to be the bottom type of all heap types as well.

I wonder if we should remove the validation algorithm from the appendix. It doesn't seem that anyone is following it closely (except wasm-tools).

[rossberg]

@tlively:

I wonder if we should remove the validation algorithm from the appendix. It doesn't seem that anyone is following it closely (except wasm-tools).

Er, isn't that a real backwards conclusion? Because too many implement it incorrectly, we remove the available guidance on how to implement it correctly?