Explanation of type matching in br_on_cast instruction

[q82419]

Hi, I have some questions from the test suites.

At this line:

(assert_return (invoke "null-diff" (i32.const 0)) (i32.const 1))

The argument is 0, and the return value is 1, in this function:

  (func (export "null-diff") (param $i i32) (result i32)
    (block $l (result (ref null struct))
      (block (result (ref any))
        (br_on_cast $l (ref null any) (ref null struct) (table.get (local.get $i)))
      )
      (return (i32.const 0))
    )
    (return (i32.const 1))
  )

Which the 0th value in the table instance is ref.null any assigned in the init function:

  (func (export "init") (param $x externref)
    (table.set (i32.const 0) (ref.null any))
    (table.set (i32.const 1) (ref.i31 (i32.const 7)))
    (table.set (i32.const 2) (struct.new $st (i32.const 6)))
    (table.set (i32.const 3) (array.new $at (i32.const 5) (i32.const 3)))
    (table.set (i32.const 4) (any.convert_extern (local.get $x)))
  )

When invoking null-diff function with the argument 0, it will enter the 2 blocks and run the instruction (br_on_cast $l (ref null any) (ref null struct) (table.get (local.get $i))).
Noticed that the (table.get (local.get $i))) will be ref null any, which $i is 0 from the argument.

According to the spec of executing br_on_cast instruction, the branch occurs when the reference type of the reference (will be ref null any here) matching the rt2 (will be ref null struct here).

The question is, this matching should fail -- cannot find the matching rule of ref null any matching ref null struct.
Therefore the branch will not occur, and this function return 0 at the next line.
But the test suite expected the return value 1, means the branch is expected to occur and the matching succeeded.

Can you help to explain the matching rule here? Thanks!

[tlively]

The cast succeeds because the dynamic type of ref.null any is nullref, i.e. (ref null none) despite the any annotation. nullref <: (ref null struct), so the cast succeeds and the branch is taken.

The spec for ref.null where this behavior is described is here.

Although @rossberg, it looks like the execution spec for the ref.null instruction is out of date.

[q82419]

Thanks for the explanation. I think the ref.null instruction here you mentioned means that the cases of abstract heap type are typed with the least types.

[rossberg]

To give a bit of background, this wart exists because the CG decided to cut nullref from Wasm 2.0, so that we had to introduce the (static) type annotation to determine the type of ref.null instructions. At the same time, this annotation should not have any dynamic meaning, since that would require engines to carry a runtime type around with each null reference, which clearly is undesirable.

@tlively, can you clarify what is outdated?

[tlively]

Ah, I think I misread how the ref.null value worked. I was thinking that ref.null ht was only a value if ht was a none, nofunc, or noextern, so I thought that the execution of ref.null ht was out of date because it was pushing ref.null ht values to the stack without ensuring ht was a bottom type.

I see that any ht is allowed in a ref.null ht value, but does not affect the type of the value, though, so everything makes sense.