Skip to content

Commit 2b194ce

Browse files
rossbergrossberg
authored
Add type annotation to call_ref (WebAssembly#76)
1 parent b04e3be commit 2b194ce

File tree

22 files changed

+148
-141
lines changed

22 files changed

+148
-141
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
8181
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'),
8282
Instruction(None, r'\hex{12}'),
8383
Instruction(None, r'\hex{13}'),
84-
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'),
84+
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'),
8585
Instruction(None, r'\hex{15}'),
8686
Instruction(None, r'\hex{16}'),
8787
Instruction(None, r'\hex{17}'),

‎document/core/appendix/index-instructions.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Instruction Binary Opcode
2929
: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>`
3030
(reserved) :math:`\hex{12}`
3131
(reserved) :math:`\hex{13}`
32-
: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>`
32+
: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>`
3333
(reserved) :math:`\hex{15}`
3434
(reserved) :math:`\hex{16}`
3535
(reserved) :math:`\hex{17}`

‎document/core/binary/instructions.rst

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -66,9 +66,9 @@ Control Instructions
6666
\hex{0F} &\Rightarrow& \RETURN \\ &&|&
6767
\hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
6868
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|&
69-
\hex{14} &\Rightarrow& \CALLREF \\ &&|&
70-
\hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|&
71-
\hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\
69+
\hex{14}~~x{:}\Btypeidx &\Rightarrow& \CALLREF~x \\ &&|&
70+
\hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|&
71+
\hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\
7272
\end{array}
7373
7474
.. note::

‎document/core/exec/instructions.rst

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2837,8 +2837,8 @@ Control Instructions
28372837
28382838
.. _exec-call_ref:
28392839

2840-
:math:`\CALLREF`
2841-
................
2840+
:math:`\CALLREF~x`
2841+
..................
28422842

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

@@ -2848,7 +2848,7 @@ Control Instructions
28482848

28492849
.. math::
28502850
\begin{array}{lcl@{\qquad}l}
2851-
F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a)
2851+
F; (\REFFUNCADDR~a)~\CALLREF~x &\stepto& F; (\INVOKE~a)
28522852
\end{array}
28532853
28542854

‎document/core/syntax/instructions.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -648,7 +648,7 @@ Instructions in this group affect the flow of control.
648648
\BRONNONNULL~\labelidx \\&&|&
649649
\RETURN \\&&|&
650650
\CALL~\funcidx \\&&|&
651-
\CALLREF \\&&|&
651+
\CALLREF~\typeidx \\&&|&
652652
\CALLINDIRECT~\tableidx~\typeidx \\
653653
\end{array}
654654

‎document/core/text/instructions.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ All other control instruction are represented verbatim.
117117
\text{br\_on\_non\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNONNULL~l \\ &&|&
118118
\text{return} &\Rightarrow& \RETURN \\ &&|&
119119
\text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
120-
\text{call\_ref} &\Rightarrow& \CALLREF \\ &&|&
120+
\text{call\_ref}~~x{:}\Ttypeidx &\Rightarrow& \CALLREF~x \\ &&|&
121121
\text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y
122122
& (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
123123
\end{array}

‎document/core/valid/instructions.rst

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1538,18 +1538,20 @@ Control Instructions
15381538
15391539
.. _valid-call_ref:
15401540

1541-
:math:`\CALLREF`
1542-
................
1541+
:math:`\CALLREF~x`
1542+
..................
1543+
1544+
* The type :math:`C.\CTYPES[x]` must be defined in the context.
15431545

1544-
* 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]`.
1546+
* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`C.\CTYPES[x]`.
15451547

15461548
* Then the instruction is valid with type :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`.
15471549

15481550
.. math::
15491551
\frac{
15501552
C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast]
15511553
}{
1552-
C \vdashinstr \CALLREF : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]
1554+
C \vdashinstr \CALLREF~x : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]
15531555
}
15541556
15551557

‎interpreter/binary/decode.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -318,8 +318,8 @@ let rec instr s =
318318

319319
| 0x12 | 0x13 as b -> illegal s pos b (* return_call, return_call_indirect *)
320320

321-
| 0x14 -> call_ref
322-
| 0x15 -> return_call_ref
321+
| 0x14 -> call_ref (at var s)
322+
| 0x15 -> return_call_ref (at var s)
323323

324324
| 0x16 as b -> illegal s pos b
325325

‎interpreter/binary/encode.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -197,9 +197,9 @@ struct
197197
| BrOnNonNull x -> op 0xd6; var x
198198
| Return -> op 0x0f
199199
| Call x -> op 0x10; var x
200-
| CallRef -> op 0x14
200+
| CallRef x -> op 0x14; var x
201201
| CallIndirect (x, y) -> op 0x11; var y; var x
202-
| ReturnCallRef -> op 0x15
202+
| ReturnCallRef x -> op 0x15; var x
203203

204204
| Drop -> op 0x1a
205205
| Select None -> op 0x1b

‎interpreter/exec/eval.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -222,10 +222,10 @@ let rec step (c : config) : config =
222222
| Call x, vs ->
223223
vs, [Invoke (func c.frame.inst x) @@ e.at]
224224

225-
| CallRef, Ref (NullRef _) :: vs ->
225+
| CallRef _x, Ref (NullRef _) :: vs ->
226226
vs, [Trapping "null function reference" @@ e.at]
227227

228-
| CallRef, Ref (FuncRef f) :: vs ->
228+
| CallRef _x, Ref (FuncRef f) :: vs ->
229229
vs, [Invoke f @@ e.at]
230230

231231
| CallIndirect (x, y), Num (I32 i) :: vs ->
@@ -237,11 +237,11 @@ let rec step (c : config) : config =
237237
else
238238
vs, [Trapping "indirect call type mismatch" @@ e.at]
239239

240-
| ReturnCallRef, Ref (NullRef _) :: vs ->
240+
| ReturnCallRef _x, Ref (NullRef _) :: vs ->
241241
vs, [Trapping "null function reference" @@ e.at]
242242

243-
| ReturnCallRef, vs ->
244-
(match (step {c with code = (vs, [Plain CallRef @@ e.at])}).code with
243+
| ReturnCallRef x, vs ->
244+
(match (step {c with code = (vs, [Plain (CallRef x) @@ e.at])}).code with
245245
| vs', [{it = Invoke a; at}] -> vs', [ReturningInvoke (vs', a) @@ at]
246246
| vs', [{it = Trapping s; at}] -> vs', [Trapping s @@ at]
247247
| _ -> assert false

‎interpreter/syntax/ast.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -153,9 +153,9 @@ and instr' =
153153
| BrOnNonNull of idx (* break on non-null *)
154154
| Return (* break from function body *)
155155
| Call of idx (* call function *)
156-
| CallRef (* call function through reference *)
156+
| CallRef of idx (* call function through reference *)
157157
| CallIndirect of idx * idx (* call function through table *)
158-
| ReturnCallRef (* tail call through reference *)
158+
| ReturnCallRef of idx (* tail call through reference *)
159159
| LocalGet of idx (* read local idxiable *)
160160
| LocalSet of idx (* write local idxiable *)
161161
| LocalTee of idx (* write local idxiable and keep value *)

‎interpreter/syntax/free.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,8 +108,9 @@ let rec instr (e : instr) =
108108
| If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
109109
| Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
110110
| BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
111-
| Return | CallRef | ReturnCallRef -> empty
111+
| Return -> empty
112112
| Call x -> funcs (idx x)
113+
| CallRef x | ReturnCallRef x -> types (idx x)
113114
| CallIndirect (x, y) -> tables (idx x) ++ types (idx y)
114115
| LocalGet x | LocalSet x | LocalTee x -> locals (idx x)
115116
| GlobalGet x | GlobalSet x -> globals (idx x)

‎interpreter/syntax/operators.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,9 +32,9 @@ let br_on_non_null x = BrOnNonNull x
3232

3333
let return = Return
3434
let call x = Call x
35-
let call_ref = CallRef
35+
let call_ref x = CallRef x
3636
let call_indirect x y = CallIndirect (x, y)
37-
let return_call_ref = ReturnCallRef
37+
let return_call_ref x = ReturnCallRef x
3838

3939
let local_get x = LocalGet x
4040
let local_set x = LocalSet x

‎interpreter/text/arrange.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -456,10 +456,10 @@ let rec instr e =
456456
| BrOnNonNull x -> "br_on_non_null " ^ var x, []
457457
| Return -> "return", []
458458
| Call x -> "call " ^ var x, []
459-
| CallRef -> "call_ref", []
459+
| CallRef x -> "call_ref " ^ var x, []
460460
| CallIndirect (x, y) ->
461461
"call_indirect " ^ var x, [Node ("type " ^ var y, [])]
462-
| ReturnCallRef -> "return_call_ref", []
462+
| ReturnCallRef x -> "return_call_ref " ^ var x, []
463463
| LocalGet x -> "local.get " ^ var x, []
464464
| LocalSet x -> "local.set " ^ var x, []
465465
| LocalTee x -> "local.tee " ^ var x, []

‎interpreter/text/parser.mly

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -447,8 +447,8 @@ plain_instr :
447447
| BR_ON_NON_NULL var { fun c -> br_on_non_null ($2 c label) }
448448
| RETURN { fun c -> return }
449449
| CALL var { fun c -> call ($2 c func) }
450-
| CALL_REF { fun c -> call_ref }
451-
| RETURN_CALL_REF { fun c -> return_call_ref }
450+
| CALL_REF var { fun c -> call_ref ($2 c type_) }
451+
| RETURN_CALL_REF var { fun c -> return_call_ref ($2 c type_) }
452452
| LOCAL_GET var { fun c -> local_get ($2 c local) }
453453
| LOCAL_SET var { fun c -> local_set ($2 c local) }
454454
| LOCAL_TEE var { fun c -> local_tee ($2 c local) }

‎interpreter/valid/valid.ml

Lines changed: 10 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -392,18 +392,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
392392
let FuncT (ts1, ts2) = func c x in
393393
ts1 --> ts2, []
394394

395-
| CallRef ->
396-
(match peek_ref 0 s e.at with
397-
| (_, DefHT x) ->
398-
let FuncT (ts1, ts2) = func_type c (x @@ e.at) in
399-
(ts1 @ [RefT (Null, DefHT x)]) --> ts2, []
400-
| (_, BotHT) ->
401-
[RefT (Null, BotHT)] -->... [], []
402-
| rt ->
403-
error e.at
404-
("type mismatch: instruction requires function reference type" ^
405-
" but stack has " ^ string_of_val_type (RefT rt))
406-
)
395+
| CallRef x ->
396+
let FuncT (ts1, ts2) = func_type c x in
397+
(ts1 @ [RefT (Null, DefHT x.it)]) --> ts2, []
407398

408399
| CallIndirect (x, y) ->
409400
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
413404
" but table has element type " ^ string_of_ref_type t);
414405
(ts1 @ [NumT I32T]) --> ts2, []
415406

416-
| ReturnCallRef ->
417-
(match peek_ref 0 s e.at with
418-
| (_, DefHT x) ->
419-
let FuncT (ts1, ts2) = func_type c (x @@ e.at) in
420-
require (match_result_type c.types [] ts2 c.results) e.at
421-
("type mismatch: current function requires result type " ^
422-
string_of_result_type c.results ^
423-
" but callee returns " ^ string_of_result_type ts2);
424-
(ts1 @ [RefT (Null, DefHT x)]) -->... [], []
425-
| (_, BotHT) ->
426-
[RefT (Null, BotHT)] -->... [], []
427-
| rt ->
428-
error e.at
429-
("type mismatch: instruction requires function reference type" ^
430-
" but stack has " ^ string_of_ref_type rt)
431-
)
407+
| ReturnCallRef x ->
408+
let FuncT (ts1, ts2) = func_type c x in
409+
require (match_result_type c.types [] ts2 c.results) e.at
410+
("type mismatch: current function requires result type " ^
411+
string_of_result_type c.results ^
412+
" but callee returns " ^ string_of_result_type ts2);
413+
(ts1 @ [RefT (Null, DefHT x.it)]) -->... [], []
432414

433415
| LocalGet x ->
434416
let LocalT (init, t) = local c x in

‎proposals/function-references/Overview.md

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ The function `$hof` takes a function pointer as parameter, and is invoked by `$c
4848
(type $i32-i32 (func (param i32) (result i32)))
4949
5050
(func $hof (param $f (ref $i32-i32)) (result i32)
51-
(i32.add (i32.const 10) (call_ref (i32.const 42) (local.get $f)))
51+
(i32.add (i32.const 10) (call_ref $i32-i32 (i32.const 42) (local.get $f)))
5252
)
5353
5454
(func $inc (param $i i32) (result i32)
@@ -204,21 +204,21 @@ Note: Extending block types with index sets to allow initialization status to la
204204
- iff `$f : $t`
205205
- this is a *constant instruction*
206206

207-
* `call_ref` calls a function through a reference
208-
- `call_ref : [t1* (ref null $t)] -> [t2*]`
207+
* `call_ref <typeidx>` calls a function through a reference
208+
- `call_ref $t : [t1* (ref null $t)] -> [t2*]`
209209
- iff `$t = [t1*] -> [t2*]`
210210
- traps on `null`
211211

212212
* 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`:
213-
- `return_call_ref : [t1* (ref null $t)] -> [t2*]`
213+
- `return_call_ref $t : [t1* (ref null $t)] -> [t2*]`
214214
- iff `$t = [t1*] -> [t2*]`
215215
- and `t2* <: C.result`
216216
- traps on `null`
217217

218218

219219
#### Optional References
220220

221-
* `ref.null` is generalised to take a `<heaptype>` immediate
221+
* `ref.null <heaptype>` is generalised to take a `<heaptype>` immediate
222222
- `ref.null ht: [] -> [(ref null ht)]`
223223
- iff `ht ok`
224224

@@ -227,13 +227,13 @@ Note: Extending block types with index sets to allow initialization status to la
227227
- iff `ht ok`
228228
- traps on `null`
229229

230-
* `br_on_null $l` checks for null and branches if present
230+
* `br_on_null <labelidx>` checks for null and branches if present
231231
- `br_on_null $l : [t* (ref null ht)] -> [t* (ref ht)]`
232232
- iff `$l : [t*]`
233233
- and `ht ok`
234234
- branches to `$l` on `null`, otherwise returns operand as non-null
235235

236-
* `br_on_non_null $l` checks for null and branches if not present
236+
* `br_on_non_null <labelidx>` checks for null and branches if not present
237237
- `br_on_non_null $l : [t* (ref null ht)] -> [t*]`
238238
- iff `$l : [t* (ref ht)]`
239239
- and `ht ok`
@@ -246,15 +246,15 @@ Note: Extending block types with index sets to allow initialization status to la
246246

247247
Typing of local instructions is updated to account for the initialization status of locals.
248248

249-
* `local.get $x`
249+
* `local.get <localidx>`
250250
- `local.get $x : [] -> [t]`
251251
- iff `$x : set t`
252252

253-
* `local.set $x`
253+
* `local.set <localidx>`
254254
- `local.set $x : [t] -> [] $x`
255255
- iff `$x : set? t`
256256

257-
* `local.tee $x`
257+
* `local.tee <localidx>`
258258
- `local.tee $x : [t] -> [t] $x`
259259
- iff `$x : set? t`
260260

@@ -319,8 +319,8 @@ The opcode for heap types is encoded as an `s33`.
319319

320320
| Opcode | Instruction | Immediates |
321321
| ------ | ------------------------ | ---------- |
322-
| 0x14 | `call_ref` | |
323-
| 0x15 | `return_call_ref` | |
322+
| 0x14 | `call_ref $t` | `$t : u32` |
323+
| 0x15 | `return_call_ref $t` | `$t : u32` |
324324
| 0xd3 | `ref.as_non_null` | |
325325
| 0xd4 | `br_on_null $l` | `$l : u32` |
326326
| 0xd6 | `br_on_non_null $l` | `$l : u32` |

‎test/core/br_on_non_null.wast

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@
22
(type $t (func (result i32)))
33

44
(func $nn (param $r (ref $t)) (result i32)
5-
(call_ref
5+
(call_ref $t
66
(block $l (result (ref $t))
77
(br_on_non_null $l (local.get $r))
88
(return (i32.const -1))
99
)
1010
)
1111
)
1212
(func $n (param $r (ref null $t)) (result i32)
13-
(call_ref
13+
(call_ref $t
1414
(block $l (result (ref $t))
1515
(br_on_non_null $l (local.get $r))
1616
(return (i32.const -1))
@@ -27,7 +27,7 @@
2727

2828
(func (export "unreachable") (result i32)
2929
(block $l
30-
(return (call_ref (br_on_null $l (unreachable))))
30+
(return (call_ref $t (br_on_null $l (unreachable))))
3131
)
3232
(i32.const -1)
3333
)
@@ -53,7 +53,7 @@
5353
(func $f (param i32) (result i32) (i32.mul (local.get 0) (local.get 0)))
5454

5555
(func $a (param $n i32) (param $r (ref null $t)) (result i32)
56-
(call_ref
56+
(call_ref $t
5757
(block $l (result i32 (ref $t))
5858
(return (br_on_non_null $l (local.get $n) (local.get $r)))
5959
)

0 commit comments

Comments
 (0)