Reftype mismatch between parser and spec?

[presenthee]

Hi, I'm currently debugging assertions in the interpreter backend. Val_type rule is now temporarily implemented as a typing function call, and its implementation uses a value to type conversion function in the reference interpreter.

(* backend-interpreter/manual.ml *)
let val_type = function
  | [ vt ] ->
    vt
    |> Construct.al_to_value
    |> Reference_interpreter.Value.type_of_value
    |> Construct.al_of_val_type in
  | vs -> Numerics.error_values "$Val_type" vs

However, there is a mismatch when checking reference types using the above function. In runtime-typing of spec, Ref_type rules are defined as follows:

(* spec/wasm-3.0/7-runtime-typing.watsup *)
rule Ref_type/null:
  s |- REF.NULL ht : (REF NULL ht)

rule Ref_type/i31:
  s |- REF.I31_NUM i : (REF eps I31)

rule Ref_type/struct:
  s |- REF.STRUCT_ADDR a : (REF eps dt)
  -- if s.STRUCTS[a].TYPE = dt

rule Ref_type/array:
  s |- REF.ARRAY_ADDR a : (REF eps dt)
  -- if s.ARRAYS[a].TYPE = dt

rule Ref_type/func:
  s |- REF.FUNC_ADDR a : (REF eps dt)
  -- if s.FUNCS[a].TYPE = dt

rule Ref_type/exn:
  s |- REF.EXN_ADDR a : (REF eps EXN)

rule Ref_type/host:
  s |- REF.HOST_ADDR a : (REF eps ANY)

rule Ref_type/extern:
  s |- REF.EXTERN addrref : (REF eps EXTERN)

In the reference interpreter, ref_type is parsed as follows:

(* reference-interpreter/text/parser.mly *)
ref_type :
  | LPAR REF null_opt heap_type RPAR { fun c -> ($3, $4 c) }
  | ANYREF { fun c -> (Null, AnyHT) }  /* Sugar */
  | NULLREF { fun c -> (Null, NoneHT) }  /* Sugar */
  | EQREF { fun c -> (Null, EqHT) }  /* Sugar */
  | I31REF { fun c -> (Null, I31HT) }  /* Sugar */
  | STRUCTREF { fun c -> (Null, StructHT) }  /* Sugar */
  | ARRAYREF { fun c -> (Null, ArrayHT) }  /* Sugar */
  | FUNCREF { fun c -> (Null, FuncHT) }  /* Sugar */
  | NULLFUNCREF { fun c -> (Null, NoFuncHT) }  /* Sugar */
  | EXNREF { fun c -> (Null, ExnHT) }  /* Sugar */
  | NULLEXNREF { fun c -> (Null, NoExnHT) }  /* Sugar */
  | EXTERNREF { fun c -> (NoNull, ExternHT) }  /* Sugar */
  | NULLEXTERNREF { fun c -> (Null, NoExternHT) }  /* Sugar */

I think the first fields of tuples should be NoNull instead of Null except for the NULLREF case for assertions to work well. Is it a minor issue in the parser of the reference interpreter, or are there any parts I'm missing? Thank you.

[rossberg]

That should be correct. The two are unrelated: the Ref_type rules specify the typing of reference values, while the snippet from the parser implements the expansion of type short-hands, which has nothing to do with values.

The interpreter code corresponding to the Ref_type rule is the type_of_ref function in runtime/value.ml. For modularity reasons, its implementation is split up across multiple places; you can grep for type_of_ref' := in runtime/* to find them all.

[presenthee]

Oh, thanks for the detailed explanation. After looking at the code mentioned above, I found that the problem is in the interpreter backend, where we are replacing the typing relation with the function call. I'll close the issue, thanks!