Skip to content

Commit

Permalink
[spec] Fix minor errors and inconsistencies (WebAssembly#1564)
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg committed Mar 1, 2023
1 parent 319dfe2 commit 782534c
Show file tree
Hide file tree
Showing 4 changed files with 59 additions and 57 deletions.
2 changes: 1 addition & 1 deletion document/core/appendix/properties.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
......................................................................................

* The :ref:`memory type <syntax-memtype>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-memtype>`.
* The :ref:`memory type <syntax-memtype>` :math:`\limits` must be :ref:`valid <valid-memtype>`.

* The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.

Expand Down
46 changes: 24 additions & 22 deletions document/core/exec/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1256,7 +1256,7 @@ Table Instructions
.. math::
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \TABLESIZE~x &\stepto& S; F; (\I32.\CONST~\X{sz})
S; F; (\TABLESIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz})
\end{array}
\\ \qquad
(\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\
Expand Down Expand Up @@ -1288,19 +1288,21 @@ Table Instructions

10. Pop the value :math:`\val` from the stack.

11. Either, try :ref:`growing <grow-table>` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`:
11. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`.

12. Either, try :ref:`growing <grow-table>` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`:

a. If it succeeds, push the value :math:`\I32.\CONST~\X{sz}` to the stack.

b. Else, push the value :math:`\I32.\CONST~(-1)` to the stack.
b. Else, push the value :math:`\I32.\CONST~\X{err}` to the stack.

12. Or, push the value :math:`\I32.\CONST~(-1)` to the stack.
13. Or, push the value :math:`\I32.\CONST~\X{err}` to the stack.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \val~(\I32.\CONST~n)~\TABLEGROW~x &\stepto& S'; F; (\I32.\CONST~\X{sz})
S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz})
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
Expand All @@ -1310,7 +1312,7 @@ Table Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~\TABLEGROW~x &\stepto& S; F; (\I32.\CONST~{-1})
S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
\end{array}
\end{array}
Expand Down Expand Up @@ -1511,7 +1513,7 @@ Table Instructions
\quad\stepto
\\ \qquad S; F;
\begin{array}[t]{@{}l@{}}
(\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\
(\I32.\CONST~d+n)~(\I32.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\
(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\
\end{array}
\\ \qquad
Expand Down Expand Up @@ -1722,7 +1724,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -1783,7 +1785,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -1840,7 +1842,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -1895,7 +1897,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -1957,7 +1959,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -2034,7 +2036,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -2091,7 +2093,7 @@ Memory Instructions
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~k)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP
S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise) \\
Expand Down Expand Up @@ -2376,8 +2378,8 @@ Memory Instructions
\quad\stepto
\\ \qquad S; F;
\begin{array}[t]{@{}l@{}}
(\I32.\CONST~d+n-1) \\
(\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\
(\I32.\CONST~d+n) \\
(\I32.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\
(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\
(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY~x~y \\
\end{array}
Expand Down Expand Up @@ -2687,7 +2689,7 @@ Control Instructions
:math:`\BRTABLE~l^\ast~l_N`
...........................

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

2. Pop the value :math:`\I32.\CONST~i` from the stack.

Expand Down Expand Up @@ -2866,22 +2868,22 @@ Exiting :math:`\instr^\ast` with label :math:`L`

When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.

1. Let :math:`m` be the number of values on the top of the stack.
1. Let :math:`n` be the number of values on the top of the stack.

2. Pop the values :math:`\val^m` from the stack.
2. Pop the values :math:`\val^n` from the stack.

3. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack.
3. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack and has arity :math:`n`.

4. Pop the label from the stack.

5. Push :math:`\val^m` back to the stack.
5. Push :math:`\val^n` back to the stack.

6. Jump to the position after the |END| of the :ref:`structured control instruction <syntax-instr-control>` associated with the label :math:`L`.

.. math::
~\\[-1ex]
\begin{array}{lcl@{\qquad}l}
\LABEL_n\{\instr^\ast\}~\val^m~\END &\stepto& \val^m
\LABEL_n\{\instr^\ast\}~\val^n~\END &\stepto& \val^n
\end{array}
.. note::
Expand Down
66 changes: 33 additions & 33 deletions document/core/exec/runtime.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,18 +30,18 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre

.. math::
\begin{array}{llcl}
\production{(number)} & \num &::=&
\production{number} & \num &::=&
\I32.\CONST~\i32 \\&&|&
\I64.\CONST~\i64 \\&&|&
\F32.\CONST~\f32 \\&&|&
\F64.\CONST~\f64 \\
\production{(vector)} & \vecc &::=&
\production{vector} & \vecc &::=&
\V128.\CONST~\i128 \\
\production{(reference)} & \reff &::=&
\production{reference} & \reff &::=&
\REFNULL~t \\&&|&
\REFFUNCADDR~\funcaddr \\&&|&
\REFEXTERNADDR~\externaddr \\
\production{(value)} & \val &::=&
\production{value} & \val &::=&
\num ~|~ \vecc ~|~ \reff \\
\end{array}
Expand Down Expand Up @@ -79,7 +79,7 @@ It is either a sequence of :ref:`values <syntax-val>` or a :ref:`trap <syntax-tr

.. math::
\begin{array}{llcl}
\production{(result)} & \result &::=&
\production{result} & \result &::=&
\val^\ast \\&&|&
\TRAP
\end{array}
Expand All @@ -101,7 +101,7 @@ Syntactically, the store is defined as a :ref:`record <notation-record>` listing

.. math::
\begin{array}{llll}
\production{(store)} & \store &::=& \{~
\production{store} & \store &::=& \{~
\begin{array}[t]{l@{~}ll}
\SFUNCS & \funcinst^\ast, \\
\STABLES & \tableinst^\ast, \\
Expand Down Expand Up @@ -157,21 +157,21 @@ In addition, an :ref:`embedder <embedder>` may supply an uninterpreted set of *h

.. math::
\begin{array}{llll}
\production{(address)} & \addr &::=&
\production{address} & \addr &::=&
0 ~|~ 1 ~|~ 2 ~|~ \dots \\
\production{(function address)} & \funcaddr &::=&
\production{function address} & \funcaddr &::=&
\addr \\
\production{(table address)} & \tableaddr &::=&
\production{table address} & \tableaddr &::=&
\addr \\
\production{(memory address)} & \memaddr &::=&
\production{memory address} & \memaddr &::=&
\addr \\
\production{(global address)} & \globaladdr &::=&
\production{global address} & \globaladdr &::=&
\addr \\
\production{(element address)} & \elemaddr &::=&
\production{element address} & \elemaddr &::=&
\addr \\
\production{(data address)} & \dataaddr &::=&
\production{data address} & \dataaddr &::=&
\addr \\
\production{(extern address)} & \externaddr &::=&
\production{extern address} & \externaddr &::=&
\addr \\
\end{array}
Expand Down Expand Up @@ -204,7 +204,7 @@ and collects runtime representations of all entities that are imported, defined,

.. math::
\begin{array}{llll}
\production{(module instance)} & \moduleinst &::=& \{
\production{module instance} & \moduleinst &::=& \{
\begin{array}[t]{l@{~}ll}
\MITYPES & \functype^\ast, \\
\MIFUNCS & \funcaddr^\ast, \\
Expand Down Expand Up @@ -238,10 +238,10 @@ The module instance is used to resolve references to other definitions during ex

.. math::
\begin{array}{llll}
\production{(function instance)} & \funcinst &::=&
\production{function instance} & \funcinst &::=&
\{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|&
\{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\
\production{(host function)} & \hostfunc &::=& \dots \\
\production{host function} & \hostfunc &::=& \dots \\
\end{array}
A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module <syntax-module>` as an :ref:`import <syntax-import>`.
Expand All @@ -268,7 +268,7 @@ It records its :ref:`type <syntax-tabletype>` and holds a vector of :ref:`refere

.. math::
\begin{array}{llll}
\production{(table instance)} & \tableinst &::=&
\production{table instance} & \tableinst &::=&
\{ \TITYPE~\tabletype, \TIELEM~\vec(\reff) \} \\
\end{array}
Expand All @@ -292,7 +292,7 @@ It records its :ref:`type <syntax-memtype>` and holds a vector of :ref:`bytes <s

.. math::
\begin{array}{llll}
\production{(memory instance)} & \meminst &::=&
\production{memory instance} & \meminst &::=&
\{ \MITYPE~\memtype, \MIDATA~\vec(\byte) \} \\
\end{array}
Expand All @@ -316,7 +316,7 @@ It records its :ref:`type <syntax-globaltype>` and holds an individual :ref:`val

.. math::
\begin{array}{llll}
\production{(global instance)} & \globalinst &::=&
\production{global instance} & \globalinst &::=&
\{ \GITYPE~\globaltype, \GIVALUE~\val \} \\
\end{array}
Expand All @@ -338,7 +338,7 @@ It holds a vector of references and their common :ref:`type <syntax-reftype>`.

.. math::
\begin{array}{llll}
\production{(element instance)} & \eleminst &::=&
\production{element instance} & \eleminst &::=&
\{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\
\end{array}
Expand All @@ -356,7 +356,7 @@ It holds a vector of :ref:`bytes <syntax-byte>`.

.. math::
\begin{array}{llll}
\production{(data instance)} & \datainst &::=&
\production{data instance} & \datainst &::=&
\{ \DIDATA~\vec(\byte) \} \\
\end{array}
Expand All @@ -374,7 +374,7 @@ It defines the export's :ref:`name <syntax-name>` and the associated :ref:`exter

.. math::
\begin{array}{llll}
\production{(export instance)} & \exportinst &::=&
\production{export instance} & \exportinst &::=&
\{ \EINAME~\name, \EIVALUE~\externval \} \\
\end{array}
Expand All @@ -392,7 +392,7 @@ It is an :ref:`address <syntax-addr>` denoting either a :ref:`function instance

.. math::
\begin{array}{llcl}
\production{(external value)} & \externval &::=&
\production{external value} & \externval &::=&
\EVFUNC~\funcaddr \\&&|&
\EVTABLE~\tableaddr \\&&|&
\EVMEM~\memaddr \\&&|&
Expand Down Expand Up @@ -456,7 +456,7 @@ Labels carry an argument arity :math:`n` and their associated branch *target*, w

.. math::
\begin{array}{llll}
\production{(label)} & \label &::=&
\production{label} & \label &::=&
\LABEL_n\{\instr^\ast\} \\
\end{array}
Expand Down Expand Up @@ -485,9 +485,9 @@ and a reference to the function's own :ref:`module instance <syntax-moduleinst>`

.. math::
\begin{array}{llll}
\production{(activation)} & \X{activation} &::=&
\production{activation} & \X{activation} &::=&
\FRAME_n\{\frame\} \\
\production{(frame)} & \frame &::=&
\production{frame} & \frame &::=&
\{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\
\end{array}
Expand Down Expand Up @@ -529,7 +529,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca

.. math::
\begin{array}{llcl}
\production{(administrative instruction)} & \instr &::=&
\production{administrative instruction} & \instr &::=&
\dots \\ &&|&
\TRAP \\ &&|&
\REFFUNCADDR~\funcaddr \\ &&|&
Expand Down Expand Up @@ -590,9 +590,9 @@ In order to specify the reduction of :ref:`branches <syntax-instr-control>`, the

.. math::
\begin{array}{llll}
\production{(block contexts)} & \XB^0 &::=&
\production{block contexts} & \XB^0 &::=&
\val^\ast~[\_]~\instr^\ast \\
\production{(block contexts)} & \XB^{k+1} &::=&
\production{block contexts} & \XB^{k+1} &::=&
\val^\ast~\LABEL_n\{\instr^\ast\}~\XB^k~\END~\instr^\ast \\
\end{array}
Expand Down Expand Up @@ -624,9 +624,9 @@ that operates relative to a current :ref:`frame <syntax-frame>` referring to the

.. math::
\begin{array}{llcl}
\production{(configuration)} & \config &::=&
\production{configuration} & \config &::=&
\store; \thread \\
\production{(thread)} & \thread &::=&
\production{thread} & \thread &::=&
\frame; \instr^\ast \\
\end{array}
Expand All @@ -645,7 +645,7 @@ Finally, the following definition of *evaluation context* and associated structu

.. math::
\begin{array}{llll}
\production{(evaluation contexts)} & E &::=&
\production{evaluation contexts} & E &::=&
[\_] ~|~
\val^\ast~E~\instr^\ast ~|~
\LABEL_n\{\instr^\ast\}~E~\END \\
Expand Down
Loading

0 comments on commit 782534c

Please sign in to comment.