[spec] Narrow definition of null ref values

[rossberg]

Tighten the definition of ref.null refs, so that there no longer is an overlap between ref.null reduction and cast-fail rules.

@zilinc, PTAL.

[zilinc]

Thanks. I will need to implement a more correct pattern matching in my meta-interpreter to account for the premises attached to the constructors. My understanding is that the front-end elaborator won't check the premises to try to infer the most precise type. In the following example, both arguments to the $is_sub function are inferred to be supt type, and both args to $only_sub are inferred subt.

syntax supt = C int | D bool
syntax subt = C int -- if int > 100

def $is_sub(supt) : bool
def $is_sub(subt) = true
def $is_sub(supt) = false -- otherwise

def $only_sub(subt) : bool
def $only_sub(C n) = true

def $caller() : bool
def $caller() = $is_sub(C 100) /\ $is_sub(C 101) /\ $only_sub(C 100) /\ $only_sub(C 101)

If that's the case, then I'm not entirely sure if Il.Eval.match_exp is doing the right thing.

[zilinc]

Another question I have is about the right way to do substitution on the premises in typecase? Say we have

syntax supt = C int int | D bool
syntax subt = C int_1 int_2 -- if int_1 > 100 /\ int_2 < 100

def $is_sub(supt) : bool
def $is_sub(subt) = true
def $is_sub(supt) = false -- otherwise

Say if the actual argument passed in is C 100 0, and the pattern is SubE (VarE _, subt, supt). We want to check if the argument can be a subt. By looking up subt type and unfold its definition, we get the relevant typecase C%%, (TupT [int, int], [(int_1 : int), (int_2 : int)], IfPr (int_1 > 100 /\ int_2 < 100)), hints. What is the right way to substitute in 100 and 0 to the premise? Is there an implicit order in the quant list that correspond to how they appear in the type definition?

A more complicated example is

syntax t = C (int_1, int_2) (int_3, int_4) -- if int_1 > 1 /\ int_2 > 2 /\ int_3 > 3 /\ int_4 > 4

var n : int

def $foo(t) : int
def $foo(C (n_1, n_2) (n_3, n_4)) = $(n_1 + n_2 + n_3 + n_4)

def $caller() : int
def $caller() = $foo(C nn_12 nn_34)
  -- if ($int$(1), $int$(2)) = nn_12
  -- if ($int$(3), $int$(4)) = nn_34

If I want to match C nn_12 nn_34 against type t, then I'd need to normalise this expression to C (1, 2) (3, 4). In the typecase, I believe it'd be C, (TupT [TupT [int; int]; TupT [int; int]], [(int_1: int), (int_2 : int), (int_3 : int), (int_4 : int)], prems), hints. What is the way that I can associate (1, 2) (3, 4) to the int_n binders?

[rossberg]

Well, it's doing the "right" thing in that (a) type side conditions do not affect operational behaviour, and (b) the definition of $is_sub above violates the coherence assumption under that semantics, so can return either.

But I agree that we perhaps shouldn't use something like that to distinguish rules either. I'm preparing a better fix.

[rossberg]

@zilinc, this fixes it in a much cleaner manner, please have a look.

The abstract syntax now properly distinguishes ref.null instructions from ref.null_addr values, the latter not carrying a type annotation anymore, eliminating the whole problem. Unfortunately, though, this had various repercussions and required some adjustments to the AL interpreter as well as the reference interpreter.

@f52985, there are 3 2 remaining failures with the interpreter that I wasn't able to figure out after an afternoon of chasing. In the first two, it looks like it doesn't recognise REF.NULL_ADDR (some printf debugging told me that val in the assertion is REF.NULL_ADDR, which should have been handled by the first rule). In the third case, there is a REF.NULL showing up as a value, although that should already have been reduced away.

[rossberg]

Okay, I fixed the third failure, but I think there is a bug with the AL translation that causes the remaining two, because ANY.CONVERT_EXTERN looks like this in AL:

Al ANY.CONVERT_EXTERN ():
 Assert (top_value())
 Pop val
 If ((val = REF.NULL_ADDR)) {
   Push REF.NULL_ADDR
 }
 Assert (case(val) == REF.EXTERN)
 Let (REF.EXTERN ref) = val
 Push ref

I think the statements after the If ought to be in an Else branch?

[zilinc]

@zilinc, this fixes it in a much cleaner manner, please have a look.

The abstract syntax now properly distinguishes ref.null instructions from ref.null_addr values, the latter not carrying a type annotation anymore, eliminating the whole problem. Unfortunately, though, this had various repercussions and required some adjustments to the AL interpreter as well as the reference interpreter.

Thanks Andreas. It indeed looks to be a net simplification, and it should become totally standard in my meta-interpreter.

One semi-related thing is in the bikeshed doc, https://webassembly.github.io/spec/core/bikeshed/#values%E2%91%A2 in section 4.2.1, it has the 0.8ex gibberish rendered and is messed up terribly. It may need some care.

[rossberg]

@zilinc, sigh, this appears to be another episode in the saga of Bikeshed breaking the Wasm spec. I tried a fix that seems to have worked (annoyingly, the Bikeshed build doesn't work on my Mac, so I cannot test it locally).

(That said, I do not recommend the Bikeshed version of the spec. It has many issues due to missing/broken functionality in the Katex renderer it is using.)

[f52985]

Okay, I fixed the third failure, but I think there is a bug with the AL translation that causes the remaining two, because ANY.CONVERT_EXTERN looks like this in AL:

Al ANY.CONVERT_EXTERN ():
 Assert (top_value())
 Pop val
 If ((val = REF.NULL_ADDR)) {
   Push REF.NULL_ADDR
 }
 Assert (case(val) == REF.EXTERN)
 Let (REF.EXTERN ref) = val
 Push ref

I think the statements after the If ought to be in an Else branch?

Sorry for the delay.

The cause was somewhat subtle. The translator had a heuristic pass that treated a single case-checking condition within a block as an assertion.

Previously, both conditions were case-checking conditions:

If (case(val) == REF.NULL_ADDR)
...
If (case(val) == REF.EXTERN)

Because there were two such conditions, both remained simple if statements.

After this PR, however, the first condition was changed into a comparison expression involving a nullary CaseE. As a result, the second condition became the only case-checking condition in the block, and the heuristic incorrectly transformed it into an assertion.

This has now been fixed so that the translator correctly recognizes this pattern and avoids converting it into an assertion.