Skip to content

Commit

Permalink
Merge with WebAssembly/spec, WebAssembly/function-references, and Web…
Browse files Browse the repository at this point in the history
…Assembly/gc
  • Loading branch information
dhil committed Dec 6, 2023
2 parents 50b8d7d + c7eef19 commit b77ab8d
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 13 deletions.
16 changes: 8 additions & 8 deletions document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -2000,9 +2000,9 @@ Most other vector instructions are defined in terms of numeric operators that ar

1. Assert: due to :ref:`validation <valid-vtestop>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.

2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
2. Pop the value :math:`\V128.\VCONST~c` from the stack.

3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`.
3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c)`.

4. Let :math:`i` be the result of computing :math:`\tobool(\bigwedge(i_1 \neq 0)^\ast)`.

Expand All @@ -2012,7 +2012,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
.. math::
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
(\V128\K{.}\VCONST~c_1)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i)
(\V128\K{.}\VCONST~c)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i)
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
Expand All @@ -2029,7 +2029,7 @@ Most other vector instructions are defined in terms of numeric operators that ar

1. Assert: due to :ref:`validation <valid-vec-bitmask>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.

2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
2. Pop the value :math:`\V128.\VCONST~c` from the stack.

3. Let :math:`i_1^N` be the result of computing :math:`\lanes_{t\K{x}N}(c)`.

Expand All @@ -2039,14 +2039,14 @@ Most other vector instructions are defined in terms of numeric operators that ar

6. Let :math:`j^\ast` be the concatenation of the two sequences :math:`i_2^N` and :math:`0^{32-N}`.

7. Let :math:`c` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`.
7. Let :math:`i` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`.

8. Push the value :math:`\I32.\CONST~c` onto the stack.
8. Push the value :math:`\I32.\CONST~i` onto the stack.

.. math::
\begin{array}{lcl@{\qquad}l}
(\V128\K{.}\VCONST~c_1)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~c)
& (\iff c = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N)))
(\V128\K{.}\VCONST~c)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~i)
& (\iff i = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N)))
\\
\end{array}
Expand Down
15 changes: 10 additions & 5 deletions document/core/valid/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -1972,17 +1972,22 @@ Control Instructions
...........................


* The label :math:`C.\CLABELS[l_N]` must be defined in the context.
* The :ref:`label <syntax-label>` :math:`C.\CLABELS[l_N]` must be defined in the context.

* For all :math:`l_i` in :math:`l^\ast`,
* For each :ref:`label <syntax-label>` :math:`l_i` in :math:`l^\ast`,
the label :math:`C.\CLABELS[l_i]` must be defined in the context.

* There must be a sequence :math:`t^\ast` of :ref:`value types <syntax-valtype>`, such that:

* The result type :math:`[t^\ast]` :ref:`matches <match-resulttype>` :math:`C.\CLABELS[l_N]`.
* The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_N]`.

* For all :math:`l_i` in :math:`l^\ast`,
the result type :math:`[t^\ast]` :ref:`matches <match-resulttype>` :math:`C.\CLABELS[l_i]`.
* For each :ref:`operand type <syntax-opdtype>` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{Nj}` in :math:`C.\CLABELS[l_N]`, :math:`t_j` :ref:`matches <match-opdtype>` :math:`t'_{Nj}`.

* For each :ref:`label <syntax-label>` :math:`l_i` in :math:`l^\ast`:

* The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_i]`.

* For each :ref:`operand type <syntax-opdtype>` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches <match-opdtype>` :math:`t'_{ij}`.

* Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`.

Expand Down

0 comments on commit b77ab8d

Please sign in to comment.