Spec return_call_ref (PR #89)

Author: rossberg

document/core/appendix/gen-index-instructions.py

@@ -90,7 +90,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     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', r'\hex{13}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-return_call_indirect', r'exec-return_call_indirect'),
     Instruction(r'\CALLREF~x', 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(r'\RETURNCALLREF~x', r'\hex{15}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-return_call_ref', r'exec-return_call_ref'),
     Instruction(None, r'\hex{16}'),
     Instruction(None, r'\hex{17}'),
     Instruction(None, r'\hex{18}'),

document/core/appendix/index-instructions.rst

@@ -30,7 +30,7 @@ Instruction                                        Binary Opcode
 :math:`\RETURNCALL~x`                              :math:`\hex{12}`                      :math:`[t_1^\ast] \to [t_2^\ast]`                                :ref:`validation <valid-return_call>`           :ref:`execution <exec-return_call>`                               
 :math:`\RETURNCALLINDIRECT~x`                      :math:`\hex{13}`                      :math:`[t_1^\ast~\I32] \to [t_2^\ast]`                           :ref:`validation <valid-return_call_indirect>`  :ref:`execution <exec-return_call_indirect>`                      
 :math:`\CALLREF~x`                                 :math:`\hex{14}`                      :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`                 :ref:`validation <valid-call_ref>`              :ref:`execution <exec-call_ref>`                                  
-(reserved)                                         :math:`\hex{15}`                                                                                                                                                                                                         
+:math:`\RETURNCALLREF~x`                           :math:`\hex{15}`                      :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`                 :ref:`validation <valid-return_call_ref>`       :ref:`execution <exec-return_call_ref>`                           
 (reserved)                                         :math:`\hex{16}`                                                                                                                                                                                                         
 (reserved)                                         :math:`\hex{17}`                                                                                                                                                                                                         
 (reserved)                                         :math:`\hex{18}`                                                                                                                                                                                                         

document/core/binary/instructions.rst

@@ -71,6 +71,7 @@ Control Instructions
      \hex{12}~~x{:}\Bfuncidx &\Rightarrow& \RETURNCALL~x \\ &&|&
      \hex{13}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \RETURNCALLINDIRECT~x~y \\ &&|&
      \hex{14}~~x{:}\Btypeidx &\Rightarrow& \CALLREF~x \\ &&|&
+     \hex{15}~~x{:}\Btypeidx &\Rightarrow& \RETURNCALLREF~x \\ &&|&
      \hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|&
      \hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\
    \end{array}

document/core/exec/instructions.rst

@@ -2842,15 +2842,24 @@ Control Instructions
 :math:`\CALLREF~x`
 ..................
 
-1. Assert: due to :ref:`validation <valid-call_ref>`, a :ref:`function reference <syntax-ref>` is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-call_ref>`, a null or :ref:`function reference <syntax-ref>` is on the top of the stack.
 
-2. Pop the value :math:`\REFFUNCADDR~a` from the stack.
+2. Pop the reference value :math:`r` from the stack.
 
-3. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.
+3. If :math:`r` is :math:`\REFNULL~\X{ht}`, then:
+
+    a. Trap.
+
+4. Assert: due to :ref:`validation <valid-call_ref>`, :math:`r` is a :ref:`function reference <syntax-ref>`.
+
+5. Let :math:`\REFFUNCADDR~a` be the reference :math:`r`.
+
+6. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   F; (\REFFUNCADDR~a)~\CALLREF~x &\stepto& F; (\INVOKE~a)
+   F; (\REFFUNCADDR~a)~(\CALLREF~x) &\stepto& F; (\INVOKE~a) \\
+   F; (\REFNULL~\X{ht})~(\CALLREF~x) &\stepto& F; \TRAP \\
    \end{array}
 
 
@@ -2951,6 +2960,34 @@ Control Instructions
    \end{array}
 
 
+.. _exec-return_call_ref:
+
+:math:`\RETURNCALLREF~x`
+........................
+
+1. Assert: due to :ref:`validation <valid-return_call_ref>`, a :ref:`function reference <syntax-ref>` is on the top of the stack.
+
+2. Pop the reference value :math:`r` from the stack.
+
+3. If :math:`r` is :math:`\REFNULL~\X{ht}`, then:
+
+    a. Trap.
+
+4. Assert: due to :ref:`validation <valid-call_ref>`, :math:`r` is a :ref:`function reference <syntax-ref>`.
+
+5. Let :math:`\REFFUNCADDR~a` be the reference :math:`r`.
+
+6. :ref:`Tail-invoke <exec-return-invoke>` the function instance at address :math:`a`.
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   \val~(\RETURNCALLREF~x) &\stepto& (\RETURNINVOKE~a)
+     & (\iff \val~(\CALLREF~x) \stepto (\INVOKE~a)) \\
+   \val~(\RETURNCALLREF~x) &\stepto& \TRAP
+     & (\iff \val~(\CALLREF~x) \stepto \TRAP) \\
+   \end{array}
+
+
 .. _exec-return_call_indirect:
 
 :math:`\RETURNCALLINDIRECT~x`

document/core/syntax/instructions.rst

@@ -657,8 +657,9 @@ Instructions in this group affect the flow of control.
      \RETURN \\&&|&
      \CALL~\funcidx \\&&|&
      \CALLREF~\typeidx \\&&|&
-     \CALLINDIRECT~\tableidx~\typeidx \\
+     \CALLINDIRECT~\tableidx~\typeidx \\&&|&
      \RETURNCALL~\funcidx \\&&|&
+     \RETURNCALLREF~\funcidx \\&&|&
      \RETURNCALLINDIRECT~\tableidx~\typeidx \\
    \end{array}
 
@@ -708,7 +709,7 @@ 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.
+The |RETURNCALL|, |RETURNCALLREF|, 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.
 

document/core/text/instructions.rst

@@ -128,6 +128,7 @@ All other control instruction are represented verbatim.
      \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\_ref}~~x{:}\Ttypeidx &\Rightarrow& \RETURNCALLREF~x \\ &&|&
      \text{return\_call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \RETURNCALLINDIRECT~x~y
        & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
    \end{array}

document/core/util/macros.def

@@ -386,6 +386,7 @@
 .. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}}
 .. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
 .. |RETURNCALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call}}
+.. |RETURNCALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call\_ref}}
 .. |RETURNCALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call\_indirect}}
 
 .. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}

document/core/valid/instructions.rst

@@ -1618,6 +1618,29 @@ Control Instructions
    The |RETURNCALL| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
 
+.. _valid-return_call_ref:
+
+:math:`\RETURNCALLREF~x`
+........................
+
+* The type :math:`C.\CTYPES[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.\CTYPES[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_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`.
+
+.. math::
+   \frac{
+     C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast]
+     \qquad
+     C.\CRETURN = [t_2^\ast]
+   }{
+     C \vdashinstr \CALLREF~x : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]
+   }
+
+
 .. _valid-return_call_indirect:
 
 :math:`\RETURNCALLINDIRECT~x~y`

interpreter/README.md

@@ -254,14 +254,13 @@ op:
   br_if <var>
   br_table <var>+
   br_on_null <var> <heap_type>
-  return
-  return_call <var>
-  return_call_indirect <func_type>
   call <var>
+  call_ref <var>
   call_indirect <var>? <func_type>
-  call_ref
-  return_call_ref
-  func.bind <func_type>
+  return
+  return_call <var>
+  return_call_ref <var>
+  return_call_indirect <var>? <func_type>
   local.get <var>
   local.set <var>
   local.tee <var>

proposals/function-references/Overview.md

@@ -209,7 +209,7 @@ Note: Extending block types with index sets to allow initialization status to la
      - iff `$t = [t1*] -> [t2*]`
   - traps on `null`
 
-* With the [tail call proposal](https://github.com/WebAssembly/tail-call/blob/master/proposals/tail-call/Overview.md), there will also be `return_call_ref`:
+* `return_call_ref` tail-calls a function through a reference
   - `return_call_ref $t : [t1* (ref null $t)] -> [t2*]`
      - iff `$t = [t1*] -> [t2*]`
      - and `t2* <: C.result`