diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 30cbc0a6e1..4303854465 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -182,6 +182,14 @@ $${definition: instantiate} where: +.. _eval-exprs: + +$${definition-prose: evalexprs} + +$${definition: evalexprs} + +and: + .. _eval-globals: $${definition-prose: evalglobals} diff --git a/specification/wasm-3.0/4.4-execution.modules.spectec b/specification/wasm-3.0/4.4-execution.modules.spectec index cd21223365..91b2c9b3f7 100644 --- a/specification/wasm-3.0/4.4-execution.modules.spectec +++ b/specification/wasm-3.0/4.4-execution.modules.spectec @@ -157,17 +157,31 @@ 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 $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%))) +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'*) +def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*) ---- - -- Eval_expr: z; expr ~>* z; val - -- if z = s; f + -- 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'*) + -- 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? +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)* @@ -184,11 +198,12 @@ def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* ins GLOBALS $globalsxa(externaddr*), FUNCS $funcsxa(externaddr*) ($(|s.FUNCS|+i_F))^(i_F<|func*|) \ } - -- if z = s; {MODULE moduleinst_0} ;; TODO(2, rossberg): inline + -- if z = s; {MODULE moduleinst_0} -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*) - -- (Eval_expr : z'; expr_T ~>* z'; ref_T)* - -- (Eval_expr : z'; expr_E ~>* z'; ref_E)** - -- if (s', moduleinst) = $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) + -- 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)? diff --git a/specification/wasm-latest/4.4-execution.modules.spectec b/specification/wasm-latest/4.4-execution.modules.spectec index cd21223365..91b2c9b3f7 100644 --- a/specification/wasm-latest/4.4-execution.modules.spectec +++ b/specification/wasm-latest/4.4-execution.modules.spectec @@ -157,17 +157,31 @@ 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 $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%))) +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'*) +def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*) ---- - -- Eval_expr: z; expr ~>* z; val - -- if z = s; f + -- 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'*) + -- 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? +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)* @@ -184,11 +198,12 @@ def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* ins GLOBALS $globalsxa(externaddr*), FUNCS $funcsxa(externaddr*) ($(|s.FUNCS|+i_F))^(i_F<|func*|) \ } - -- if z = s; {MODULE moduleinst_0} ;; TODO(2, rossberg): inline + -- if z = s; {MODULE moduleinst_0} -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*) - -- (Eval_expr : z'; expr_T ~>* z'; ref_T)* - -- (Eval_expr : z'; expr_E ~>* z'; ref_E)** - -- if (s', moduleinst) = $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) + -- 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)? diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index ef5f391740..a720e239ba 100644 Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml index c13157538a..5308fefc99 100644 --- a/spectec/src/il2al/animate.ml +++ b/spectec/src/il2al/animate.ml @@ -243,7 +243,7 @@ let large_enough_subsets xs = let min = if n >= 2 then n-1 else n in List.filter ( fun ys -> min <= List.length ys ) yss -let (@@) f g x = f x @ g x +let (@@@) f g x = f x @ g x let is_not_lhs e = match e.it with | LenE _ | IterE (_, (ListN (_, Some _), _)) | DotE _ -> true @@ -262,7 +262,7 @@ let is_call e = match e.it with let subset_selector e = if is_not_lhs e then (fun _ -> []) - else if is_call e then singletons @@ group_arg e + else if is_call e then singletons @@@ group_arg e else if is_atomic_lhs e then wrap else large_enough_subsets @@ -294,13 +294,24 @@ let rec rows_of_prem vars len i p = let covering_vars = List.filter_map (index_of len vars) targets in [ Assign targets, p, [i] @ covering_vars ] | RulePr (_, _, _, { it = TupE args; _ }) -> - (* Assumpton: the only possible assigned-value is the last arg (i.e. ... |- lhs ) *) - let _, l = Util.Lib.List.split_last args in - let frees = (free_exp_list l) in - [ - Condition, p, [i]; - Assign frees, p, [i] @ List.filter_map (index_of len vars) (free_exp_list l) - ] + (* Assumption: + * The only possible set of output variable + * is the last arg (i.e. ... |- lhs ) + * or the last two args (i.e. ... ~>* z; v) *) + let assign_last n = + if List.length args <= n then [] else + let outs, ins = Lib.List.split n (List.rev args) in + let free_exps es = es |> List.map (free_exp false) |> List.fold_left union empty in + let free_set = free_exps outs in + let bound_set = free_exps ins in + if not (disjoint free_set bound_set) then [] else + let frees = free_set.varid |> Set.elements in + [ Assign frees, p, [i] @ List.filter_map (index_of len vars) frees ] + in + + [ Condition, p, [i] ] + @ assign_last 1 + @ assign_last 2 | IterPr (p', iterexp) -> let p_r = rewrite_iterexp iterexp p' in let to_iter (tag, p, coverings) = tag, IterPr (recover_iterexp iterexp p, iterexp) $ p.at, coverings in @@ -342,7 +353,7 @@ let animate_prems known_vars prems = Error.error (over_region (List.map at unhandled_prems)) "prose translation" "There might be a cyclic binding" else snd !best' - | Some x -> x + | Some prems -> prems (* Animate rule *) let animate_rule r = match r.it with diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml index b343e16c04..94a2ec01cf 100644 --- a/spectec/src/il2al/transpile.ml +++ b/spectec/src/il2al/transpile.ml @@ -946,6 +946,7 @@ let hide_state_expr expr = | CallE (f, args) -> CallE (f, hide_state_args args) | TupE [ s; e ] when is_store s -> e.it | TupE [ z; e ] when is_state z -> e.it + | VarE id when is_state expr && String.starts_with ~prefix:"z" id -> VarE "z" | e -> e in { expr with it = expr' } diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index e3570fb28d..8466af4b89 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -7285,22 +7285,48 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr* ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec rec { -;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.94 +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92 +def $evalexprs(state : state, expr*) : (state, ref*) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34 + def $evalexprs{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-165.46 + def $evalexprs{z : state, expr : expr, `expr'*` : expr*, z'' : state, ref : ref, `ref'*` : ref*, z' : state}(z, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [ref] ++ ref'*{ref' <- `ref'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [(ref : ref <: val)]) + -- if ((z'', ref'*{ref' <- `ref'*`}) = $evalexprs(z', expr'*{expr' <- `expr'*`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96 +def $evalexprss(state : state, expr**) : (state, ref**) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35 + def $evalexprss{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-172.49 + def $evalexprss{z : state, `expr*` : expr*, `expr'**` : expr**, z'' : state, `ref*` : ref*, `ref'**` : ref**, z' : state}(z, [expr*{expr <- `expr*`}] ++ expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}) = (z'', [ref*{ref <- `ref*`}] ++ ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) + -- if ((z', ref*{ref <- `ref*`}) = $evalexprs(z, expr*{expr <- `expr*`})) + -- if ((z'', ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) = $evalexprss(z', expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.41 + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-167.81 - def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) - -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) - -- if (z = `%;%`_state(s, f)) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:176.1-181.82 + def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val]) + -- if (z' = `%;%`_state(s, f)) -- if ((s', a) = $allocglobal(s, gt, val)) - -- if ((z', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) + -- if ((z'', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) } ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec def $instantiate(store : store, module : module, externaddr*) : config ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec - def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, `ref_T*` : ref*, `ref_E**` : ref**, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) + def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`})) -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`} -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) @@ -7312,9 +7338,10 @@ def $instantiate(store : store, module : module, externaddr*) : config -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){}, DATAS [], ELEMS [], EXPORTS []}) -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0})) -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`})) - -- (Eval_expr: `%;%~>*%;%`(z', expr_T, z', [(ref_T : ref <: val)]))*{expr_T <- `expr_T*`, ref_T <- `ref_T*`} - -- (Eval_expr: `%;%~>*%;%`(z', expr_E, z', [(ref_E : ref <: val)]))*{expr_E <- `expr_E*`, ref_E <- `ref_E*`}*{`expr_E*` <- `expr_E**`, `ref_E*` <- `ref_E**`} - -- if ((s', moduleinst) = $allocmodule(s, module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`})) + -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`})) + -- if (z''' = `%;%`_state(s''', f)) + -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){})) -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){})) -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`}) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 710194603e..4a45e4ccff 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -11142,17 +11142,45 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lcl@{}l@{}} +{{{\mathrm{evalexpr}}^\ast}}{(z, \epsilon)} & = & (z, \epsilon) \\ +{{{\mathrm{evalexpr}}^\ast}}{(z, {\mathit{expr}}~{{\mathit{expr}'}^\ast})} & = & ({z''}, {\mathit{ref}}~{{\mathit{ref}'}^\ast}) & \\ +&& \multicolumn{2}{@{}l@{}}{\quad +\quad +\begin{array}[t]{@{}l@{}} +\mbox{if}~ z ; {\mathit{expr}} \hookrightarrow^\ast {z'} ; {\mathit{ref}} \\ +{\land}~ ({z''}, {{\mathit{ref}'}^\ast}) = {{{\mathrm{evalexpr}}^\ast}}{({z'}, {{\mathit{expr}'}^\ast})} \\ +\end{array} +} \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lcl@{}l@{}} +{{{{\mathrm{evalexpr}}^\ast}^\ast}}{(z, \epsilon)} & = & (z, \epsilon) \\ +{{{{\mathrm{evalexpr}}^\ast}^\ast}}{(z, {{\mathit{expr}}^\ast}~{{{\mathit{expr}'}^\ast}^\ast})} & = & ({z''}, {{\mathit{ref}}^\ast}~{{{\mathit{ref}'}^\ast}^\ast}) & \\ +&& \multicolumn{2}{@{}l@{}}{\quad +\quad +\begin{array}[t]{@{}l@{}} +\mbox{if}~ ({z'}, {{\mathit{ref}}^\ast}) = {{{\mathrm{evalexpr}}^\ast}}{(z, {{\mathit{expr}}^\ast})} \\ +{\land}~ ({z''}, {{{\mathit{ref}'}^\ast}^\ast}) = {{{{\mathrm{evalexpr}}^\ast}^\ast}}{({z'}, {{{\mathit{expr}'}^\ast}^\ast})} \\ +\end{array} +} \\ +\end{array} +$$ + $$ \begin{array}[t]{@{}lcl@{}l@{}} {{{\mathrm{evalglobal}}^\ast}}{(z, \epsilon, \epsilon)} & = & (z, \epsilon) \\ -{{{\mathrm{evalglobal}}^\ast}}{(z, {\mathit{gt}}~{{\mathit{gt}'}^\ast}, {\mathit{expr}}~{{\mathit{expr}'}^\ast})} & = & ({z'}, {\mathit{val}}~{{\mathit{val}'}^\ast}) & \\ +{{{\mathrm{evalglobal}}^\ast}}{(z, {\mathit{gt}}~{{\mathit{gt}'}^\ast}, {\mathit{expr}}~{{\mathit{expr}'}^\ast})} & = & ({z''}, {\mathit{val}}~{{\mathit{val}'}^\ast}) & \\ && \multicolumn{2}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} -\mbox{if}~ z ; {\mathit{expr}} \hookrightarrow^\ast z ; {\mathit{val}} \\ -{\land}~ z = s ; f \\ +\mbox{if}~ z ; {\mathit{expr}} \hookrightarrow^\ast {z'} ; {\mathit{val}} \\ +{\land}~ {z'} = s ; f \\ {\land}~ ({s'}, a) = {\mathrm{allocglobal}}(s, {\mathit{gt}}, {\mathit{val}}) \\ -{\land}~ ({z'}, {{\mathit{val}'}^\ast}) = {{{\mathrm{evalglobal}}^\ast}}{(({s'} ; f{}[{.}\mathsf{module}{.}\mathsf{globals} \mathrel{{=}{\oplus}} a]), {{\mathit{gt}'}^\ast}, {{\mathit{expr}'}^\ast})} \\ +{\land}~ ({z''}, {{\mathit{val}'}^\ast}) = {{{\mathrm{evalglobal}}^\ast}}{(({s'} ; f{}[{.}\mathsf{module}{.}\mathsf{globals} \mathrel{{=}{\oplus}} a]), {{\mathit{gt}'}^\ast}, {{\mathit{expr}'}^\ast})} \\ \end{array} } \\ \end{array} @@ -11160,7 +11188,7 @@ $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{\mathrm{instantiate}}(s, {\mathit{module}}, {{\mathit{externaddr}}^\ast}) & = & {s'} ; \{ \mathsf{module}~{\mathit{moduleinst}} \} ; {{\mathit{instr}}_{\mathsf{e}}^\ast}~{{\mathit{instr}}_{\mathsf{d}}^\ast}~{{\mathit{instr}}_{\mathsf{s}}^?} & \\ +{\mathrm{instantiate}}(s, {\mathit{module}}, {{\mathit{externaddr}}^\ast}) & = & {s''''} ; \{ \mathsf{module}~{\mathit{moduleinst}} \} ; {{\mathit{instr}}_{\mathsf{e}}^\ast}~{{\mathit{instr}}_{\mathsf{d}}^\ast}~{{\mathit{instr}}_{\mathsf{s}}^?} & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} @@ -11178,9 +11206,10 @@ $$ \mathsf{funcs}~{\mathrm{funcs}}({{\mathit{externaddr}}^\ast})~{({|s{.}\mathsf{funcs}|} + i_{\mathsf{f}})^{i_{\mathsf{f}}<{|{{\mathit{func}}^\ast}|}}} \}\end{array} \\ {\land}~ z = s ; \{ \mathsf{module}~{\mathit{moduleinst}}_0 \} \\ {\land}~ ({z'}, {{\mathit{val}}_{\mathsf{g}}^\ast}) = {{{\mathrm{evalglobal}}^\ast}}{(z, {{\mathit{globaltype}}^\ast}, {{\mathit{expr}}_{\mathsf{g}}^\ast})} \\ -{\land}~ ({z'} ; {\mathit{expr}}_{\mathsf{t}} \hookrightarrow^\ast {z'} ; {\mathit{ref}}_{\mathsf{t}})^\ast \\ -{\land}~ {({z'} ; {\mathit{expr}}_{\mathsf{e}} \hookrightarrow^\ast {z'} ; {\mathit{ref}}_{\mathsf{e}})^\ast}^\ast \\ -{\land}~ ({s'}, {\mathit{moduleinst}}) = {\mathrm{allocmodule}}(s, {\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {({{\mathit{ref}}_{\mathsf{e}}^\ast})^\ast}) \\ +{\land}~ ({z''}, {{\mathit{ref}}_{\mathsf{t}}^\ast}) = {{{\mathrm{evalexpr}}^\ast}}{({z'}, {{\mathit{expr}}_{\mathsf{t}}^\ast})} \\ +{\land}~ ({z'''}, {{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast}) = {{{{\mathrm{evalexpr}}^\ast}^\ast}}{({z''}, {{{\mathit{expr}}_{\mathsf{e}}^\ast}^\ast})} \\ +{\land}~ {z'''} = {s'''} ; f \\ +{\land}~ ({s''''}, {\mathit{moduleinst}}) = {\mathrm{allocmodule}}({s'''}, {\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {({{\mathit{ref}}_{\mathsf{e}}^\ast})^\ast}) \\ {\land}~ {{\mathit{instr}}_{\mathsf{d}}^\ast} = {\bigoplus}\, {{{\mathrm{rundata}}}_{i_{\mathsf{d}}}({{\mathit{data}}^\ast}{}[i_{\mathsf{d}}])^{i_{\mathsf{d}}<{|{{\mathit{data}}^\ast}|}}} \\ {\land}~ {{\mathit{instr}}_{\mathsf{e}}^\ast} = {\bigoplus}\, {{{\mathrm{runelem}}}_{i_{\mathsf{e}}}({{\mathit{elem}}^\ast}{}[i_{\mathsf{e}}])^{i_{\mathsf{e}}<{|{{\mathit{elem}}^\ast}|}}} \\ {\land}~ {{\mathit{instr}}_{\mathsf{s}}^?} = {(\mathsf{call}~x)^?} \\ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 6a33a4e453..ce7873e553 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -7275,22 +7275,48 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr* ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec rec { -;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.94 +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92 +def $evalexprs(state : state, expr*) : (state, ref*) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34 + def $evalexprs{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-165.46 + def $evalexprs{z : state, expr : expr, `expr'*` : expr*, z'' : state, ref : ref, `ref'*` : ref*, z' : state}(z, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [ref] ++ ref'*{ref' <- `ref'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [(ref : ref <: val)]) + -- if ((z'', ref'*{ref' <- `ref'*`}) = $evalexprs(z', expr'*{expr' <- `expr'*`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96 +def $evalexprss(state : state, expr**) : (state, ref**) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35 + def $evalexprss{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-172.49 + def $evalexprss{z : state, `expr*` : expr*, `expr'**` : expr**, z'' : state, `ref*` : ref*, `ref'**` : ref**, z' : state}(z, [expr*{expr <- `expr*`}] ++ expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}) = (z'', [ref*{ref <- `ref*`}] ++ ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) + -- if ((z', ref*{ref <- `ref*`}) = $evalexprs(z, expr*{expr <- `expr*`})) + -- if ((z'', ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) = $evalexprss(z', expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.41 + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-167.81 - def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) - -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) - -- if (z = `%;%`_state(s, f)) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:176.1-181.82 + def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val]) + -- if (z' = `%;%`_state(s, f)) -- if ((s', a) = $allocglobal(s, gt, val)) - -- if ((z', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) + -- if ((z'', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) } ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec def $instantiate(store : store, module : module, externaddr*) : config ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec - def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, `ref_T*` : ref*, `ref_E**` : ref**, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) + def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`})) -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`} -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) @@ -7302,9 +7328,10 @@ def $instantiate(store : store, module : module, externaddr*) : config -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){}, DATAS [], ELEMS [], EXPORTS []}) -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0})) -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`})) - -- (Eval_expr: `%;%~>*%;%`(z', expr_T, z', [(ref_T : ref <: val)]))*{expr_T <- `expr_T*`, ref_T <- `ref_T*`} - -- (Eval_expr: `%;%~>*%;%`(z', expr_E, z', [(ref_E : ref <: val)]))*{expr_E <- `expr_E*`, ref_E <- `ref_E*`}*{`expr_E*` <- `expr_E**`, `ref_E*` <- `ref_E**`} - -- if ((s', moduleinst) = $allocmodule(s, module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`})) + -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`})) + -- if (z''' = `%;%`_state(s''', f)) + -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){})) -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){})) -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`}) @@ -18640,22 +18667,48 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr* ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec rec { -;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.94 +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92 +def $evalexprs(state : state, expr*) : (state, ref*) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34 + def $evalexprs{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-165.46 + def $evalexprs{z : state, expr : expr, `expr'*` : expr*, z'' : state, ref : ref, `ref'*` : ref*, z' : state}(z, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [ref] ++ ref'*{ref' <- `ref'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [(ref : ref <: val)]) + -- if ((z'', ref'*{ref' <- `ref'*`}) = $evalexprs(z', expr'*{expr' <- `expr'*`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96 +def $evalexprss(state : state, expr**) : (state, ref**) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35 + def $evalexprss{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-172.49 + def $evalexprss{z : state, `expr*` : expr*, `expr'**` : expr**, z'' : state, `ref*` : ref*, `ref'**` : ref**, z' : state}(z, [expr*{expr <- `expr*`}] ++ expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}) = (z'', [ref*{ref <- `ref*`}] ++ ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) + -- if ((z', ref*{ref <- `ref*`}) = $evalexprs(z, expr*{expr <- `expr*`})) + -- if ((z'', ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) = $evalexprss(z', expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.41 + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-167.81 - def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) - -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) - -- if (z = `%;%`_state(s, f)) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:176.1-181.82 + def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val]) + -- if (z' = `%;%`_state(s, f)) -- if ((s', a) = $allocglobal(s, gt, val)) - -- if ((z', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) + -- if ((z'', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) } ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec def $instantiate(store : store, module : module, externaddr*) : config ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec - def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, `ref_T*` : ref*, `ref_E**` : ref**, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) + def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`})) -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`} -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) @@ -18667,9 +18720,10 @@ def $instantiate(store : store, module : module, externaddr*) : config -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){}, DATAS [], ELEMS [], EXPORTS []}) -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0})) -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`})) - -- (Eval_expr: `%;%~>*%;%`(z', expr_T, z', [(ref_T : ref <: val)]))*{expr_T <- `expr_T*`, ref_T <- `ref_T*`} - -- (Eval_expr: `%;%~>*%;%`(z', expr_E, z', [(ref_E : ref <: val)]))*{expr_E <- `expr_E*`, ref_E <- `ref_E*`}*{`expr_E*` <- `expr_E**`, `ref_E*` <- `ref_E**`} - -- if ((s', moduleinst) = $allocmodule(s, module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`})) + -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`})) + -- if (z''' = `%;%`_state(s''', f)) + -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){})) -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){})) -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`}) @@ -30184,22 +30238,48 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr* ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec rec { -;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.94 +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92 +def $evalexprs(state : state, expr*) : (state, ref*) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34 + def $evalexprs{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-165.46 + def $evalexprs{z : state, expr : expr, `expr'*` : expr*, z'' : state, ref : ref, `ref'*` : ref*, z' : state}(z, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [ref] ++ ref'*{ref' <- `ref'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [(ref : ref <: val)]) + -- if ((z'', ref'*{ref' <- `ref'*`}) = $evalexprs(z', expr'*{expr' <- `expr'*`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96 +def $evalexprss(state : state, expr**) : (state, ref**) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35 + def $evalexprss{z : state}(z, []) = (z, []) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-172.49 + def $evalexprss{z : state, `expr*` : expr*, `expr'**` : expr**, z'' : state, `ref*` : ref*, `ref'**` : ref**, z' : state}(z, [expr*{expr <- `expr*`}] ++ expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}) = (z'', [ref*{ref <- `ref*`}] ++ ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) + -- if ((z', ref*{ref <- `ref*`}) = $evalexprs(z, expr*{expr <- `expr*`})) + -- if ((z'', ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) = $evalexprss(z', expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`})) +} + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec +rec { + +;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111 def $evalglobals(state : state, globaltype*, expr*) : (state, val*) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.41 + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41 def $evalglobals{z : state}(z, [], []) = (z, []) - ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-167.81 - def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`}) - -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val]) - -- if (z = `%;%`_state(s, f)) + ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:176.1-181.82 + def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`}) + -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val]) + -- if (z' = `%;%`_state(s, f)) -- if ((s', a) = $allocglobal(s, gt, val)) - -- if ((z', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) + -- if ((z'', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`})) } ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec def $instantiate(store : store, module : module, externaddr*) : config ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec - def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, `ref_T*` : ref*, `ref_E**` : ref**, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) + def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`})) -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`})) -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`} -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) @@ -30211,9 +30291,10 @@ def $instantiate(store : store, module : module, externaddr*) : config -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){}, DATAS [], ELEMS [], EXPORTS []}) -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0})) -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`})) - -- (Eval_expr: `%;%~>*%;%`(z', expr_T, z', [(ref_T : ref <: val)]))*{expr_T <- `expr_T*`, ref_T <- `ref_T*`} - -- (Eval_expr: `%;%~>*%;%`(z', expr_E, z', [(ref_E : ref <: val)]))*{expr_E <- `expr_E*`, ref_E <- `ref_E*`}*{`expr_E*` <- `expr_E**`, `ref_E*` <- `ref_E**`} - -- if ((s', moduleinst) = $allocmodule(s, module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) + -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`})) + -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`})) + -- if (z''' = `%;%`_state(s''', f)) + -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`})) -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){})) -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){})) -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`}) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index f18397976a..ea9df342d5 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -26359,6 +26359,40 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Return :math:`{{\mathit{instr}}^\ast}~(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~0)~(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~n)~(\mathsf{table{.}init}~y~x)~(\mathsf{elem{.}drop}~x)`. +:math:`{{{\mathrm{evalexpr}}^\ast}}{(z, {{\mathit{expr}''}^\ast})}` +................................................................... + + +1. If :math:`{{\mathit{expr}''}^\ast} = \epsilon`, then: + + a. Return :math:`\epsilon`. + +#. Let :math:`{\mathit{expr}}~{{\mathit{expr}'}^\ast}` be :math:`{{\mathit{expr}''}^\ast}`. + +#. Let :math:`{\mathit{ref}}` be the result of :ref:`evaluating ` :math:`{\mathit{expr}}` with state :math:`z`. + +#. Let :math:`{{\mathit{ref}'}^\ast}` be :math:`{{{\mathrm{evalexpr}}^\ast}}{(z, {{\mathit{expr}'}^\ast})}`. + +#. Return :math:`{\mathit{ref}}~{{\mathit{ref}'}^\ast}`. + + +:math:`{{{{\mathrm{evalexpr}}^\ast}^\ast}}{(z, {{\mathit{expr}''}^\ast})}` +.......................................................................... + + +1. If :math:`{{\mathit{expr}''}^\ast} = \epsilon`, then: + + a. Return :math:`\epsilon`. + +#. Let :math:`{{\mathit{expr}}^\ast}~{{{\mathit{expr}'}^\ast}^\ast}` be :math:`{{\mathit{expr}''}^\ast}`. + +#. Let :math:`{{\mathit{ref}}^\ast}` be :math:`{{{\mathrm{evalexpr}}^\ast}}{(z, {{\mathit{expr}}^\ast})}`. + +#. Let :math:`{{{\mathit{ref}'}^\ast}^\ast}` be :math:`{{{{\mathrm{evalexpr}}^\ast}^\ast}}{(z, {{{\mathit{expr}'}^\ast}^\ast})}`. + +#. Return :math:`{{\mathit{ref}}^\ast}~{{{\mathit{ref}'}^\ast}^\ast}`. + + :math:`{{{\mathrm{evalglobal}}^\ast}}{(z, {{\mathit{globaltype}}^\ast}, {{\mathit{expr}''}^\ast})}` ................................................................................................... @@ -26377,10 +26411,10 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Let :math:`{\mathit{gt}}~{{\mathit{gt}'}^\ast}` be :math:`{{\mathit{globaltype}}^\ast}`. - #. Let :math:`(s, f)` be the destructuring of :math:`z`. - #. Let :math:`{\mathit{val}}` be the result of :ref:`evaluating ` :math:`{\mathit{expr}}` with state :math:`z`. + #. Let :math:`(s, f)` be the destructuring of :math:`z`. + #. Let :math:`a` be :math:`{\mathrm{allocglobal}}(s, {\mathit{gt}}, {\mathit{val}})`. #. Append :math:`a` to :math:`f{.}\mathsf{module}{.}\mathsf{globals}`. @@ -26454,30 +26488,14 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Let :math:`{{\mathit{val}}_{\mathsf{g}}^\ast}` be :math:`{{{\mathrm{evalglobal}}^\ast}}{(z, {{\mathit{globaltype}}^\ast}, {{\mathit{expr}}_{\mathsf{g}}^\ast})}`. -#. Let :math:`{{\mathit{ref}}_{\mathsf{t}}^\ast}` be the reference value sequence :math:`\epsilon`. - -#. For each :math:`{\mathit{expr}}_{\mathsf{t}}` in :math:`{{\mathit{expr}}_{\mathsf{t}}^\ast}`, do: - - a. Let :math:`{\mathit{ref}}_{\mathsf{t}}` be the result of :ref:`evaluating ` :math:`{\mathit{expr}}_{\mathsf{t}}` with state :math:`z`. - - #. Append :math:`{\mathit{ref}}_{\mathsf{t}}` to :math:`{{\mathit{ref}}_{\mathsf{t}}^\ast}`. - -#. Let :math:`{{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast}` be the reference value sequence sequence :math:`\epsilon`. - -#. For each :math:`{{\mathit{expr}}_{\mathsf{e}}^\ast}` in :math:`{{{\mathit{expr}}_{\mathsf{e}}^\ast}^\ast}`, do: - - a. Let :math:`{{\mathit{ref}}_{\mathsf{e}}^\ast}` be the reference value sequence :math:`\epsilon`. - - #. For each :math:`{\mathit{expr}}_{\mathsf{e}}` in :math:`{{\mathit{expr}}_{\mathsf{e}}^\ast}`, do: - - 1) Let :math:`{\mathit{ref}}_{\mathsf{e}}` be the result of :ref:`evaluating ` :math:`{\mathit{expr}}_{\mathsf{e}}` with state :math:`z`. - - #) Append :math:`{\mathit{ref}}_{\mathsf{e}}` to :math:`{{\mathit{ref}}_{\mathsf{e}}^\ast}`. +#. Let :math:`{{\mathit{ref}}_{\mathsf{t}}^\ast}` be :math:`{{{\mathrm{evalexpr}}^\ast}}{(z, {{\mathit{expr}}_{\mathsf{t}}^\ast})}`. - #. Append :math:`{{\mathit{ref}}_{\mathsf{e}}^\ast}` to :math:`{{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast}`. +#. Let :math:`{{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast}` be :math:`{{{{\mathrm{evalexpr}}^\ast}^\ast}}{(z, {{{\mathit{expr}}_{\mathsf{e}}^\ast}^\ast})}`. #. Pop the :math:`\mathsf{frame}` from the stack. +#. Let :math:`(s, f)` be the destructuring of :math:`z`. + #. Let :math:`{\mathit{moduleinst}}` be :math:`{\mathrm{allocmodule}}(s, {\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast})`. #. Let :math:`{F'}` be the :math:`\mathsf{frame}` :math:`\{ \mathsf{module}~{\mathit{moduleinst}} \}`. @@ -32876,6 +32894,22 @@ runelem_ x (ELEM rt e^n elemmode) 4. Let (ACTIVE y instr*) be elemmode. 5. Return instr* :: [(I32.CONST 0), (I32.CONST n), (TABLE.INIT y x), (ELEM.DROP x)]. +evalexprs z expr''* +1. If (expr''* = []), then: + a. Return []. +2. Let [expr] :: expr'* be expr''*. +3. Let [ref] be $Eval_expr(z, expr). +4. Let ref'* be $evalexprs(z, expr'*). +5. Return [ref] :: ref'*. + +evalexprss z expr''* +1. If (expr''* = []), then: + a. Return []. +2. Let [expr*] :: expr'** be expr''*. +3. Let ref* be $evalexprs(z, expr*). +4. Let ref'** be $evalexprss(z, expr'**). +5. Return [ref*] :: ref'**. + evalglobals z globaltype* expr''* 1. If (expr''* = []), then: a. Assert: Due to validation, (globaltype* = []). @@ -32884,8 +32918,8 @@ evalglobals z globaltype* expr''* a. Let [expr] :: expr'* be expr''*. b. Assert: Due to validation, (|globaltype*| >= 1). c. Let [gt] :: gt'* be globaltype*. - d. Let (s, f) be z. - e. Let [val] be $Eval_expr(z, expr). + d. Let [val] be $Eval_expr(z, expr). + e. Let (s, f) be z. f. Let a be $allocglobal(s, gt, val). g. Append a to the f.MODULE.GLOBALS. h. Let val'* be $evalglobals((s, f), gt'*, expr'*). @@ -32916,28 +32950,20 @@ instantiate s module externaddr* 14. Let z be (s, { MODULE: moduleinst_0 }). 15. Push the frame (FRAME_ 0 { $frame(z) }) to the stack. 16. Let val_G* be $evalglobals(z, globaltype*, expr_G*). -17. Let ref_T* be []. -18. For each expr_T in expr_T*, do: - a. Let [ref_T] be $Eval_expr(z, expr_T). - b. Append ref_T to the ref_T*. -19. Let ref_E** be []. -20. For each expr_E* in expr_E**, do: - a. Let ref_E* be []. - b. For each expr_E in expr_E*, do: - 1) Let [ref_E] be $Eval_expr(z, expr_E). - 2) Append ref_E to the ref_E*. - c. Append ref_E* to the ref_E**. -21. Pop the frame (FRAME_ 0 { f }) from the stack. -22. Let moduleinst be $allocmodule(s, module, externaddr*, val_G*, ref_T*, ref_E**). -23. Push the frame (FRAME_ 0 { { MODULE: moduleinst } }) to the stack. -24. Execute the sequence instr_E*. -25. Execute the sequence instr_D*. -26. If start? is defined, then: +17. Let ref_T* be $evalexprs(z, expr_T*). +18. Let ref_E** be $evalexprss(z, expr_E**). +19. Pop the frame (FRAME_ 0 { f }) from the stack. +20. Let (s, f) be z. +21. Let moduleinst be $allocmodule(s, module, externaddr*, val_G*, ref_T*, ref_E**). +22. Push the frame (FRAME_ 0 { { MODULE: moduleinst } }) to the stack. +23. Execute the sequence instr_E*. +24. Execute the sequence instr_D*. +25. If start? is defined, then: a. Let ?((START x)) be start?. b. Let instr_S be (CALL x). c. Execute the instruction instr_S. -27. Pop the frame (FRAME_ 0 { { MODULE: moduleinst } }) from the stack. -28. Return moduleinst. +26. Pop the frame (FRAME_ 0 { { MODULE: moduleinst } }) from the stack. +27. Return moduleinst. invoke s funcaddr val* 1. Assert: Due to validation, $Expand(s.FUNCS[funcaddr].TYPE) is some ->. diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index d4902fb045..1b03a9fa19 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1531,6 +1531,8 @@ warning: definition `dots` was never spliced warning: definition `elem` was never spliced warning: definition `eleminst` was never spliced warning: definition `elemsd` was never spliced +warning: definition `evalexprs` was never spliced +warning: definition `evalexprss` was never spliced warning: definition `evalglobals` was never spliced warning: definition `exninst` was never spliced warning: definition `expanddt` was never spliced @@ -2404,6 +2406,8 @@ warning: definition prose `disjoint_` was never spliced warning: definition prose `elem` was never spliced warning: definition prose `eleminst` was never spliced warning: definition prose `elemsd` was never spliced +warning: definition prose `evalexprs` was never spliced +warning: definition prose `evalexprss` was never spliced warning: definition prose `evalglobals` was never spliced warning: definition prose `exninst` was never spliced warning: definition prose `expanddt` was never spliced