Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
[spec/interpreter/test] Implement basic tail-call proposal
  • Loading branch information
rossberg committed Apr 4, 2018
1 parent fd9dd22 commit 8e82d8c
Show file tree
Hide file tree
Showing 20 changed files with 1,017 additions and 28 deletions.
8 changes: 6 additions & 2 deletions document/core/binary/instructions.rst
Expand Up @@ -33,6 +33,8 @@ Control Instructions
.. _binary-return:
.. _binary-call:
.. _binary-call_indirect:
.. _binary-return_call:
.. _binary-return_call_indirect:

.. math::
\begin{array}{llclll}
Expand All @@ -54,15 +56,17 @@ Control Instructions
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
\hex{0F} &\Rightarrow& \RETURN \\ &&|&
\hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
\hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\
\hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\ &&|&
\hex{12}~~x{:}\Bfuncidx &\Rightarrow& \RETURNCALL~x \\ &&|&
\hex{13}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \RETURNCALLINDIRECT~x \\
\end{array}
.. note::
The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty.

.. note::
In future versions of WebAssembly, the zero byte occurring in the encoding
of the |CALLINDIRECT| instruction may be used to index additional tables.
of the |CALLINDIRECT| and |RETURNCALLINDIRECT| instructions may be used to index additional tables.

.. index:: value type, polymorphism
pair: binary format; instruction
Expand Down
112 changes: 112 additions & 0 deletions document/core/exec/instructions.rst
Expand Up @@ -934,6 +934,82 @@ Control Instructions
\end{array}
.. _exec-return_call:

:math:`\RETURNCALL~x`
.....................

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

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

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

4. :ref:`Tail-invoke <exec-return-invoke>` the function instance at address :math:`a`.


.. math::
\begin{array}{lcl@{\qquad}l}
(\RETURNCALL~x) &\stepto& (\RETURNINVOKE~a)
& (\iff \CALL~x \stepto \INVOKE~a)
\end{array}
.. _exec-return_call_indirect:

:math:`\RETURNCALLINDIRECT~x`
.............................

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

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

3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.

4. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`S.\STABLES[\X{ta}]` exists.

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

6. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\AMODULE.\MITYPES[x]` exists.

7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[x]`.

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

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

10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then:

a. Trap.

11. If :math:`\X{tab}.\TIELEM[i]` is uninitialized, then:

a. Trap.

12. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`\X{tab}.\TIELEM[i]`.

13. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`S.\SFUNCS[a]` exists.

14. Let :math:`\X{f}` be the :ref:`function instance <syntax-funcinst>` :math:`S.\SFUNCS[a]`.

15. Let :math:`\X{ft}_{\F{actual}}` be the :ref:`function type <syntax-functype>` :math:`\X{f}.\FITYPE`.

16. If :math:`\X{ft}_{\F{actual}}` and :math:`\X{ft}_{\F{expect}}` differ, then:

a. Trap.

17. :ref:`Tail-invoke <exec-return-invoke>` the function instance at address :math:`a`.


.. math::
\begin{array}{lcl@{\qquad}l}
(\RETURNCALLINDIRECT~x) &\stepto& (\RETURNINVOKE~a)
& (\iff \CALLINDIRECT~x \stepto \INVOKE~a) \\
(\RETURNCALLINDIRECT~x) &\stepto& \TRAP
& (\iff \CALLINDIRECT~x \stepto \TRAP) \\
\end{array}
.. index:: instruction, instruction sequence, block
.. _exec-instr-seq:

Expand Down Expand Up @@ -1044,6 +1120,42 @@ Invocation of :ref:`function address <syntax-funcaddr>` :math:`a`
\end{array}
.. _exec-return-invoke:

Tail-invocation of :ref:`function address <syntax-funcaddr>` :math:`a`
......................................................................

1. Assert: due to :ref:`validation <valid-call>`, :math:`S.\SFUNCS[a]` exists.

2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type <syntax-functype>` :math:`S.\SFUNCS[a].\FITYPE`.

3. Assert: due to :ref:`validation <valid-return_call>`, there are at least :math:`m` values on the top of the stack.

4. Pop the results :math:`\val^m` from the stack.

5. Assert: due to :ref:`validation <valid-return_call>`, the stack contains at least one :ref:`frame <syntax-frame>`.

6. While the top of the stack is not a frame, do:

a. Pop the top element from the stack.

7. Assert: the top of the stack is a frame.

8. Pop the frame from the stack.

9. Push :math:`\val^m` to the stack.

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

.. math::
~\\[-1ex]
\begin{array}{lcl@{\qquad}l}
S; \FRAME_n\{F\}~B^*[\val^m~(\RETURNINVOKE~a)]~\END &\stepto&
\val^m~(\INVOKE~a)
& (\iff S.\SFUNCS[a].\FITYPE = [t_1^m] \to [t_2^n])
\end{array}
.. _exec-invoke-exit:

Returning from a function
Expand Down
2 changes: 2 additions & 0 deletions document/core/exec/runtime.rst
Expand Up @@ -443,6 +443,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
\dots \\ &&|&
\TRAP \\ &&|&
\INVOKE~\funcaddr \\ &&|&
\RETURNINVOKE~\funcaddr \\ &&|&
\INITELEM~\tableaddr~\u32~\funcidx^\ast \\ &&|&
\INITDATA~\memaddr~\u32~\byte^\ast \\ &&|&
\LABEL_n\{\instr^\ast\}~\instr^\ast~\END \\ &&|&
Expand All @@ -454,6 +455,7 @@ Traps are bubbled up through nested instruction sequences, ultimately reducing t

The |INVOKE| instruction represents the imminent invocation of a :ref:`function instance <syntax-funcinst>`, identified by its :ref:`address <syntax-funcaddr>`.
It unifies the handling of different forms of calls.
Analogously, |RETURNINVOKE| represents the imminent tail invocation of a function instance.

The |INITELEM| and |INITDATA| instructions perform initialization of :ref:`element <syntax-elem>` and :ref:`data <syntax-data>` segments during module :ref:`instantiation <exec-instantiation>`.

Expand Down
10 changes: 8 additions & 2 deletions document/core/syntax/instructions.rst
Expand Up @@ -301,7 +301,9 @@ Instructions in this group affect the flow of control.
\BRTABLE~\vec(\labelidx)~\labelidx \\&&|&
\RETURN \\&&|&
\CALL~\funcidx \\&&|&
\CALLINDIRECT~\typeidx \\
\CALLINDIRECT~\typeidx \\&&|&
\RETURNCALL~\funcidx \\&&|&
\RETURNCALLINDIRECT~\typeidx \\
\end{array}
The |NOP| instruction does nothing.
Expand Down Expand Up @@ -344,9 +346,13 @@ The |CALLINDIRECT| instruction calls a function indirectly through an operand in
Since tables may contain function elements of heterogeneous type |ANYFUNC|,
the callee is dynamically checked against the :ref:`function type <syntax-functype>` indexed by the instruction's immediate, and the call aborted with a :ref:`trap <trap>` if it does not match.

The |RETURNCALL| and |RETURNCALLINDIRECT| instructions are *tail-call* variants of the previous ones.
That is, they first return from the current function before actually performing the respective call.
It is guaranteed that no sequence of nested calls using only these instructions can cause resource exhaustion due to hitting an :ref:`implementation's limit <impl-exec>` on the number of active calls.

.. note::
In the current version of WebAssembly,
|CALLINDIRECT| implicitly operates on :ref:`table <syntax-table>` :ref:`index <syntax-tableidx>` :math:`0`.
|CALLINDIRECT| and |RETURNCALLINDIRECT| implicitly operate on :ref:`table <syntax-table>` :ref:`index <syntax-tableidx>` :math:`0`.
This restriction may be lifted in future versions.


Expand Down
5 changes: 5 additions & 0 deletions document/core/text/instructions.rst
Expand Up @@ -83,6 +83,8 @@ The same label identifier may optionally be repeated after the corresponding :ma
.. _text-return:
.. _text-call:
.. _text-call_indirect:
.. _text-return_call:
.. _text-return_call_indirect:

All other control instruction are represented verbatim.

Expand All @@ -98,6 +100,9 @@ All other control instruction are represented verbatim.
\text{return} &\Rightarrow& \RETURN \\ &&|&
\text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
\text{call\_indirect}~~x,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x
& (\iff I' = \{\}) \\ &&|&
\text{return\_call}~~x{:}\Tfuncidx_I &\Rightarrow& \RETURNCALL~x \\ &&|&
\text{return\_call\_indirect}~~x,I'{:}\Ttypeuse_I &\Rightarrow& \RETURNCALLINDIRECT~x
& (\iff I' = \{\}) \\
\end{array}
Expand Down
3 changes: 3 additions & 0 deletions document/core/util/macros.def
Expand Up @@ -313,6 +313,8 @@
.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
.. |RETURNCALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call}}
.. |RETURNCALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call\_indirect}}

.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
.. |SELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{select}}
Expand Down Expand Up @@ -865,6 +867,7 @@

.. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
.. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
.. |RETURNINVOKE| mathdef:: \xref{exec/runtime}{syntax-return_invoke}{\K{return\_invoke}}
.. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}}
.. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}}

Expand Down
63 changes: 63 additions & 0 deletions document/core/valid/instructions.rst
Expand Up @@ -681,6 +681,69 @@ Control Instructions
}
.. _valid-return_call:

:math:`\RETURNCALL~x`
.....................

* The return type :math:`C.\CRETURN` must not be empty in the context.

* The function :math:`C.\CFUNCS[x]` must be defined in the context.

* Let :math:`[t_1^\ast] \to [t_2^?]` be the :ref:`function type <syntax-functype>` :math:`C.\CFUNCS[x]`.

* The :ref:`result type <syntax-resulttype>` must be the same as :math:`C.\CRETURN`.

* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.

.. math::
\frac{
C.\CFUNCS[x] = [t_1^\ast] \to [t_2^?]
\qquad
C.\CRETURN = [t_2^?]
}{
C \vdashinstr \CALL~x : [t_3^\ast~t_1^\ast] \to [t_4^\ast]
}
.. note::
The |RETURNCALL| instruction is :ref:`stack-polymorphic <polymorphism>`.


.. _valid-return_call_indirect:

:math:`\RETURNCALLINDIRECT~x`
.............................

* The return type :math:`C.\CRETURN` must not be empty in the context.

* The table :math:`C.\CTABLES[0]` must be defined in the context.

* Let :math:`\limits~\elemtype` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[0]`.

* The :ref:`element type <syntax-elemtype>` :math:`\elemtype` must be |ANYFUNC|.

* The type :math:`C.\CTYPES[x]` must be defined in the context.

* Let :math:`[t_1^\ast] \to [t_2^?]` be the :ref:`function type <syntax-functype>` :math:`C.\CTYPES[x]`.

* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.


.. math::
\frac{
C.\CTABLES[0] = \limits~\ANYFUNC
\qquad
C.\CTYPES[x] = [t_1^\ast] \to [t_2^?]
\qquad
C.\CRETURN = [t_2^?]
}{
C \vdashinstr \CALLINDIRECT~x : [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]
}
.. note::
The |RETURNCALLINDIRECT| instruction is :ref:`stack-polymorphic <polymorphism>`.


.. index:: instruction, instruction sequence
.. _valid-instr-seq:

Expand Down
2 changes: 2 additions & 0 deletions interpreter/README.md
Expand Up @@ -214,6 +214,8 @@ op:
br_if <var>
br_table <var>+
return
return_call <var>
return_call_indirect <func_type>
call <var>
call_indirect <func_type>
drop
Expand Down
7 changes: 6 additions & 1 deletion interpreter/binary/decode.ml
Expand Up @@ -246,8 +246,13 @@ let rec instr s =
let x = at var s in
expect 0x00 s "zero flag expected";
call_indirect x
| 0x12 -> return_call (at var s)
| 0x13 ->
let x = at var s in
expect 0x00 s "zero flag expected";
return_call_indirect x

| 0x12 | 0x13 | 0x14 | 0x15 | 0x16 | 0x17 | 0x18 | 0x19 as b -> illegal s pos b
| 0x14 | 0x15 | 0x16 | 0x17 | 0x18 | 0x19 as b -> illegal s pos b

| 0x1a -> drop
| 0x1b -> select
Expand Down
2 changes: 2 additions & 0 deletions interpreter/binary/encode.ml
Expand Up @@ -157,6 +157,8 @@ let encode m =
| Return -> op 0x0f
| Call x -> op 0x10; var x
| CallIndirect x -> op 0x11; var x; u8 0x00
| ReturnCall x -> op 0x12; var x
| ReturnCallIndirect x -> op 0x13; var x; u8 0x00

| Drop -> op 0x1a
| Select -> op 0x1b
Expand Down

0 comments on commit 8e82d8c

Please sign in to comment.