diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 1fd7eecce1..10f6b25065 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -21,7 +21,10 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b Data Structures ~~~~~~~~~~~~~~~ -Types are representable as a set of enumerations. +Types +..... + +Value types are representable as a set of enumerations. .. code-block:: pseudo @@ -65,37 +68,64 @@ Equivalence and subtyping checks can be defined on these types. return matches_heap(t1.heap, t2.heap) && matches_null(t1.null, t2.null) func matches(t1 : val_type, t2 : val_type) : bool = - return - (is_num t1 && is_num t2 && t1 = t2) || - (is_vec t1 && is_vec t2 && t1 = t2) || - (is_ref t1 && is_ref t2 && matches_ref(t1, t2)) || - t1 = Bot + switch (t1, t2) + case (Ref(_), Ref(_)) + return matches_ref(t1, t2) + case (Bot, _) + return true + case (_, _) + return t1 = t2 + +Context +....... + +Validation requires a :ref:`context ` for checking uses of :ref:`indices `. +For the purpose of presenting the algorithm, it is maintained in a set of global variables: + +.. code-block:: pseudo + + var locals : array(val_type) + var locals_init : array(bool) + var globals : array(global_type) + var funcs : array(func_type) + var tables : array(table_type) + var mems : array(mem_type) + +This assumes suitable representations for the various :ref:`types ` besides :code:`val_type`, which are omitted here. + +For locals, there is an additional array recording the initialization status of each local. + +Stacks +...... -The algorithm uses two separate stacks: the *value stack* and the *control stack*. -The former tracks the :ref:`types ` of operand values on the :ref:`stack `, -the latter surrounding :ref:`structured control instructions ` and their associated :ref:`blocks `. +The algorithm uses three separate stacks: the *value stack*, the *control stack*, and the *initialization stack*. +The value stack tracks the :ref:`types ` of operand values on the :ref:`stack `. +The control stack tracks surrounding :ref:`structured control instructions ` and their associated :ref:`blocks `. +The initialization stack records all :ref:`locals ` that have been initialized since the beginning of the function. .. code-block:: pseudo type val_stack = stack(val_type) + type init_stack = stack(u32) type ctrl_stack = stack(ctrl_frame) type ctrl_frame = { opcode : opcode start_types : list(val_type) end_types : list(val_type) - height : nat + val_height : nat + init_height : nat unreachable : bool } -For each value, the value stack records its :ref:`value type `. -For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic ` typing after branches). +For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), the height of the initialization stack at the start of the block (used to reset initialization status at the end of the block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic ` typing after branches). -For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables: +For the purpose of presenting the algorithm, these stacks are simply maintained as global variables: .. code-block:: pseudo var vals : val_stack + var inits : init_stack var ctrls : ctrl_stack However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions: @@ -123,7 +153,7 @@ However, these variables are not manipulated directly by the main checking funct func pop_ref() : ref_type = let actual = pop_val() error_if(not is_ref(actual)) - if actual = Bot then return Ref(Bot, false) + if (actual = Bot) return Ref(Bot, false) return actual func push_vals(types : list(val_type)) = foreach (t in types) push_val(t) @@ -150,12 +180,35 @@ Finally, there are accumulative functions for pushing or popping multiple operan so that, e.g., :code:`ctrls[0]` accesses the element pushed last. +The initialization stack and the initialization status of locals is manipulated through the following functions: + +.. code-block:: pseudo + + func get_local(idx : u32) = + error_if(not (locals_init[idx] || ctrls[0].unreachable)) + + func set_local(idx : u32) = + if (not locals_init[idx]) + inits.push(idx) + locals_init[idx] := true + + func reset_locals(height : nat) = + while (inits.size() > height) + locals_init[inits.pop()] := false + +Getting a local verifies that it is either known to be initialized, or that that the operation is unreachable in the current stack frame. +When a local is set that was not set already, +then its initialization status is updated and the change is recorded in the initialization stack. +Thus, the initialization status of all locals can be reset to a previous state by denoting a specific height in the initialization stack. + +The size of the initialization stack is bounded by the number of (non-defaultable) locals in a function, so can be preallocated by an algorithm. + The control stack is likewise manipulated through auxiliary functions: .. code-block:: pseudo func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) = - let frame = ctrl_frame(opcode, in, out, vals.size(), false) + let frame = ctrl_frame(opcode, in, out, vals.size(), inits.size(), false) ctrls.push(frame) push_vals(in) @@ -163,12 +216,13 @@ The control stack is likewise manipulated through auxiliary functions: error_if(ctrls.is_empty()) let frame = ctrls[0] pop_vals(frame.end_types) - error_if(vals.size() =/= frame.height) + error_if(vals.size() =/= frame.val_height) + reset_locals(frame.init_height) ctrls.pop() return frame func label_types(frame : ctrl_frame) : list(val_types) = - return (if frame.opcode == loop then frame.start_types else frame.end_types) + return (if (frame.opcode = loop) frame.start_types else frame.end_types) func unreachable() = vals.resize(ctrls[0].height) @@ -180,6 +234,7 @@ It allocates a new frame record recording them along with the current height of Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it checks that the stack has shrunk back to its initial height. +Finally, it undoes all changes to the initialization status of locals that happend inside the block. The type of the :ref:`label ` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. @@ -192,6 +247,7 @@ In that case, all existing operand types are purged from the value stack, in ord However, a polymorphic stack cannot underflow, but instead generates :code:`Bot` types as needed. + .. index:: opcode Validation of Opcode Sequences @@ -200,10 +256,6 @@ Validation of Opcode Sequences The following function shows the validation of a number of representative instructions that manipulate the stack. Other instructions are checked in a similar manner. -.. note:: - Various instructions not shown here will additionally require the presence of a validation :ref:`context ` for checking uses of :ref:`indices `. - That is an easy addition and therefore omitted from this presentation. - .. code-block:: pseudo func validate(opcode) = @@ -222,7 +274,7 @@ Other instructions are checked in a similar manner. let t2 = pop_val() error_if(not (is_num(t1) && is_num(t2) || is_vec(t1) && is_vec(t2))) error_if(t1 =/= t2 && t1 =/= Bot && t2 =/= Bot) - push_val(if (t1 == Bot) t2 else t1) + push_val(if (t1 = Bot) t2 else t1) case (select t) pop_val(I32) @@ -238,6 +290,14 @@ Other instructions are checked in a similar manner. let rt = pop_ref() push_val(Ref(rt.heap, false)) + case (local.get x) + get_local(x) + push_val(locals[x]) + + case (local.set x) + pop_val(locals[x]) + set_local(x) + case (unreachable) unreachable() @@ -296,7 +356,7 @@ Other instructions are checked in a similar manner. let rt = pop_ref() if (rt.heap =/= Bot) error_if(not is_def(rt.heap)) - let ft = lookup_func_type(rt.heap.idx) // TODO + let ft = funcs[rt.heap.idx] pop_vals(ft.params) push_vals(ft.results) diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index 339cb25f9d..710d574bcb 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -138,6 +138,17 @@ Added vector type and instructions that manipulate multiple numeric values in pa * New injection/projection :ref:`vector instructions `: :math:`\K{i}\!N\!\K{x}\!M\!\K{.splat}`, :math:`\K{f}\!N\!\K{x}\!M\!\K{.splat}`, :math:`\K{i}\!N\!\K{x}\!M\!\K{.bitmask}` +Release 2.1 +~~~~~~~~~~~ + +.. index:: reference + +Typeful References +.................. + +.. todo:: describe + + .. [#proposal-signext] https://github.com/WebAssembly/spec/tree/main/proposals/sign-extension-ops/ diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 7551421845..3a21e3c94e 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -14,8 +14,14 @@ Typing of Static Constructs Construct Judgement =============================================== =============================================================================== :ref:`Limits ` :math:`C \vdashlimits \limits : k` +:ref:`Numeric type ` :math:`C \vdashnumtype \numtype \ok` +:ref:`Vector type ` :math:`C \vdashvectype \vectype \ok` +:ref:`Heap type ` :math:`C \vdashheaptype \heaptype \ok` +:ref:`Reference type ` :math:`C \vdashreftype \reftype \ok` +:ref:`Value type ` :math:`C \vdashvaltype \valtype \ok` :ref:`Function type ` :math:`C \vdashfunctype \functype \ok` -:ref:`Block type ` :math:`C \vdashblocktype \blocktype \ok` +:ref:`Block type ` :math:`C \vdashblocktype \blocktype : \instrtype` +:ref:`Instruction type ` :math:`C \vdashinstrtype \instrtype \ok` :ref:`Table type ` :math:`C \vdashtabletype \tabletype \ok` :ref:`Memory type ` :math:`C \vdashmemtype \memtype \ok` :ref:`Global type ` :math:`C \vdashglobaltype \globaltype \ok` @@ -24,6 +30,7 @@ Construct Judgement :ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` :ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` :ref:`Function ` :math:`C \vdashfunc \func : \functype` +:ref:`Local ` :math:`C \vdashlocal \local : \localtype` :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` @@ -66,6 +73,16 @@ Construct Judgement =============================================== =============================================================================== +Defaultability +~~~~~~~~~~~~~~ + +================================================= =============================================================================== +Construct Judgement +================================================= =============================================================================== +:ref:`Defaultable value type ` :math:`C \vdashvaltypedefaultable \valtype \defaultable` +================================================= =============================================================================== + + Constantness ~~~~~~~~~~~~ diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index e9c72b61a5..6070144119 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -405,15 +405,15 @@ denoting *count* locals of the same value type. \X{size}{:}\Bu32~~\X{code}{:}\Bfunc &\Rightarrow& \X{code} & (\iff \X{size} = ||\Bfunc||) \\ \production{function} & \Bfunc &::=& - (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr - &\Rightarrow& \concat((t^\ast)^\ast), e - & (\iff |\concat((t^\ast)^\ast)| < 2^{32}) \\ + (\local^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr + &\Rightarrow& \concat((\local^\ast)^\ast), e + & (\iff |\concat((\local^\ast)^\ast)| < 2^{32}) \\ \production{locals} & \Blocals &::=& - n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& t^n \\ + n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& \{ \LTYPE~t \}^n \\ \end{array} Here, :math:`\X{code}` ranges over pairs :math:`(\valtype^\ast, \expr)`. -The meta function :math:`\concat((t^\ast)^\ast)` concatenates all sequences :math:`t_i^\ast` in :math:`(t^\ast)^\ast`. +The meta function :math:`\concat((\local^\ast)^\ast)` concatenates all sequences :math:`\local_i^\ast` in :math:`(\local^\ast)^\ast`. Any code for which the length of the resulting sequence is out of bounds of the maximum size of a :ref:`vector ` is malformed. .. note:: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 57ff1a5f1c..0c94ae6cff 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1043,7 +1043,7 @@ Variable Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\ALOCALS[x]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\ALOCALS[x]` exists and is non-empty. 3. Let :math:`\val` be the value :math:`F.\ALOCALS[x]`. @@ -3007,7 +3007,7 @@ Invocation of :ref:`function address ` :math:`a` 3. Let :math:`[t_1^n] \to [t_2^m]` be the :ref:`function type ` :math:`f.\FITYPE`. -4. Let :math:`t^\ast` be the list of :ref:`value types ` :math:`f.\FICODE.\FLOCALS`. +4. Let :math:`\local^\ast` be the list of :ref:`locals ` :math:`f.\FICODE.\FLOCALS`. 5. Let :math:`\instr^\ast~\END` be the :ref:`expression ` :math:`f.\FICODE.\FBODY`. @@ -3015,15 +3015,13 @@ Invocation of :ref:`function address ` :math:`a` 7. Pop the values :math:`\val^n` from the stack. -8. Let :math:`\val_0^\ast` be the list of zero values of types :math:`t^\ast`. +8. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. -9. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. +9. Push the activation of :math:`F` with arity :math:`m` to the stack. -10. Push the activation of :math:`F` with arity :math:`m` to the stack. +10. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. -11. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. - -12. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L`. +11. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L`. .. math:: ~\\[-1ex] @@ -3035,11 +3033,14 @@ Invocation of :ref:`function address ` :math:`a` \begin{array}[t]{@{}r@{~}l@{}} (\iff & S.\SFUNCS[a] = f \\ \wedge & f.\FITYPE = [t_1^n] \to [t_2^m] \\ - \wedge & f.\FICODE = \{ \FTYPE~x, \FLOCALS~t^k, \FBODY~\instr^\ast~\END \} \\ + \wedge & f.\FICODE = \{ \FTYPE~x, \FLOCALS~\{\LTYPE~t\}^k, \FBODY~\instr^\ast~\END \} \\ \wedge & F = \{ \AMODULE~f.\FIMODULE, ~\ALOCALS~\val^n~(\default_t)^k \}) \end{array} \\ \end{array} +.. note:: + For non-defaultable types, the respective local is left uninitialized by these rules. + .. _exec-invoke-exit: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 50cb93e056..869d197eb5 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -51,14 +51,16 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre .. _default-val: -Each :ref:`value type ` has an associated *default value*; -it is the respective value :math:`0` for :ref:`number types `, :math:`0` for :ref:`vector types `, and null for :ref:`reference types `. +:ref:`Value types ` can have an associated *default value*; +it is the respective value :math:`0` for :ref:`number types `, :math:`0` for :ref:`vector types `, and null for nullable :ref:`reference types `. +For other references, no default value is defined, :math:`\default_t` hence is an optional value :math:`\val^?`. .. math:: \begin{array}{lcl@{\qquad}l} \default_t &=& t{.}\CONST~0 & (\iff t = \numtype) \\ \default_t &=& t{.}\CONST~0 & (\iff t = \vectype) \\ \default_t &=& \REFNULL~t & (\iff t = (\REF~\NULL~\heaptype)) \\ + \default_t &=& \epsilon & (\iff t = (\REF~\heaptype)) \\ \end{array} @@ -493,10 +495,11 @@ and a reference to the function's own :ref:`module instance ` \production{(activation)} & \X{activation} &::=& \FRAME_n\{\frame\} \\ \production{(frame)} & \frame &::=& - \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ + \{ \ALOCALS~(\val^?)^\ast, \AMODULE~\moduleinst \} \\ \end{array} -The values of the locals are mutated by respective :ref:`variable instructions `. +Locals may be uninitialized, in which case they are empty. +Locals are mutated by respective :ref:`variable instructions `. .. _exec-expand: diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index f51a504f0c..29a598aa8c 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -142,7 +142,9 @@ The |MFUNCS| component of a module defines a vector of *functions* with the foll .. math:: \begin{array}{llll} \production{function} & \func &::=& - \{ \FTYPE~\typeidx, \FLOCALS~\vec(\valtype), \FBODY~\expr \} \\ + \{ \FTYPE~\typeidx, \FLOCALS~\vec(\local), \FBODY~\expr \} \\ + \production{local} & \local &::=& + \{ \LTYPE~\valtype \} \\ \end{array} The |FTYPE| of a function declares its signature by reference to a :ref:`type ` defined in the module. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index bf264d39cf..818d7d9485 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -167,6 +167,55 @@ which is a sequence of values, written with brackets. \end{array} +.. index:: ! instruction type, value type, result type, instruction, local, local index + pair: abstract syntax; instruction type + pair: instruction; type +.. _syntax-instrtype: + +Instruction Types +~~~~~~~~~~~~~~~~~ + +*Instruction types* classify the behaviour of :ref:`instructions ` or instruction sequences, by describing how they manipulate the :ref:`operand stack ` and the initialization status of :ref:`locals `: + +.. math:: + \begin{array}{llll} + \production{instruction type} & \instrtype &::=& + \resulttype \to_{\localidx^\ast} \resulttype \\ + \end{array} + +An instruction type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` describes the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off +and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back. +Moreover, it enumerates the :ref:`indices ` :math:`x^\ast` of locals that have been set by the instruction or sequence. + +.. note:: + Instruction types are only used for :ref:`validation `, + they do not occur in programs. + + +.. index:: ! local type, value type, local, local index + pair: abstract syntax; local type + pair: local; type +.. _syntax-init: +.. _syntax-localtype: + +Local Types +~~~~~~~~~~~ + +*Local types* classify :ref:`locals `, by describing their :ref:`value type ` as well as their *initialization status*: + +.. math:: + \begin{array}{llll} + \production{(initialization status)} & \init &::=& + \SET ~|~ \UNSET \\ + \production{(local type)} & \localtype &::=& + \init~\valtype \\ + \end{array} + +.. note:: + Local types are only used for :ref:`validation `, + they do not occur in programs. + + .. index:: ! function type, value type, vector, function, parameter, result, result type pair: abstract syntax; function type pair: function; type diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 61e419246b..84aaf11381 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -198,12 +198,12 @@ Function definitions can bind a symbolic :ref:`function identifier `, a \begin{array}{llclll} \production{function} & \Tfunc_I &::=& \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~~ - (t{:}\Tlocal_I)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad + (\X{loc}{:}\Tlocal_I)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~\X{loc}^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad (\iff I'' = I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex] \production{local} & \Tlocal_I &::=& \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype_I~\text{)} - \quad\Rightarrow\quad t \\ + \quad\Rightarrow\quad \{ \LTYPE~t \} \\ \end{array} The definition of the local :ref:`identifier context ` :math:`I''` uses the following auxiliary function to extract optional identifiers from locals: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index c19f2020c0..f73c2d5b47 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -172,7 +172,7 @@ .. Types, terminals .. |to| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow} - + .. |BOT| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{bot}} .. |I8| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i8}} @@ -200,6 +200,9 @@ .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} +.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{set}}} +.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{unset}}} + .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}} .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}} @@ -225,7 +228,10 @@ .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}} +.. |init| mathdef:: \xref{syntax/types}{syntax-init}{\X{init}} +.. |instrtype| mathdef:: \xref{syntax/types}{syntax-instrtype}{\X{instrtype}} +.. |localtype| mathdef:: \xref{syntax/types}{syntax-localtype}{\X{localtype}} .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}} @@ -280,6 +286,8 @@ .. |FLOCALS| mathdef:: \xref{syntax/modules}{syntax-func}{\K{locals}} .. |FBODY| mathdef:: \xref{syntax/modules}{syntax-func}{\K{body}} +.. |LTYPE| mathdef:: \xref{syntax/modules}{syntax-local}{\K{type}} + .. |TTYPE| mathdef:: \xref{syntax/modules}{syntax-table}{\K{type}} .. |MTYPE| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{type}} @@ -326,6 +334,7 @@ .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} .. |type| mathdef:: \xref{syntax/types}{syntax-functype}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} +.. |local| mathdef:: \xref{syntax/modules}{syntax-local}{\X{local}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} .. |global| mathdef:: \xref{syntax/modules}{syntax-global}{\X{global}} @@ -925,6 +934,8 @@ .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} +.. |vdashinstrtype| mathdef:: \xref{valid/instructions}{valid-instrtype}{\vdash} + .. |vdashvaltypedefaultable| mathdef:: \xref{valid/types}{valid-defaultable}{\vdash} .. |vdashtabletypedefaultable| mathdef:: \xref{valid/types}{valid-defaultable}{\vdash} @@ -949,6 +960,7 @@ .. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash} .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} +.. |vdashlocal| mathdef:: \xref{valid/modules}{valid-local}{\vdash} .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} .. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index ae219e44a2..528016fd2e 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,7 +24,7 @@ That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the :ref:`appendix `. -.. index:: ! context, function type, table type, memory type, global type, value type, result type, index space, module, function +.. index:: ! context, local type, function type, table type, memory type, global type, value type, result type, index space, module, function, local type .. _context: Contexts @@ -40,7 +40,7 @@ which collects relevant information about the surrounding :ref:`module ` that occur in the module outside functions and can hence be used to form references inside them. @@ -63,11 +63,11 @@ More concretely, contexts are defined as :ref:`records ` :math: & \CGLOBALS & \globaltype^\ast, \\ & \CELEMS & \reftype^\ast, \\ & \CDATAS & {\ok}^\ast, \\ - & \CLOCALS & \valtype^\ast, \\ + & \CLOCALS & \localtype^\ast, \\ & \CLABELS & \resulttype^\ast, \\ & \CRETURN & \resulttype^?, \\ & \CREFS & \funcidx^\ast ~\} \\ - \end{array} + \end{array} \\ \end{array} .. _notation-extend: @@ -158,15 +158,15 @@ and there is one respective rule for each relevant construct :math:`A` of the ab .. math:: \frac{ - C.\CLOCALS[x] = t + C.\CGLOBALS[x] = \mut~t }{ - C \vdash \LOCALGET~x : [] \to [t] + C \vdash \GLOBALGET~x : [] \to [t] } - Here, the premise enforces that the immediate :ref:`local index ` :math:`x` exists in the context. + Here, the premise enforces that the immediate :ref:`global index ` :math:`x` exists in the context. The instruction produces a value of its respective type :math:`t` (and does not consume any values). - If :math:`C.\CLOCALS[x]` does not exist then the premise does not hold, + If :math:`C.\CGLOBALS[x]` does not exist then the premise does not hold, and the instruction is ill-typed. Finally, a :ref:`structured ` instruction requires diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index e6d1ea13ba..c9bad0e4ed 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1,20 +1,22 @@ -.. index:: instruction, function type, context, value, operand stack, ! polymorphism, ! bottom type +.. index:: instruction, ! instruction type, context, value, operand stack, ! polymorphism .. _valid-instr: Instructions ------------ -:ref:`Instructions ` are classified by :ref:`function types ` :math:`[t_1^\ast] \to [t_2^\ast]` -that describe how they manipulate the :ref:`operand stack `. -The types describe the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off +:ref:`Instructions ` are classified by :ref:`instruction types ` that describe how they manipulate the :ref:`operand stack ` and initialize :ref:`locals `: +A type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` describes the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back. +Moreover, it enumerates the :ref:`indices ` :math:`x^\ast` of locals that have been set by the instruction. +In most cases, this is empty. .. note:: For example, the instruction :math:`\I32.\ADD` has type :math:`[\I32~\I32] \to [\I32]`, consuming two |I32| values and producing one. + The instruction :math:`LOCALSET~x` has type :math:`[t] \to_x []`, provided :math:`t` is the type declared for the local :math:`x`. Typing extends to :ref:`instruction sequences ` :math:`\instr^\ast`. -Such a sequence has a :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]` if the accumulative effect of executing the instructions is consuming values of types :math:`t_1^\ast` off the operand stack and pushing new values of types :math:`t_2^\ast`. +Such a sequence has an instruction type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` if the accumulative effect of executing the instructions is consuming values of types :math:`t_1^\ast` off the operand stack, pushing new values of types :math:`t_2^\ast`, and setting all locals :math:`x^\ast`. .. _polymorphism: @@ -27,9 +29,8 @@ Two degrees of polymorphism can be distinguished: the :ref:`value type ` :math:`t` of one or several individual operands is unconstrained. That is the case for all :ref:`parametric instructions ` like |DROP| and |SELECT|. - * *stack-polymorphic*: - the entire (or most of the) :ref:`function 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] \to_{x^\ast} [t_2^\ast]` of the instruction is unconstrained. 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. @@ -47,13 +48,14 @@ 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 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`. + The |UNREACHABLE| instruction is stack-polymorphic, + and hence valid with type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` for any possible sequences of value types :math:`t_1^\ast` and :math:`t_2^\ast` and sequence of locals :math:`x^\ast`. Consequently, .. math:: \UNREACHABLE~~\I32.\ADD - is valid by assuming type :math:`[] \to [\I32~\I32]` for the |UNREACHABLE| instruction. + is valid by assuming type :math:`[] \to [\I32]` for the |UNREACHABLE| instruction. In contrast, .. math:: @@ -650,13 +652,15 @@ Variable Instructions * The local :math:`C.\CLOCALS[x]` must be defined in the context. -* Let :math:`t` be the :ref:`value type ` :math:`C.\CLOCALS[x]`. +* Let :math:`\init~t` be the :ref:`local type ` :math:`C.\CLOCALS[x]`. + +* The :ref:`initialization status ` :math:`\init` must be :math:`\SET`. * Then the instruction is valid with type :math:`[] \to [t]`. .. math:: \frac{ - C.\CLOCALS[x] = t + C.\CLOCALS[x] = \SET~t }{ C \vdashinstr \LOCALGET~x : [] \to [t] } @@ -669,15 +673,15 @@ Variable Instructions * The local :math:`C.\CLOCALS[x]` must be defined in the context. -* Let :math:`t` be the :ref:`value type ` :math:`C.\CLOCALS[x]`. +* Let :math:`\init~t` be the :ref:`local type ` :math:`C.\CLOCALS[x]`. -* Then the instruction is valid with type :math:`[t] \to []`. +* Then the instruction is valid with type :math:`[t] \to_x []`. .. math:: \frac{ - C.\CLOCALS[x] = t + C.\CLOCALS[x] = \init~t }{ - C \vdashinstr \LOCALSET~x : [t] \to [] + C \vdashinstr \LOCALSET~x : [t] \to_x [] } @@ -688,15 +692,15 @@ Variable Instructions * The local :math:`C.\CLOCALS[x]` must be defined in the context. -* Let :math:`t` be the :ref:`value type ` :math:`C.\CLOCALS[x]`. +* Let :math:`\init~t` be the :ref:`local type ` :math:`C.\CLOCALS[x]`. -* Then the instruction is valid with type :math:`[t] \to [t]`. +* Then the instruction is valid with type :math:`[t] \to_x [t]`. .. math:: \frac{ - C.\CLOCALS[x] = t + C.\CLOCALS[x] = \init~t }{ - C \vdashinstr \LOCALTEE~x : [t] \to [t] + C \vdashinstr \LOCALTEE~x : [t] \to_x [t] } @@ -1253,13 +1257,13 @@ Control Instructions :math:`\UNREACHABLE` .................... -* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* The instruction is valid with any :ref:`valid ` type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`. .. math:: \frac{ - C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashinstrtype [t_1^\ast] \to_{x^\ast} [t_2^\ast] \ok }{ - C \vdashinstr \UNREACHABLE : [t_1^\ast] \to [t_2^\ast] + C \vdashinstr \UNREACHABLE : [t_1^\ast] \to_{x^\ast} [t_2^\ast] } .. note:: @@ -1276,7 +1280,7 @@ Control Instructions * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`, for any sequence of :ref:`local indices ` :math:`x^\ast`. * Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1284,7 +1288,7 @@ Control Instructions \frac{ C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_2^\ast] + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast] \to_{x^\ast} [t_2^\ast] }{ C \vdashinstr \BLOCK~\blocktype~\instr^\ast~\END : [t_1^\ast] \to [t_2^\ast] } @@ -1298,12 +1302,12 @@ Control Instructions :math:`\LOOP~\blocktype~\instr^\ast~\END` ......................................... -* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. +* The :ref:`block type ` must be :ref:`valid ` as some :ref:`instruction type ` :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`. * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`, for any sequence of :ref:`local indices ` :math:`x^\ast`. * Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1311,7 +1315,7 @@ Control Instructions \frac{ C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLABELS\,[t_1^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_2^\ast] + C,\CLABELS\,[t_1^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast] \to_{x^\ast} [t_2^\ast] }{ C \vdashinstr \LOOP~\blocktype~\instr^\ast~\END : [t_1^\ast] \to [t_2^\ast] } @@ -1330,10 +1334,10 @@ Control Instructions * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to_{x_1^\ast} [t_2^\ast]`, for any sequence of :ref:`local indices ` :math:`x_1^\ast`. * Under context :math:`C'`, - the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to_{x_2^\ast} [t_2^\ast]`, for any sequence of :ref:`local indices ` :math:`x_2^\ast`. * Then the compound instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`. @@ -1341,9 +1345,9 @@ Control Instructions \frac{ C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_1^\ast : [t_1^\ast] \to [t_2^\ast] + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_1^\ast : [t_1^\ast] \to_{x_1^\ast} [t_2^\ast] \qquad - C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_2^\ast : [t_1^\ast] \to [t_2^\ast] + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_2^\ast : [t_1^\ast] \to_{x_2^\ast} [t_2^\ast] }{ C \vdashinstr \IF~\blocktype~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [t_1^\ast~\I32] \to [t_2^\ast] } @@ -1361,15 +1365,15 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to_{x^\ast} [t_2^\ast]`, for any :ref:`valid ` type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`. .. math:: \frac{ C.\CLABELS[l] = [t^\ast] \qquad - C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashinstrtype [t_1^\ast] \to_{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] \to_{x^\ast} [t_2^\ast] } .. note:: @@ -1418,7 +1422,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 type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to_{x^\ast} [t_2^\ast]`, for any :ref:`valid ` type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`. .. math:: \frac{ @@ -1426,9 +1430,9 @@ Control Instructions \qquad C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N] \qquad - C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashinstrtype [t_1^\ast] \to_{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] \to_{x^\ast} [t_2^\ast] } .. note:: @@ -1496,15 +1500,15 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` of :math:`C.\CRETURN`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to_{x^\ast} [t_2^\ast]`, for any :ref:`valid ` type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]`. .. math:: \frac{ C.\CRETURN = [t^\ast] \qquad - C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashinstrtype [t_1^\ast] \to_{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] \to_{x^\ast} [t_2^\ast] } .. note:: @@ -1578,7 +1582,7 @@ Control Instructions } -.. index:: instruction, instruction sequence +.. index:: instruction, instruction sequence, local type .. _valid-instr-seq: Instruction Sequences @@ -1603,10 +1607,15 @@ Empty Instruction Sequence: :math:`\epsilon` Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` ............................................................ -* The instruction sequence :math:`\instr^\ast` must be valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, +* The instruction sequence :math:`\instr^\ast` must be valid with type :math:`[t_1^\ast] \to_{x_1^\ast} [t_2^\ast]`, for some sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. -* The instruction :math:`\instr_N` must be valid with type :math:`[t^\ast] \to [t_3^\ast]`, +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, + but with: + + * |CLOCALS| the same as in C, except that for every :ref:`local index ` :math:`x` in :math:`x_1^\ast`, the :ref:`local type ` :math:`\CLOCALS[x]` has been updated to :ref:`initialization status ` `\SET`. + +* Under context :math:`C'`, the instruction :math:`\instr_N` must be valid with type :math:`[t^\ast] \to_{x_2^\ast} [t_3^\ast]`, for some sequences of :ref:`value types ` :math:`t^\ast` and :math:`t_3^\ast`. * There must be a sequence of :ref:`value types ` :math:`t_0^\ast`, @@ -1614,17 +1623,23 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` * For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding type :math:`t_i` in :math:`t^\ast`, the type :math:`t'_i` must :ref:`match ` :math:`t_i`. -* Then the combined instruction sequence is valid with type :math:`[t_1^\ast] \to [t_0^\ast~t_3^\ast]`. +* Then the combined instruction sequence is valid with type :math:`[t_1^\ast] \to_{x_1^\ast x_2^\ast} [t_0^\ast~t_3^\ast]`. .. math:: \frac{ - C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast] + \begin{array}{@{}c@{}} + C \vdashinstrseq \instr^\ast : [t_1^\ast] \to_{x_1^\ast} [t_0^\ast~{t'}^\ast] \qquad (C \vdashvaltypematch t' \matchesvaltype t)^\ast \qquad - C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast] + C' \vdashinstr \instr_N : [t^\ast] \to_{x_2^\ast} [t_3^\ast] + \\ + (\init~t = C.\CLOCALS[x_1])^\ast + \qquad + C' = C~(\with C.\CLOCALS[x_1] = \SET~t)^\ast + \end{array} }{ - C \vdashinstrseq \instr^\ast~\instr_N : [t_1^\ast] \to [t_0^\ast~t_3^\ast] + C \vdashinstrseq \instr^\ast~\instr_N : [t_1^\ast] \to_{x_1^\ast x_2^\ast} [t_0^\ast~t_3^\ast] } @@ -1643,7 +1658,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`type ` :math:`[] \to [{t'}^\ast]`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some :ref:`type ` :math:`[] \to_{x^\ast} [{t'}^\ast]`. * For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`valid ` :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. @@ -1651,7 +1666,7 @@ Expressions :math:`\expr` are classified by :ref:`result types * Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. +* For each local declared by a :ref:`value type ` :math:`t` in :math:`t^\ast`: + + * The local for type :math:`t` must be :ref:`valid ` with :ref:`local type ` :math:`\localtype_i`. + +* Let :math:`\localtype^\ast` be the concatenation of all :math:`\localtype_i`. + * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with: - * |CLOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, + * |CLOCALS| set to the sequence of :ref:`value types ` :math:`(\SET~t_1)^\ast~\localtype^\ast`, concatenating parameters and locals, * |CLABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. @@ -42,12 +48,57 @@ Functions :math:`\func` are classified by :ref:`function types \frac{ C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] + (C \vdashlocal t : \init~t)^\ast + \qquad + C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] }{ C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^\ast] } +.. index:: local, local type, value type + pair: validation; local + single: abstract syntax; local +.. _valid-localtype: + +Locals +~~~~~~ + +:ref:`Locals ` are classified with :ref:`local types `. + +:math:`\{ \LTYPE~\valtype \}` +............................. + +* The :ref:`value type ` :math:`\valtype` must be :ref:`valid `. + +* If :math:`\valtype` is :ref:`defaultable `, then: + + * The local is valid with :ref:`local type ` :math:`\SET~\valtype`. + +* Else: + + * The local is valid with :ref:`local type ` :math:`\UNSET~\valtype`. + +.. math:: + \frac{ + C \vdashvaltype t \ok + \qquad + C \vdashvaltypedefaultable t \defaultable + }{ + C \vdashlocal \{ \LTYPE~t \} : \SET~t \ok + } + +.. math:: + \frac{ + C \vdashvaltype t \ok + }{ + C \vdashlocal \{ LTYPE~t \} : \UNSET~t \ok + } + +.. note:: + For cases where both rules are applicable, the former yields the more permissable type. + + .. index:: table, table type, defaultable pair: validation; table single: abstract syntax; table diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index e4f7a7995d..ad9c429132 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -146,7 +146,7 @@ Valid :ref:`value types ` are either valid :ref:`number type ` are either valid :ref:`number type ` may be expressed in one of two forms, both of which are converted to plain :ref:`function types ` by the following rules. +:ref:`Block types ` may be expressed in one of two forms, both of which are converted to :ref:`instruction types ` by the following rules. :math:`\typeidx` ................ * The type :math:`C.\CTYPES[\typeidx]` must be defined in the context. -* Then the block type is valid as :ref:`function type ` :math:`C.\CTYPES[\typeidx]`. +* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[\typeidx]`. + +* Then the block type is valid as :ref:`instruction type ` :math:`[t_1^\ast] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTYPES[\typeidx] = \functype + C.\CTYPES[\typeidx] = [t_1^\ast] \to [t_2^\ast] }{ - C \vdashblocktype \typeidx : \functype + C \vdashblocktype \typeidx : [t_1^\ast] \to [t_2^\ast] } @@ -176,7 +178,7 @@ Block Types * The value type :math:`\valtype` must either be absent, or :ref:`valid `. -* Then the block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. +* Then the block type is valid as :ref:`instruction type ` :math:`[] \to [\valtype^?]`. .. math:: \frac{ @@ -209,38 +211,34 @@ Result Types } -.. index:: limits - pair: validation; limits - single: abstract syntax; limits -.. _valid-limits: - -Limits -~~~~~~ - -:ref:`Limits ` must have meaningful bounds that are within a given range. +.. index:: instruction type + pair: validation; instruction type + single: abstract syntax; instruction type +.. _valid-instrtype: -:math:`\{ \LMIN~n, \LMAX~m^? \}` -................................ +Instruction Types +~~~~~~~~~~~~~~~~~ -* The value of :math:`n` must not be larger than :math:`k`. +:math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` +.......................................... -* If the maximum :math:`m^?` is not empty, then: +* The :ref:`result type ` :math:`[t_1^\ast]` must be :ref:`valid `. - * Its value must not be larger than :math:`k`. +* The :ref:`result type ` :math:`[t_2^\ast]` must be :ref:`valid `. - * Its value must not be smaller than :math:`n`. +* Each :ref:`local index ` :math:`x_i` in :math:`x^\ast` must be defined in the context. -* Then the limit is valid within range :math:`k`. +* Then the instruction type is valid. .. math:: \frac{ - n \leq k + C \vdashvaltype [t_1^\ast] \ok \qquad - (m \leq k)^? + C \vdashvaltype [t_2^\ast] \ok \qquad - (n \leq m)^? + (C.\CLOCALS[x] = \localtype)^\ast }{ - C \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k + C \vdashfunctype [t_1^\ast] \to_{x^\ast} [t_2^\ast] \ok } @@ -271,6 +269,41 @@ Function Types } +.. index:: limits + pair: validation; limits + single: abstract syntax; limits +.. _valid-limits: + +Limits +~~~~~~ + +:ref:`Limits ` must have meaningful bounds that are within a given range. + +:math:`\{ \LMIN~n, \LMAX~m^? \}` +................................ + +* The value of :math:`n` must not be larger than :math:`k`. + +* If the maximum :math:`m^?` is not empty, then: + + * Its value must not be larger than :math:`k`. + + * Its value must not be smaller than :math:`n`. + +* Then the limit is valid within range :math:`k`. + +.. math:: + \frac{ + n \leq k + \qquad + (m \leq k)^? + \qquad + (n \leq m)^? + }{ + C \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k + } + + .. index:: table type, reference type, limits pair: validation; table type single: abstract syntax; table type