specification/wasm-3.0/4.4-execution.modules.spectec

;;
;; Execution of Modules
;;

;; Allocation

def $alloctypes(type*) : deftype* hint(show $alloctype*#((%)))
def $alloctypes(eps) = eps
def $alloctypes(type'* type) = deftype'* deftype*
  -- if deftype'* = $alloctypes(type'*)
  -- if type = TYPE rectype
  -- if deftype* = $subst_all_deftypes($rolldt(x, rectype), deftype'*)
  -- if x = |deftype'*|

def $alloctag(store, tagtype) : (store, tagaddr)
def $alloctag(s, tagtype) = (s ++ {TAGS taginst}, |s.TAGS|)
  ---- ----
  -- if taginst = { TYPE tagtype }

def $alloctags(store, tagtype*) : (store, tagaddr*) hint(show $alloctag*#((%,%))) hint(prose_allocxs)
def $alloctags(s, eps) = (s, eps)
def $alloctags(s, tagtype tagtype'*) = (s_2, ja ja'*)
  -- if (s_1, ja) = $alloctag(s, tagtype)
  -- if (s_2, ja'*) = $alloctags(s_1, tagtype'*)

def $allocglobal(store, globaltype, val) : (store, globaladdr)
def $allocglobal(s, globaltype, val) = (s ++ {GLOBALS globalinst}, |s.GLOBALS|)
  ---- ----
  -- if globalinst = { TYPE globaltype, VALUE val }

def $allocglobals(store, globaltype*, val*) : (store, globaladdr*) hint(show $allocglobal*#((%,%,%))) hint(prose_allocxs)
def $allocglobals(s, eps, eps) = (s, eps)
def $allocglobals(s, globaltype globaltype'*, val val'*) = (s_2, ga ga'*)
  -- if (s_1, ga) = $allocglobal(s, globaltype, val)
  -- if (s_2, ga'*) = $allocglobals(s_1, globaltype'*, val'*)

def $allocmem(store, memtype) : (store, memaddr)
def $allocmem(s, at `[i .. j?] PAGE) = (s ++ {MEMS meminst}, |s.MEMS|)
  ---- ----
  -- if meminst = { TYPE (at `[i .. j?] PAGE), BYTES (0x00)^(i * $($(64 * $Ki))) }

def $allocmems(store, memtype*) : (store, memaddr*) hint(show $allocmem*#((%,%))) hint(prose_allocxs)
def $allocmems(s, eps) = (s, eps)
def $allocmems(s, memtype memtype'*) = (s_2, ma ma'*)
  -- if (s_1, ma) = $allocmem(s, memtype)
  -- if (s_2, ma'*) = $allocmems(s_1, memtype'*)

def $alloctable(store, tabletype, ref) : (store, tableaddr)
def $alloctable(s, at `[i .. j?] rt, ref) = (s ++ {TABLES tableinst}, |s.TABLES|)
  ---- ----
  -- if tableinst = { TYPE (at `[i .. j?] rt), REFS ref^i }

def $alloctables(store, tabletype*, ref*) : (store, tableaddr*) hint(show $alloctable*#((%,%,%))) hint(prose_allocxs)
def $alloctables(s, eps, eps) = (s, eps)
def $alloctables(s, tabletype tabletype'*, ref ref'*) = (s_2, ta ta'*)
  -- if (s_1, ta) = $alloctable(s, tabletype, ref)
  -- if (s_2, ta'*) = $alloctables(s_1, tabletype'*, ref'*)

def $allocfunc(store, deftype, funccode, moduleinst) : (store, funcaddr)
def $allocfunc(s, deftype, funccode, moduleinst) = (s ++ {FUNCS funcinst}, |s.FUNCS|)
  ---- ----
  -- if funcinst = { TYPE deftype, MODULE moduleinst, CODE funccode }

def $allocfuncs(store, deftype*, funccode*, moduleinst*) : (store, funcaddr*) hint(show $allocfunc*#((%,%,%,%))) hint(prose_allocxs)
def $allocfuncs(s, eps, eps, eps) = (s, eps)
def $allocfuncs(s, dt dt'*, funccode funccode'*, moduleinst moduleinst'*) = (s_2, fa fa'*)
  -- if (s_1, fa) = $allocfunc(s, dt, funccode, moduleinst)
  -- if (s_2, fa'*) = $allocfuncs(s_1, dt'*, funccode'*, moduleinst'*)

def $allocdata(store, datatype, byte*) : (store, dataaddr)
def $allocdata(s, OK, byte*) = (s ++ {DATAS datainst}, |s.DATAS|)
  ---- ----
  -- if datainst = { BYTES byte* }

def $allocdatas(store, datatype*, (byte*)*) : (store, dataaddr*) hint(show $allocdata*#((%,%,%))) hint(prose_allocxs)
def $allocdatas(s, eps, eps) = (s, eps)
def $allocdatas(s, ok ok'*, (b*) (b'*)*) = (s_2, da da'*)
  -- if (s_1, da) = $allocdata(s, ok, b*)
  -- if (s_2, da'*) = $allocdatas(s_1, ok'*, (b'*)*)

def $allocelem(store, elemtype, ref*) : (store, elemaddr)
def $allocelem(s, elemtype, ref*) = (s ++ {ELEMS eleminst}, |s.ELEMS|)
  ---- ----
  -- if eleminst = { TYPE elemtype, REFS ref* }

def $allocelems(store, elemtype*, (ref*)*) : (store, elemaddr*) hint(show $allocelem*#((%,%,%))) hint(prose_allocxs)
def $allocelems(s, eps, eps) = (s, eps)
def $allocelems(s, rt rt'*, (ref*) (ref'*)*) = (s_2, ea ea'*)
  -- if (s_1, ea) = $allocelem(s, rt, ref*)
  -- if (s_2, ea'*) = $allocelems(s_1, rt'*, (ref'*)*)

def $allocexport(moduleinst, export) : exportinst hint(show $allocexport(moduleinst, %2))  ;; HACK !
def $allocexport(moduleinst, EXPORT name (TAG x)) = { NAME name, ADDR (TAG moduleinst.TAGS[x]) }
def $allocexport(moduleinst, EXPORT name (GLOBAL x)) = { NAME name, ADDR (GLOBAL moduleinst.GLOBALS[x]) }
def $allocexport(moduleinst, EXPORT name (MEM x)) = { NAME name, ADDR (MEM moduleinst.MEMS[x]) }
def $allocexport(moduleinst, EXPORT name (TABLE x)) = { NAME name, ADDR (TABLE moduleinst.TABLES[x]) }
def $allocexport(moduleinst, EXPORT name (FUNC x)) = { NAME name, ADDR (FUNC moduleinst.FUNCS[x]) }

def $allocexports(moduleinst, export*) : exportinst* hint(show $allocexport*#(%,%)) hint(prose_allocxs)
def $allocexports(moduleinst, export*) = $allocexport(moduleinst, export)*


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* tag* global* mem* table* func* data* elem* start? export*
  -- if tag* = (TAG tagtype)*
  -- if global* = (GLOBAL globaltype expr_G)*
  -- if mem* = (MEMORY memtype)*
  -- if table* = (TABLE tabletype expr_T)*
  -- if func* = (FUNC x local* expr_F)*
  -- if data* = (DATA byte* datamode)*
  -- if elem* = (ELEM elemtype expr_E* elemmode)*
  ;; TODO(3, rossberg): inline these
  -- if aa_I* = $tagsxa(externaddr*)
  -- if ga_I* = $globalsxa(externaddr*)
  -- if ma_I* = $memsxa(externaddr*)
  -- if ta_I* = $tablesxa(externaddr*)
  -- if fa_I* = $funcsxa(externaddr*)
  -- if dt* = $alloctypes(type*)
  ;; TODO(3, rossberg): get rid of this forward guess?
  -- if fa* = ($(|s.FUNCS|+i_F))^(i_F<|func*|)
  ;; TODO(3, rossberg): use $inst_type(_, moduleinst) instead of $subst_all_type(_, dt*) below
  -- if (s_1, aa*) = $alloctags(s, $subst_all_tagtype(tagtype, dt*)*)
  -- if (s_2, ga*) = $allocglobals(s_1, $subst_all_globaltype(globaltype, dt*)*, val_G*)
  -- if (s_3, ma*) = $allocmems(s_2, $subst_all_memtype(memtype, dt*)*)
  -- if (s_4, ta*) = $alloctables(s_3, $subst_all_tabletype(tabletype, dt*)*, ref_T*)
  -- if (s_5, da*) = $allocdatas(s_4, OK^(|data*|), (byte*)*)
  -- if (s_6, ea*) = $allocelems(s_5, $subst_all_reftype(elemtype, dt*)*, (ref_E*)*)
  -- if (s_7, fa*) = $allocfuncs(s_6, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|))
  ;; TODO(3, rossberg): use moduleinst here and remove hack above
  -- if xi* = $allocexports({TAGS aa_I* aa*, GLOBALS ga_I* ga*, MEMS ma_I* ma*, TABLES ta_I* ta*, FUNCS fa_I* fa*}, export*)
  -- if moduleinst = {
      TYPES dt*,
      TAGS aa_I* aa*, \
      GLOBALS ga_I* ga*,
      MEMS ma_I* ma*,
      TABLES ta_I* ta*, \
      FUNCS fa_I* fa*, \
      DATAS da*,
      ELEMS ea*, \
      EXPORTS xi*
    }


;; Instantiation

def $rundata_(dataidx, data) : instr*
def $rundata_(x, DATA b^n (PASSIVE)) = eps
def $rundata_(x, DATA b^n (ACTIVE y instr*)) =
  instr* (CONST I32 0) (CONST I32 n) (MEMORY.INIT y x) (DATA.DROP x)

def $runelem_(elemidx, elem) : instr*
def $runelem_(x, ELEM rt e^n (PASSIVE)) = eps
def $runelem_(x, ELEM rt e^n (DECLARE)) = (ELEM.DROP x)
def $runelem_(x, ELEM rt e^n (ACTIVE y instr*)) =
  instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT y x) (ELEM.DROP x)

;; TODO(2, rossberg): replace with something more uniform
def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%))) hint(macro none)
def $evalexprs(z, eps) = (z, eps)
def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
  ----
  -- Eval_expr: z; expr ~>* z'; ref
  -- if (z'', ref'*) = $evalexprs(z', expr'*)

def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%))) hint(macro none)
def $evalexprss(z, eps) = (z, eps)
def $evalexprss(z, expr* expr'**) = (z'', ref* ref'**)
  ----
  -- if (z', ref*) = $evalexprs(z, expr*)
  -- if (z'', ref'**) = $evalexprss(z', expr'**)

def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%))) hint(macro none)
def $evalglobals(z, eps, eps) = (z, eps)
def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
  ----
  -- Eval_expr: z; expr ~>* z'; val
  -- if z' = s; f
  -- if (s', a) = $allocglobal(s, gt, val)
  -- if (z'', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)

def $instantiate(store, module, externaddr*) : config
def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E* instr_D* instr_S?
  ---- ----
  -- Module_ok: |- module : xt_I* -> xt_E*
  -- (Externaddr_ok: s |- externaddr : xt_I)*
  ----
  -- if module = MODULE type* import* tag* global* mem* table* func* data* elem* start? export*
  -- if global* = (GLOBAL globaltype expr_G)*
  -- if table* = (TABLE tabletype expr_T)*
  -- if data* = (DATA byte* datamode)*
  -- if elem* = (ELEM reftype expr_E* elemmode)*
  -- if start? = (START x)?
  ;; TODO(2, rossberg): avoid this HACK and use moduleinst directly, or built it fully incrementally
  -- if moduleinst_0 = {
      TYPES $alloctypes(type*),
      GLOBALS $globalsxa(externaddr*),
      FUNCS $funcsxa(externaddr*) ($(|s.FUNCS|+i_F))^(i_F<|func*|) \
    }
  -- if z = s; {MODULE moduleinst_0}
  -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*)
  -- if (z'', ref_T*) = $evalexprs(z', expr_T*)
  -- if (z''', ref_E**) = $evalexprss(z'', expr_E**)
  -- if z''' = s'''; f
  -- if (s'''', moduleinst) = $allocmodule(s''', module, externaddr*, val_G*, ref_T*, (ref_E*)*)
  -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))
  -- if instr_E* = $concat_(instr, $runelem_(i_E, elem*[i_E])^(i_E<|elem*|))
  -- if instr_S? = (CALL x)?


;; Invocation

def $invoke(store, funcaddr, val*) : config
def $invoke(s, funcaddr, val*) = s; {MODULE {}}; val* (REF.FUNC_ADDR funcaddr) (CALL_REF s.FUNCS[funcaddr].TYPE)
  ----
  -- Expand: s.FUNCS[funcaddr].TYPE ~~ FUNC t_1* -> t_2*
  -- (Val_ok: s |- val : t_1)*