Add type annotation to call_ref (WebAssembly#76)

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

@@ -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(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(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(None, r'\hex{16}'),
     Instruction(None, r'\hex{17}'),

document/core/appendix/index-instructions.rst

@@ -29,7 +29,7 @@ Instruction                                        Binary Opcode
 :math:`\CALLINDIRECT~x~y`                          :math:`\hex{11}`                      :math:`[t_1^\ast~\I32] \to [t_2^\ast]`                           :ref:`validation <valid-call_indirect>`        :ref:`execution <exec-call_indirect>`                             
 (reserved)                                         :math:`\hex{12}`                                                                                                                                                                                                        
 (reserved)                                         :math:`\hex{13}`                                                                                                                                                                                                        
-:math:`\CALLREF`                                   :math:`\hex{14}`                      :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`                 :ref:`validation <valid-call_ref>`             :ref:`execution <exec-call_ref>`                                  
+: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}`                                                                                                                                                                                                        
 (reserved)                                         :math:`\hex{16}`                                                                                                                                                                                                        
 (reserved)                                         :math:`\hex{17}`                                                                                                                                                                                                        

document/core/binary/instructions.rst

@@ -66,9 +66,9 @@ Control Instructions
      \hex{0F} &\Rightarrow& \RETURN \\ &&|&
      \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
      \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|&
-     \hex{14} &\Rightarrow& \CALLREF \\ &&|&
-     \hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|&
-     \hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\
+     \hex{14}~~x{:}\Btypeidx &\Rightarrow& \CALLREF~x \\ &&|&
+     \hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|&
+     \hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\
    \end{array}
 
 .. note::

document/core/exec/instructions.rst

@@ -2837,8 +2837,8 @@ Control Instructions
 
 .. _exec-call_ref:
 
-:math:`\CALLREF`
-................
+: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.
 
@@ -2848,7 +2848,7 @@ Control Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a)
+   F; (\REFFUNCADDR~a)~\CALLREF~x &\stepto& F; (\INVOKE~a)
    \end{array}
 
 

document/core/syntax/instructions.rst

@@ -648,7 +648,7 @@ Instructions in this group affect the flow of control.
      \BRONNONNULL~\labelidx \\&&|&
      \RETURN \\&&|&
      \CALL~\funcidx \\&&|&
-     \CALLREF \\&&|&
+     \CALLREF~\typeidx \\&&|&
      \CALLINDIRECT~\tableidx~\typeidx \\
    \end{array}
 

document/core/text/instructions.rst

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

document/core/valid/instructions.rst

@@ -1538,18 +1538,20 @@ Control Instructions
 
 .. _valid-call_ref:
 
-:math:`\CALLREF`
-................
+:math:`\CALLREF~x`
+..................
+
+* The type :math:`C.\CTYPES[x]` must be defined in the context.
 
-* Let :math:`x` be some :ref:`type index <syntax-typeidx>` for which :math:`C.\CTYPES[x]` is a :ref:`function type <syntax-functype>` of the form :math:`[t_1^\ast] \to [t_2^\ast]`.
+* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`C.\CTYPES[x]`.
 
 * 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]
    }{
-     C \vdashinstr \CALLREF : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]
+     C \vdashinstr \CALLREF~x : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]
    }
 
 

interpreter/binary/decode.ml

@@ -318,8 +318,8 @@ let rec instr s =
 
   | 0x12 | 0x13 as b -> illegal s pos b  (* return_call, return_call_indirect *)
 
-  | 0x14 -> call_ref
-  | 0x15 -> return_call_ref
+  | 0x14 -> call_ref (at var s)
+  | 0x15 -> return_call_ref (at var s)
 
   | 0x16 as b -> illegal s pos b
 

interpreter/binary/encode.ml

@@ -197,9 +197,9 @@ struct
     | BrOnNonNull x -> op 0xd6; var x
     | Return -> op 0x0f
     | Call x -> op 0x10; var x
-    | CallRef -> op 0x14
+    | CallRef x -> op 0x14; var x
     | CallIndirect (x, y) -> op 0x11; var y; var x
-    | ReturnCallRef -> op 0x15
+    | ReturnCallRef x -> op 0x15; var x
 
     | Drop -> op 0x1a
     | Select None -> op 0x1b

interpreter/exec/eval.ml

@@ -222,10 +222,10 @@ let rec step (c : config) : config =
       | Call x, vs ->
         vs, [Invoke (func c.frame.inst x) @@ e.at]
 
-      | CallRef, Ref (NullRef _) :: vs ->
+      | CallRef _x, Ref (NullRef _) :: vs ->
         vs, [Trapping "null function reference" @@ e.at]
 
-      | CallRef, Ref (FuncRef f) :: vs ->
+      | CallRef _x, Ref (FuncRef f) :: vs ->
         vs, [Invoke f @@ e.at]
 
       | CallIndirect (x, y), Num (I32 i) :: vs ->
@@ -237,11 +237,11 @@ let rec step (c : config) : config =
         else
           vs, [Trapping "indirect call type mismatch" @@ e.at]
 
-      | ReturnCallRef, Ref (NullRef _) :: vs ->
+      | ReturnCallRef _x, Ref (NullRef _) :: vs ->
         vs, [Trapping "null function reference" @@ e.at]
 
-      | ReturnCallRef, vs ->
-        (match (step {c with code = (vs, [Plain CallRef @@ e.at])}).code with
+      | ReturnCallRef x, vs ->
+        (match (step {c with code = (vs, [Plain (CallRef x) @@ e.at])}).code with
         | vs', [{it = Invoke a; at}] -> vs', [ReturningInvoke (vs', a) @@ at]
         | vs', [{it = Trapping s; at}] -> vs', [Trapping s @@ at]
         | _ -> assert false

interpreter/syntax/ast.ml

@@ -153,9 +153,9 @@ and instr' =
   | BrOnNonNull of idx                (* break on non-null *)
   | Return                            (* break from function body *)
   | Call of idx                       (* call function *)
-  | CallRef                           (* call function through reference *)
+  | CallRef of idx                    (* call function through reference *)
   | CallIndirect of idx * idx         (* call function through table *)
-  | ReturnCallRef                     (* tail call through reference *)
+  | ReturnCallRef of idx              (* tail call through reference *)
   | LocalGet of idx                   (* read local idxiable *)
   | LocalSet of idx                   (* write local idxiable *)
   | LocalTee of idx                   (* write local idxiable and keep value *)

interpreter/syntax/free.ml

@@ -108,8 +108,9 @@ let rec instr (e : instr) =
   | If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
   | Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
   | BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
-  | Return | CallRef | ReturnCallRef -> empty
+  | Return -> empty
   | Call x -> funcs (idx x)
+  | CallRef x | ReturnCallRef x -> types (idx x)
   | CallIndirect (x, y) -> tables (idx x) ++ types (idx y)
   | LocalGet x | LocalSet x | LocalTee x -> locals (idx x)
   | GlobalGet x | GlobalSet x -> globals (idx x)

interpreter/syntax/operators.ml

@@ -32,9 +32,9 @@ let br_on_non_null x = BrOnNonNull x
 
 let return = Return
 let call x = Call x
-let call_ref = CallRef
+let call_ref x = CallRef x
 let call_indirect x y = CallIndirect (x, y)
-let return_call_ref = ReturnCallRef
+let return_call_ref x = ReturnCallRef x
 
 let local_get x = LocalGet x
 let local_set x = LocalSet x

interpreter/text/arrange.ml

@@ -456,10 +456,10 @@ let rec instr e =
     | BrOnNonNull x -> "br_on_non_null " ^ var x, []
     | Return -> "return", []
     | Call x -> "call " ^ var x, []
-    | CallRef -> "call_ref", []
+    | CallRef x -> "call_ref " ^ var x, []
     | CallIndirect (x, y) ->
       "call_indirect " ^ var x, [Node ("type " ^ var y, [])]
-    | ReturnCallRef -> "return_call_ref", []
+    | ReturnCallRef x -> "return_call_ref " ^ var x, []
     | LocalGet x -> "local.get " ^ var x, []
     | LocalSet x -> "local.set " ^ var x, []
     | LocalTee x -> "local.tee " ^ var x, []

interpreter/text/parser.mly

@@ -447,8 +447,8 @@ plain_instr :
   | BR_ON_NON_NULL var { fun c -> br_on_non_null ($2 c label) }
   | RETURN { fun c -> return }
   | CALL var { fun c -> call ($2 c func) }
-  | CALL_REF { fun c -> call_ref }
-  | RETURN_CALL_REF { fun c -> return_call_ref }
+  | CALL_REF var { fun c -> call_ref ($2 c type_) }
+  | RETURN_CALL_REF var { fun c -> return_call_ref ($2 c type_) }
   | LOCAL_GET var { fun c -> local_get ($2 c local) }
   | LOCAL_SET var { fun c -> local_set ($2 c local) }
   | LOCAL_TEE var { fun c -> local_tee ($2 c local) }

interpreter/valid/valid.ml

@@ -392,18 +392,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     let FuncT (ts1, ts2) = func c x in
     ts1 --> ts2, []
 
-  | CallRef ->
-    (match peek_ref 0 s e.at with
-    | (_, DefHT x) ->
-      let FuncT (ts1, ts2) = func_type c (x @@ e.at) in
-      (ts1 @ [RefT (Null, DefHT x)]) --> ts2, []
-    | (_, BotHT) ->
-      [RefT (Null, BotHT)] -->... [], []
-    | rt ->
-      error e.at
-        ("type mismatch: instruction requires function reference type" ^
-         " but stack has " ^ string_of_val_type (RefT rt))
-    )
+  | CallRef x ->
+    let FuncT (ts1, ts2) = func_type c x in
+    (ts1 @ [RefT (Null, DefHT x.it)]) --> ts2, []
 
   | CallIndirect (x, y) ->
     let TableT (_lim, t) = table c x in
@@ -413,22 +404,13 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
        " but table has element type " ^ string_of_ref_type t);
     (ts1 @ [NumT I32T]) --> ts2, []
 
-  | ReturnCallRef ->
-    (match peek_ref 0 s e.at with
-    | (_, DefHT x) ->
-      let FuncT (ts1, ts2) = func_type c (x @@ e.at) in
-      require (match_result_type c.types [] ts2 c.results) e.at
-        ("type mismatch: current function requires result type " ^
-         string_of_result_type c.results ^
-         " but callee returns " ^ string_of_result_type ts2);
-      (ts1 @ [RefT (Null, DefHT x)]) -->... [], []
-    | (_, BotHT) ->
-      [RefT (Null, BotHT)] -->... [], []
-    | rt ->
-      error e.at
-        ("type mismatch: instruction requires function reference type" ^
-         " but stack has " ^ string_of_ref_type rt)
-    )
+  | ReturnCallRef x ->
+    let FuncT (ts1, ts2) = func_type c x in
+    require (match_result_type c.types [] ts2 c.results) e.at
+      ("type mismatch: current function requires result type " ^
+       string_of_result_type c.results ^
+       " but callee returns " ^ string_of_result_type ts2);
+    (ts1 @ [RefT (Null, DefHT x.it)]) -->... [], []
 
   | LocalGet x ->
     let LocalT (init, t) = local c x in

proposals/function-references/Overview.md

@@ -48,7 +48,7 @@ The function `$hof` takes a function pointer as parameter, and is invoked by `$c
 (type $i32-i32 (func (param i32) (result i32)))
 
 (func $hof (param $f (ref $i32-i32)) (result i32)
-  (i32.add (i32.const 10) (call_ref (i32.const 42) (local.get $f)))
+  (i32.add (i32.const 10) (call_ref $i32-i32 (i32.const 42) (local.get $f)))
 )
 
 (func $inc (param $i i32) (result i32)
@@ -204,21 +204,21 @@ Note: Extending block types with index sets to allow initialization status to la
      - iff `$f : $t`
   - this is a *constant instruction*
 
-* `call_ref` calls a function through a reference
-  - `call_ref : [t1* (ref null $t)] -> [t2*]`
+* `call_ref <typeidx>` calls a function through a reference
+  - `call_ref $t : [t1* (ref null $t)] -> [t2*]`
      - 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 : [t1* (ref null $t)] -> [t2*]`
+  - `return_call_ref $t : [t1* (ref null $t)] -> [t2*]`
      - iff `$t = [t1*] -> [t2*]`
      - and `t2* <: C.result`
   - traps on `null`
 
 
 #### Optional References
 
-* `ref.null` is generalised to take a `<heaptype>` immediate
+* `ref.null <heaptype>` is generalised to take a `<heaptype>` immediate
   - `ref.null ht: [] -> [(ref null ht)]`
     - iff `ht ok`
 
@@ -227,13 +227,13 @@ Note: Extending block types with index sets to allow initialization status to la
     - iff `ht ok`
   - traps on `null`
 
-* `br_on_null $l` checks for null and branches if present
+* `br_on_null <labelidx>` checks for null and branches if present
   - `br_on_null $l : [t* (ref null ht)] -> [t* (ref ht)]`
     - iff `$l : [t*]`
     - and `ht ok`
   - branches to `$l` on `null`, otherwise returns operand as non-null
 
-* `br_on_non_null $l` checks for null and branches if not present
+* `br_on_non_null <labelidx>` checks for null and branches if not present
   - `br_on_non_null $l : [t* (ref null ht)] -> [t*]`
     - iff `$l : [t* (ref ht)]`
     - and `ht ok`
@@ -246,15 +246,15 @@ Note: Extending block types with index sets to allow initialization status to la
 
 Typing of local instructions is updated to account for the initialization status of locals.
 
-* `local.get $x`
+* `local.get <localidx>`
   - `local.get $x : [] -> [t]`
     - iff `$x : set t`
 
-* `local.set $x`
+* `local.set <localidx>`
   - `local.set $x : [t] -> [] $x`
     - iff `$x : set? t`
 
-* `local.tee $x`
+* `local.tee <localidx>`
   - `local.tee $x : [t] -> [t] $x`
     - iff `$x : set? t`
 
@@ -319,8 +319,8 @@ The opcode for heap types is encoded as an `s33`.
 
 | Opcode | Instruction              | Immediates |
 | ------ | ------------------------ | ---------- |
-| 0x14   | `call_ref`               |            |
-| 0x15   | `return_call_ref`        |            |
+| 0x14   | `call_ref $t`            | `$t : u32` |
+| 0x15   | `return_call_ref $t`     | `$t : u32` |
 | 0xd3   | `ref.as_non_null`        |            |
 | 0xd4   | `br_on_null $l`          | `$l : u32` |
 | 0xd6   | `br_on_non_null $l`      | `$l : u32` |

test/core/br_on_non_null.wast

@@ -2,15 +2,15 @@
   (type $t (func (result i32)))
 
   (func $nn (param $r (ref $t)) (result i32)
-    (call_ref
+    (call_ref $t
       (block $l (result (ref $t))
         (br_on_non_null $l (local.get $r))
         (return (i32.const -1))
       )
     )
   )
   (func $n (param $r (ref null $t)) (result i32)
-    (call_ref
+    (call_ref $t
       (block $l (result (ref $t))
         (br_on_non_null $l (local.get $r))
         (return (i32.const -1))
@@ -27,7 +27,7 @@
 
   (func (export "unreachable") (result i32)
     (block $l
-      (return (call_ref (br_on_null $l (unreachable))))
+      (return (call_ref $t (br_on_null $l (unreachable))))
     )
     (i32.const -1)
   )
@@ -53,7 +53,7 @@
   (func $f (param i32) (result i32) (i32.mul (local.get 0) (local.get 0)))
 
   (func $a (param $n i32) (param $r (ref null $t)) (result i32)
-    (call_ref
+    (call_ref $t
       (block $l (result i32 (ref $t))
         (return (br_on_non_null $l (local.get $n) (local.get $r)))
       )