diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 05581d4e..735441d5 100644 --- a/document/core/valid/instructions.rst +++ b/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 ` like |DROP| and |SELECT|. * *stack-polymorphic*: - the entire (or most of the) :ref:`instruction type ` :math:`[t_1^\ast] \to [t_2^\ast]` of the instruction is unconstrained. + the entire (or most of the) :ref:`instruction type ` :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 ` 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 ` :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 ` describes a type checking :ref:`algorithm ` 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 ` type of the form :math:`[t_1^\ast] \to [t_2^\ast]`. +* The instruction is valid with any :ref:`valid ` 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 ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with any :ref:`valid ` type of the form :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`. +* Then the instruction is valid with any :ref:`valid ` 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,7 +1428,7 @@ Control Instructions * For all :math:`l_i` in :math:`l^\ast`, the result type :math:`[t^\ast]` :ref:`matches ` :math:`C.\CLABELS[l_i]`. -* Then the instruction is valid with any :ref:`valid ` type of the form :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`. +* Then the instruction is valid with any :ref:`valid ` type of the form :math:`[t_1^\ast~t^\ast~\I32] \toX{x^\ast} [t_2^\ast]`. .. math:: \frac{ @@ -1430,9 +1436,9 @@ Control Instructions \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 ` of :math:`C.\CRETURN`. -* Then the instruction is valid with any :ref:`valid ` type of the form :math:`[t_1^\ast] \to [t_2^\ast]`. +* Then the instruction is valid with any :ref:`valid ` 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 ` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`. -* Then the instruction is valid with any :ref:`valid ` type :math:`[t_3^\ast~t_1^\ast] \to [t_4^\ast]`. +* Then the instruction is valid with any :ref:`valid ` 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 ` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`. -* Then the instruction is valid with any :ref:`valid ` type :math:`[t_3^\ast~t_1^\ast~(\REF~\NULL~x)] \to [t_4^\ast]`. +* Then the instruction is valid with any :ref:`valid ` 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 ` :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 ` :math:`t_3^\ast` and :math:`t_4^\ast`. +* Then the instruction is valid for any :ref:`valid ` 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:: diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 9c7437da..a7999424 100644 --- a/interpreter/valid/valid.ml +++ b/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,7 +413,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 -->... [], [] + ts1 -->... [], all_locals c | ReturnCallRef x -> let FuncT (ts1, ts2) as ft = func_type c x in @@ -418,7 +421,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 @ [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 diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md index eb32bc37..88363586 100644 --- a/proposals/function-references/Overview.md +++ b/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 ` + - `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. diff --git a/test/core/local_init.wast b/test/core/local_init.wast index 176ccc64..7acd3586 100644 --- a/test/core/local_init.wast +++ b/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))))