Skip to content

Commit 983df68

Browse files
binjibinji
authored
[spec] Add table.init, elem.drop exec text (WebAssembly#95)
This also adds `table.set` and `table.get` administrative instructions. Only `table.set` is used for now, but `table.copy` will use both.
1 parent 80aea4a commit 983df68

File tree

4 files changed

+251
-1
lines changed

4 files changed

+251
-1
lines changed

‎document/core/exec/conventions.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ The following conventions are adopted in stating these rules.
3333

3434
* The execution rules also assume the presence of an implicit :ref:`stack <stack>`
3535
that is modified by *pushing* or *popping*
36-
:ref:`values <syntax-value>`, :ref:`labels <syntax-label>`, and :ref:`frames <syntax-frame>`.
36+
:ref:`values <syntax-value>`, :ref:`function elements <syntax-funcelem>`, :ref:`labels <syntax-label>`, and :ref:`frames <syntax-frame>`.
3737

3838
* Certain rules require the stack to contain at least one frame.
3939
The most recent frame is referred to as the *current* frame.

‎document/core/exec/instructions.rst

Lines changed: 239 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -830,6 +830,245 @@ Memory Instructions
830830
\end{array}
831831
832832
833+
.. index:: table instruction, table index, store, frame, address, table address, table instance, function element, element address, element instance, value type
834+
pair: execution; instruction
835+
single: abstract syntax; instruction
836+
.. _exec-instr-table:
837+
838+
Table Instructions
839+
~~~~~~~~~~~~~~~~~~
840+
841+
.. _exec-table.init:
842+
843+
:math:`\TABLEINIT~x`
844+
....................
845+
846+
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
847+
848+
2. Assert: due to :ref:`validation <valid-table.init>`, :math:`F.\AMODULE.\MITABLES[0]` exists.
849+
850+
3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.
851+
852+
4. Assert: due to :ref:`validation <valid-table.init>`, :math:`S.\STABLES[\X{ta}]` exists.
853+
854+
5. Let :math:`\X{table}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[\X{ta}]`.
855+
856+
6. Assert: due to :ref:`validation <valid-elem.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
857+
858+
7. Let :math:`\X{ea}` be the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.
859+
860+
8. Assert: due to :ref:`validation <valid-elem.init>`, :math:`S.\SELEM[\X{ea}]` exists.
861+
862+
9. Let :math:`\X{elem}^?` be the optional :ref:`element instance <syntax-eleminst>` :math:`S.\SELEM[\X{ea}]`.
863+
864+
10. If :math:`\X{elem}^? = \epsilon`, then:
865+
866+
a. Trap.
867+
868+
11. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
869+
870+
12. Pop the value :math:`\I32.\CONST~n` from the stack.
871+
872+
13. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
873+
874+
14. Pop the value :math:`\I32.\CONST~s` from the stack.
875+
876+
15. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
877+
878+
16. Pop the value :math:`\I32.\CONST~d` from the stack.
879+
880+
17. If :math:`n` is :math:`0`, then:
881+
882+
a. If :math:`d` is larger than the length of :math:`\X{table}.\TIELEM`, then:
883+
884+
i. Trap.
885+
886+
b. If :math:`s` is larger than the length of :math:`\X{elem}.\EIINIT`, then:
887+
888+
i. Trap.
889+
890+
18. Else:
891+
892+
a. Push the value :math:`\I32.\CONST~d` to the stack.
893+
894+
b. Let :math:`\funcelem` be the :ref:`function element <syntax-funcelem>` :math:`\X{elem}.\EIINIT[s]`.
895+
896+
d. Execute the instruction :math:`\TABLESET~\funcelem`.
897+
898+
e. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
899+
900+
f. Push the value :math:`\I32.\CONST~(s+1)` to the stack.
901+
902+
g. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
903+
904+
h. Execute the instruction :math:`\TABLEINIT~x`.
905+
906+
.. math::
907+
~\\[-1ex]
908+
\begin{array}{l}
909+
\begin{array}{lcl@{\qquad}l}
910+
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~(n+1))~(\TABLEINIT~x) &\stepto& S; F;
911+
\begin{array}[t]{@{}l@{}}
912+
(\I32.\CONST~d)~\funcelem~\TABLESET \\
913+
(\I32.\CONST~(d+1))~(\I32.\CONST~(s+1))~(\I32.\CONST~n)~(\TABLEINIT~x) \\
914+
\end{array} \\
915+
\end{array} \\
916+
\\ \qquad
917+
\begin{array}[t]{@{}r@{~}l@{}}
918+
(\iff & s < |S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT| \\
919+
\wedge & \funcelem = S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT[s]) \\
920+
\end{array}
921+
\\[1ex]
922+
\begin{array}{lcl@{\qquad}l}
923+
S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\TABLEINIT~x) &\stepto& S; F; \epsilon
924+
\end{array}
925+
\\ \qquad
926+
\begin{array}[t]{@{}r@{~}l@{}}
927+
(\iff & d \leq |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM| \\
928+
\wedge & s \leq |S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT|) \\
929+
\end{array}
930+
\\[1ex]
931+
\begin{array}{lcl@{\qquad}l}
932+
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x) &\stepto& S; F; \TRAP
933+
\end{array}
934+
\\ \qquad
935+
(\otherwise) \\
936+
\end{array}
937+
938+
939+
.. _exec-elem.drop:
940+
941+
:math:`\ELEMDROP~x`
942+
...................
943+
944+
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
945+
946+
2. Assert: due to :ref:`validation <valid-elem.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
947+
948+
3. Let :math:`a` be the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.
949+
950+
4. Assert: due to :ref:`validation <valid-elem.init>`, :math:`S.\SELEM[a]` exists.
951+
952+
5. Let :math:`\X{elem}^?` be the optional :ref:`elem instance <syntax-eleminst>` :math:`S.\SELEM[a]`.
953+
954+
6. If :math:`\X{elem}^? = \epsilon`, then:
955+
956+
a. Trap.
957+
958+
7. Replace :math:`S.\SELEM[a]` with :math:`\epsilon`.
959+
960+
.. math::
961+
~\\[-1ex]
962+
\begin{array}{l}
963+
\begin{array}{lcl@{\qquad}l}
964+
S; F; (\ELEMDROP~x) &\stepto& S'; F; \epsilon
965+
\end{array}
966+
\\ \qquad
967+
\begin{array}[t]{@{}r@{~}l@{}}
968+
(\iff & S.\SELEM[F.\AMODULE.\MIELEMS[x]] \ne \epsilon \\
969+
\wedge & S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \epsilon) \\
970+
\end{array}
971+
\\[1ex]
972+
\begin{array}{lcl@{\qquad}l}
973+
S; F; (\ELEMDROP~x) &\stepto& S; F; \TRAP
974+
\end{array}
975+
\\ \qquad
976+
(\otherwise)
977+
\end{array}
978+
979+
980+
.. _exec-table.get:
981+
982+
:math:`\TABLEGET`
983+
.................
984+
985+
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
986+
987+
2. Assert: :math:`F.\AMODULE.\MITABLES[0]` exists.
988+
989+
3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.
990+
991+
4. Assert: :math:`S.\STABLES[\X{ta}]` exists.
992+
993+
5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[\X{ta}]`.
994+
995+
6. Assert: a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
996+
997+
7. Pop the value :math:`\I32.\CONST~i` from the stack.
998+
999+
8. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then:
1000+
1001+
a. Trap.
1002+
1003+
9. Push the :ref:`function element <syntax-funcelem>` :math:`X{tab}.\TIELEM[i]` to the stack.
1004+
1005+
.. math::
1006+
~\\[-1ex]
1007+
\begin{array}{l}
1008+
\begin{array}{lcl@{\qquad}l}
1009+
S; F; (\I32.\CONST~i)~\TABLEGET &\stepto& S; F; \funcelem
1010+
\end{array}
1011+
\\ \qquad
1012+
\begin{array}[t]{@{}r@{~}l@{}}
1013+
(\iff & \funcelem = S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM[i])
1014+
\end{array}
1015+
\\[1ex]
1016+
\begin{array}{lcl@{\qquad}l}
1017+
S; F; (\I32.\CONST~i)~\TABLEGET &\stepto& S; F; \TRAP
1018+
\end{array}
1019+
\\ \qquad
1020+
(\otherwise) \\
1021+
\end{array}
1022+
1023+
1024+
.. _exec-table.set:
1025+
1026+
:math:`\TABLESET`
1027+
.................
1028+
1029+
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
1030+
1031+
2. Assert: :math:`F.\AMODULE.\MITABLES[0]` exists.
1032+
1033+
3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.
1034+
1035+
4. Assert: :math:`S.\STABLES[\X{ta}]` exists.
1036+
1037+
5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[\X{ta}]`.
1038+
1039+
6. Assert: a :ref:`function element <syntax-funcelem>` is on the top of the stack.
1040+
1041+
7. Pop the function element :math:`\funcelem` from the stack.
1042+
1043+
8. Assert: a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
1044+
1045+
9. Pop the value :math:`\I32.\CONST~i` from the stack.
1046+
1047+
10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then:
1048+
1049+
a. Trap.
1050+
1051+
11. Replace :math:`X{tab}.\TIELEM[i]` with :math:`\funcelem`.
1052+
1053+
.. math::
1054+
~\\[-1ex]
1055+
\begin{array}{l}
1056+
\begin{array}{lcl@{\qquad}l}
1057+
S; F; (\I32.\CONST~i)~\funcelem~\TABLESET &\stepto& S'; F; \epsilon
1058+
\end{array}
1059+
\\ \qquad
1060+
\begin{array}[t]{@{}r@{~}l@{}}
1061+
(\iff & S' = S \with \STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM[i] = \funcelem)
1062+
\end{array}
1063+
\\[1ex]
1064+
\begin{array}{lcl@{\qquad}l}
1065+
S; F; (\I32.\CONST~i)~\funcelem~\TABLESET &\stepto& S; F; \TRAP
1066+
\end{array}
1067+
\\ \qquad
1068+
(\otherwise) \\
1069+
\end{array}
1070+
1071+
8331072
.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame
8341073
pair: execution; instruction
8351074
single: abstract syntax; instruction

‎document/core/exec/runtime.rst

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -480,6 +480,8 @@ Conventions
480480
.. _syntax-invoke:
481481
.. _syntax-init_elem:
482482
.. _syntax-init_data:
483+
.. _syntax-table_get:
484+
.. _syntax-table_set:
483485
.. _syntax-instr-admin:
484486

485487
Administrative Instructions
@@ -498,6 +500,8 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
498500
\INVOKE~\funcaddr \\ &&|&
499501
\INITELEM~\tableaddr~\u32~\funcidx^\ast \\ &&|&
500502
\INITDATA~\memaddr~\u32~\byte^\ast \\ &&|&
503+
\TABLEGET \\ &&|&
504+
\TABLESET \\ &&|&
501505
\LABEL_n\{\instr^\ast\}~\instr^\ast~\END \\ &&|&
502506
\FRAME_n\{\frame\}~\instr^\ast~\END \\
503507
\end{array}
@@ -513,6 +517,11 @@ The |INITELEM| and |INITDATA| instructions perform initialization of :ref:`eleme
513517
.. note::
514518
The reason for splitting instantiation into individual reduction steps is to provide a semantics that is compatible with future extensions like threads.
515519

520+
The |TABLEGET| and |TABLESET| instructions are used to simplify the specification of the |TABLEINIT| and |TABLECOPY| instructions.
521+
522+
.. note::
523+
In the future, |TABLEGET| and |TABLESET| may be provided as regular instructions.
524+
516525
The |LABEL| and |FRAME| instructions model :ref:`labels <syntax-label>` and :ref:`frames <syntax-frame>` :ref:`"on the stack" <exec-notation>`.
517526
Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instr-seq>` with an |END| marker.
518527
That way, the end of the inner instruction sequence is known when part of an outer sequence.

‎document/core/util/macros.def

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -922,6 +922,8 @@
922922
.. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
923923
.. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}}
924924
.. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}}
925+
.. |TABLEGET| mathdef:: \xref{exec/runtime}{syntax-table_get}{\K{table.get}
926+
.. |TABLESET| mathdef:: \xref{exec/runtime}{syntax-table_set}{\K{table.set}
925927

926928

927929
.. Values & Results, non-terminals

0 commit comments

Comments
 (0)