Request for clarification: is this Wasm valid or not?

[fitzgen]

Context: I'm in the process of adding GC support to wasm-smith and hammering out the bugs in wasmparser's GC validation.

Firefox claims it is not valid with "type mismatch: expression has type (ref any) but expected eqref" on the br_on_non_null instruction. FWIW, wasmparser claims the same, but I don't trust it that much yet.

Binaryen, on the other hand, claims that this is valid.

I've annotated the disassembly with the types on the stack up until the br_on_non_null instruction.

I think the disagreement comes down to the interpretation of the br_on_cast just before. If I understand correctly, it should be typed [externref eqref] -> [externref (ref any)] because diff(anyref, arrayref) = (ref any). It seems like binaryen might be incorrectly leaving the eqref instead of computing the diff? (And also I must be doing the same thing in wasm-smith) But I'd appreciate confirmation / a second pair of eyes on this. Thanks!

(module
  (rec
    (type (;0;) (sub (func (result externref eqref))))
    (type (;1;) (array (mut externref)))
  )
  (import "" "" (global (;0;) (mut f32)))
  (func (;0;) (type 0) (result externref eqref)
    ;; []
    block (type 0) (result externref eqref) ;; label = @1
      ;; []
      block ;; label = @2
        ;; []
        loop (result (ref null 0)) ;; label = @3
          ;; []
          ref.null i31
          ;; [i31ref]
          call 0
          ;; [i31ref externref eqref]
          br 2 (;@1;)
          ;; [i31ref externref eqref]
          global.get 0
          ;; [i31ref externref eqref f32]
          f32.ceil
          ;; [i31ref externref eqref f32]
          call 0
          ;; [i31ref externref eqref f32 externref eqref]
          call 2
          ;; [i31ref externref eqref f32 externref eqref externref eqref]
          br_on_cast 2 (;@1;) anyref arrayref
          ;; [i31ref externref eqref f32 externref eqref externref (ref any)]
          br_on_non_null 3 (;@0;) ;; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< validation error or not?
          ref.is_null
          nop
          unreachable
        end
        unreachable
      end
      unreachable
    end
  )
  (func (;1;) (type 0) (result externref eqref)
    unreachable
  )
  (func (;2;) (type 0) (result externref eqref)
    unreachable
  )
  (memory (;0;) 15 18996)
)

cc @tlively @eqrion

[rossberg]

If in doubt, try the reference interpreter? ;)

I just did, and it agrees with Firefox and wasmparser. Your analysis sounds correct as well.

[fitzgen]

Thanks for the reply, and thanks for checking with the reference interpreter, I should reach for it more often.

Will close this issue and open one in Binaryen.