Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

[spec] New instructions #52

Merged
rossberg merged 3 commits into from
Sep 17, 2021
Merged

[spec] New instructions #52

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
96ae61e
[spec] Add concrete ref types and surrounding semantics
rossberg Jun 24, 2021
ea1e36c
[spec] New instructions
rossberg Jun 25, 2021
1331021
Merge branch 'master' into spec2
rossberg Aug 9, 2021
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
12 changes: 6 additions & 6 deletions document/core/appendix/gen-index-instructions.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(r'\CALLINDIRECT~x~y', r'\hex{11}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-call_indirect', r'exec-call_indirect'),
Instruction(None, r'\hex{12}'),
Instruction(None, r'\hex{13}'),
Instruction(None, r'\hex{14}'),
Instruction(r'\CALLREF', r'\hex{14}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-call_ref', r'exec-call_ref'),
Instruction(None, r'\hex{15}'),
Instruction(None, r'\hex{16}'),
Instruction(None, r'\hex{17}'),
Expand Down Expand Up @@ -269,13 +269,13 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(None, r'\hex{CD}'),
Instruction(None, r'\hex{CE}'),
Instruction(None, r'\hex{CF}'),
Instruction(r'\REFNULL~t', r'\hex{D0}', r'[] \to [t]', r'valid-ref.null', r'exec-ref.null'),
Instruction(r'\REFISNULL', r'\hex{D1}', r'[t] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'),
Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
Instruction(None, r'\hex{D3}'),
Instruction(None, r'\hex{D4}'),
Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
Instruction(None, r'\hex{D5}'),
Copy link
Contributor

@conrad-watt conrad-watt Sep 17, 2021

Choose a reason for hiding this comment

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

Is there a reason br_on_null isn't next to br_on_non_null in the index space?

Copy link
Member Author

@rossberg rossberg Sep 17, 2021

Choose a reason for hiding this comment

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

D5 was already assigned to ref.eq at the time we added br_on_non_null.

Instruction(None, r'\hex{D6}'),
Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'),
Instruction(None, r'\hex{D7}'),
Instruction(None, r'\hex{D8}'),
Instruction(None, r'\hex{D9}'),
Expand Down
548 changes: 274 additions & 274 deletions document/core/appendix/index-instructions.rst
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 10 additions & 2 deletions document/core/binary/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,11 @@ Control Instructions
.. _binary-br:
.. _binary-br_if:
.. _binary-br_table:
.. _binary-br_on_null:
.. _binary-br_on_non_null:
.. _binary-return:
.. _binary-call:
.. _binary-call_ref:
.. _binary-call_indirect:

.. math::
Expand All @@ -62,7 +65,10 @@ Control Instructions
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
\hex{0F} &\Rightarrow& \RETURN \\ &&|&
\hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|&
\hex{14}~~x{:}\Bfuncidx &\Rightarrow& \CALLREF \\ &&|&
\hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|&
\hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\
\end{array}

.. note::
Expand All @@ -84,13 +90,15 @@ Reference Instructions
.. _binary-ref.null:
.. _binary-ref.func:
.. _binary-ref.is_null:
.. _binary-ref.as_non_null:

.. math::
\begin{array}{llclll}
\production{instruction} & \Binstr &::=& \dots \\ &&|&
\hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|&
\hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
\hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
\hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
\hex{D3} &\Rightarrow& \REFASNONNULL \\
\end{array}


Expand Down
125 changes: 110 additions & 15 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,15 +192,35 @@ Reference Instructions

.. _exec-ref.null:

:math:`\REFNULL~t`
..................
:math:`\REFNULL~\X{ht}`
.......................

1. Push the value :math:`\REFNULL~t` to the stack.
1. Push the value :math:`\REFNULL~\X{ht}` to the stack.

.. note::
No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value <syntax-val>`.


.. _exec-ref.func:

:math:`\REFFUNC~x`
..................

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

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

3. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`F.\AMODULE.\MIFUNCS[x]`.

4. Push the value :math:`\REFFUNCADDR~a` to the stack.

.. math::
\begin{array}{lcl@{\qquad}l}
F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a
& (\iff a = F.\AMODULE.\MIFUNCS[x]) \\
\end{array}


.. _exec-ref.is_null:

:math:`\REFISNULL`
Expand All @@ -210,7 +230,7 @@ Reference Instructions

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

3. If :math:`\val` is :math:`\REFNULL~t`, then:
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:

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

Expand All @@ -221,29 +241,33 @@ Reference Instructions
.. math::
\begin{array}{lcl@{\qquad}l}
\val~\REFISNULL &\stepto& \I32.\CONST~1
& (\iff \val = \REFNULL~t) \\
& (\iff \val = \REFNULL~\X{ht}) \\
\val~\REFISNULL &\stepto& \I32.\CONST~0
& (\otherwise) \\
\end{array}


.. _exec-ref.func:
.. _exec-ref.as_non_null:

:math:`\REFFUNC~x`
..................
:math:`\REFASNONNULL`
.....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.

2. Assert: due to :ref:`validation <valid-ref.func>`, :math:`F.\AMODULE.\MIFUNCS[x]` exists.
2. Pop the value :math:`\val` from the stack.

3. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`F.\AMODULE.\MIFUNCS[x]`.
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:

4. Push the value :math:`\REFFUNCADDR~a` to the stack.
a. Trap.

4. Push the value :math:`\val` back to the stack.

.. math::
\begin{array}{lcl@{\qquad}l}
F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a
& (\iff a = F.\AMODULE.\MIFUNCS[x]) \\
\val~\REFASNONNULL &\stepto& \TRAP
& (\iff \val = \REFNULL~\X{ht}) \\
\val~\REFASNONNULL &\stepto& \val
& (\otherwise) \\
\end{array}


Expand Down Expand Up @@ -1722,6 +1746,60 @@ Control Instructions
\end{array}


.. _exec-br_on_null:

:math:`\BRONNULL~l`
...................

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

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

3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:

a. :ref:`Execute <exec-br>` the instruction :math:`(\BR~l)`.

4. Else:

a. Push the value :math:`\val` back to the stack.

.. math::
\begin{array}{lcl@{\qquad}l}
\val~(\BRONNULL~l) &\stepto& (\BR~l)
& (\iff \val = \REFNULL~\X{ht}) \\
\val~(\BRONNULL~l) &\stepto& \val
& (\otherwise) \\
\end{array}


.. _exec-br_on_non_null:

:math:`\BRONNONNULL~l`
......................

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

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

3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:

a. Do nothing.

4. Else:

a. Push the value :math:`\val` back to the stack.

b. :ref:`Execute <exec-br>` the instruction :math:`(\BR~l)`.

.. math::
\begin{array}{lcl@{\qquad}l}
\val~(\BRONNONNULL~l) &\stepto& \epsilon
& (\iff \val = \REFNULL~\X{ht}) \\
\val~(\BRONNONNULL~l) &\stepto& \val~(\BR~l)
& (\otherwise) \\
\end{array}


.. _exec-return:

:math:`\RETURN`
Expand Down Expand Up @@ -1776,6 +1854,23 @@ Control Instructions
\end{array}


.. _exec-call_ref:

:math:`\CALLREF`
................

1. Assert: due to :ref:`validation <valid-call_ref>`, a :ref:`function reference <syntax-ref>` is on the top of the stack.

2. Pop the value :math:`\REFFUNCADDR~a` from the stack.

3. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.

.. math::
\begin{array}{lcl@{\qquad}l}
F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a)
\end{array}


.. _exec-call_indirect:

:math:`\CALLINDIRECT~x~y`
Expand Down Expand Up @@ -1805,7 +1900,7 @@ Control Instructions

11. Let :math:`r` be the :ref:`reference <syntax-ref>` :math:`\X{tab}.\TIELEM[i]`.

12. If :math:`r` is :math:`\REFNULL~t`, then:
12. If :math:`r` is :math:`\REFNULL~\X{ht}`, then:

a. Trap.

Expand Down
14 changes: 11 additions & 3 deletions document/core/syntax/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,8 +174,9 @@ Occasionally, it is convenient to group operators together according to the foll
.. index:: ! reference instruction, reference, null
pair: abstract syntax; instruction
.. _syntax-ref.null:
.. _syntax-ref.is_null:
.. _syntax-ref.func:
.. _syntax-ref.is_null:
.. _syntax-ref.as_non_null:
.. _syntax-instr-ref:

Reference Instructions
Expand All @@ -188,11 +189,13 @@ Instructions in this group are concerned with accessing :ref:`references <syntax
\production{instruction} & \instr &::=&
\dots \\&&|&
\REFNULL~\reftype \\&&|&
Copy link
Contributor

@conrad-watt conrad-watt Sep 17, 2021

Choose a reason for hiding this comment

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

\reftype here should be \heaptype - sorry if I missed this previously.

Copy link
Member Author

@rossberg rossberg Sep 17, 2021

Choose a reason for hiding this comment

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

Fixed.

\REFFUNC~\funcidx \\&&|&
\REFISNULL \\&&|&
\REFFUNC~\funcidx \\
\REFASNONNULL \\
\end{array}

These instruction produce a null value, check for a null value, or produce a reference to a given function, respectively.
The first three of these instruction produce a :ref:`null <syntax-null>` value, produce a reference to a given function, or check for a null value, respectively.
The |REFASNONNULL| casts a :ref:`nullable <syntax-reftype>` to a non-null one, and :ref:`traps <trap>` if it encounters null.


.. index:: ! parametric instruction, value type
Expand Down Expand Up @@ -389,8 +392,11 @@ Instructions in this group affect the flow of control.
\BR~\labelidx \\&&|&
\BRIF~\labelidx \\&&|&
\BRTABLE~\vec(\labelidx)~\labelidx \\&&|&
\BRONNULL~\labelidx \\&&|&
\BRONNONNULL~\labelidx \\&&|&
\RETURN \\&&|&
\CALL~\funcidx \\&&|&
\CALLREF \\&&|&
\CALLINDIRECT~\tableidx~\typeidx \\
\end{array}

Expand Down Expand Up @@ -427,13 +433,15 @@ Branch instructions come in several flavors:
|BR| performs an unconditional branch,
|BRIF| performs a conditional branch,
and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds.
The |BRONNULL| and |BRONNONNULL| instructions check whether a reference operand is :ref:`null <syntax-null>` and branch if that is the case or not the case, respectively.
The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function.
Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered.
However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding.
Forward branches require operands according to the output of the targeted block's type, i.e., represent the values produced by the terminated block.
Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block.

The |CALL| instruction invokes another :ref:`function <syntax-func>`, consuming the necessary arguments from the stack and returning the result values of the call.
The |CALLREF| instruction invokes a function indirectly through a :ref:`function reference <syntax-reftype>` operand.
The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table <syntax-table>` that is denoted by a :ref:`table index <syntax-tableidx>` and must contain :ref:`function references <syntax-reftype>`.
Since it may contain functions of heterogeneous type,
the callee is dynamically checked against the :ref:`function type <syntax-functype>` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap <trap>` if it does not match.
Expand Down
12 changes: 10 additions & 2 deletions document/core/text/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,11 @@ However, the special case of a type use that is syntactically empty or consists
.. _text-br:
.. _text-br_if:
.. _text-br_table:
.. _text-br_on_null:
.. _text-br_on_non_null:
.. _text-return:
.. _text-call:
.. _text-call_ref:
.. _text-call_indirect:

All other control instruction are represented verbatim.
Expand All @@ -110,8 +113,11 @@ All other control instruction are represented verbatim.
\text{br\_if}~~l{:}\Tlabelidx_I &\Rightarrow& \BRIF~l \\ &&|&
\text{br\_table}~~l^\ast{:}\Tvec(\Tlabelidx_I)~~l_N{:}\Tlabelidx_I
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
\text{br\_on\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNULL~l \\ &&|&
\text{br\_on\_non\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNONNULL~l \\ &&|&
\text{return} &\Rightarrow& \RETURN \\ &&|&
\text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
\text{call\_ref} &\Rightarrow& \CALLREF \\ &&|&
\text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y
& (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
\end{array}
Expand Down Expand Up @@ -152,15 +158,17 @@ Reference Instructions
~~~~~~~~~~~~~~~~~~~~~~

.. _text-ref.null:
.. _text-ref.is_null:
.. _text-ref.func:
.. _text-ref.is_null:
.. _text-ref.as_non_null:

.. math::
\begin{array}{llclll}
\production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
\text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|&
\text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
\text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
\text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
\text{ref.as\_non\_null} &\Rightarrow& \REFASNONNULL \\
\end{array}


Expand Down
14 changes: 9 additions & 5 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -351,8 +351,11 @@
.. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}}
.. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}}
.. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}}
.. |BRONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_null}}
.. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}}
.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
.. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}}
.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}

.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
Expand Down Expand Up @@ -383,8 +386,9 @@
.. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data.drop}}

.. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}}
.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
.. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}}
.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
.. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}}

.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
Expand Down Expand Up @@ -789,8 +793,8 @@
.. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq}
.. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq}
.. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq}
.. |matchesexterntype| mathdef:: \xref{exec/matching}{match-externtype}{\leq}
.. |matcheslimits| mathdef:: \xref{exec/matching}{match-limits}{\leq}
.. |matchesexterntype| mathdef:: \xref{valid/matching}{match-externtype}{\leq}
.. |matcheslimits| mathdef:: \xref{valid/matching}{match-limits}{\leq}


.. Contexts
Expand Down Expand Up @@ -832,8 +836,8 @@
.. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash}
.. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash}
.. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash}
.. |vdashexterntypematch| mathdef:: \xref{exec/matching}{match-externtype}{\vdash}
.. |vdashlimitsmatch| mathdef:: \xref{exec/matching}{match-limits}{\vdash}
.. |vdashexterntypematch| mathdef:: \xref{valid/matching}{match-externtype}{\vdash}
.. |vdashlimitsmatch| mathdef:: \xref{valid/matching}{match-limits}{\vdash}

.. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash}
.. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash}
Expand Down
Loading