Validation rule for call_ref with polymorphic stack about function-references

[rossberg]

Good catch! The reference interpreter allows this [edit: with the fix @jakobkummerow points out below], since it just assumes the operand can be (the subtype of) any function type. But as you correctly point out, that is not actually supported by the typing rule, which requires the type to exist in the current module.

In the absence of a type annotation, there is no simple solution to this within the current type system, where type indices are not substituted by definitions. To avoid a crazy algorithm, we'd need to introduce an additional special-case rule for Bottom to achieve more relaxed typing – and similarly for other instructions with reference operands, if we remove their annotations. That would be half a step in the direction of @conrad-watt's relaxed dead code typing proposal, though handling this kind of case would actually require way more changes/additions than what is currently described in that proposal's overview.

So this definitely is an argument for having type annotations.

[jakobkummerow]

FWIW, V8 is fine with the call_ref + f64.add in this example, but complains at the end:
Compiling function #0 failed: expected 2 elements on the stack for fallthru, found 3 @+38
When I add a drop after the f64.add, the module validates in V8. Checking for too many stack values in unreachable code may well be a bug.

Binaryen's wasm-dis and wasm-opt accept the module without any changes; I'm not sure whether this implies that Binaryen ran proper validation on it.

So this definitely is an argument for having type annotations.

I don't think anything about unreachable code is an argument for adding bytes to non-unreachable code.

[tlively]

Binaryen's wasm-dis and wasm-opt accept the module without any changes; I'm not sure whether this implies that Binaryen ran proper validation on it.

Binaryen's validation algorithm is already similar to the one in the relaxed dead code typing proposal, so proper validation was definitely not run.

[rossberg]

@jakobkummerow:

When I add a drop after the f64.add, the module validates in V8. Checking for too many stack values in unreachable code may well be a bug.

No, I think you and V8 are correct, as written, this particular example has to be rejected regardless.

[rossberg]

Closing via #76.