Skip to content

Commit

Permalink
[spec/interpreter/test] Add table bulk instructions missing from bulk…
Browse files Browse the repository at this point in the history
… op proposal (WebAssembly#35)

Adds table.size, table.grow, table.fill to overview, spec, interpreter, and tests, as decided at recent CG meeting. Also adds a few more tests for table.get and table.set.

Also, change interpreter's segment encoding to match bulk ops proposal, addressing WebAssembly#18. (Not updated in spec yet, since corresponding spec text is still missing from bulk ops proposal.)
  • Loading branch information
rossberg authored Apr 3, 2019
1 parent ef6678a commit c3d5cbc
Show file tree
Hide file tree
Showing 29 changed files with 975 additions and 70 deletions.
16 changes: 8 additions & 8 deletions document/core/appendix/embedding.rst
Original file line number Diff line number Diff line change
Expand Up @@ -294,16 +294,16 @@ Tables

.. _embed-alloc-table:

:math:`\F{alloc\_table}(\store, \tabletype) : (\store, \tableaddr)`
...................................................................
:math:`\F{alloc\_table}(\store, \tabletype) : (\store, \tableaddr, \val)`
.........................................................................

1. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype`.

2. Return the new store paired with :math:`\tableaddr`.

.. math::
\begin{array}{lclll}
\F{alloc\_table}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\
\F{alloc\_table}(S, \X{tt}, v) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}, v) = S', \X{a}) \\
\end{array}
Expand Down Expand Up @@ -390,8 +390,8 @@ Tables
.. _embed-grow-table:

:math:`\F{grow\_table}(\store, \tableaddr, n) : \store ~|~ \error`
..................................................................
:math:`\F{grow\_table}(\store, \tableaddr, n, \val) : \store ~|~ \error`
........................................................................

1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.

Expand All @@ -406,9 +406,9 @@ Tables
.. math::
~ \\
\begin{array}{lclll}
\F{grow\_table}(S, a, n) &=& S' &&
(\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n)) \\
\F{grow\_table}(S, a, n) &=& \ERROR && (\otherwise) \\
\F{grow\_table}(S, a, n, v) &=& S' &&
(\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, v)) \\
\F{grow\_table}(S, a, n, v) &=& \ERROR && (\otherwise) \\
\end{array}
Expand Down
13 changes: 8 additions & 5 deletions document/core/binary/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -138,21 +138,24 @@ Variable Instructions
Table Instructions
~~~~~~~~~~~~~~~~~~

:ref:`Table instructions <syntax-instr-table>` are represented by single byte codes.
:ref:`Table instructions <syntax-instr-table>` are represented by either single byte or two byte codes.

.. _binary-table.get:
.. _binary-table.set:
.. _binary-table.size:
.. _binary-table.grow:
.. _binary-table.fill:

.. math::
\begin{array}{llclll}
\production{instruction} & \Binstr &::=& \dots \\ &&|&
\hex{25}~~x{:}\Btableidx &\Rightarrow& \TABLEGET~x \\ &&|&
\hex{26}~~x{:}\Btableidx &\Rightarrow& \TABLESET~x \\
\hex{26}~~x{:}\Btableidx &\Rightarrow& \TABLESET~x \\ &&|&
\hex{FC}~\hex{0F}~~x{:}\Btableidx &\Rightarrow& \TABLEGROW~x \\ &&|&
\hex{FC}~\hex{10}~~x{:}\Btableidx &\Rightarrow& \TABLESIZE~x \\ &&|&
\hex{FC}~\hex{11}~~x{:}\Btableidx &\Rightarrow& \TABLEFILL~x \\
\end{array}
.. note::
These opcode assignments are preliminary.

.. index:: memory instruction, memory index
pair: binary format; instruction
Expand Down
156 changes: 156 additions & 0 deletions document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -522,6 +522,162 @@ Table Instructions
\end{array}
.. _exec-table.size:

:math:`\TABLESIZE~x`
....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.size>`, :math:`F.\AMODULE.\MITABLES[x]` exists.

3. Let :math:`a` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[x]`.

4. Assert: due to :ref:`validation <valid-table.size>`, :math:`S.\STABLES[a]` exists.

5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.

6. Let :math:`\X{sz}` be the length of :math:`\X{tab}.\TIELEM`.

7. Push the value :math:`\I32.\CONST~\X{sz}` to the stack.

.. math::
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \TABLESIZE~x &\stepto& S; F; (\I32.\CONST~\X{sz})
\end{array}
\\ \qquad
(\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\
\end{array}
.. _exec-table.grow:

:math:`\TABLEGROW~x`
....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.grow>`, :math:`F.\AMODULE.\MITABLES[x]` exists.

3. Let :math:`a` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[x]`.

4. Assert: due to :ref:`validation <valid-table.grow>`, :math:`S.\STABLES[a]` exists.

5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.

6. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`.

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

8. Pop the value :math:`\I32.\CONST~n` from the stack.

9. Assert: due to :ref:`validation <valid-table.fill>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.

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`:

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.

12. Or, push the value :math:`\I32.\CONST~(-1)` 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})
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MITABLES[x] = a \\
\wedge & \X{sz} = |S.\STABLES[a].\TIELEM| \\
\wedge & S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, \val)) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~\TABLEGROW~x &\stepto& S; F; (\I32.\CONST~{-1})
\end{array}
\end{array}
.. note::
The |TABLEGROW| instruction is non-deterministic.
It may either succeed, returning the old table size :math:`\X{sz}`,
or fail, returning :math:`{-1}`.
Failure *must* occur if the referenced table instance has a maximum size defined that would be exceeded.
However, failure *can* occur in other cases as well.
In practice, the choice depends on the :ref:`resources <impl-exec>` available to the :ref:`embedder <embedder>`.


.. _exec-table.fill:

:math:`\TABLEFILL~x`
....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-table.fill>`, :math:`F.\AMODULE.\MITABLES[x]` exists.

3. Let :math:`a` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[x]`.

4. Assert: due to :ref:`validation <valid-table.fill>`, :math:`S.\STABLES[a]` exists.

5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.

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

7. Pop the value :math:`\I32.\CONST~n` from the stack.

8. Assert: due to :ref:`validation <valid-table.fill>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.

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

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

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

12. If :math:`n` is :math:`0`, then:

a. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:

i. Trap.

12. Else:

a. Push the value :math:`\I32.CONST~i` to the stack.

b. Push the value :math:`\val` to the stack.

c. Execute the instruction :math:`\TABLESET~x`.

d. Push the value :math:`\I32.CONST~(i+1)` to the stack.

e. Push the value :math:`\val` to the stack.

f. Push the value :math:`\I32.CONST~(n-1)` to the stack.

c. Execute the instruction :math:`\TABLEFILL~x`.

.. math::
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~(n+1))~(\TABLEFILL~x) &\stepto& S'; F; (\I32.\CONST~i)~\val~(\TABLESET~x)~(\I32.\CONST~(i+1))~\val~(\I32.\CONST~n)~(\TABLEFILL~x)
\end{array} \\
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
(\iff i \leq |\STABLES[F.\AMODULE.\MITABLES[x]]|) \\
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~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
Expand Down
12 changes: 6 additions & 6 deletions document/core/exec/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
:ref:`Tables <syntax-tableinst>`
................................

1. Let :math:`\tabletype` be the :ref:`table type <syntax-tabletype>` to allocate.
1. Let :math:`\tabletype` be the :ref:`table type <syntax-tabletype>` to allocate and :math:`\val` the initialization value.

2. Let :math:`(\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tabletype`.

Expand All @@ -312,11 +312,11 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei

.. math::
\begin{array}{rlll}
\alloctable(S, \tabletype) &=& S', \tableaddr \\[1ex]
\alloctable(S, \tabletype, \val) &=& S', \tableaddr \\[1ex]
\mbox{where:} \hfill \\
\tabletype &=& \{\LMIN~n, \LMAX~m^?\}~\reftype \\
\tableaddr &=& |S.\STABLES| \\
\tableinst &=& \{ \TIELEM~\REFNULL^n, \TIMAX~m^? \} \\
\tableinst &=& \{ \TIELEM~\val^n, \TIMAX~m^? \} \\
S' &=& S \compose \{\STABLES~\tableinst\} \\
\end{array}
Expand Down Expand Up @@ -385,7 +385,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
Growing :ref:`tables <syntax-tableinst>`
........................................

1. Let :math:`\tableinst` be the :ref:`table instance <syntax-tableinst>` to grow and :math:`n` the number of elements by which to grow it.
1. Let :math:`\tableinst` be the :ref:`table instance <syntax-tableinst>` to grow, :math:`n` the number of elements by which to grow it, and :math:`\val` the initialization value.

2. Let :math:`\X{len}` be :math:`n` added to the length of :math:`\tableinst.\TIELEM`.

Expand All @@ -397,7 +397,7 @@ Growing :ref:`tables <syntax-tableinst>`

.. math::
\begin{array}{rllll}
\growtable(\tableinst, n) &=& \tableinst \with \TIELEM = \tableinst.\TIELEM~\REFNULL^n \\
\growtable(\tableinst, n, \val) &=& \tableinst \with \TIELEM = \tableinst.\TIELEM~\val^n \\
&& (
\begin{array}[t]{@{}r@{~}l@{}}
\iff & \X{len} = n + |\tableinst.\TIELEM| \\
Expand Down Expand Up @@ -519,7 +519,7 @@ where:
\MIEXPORTS~\exportinst^\ast ~\}
\end{array} \\[1ex]
S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast)
S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast, \REFNULL)
\qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES) \\
S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast)
\qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\
Expand Down
16 changes: 14 additions & 2 deletions document/core/syntax/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,9 @@ The |LOCALTEE| instruction is like |LOCALSET| but also returns its argument.
pair: abstract syntax; instruction
.. _syntax-table.get:
.. _syntax-table.set:
.. _syntax-table.size:
.. _syntax-table.grow:
.. _syntax-table.fill:
.. _syntax-instr-table:

Table Instructions
Expand All @@ -253,10 +256,19 @@ Instructions in this group are concerned with accessing :ref:`tables <syntax-tab
\production{instruction} & \instr &::=&
\dots \\&&|&
\TABLEGET~\tableidx \\&&|&
\TABLESET~\tableidx \\
\TABLESET~\tableidx \\&&|&
\TABLESIZE~\tableidx \\&&|&
\TABLEGROW~\tableidx \\&&|&
\TABLEFILL~\tableidx \\
\end{array}
These instructions get or set an element in a table, respectively.
The |TABLEGET| and |TABLESET| instructions load or store an element in a table, respectively.

The |TABLESIZE| instruction returns the current size of a table.
The |TABLEGROW| instruction grows table by a given delta and returns the previous size, or :math:`-1` if enough space cannot be allocated.
It also takes an initialization value for the newly allocated entries.

The |TABLEFILL| instruction sets all entries in a range to a given value.

An additional instruction that accesses a table is the :ref:`control instruction <syntax-instr-control>` |CALLINDIRECT|.

Expand Down
8 changes: 7 additions & 1 deletion document/core/text/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -200,12 +200,18 @@ Table Instructions

.. _text-table.get:
.. _text-table.set:
.. _text-table.size:
.. _text-table.grow:
.. _text-table.fill:

.. math::
\begin{array}{llclll}
\production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
\text{table.get}~~x{:}\Ttableidx_I &\Rightarrow& \TABLEGET~x \\ &&|&
\text{table.set}~~x{:}\Ttableidx_I &\Rightarrow& \TABLESET~x \\
\text{table.set}~~x{:}\Ttableidx_I &\Rightarrow& \TABLESET~x \\ &&|&
\text{table.size}~~x{:}\Ttableidx_I &\Rightarrow& \TABLESIZE~x \\ &&|&
\text{table.grow}~~x{:}\Ttableidx_I &\Rightarrow& \TABLEGROW~x \\ &&|&
\text{table.fill}~~x{:}\Ttableidx_I &\Rightarrow& \TABLEFILL~x \\
\end{array}
Expand Down
3 changes: 3 additions & 0 deletions document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,9 @@

.. |TABLEGET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.get}}
.. |TABLESET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.set}}
.. |TABLESIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.size}}
.. |TABLEGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.grow}}
.. |TABLEFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.fill}}

.. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
.. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
Expand Down
Loading

0 comments on commit c3d5cbc

Please sign in to comment.