[spec/interpreter/tests] Prep merge of tail call proposal

document/core/appendix/changes.rst

@@ -160,3 +160,13 @@ Added vector type and instructions that manipulate multiple numeric values in pa
 Release 3.0
 ~~~~~~~~~~~
 
+Tail calls
+..........
+
+Added instructions to perform tail calls [#proposal-tailcall]_.
+
+* New :ref:`control instructions <syntax-instr-control>`: :math:`RETURNCALL` and :math:`RETURNCALLINDIRECT`
+
+
+.. [#proposal-tailcall]
+   https://github.com/WebAssembly/spec/tree/main/proposals/tail-call/

document/core/appendix/index-instructions.py

@@ -87,8 +87,8 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\RETURN', r'\hex{0F}', r'[t_1^\ast~t^\ast] \to [t_2^\ast]', r'valid-return', r'exec-return'),
     Instruction(r'\CALL~x', r'\hex{10}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-call', r'exec-call'),
     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(r'\RETURNCALL~x', r'\hex{12}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-return_call', r'exec-return_call'),
+    Instruction(r'\RETURNCALLINDIRECT~x~y', r'\hex{13}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-return_call_indirect', r'exec-return_call_indirect'),
     Instruction(None, r'\hex{14}'),
     Instruction(None, r'\hex{15}'),
     Instruction(None, r'\hex{16}'),

document/core/binary/instructions.rst

@@ -37,6 +37,8 @@ Control Instructions
 .. _binary-return:
 .. _binary-call:
 .. _binary-call_indirect:
+.. _binary-return_call:
+.. _binary-return_call_indirect:
 
 .. math::
    \begin{array}{llcllll}
@@ -63,6 +65,8 @@ Control Instructions
      \hex{0F} &\Rightarrow& \RETURN \\ &&|&
      \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
      \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\
+     \hex{12}~~x{:}\Bfuncidx &\Rightarrow& \RETURNCALL~x \\ &&|&
+     \hex{13}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \RETURNCALLINDIRECT~x~y \\
    \end{array}
 
 .. note::

document/core/conf.py

@@ -66,10 +66,10 @@
 logo = 'static/webassembly.png'
 
 # The name of the GitHub repository this resides in
-repo = 'spec'
+repo = 'tail-call'
 
 # The name of the proposal it represents, if any
-proposal = ''
+proposal = 'tail calls'
 
 # The draft version string (clear out for release cuts)
 draft = ' (Draft ' + date.today().strftime("%Y-%m-%d") + ')'

document/core/exec/instructions.rst

@@ -2806,7 +2806,7 @@ Control Instructions
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   \FRAME_n\{F\}~\XB^k[\val^n~\RETURN]~\END &\stepto& \val^n
+   \FRAME_n\{F\}~B^\ast[\val^n~\RETURN]~\END &\stepto& \val^n
    \end{array}
 
 
@@ -2900,6 +2900,84 @@ Control Instructions
    \end{array}
 
 
+.. _exec-return_call:
+
+:math:`\RETURNCALL~x`
+.....................
+
+.. todo: find a way to reuse call/call_indirect prose for tail call versions
+
+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~y`
+...............................
+
+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[x]` exists.
+
+3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[x]`.
+
+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[y]` exists.
+
+7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[y]`.
+
+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}
+   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& (\RETURNINVOKE~a)
+     & (\iff \val~(\CALLINDIRECT~x~y) \stepto (\INVOKE~a)) \\
+   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& \TRAP
+     & (\iff \val~(\CALLINDIRECT~x~y) \stepto \TRAP) \\
+   \end{array}
+
+
 .. index:: instruction, instruction sequence, block
 .. _exec-instr-seq:
 
@@ -3005,6 +3083,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^n] \to [t_2^m]` 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:`n` values on the top of the stack.
+
+4. Pop the results :math:`\val^n` 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^n` to the stack.
+
+10. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.
+
+.. math::
+   ~\\[-1ex]
+   \begin{array}{lcl@{\qquad}l}
+    S; \FRAME_m\{F\}~B^\ast[\val^n~(\RETURNINVOKE~a)]~\END &\stepto&
+      \val^n~(\INVOKE~a)
+      & (\iff S.\SFUNCS[a].\FITYPE = [t_1^n] \to [t_2^m])
+   \end{array}
+
+
 .. _exec-invoke-exit:
 
 Returning from a function

document/core/exec/runtime.rst

@@ -533,6 +533,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
      \REFFUNCADDR~\funcaddr \\ &&|&
      \REFEXTERNADDR~\externaddr \\ &&|&
      \INVOKE~\funcaddr \\ &&|&
+     \RETURNINVOKE~\funcaddr \\ &&|&
      \LABEL_n\{\instr^\ast\}~\instr^\ast~\END \\ &&|&
      \FRAME_n\{\frame\}~\instr^\ast~\END \\
    \end{array}
@@ -544,6 +545,7 @@ The |REFFUNCADDR| instruction represents :ref:`function reference values <syntax
 
 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 |LABEL| and |FRAME| instructions model :ref:`labels <syntax-label>` and :ref:`frames <syntax-frame>` :ref:`"on the stack" <exec-notation>`.
 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.

document/core/syntax/instructions.rst

@@ -652,6 +652,8 @@ Instructions in this group affect the flow of control.
      \RETURN \\&&|&
      \CALL~\funcidx \\&&|&
      \CALLINDIRECT~\tableidx~\typeidx \\
+     \RETURNCALL~\funcidx \\&&|&
+     \RETURNCALLINDIRECT~\tableidx~\typeidx \\
    \end{array}
 
 The |NOP| instruction does nothing.
@@ -698,6 +700,10 @@ The |CALLINDIRECT| instruction calls a function indirectly through an operand in
 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.
 
+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.
+
 
 .. index:: ! expression, constant, global, offset, element, data, instruction
    pair: abstract syntax; expression

document/core/text/instructions.rst

@@ -103,6 +103,8 @@ However, the special case of a type use that is syntactically empty or consists
 .. _text-return:
 .. _text-call:
 .. _text-call_indirect:
+.. _text-return_call:
+.. _text-return_call_indirect:
 
 All other control instruction are represented verbatim.
 
@@ -118,6 +120,9 @@ All other control instruction are represented verbatim.
      \text{return} &\Rightarrow& \RETURN \\ &&|&
      \text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
      \text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y
+       & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\&&|&
+     \text{return\_call}~~x{:}\Tfuncidx_I &\Rightarrow& \RETURNCALL~x \\ &&|&
+     \text{return\_call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \RETURNCALLINDIRECT~x~y
        & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
    \end{array}
 
@@ -138,14 +143,17 @@ The :math:`\text{else}` keyword of an :math:`\text{if}` instruction can be omitt
      \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{else}~~\text{end}
    \end{array}
 
-Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` can be omitted, defaulting to :math:`0`.
+Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` and :math:`\text{return\_call\_indirect}` can be omitted, defaulting to :math:`0`.
 
 .. math::
    \begin{array}{llclll}
    \production{plain instruction} &
      \text{call\_indirect}~~\Ttypeuse
        &\equiv&
-     \text{call\_indirect}~~0~~\Ttypeuse
+     \text{call\_indirect}~~0~~\Ttypeuse \\
+     \text{return\_call\_indirect}~~\Ttypeuse
+       &\equiv&
+     \text{return\_call\_indirect}~~0~~\Ttypeuse \\
    \end{array}
 
 

document/core/util/macros.def

@@ -368,6 +368,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}}
@@ -1068,6 +1070,7 @@
 .. |REFEXTERNADDR| mathdef:: \xref{exec/runtime}{syntax-ref.extern}{\K{ref{.}extern}}
 .. |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}}
 
 
 .. Values & Results, non-terminals

document/core/valid/instructions.rst

@@ -1511,6 +1511,71 @@ Control Instructions
    }
 
 
+.. _valid-return_call:
+
+:math:`\RETURNCALL~x`
+.....................
+
+* The return type :math:`C.\CRETURN` must not be absent in the context.
+
+* The function :math:`C.\CFUNCS[x]` must be defined in the context.
+
+* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`C.\CFUNCS[x]`.
+
+* The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` 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^\ast]
+     \qquad
+     C.\CRETURN = [t_2^\ast]
+   }{
+     C \vdashinstr \RETURNCALL~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~y`
+...............................
+
+* The return type :math:`C.\CRETURN` must not be empty in the context.
+
+* The table :math:`C.\CTABLES[x]` must be defined in the context.
+
+* Let :math:`\limits~\reftype` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* The :ref:`reference type <syntax-reftype>` :math:`\reftype` must be |FUNCREF|.
+
+* The type :math:`C.\CTYPES[y]` must be defined in the context.
+
+* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`C.\CTYPES[y]`.
+
+* The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must be the same as :math:`C.\CRETURN`.
+
+* 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[x] = \limits~\FUNCREF
+     \qquad
+     C.\CTYPES[y] = [t_1^\ast] \to [t_2^\ast]
+     \qquad
+     C.\CRETURN = [t_2^\ast]
+   }{
+     C \vdashinstr \RETURNCALLINDIRECT~x~y : [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:
 

interpreter/README.md

@@ -234,6 +234,8 @@ op:
   br_if <var>
   br_table <var>+
   return
+  return_call <var>
+  return_call_indirect <func_type>
   call <var>
   call_indirect <var>? <func_type>
   drop

interpreter/binary/decode.ml

@@ -278,8 +278,13 @@ let rec instr s =
     let y = at var s in
     let x = at var s in
     call_indirect x y
+  | 0x12 -> return_call (at var s)
+  | 0x13 ->
+    let y = at var s in
+    let x = at var s in
+    return_call_indirect x y
 
-  | 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 None

interpreter/binary/encode.ml

@@ -173,6 +173,8 @@ struct
     | Return -> op 0x0f
     | Call x -> op 0x10; var x
     | CallIndirect (x, y) -> op 0x11; var y; var x
+    | ReturnCall x -> op 0x12; var x
+    | ReturnCallIndirect (x, y) -> op 0x13; var y; var x
 
     | Drop -> op 0x1a
     | Select None -> op 0x1b