[spec] Fix state for expression evaluation (#2078)

Author: rossberg

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}

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)?

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)?

spectec/doc/example/output/NanoWasm.pdf

@@ -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

spectec/src/il2al/animate.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' }

spectec/src/il2al/transpile.ml

@@ -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?`})