Fix spec (#50)

Wasm-DSL · Nov 30, 2023 · ec79d67 · ec79d67
1 parent d2966be
commit ec79d67
Show file tree

Hide file tree

Showing 7 changed files with 92 additions and 70 deletions.
diff --git a/spectec/spec/wasm-1.0/8-reduction.watsup b/spectec/spec/wasm-1.0/8-reduction.watsup
@@ -116,8 +116,7 @@ rule Step_read/call:
 rule Step_read/call_indirect-call:
   z; (CONST I32 i) (CALL_INDIRECT x)  ~>  (CALL_ADDR a)
   -- if $table(z, 0).ELEM[i] = a
-  -- if $funcinst(z)[a].CODE = FUNC x' (LOCAL t)* instr*
-  -- if $type(z, x) = $type(z, x')
+  -- if $type(z, x) = $funcinst(z)[a].TYPE
 
 rule Step_read/call_indirect-trap:
   z; (CONST I32 i) (CALL_INDIRECT x)  ~>  TRAP

diff --git a/spectec/spec/wasm-1.0/9-module.watsup b/spectec/spec/wasm-1.0/9-module.watsup
@@ -108,7 +108,7 @@ def $allocmodule(s, module, externval*, val*) = (s_4, mm)
   -- if ma* = $(|s.MEM|+i_mem)^(i_mem<n_mem)
   -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
   -- if mm = {
-      TYPE ft,
+      TYPE ft*,
       FUNC fa_ex* fa*,
       GLOBAL ga_ex* ga*,
       TABLE ta_ex* ta*,
@@ -129,31 +129,40 @@ def $concat_instr((instr*)*) : instr*
 def $concat_instr(epsilon) = epsilon
 def $concat_instr((instr*) (instr'*)*) = instr* $concat_instr((instr'*)*)
 
-def $initelem(store, tableaddr, u32*, (funcaddr*)*) : store
-def $initelem(s, ta, epsilon, epsilon) = s
-def $initelem(s, ta, i i'*, (a*) (a'*)*) = s[.TABLE[ta].ELEM[i:|a*|] = a*]
+def $initelem(store, moduleinst, u32*, (funcaddr*)*) : store
+def $initelem(s, mm, epsilon, epsilon) = s
+def $initelem(s, mm, i i'*, (a*) (a'*)*) = s_2
+  -- if s_1 = s[.TABLE[mm.TABLE[0]].ELEM[i:|a*|] = a*]
+  -- if s_2 = $initelem(s_1, mm, i'*, (a'*)*)
 
-def $initdata(store, memaddr, u32*, (byte*)*) : store
-def $initdata(s, ma, epsilon, epsilon) = s
-def $initdata(s, ma, i i'*, (b*) (b'*)*) = s[.MEM[ma].DATA[i:|b*|] = b*]
+def $initdata(store, moduleinst, u32*, (byte*)*) : store
+def $initdata(s, mm, epsilon, epsilon) = s
+def $initdata(s, mm, i i'*, (b*) (b'*)*) = s_2
+  -- if s_1 = s[.MEM[mm.MEM[0]].DATA[i:|b*|] = b*]
+  -- if s_2 = $initdata(s_1, mm, i'*, (b'*)*)
 
 def $instantiate(store, module, externval*) : config
-def $instantiate(s, module, externval*) = s'; f; (CALL x')?
+def $instantiate(s, module, externval*) = 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 mm_init = {TYPE functype*, FUNC $funcs(externval*), GLOBAL $globals(externval*)}
+  -- if n_F = |func*|
+  -- if mm_init = {
+      TYPE functype*,
+      FUNC $funcs(externval*) $(|s.FUNC|+i_F)^(i_F<n_F),
+      GLOBAL $globals(externval*)
+    }
   -- if f_init = { LOCAL epsilon, MODULE mm_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', mm) = $allocmodule(s, module, externval*, val*)
-  -- if s'' = $initelem(s', mm.TABLE[0], i_E*, mm.FUNC[x]**)
-  -- if s''' = $initdata(s'', mm.MEM[0], i_D*, b**)
+  -- if (s_1, mm) = $allocmodule(s, module, externval*, val*)
+  -- if s_2 = $initelem(s_1, mm, i_E*, mm.FUNC[x]**)
+  -- if s_3 = $initdata(s_2, mm, i_D*, b**)
   -- if f = { LOCAL epsilon, MODULE mm }
 
 

diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -122,8 +122,7 @@ rule Step_read/call:
 rule Step_read/call_indirect-call:
   z; (CONST I32 i) (CALL_INDIRECT x y)  ~>  (CALL_ADDR a)
   -- if $table(z, x).ELEM[i] = (REF.FUNC_ADDR a)
-  -- if $funcinst(z)[a].CODE = FUNC y' (LOCAL t)* instr*
-  -- if $type(z, y) = $type(z, y')
+  -- if $type(z, y) = $funcinst(z)[a].TYPE
 
 rule Step_read/call_indirect-trap:
   z; (CONST I32 i) (CALL_INDIRECT x y)  ~>  TRAP

diff --git a/spectec/spec/wasm-2.0/9-module.watsup b/spectec/spec/wasm-2.0/9-module.watsup
@@ -130,7 +130,7 @@ def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, mm)
   -- if da* = $(|s.DATA|+i_data)^(i_data<n_data)
   -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
   -- if mm = {
-      TYPE ft,
+      TYPE ft*,
       FUNC fa_ex* fa*,
       GLOBAL ga_ex* ga*,
       TABLE ta_ex* ta*,
@@ -175,9 +175,14 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)?
   -- if global* = (GLOBAL globaltype expr_G)*
   -- if elem* = (ELEM reftype expr_E* elemmode)*
   -- if start? = (START x)?
+  -- if n_F = |func*|
   -- if n_E = |elem*|
   -- if n_D = |data*|
-  -- if mm_init = {TYPE functype*, FUNC $funcs(externval*), GLOBAL $globals(externval*)}
+  -- if mm_init = {
+       TYPE functype*,
+       FUNC $funcs(externval*) $(|s.FUNC|+i_F)^(i_F<n_F),
+       GLOBAL $globals(externval*)
+     }
   -- if f_init = { LOCAL epsilon, MODULE mm_init }
   -- if z = s; f_init
   -- (Eval_expr : z; expr_G ~>* z; val)*

diff --git a/spectec/spec/wasm-3.0/9-module.watsup b/spectec/spec/wasm-3.0/9-module.watsup
@@ -148,16 +148,17 @@ def $rundata(DATA byte* (ACTIVE x instr*), y) =
 
 def $instantiate(store, module, externval*) : config
 def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)?
-  -- if module = MODULE type* import* func^n_func global* table* mem* elem* data* start? export*
+  -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if global* = (GLOBAL globaltype expr_G)*
   -- if table* = (TABLE tabletype expr_T)*
   -- if elem* = (ELEM reftype expr_E* elemmode)*
   -- if start? = (START x)?
+  -- if n_F = |func*|
   -- if n_E = |elem*|
   -- if n_D = |data*|
   -- if mm_init = {
       TYPE $alloctypes(type*),
-      FUNC $funcsxv(externval*) $(|s.FUNC|+i_func)^(i_func<n_func),
+      FUNC $funcsxv(externval*) $(|s.FUNC|+i_F)^(i_F<n_F),
       GLOBAL $globalsxv(externval*),
     }
   -- if z = s; { MODULE mm_init }

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
@@ -3912,16 +3912,17 @@ def rundata : (data, idx) -> instr*
 
 ;; 9-module.watsup:149.1-149.53
 def instantiate : (store, module, externval*) -> config
-  ;; 9-module.watsup:150.1-170.64
-  def {data* : data*, elem* : elem*, elemmode* : elemmode*, export* : export*, expr_E** : expr**, expr_G* : expr*, expr_T* : expr*, externval* : externval*, f : frame, func^n_func : func^n_func, global* : global*, globaltype* : globaltype*, i^n_E : nat^n_E, i_func^n_func : nat^n_func, import* : import*, instr_D* : instr*, instr_E* : instr*, j^n_D : nat^n_D, mem* : mem*, mm : moduleinst, mm_init : moduleinst, module : module, n_D : n, n_E : n, n_func : n, ref_E** : ref**, ref_T* : ref*, reftype* : reftype*, s : store, s' : store, start? : start?, table* : table*, tabletype* : tabletype*, type* : type*, val_G* : val*, x? : idx?, z : state} instantiate(s, module, externval*{externval}) = `%;%*`(`%;%`(s', f), (instr_E <: admininstr)*{instr_E} :: (instr_D <: admininstr)*{instr_D} :: CALL_admininstr(x)?{x})
-    -- if (module = `MODULE%*%*%*%*%*%*%*%*%*%*`(type*{type}, import*{import}, func^n_func{func}, global*{global}, table*{table}, mem*{mem}, elem*{elem}, data*{data}, start?{start}, export*{export}))
+  ;; 9-module.watsup:150.1-171.64
+  def {data* : data*, elem* : elem*, elemmode* : elemmode*, export* : export*, expr_E** : expr**, expr_G* : expr*, expr_T* : expr*, externval* : externval*, f : frame, func* : func*, global* : global*, globaltype* : globaltype*, i^n_E : nat^n_E, i_F^n_F : nat^n_F, import* : import*, instr_D* : instr*, instr_E* : instr*, j^n_D : nat^n_D, mem* : mem*, mm : moduleinst, mm_init : moduleinst, module : module, n_D : n, n_E : n, n_F : n, ref_E** : ref**, ref_T* : ref*, reftype* : reftype*, s : store, s' : store, start? : start?, table* : table*, tabletype* : tabletype*, type* : type*, val_G* : val*, x? : idx?, z : state} instantiate(s, module, externval*{externval}) = `%;%*`(`%;%`(s', f), (instr_E <: admininstr)*{instr_E} :: (instr_D <: admininstr)*{instr_D} :: CALL_admininstr(x)?{x})
+    -- if (module = `MODULE%*%*%*%*%*%*%*%*%*%*`(type*{type}, import*{import}, func*{func}, global*{global}, table*{table}, mem*{mem}, elem*{elem}, data*{data}, start?{start}, export*{export}))
     -- if (global*{global} = GLOBAL(globaltype, expr_G)*{expr_G globaltype})
     -- if (table*{table} = TABLE(tabletype, expr_T)*{expr_T tabletype})
     -- if (elem*{elem} = `ELEM%%*%`(reftype, expr_E*{expr_E}, elemmode)*{elemmode expr_E reftype})
     -- if (start?{start} = START(x)?{x})
+    -- if (n_F = |func*{func}|)
     -- if (n_E = |elem*{elem}|)
     -- if (n_D = |data*{data}|)
-    -- if (mm_init = {TYPE $alloctypes(type*{type}), FUNC $funcsxv(externval*{externval}) :: (|s.FUNC_store| + i_func)^(i_func<n_func){i_func}, GLOBAL $globalsxv(externval*{externval}), TABLE [], MEM [], ELEM [], DATA [], EXPORT []})
+    -- if (mm_init = {TYPE $alloctypes(type*{type}), FUNC $funcsxv(externval*{externval}) :: (|s.FUNC_store| + i_F)^(i_F<n_F){i_F}, GLOBAL $globalsxv(externval*{externval}), TABLE [], MEM [], ELEM [], DATA [], EXPORT []})
     -- if (z = `%;%`(s, {LOCAL [], MODULE mm_init}))
     -- (Eval_expr: `%;%~>*%;%*`(z, expr_G, z, [val_G]))*{expr_G val_G}
     -- (Eval_expr: `%;%~>*%;%*`(z, expr_T, z, [(ref_T <: val)]))*{expr_T ref_T}
@@ -3931,9 +3932,9 @@ def instantiate : (store, module, externval*) -> config
     -- if (instr_E*{instr_E} = $concat_instr($runelem(elem*{elem}[i], i)^(i<n_E){i}))
     -- if (instr_D*{instr_D} = $concat_instr($rundata(data*{data}[j], j)^(j<n_D){j}))
 
-;; 9-module.watsup:177.1-177.44
+;; 9-module.watsup:178.1-178.44
 def invoke : (store, funcaddr, val*) -> config
-  ;; 9-module.watsup:178.1-181.53
+  ;; 9-module.watsup:179.1-182.53
   def {expr : expr, f : frame, fa : funcaddr, local* : local*, n : n, s : store, t_1^n : valtype^n, t_2* : valtype*, val^n : val^n, x : idx} invoke(s, fa, val^n{val}) = `%;%*`(`%;%`(s, f), (val <: admininstr)^n{val} :: [REF.FUNC_ADDR_admininstr(fa) CALL_REF_admininstr(?(0))])
     -- if (f = {LOCAL [], MODULE {TYPE [], FUNC [], GLOBAL [], TABLE [], MEM [], ELEM [], DATA [], EXPORT []}})
     -- if ($funcinst(`%;%`(s, f))[fa].CODE_funcinst = `FUNC%%*%`(x, local*{local}, expr))
@@ -9038,16 +9039,17 @@ $$
 $$
 \begin{array}{@{}lcl@{}l@{}}
 {\mathrm{instantiate}}({\mathit{s}},\, {\mathit{module}},\, {{\mathit{externval}}^\ast}) &=& {\mathit{s}'} ; {\mathit{f}} ; {{\mathit{instr}}_{{\mathit{E}}}^\ast}~{{\mathit{instr}}_{{\mathsf{d}}}^\ast}~{(\mathsf{call}~{\mathit{x}})^?} &\quad
-  \mbox{if}~{\mathit{module}} = \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{{\mathit{n}}_{{\mathit{func}}}}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast} \\
+  \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} \\
  &&&\quad {\land}~{{\mathit{global}}^\ast} = {(\mathsf{global}~{\mathit{globaltype}}~{\mathit{expr}}_{{\mathsf{g}}})^\ast} \\
  &&&\quad {\land}~{{\mathit{table}}^\ast} = {(\mathsf{table}~{\mathit{tabletype}}~{\mathit{expr}}_{{\mathsf{t}}})^\ast} \\
  &&&\quad {\land}~{{\mathit{elem}}^\ast} = {(\mathsf{elem}~{\mathit{reftype}}~{{\mathit{expr}}_{{\mathit{E}}}^\ast}~{\mathit{elemmode}})^\ast} \\
  &&&\quad {\land}~{{\mathit{start}}^?} = {(\mathsf{start}~{\mathit{x}})^?} \\
+ &&&\quad {\land}~{\mathit{n}}_{{\mathsf{f}}} = {|{{\mathit{func}}^\ast}|} \\
  &&&\quad {\land}~{\mathit{n}}_{{\mathit{E}}} = {|{{\mathit{elem}}^\ast}|} \\
  &&&\quad {\land}~{\mathit{n}}_{{\mathsf{d}}} = {|{{\mathit{data}}^\ast}|} \\
  &&&\quad {\land}~{\mathit{mm}}_{{\mathit{init}}} = \{ \begin{array}[t]{@{}l@{}}
 \mathsf{type}~{\mathrm{alloctypes}}({{\mathit{type}}^\ast}),\; \\
-  \mathsf{func}~{\mathrm{funcs}}({{\mathit{externval}}^\ast})~{{|{\mathit{s}}.\mathsf{func}|} + {\mathit{i}}_{{\mathit{func}}}^{{\mathit{i}}_{{\mathit{func}}}<{\mathit{n}}_{{\mathit{func}}}}},\; \\
+  \mathsf{func}~{\mathrm{funcs}}({{\mathit{externval}}^\ast})~{{|{\mathit{s}}.\mathsf{func}|} + {\mathit{i}}_{{\mathsf{f}}}^{{\mathit{i}}_{{\mathsf{f}}}<{\mathit{n}}_{{\mathsf{f}}}}},\; \\
   \mathsf{global}~{\mathrm{globals}}({{\mathit{externval}}^\ast}),\; \\
    \}\end{array} \\
  &&&\quad {\land}~{\mathit{z}} = {\mathit{s}} ; \{ \begin{array}[t]{@{}l@{}}