From 859de657a294dc2f46f731acef7b59fe2312c3a2 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 4 Jun 2024 11:46:01 +0200 Subject: [PATCH 1/2] Outline start function instructions --- spectec/spec/wasm-3.0/9-module.watsup | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/spec/wasm-3.0/9-module.watsup b/spectec/spec/wasm-3.0/9-module.watsup index 982e510da0..586666933e 100644 --- a/spectec/spec/wasm-3.0/9-module.watsup +++ b/spectec/spec/wasm-3.0/9-module.watsup @@ -149,7 +149,7 @@ def $rundata_(x, DATA b^n (ACTIVE y instr*)) = instr* (CONST I32 0) (CONST I32 n) (MEMORY.INIT y x) (DATA.DROP x) def $instantiate(store, module, externval*) : config -def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)? +def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* instr_S? ---- ---- ;; TODO: -- Module_ok: |- module : xt_I* -> xt_E* ;; TODO: -- (Externval_type: s |- externval : xt_I)* @@ -175,7 +175,7 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)? -- if f = {MODULE mm} ;; TODO: inline -- if instr_E* = $concat_(instr, $runelem_(i_E, elem*[i_E])^(i_E<|elem*|)) -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|)) - ;;-- if instr_S? = (CALL x)? ;; TODO: use above + -- if instr_S? = (CALL x)? ;; From 7e5b8d73faf2bbcb845d5207484f6846591b5fa3 Mon Sep 17 00:00:00 2001 From: Wonho Date: Wed, 5 Jun 2024 14:52:20 +0900 Subject: [PATCH 2/2] Generalize translating rhs with iter --- spectec/src/il2al/translate.ml | 25 +++++++++------- spectec/test-frontend/TEST.md | 3 +- spectec/test-latex/TEST.md | 3 +- spectec/test-middlend/TEST.md | 15 ++++++---- spectec/test-prose/TEST.md | 53 +++++++++++++++++----------------- 5 files changed, 55 insertions(+), 44 deletions(-) diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 299a98515e..2cf39188a6 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -349,18 +349,21 @@ let rec translate_rhs exp = | Il.CaseE ([{it = Atom "TRAP"; _}]::_, _) -> [ trapI () ~at:at ] (* Execute instrs * TODO: doing this based on variable name is too ad-hoc. Need smarter way. *) - | Il.IterE ({ it = VarE id; _ }, (Il.List, _)) - | Il.IterE ({ it = SubE ({ it = VarE id; _ }, _, _); _}, (Il.List, _)) + | Il.IterE ({ it = VarE id; _ }, (List, _)) + | Il.IterE ({ it = SubE ({ it = VarE id; _ }, _, _); _}, (List, _)) when String.starts_with ~prefix:"instr" id.it -> - [ executeseqI (translate_exp exp) ~at:at ] - | Il.IterE ({ it = CaseE ([{it = Atom "CALL"; _} as atom]::_, _); _ }, (Opt, [ (id, _) ])) -> - let new_name = varE (id.it ^ "_0") in - [ ifI (isDefinedE (varE id.it), - [ - letI (optE (Some new_name), varE id.it) ~at:at; - executeI (caseE (translate_atom atom, [ new_name ])) ~at:at - ], - []) ~at:at ] + [executeseqI (translate_exp exp) ~at:at ] + | Il.VarE id | Il.SubE ({ it = VarE id; _ }, _, _) + when String.starts_with ~prefix:"instr" id.it -> + [ executeI (translate_exp exp) ~at:at ] + | Il.IterE (_, (Opt, _)) -> + (* TODO: need AL expression for unwrapping option *) + let tmp_name = varE "instr_0" in + [ ifI ( + isDefinedE (translate_exp exp), + [ letI (optE (Some tmp_name), translate_exp exp) ~at:at; executeI tmp_name ], + [] + ) ~at:at ] (* Push *) | Il.SubE _ | CallE _ | IterE _ -> [ pushI (translate_exp exp) ~at:at ] | Il.CaseE ([{it = Atom id; _}]::_, _) when List.mem id [ diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 86eb824d0d..02cd3c8900 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -5702,7 +5702,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export})) -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype}) -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype}) @@ -5718,6 +5718,7 @@ def $instantiate(store : store, module : module, externval*) : config -- if (f = {LOCALS [], MODULE mm}) -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat})) -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat})) + -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx}) ;; 9-module.watsup def $invoke(store : store, funcaddr : funcaddr, val*) : config diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 7960de5221..6f41664361 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8078,7 +8078,7 @@ $$ $$ \begin{array}{@{}lcl@{}l@{}} -{\mathrm{instantiate}}(s, {\mathit{module}}, {{\mathit{externval}}^\ast}) &=& \multicolumn{2}{l@{}}{ {s'} ; f ; {{\mathit{instr}}_{\mathsf{e}}^\ast}~{{\mathit{instr}}_{\mathsf{d}}^\ast}~{(\mathsf{call}~x)^?} } \\ +{\mathrm{instantiate}}(s, {\mathit{module}}, {{\mathit{externval}}^\ast}) &=& \multicolumn{2}{l@{}}{ {s'} ; f ; {{\mathit{instr}}_{\mathsf{e}}^\ast}~{{\mathit{instr}}_{\mathsf{d}}^\ast}~{{\mathit{instr}}_{\mathsf{s}}^?} } \\ \multicolumn{4}{@{}l@{}}{\qquad\quad \mbox{if}~{\mathit{module}} = \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^\ast}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}} \\ \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{global}}^\ast} = {(\mathsf{global}~{\mathit{globaltype}}~{\mathit{expr}}_{\mathsf{g}})^\ast}} \\ \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{table}}^\ast} = {(\mathsf{table}~{\mathit{tabletype}}~{\mathit{expr}}_{\mathsf{t}})^\ast}} \\ @@ -8099,6 +8099,7 @@ $$ \mathsf{module}~{\mathit{mm}} \}\end{array}} \\ \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{e}}^\ast} = {\mathrm{concat}}({{{\mathrm{runelem}}}_{i_{\mathsf{e}}}({{\mathit{elem}}^\ast}{}[i_{\mathsf{e}}])^{i_{\mathsf{e}}<{|{{\mathit{elem}}^\ast}|}}})} \\ \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{d}}^\ast} = {\mathrm{concat}}({{{\mathrm{rundata}}}_{i_{\mathsf{d}}}({{\mathit{data}}^\ast}{}[i_{\mathsf{d}}])^{i_{\mathsf{d}}<{|{{\mathit{data}}^\ast}|}}})} \\ + \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{s}}^?} = {(\mathsf{call}~x)^?}} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index c984c3f257..5e0828ee57 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -5692,7 +5692,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export})) -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype}) -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype}) @@ -5708,6 +5708,7 @@ def $instantiate(store : store, module : module, externval*) : config -- if (f = {LOCALS [], MODULE mm}) -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat})) -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat})) + -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx}) ;; 9-module.watsup def $invoke(store : store, funcaddr : funcaddr, val*) : config @@ -11534,7 +11535,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export})) -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype}) -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype}) @@ -11550,6 +11551,7 @@ def $instantiate(store : store, module : module, externval*) : config -- if (f = {LOCALS [], MODULE mm}) -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat})) -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat})) + -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx}) ;; 9-module.watsup def $invoke(store : store, funcaddr : funcaddr, val*) : config @@ -17376,7 +17378,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export})) -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype}) -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype}) @@ -17392,6 +17394,7 @@ def $instantiate(store : store, module : module, externval*) : config -- if (f = {LOCALS [], MODULE mm}) -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat})) -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat})) + -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx}) ;; 9-module.watsup def $invoke(store : store, funcaddr : funcaddr, val*) : config @@ -23380,7 +23383,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export})) -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype}) -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype}) @@ -23396,6 +23399,7 @@ def $instantiate(store : store, module : module, externval*) : config -- if (f = {LOCALS [], MODULE mm}) -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat})) -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat})) + -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx}) ;; 9-module.watsup def $invoke(store : store, funcaddr : funcaddr, val*) : config @@ -29448,7 +29452,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr* ;; 9-module.watsup def $instantiate(store : store, module : module, externval*) : config ;; 9-module.watsup - def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, x? : idx?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: CALL_instr(x)?{x : funcidx}) + def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr}) -- where MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}) = module -- where instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat}) -- where instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat}) @@ -29458,6 +29462,7 @@ def $instantiate(store : store, module : module, externval*) : config -- where GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype} = global*{global : global} -- where TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype} = table*{table : table} -- where ELEM_elem(reftype, expr_E*{expr_E : expr}, elemmode)*{elemmode : elemmode, expr_E : expr, reftype : reftype} = elem*{elem : elem} + -- where instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx} -- where z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0}) -- (Eval_expr: `%;%~>*%;%`(z, expr_G, z, [val_G]))*{expr_G : expr, val_G : val} -- (Eval_expr: `%;%~>*%;%`(z, expr_T, z, [(ref_T : ref <: val)]))*{expr_T : expr, ref_T : ref} diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index a573c51e3e..7ba0b1a153 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -880,9 +880,9 @@ instantiate module externval* 23. Perform $initelem(mm, i_E*, mm.FUNCS[x]**). 24. Perform $initdata(mm, i_D*, b**). 25. Push the activation of f with arity 0 to the stack. -26. If x' is defined, then: - a. Let ?(x'_0) be x'. - b. Execute the instruction (CALL x'_0). +26. If (CALL x')? is defined, then: + a. Let ?(instr_0) be (CALL x')?. + b. Execute the instruction instr_0. 27. Pop the activation of f with arity 0 from the stack. 28. Return mm. @@ -2809,9 +2809,9 @@ instantiate module externval* 23. Push the activation of f with arity 0 to the stack. 24. Execute the sequence (instr_E*). 25. Execute the sequence (instr_D*). -26. If x is defined, then: - a. Let ?(x_0) be x. - b. Execute the instruction (CALL x_0). +26. If (CALL x)? is defined, then: + a. Let ?(instr_0) be (CALL x)?. + b. Execute the instruction instr_0. 27. Pop the activation of f with arity 0 from the stack. 28. Return mm. @@ -5860,26 +5860,27 @@ instantiate module externval* 7. Let (GLOBAL globaltype expr_G)* be global*. 8. Let (TABLE tabletype expr_T)* be table*. 9. Let (ELEM reftype expr_E* elemmode)* be elem*. -10. Let z be { LOCALS: []; MODULE: moduleinst_0; }. -11. Push the activation of z to the stack. -12. Let [val_G]* be $eval_expr(expr_G)*. -13. Pop the activation of z from the stack. -14. Push the activation of z to the stack. -15. Let [ref_T]* be $eval_expr(expr_T)*. -16. Pop the activation of z from the stack. -17. Push the activation of z to the stack. -18. Let [ref_E]** be $eval_expr(expr_E)**. -19. Pop the activation of z from the stack. -20. Let mm be $allocmodule(module, externval*, val_G*, ref_T*, ref_E**). -21. Let f be { LOCALS: []; MODULE: mm; }. -22. Push the activation of f with arity 0 to the stack. -23. Execute the sequence (instr_E*). -24. Execute the sequence (instr_D*). -25. If x is defined, then: - a. Let ?(x_0) be x. - b. Execute the instruction (CALL x_0). -26. Pop the activation of f with arity 0 from the stack. -27. Return mm. +10. Let instr_S? be (CALL x)?. +11. Let z be { LOCALS: []; MODULE: moduleinst_0; }. +12. Push the activation of z to the stack. +13. Let [val_G]* be $eval_expr(expr_G)*. +14. Pop the activation of z from the stack. +15. Push the activation of z to the stack. +16. Let [ref_T]* be $eval_expr(expr_T)*. +17. Pop the activation of z from the stack. +18. Push the activation of z to the stack. +19. Let [ref_E]** be $eval_expr(expr_E)**. +20. Pop the activation of z from the stack. +21. Let mm be $allocmodule(module, externval*, val_G*, ref_T*, ref_E**). +22. Let f be { LOCALS: []; MODULE: mm; }. +23. Push the activation of f with arity 0 to the stack. +24. Execute the sequence (instr_E*). +25. Execute the sequence (instr_D*). +26. If instr_S? is defined, then: + a. Let ?(instr_0) be instr_S?. + b. Execute the instruction instr_0. +27. Pop the activation of f with arity 0 from the stack. +28. Return mm. invoke funcaddr val* 1. Let f be { LOCALS: []; MODULE: { TYPES: []; FUNCS: []; GLOBALS: []; TABLES: []; MEMS: []; ELEMS: []; DATAS: []; EXPORTS: []; }; }.