Merge pull request #1 from WebAssembly/spec

document/core/binary/instructions.rst

@@ -13,15 +13,19 @@ The only exception are :ref:`structured control instructions <binary-instr-contr
    Gaps in the byte code ranges for encoding instructions are reserved for future extensions.
 
 
-.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism
+.. index:: control instructions, structured control, label, block, branch, result type, value type, block type, label index, function index, type index, vector, polymorphism, LEB128
    pair: binary format; instruction
+   pair: binary format; block type
 .. _binary-instr-control:
 
 Control Instructions
 ~~~~~~~~~~~~~~~~~~~~
 
 :ref:`Control instructions <syntax-instr-control>` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END| and |ELSE|.
 
+:ref:`Block types <syntax-blocktype>` are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type, as a single :ref:`value type <binary-valtype>`, or as a :ref:`type index <binary-typeidx>` encoded as a positive :ref:`signed integer <binary-sint>`.
+
+.. _binary-blocktype:
 .. _binary-nop:
 .. _binary-unreachable:
 .. _binary-block:
@@ -36,18 +40,22 @@ Control Instructions
 
 .. math::
    \begin{array}{llclll}
+   \production{block type} & \Bblocktype &::=&
+     \hex{40} &\Rightarrow& \epsilon \\ &&|&
+     t{:}\Bvaltype &\Rightarrow& t \\ &&|&
+     x{:}\Bs33 &\Rightarrow& x \\
    \production{instruction} & \Binstr &::=&
      \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|&
      \hex{01} &\Rightarrow& \NOP \\ &&|&
-     \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
-       &\Rightarrow& \BLOCK~\X{rt}~\X{in}^\ast~\END \\ &&|&
-     \hex{03}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
-       &\Rightarrow& \LOOP~\X{rt}~\X{in}^\ast~\END \\ &&|&
-     \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
-       &\Rightarrow& \IF~\X{rt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|&
-     \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~
+     \hex{02}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
+       &\Rightarrow& \BLOCK~\X{bt}~\X{in}^\ast~\END \\ &&|&
+     \hex{03}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
+       &\Rightarrow& \LOOP~\X{bt}~\X{in}^\ast~\END \\ &&|&
+     \hex{04}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B}
+       &\Rightarrow& \IF~\X{bt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|&
+     \hex{04}~~\X{bt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~
        \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B}
-       &\Rightarrow& \IF~\X{rt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|&
+       &\Rightarrow& \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|&
      \hex{0C}~~l{:}\Blabelidx &\Rightarrow& \BR~l \\ &&|&
      \hex{0D}~~l{:}\Blabelidx &\Rightarrow& \BRIF~l \\ &&|&
      \hex{0E}~~l^\ast{:}\Bvec(\Blabelidx)~~l_N{:}\Blabelidx
@@ -60,6 +68,10 @@ Control Instructions
 .. note::
    The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty.
 
+   Unlike any :ref:`other occurrence <binary-typeidx>`, the :ref:`type index <syntax-typeidx>` in a :ref:`block type <syntax-blocktype>` is encoded as a positive :ref:`signed integer <syntax-sint>`, so that its `LEB128 <https://en.wikipedia.org/wiki/LEB128#Signed_LEB128>`_ bit pattern cannot collide with the encoding of :ref:`value types <binary-valtype>` or the special code :math:`\hex{40}`, which correspond to the LEB128 encoding of negative integers.
+   To avoid any loss in the range of allowed indices, it is treated as a 33 bit signed integer. 
+
+
 
 .. index:: value type, polymorphism
    pair: binary format; instruction

document/core/binary/types.rst

@@ -24,30 +24,25 @@ Value Types
    \end{array}
 
 .. note::
-   In future versions of WebAssembly, value types may include types denoted by :ref:`type indices <syntax-typeidx>`.
-   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 can occur in contexts where :ref:`type indices <syntax-typeidx>` are also allowed, such as in the case of :ref:`block types <binary-blocktype>`.
+   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 be distinguished from (positive) type indices.
 
 
 .. index:: result type, value type
    pair: binary format; result type
-.. _binary-blocktype:
 .. _binary-resulttype:
 
 Result Types
 ~~~~~~~~~~~~
 
-The only :ref:`result types <syntax-resulttype>` occurring in the binary format are the types of blocks. These are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type or as a single :ref:`value type <binary-valtype>`.
+:ref:`Result types <syntax-resulttype>` are encoded by the respective :ref:`vectors <binary-vec>` of :ref:`value types `<binary-valtype>`.
 
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
-   \production{result type} & \Bblocktype &::=&
-     \hex{40} &\Rightarrow& [] \\ &&|&
-     t{:}\Bvaltype &\Rightarrow& [t] \\
+   \production{result type} & \Bresulttype &::=&
+     t^\ast{:\,}\Bvec(\Bvaltype) &\Rightarrow& [t^\ast] \\
    \end{array}
 
-.. note::
-   In future versions of WebAssembly, this scheme may be extended to support multiple results or more general block types.
-
 
 .. index:: function type, value type, result type
    pair: binary format; function type
@@ -61,8 +56,8 @@ Function Types
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{function type} & \Bfunctype &::=&
-     \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype)
-       &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\
+     \hex{60}~~\X{rt}_1{:\,}\Bresulttype~~\X{rt}_2{:\,}\Bresulttype
+       &\Rightarrow& \X{rt}_1 \to \X{rt}_2 \\
    \end{array}
 
 

document/core/exec/instructions.rst

@@ -651,70 +651,80 @@ Control Instructions
 
 .. _exec-block:
 
-:math:`\BLOCK~[t^?]~\instr^\ast~\END`
-.....................................
+:math:`\BLOCK~\blocktype~\instr^\ast~\END`
+..........................................
 
-1. Let :math:`n` be the arity :math:`|t^?|` of the :ref:`result type <syntax-resulttype>` :math:`t^?`.
+1. Assert: due to :ref:`validation <valid-blocktype>`, :math:`\expand_F(\blocktype)` is defined.
 
-2. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the block.
+2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type <syntax-functype>` :math:`\expand_F(\blocktype)`.
 
-3. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr^\ast` with label :math:`L`.
+3. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the block.
+
+4. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   \BLOCK~[t^n]~\instr^\ast~\END &\stepto&
-     \LABEL_n\{\epsilon\}~\instr^\ast~\END
+   F; \BLOCK~\X{bt}~\instr^\ast~\END &\stepto&
+     F; \LABEL_n\{\epsilon\}~\instr^\ast~\END
+     & (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
    \end{array}
 
 
 .. _exec-loop:
 
-:math:`\LOOP~[t^?]~\instr^\ast~\END`
-....................................
+:math:`\LOOP~\blocktype~\instr^\ast~\END`
+.........................................
+
+1. Assert: due to :ref:`validation <valid-blocktype>`, :math:`\expand_F(\blocktype)` is defined.
+
+2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type <syntax-functype>` :math:`\expand_F(\blocktype)`.
 
-1. Let :math:`L` be the label whose arity is :math:`0` and whose continuation is the start of the loop.
+3. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the start of the loop.
 
-2. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr^\ast` with label :math:`L`.
+4. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   \LOOP~[t^?]~\instr^\ast~\END &\stepto&
-     \LABEL_0\{\LOOP~[t^?]~\instr^\ast~\END\}~\instr^\ast~\END
+   F; \LOOP~\X{bt}~\instr^\ast~\END &\stepto&
+     F; \LABEL_m\{\LOOP~\X{bt}~\instr^\ast~\END\}~\instr^\ast~\END
+     & (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
    \end{array}
 
 
 .. _exec-if:
 
-:math:`\IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END`
-........................................................
+:math:`\IF~\blocktype~\instr_1^\ast~\ELSE~\instr_2^\ast~\END`
+.............................................................
 
-1. Assert: due to :ref:`validation <valid-if>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-blocktype>`, :math:`\expand_F(\blocktype)` is defined.
 
-2. Pop the value :math:`\I32.\CONST~c` from the stack.
+2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type <syntax-functype>` :math:`\expand_F(\blocktype)`.
 
-3. Let :math:`n` be the arity :math:`|t^?|` of the :ref:`result type <syntax-resulttype>` :math:`t^?`.
+3. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the |IF| instruction.
 
-4. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the |IF| instruction.
+4. Assert: due to :ref:`validation <valid-if>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
 
-5. If :math:`c` is non-zero, then:
+5. Pop the value :math:`\I32.\CONST~c` from the stack.
+
+6. If :math:`c` is non-zero, then:
 
    a. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr_1^\ast` with label :math:`L`.
 
-6. Else:
+7. Else:
 
    a. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr_2^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   (\I32.\CONST~c)~\IF~[t^n]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
-     \LABEL_n\{\epsilon\}~\instr_1^\ast~\END
-     & (\iff c \neq 0) \\
-   (\I32.\CONST~c)~\IF~[t^n]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
-     \LABEL_n\{\epsilon\}~\instr_2^\ast~\END
-     & (\iff c = 0) \\
+   F; (\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
+     F; \LABEL_n\{\epsilon\}~\instr_1^\ast~\END
+     & (\iff c \neq 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
+   F; (\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
+     F; \LABEL_n\{\epsilon\}~\instr_2^\ast~\END
+     & (\iff c = 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
    \end{array}
 
 
@@ -1021,13 +1031,15 @@ Invocation of :ref:`function address <syntax-funcaddr>` :math:`a`
 
 10. Push the activation of :math:`F` with arity :math:`m` to the stack.
 
-11. :ref:`Execute <exec-block>` the instruction :math:`\BLOCK~[t_2^m]~\instr^\ast~\END`.
+11. Let :math:`L` be the :ref:`label <syntax-label>` whose arity is :math:`m` and whose continuation is the end of the function.
+
+12. :ref:`Enter <exec-instr-seq-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S; \FRAME_m\{F\}~\BLOCK~[t_2^m]~\instr^\ast~\END~\END
+   S; \val^n~(\INVOKE~a) &\stepto& S; \FRAME_m\{F\}~\LABEL_m\{\}~\instr^\ast~\END~\END
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}

document/core/exec/runtime.rst

@@ -307,13 +307,7 @@ It filters out entries of a specific kind in an order-preserving fashion:
 * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]`
 
 
-.. index:: ! stack, ! frame, ! label, instruction, store, activation, function, call, local, module instance
-   pair: abstract syntax; frame
-   pair: abstract syntax; label
-.. _syntax-frame:
-.. _syntax-label:
-.. _frame:
-.. _label:
+.. index:: ! stack, frame, label, instruction, store, activation, function, call, local, module instance
 .. _stack:
 
 Stack
@@ -342,6 +336,12 @@ Values
 
 Values are represented by :ref:`themselves <syntax-val>`.
 
+
+.. index:: ! label, instruction
+   pair: abstract syntax; label
+.. _syntax-label:
+.. _label:
+
 Labels
 ......
 
@@ -359,7 +359,7 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc
    For example, a loop label has the form
 
    .. math::
-      \LABEL_n\{\LOOP~[t^?]~\dots~\END\}
+      \LABEL_n\{\LOOP~\dots~\END\}
 
    When performing a branch to this label, this executes the loop, effectively restarting it from the beginning.
    Conversely, a simple block label has the form
@@ -369,6 +369,12 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc
 
    When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
 
+
+.. index:: ! frame, instruction, activation, local, module instance
+   pair: abstract syntax; frame
+.. _syntax-frame:
+.. _frame:
+
 Frames
 ......
 
@@ -394,9 +400,13 @@ Conventions
 
 * The meta variable :math:`F` ranges over frames where clear from context.
 
-.. note::
-   In the current version of WebAssembly, the arities of labels and frames cannot be larger than :math:`1`.
-   This may be generalized in future versions.
+* The following auxiliary definition takes a :ref:`block type <syntax-blocktype>` and looks up the :ref:`function type <syntax-functype>` that it denotes in the current frame:
+
+.. math::
+   \begin{array}{lll}
+   \expand_F(\typeidx) &=& F.\AMODULE.\MITYPES[\typeidx] \\
+   \expand_F([\valtype^?]) &=& [] \to [\valtype^?] \\
+   \end{array}
 
 
 .. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call