This repository was archived by the owner on Apr 25, 2025. It is now read-only.
Repository navigation
This repository was archived by the owner on Apr 25, 2025. It is now read-only.
Validation rule for call_ref with polymorphic stack #69
Description
Should the following module validate?
(module
(type (func (result f32 f32)))
(func (result f32 f32)
unreachable
call_ref
f64.add
(; to make func result correct ;)
f32.const 0
f32.const 0
)
)
Here's the rule for call_ref:
call_ref calls a function through a reference
call_ref : [t1* (ref null $t)] -> [t2*]
iff $t = [t1*] -> [t2*]
traps on null
The polymorphic stack after unreachable can materialize an unknown type for the callee funcref, but what would the $t of the typing rule be then? And therefore what gets pushed after call_ref?
In the above example, the only legal $t is (type (func (result f32 f32)), and therefore call_ref would push two f32's, which would cause the module to fail validation. This assumes that a legal substitution in that rule must be a declared type in the module the call_ref is in.
If the $t can be synthesized to be any theoretical function type, then the results of a call_ref with an unknown input yields essentially a new polymorphic stack.
Activity
rossberg commentedon Jul 25, 2022
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 commentedon Jul 25, 2022
FWIW, V8 is fine with the
call_ref+f64.addin this example, but complains at the end:Compiling function #0 failed: expected 2 elements on the stack for fallthru, found 3 @+38When I add a
dropafter thef64.add, the module validates in V8. Checking for too many stack values in unreachable code may well be a bug.Binaryen's
wasm-disandwasm-optaccept the module without any changes; I'm not sure whether this implies that Binaryen ran proper validation on it.I don't think anything about unreachable code is an argument for adding bytes to non-unreachable code.
tlively commentedon Jul 25, 2022
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 commentedon Jul 25, 2022
@jakobkummerow:
No, I think you and V8 are correct, as written, this particular example has to be rejected regardless.
rossberg commentedon Aug 25, 2022
Closing via #76.