The reference interpreter currently additionally performs a substitution of the local type before producing the default values at a function call (which is still using the old name Invoke) where the spec does not. Compare the following:
exec/eval.ml, L1117-1130:
| Invoke f, vs ->
let (ts1, ts2) = functype_of_comptype (expand_deftype (Func.type_of f)) in
let n1, n2 = List.length ts1, List.length ts2 in
let args, vs' = split n1 vs e.at in
(match f with
| Func.AstFunc (_, inst', func) ->
let Func (_x, ls, es) = func.it in
let m = Lib.Promise.value inst' in
let s = subst_of m in
let ts = List.map (fun {it = Local t; _} -> subst_valtype s t) ls in
let lvs = List.(rev (map Option.some args) @ map default_value ts) in
let frame' = {inst = m; locals = List.map ref lvs} in
let instr' = [Label (n2, [], ([], List.map plain es)) @@ func.at] in
vs', [Frame (n2, frame', ([], instr')) @@ e.at]4.3-execution.instrutions.spectec, L180-186:
rule Step_read/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
----
-- if $funcinst(z)[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = FUNC x (LOCAL t)* (instr*)
-- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE}
Note that the interpreter performs a substitution of ls (which is the local types declared by the function) before mapping it by default_value, but the spec directly uses default_(t)* instead of a similar substitution such as default_(inst_valtype(fi.MODULE, t))*. Actually, the type instantiation definition inst_valtype seems to be unused in all later files.
An interesting part is that this mismatch used to be observable before the narrowing of null references (when ref.null carried a heaptype), as there could be type indices that were not closed and need substitution to resolve them to concrete deftypes. However, after #2093 simplified null references to be a ref.null_addr only, this mismatch was incidentally fixed, because inst_valtype is a noop for generating the default values anyway (numeric/vector values don't care about substitution, null references don't carry a type anymore), so one can argue that this substitution is no longer necessary now. I'm not sure if this was a deliberate fix or not, as inst_valtype seems to be already unused before #2093 was merged. The simpler fix is to add the substitution to the spec I guess.
Also, among all the inst_*type definitions in 4.2, currently only inst_reftype is used (in ref casting/testing rules). I see in the module instantiation spec file that there's a TODO comment for using these inst_global/mem/tabletype definitions though, so I understand that they are planned to replace the current subst_all_*type usages eventually.
The reference interpreter currently additionally performs a substitution of the local type before producing the default values at a function call (which is still using the old name
Invoke) where the spec does not. Compare the following:exec/eval.ml, L1117-1130:
4.3-execution.instrutions.spectec, L180-186:
Note that the interpreter performs a substitution of
ls(which is the local types declared by the function) before mapping it bydefault_value, but the spec directly usesdefault_(t)*instead of a similar substitution such asdefault_(inst_valtype(fi.MODULE, t))*. Actually, the type instantiation definitioninst_valtypeseems to be unused in all later files.An interesting part is that this mismatch used to be observable before the narrowing of null references (when ref.null carried a heaptype), as there could be type indices that were not closed and need substitution to resolve them to concrete deftypes. However, after #2093 simplified null references to be a
ref.null_addronly, this mismatch was incidentally fixed, becauseinst_valtypeis a noop for generating the default values anyway (numeric/vector values don't care about substitution, null references don't carry a type anymore), so one can argue that this substitution is no longer necessary now. I'm not sure if this was a deliberate fix or not, asinst_valtypeseems to be already unused before #2093 was merged. The simpler fix is to add the substitution to the spec I guess.Also, among all the
inst_*typedefinitions in 4.2, currently onlyinst_reftypeis used (in ref casting/testing rules). I see in the module instantiation spec file that there's a TODO comment for using theseinst_global/mem/tabletypedefinitions though, so I understand that they are planned to replace the currentsubst_all_*typeusages eventually.