Fix ref.null semantics

[ShinWonho]

Problem

This is the semantics of ref.null ht in the current specification.
But I think simply pushing ref.null ht is problematic.

Example

Consider the following example, which is simplified version of "test-sub" in ref_test.wast.

(module
  (type $t0 (sub (struct)))

  (func (export "test-sub")
    ;; must hold
    (ref.test (ref null $t0) (ref.null $t0))
    (drop)))

(assert_return (invoke "test-sub"))

According to the semantics of ref.test, we first need to get the reference type of ref.null $t0.

However, the typeindex $t0 is not ok under empty context.

Suggested change

In the reference interpreter, type index of ref.null $t0 is substituted before pushed.

let rec step (c : config) : config =

      ....

      | RefNull t, vs' ->
        Ref (NullRef (subst_heap_type (subst_of c.frame.inst) t)) :: vs', []

Therefore, I fixed the semantics according to the reference interpreter.

[rossberg]

Ah, good catch! This is rather annoying, if only ref.null didn't have this dreaded type annotation...

Unfortunately, I think the fix isn't quite as easy as that. Because (ref.null ht) is defined to be a value, and values must never reduce, otherwise the Progress statement is compromised.

So we need to syntactically distinguish reduced null refs from non-reduced ones. We could do it based on the shape of the ht, which is probably fine for now (you'll need to add a side condition to the grammar of reference values), but is a bit hacky and not very robust.

Long-term, I think the cleaner fix is to make the type annotation optional. Then the reduction rule would remove it. And the typing rule for valid-ref would only allow unannotated ref.null and assign it type (ref null bot).

But changing the syntax of reference values like that requires more adjustments throughout the spec, and even the JS API spec. The interpreter should be adjusted as well then. That's quite a bit of work, so perhaps for later.

[zapashcanon]

Because (ref.null ht) is defined to be a value, and values must never reduce, otherwise the Progress statement is compromised.

Wouldn't having null.new $t to be an instruction and ref.null $t a value fix the issue ?

[rossberg]

See my reply on the other issue. Also, ref.null is already standardised as part of Wasm 2.0 (as is ref.func, btw), so we cannot change it anymore.

[ShinWonho]

I changed the syntax of ref.null value so that ref.null with type index cannot be a value.
Is this right fix?

[rossberg]

This is correct in spirit, but technically, since meta variables are existentially quantified, a negation like this doesn't do the right thing – you can always take a different type index to make it true. I think you need to say some like "t = absheaptype ∨ t = deftype". Or perhaps spell it out as \REFNULL~\absheaptype~|~\REFNULL~\deftype.

[ShinWonho]

Thank you for the comment! I fixed this.

[rossberg]

I think a variation of this note still applies, since we only reduce some ref.null's.

[ShinWonho]

I added a note like this. If you think there are better words, feel free to change it.

[rossberg]

Thanks!