1385717 - Rejection of valid wasm binary

Status: RESOLVED INVALID

(Core :: JavaScript Engine, defect)

Description

[Alon Zakai (:azakai)]

Attachment: 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?

Comment 1

[Alon Zakai (:azakai)]

Attachment: 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.)

Comment 2

[Luke Wagner [:luke]]

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.