diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index d11095af..5253a4a9 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -21,15 +21,49 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b Data Structures ~~~~~~~~~~~~~~~ +Types are representable as an enumeration. +In addition to the plain types from the WebAssembly validation semantics, an extended notion of operand type includes a bottom type `Unknown` that is used as the type of :ref:`polymorphic ` operands. + +A simple subtyping check can be defined on these types. +In addition, corresponding functions computing the join (least upper bound) and meet (greatest lower bound) of two types are used. +Because there is no top type, a join does not exist in all cases. +Similarly, a meet must always be defined on known value types that exclude the auxiliary bottom type `Unknown`, +hence a meet does not exist in all cases either. +A type error is encountered if a join or meet is required when it does not exist. + +.. code-block:: pseudo + + type val_type = I32 | I64 | F32 | F64 | Anyref | Anyfunc | Anyeqref | Nullref + type opd_type = val_type | Unknown + + func is_ref(t : opd_type) : bool = + return t = Anyref || t = Anyfunc || t = Anyeqref || t = Nullref + + func matches(t1 : opd_type, t2 : opd_type) : bool = + return t1 = t2 || t1 = Unknown || + (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref) + + func join(t1 : opd_type, t2 : opd_type) : opd_type = + if (t1 = t2) return t1 + if (matches(t1, t2)) return t2 + if (matches(t2, t1)) return t1 + error_if(not (is_ref(t1) && is_ref(t2))) + return Anyref + + func meet(t1 : val_type, t2 : val_type) : val_type = + if (t1 = t2) return t1 + if (matches(t1, t2)) return t1 + if (matches(t2, t1)) return t2 + error_if(not (is_ref(t1) && is_ref(t2))) + return Nullref + The algorithm uses two separate stacks: the *operand 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 `. .. code-block:: pseudo - type val_type = I32 | I64 | F32 | F64 - - type opd_stack = stack(val_type | Unknown) + type opd_stack = stack(opd_type) type ctrl_stack = stack(ctrl_frame) type ctrl_frame = { @@ -58,20 +92,17 @@ However, these variables are not manipulated directly by the main checking funct .. code-block:: pseudo - func push_opd(type : val_type | Unknown) = + func push_opd(type : opd_type) = opds.push(type) - func pop_opd() : val_type | Unknown = + func pop_opd() : opd_type = if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown error_if(opds.size() = ctrls[0].height) return opds.pop() - func pop_opd(expect : val_type | Unknown) : val_type | Unknown = + func pop_opd(expect : val_type) = let actual = pop_opd() - if (actual = Unknown) return expect - if (expect = Unknown) return actual - error_if(actual =/= expect) - return actual + error_if(not matches(actual, expect)) func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t) func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t) @@ -83,9 +114,8 @@ But first, a special case is handled where the block contains no known operands, That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically `. In that case, an unknown type is returned. -A second function for popping an operand takes an expected type, which the actual operand type is checked against. -The types may differ in case one of them is Unknown. -The more specific type is returned. +A second function for popping an operand takes an expected (known) type, which the actual operand type is checked against. +The types may differ by subtyping, inlcuding the case where the actual type is unknown. Finally, there are accumulative functions for pushing or popping multiple operand types. @@ -150,14 +180,19 @@ Other instructions are checked in a similar manner. pop_opd(I32) push_opd(I32) + case (ref.eq) + pop_opd(Anyeqref) + pop_opd(Anyeqref) + push_opd(I32) + case (drop) pop_opd() case (select) pop_opd(I32) let t1 = pop_opd() - let t2 = pop_opd(t1) - push_opd(t2) + let t2 = pop_opd() + push_opd(join(t1, t2))    case (unreachable)       unreachable() @@ -193,10 +228,12 @@ Other instructions are checked in a similar manner.    case (br_table n* m)       error_if(ctrls.size() < m) + var ts = ctrls[m].label_types       foreach (n in n*) -         error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types) +         error_if(ctrls.size() < n) + ts := meet(ts, ctrls[n].label_types) pop_opd(I32) -       pop_opds(ctrls[m].label_types) +       pop_opds(ts)       unreachable() .. note:: diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index f5811e02..d1997791 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -24,7 +24,7 @@ Instruction Binary Opcode Type :math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` :math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` :math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALLINDIRECT~x` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` (reserved) :math:`\hex{12}` (reserved) :math:`\hex{13}` (reserved) :math:`\hex{14}` @@ -44,8 +44,8 @@ Instruction Binary Opcode Type :math:`\TEELOCAL~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` :math:`\GETGLOBAL~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` :math:`\SETGLOBAL~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{25}` -(reserved) :math:`\hex{26}` +:math:`\GETTABLE~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\SETTABLE~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` (reserved) :math:`\hex{27}` :math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` :math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` @@ -199,5 +199,24 @@ Instruction Binary Opcode Type :math:`\I64.\REINTERPRET\K{/}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` :math:`\F32.\REINTERPRET\K{/}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` :math:`\F64.\REINTERPRET\K{/}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +(reserved) :math:`\hex{C0}` +(reserved) :math:`\hex{C1}` +(reserved) :math:`\hex{C2}` +(reserved) :math:`\hex{C3}` +(reserved) :math:`\hex{C4}` +(reserved) :math:`\hex{C5}` +(reserved) :math:`\hex{C6}` +(reserved) :math:`\hex{C7}` +(reserved) :math:`\hex{C8}` +(reserved) :math:`\hex{C9}` +(reserved) :math:`\hex{CA}` +(reserved) :math:`\hex{CB}` +(reserved) :math:`\hex{CC}` +(reserved) :math:`\hex{CD}` +(reserved) :math:`\hex{CE}` +(reserved) :math:`\hex{CF}` +:math:`\REFNULL` :math:`\hex{D0}` :math:`[] \to [\NULLREF]` :ref:`validation ` :ref:`execution ` +:math:`\REFISNULL` :math:`\hex{D1}` :math:`[\ANYREF] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\REFEQ` :math:`\hex{D2}` :math:`[\ANYEQREF~\ANYEQREF] \to [\I32]` :ref:`validation ` :ref:`execution ` =================================== ================ ========================================== ======================================== =============================================================== diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 28154806..75ba290e 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -71,14 +71,15 @@ Construct Judgement =============================================== =============================================================================== -Import Matching -~~~~~~~~~~~~~~~ +Matching +~~~~~~~~ =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matches \limits_2` -:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matches \externtype_2` +:ref:`Value type ` :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` +:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` +:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2` =============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 972ae6b4..81992294 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -8,17 +8,19 @@ Index of Types Category Constructor Binary Opcode ======================================== =========================================== =============================================================================== :ref:`Type index ` :math:`x` (positive number as |Bs32| or |Bu32|) -:ref:`Value type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) -:ref:`Value type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) -:ref:`Value type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) -:ref:`Value type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) -(reserved) :math:`\hex{7C}` .. :math:`\hex{71}` -:ref:`Element type ` |ANYFUNC| :math:`\hex{70}` (-16 as |Bs7|) -(reserved) :math:`\hex{6F}` .. :math:`\hex{61}` +:ref:`Number type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) +:ref:`Number type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) +:ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) +:ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) +(reserved) :math:`\hex{7B}` .. :math:`\hex{71}` +:ref:`Reference type ` |ANYFUNC| :math:`\hex{70}` (-16 as |Bs7|) +:ref:`Reference type ` |ANYREF| :math:`\hex{6F}` (-17 as |Bs7|) +:ref:`Reference type ` |ANYEQREF| :math:`\hex{6E}` (-18 as |Bs7|) +(reserved) :math:`\hex{6D}` .. :math:`\hex{61}` :ref:`Function type ` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) (reserved) :math:`\hex{5F}` .. :math:`\hex{41}` :ref:`Result type ` :math:`\epsilon` :math:`\hex{40}` (-64 as |Bs7|) -:ref:`Table type ` :math:`\limits~\elemtype` (none) +:ref:`Table type ` :math:`\limits~\reftype` (none) :ref:`Memory type ` :math:`\limits` (none) :ref:`Global type ` :math:`\mut~\valtype` (none) ======================================== =========================================== =============================================================================== diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index faf5411d..e83c57ac 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -54,17 +54,39 @@ Control Instructions &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& \hex{0F} &\Rightarrow& \RETURN \\ &&|& \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|& - \hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\ + \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ \end{array} .. note:: The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty. + +.. index:: reference instruction + pair: binary format; instruction +.. _binary-instr-ref: + +Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~ + +:ref:`Reference instructions ` are represented by single byte codes. + +.. _binary-ref_null: +.. _binary-ref_isnull: +.. _binary-ref_eq: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots \\ &&|& + \hex{D0} &\Rightarrow& \REFNULL \\ &&|& + \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& + \hex{D2} &\Rightarrow& \REFEQ \\ + \end{array} + .. note:: - In future versions of WebAssembly, the zero byte occurring in the encoding - of the |CALLINDIRECT| instruction may be used to index additional tables. + These opcode assignments are preliminary. + -.. index:: value type, polymorphism +.. index:: parametric instruction, value type, polymorphism pair: binary format; instruction .. _binary-instr-parametric: @@ -110,6 +132,29 @@ Variable Instructions \end{array} +.. index:: table instruction, table index + pair: binary format; instruction +.. _binary-instr-table: + +Table Instructions +~~~~~~~~~~~~~~~~~~ + +:ref:`Table instructions ` are represented by single byte codes. + +.. _binary-get_table: +.. _binary-set_table: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots \\ &&|& + \hex{25}~~x{:}\Btableidx &\Rightarrow& \GETTABLE~x \\ &&|& + \hex{26}~~x{:}\Btableidx &\Rightarrow& \SETTABLE~x \\ + \end{array} + +.. note:: + These opcode assignments are preliminary. + + .. index:: memory instruction, memory index pair: binary format; instruction .. _binary-instr-memory: diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index e5342259..21b4ec1b 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -5,27 +5,63 @@ Types ----- -.. index:: value type - pair: binary format; value type -.. _binary-valtype: +.. note:: + In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. + Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future. -Value Types -~~~~~~~~~~~ -:ref:`Value types ` are encoded by a single byte. +.. index:: number type + pair: binary format; number type +.. _binary-numtype: + +Number Types +~~~~~~~~~~~~ + +:ref:`Number types ` are encoded by a single byte. .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{value type} & \Bvaltype &::=& + \production{number type} & \Bnumtype &::=& \hex{7F} &\Rightarrow& \I32 \\ &&|& \hex{7E} &\Rightarrow& \I64 \\ &&|& \hex{7D} &\Rightarrow& \F32 \\ &&|& \hex{7C} &\Rightarrow& \F64 \\ \end{array} -.. note:: - In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. - Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future. + +.. index:: reference type + pair: binary format; reference type +.. _binary-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +:ref:`Reference types ` are also encoded by a single byte. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{reference type} & \Breftype &::=& + \hex{70} &\Rightarrow& \ANYFUNC \\ &&|& + \hex{6F} &\Rightarrow& \ANYREF \\ &&|& + \hex{6E} &\Rightarrow& \ANYEQREF \\ + \end{array} + + +.. index:: value type, number type, reference type + pair: binary format; value type +.. _binary-valtype: + +Value Types +~~~~~~~~~~~ + +:ref:`Value types ` are encoded with their respective encoding as a :ref:`number type ` or :ref:`reference type `. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{value type} & \Bvaltype &::=& + t{:}\Bnumtype &\Rightarrow& t \\ &&|& + t{:}\Breftype &\Rightarrow& t \\ + \end{array} .. index:: result type, value type @@ -99,23 +135,19 @@ Memory Types \end{array} -.. index:: table type, element type, limits +.. index:: table type, reference type, limits pair: binary format; table type - pair: binary format; element type -.. _binary-elemtype: .. _binary-tabletype: Table Types ~~~~~~~~~~~ -:ref:`Table types ` are encoded with their :ref:`limits ` and a constant byte indicating their :ref:`element type `. +:ref:`Table types ` are encoded with their :ref:`limits ` and the encoding of their element :ref:`reference type `. .. math:: \begin{array}{llclll} \production{table type} & \Btabletype &::=& - \X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ - \production{element type} & \Belemtype &::=& - \hex{70} &\Rightarrow& \ANYFUNC \\ + \X{et}{:}\Breftype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index f0990ad2..41620bd0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -43,7 +43,7 @@ Where the underlying operators are non-deterministic, because they may return on 1. Push the value :math:`t.\CONST~c` to the stack. .. note:: - No formal reduction rule is required for this instruction, since |CONST| instructions coincide with :ref:`values `. + No formal reduction rule is required for this instruction, since |CONST| instructions already are :ref:`values `. .. _exec-unop: @@ -174,6 +174,79 @@ Where the underlying operators are non-deterministic, because they may return on \end{array} +.. index:: reference instructions, reference + pair: execution; instruction + single: abstract syntax; instruction +.. _exec-instr-ref: + +Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~ + +.. _exec-ref_null: + +:math:`\REFNULL` +................ + +1. Push the value :math:`\REFNULL` to the stack. + +.. note:: + No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value `. + + +.. _exec-ref_isnull: + +:math:`\REFISNULL` +.................. + +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +2. Pop the value :math:`\val` from the stack. + +3. If :math:`\val` is |REFNULL|, then: + + a. Push the value :math:`\I32.\CONST~1` to the stack. + +4. Else: + + a. Push the value :math:`\I32.\CONST~0` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val~\REFISNULL &\stepto& \I32.\CONST~1 + & (\iff \val = \REFNULL) \\ + \val~\REFISNULL &\stepto& \I32.\CONST~0 + & (\iff \val \neq \REFNULL) \\ + \end{array} + + +.. _exec-ref_eq: + +:math:`\REFEQ` +.............. + +1. Assert: due to :ref:`validation `, two :ref:`reference values ` are on the top of the stack. + +2. Pop the value :math:`\val_2` from the stack. + +3. Pop the value :math:`\val_1` from the stack. + +3. If :math:`\val_1` is the same as :math:`\val_2`, then: + + a. Push the value :math:`\I32.\CONST~1` to the stack. + +4. Else: + + a. Push the value :math:`\I32.\CONST~0` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val_1~\val_2~\REFEQ &\stepto& \I32.\CONST~1 + & (\iff \val_1 = \val_2) \\ + \val_1~\val_2~\REFEQ &\stepto& \I32.\CONST~0 + & (\iff \val_1 \neq \val_2) \\ + \end{array} + + .. index:: parametric instructions, value pair: execution; instruction single: abstract syntax; instruction @@ -363,7 +436,101 @@ Variable Instructions :ref:`Validation ` ensures that the global is, in fact, marked as mutable. -.. index:: memory instruction, memory index, store, frame, address, memory address, memory instance, store, frame, value, integer, limits, value type, bit width +.. index:: table instruction, table index, store, frame, address, table address, table instance, value, integer, limits, reference, reference type + pair: execution; instruction + single: abstract syntax; instruction +.. _exec-instr-table: + +Table Instructions +~~~~~~~~~~~~~~~~~~ + +.. _exec-get_table: + +:math:`\GETTABLE~x` +................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. + +3. Let :math:`a` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[a]` exists. + +5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. + +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. + +7. Pop the value :math:`\I32.\CONST~i` from the stack. + +8. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: + + a. Trap. + +6. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. + +7. Push the value :math:`\val` to the stack. + +.. math:: + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~i)~(\GETTABLE~x) &\stepto& S; F; \val + \end{array} + \\ \qquad + (\iff S.\STABLES[F.\AMODULE.\MITABLES[x]][i] = \val) \\ + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~i)~(\GETTABLE~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) \\ + \end{array} + + +.. _exec-set_table: + +:math:`\SETTABLE~x` +................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. + +3. Let :math:`a` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[a]` exists. + +5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. + +6. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +7. Pop the value :math:`\val` from the stack. + +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. + +9. Pop the value :math:`\I32.\CONST~i` from the stack. + +10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: + + a. Trap. + +11. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. + +.. math:: + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~i)~\val~(\SETTABLE~x) &\stepto& S'; F; \epsilon + \end{array} + \\ \qquad + (\iff S' = S \with \STABLES[F.\AMODULE.\MITABLES[x]][i] = \val) \\ + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~i)~\val~(\SETTABLE~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) \\ + \end{array} + + +.. index:: memory instruction, memory index, store, frame, address, memory address, memory instance, value, integer, limits, value type, bit width pair: execution; instruction single: abstract syntax; instruction .. _exec-memarg: @@ -512,7 +679,7 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + |t|/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8] = \bytes_t(c) + \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8] = \bytes_t(c)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -870,22 +1037,22 @@ Control Instructions .. _exec-call_indirect: -:math:`\CALLINDIRECT~x` -....................... +:math:`\CALLINDIRECT~x~y` +......................... 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. -3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. +3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. 4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}]` exists. 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITYPES[x]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITYPES[y]` exists. -7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type ` :math:`F.\AMODULE.\MITYPES[x]`. +7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type ` :math:`F.\AMODULE.\MITYPES[y]`. 8. Assert: due to :ref:`validation `, a value with :ref:`value type ` |I32| is on the top of the stack. @@ -895,39 +1062,43 @@ Control Instructions a. Trap. -11. If :math:`\X{tab}.\TIELEM[i]` is uninitialized, then: +11. Let :math:`r` be the :ref:`reference ` :math:`\X{tab}.\TIELEM[i]`. + +12. If :math:`r` is |REFNULL|, then: a. Trap. -12. Let :math:`a` be the :ref:`function address ` :math:`\X{tab}.\TIELEM[i]`. +13. Assert: due to :ref:`validation of table mutation `, :math:`r` is a :ref:`function reference `. + +14. Let :math:`\REFFUNC~a` be the :ref:`function reference ` :math:`r`. -13. Assert: due to :ref:`validation `, :math:`S.\SFUNCS[a]` exists. +15. Assert: due to :ref:`validation of table mutation `, :math:`S.\SFUNCS[a]` exists. -14. Let :math:`\X{f}` be the :ref:`function instance ` :math:`S.\SFUNCS[a]`. +16. Let :math:`\X{f}` be the :ref:`function instance ` :math:`S.\SFUNCS[a]`. -15. Let :math:`\X{ft}_{\F{actual}}` be the :ref:`function type ` :math:`\X{f}.\FITYPE`. +17. Let :math:`\X{ft}_{\F{actual}}` be the :ref:`function type ` :math:`\X{f}.\FITYPE`. -16. If :math:`\X{ft}_{\F{actual}}` and :math:`\X{ft}_{\F{expect}}` differ, then: +18. If :math:`\X{ft}_{\F{actual}}` and :math:`\X{ft}_{\F{expect}}` differ, then: a. Trap. -17. :ref:`Invoke ` the function instance at address :math:`a`. +19. :ref:`Invoke ` the function instance at address :math:`a`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\CALLINDIRECT~x) &\stepto& S; F; (\INVOKE~a) + S; F; (\I32.\CONST~i)~(\CALLINDIRECT~x~y) &\stepto& S; F; (\INVOKE~a) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM[i] = a \\ + (\iff & S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \REFFUNC~a \\ \wedge & S.\SFUNCS[a] = f \\ - \wedge & F.\AMODULE.\MITYPES[x] = f.\FITYPE) + \wedge & F.\AMODULE.\MITYPES[y] = f.\FITYPE) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\CALLINDIRECT~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\CALLINDIRECT~x~y) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) @@ -1019,13 +1190,11 @@ Invocation of :ref:`function address ` :math:`a` 8. Pop the values :math:`\val^n` from the stack. -9. Let :math:`\val_0^\ast` be the list of zero values of types :math:`t^\ast`. - -10. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~\val_0^\ast \}`. +9. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. -11. 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. -12. :ref:`Execute ` the instruction :math:`\BLOCK~[t_2^m]~\instr^\ast~\END`. +11. :ref:`Execute ` the instruction :math:`\BLOCK~[t_2^m]~\instr^\ast~\END`. .. math:: ~\\[-1ex] @@ -1039,7 +1208,7 @@ Invocation of :ref:`function address ` :math:`a` \wedge & f.\FITYPE = [t_1^n] \to [t_2^m] \\ \wedge & m \leq 1 \\ \wedge & f.\FICODE = \{ \FTYPE~x, \FLOCALS~t^k, \FBODY~\instr^\ast~\END \} \\ - \wedge & F = \{ \AMODULE~f.\FIMODULE, ~\ALOCALS~\val^n~(t.\CONST~0)^k \}) + \wedge & F = \{ \AMODULE~f.\FIMODULE, ~\ALOCALS~\val^n~(\default_t)^k \}) \end{array} \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index bc772ddc..aa1d82be 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -126,7 +126,7 @@ Limits \frac{ n_1 \geq n_2 }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matches \{ \LMIN~n_2, \LMAX~\epsilon \} + \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \} } \quad \frac{ @@ -134,7 +134,7 @@ Limits \qquad m_1 \leq m_2 }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matches \{ \LMIN~n_2, \LMAX~m_2 \} + \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \} } @@ -154,7 +154,7 @@ An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches ~\\[-1ex] \frac{ }{ - \vdashexterntypematch \ETFUNC~\functype \matches \ETFUNC~\functype + \vdashexterntypematch \ETFUNC~\functype \matchesexterntype \ETFUNC~\functype } @@ -164,17 +164,17 @@ An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches Tables ...... -An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\elemtype_1)` matches :math:`\ETTABLE~(\limits_2~\elemtype_2)` if and only if: +An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\reftype_1)` matches :math:`\ETTABLE~(\limits_2~\reftype_2)` if and only if: * Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. -* Both :math:`\elemtype_1` and :math:`\elemtype_2` are the same. +* Both :math:`\reftype_1` and :math:`\reftype_2` are the same. .. math:: \frac{ - \vdashlimitsmatch \limits_1 \matches \limits_2 + \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 }{ - \vdashexterntypematch \ETTABLE~(\limits_1~\elemtype) \matches \ETTABLE~(\limits_2~\elemtype) + \vdashexterntypematch \ETTABLE~(\limits_1~\reftype) \matchesexterntype \ETTABLE~(\limits_2~\reftype) } @@ -190,9 +190,9 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma .. math:: \frac{ - \vdashlimitsmatch \limits_1 \matches \limits_2 + \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 }{ - \vdashexterntypematch \ETMEM~\limits_1 \matches \ETMEM~\limits_2 + \vdashexterntypematch \ETMEM~\limits_1 \matchesexterntype \ETMEM~\limits_2 } @@ -202,15 +202,23 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma Globals ....... -An :ref:`external type ` :math:`\ETGLOBAL~\globaltype_1` matches :math:`\ETGLOBAL~\globaltype_2` if and only if: +An :ref:`external type ` :math:`\ETGLOBAL~(\mut_1~t_1)` matches :math:`\ETGLOBAL~(\mut_2~t_2)` if and only if: -* Both :math:`\globaltype_1` and :math:`\globaltype_2` are the same. +* Either both :math:`\mut_1` and :math:`\mut_2` are |MVAR| and :math:`t_1` and :math:`t_2` are the same. + +* Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. .. math:: ~\\[-1ex] \frac{ }{ - \vdashexterntypematch \ETGLOBAL~\globaltype \matches \ETGLOBAL~\globaltype + \vdashexterntypematch \ETGLOBAL~(\MVAR~t) \matchesexterntype \ETGLOBAL~(\MVAR~t) + } + \qquad + \frac{ + \vdashvaltypematch t_1 \matchesvaltype t_2 + }{ + \vdashexterntypematch \ETGLOBAL~(\MCONST~t_1) \matchesexterntype \ETGLOBAL~(\MCONST~t_2) } @@ -292,11 +300,11 @@ New instances of :ref:`functions `, :ref:`tables ` to allocate. -2. Let :math:`(\{\LMIN~n, \LMAX~m^?\}~\elemtype)` be the structure of :ref:`table type ` :math:`\tabletype`. +2. Let :math:`(\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type ` :math:`\tabletype`. 3. Let :math:`a` be the first free :ref:`table address ` in :math:`S`. -4. Let :math:`\tableinst` be the :ref:`table instance ` :math:`\{ \TIELEM~(\epsilon)^n, \TIMAX~m^? \}` with :math:`n` empty elements. +4. Let :math:`\tableinst` be the :ref:`table instance ` :math:`\{ \TIELEM~\REFNULL^n, \TIMAX~m^? \}` with :math:`n` empty elements. 5. Append :math:`\tableinst` to the |STABLES| of :math:`S`. @@ -306,9 +314,9 @@ New instances of :ref:`functions `, :ref:`tables ` 2. If :math:`\tableinst.\TIMAX` is not empty and smaller than :math:`n` added to the length of :math:`\tableinst.\TIELEM`, then fail. -3. Append :math:`n` empty elements to :math:`\tableinst.\TIELEM`. +3. Append :math:`\REFNULL^n` to :math:`\tableinst.\TIELEM`. .. math:: \begin{array}{rllll} - \growtable(\tableinst, n) &=& \tableinst \with \TIELEM = \tableinst.\TIELEM~(\epsilon)^n \\ + \growtable(\tableinst, n) &=& \tableinst \with \TIELEM = \tableinst.\TIELEM~\REFNULL^n \\ && (\iff \tableinst.\TIMAX = \epsilon \vee |\tableinst.\TIELEM| + n \leq \tableinst.\TIMAX) \\ \end{array} @@ -651,7 +659,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep ii. Let :math:`\funcaddr_{ij}` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`. - iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`. + iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\REFFUNC~\funcaddr_{ij}`. 14. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: @@ -680,7 +688,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep &(\iff & \vdashmodule \module : \externtype_{\F{im}}^n \to \externtype_{\F{ex}}^\ast \\ &\wedge& (S \vdashexternval \externval : \externtype)^n \\ - &\wedge& (\vdashexterntypematch \externtype \matches \externtype_{\F{im}})^n \\[1ex] + &\wedge& (\vdashexterntypematch \externtype \matchesexterntype \externtype_{\F{im}})^n \\[1ex] &\wedge& \module.\MGLOBALS = \global^\ast \\ &\wedge& \module.\MELEM = \elem^\ast \\ &\wedge& \module.\MDATA = \data^\ast \\ @@ -701,7 +709,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep S; F; \epsilon \\ S; F; \INITELEM~a~i~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~a~(i+1)~x^\ast \\ && - (\iff S' = S \with \STABLES[a].\TIELEM[i] = F.\AMODULE.\MIFUNCS[x_0]) + (\iff S' = S \with \STABLES[a].\TIELEM[i] = \REFFUNC~F.\AMODULE.\MIFUNCS[x_0]) \\[1ex] S; F; \INITDATA~a~i~\epsilon &\stepto& S; F; \epsilon \\ diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index e798f06f..b730a898 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -7,29 +7,63 @@ Runtime Structure :ref:`Store `, :ref:`stack `, and other *runtime structure* forming the WebAssembly abstract machine, such as :ref:`values ` or :ref:`module instances `, are made precise in terms of additional auxiliary syntax. -.. index:: ! value, constant, value type, integer, floating-point +.. index:: ! value, number, reference, constant, number type, reference type, ! host address, value type, integer, floating-point, ! default value pair: abstract syntax; value +.. _syntax-num: +.. _syntax-ref: +.. _syntax-ref_func: +.. _syntax-ref_host: .. _syntax-val: Values ~~~~~~ -WebAssembly computations manipulate *values* of the four basic :ref:`value types `: :ref:`integers ` and :ref:`floating-point data ` of 32 or 64 bit width each, respectively. +WebAssembly computations manipulate *values* of either the four basic :ref:`number types `, i.e., :ref:`integers ` and :ref:`floating-point data ` of 32 or 64 bit width each, or of :ref:`reference type `. In most places of the semantics, values of different types can occur. In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit. -It is convenient to reuse the same notation as for the |CONST| :ref:`instructions ` producing them: +It is convenient to reuse the same notation as for the |CONST| :ref:`instructions ` and |REFNULL| producing them. + +References other than null are represented with additional :ref:`administrative instructions `. +They either are *function references*, pointing to a specific :ref:`function address `, +or *host references* pointing to an uninterpreted form of :ref:`host address ` that can be defined by the :ref:`embedder `. .. math:: \begin{array}{llcl} - \production{(value)} & \val &::=& + \production{(number)} & \num &::=& \I32.\CONST~\i32 \\&&|& \I64.\CONST~\i64 \\&&|& \F32.\CONST~\f32 \\&&|& - \F64.\CONST~\f64 + \F64.\CONST~\f64 \\ + \production{(reference)} & \reff &::=& + \REFNULL \\&&|& + \REFFUNC~\funcaddr \\&&|& + \REFHOST~\hostaddr \\ + \production{(value)} & \val &::=& + \num ~|~ \reff \\ + \end{array} + +.. note:: + Future versions of WebAssembly may add additional forms of reference. + +.. _default-val: + +Each :ref:`value type ` has an associated *default value*; +it is the respective value :math:`0` for :ref:`number types ` and null for :ref:`reference types `. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \default_t &=& t{.}\CONST~0 & (\iff t = \numtype) \\ + \default_t &=& \REFNULL & (\iff t = \reftype) \\ \end{array} +Convention +.......... + +* The meta variable :math:`r` ranges over reference values where clear from context. + + .. index:: ! result, value, trap pair: abstract syntax; result .. _syntax-result: @@ -92,14 +126,17 @@ Convention pair: abstract syntax; table address pair: abstract syntax; memory address pair: abstract syntax; global address + pair: abstract syntax; host address pair: function; address pair: table; address pair: memory; address pair: global; address + pair: host; address .. _syntax-funcaddr: .. _syntax-tableaddr: .. _syntax-memaddr: .. _syntax-globaladdr: +.. _syntax-hostaddr: .. _syntax-addr: Addresses @@ -107,6 +144,7 @@ Addresses :ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, and :ref:`global instances ` in the :ref:`store ` are referenced with abstract *addresses*. These are simply indices into the respective store component. +In addition, an :ref:`embedder ` may supply an uninterpreted set of *host addresses*. .. math:: \begin{array}{llll} @@ -120,6 +158,8 @@ These are simply indices into the respective store component. \addr \\ \production{(global address)} & \globaladdr &::=& \addr \\ + \production{(host address)} & \hostaddr &::=& + \addr \\ \end{array} An :ref:`embedder ` may assign identity to :ref:`exported ` store objects corresponding to their addresses, @@ -212,22 +252,17 @@ Table Instances A *table instance* is the runtime representation of a :ref:`table `. It holds a vector of *function elements* and an optional maximum size, if one was specified in the :ref:`table type ` at the table's definition site. -Each function element is either empty, representing an uninitialized table entry, or a :ref:`function address `. -Function elements can be mutated through the execution of an :ref:`element segment ` or by external means provided by the :ref:`embedder `. +Each table element is a :ref:`reference value `. +Table elements can be mutated through :ref:`table instructions `, the execution of an :ref:`element segment `, or by external means provided by the :ref:`embedder `. .. math:: \begin{array}{llll} \production{(table instance)} & \tableinst &::=& - \{ \TIELEM~\vec(\funcelem), \TIMAX~\u32^? \} \\ - \production{(function element)} & \funcelem &::=& - \funcaddr^? \\ + \{ \TIELEM~\vec(\reff), \TIMAX~\u32^? \} \\ \end{array} It is an invariant of the semantics that the length of the element vector never exceeds the maximum size, if present. -.. note:: - Other table elements may be added in future versions of WebAssembly. - .. index:: ! memory instance, memory, byte, ! page size, memory type, embedder, data segment, instruction pair: abstract syntax; memory instance @@ -442,6 +477,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`calls `. + The |INVOKE| instruction represents the imminent invocation of a :ref:`function instance `, identified by its :ref:`address `. It unifies the handling of different forms of calls. diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 060933bf..3fc2996e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -166,6 +166,30 @@ Occasionally, it is convenient to group operators together according to the foll \end{array} +.. index:: ! reference instruction, reference, null + pair: abstract syntax; instruction +.. _syntax-ref_null: +.. _syntax-ref_isnull: +.. _syntax-ref_eq: +.. _syntax-instr-ref: + +Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~ + +Instructions in this group are concerned with accessing :ref:`references `. + +.. math:: + \begin{array}{llcl} + \production{instruction} & \instr &::=& + \dots \\&&|& + \REFNULL \\&&|& + \REFISNULL \\&&|& + \REFEQ \\ + \end{array} + +These instruction produce a null value, check for a null value, or compare two references, respectively. + + .. index:: ! parametric instruction, value type pair: abstract syntax; instruction .. _syntax-instr-parametric: @@ -212,6 +236,30 @@ These instructions get or set the values of variables, respectively. The |TEELOCAL| instruction is like |SETLOCAL| but also returns its argument. +.. index:: ! table instruction, table, table index, trap + pair: abstract syntax; instruction +.. _syntax-get_table: +.. _syntax-set_table: +.. _syntax-instr-table: + +Table Instructions +~~~~~~~~~~~~~~~~~~ + +Instructions in this group are concerned with accessing :ref:`tables `. + +.. math:: + \begin{array}{llcl} + \production{instruction} & \instr &::=& + \dots \\&&|& + \GETTABLE~\tableidx \\&&|& + \SETTABLE~\tableidx \\ + \end{array} + +These instructions get or set an element in a table, respectively. + +An additional instruction that accesses a table is the :ref:`control instruction ` |CALLINDIRECT|. + + .. index:: ! memory instruction, memory, memory index, page size, little endian, trap pair: abstract syntax; instruction .. _syntax-loadn: @@ -301,7 +349,7 @@ Instructions in this group affect the flow of control. \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& \RETURN \\&&|& \CALL~\funcidx \\&&|& - \CALLINDIRECT~\typeidx \\ + \CALLINDIRECT~\tableidx~\typeidx \\ \end{array} The |NOP| instruction does nothing. @@ -340,14 +388,9 @@ Taking a branch *unwinds* the operand stack up to the height where the targeted However, forward branches that target a control instruction with a non-empty result type consume matching operands first and push them back on the operand stack after unwinding, as a result for the terminated structured instruction. The |CALL| instruction invokes another :ref:`function `, consuming the necessary arguments from the stack and returning the result values of the call. -The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table `. -Since tables may contain function elements of heterogeneous type |ANYFUNC|, -the callee is dynamically checked against the :ref:`function type ` indexed by the instruction's immediate, and the call aborted with a :ref:`trap ` if it does not match. - -.. note:: - In the current version of WebAssembly, - |CALLINDIRECT| implicitly operates on :ref:`table ` :ref:`index ` :math:`0`. - This restriction may be lifted in future versions. +The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must have type |ANYFUNC|. +Since it may contain functions of heterogeneous type, +the callee is dynamically checked against the :ref:`function type ` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap ` if it does not match. .. index:: ! expression, constant, global, offset, element, data, instruction diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index fe2b3cd7..ae285b64 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -147,7 +147,7 @@ The |MTABLES| component of a module defines a vector of *tables* described by th \{ \TTYPE~\tabletype \} \\ \end{array} -A table is a vector of opaque values of a particular table :ref:`element type `. +A table is a vector of opaque values of a particular :ref:`reference type `. The |LMIN| size in the :ref:`limits ` of the table type specifies the initial size of that table, while its |LMAX|, if present, restricts the size to which it can grow later. Tables can be initialized through :ref:`element segments `. @@ -237,8 +237,8 @@ The |MELEM| component of a module defines a vector of *element segments* that in The |EOFFSET| is given by a :ref:`constant ` :ref:`expression `. .. note:: - In the current version of WebAssembly, at most one table is allowed in a module. - Consequently, the only valid |tableidx| is :math:`0`. + In the current version of WebAssembly, only tables of element type |ANYFUNC| can be initialized with an element segment. + This limitation may be lifted in the future. .. index:: ! data, memory, memory index, expression, constant, byte, vector diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 6898fb59..9749b97d 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -9,19 +9,19 @@ Various entitites in WebAssembly are classified by types. Types are checked during :ref:`validation `, :ref:`instantiation `, and possibly :ref:`execution `. -.. index:: ! value type, integer, floating-point, IEEE 754, bit width - pair: abstract syntax; value type - pair: value; type -.. _syntax-valtype: +.. index:: ! number type, integer, floating-point, IEEE 754, bit width, memory + pair: abstract syntax; number type + pair: number; type +.. _syntax-numtype: -Value Types -~~~~~~~~~~~ +Number Types +~~~~~~~~~~~~ -*Value types* classify the individual values that WebAssembly code can compute with and the values that a variable accepts. +*Number types* classify numeric values. .. math:: \begin{array}{llll} - \production{value type} & \valtype &::=& + \production{number type} & \numtype &::=& \I32 ~|~ \I64 ~|~ \F32 ~|~ \F64 \\ \end{array} @@ -31,15 +31,73 @@ Integers are not inherently signed or unsigned, their interpretation is determin The types |F32| and |F64| classify 32 and 64 bit floating-point data, respectively. They correspond to the respective binary floating-point representations, also known as *single* and *double* precision, as defined by the |IEEE754|_ standard (Section 3.3). +Number types are *transparent*, meaning that their bit patterns can be observed. +Values of number type can be stored in :ref:`memories `. + Conventions ........... -* The meta variable :math:`t` ranges over value types where clear from context. - -* The notation :math:`|t|` denotes the *bit width* of a value type. +* The notation :math:`|t|` denotes the *bit width* of a number type :math:`t`. That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`. +.. index:: ! reference type, reference, table, function, function type, null + pair: abstract syntax; reference type + pair: reference; type +.. _syntax-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +*Reference types* classify first-class references to objects in the runtime :ref:`store `. + +.. math:: + \begin{array}{llll} + \production{reference type} & \reftype &::=& + \ANYREF ~|~ \ANYFUNC ~|~ \ANYEQREF ~|~ \NULLREF \\ + \end{array} + +The type |ANYREF| denotes the infinite union of all references, and thereby a :ref:`supertype ` of all other reference types. + +The type |ANYFUNC| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. + +The type |ANYEQREF| denotes the infinite union of all references that can be compared for equality; +in order to avoid exposing implementation details, some reference types, such as |ANYFUNC|, do not admit equality, and therefore are not :ref:`subtypes ` of |ANYEQREF|. + +The type |NULLREF| only contains a single value: the :ref:`null ` reference. +It is a :ref:`subtype ` of all other reference types. +By virtue of not being representable in either the :ref:`binary format ` nor the :ref:`text format `, the |NULLREF| type cannot be used in a program; +it only occurs during :ref:`validation `. + +.. note:: + Future versions of WebAssembly may include reference types that do not include null and hence are not supertypes of |NULLREF|. + +Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. +Values of reference type can be stored in :ref:`tables `. + + +.. index:: ! value type, number type, reference type + pair: abstract syntax; value type + pair: value; type +.. _syntax-valtype: + +Value Types +~~~~~~~~~~~ + +*Value types* classify the individual values that WebAssembly code can compute with and the values that a variable accepts. + +.. math:: + \begin{array}{llll} + \production{value type} & \valtype &::=& + \numtype ~|~ \reftype \\ + \end{array} + +Conventions +........... + +* The meta variable :math:`t` ranges over value types or subclasses thereof where clear from context. + + .. index:: ! result type, value type, instruction, execution, block pair: abstract syntax; result type pair: result; type @@ -126,34 +184,26 @@ The limits constrain the minimum and optionally the maximum size of a memory. The limits are given in units of :ref:`page size `. -.. index:: ! table type, ! element type, limits, table, element +.. index:: ! table type, reference type, limits, table, element pair: abstract syntax; table type - pair: abstract syntax; element type pair: table; type pair: table; limits - pair: element; type -.. _syntax-elemtype: .. _syntax-tabletype: Table Types ~~~~~~~~~~~ -*Table types* classify :ref:`tables ` over elements of *element types* within a size range. +*Table types* classify :ref:`tables ` over elements of :ref:`reference type ` within a size range. .. math:: \begin{array}{llll} \production{table type} & \tabletype &::=& - \limits~\elemtype \\ - \production{element type} & \elemtype &::=& - \ANYFUNC \\ + \limits~\reftype \\ \end{array} Like memories, tables are constrained by limits for their minimum and optionally maximum size. The limits are given in numbers of entries. -The element type |ANYFUNC| is the infinite union of all :ref:`function types `. -A table of that type thus contains references to functions of heterogeneous type. - .. note:: In future versions of WebAssembly, additional element types may be introduced. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index dadd435b..ddf773a0 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -97,7 +97,7 @@ All other control instruction are represented verbatim. &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& \text{return} &\Rightarrow& \RETURN \\ &&|& \text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|& - \text{call\_indirect}~~x,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x + \text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y & (\iff I' = \{\}) \\ \end{array} @@ -118,8 +118,38 @@ The :math:`\text{else}` keyword of an :math:`\text{if}` instruction can be omitt \text{if}~~\Tlabel~~\Tresulttype~~\Tinstr^\ast~~\text{else}~~\text{end} \end{array} +Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` can be omitted, defaulting to :math:`0`. -.. index:: value type, polymorphism +.. math:: + \begin{array}{llclll} + \production{plain instruction} & + \text{call\_indirect}~~\Ttypeuse + &\equiv& + \text{call\_indirect}~~0~~\Ttypeuse + \end{array} + + +.. index:: reference instruction + pair: text format; instruction +.. _text-instr-ref: + +Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~ + +.. _text-ref_null: +.. _text-ref_isnull: +.. _text-ref_eq: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& + \text{ref.null} &\Rightarrow& \REFNULL \\ &&|& + \text{ref.isnull} &\Rightarrow& \REFISNULL \\ &&|& + \text{ref.eq} &\Rightarrow& \REFEQ \\ + \end{array} + + +.. index:: parametric instruction, value type, polymorphism pair: text format; instruction .. _text-instr-parametric: @@ -161,6 +191,24 @@ Variable Instructions \end{array} +.. index:: table instructions, table index + pair: text format; instruction +.. _text-instr-table: + +Table Instructions +~~~~~~~~~~~~~~~~~~ + +.. _text-get_table: +.. _text-set_table: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& + \text{get\_table}~~x{:}\Ttableidx_I &\Rightarrow& \GETTABLE~x \\ &&|& + \text{set\_table}~~x{:}\Ttableidx_I &\Rightarrow& \SETTABLE~x \\ + \end{array} + + .. index:: memory instruction, memory index pair: text format; instruction .. _text-instr-memory: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 24e66ff8..c718e571 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -278,8 +278,8 @@ An :ref:`element segment ` can be given inline with a table definitio .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{table}~~\Tid^?~~\Telemtype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{table}~~\Tid'~~n~~n~~\Telemtype~\text{)}~~ + \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)}~~ \text{(}~\text{elem}~~\Tid'~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tvec(\Tfuncidx)~\text{)} \\ & \qquad\qquad (\iff \Tid' = \Tid^? \neq \epsilon \vee \Tid' \idfresh) \\ @@ -471,14 +471,12 @@ Element Segments ~~~~~~~~~~~~~~~~ Element segments allow for an optional :ref:`table index ` to identify the table to initialize. -When omitted, :math:`\T{0}` is assumed. .. math:: \begin{array}{llclll} \production{element segment} & \Telem_I &::=& - \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\ - &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\ + \text{(}~\text{elem}~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ \end{array} .. note:: @@ -491,13 +489,23 @@ Abbreviations As an abbreviation, a single instruction may occur in place of the offset: -.. math: +.. math:: \begin{array}{llcll} \production{element offset} & \Tinstr &\equiv& \text{(}~\text{offset}~~\Tinstr~\text{)} \end{array} +Also, the table index can be omitted, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{element segment} & + \text{(}~\text{elem}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + &\equiv& + \text{(}~\text{elem}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + \end{array} + As another abbreviation, element segments may also be specified inline with :ref:`table ` definitions; see the respective section. @@ -535,7 +543,7 @@ Abbreviations As an abbreviation, a single instruction may occur in place of the offset: -.. math: +.. math:: \begin{array}{llcll} \production{data offset} & \Tinstr &\equiv& diff --git a/document/core/text/types.rst b/document/core/text/types.rst index de5ed5f3..1c755abd 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -5,7 +5,40 @@ Types ----- -.. index:: value type +.. index:: number type + pair: text format; number type +.. _text-numtype: + +Number Types +~~~~~~~~~~~~ + +.. math:: + \begin{array}{llcll@{\qquad\qquad}l} + \production{number type} & \Tnumtype &::=& + \text{i32} &\Rightarrow& \I32 \\ &&|& + \text{i64} &\Rightarrow& \I64 \\ &&|& + \text{f32} &\Rightarrow& \F32 \\ &&|& + \text{f64} &\Rightarrow& \F64 \\ + \end{array} + + +.. index:: reference type + pair: text format; reference type +.. _text-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +.. math:: + \begin{array}{llcll@{\qquad\qquad}l} + \production{reference type} & \Treftype &::=& + \text{anyref} &\Rightarrow& \ANYREF \\ &&|& + \text{anyfunc} &\Rightarrow& \ANYFUNC \\ &&|& + \text{anyeqref} &\Rightarrow& \ANYEQREF \\ + \end{array} + + +.. index:: value type, number type, reference type pair: text format; value type .. _text-valtype: @@ -15,10 +48,8 @@ Value Types .. math:: \begin{array}{llcll@{\qquad\qquad}l} \production{value type} & \Tvaltype &::=& - \text{i32} &\Rightarrow& \I32 \\ &&|& - \text{i64} &\Rightarrow& \I64 \\ &&|& - \text{f32} &\Rightarrow& \F32 \\ &&|& - \text{f64} &\Rightarrow& \F64 \\ + t{:}\Tnumtype &\Rightarrow& t \\ &&|& + t{:}\Treftype &\Rightarrow& t \\ \end{array} @@ -106,10 +137,8 @@ Memory Types \end{array} -.. index:: table type, element type, limits +.. index:: table type, reference type, limits pair: text format; table type - pair: text format; element type -.. _text-elemtype: .. _text-tabletype: Table Types @@ -118,14 +147,9 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Ttabletype &::=& - \X{lim}{:}\Tlimits~~\X{et}{:}\Telemtype &\Rightarrow& \X{lim}~\X{et} \\ - \production{element type} & \Telemtype &::=& - \text{anyfunc} &\Rightarrow& \ANYFUNC \\ + \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype &\Rightarrow& \X{lim}~\X{et} \\ \end{array} -.. note:: - Additional element types may be introduced in future versions of WebAssembly. - .. index:: global type, mutability, value type pair: text format; global type diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 2216694b..2038b503 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -171,7 +171,10 @@ .. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}} .. |F64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64}} -.. |ANYFUNC| mathdef:: \xref{syntax/types}{syntax-elemtype}{\K{anyfunc}} +.. |ANYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyref}} +.. |ANYFUNC| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyfunc}} +.. |ANYEQREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyeqref}} +.. |NULLREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullref}} .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} @@ -187,12 +190,13 @@ .. Types, non-terminals +.. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}} +.. |reftype| mathdef:: \xref{syntax/types}{syntax-reftype}{\X{reftype}} .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} .. |functype| mathdef:: \xref{syntax/types}{syntax-functype}{\X{functype}} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} -.. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}} .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}} .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} @@ -323,11 +327,18 @@ .. |GETGLOBAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{get\_global}} .. |SETGLOBAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{set\_global}} +.. |GETTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{get\_table}} +.. |SETTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{set\_table}} + .. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}} .. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}} .. |CURRENTMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{current\_memory}} .. |GROWMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{grow\_memory}} +.. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}} +.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}isnull}} +.. |REFEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}eq}} + .. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}} .. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}} .. |EQ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eq}} @@ -444,13 +455,14 @@ .. Types, non-terminals +.. |Bnumtype| mathdef:: \xref{binary/types}{binary-numtype}{\B{numtype}} +.. |Breftype| mathdef:: \xref{binary/types}{binary-reftype}{\B{reftype}} .. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}} .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} .. |Bblocktype| mathdef:: \xref{binary/types}{binary-blocktype}{\B{blocktype}} .. |Bfunctype| mathdef:: \xref{binary/types}{binary-functype}{\B{functype}} .. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}} .. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}} -.. |Belemtype| mathdef:: \xref{binary/types}{binary-elemtype}{\B{elemtype}} .. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}} .. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}} .. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}} @@ -603,13 +615,14 @@ .. Types, non-terminals +.. |Tnumtype| mathdef:: \xref{text/types}{text-numtype}{\T{numtype}} +.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}} .. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}} .. |Tresulttype| mathdef:: \xref{text/types}{text-resulttype}{\T{resulttype}} .. |Tblocktype| mathdef:: \xref{text/types}{text-blocktype}{\T{blocktype}} .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}} .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}} .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}} -.. |Telemtype| mathdef:: \xref{text/types}{text-elemtype}{\T{elemtype}} .. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}} .. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}} .. |Tparam| mathdef:: \xref{text/types}{text-functype}{\T{param}} @@ -704,6 +717,8 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} +.. |matchesvaltype| mathdef:: \xref{valid/types}{match-valtype}{\leq} +.. |matchesresulttype| mathdef:: \xref{valid/types}{match-resulttype}{\leq} .. Contexts @@ -726,6 +741,11 @@ .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} +.. |vdashnumtypematch| mathdef:: \xref{valid/types}{match-numtype}{\vdash} +.. |vdashreftypematch| mathdef:: \xref{valid/types}{match-reftype}{\vdash} +.. |vdashvaltypematch| mathdef:: \xref{valid/types}{match-valtype}{\vdash} +.. |vdashresulttypematch| mathdef:: \xref{valid/types}{match-resulttype}{\vdash} + .. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash} .. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash} .. |vdashexpr| mathdef:: \xref{valid/instructions}{valid-expr}{\vdash} @@ -753,7 +773,8 @@ .. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow} .. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq} -.. |matches| mathdef:: \xref{exec/modules}{match}{\leq} +.. |matchesexterntype| mathdef:: \xref{exec/modules}{match-externtype}{\leq} +.. |matcheslimits| mathdef:: \xref{exec/modules}{match-limits}{\leq} .. Allocation @@ -776,6 +797,7 @@ .. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}} .. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}} .. |globaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\X{globaladdr}} +.. |hostaddr| mathdef:: \xref{exec/runtime}{syntax-hostaddr}{\X{hostaddr}} .. Instances, terminals @@ -863,6 +885,8 @@ .. Administrative Instructions, terminals +.. |REFFUNC| mathdef:: \xref{exec/runtime}{syntax-ref_func}{\K{ref{.}func}} +.. |REFHOST| mathdef:: \xref{exec/runtime}{syntax-ref_host}{\K{ref{.}host}} .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} .. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}} @@ -871,10 +895,17 @@ .. Values & Results, non-terminals +.. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}} +.. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}} .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}} .. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}} +.. Values, meta-functions + +.. |default| mathdef:: \xref{exec/runtime}{default-val}{\F{default}} + + .. Administrative Instructions, non-terminals .. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ffc308ff..1f415d39 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -154,6 +154,57 @@ Numeric Instructions } +.. index:: reference instructions, reference type + pair: validation; instruction + single: abstract syntax; instruction +.. _valid-instr-ref: + +Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~ + +.. _valid-ref_null: + +:math:`\REFNULL` +................ + +* The instruction is valid with type :math:`[] \to [\NULLREF]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \REFNULL : [] \to [\NULLREF] + } + + +.. _valid-ref_isnull: + +:math:`\REFISNULL` +.................. + +* The instruction is valid with type :math:`[\ANYREF] \to [\I32]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \REFISNULL : [\ANYREF] \to [\I32] + } + + +.. _valid-ref_eq: + +:math:`\REFEQ` +.............. + +* The instruction is valid with type :math:`[\ANYEQREF~\ANYEQREF] \to [\I32]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \REFEQ : [\ANYEQREF~\ANYEQREF] \to [\I32] + } + + + .. index:: parametric instructions, value type, polymorphism pair: validation; instruction single: abstract syntax; instruction @@ -298,6 +349,54 @@ Variable Instructions } + + +.. index:: table instructions, table index, context + pair: validation; instruction + single: abstract syntax; instruction +.. _valid-instr-table: + +Table Instructions +~~~~~~~~~~~~~~~~~~ + +.. _valid-get_table: + +:math:`\GETTABLE~x` +................... + +* The table :math:`C.\CTABLES[x]` must be defined in the context. + +* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. + +* Then the instruction is valid with type :math:`[\I32] \to [t]`. + +.. math:: + \frac{ + C.\CTABLES[x] = \limits~t + }{ + C \vdashinstr \GETTABLE~x : [\I32] \to [t] + } + + +.. _valid-set_table: + +:math:`\SETTABLE~x` +................... + +* The local :math:`C.\CTABLES[x]` must be defined in the context. + +* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. + +* Then the instruction is valid with type :math:`[\I32~t] \to []`. + +.. math:: + \frac{ + C.\CTABLES[x] = t + }{ + C \vdashinstr \SETTABLE~x : [\I32~t] \to [] + } + + .. index:: memory instruction, memory index, context pair: validation; instruction single: abstract syntax; instruction @@ -588,21 +687,23 @@ Control Instructions * The label :math:`C.\CLABELS[l_N]` must be defined in the context. -* Let :math:`[t^?]` be the :ref:`result type ` :math:`C.\CLABELS[l_N]`. - * For all :math:`l_i` in :math:`l^\ast`, - the label :math:`C.\CLABELS[l_i]` must be defined in the context. + the label :math:`C.\CLABELS[l_i]` must be defined in the context -* For all :math:`l_i` in :math:`l^\ast`, - :math:`C.\CLABELS[l_i]` must be :math:`t^?`. +* There must be a :ref:`result type ` :math:`[t^?]`, such that: + + * The result type :math:`t^?` :ref:`matches ` :math:`C.\CLABELS[l_i]`. + + * For all :math:`l_i` in :math:`l^\ast`, + the result type :math:`t^?` :ref:`matches ` :math:`C.\CLABELS[l_i]`. * Then the instruction is valid with type :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - (C.\CLABELS[l] = [t^?])^\ast + (\vdashresulttypematch [t^?] \matchesresulttype C.\CLABELS[l])^\ast \qquad - C.\CLABELS[l_N] = [t^?] + \vdashresulttypematch [t^?] \matchesresulttype C.\CLABELS[l_N] }{ C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^?~\I32] \to [t_2^\ast] } @@ -610,6 +711,10 @@ Control Instructions .. note:: The |BRTABLE| instruction is :ref:`stack-polymorphic `. + Furthermore, the :ref:`result type ` :math:`[t^?]` is also chosen non-deterministically in this rule. + In a :ref:`type checking algorithm `, the greatest lower bound of the involved label types can be picked as a principal type, + and it is a type error if that bound does not exist. + .. _valid-return: @@ -656,28 +761,30 @@ Control Instructions .. _valid-call_indirect: -:math:`\CALLINDIRECT~x` -....................... +:math:`\CALLINDIRECT~x~y` +......................... -* The table :math:`C.\CTABLES[0]` must be defined in the context. +* The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~\elemtype` be the :ref:`table type ` :math:`C.\CTABLES[0]`. +* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* The :ref:`element type ` :math:`\elemtype` must be |ANYFUNC|. +* The :ref:`reference type ` :math:`t` must :ref:`match ` type |ANYFUNC|. -* The type :math:`C.\CTYPES[x]` must be defined in the context. +* The type :math:`C.\CTYPES[y]` must be defined in the context. -* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. +* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[y]`. * Then the instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTABLES[0] = \limits~\ANYFUNC + C.\CTABLES[x] = \limits~t + \qquad + \vdashvaltypematch t \leq \ANYFUNC \qquad - C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] + C.\CTYPES[y] = [t_1^\ast] \to [t_2^\ast] }{ - C \vdashinstr \CALLINDIRECT~x : [t_1^\ast~\I32] \to [t_2^\ast] + C \vdashinstr \CALLINDIRECT~x~y : [t_1^\ast~\I32] \to [t_2^\ast] } @@ -713,13 +820,17 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` 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`, - such that :math:`t_2^\ast = t_0^\ast~t^\ast`. + such that :math:`t_2^\ast = t_0^\ast~{t'}^\ast` where the type sequence :math:`{t'}^\ast` is as long as :math:`t^\ast`. + +* 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]`. .. math:: \frac{ - C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~t^\ast] + C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast] + \qquad + (\vdashvaltypematch t' \matchesvaltype t)^\ast \qquad C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast] }{ @@ -782,6 +893,11 @@ Constant Expressions C \vdashinstrconst t.\CONST~c \const } \qquad + \frac{ + }{ + C \vdashinstrconst \REFNULL \const + } + \qquad \frac{ C.\CGLOBALS[x] = \CONST~t }{ diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 6dc45a68..bd91d502 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -152,9 +152,9 @@ Element segments :math:`\elem` are not classified by a type. * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~\elemtype` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* The :ref:`element type ` :math:`\elemtype` must be |ANYFUNC|. +* The :ref:`reference type ` :math:`t` must be |ANYFUNC|. * The expression :math:`\expr` must be :ref:`valid ` with :ref:`result type ` :math:`[\I32]`. @@ -501,8 +501,6 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, the segment :math:`\import_i` must be :ref:`valid ` with :ref:`external type ` :math:`\externtype'_i`. -* The length of :math:`C.\CTABLES` must not be larger than :math:`1`. - * The length of :math:`C.\CMEMS` must not be larger than :math:`1`. * All export names :math:`\export_i.\ENAME` must be different. @@ -548,8 +546,6 @@ Instead, the context :math:`C` for validation of the module's content is constru \\ C' = \{ \CGLOBALS~\X{igt}^\ast \} \qquad - |C.\CTABLES| \leq 1 - \qquad |C.\CMEMS| \leq 1 \qquad (\export.\ENAME)^\ast ~\F{disjoint} @@ -582,4 +578,4 @@ Instead, the context :math:`C` for validation of the module's content is constru The effect of defining the limited context :math:`C'` for validating the module's globals is that their initialization expressions can only access imported globals and nothing else. .. note:: - The restriction on the number of tables and memories may be lifted in future versions of WebAssembly. + The restriction on the number of memories may be lifted in future versions of WebAssembly. diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 76c6c702..2d3235c2 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -4,6 +4,8 @@ Types Most :ref:`types ` are universally valid. However, restrictions apply to :ref:`function types ` as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. +On :ref:`value types `, a simple notion of subtyping is defined. + .. index:: limits pair: validation; limits @@ -57,7 +59,7 @@ Function Types This restriction may be removed in future versions of WebAssembly. -.. index:: table type, element type, limits +.. index:: table type, reference type, limits pair: validation; table type single: abstract syntax; table type .. _valid-tabletype: @@ -65,8 +67,8 @@ Function Types Table Types ~~~~~~~~~~~ -:math:`\limits~\elemtype` -......................... +:math:`\limits~\reftype` +........................ * The limits :math:`\limits` must be :ref:`valid `. @@ -76,7 +78,7 @@ Table Types \frac{ \vdashlimits \limits \ok }{ - \vdashtabletype \limits~\elemtype \ok + \vdashtabletype \limits~\reftype \ok } @@ -121,3 +123,95 @@ Global Types }{ \vdashglobaltype \mut~\valtype \ok } + + +.. index:: subtyping + +Value Subtyping +~~~~~~~~~~~~~~~ + +.. index:: number type + +.. _match-numtype: + +Number Types +............ + +A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number type ` :math:`\numtype_2` if and only if: + +* Both :math:`\numtype_1` and :math:`\numtype_2` are the same. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + \vdashnumtypematch \numtype \matchesvaltype \numtype + } + + +.. index:: reference type + +.. _match-reftype: + +Reference Types +............... + +A :ref:`reference type ` :math:`\reftype_1` matches a :ref:`number type ` :math:`\reftype_2` if and only if: + +* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same. + +* Or :math:`\reftype_1` is |NULLREF|. + +* Or :math:`\reftype_2` is |ANYREF|. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + \vdashreftypematch \reftype \matchesvaltype \reftype + } + \qquad + \frac{ + }{ + \vdashreftypematch \NULLREF \matchesvaltype \reftype + } + \qquad + \frac{ + }{ + \vdashreftypematch \reftype \matchesvaltype \ANYREF + } + + +.. index:: value type, number type, reference type + +.. _match-valtype: + +Value Types +........... + +A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value type ` :math:`\valtype_2` if and only if: + +* Either both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`number types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + + +.. _match-resulttype: + +Result Types +............ + +Subtyping is lifted to :ref:`result types ` in a pointwise manner. +That is, a :ref:`result type ` :math:`[t_1^?]` matches a :ref:`result type ` :math:`[t_2^?]` if and only if: + +* Either both :math:`t_1^?` and :math:`t_2^?` are empty. + +* Or :ref:`value type ` :math:`t_1` :ref:`matches ` :ref:`value type ` :math:`t_2`. + +.. math:: + ~\\[-1ex] + \frac{ + (\vdashvaltypematch t_1 \matchesvaltype t_2)^? + }{ + \vdashresulttypematch [t_1^?] \matchesresulttype [t_2^?] + }