Externtype checking during instantiation

[presenthee]

Hi, I would like to ask a question about type validation during instantiation.

In the wasm 3.0 spec, provided imports are checked with the declared types.

In the spec written in DSL, It seems that this checking is reflected as the rule Externaddr_type/sub.

def $instantiate(store, module, externaddr*) : config
def $instantiate(s, module, externaddr*) = s'; f; instr_E* instr_D* instr_S?
  ---- ----
  -- Module_ok: |- module : xt_I* -> xt_E*
  -- (Externaddr_type: s |- externaddr : xt_I)*
  ----
  -- if module = MODULE type* import* func* global* table* mem* tag* elem* data* start? export*
  -- if global* = (GLOBAL globaltype expr_G)*
...

rule Externaddr_type/sub:
  s |- externaddr : xt
  -- Externaddr_type: s |- externaddr : xt'
  -- Externtype_sub: {} |- xt' <: xt

But unlike current wasm 3.0 spec, DSL spec does not instantiate closed type of xt_I. I'm curious whether this is the intended difference or not. If not, a function like $clos_externtype may be needed?

Thank you!

[rossberg]

The type closure moved into the Module_ok judgement. In the old spec, module typing still produced module types whose containing externtypes were not closed. This was a bit weird, so in the SpecTec version, that rule closes these types itself, so we don't need to do it here.

As a second simplification, the application of subtyping on the imports' types moved from here to the externaddr typing judgement Externaddr_type (externaddr was called externval in the old spec). The rule Externaddr_type/sub is the subsumption rule that allows to weaken an externaddr's type to a supertype, which did not exist in the old spec. The actual subtyping between extern types is defined by the relation Externtype_sub.

[presenthee]

Thanks for the explanation! Sorry for the repetitive question, but I have an additional one.

In the module allocation, types of funcs, tables, ..., and elems are also instantiated before allocation.

Similarly, it seems that there is no explicit clos_ function application in allocmodule of the DSL spec, and I couldn't find a rule to instantiate these types (like the Module_ok rule in the instantiate function). Can you please let me know where the instantiation takes place in this case?

def $allocmodule(store, module, externaddr*, val*, ref*, (ref*)*) : (store, moduleinst)
def $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) = (s_7, moduleinst)
  ---- ----
  -- if module = MODULE type* import* func* global* table* mem* tag* elem* data* start? export*
  -- if func* = (FUNC x local* expr_F)*
  -- if global* = (GLOBAL globaltype expr_G)*
  -- if table* = (TABLE tabletype expr_T)*
  -- if mem* = (MEMORY memtype)*
  -- if tag* = (TAG y)*
  -- if elem* = (ELEM elemtype expr_E* elemmode)*
  -- if data* = (DATA byte* datamode)*
  ;; TODO(3, rossberg): inline these
  -- if fa_I* = $funcsxa(externaddr*)
  -- if ga_I* = $globalsxa(externaddr*)
  -- if ta_I* = $tablesxa(externaddr*)
  -- if ma_I* = $memsxa(externaddr*)
  -- if aa_I* = $tagsxa(externaddr*)
  ;; TODO(2, rossberg): get rid of these forward guesses
  -- if fa* = ($(|s.FUNCS|+i_F))^(i_F<|func*|)
  -- if ga* = ($(|s.GLOBALS|+i_G))^(i_G<|global*|)
  -- if ta* = ($(|s.TABLES|+i_T))^(i_T<|table*|)
  -- if aa* = ($(|s.TAGS|+i_A))^(i_A<|tag*|)
  -- if ma* = ($(|s.MEMS|+i_M))^(i_M<|mem*|)
  -- if ea* = ($(|s.ELEMS|+i_E))^(i_E<|elem*|)
  -- if da* = ($(|s.DATAS|+i_D))^(i_D<|data*|)
  -- if dt* = $alloctypes(type*)
  -- if (s_1, fa*) = $allocfuncs(s, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|))
  -- if (s_2, ga*) = $allocglobals(s_1, globaltype*, val_G*)
  -- if (s_3, ta*) = $alloctables(s_2, tabletype*, ref_T*)
  -- if (s_4, ma*) = $allocmems(s_3, memtype*)
  -- if (s_5, aa*) = $alloctags(s_4, dt*[y]*)
  -- if (s_6, ea*) = $allocelems(s_5, elemtype*, (ref_E*)*)
  -- if (s_7, da*) = $allocdatas(s_6, OK^(|data*|), (byte*)*)
  ;; TODO(2, rossberg): use moduleinst here and remove hack above
  -- if xi* = $allocexports({FUNCS fa_I* fa*, GLOBALS ga_I* ga*, TABLES ta_I* ta*, MEMS ma_I* ma*, TAGS aa_I* aa*}, export*)
  -- if moduleinst = {
      TYPES dt*,
      FUNCS fa_I* fa*, \
      GLOBALS ga_I* ga*,
      TABLES ta_I* ta*, \
      MEMS ma_I* ma*,
      TAGS aa_I* aa*,
      ELEMS ea*, \
      DATAS da*,
      EXPORTS xi*
    }

[rossberg]

You are right, it is missing there. Well-spotted!

The type arguments in the calls to allocglobals/tables/mems/elems each ought to have a call to a suitable inst_xyztype function using dt as environment. (Functions and tags are fine, because they just take their types from dt, which already is instantiated.)

I'll prepare a fix.