Allow any set status with stack-polymorphism

document/core/valid/instructions.rst

@@ -30,7 +30,7 @@ Two degrees of polymorphism can be distinguished:
   That is the case for all :ref:`parametric instructions <valid-instr-parametric>` like |DROP| and |SELECT|.
 
 * *stack-polymorphic*:
-  the entire (or most of the) :ref:`instruction type <syntax-instrtype>` :math:`[t_1^\ast] \to [t_2^\ast]` of the instruction is unconstrained.
+  the entire (or most of the) :ref:`instruction type <syntax-instrtype>` :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]` of the instruction is unconstrained, and furthermore, any local may be considered set after this instruction.
   That is the case for all :ref:`control instructions <valid-instr-control>` that perform an *unconditional control transfer*, such as |UNREACHABLE|, |BR|, |BRTABLE|, and |RETURN|.
 
 In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
@@ -49,7 +49,7 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari
    are valid, with :math:`t` in the typing of |SELECT| being instantiated to |I32| or |F64|, respectively.
 
    The |UNREACHABLE| instruction is stack-polymorphic,
-   and hence valid with type :math:`[t_1^\ast] \to [t_2^\ast]` for any possible sequences of value types :math:`t_1^\ast` and :math:`t_2^\ast`.
+   and hence valid with type :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]` for any possible sequences of value types :math:`t_1^\ast` and :math:`t_2^\ast` and any sequence of :ref:`local indices <syntax-localidx>` :math:`x^\ast` defined in the current function.
    Consequently,
 
    .. math::
@@ -62,6 +62,12 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari
       \UNREACHABLE~~(\I64.\CONST~0)~~\I32.\ADD
 
    is invalid, because there is no possible type to pick for the |UNREACHABLE| instruction that would make the sequence well-typed.
+   Furthermore,
+
+   .. math::
+      \UNREACHABLE~~(\LOCALGET~1)
+
+   is valid, even if the local with index 1 has not been set before the |UNREACHABLE|.
 
 The :ref:`Appendix <algo-valid>` describes a type checking :ref:`algorithm <algo-valid>` that efficiently implements validation of instruction sequences as prescribed by the rules given here.
 
@@ -1257,13 +1263,13 @@ Control Instructions
 :math:`\UNREACHABLE`
 ....................
 
-* The instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast] \to [t_2^\ast]`.
+* The instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]`.
 
 .. math::
    \frac{
-     C \vdashinstrtype [t_1^\ast] \to [t_2^\ast] \ok
+     C \vdashinstrtype [t_1^\ast] \toX{x^\ast} [t_2^\ast] \ok
    }{
-     C \vdashinstr \UNREACHABLE : [t_1^\ast] \to [t_2^\ast]
+     C \vdashinstr \UNREACHABLE : [t_1^\ast] \toX{x^\ast} [t_2^\ast]
    }
 
 .. note::
@@ -1365,15 +1371,15 @@ Control Instructions
 
 * Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l]`.
 
-* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`.
+* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast] \toX{x^\ast} [t_2^\ast]`.
 
 .. math::
    \frac{
      C.\CLABELS[l] = [t^\ast]
      \qquad
-     C \vdashinstrtype [t_1^\ast~t^\ast] \to [t_2^\ast] \ok
+     C \vdashinstrtype [t_1^\ast~t^\ast] \toX{x^\ast} [t_2^\ast] \ok
    }{
-     C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast]
+     C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \toX{x^\ast} [t_2^\ast]
    }
 
 .. note::
@@ -1422,17 +1428,17 @@ Control Instructions
   * For all :math:`l_i` in :math:`l^\ast`,
     the result type :math:`[t^\ast]` :ref:`matches <match-resulttype>` :math:`C.\CLABELS[l_i]`.
 
-* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`.
+* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast~\I32] \toX{x^\ast} [t_2^\ast]`.
 
 .. math::
    \frac{
      (C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l])^\ast
      \qquad
      C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N]
      \qquad
-     C \vdashinstrtype [t_1^\ast~t^\ast~\I32] \to [t_2^\ast] \ok
+     C \vdashinstrtype [t_1^\ast~t^\ast~\I32] \toX{x^\ast} [t_2^\ast] \ok
    }{
-     C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^\ast~\I32] \to [t_2^\ast]
+     C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^\ast~\I32] \toX{x^\ast} [t_2^\ast]
    }
 
 .. note::
@@ -1500,15 +1506,15 @@ Control Instructions
 
 * Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` of :math:`C.\CRETURN`.
 
-* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast] \to [t_2^\ast]`.
+* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]`.
 
 .. math::
    \frac{
      C.\CRETURN = [t^\ast]
      \qquad
-     C \vdashinstrtype [t_1^\ast~t^\ast] \to [t_2^\ast] \ok
+     C \vdashinstrtype [t_1^\ast~t^\ast] \toX{x^\ast} [t_2^\ast] \ok
    }{
-     C \vdashinstr \RETURN : [t_1^\ast~t^\ast] \to [t_2^\ast]
+     C \vdashinstr \RETURN : [t_1^\ast~t^\ast] \toX{x^\ast} [t_2^\ast]
    }
 
 .. note::
@@ -1603,13 +1609,15 @@ Control Instructions
 
 * The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`.
 
-* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type :math:`[t_3^\ast~t_1^\ast] \to [t_4^\ast]`.
+* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type :math:`[t_3^\ast~t_1^\ast] \toX{{x'}^\ast} [t_4^\ast]`.
 
 .. math::
    \frac{
      C.\CFUNCS[x] = [t_1^\ast] \toF C.\CRETURN
+     \qquad
+     C \vdashinstrtype [t_3^\ast~t_1^\ast] \toX{{x'}^\ast} [t_4^\ast] \ok
    }{
-     C \vdashinstr \RETURNCALL~x : [t_3^\ast~t_1^\ast] \to [t_4^\ast]
+     C \vdashinstr \RETURNCALL~x : [t_3^\ast~t_1^\ast] \toX{{x'}^\ast} [t_4^\ast]
    }
 
 .. note::
@@ -1627,13 +1635,15 @@ Control Instructions
 
 * The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`.
 
-* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type :math:`[t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \to [t_4^\ast]`.
+* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type :math:`[t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \toX{{x'}^\ast} [t_4^\ast]`.
 
 .. math::
    \frac{
      C.\CTYPES[x] = [t_1^\ast] \toF C.\CRETURN
+     \qquad
+     C \vdashinstrtype [t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \toX{{x'}^\ast} [t_4^\ast] \ok
    }{
-     C \vdashinstr \CALLREF~x : [t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \to [t_4^\ast]
+     C \vdashinstr \CALLREF~x : [t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \toX{{x'}^\ast} [t_4^\ast]
    }
 
 .. note::
@@ -1659,15 +1669,17 @@ Control Instructions
 
 * The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`.
 
-* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.
+* Then the instruction is valid for any :ref:`valid <valid-instrtype>` type :math:`[t_3^\ast~t_1^\ast~\I32] \toX{{x'}^\ast} [t_4^\ast]`.
 
 .. math::
    \frac{
      C.\CTABLES[x] = \limits~\FUNCREF
      \qquad
      C.\CTYPES[y] = [t_1^\ast] \toF C.\CRETURN
+     \qquad
+     C \vdashinstrtype [t_1^\ast~(\REF~\NULL~x)] \toX{{x'}^\ast} [t_2^\ast] \ok
    }{
-     C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]
+     C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\I32] \toX{{x'}^\ast} [t_4^\ast]
    }
 
 .. note::

interpreter/valid/valid.ml

@@ -73,6 +73,9 @@ let refer category (s : Free.Set.t) x =
 
 let refer_func (c : context) x = refer "function" c.refs.Free.funcs x
 
+let all_locals (c : context) =
+  Lib.List32.mapi (fun i _ -> i @@ no_region) c.locals
+
 
 (* Types *)
 
@@ -319,7 +322,7 @@ let check_block_type (c : context) (bt : block_type) at : instr_type =
 let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_instr_type =
   match e.it with
   | Unreachable ->
-    [] -->... [], []
+    [] -->... [], all_locals c
 
   | Nop ->
     [] --> [], []
@@ -357,7 +360,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (ts1 @ [NumT I32T]) --> ts2, List.map (fun x -> x @@ e.at) xs
 
   | Br x ->
-    label c x -->... [], []
+    label c x -->... [], all_locals c
 
   | BrIf x ->
     (label c x @ [NumT I32T]) --> label c x, []
@@ -367,7 +370,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     let ts = List.init n (fun i -> peek (n - i) s) in
     check_stack c ts (label c x) x.at;
     List.iter (fun x' -> check_stack c ts (label c x') x'.at) xs;
-    (ts @ [NumT I32T]) -->... [], []
+    (ts @ [NumT I32T]) -->... [], all_locals c
 
   | BrOnNull x ->
     let (_, ht) = peek_ref 0 s e.at in
@@ -386,7 +389,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (ts0 @ [RefT (Null, ht)]) --> ts0, []
 
   | Return ->
-    c.results -->... [], []
+    c.results -->... [], all_locals c
 
   | Call x ->
     let FuncT (ts1, ts2) = func c x in
@@ -410,15 +413,15 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
       ("type mismatch: current function requires result type " ^
        string_of_result_type c.results ^
        " but callee returns " ^ string_of_result_type ts2);
-    ts1 -->... [], []
+    ts1 -->... [], all_locals c
 
   | ReturnCallRef x ->
     let FuncT (ts1, ts2) as ft = func_type c x in
     require (match_result_type ts2 c.results) e.at
       ("type mismatch: current function requires result type " ^
        string_of_result_type c.results ^
        " but callee returns " ^ string_of_result_type ts2);
-    (ts1 @ [RefT (Null, DefHT (DefFuncT ft))]) -->... [], []
+    (ts1 @ [RefT (Null, DefHT (DefFuncT ft))]) -->... [], all_locals c
 
   | ReturnCallIndirect (x, y) ->
     let TableT (_lim, t) = table c x in
@@ -427,7 +430,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
       ("type mismatch: current function requires result type " ^
        string_of_result_type c.results ^
        " but callee returns " ^ string_of_result_type ts2);
-    (ts1 @ [NumT I32T]) -->... [], []
+    (ts1 @ [NumT I32T]) -->... [], all_locals c
 
   | LocalGet x ->
     let LocalT (init, t) = local c x in

proposals/function-references/Overview.md

@@ -261,6 +261,22 @@ Typing of local instructions is updated to account for the initialization status
 Note: These typing rules do not try to exclude indices for locals that have already been set, but an implementation could.
 
 
+#### Stack-polymorphic Instructions
+
+All *stack-polymorphic* instructions allow assuming an arbitrary initialization status for locals present in the current function:
+
+* `unreachable`
+  - `unreachable : [t1*] -> [t2*] x*`
+    - iff `(x : set? t)*`
+
+* `br <labelidx>`
+  - `br $l : [t1* t*] -> [t2*] x*`
+    - iff `$l : t*`
+    - and `(x : set? t)*`
+
+and so on.
+
+
 #### Instruction Sequences
 
 Typing of instruction sequences is updated to account for initialization of locals.

test/core/local_init.wast

@@ -16,11 +16,23 @@
     (local.set $x (local.get $p))
     (block (result (ref extern)) (local.get $x))
   )
+
+  (func (export "get-after-br")
+    (local $x (ref extern))
+    (br 0)
+    (drop (local.get $x))
+  )
+  (func (export "get-after-unreachable")
+    (local $x (ref extern))
+    (unreachable)
+    (drop (local.get $x))
+  )
 )
 
 (assert_return (invoke "get-after-set" (ref.extern 1)) (ref.extern 1))
 (assert_return (invoke "get-after-tee" (ref.extern 2)) (ref.extern 2))
 (assert_return (invoke "get-in-block-after-set" (ref.extern 3)) (ref.extern 3))
+(assert_return (invoke "get-after-br"))
 
 (assert_invalid
   (module (func $uninit (local $x (ref extern)) (drop (local.get $x))))