Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

Merged
merged 7 commits into from
Apr 3, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we're missing any handling of the initializer argument here?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch, fixed. That meant also adjusting the meta function and the embedding interface accordingly to support an initialisation value.

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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Technically this is possibly a little dodgy (ditto subsequent clauses, ditto clauses for TABLESET): since we're directly manipulating the stack in the recursive call below, asserting that this is true as a consequence of validation is questionable. I'm not sure it's worth fixing though.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, fair point. I think there are actually a few other such assertions already where, strictly speaking, having the right value on the stack is rather a consequence of soundness.


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