specification/wasm-1.0/9-module.spectec

;;
;; Projections
;;

def $funcs(externaddr*) : funcaddr*
def $funcs(eps) = eps
def $funcs((FUNC fa) externaddr'*) = fa $funcs(externaddr'*)
def $funcs(externaddr externaddr'*) = $funcs(externaddr'*)
  -- otherwise

def $globals(externaddr*) : globaladdr*
def $globals(eps) = eps
def $globals((GLOBAL ga) externaddr'*) = ga $globals(externaddr'*)
def $globals(externaddr externaddr'*) = $globals(externaddr'*)
  -- otherwise

def $tables(externaddr*) : tableaddr*
def $tables(eps) = eps
def $tables((TABLE ta) externaddr'*) = ta $tables(externaddr'*)
def $tables(externaddr externaddr'*) = $tables(externaddr'*)
  -- otherwise

def $mems(externaddr*) : memaddr*
def $mems(eps) = eps
def $mems((MEM ma) externaddr'*) = ma $mems(externaddr'*)
def $mems(externaddr externaddr'*) = $mems(externaddr'*)
  -- otherwise


;;
;; Allocation
;;

;; Definitions

def $allocfunc(store, moduleinst, func) : (store, funcaddr)
def $allocfunc(s, moduleinst, func) = (s[.FUNCS =++ fi], |s.FUNCS|)
  -- if fi = { TYPE moduleinst.TYPES[x], MODULE moduleinst, CODE func }
  -- if func = FUNC x local* expr

def $allocfuncs(store, moduleinst, func*) : (store, funcaddr*)
def $allocfuncs(s, moduleinst, eps) = (s, eps)
def $allocfuncs(s, moduleinst, func func'*) = (s_2, fa fa'*)
  -- if (s_1, fa) = $allocfunc(s, moduleinst, func)
  -- if (s_2, fa'*) = $allocfuncs(s_1, moduleinst, func'*)

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

def $allocglobals(store, globaltype*, val*) : (store, globaladdr*)
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 $alloctable(store, tabletype) : (store, tableaddr)
def $alloctable(s, `[i .. j?]) = (s[.TABLES =++ ti], |s.TABLES|)
  -- if ti = { TYPE `[i .. j?], REFS eps^i }

def $alloctables(store, tabletype*) : (store, tableaddr*)
def $alloctables(s, eps) = (s, eps)
def $alloctables(s, tabletype tabletype'*) = (s_2, ta ta'*)
  -- if (s_1, ta) = $alloctable(s, tabletype)
  -- if (s_2, ta'*) = $alloctables(s_1, tabletype'*)

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

def $allocmems(store, memtype*) : (store, memaddr*)
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'*)


;; Modules

def $instexport(funcaddr*, globaladdr*, tableaddr*, memaddr*, export) : exportinst
def $instexport(fa*, ga*, ta*, ma*, EXPORT name (FUNC x)) = { NAME name, ADDR (FUNC fa*[x]) }
def $instexport(fa*, ga*, ta*, ma*, EXPORT name (GLOBAL x)) = { NAME name, ADDR (GLOBAL ga*[x]) }
def $instexport(fa*, ga*, ta*, ma*, EXPORT name (TABLE x)) = { NAME name, ADDR (TABLE ta*[x]) }
def $instexport(fa*, ga*, ta*, ma*, EXPORT name (MEM x)) = { NAME name, ADDR (MEM ma*[x]) }


def $allocmodule(store, module, externaddr*, val*) : (store, moduleinst)
def $allocmodule(s, module, externaddr*, val*) = (s_4, moduleinst)
  -- if module =
    MODULE
      (TYPE ft)*
      import*
      func^n_func
      (GLOBAL globaltype expr_1)^n_global
      (TABLE tabletype)^n_table
      (MEMORY memtype)^n_mem
      elem*
      data*
      start?
      export*
  -- if fa_ex* = $funcs(externaddr*)
  -- if ga_ex* = $globals(externaddr*)
  -- if ta_ex* = $tables(externaddr*)
  -- if ma_ex* = $mems(externaddr*)
  -- if fa* = $(|s.FUNCS|+i_func)^(i_func<n_func)
  -- if ga* = $(|s.GLOBALS|+i_global)^(i_global<n_global)
  -- if ta* = $(|s.TABLES|+i_table)^(i_table<n_table)
  -- if ma* = $(|s.MEMS|+i_mem)^(i_mem<n_mem)
  -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
  -- if moduleinst = {
      TYPES ft*,
      FUNCS fa_ex* fa*,
      GLOBALS ga_ex* ga*,
      TABLES ta_ex* ta*,
      MEMS ma_ex* ma*,
      EXPORTS xi*
    }
  -- if (s_1, fa*) = $allocfuncs(s, moduleinst, func^n_func)
  -- if (s_2, ga*) = $allocglobals(s_1, globaltype^n_global, val*)
  -- if (s_3, ta*) = $alloctables(s_2, tabletype^n_table)
  -- if (s_4, ma*) = $allocmems(s_3, memtype^n_mem)


;;
;; Instantiation
;;

def $initelem(store, moduleinst, u32*, (funcaddr*)*) : store
def $initelem(s, moduleinst, eps, eps) = s
def $initelem(s, moduleinst, i i'*, (a*) (a'*)*) = s_2
  -- if s_1 = s[.TABLES[moduleinst.TABLES[0]].REFS[i:|a*|] = a*]
  -- if s_2 = $initelem(s_1, moduleinst, i'*, (a'*)*)

def $initdata(store, moduleinst, u32*, (byte*)*) : store
def $initdata(s, moduleinst, eps, eps) = s
def $initdata(s, moduleinst, i i'*, (b*) (b'*)*) = s_2
  -- if s_1 = s[.MEMS[moduleinst.MEMS[0]].BYTES[i:|b*|] = b*]
  -- if s_2 = $initdata(s_1, moduleinst, i'*, (b'*)*)

def $instantiate(store, module, externaddr*) : config
def $instantiate(s, module, externaddr*) = s_3; f; (CALL x')?
  -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
  -- if type* = (TYPE functype)*
  -- if global* = (GLOBAL globaltype expr_G)*
  -- if elem* = (ELEM expr_E x*)*
  -- if data* = (DATA expr_D b*)*
  -- if start? = (START x')?
  -- if n_F = |func*|
  -- if moduleinst_init = {
      TYPES functype*,
      FUNCS $funcs(externaddr*) $(|s.FUNCS|+i_F)^(i_F<n_F),
      GLOBALS $globals(externaddr*)
    }
  -- if f_init = { MODULE moduleinst_init }
  -- if z = s; f_init
  -- (Eval_expr : z; expr_G ~>* z; val)*
  -- (Eval_expr : z; expr_E ~>* z; (CONST I32 i_E))*
  -- (Eval_expr : z; expr_D ~>* z; (CONST I32 i_D))*
  -- if (s_1, moduleinst) = $allocmodule(s, module, externaddr*, val*)
  -- if s_2 = $initelem(s_1, moduleinst, i_E*, moduleinst.FUNCS[x]**)
  -- if s_3 = $initdata(s_2, moduleinst, i_D*, b**)
  -- if f = { MODULE moduleinst }


;;
;; Invocation
;;

def $invoke(store, funcaddr, val*) : config
def $invoke(s, fa, val^n) = s; f; val^n (CALL_ADDR fa)
  -- if f = { MODULE {} }
  -- if $funcinst((s; f))[fa].TYPE = t_1^n -> t_2*