Explanation of type matching in ref_test tests

[q82419]

Hi, when running the ref_test test suite here, I have some questions.

When validating this module, we have defined types:

  (type $t0 (sub (struct)))
  (type $t1 (sub $t0 (struct (field i32))))

And in the "test-sub" function:

  (func (export "test-sub")
    (call $init)
    (block $l
      ;; must hold
      (br_if $l (i32.eqz (ref.test (ref null $t0) (ref.null struct))))
      (br_if $l (i32.eqz (ref.test (ref null $t0) (ref.null $t0))))
      (br_if $l (i32.eqz (ref.test (ref null $t0) (ref.null $t1))))   ;; mark here
      (br_if $l (i32.eqz (ref.test (ref null $t0) (ref.null $t2))))
      (br_if $l (i32.eqz (ref.test (ref null $t0) (ref.null $t3))))
     ...

Let's focus on the ref.test instruction in the marked line (ref.test (ref null $t0) (ref.null $t1)).

First the ref.null $t1 will push the type ref null $t1 onto the stack by the validation rule.

And according to the rule of ref.test, this will be valid for any valid reference type rt' on the top of stack for which rt matches rt'.

That means, in this case, this instruction will be valid for which ref null $t0 (of this instruction) matches ref null $t1 (on the top of the stack).

That is, this instruction will be valid for which (sub (struct)) matches (sub $t0 (struct (field i32))).

Can you help to explain why this validation passes, or if I misunderstand the rules? Thanks!

[rossberg]

By subsumption, the instruction (ref.null $t1) also has type [] → [(ref null any)], and (ref null any) is a suitable rt' that is a supertype of (ref null $t0).

This is a bit of a trick of the kind sometimes used in the specification of type systems. What the rule is saying is that you can weaken the operand type to anything less precise than rt (since it's a downcast anyway). Implicitly, what it is really saying is that you can always pick the corresponding top type. Before we introduced the different subtype hierarchies (any/func/extern), ref.test in fact simply had type [anyref] → [i32]. The current formulation allows picking funcref or externref instead as the top type suitable for rt.

Since this is not so obvious, I created #513 that adds a note to this effect and a case to the validation algorithm in the Appendix.

[rossberg]

But as the spec, this case occurs only when the ht of ref.null is abstract heap type.

I'm not sure what you mean by that. The corresponding dynamic typing rule for ref.null applies for all ht.

[q82419]

Sorry that not specified so detail.

As the note in ref.null instruction:

No formal reduction rule is required for the case `ref.null absheaptype`, since the instruction form is already a value.

I recognized that only for the abstract heap type case, the dynamic typing rule will be applied.
Since the all ht are applied the dynamic typing rule, why not just push ref null t, t ∈ {none, nofunc, noextern} in step 4 of execution?
Thanks.

[rossberg]

The note is just saying why we don't need a case for the formal(!) reduction rule where ht=absheaptype, because it would reduce to itself, as it already is a value.

The dynamic typing rule will be applied to all values, but ref.null x is not a value, so needs reducing first. This is mostly a technicality because it needs to rewrite its type annotation to be closed.

The reduction rule was a late addition, when the other parts already existed and were needed. But given that we now reduce (some) ref.null anyway, you are right that this could be factored somewhat differently. But it would be slightly more cumbersome to specify the syntax of values, and to pick the correct bottom type in such a modified reduction rule for ref.null would seemingly require a dynamic type check.

[q82419]

Thanks for the information.
Sorry that there're so many questions in GC spec, aspecially in the type matching.

[rossberg]

No worries, all good questions. This is much more subtle than everything we had in the type system before.