Created attachment 8891808 [details] b.wasm The attached binary seems to be valid (is accepted by v8, wabt, binaryen) but is rejected by sm with b.js:22:41 CompileError: at offset 4169: unused values not explicitly dropped by end of block Using wabt's wasmdump, the relevant part seems to be the end of a (valueless) if, 001043: 0c 02 | br 0x2 001045: 45 | i32.eqz 001046: 00 | unreachable 001047: 0d 01 | br_if 0x1 001049: 0b | end I'm not totally sure here, but looks like the br_if is to a block with a value, so it is popping the value and then the condition. Then it re-pushes the value, which is the unreachable. That should make the stack polymorphic, so it's valid code?
Created attachment 8891809 [details] b.js JS file to run the wasm, using js b.js b.wasm (i.e. the binary as a second arg). (The JS runs a bunch of executions as well, this is fuzzer output, which are not really needed here since the issue is in validation.)
Thanks for digging into this! I think SM is actually right here and the spec interpreter confirms with validation error: b.wasm:0xfd6: invalid module: type mismatch: operator requires  but stack has [i32] The signature of 'unreachable' is [t*]->[t*] which means that it can take and produce anything required for validation to succeed. However, the following br_if explicitly leaves a monomorphic i32 on the top of the stack, leaving the stack [t* i32]. So even if we make t* = , there is still that i32 at the top of the stack so validation must fail. So probably it'd be good to file a bug on v8 and wabt. Tentatively closing, but feel free to reopen if I've been to hasty.
Status: NEW → RESOLVED
Last Resolved: a year ago
Resolution: --- → INVALID
You need to log in before you can comment on or make changes to this bug.