Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Commit 4b6ab3a

Browse files
rossbergrossberg
authored
Remove type annotations on ref.as_non_null and br_on_null (#31)
1 parent a4ef81c commit 4b6ab3a

File tree

17 files changed

+110
-93
lines changed

17 files changed

+110
-93
lines changed

‎document/core/appendix/algorithm.rst

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Types are representable as a set of enumerations.
2626
.. code-block:: pseudo
2727
2828
type num_type = I32 | I64 | F32 | F64
29-
type heap_type = Def(idx : nat) | Func | Extern
29+
type heap_type = Def(idx : nat) | Func | Extern | Bot
3030
type ref_type = Ref(heap : heap_type, null : bool)
3131
type val_type = num_type | ref_type | Bot
3232
@@ -52,6 +52,8 @@ Equivalence and subtyping checks can be defined on these types.
5252
return eq_def(n1, n2)
5353
case (Def(_), Func)
5454
return true
55+
case (Bot, _)
56+
return true
5557
case (_, _)
5658
return t1 = t2
5759
@@ -111,9 +113,10 @@ However, these variables are not manipulated directly by the main checking funct
111113
error_if(not is_num(actual))
112114
return actual
113115
114-
func pop_ref() : ref_type | Bot =
116+
func pop_ref() : ref_type =
115117
let actual = pop_val()
116118
error_if(not is_ref(actual))
119+
if actual = Bot then return Ref(Bot, false)
117120
return actual
118121
119122
func pop_val(expect : val_type) : val_type =
@@ -228,9 +231,9 @@ Other instructions are checked in a similar manner.
228231
pop_ref()
229232
push_val(I32)
230233
231-
case (ref.as_non_null ht)
232-
pop_ref()
233-
push_val(Ref(ht, false))
234+
case (ref.as_non_null)
235+
let rt = pop_ref()
236+
push_val(Ref(rt.heap, false))
234237
235238
   case (unreachable)
236239
      unreachable()
@@ -279,16 +282,16 @@ Other instructions are checked in a similar manner.
279282
      pop_vals(label_types(ctrls[m]))
280283
      unreachable()
281284
282-
case (br_on_null n ht)
285+
case (br_on_null n)
283286
     error_if(ctrls.size() < n)
284-
pop_ref()
287+
let rt = pop_ref()
285288
      pop_vals(label_types(ctrls[n]))
286289
      push_vals(label_types(ctrls[n]))
287-
push_val(Ref(ht, false))
290+
push_val(Ref(rt.heap, false))
288291
289292
case (call_ref)
290293
let rt = pop_ref()
291-
if (rt =/= Bot)
294+
if (rt.heap =/= Bot)
292295
error_if(not is_def(rt.heap))
293296
let t1*->t2* = lookup_def(rt.heap.def) // TODO
294297
pop_vals(t1*)

‎interpreter/binary/decode.ml

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -495,11 +495,8 @@ let rec instr s =
495495
| 0xd0 -> ref_null (heap_type s)
496496
| 0xd1 -> ref_is_null
497497
| 0xd2 -> ref_func (at var s)
498-
| 0xd3 -> ref_as_non_null (heap_type s)
499-
| 0xd4 ->
500-
let x = at var s in
501-
let t = heap_type s in
502-
br_on_null x t
498+
| 0xd3 -> ref_as_non_null
499+
| 0xd4 -> br_on_null (at var s)
503500

504501
| 0xfc as b1 ->
505502
(match op s with

‎interpreter/binary/encode.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ let encode m =
102102
| ExternHeapType -> vs7 (-0x11)
103103
| DefHeapType (SynVar x) -> vs33 x
104104
| DefHeapType (SemVar _) -> assert false
105+
| BotHeapType -> assert false
105106

106107
let ref_type = function
107108
| (Nullable, FuncHeapType) -> vs32 (-0x10l)
@@ -181,7 +182,7 @@ let encode m =
181182
| Br x -> op 0x0c; var x
182183
| BrIf x -> op 0x0d; var x
183184
| BrTable (xs, x) -> op 0x0e; vec var xs; var x
184-
| BrOnNull (x, t) -> op 0xd4; var x; heap_type t
185+
| BrOnNull x -> op 0xd4; var x
185186
| Return -> op 0x0f
186187
| Call x -> op 0x10; var x
187188
| CallRef -> op 0x14
@@ -258,7 +259,7 @@ let encode m =
258259

259260
| RefNull t -> op 0xd0; heap_type t
260261
| RefIsNull -> op 0xd1
261-
| RefAsNonNull t -> op 0xd3; heap_type t
262+
| RefAsNonNull -> op 0xd3
262263
| RefFunc x -> op 0xd2; var x
263264

264265
| Const {it = I32 c; _} -> op 0x41; vs32 c

‎interpreter/exec/eval.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,7 @@ let rec step (c : config) : config =
209209
else
210210
vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at]
211211

212-
| BrOnNull (x, _), Ref r :: vs' ->
212+
| BrOnNull x, Ref r :: vs' ->
213213
(match r with
214214
| NullRef _ ->
215215
vs', [Plain (Br x) @@ e.at]
@@ -492,7 +492,7 @@ let rec step (c : config) : config =
492492
Num (I32 0l) :: vs', []
493493
)
494494

495-
| RefAsNonNull _, Ref r :: vs' ->
495+
| RefAsNonNull, Ref r :: vs' ->
496496
(match r with
497497
| NullRef _ ->
498498
vs', [Trapping "null reference" @@ e.at]

‎interpreter/script/js.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -330,14 +330,15 @@ let assert_return ress ts at =
330330
| FuncHeapType -> is_funcref_idx
331331
| ExternHeapType -> is_externref_idx
332332
| DefHeapType _ -> is_funcref_idx
333+
| BotHeapType -> assert false
333334
in
334335
[ Call (is_ref_idx @@ at) @@ at;
335336
Test (I32 I32Op.Eqz) @@ at;
336337
BrIf (0l @@ at) @@ at ]
337338
| NullResult ->
338339
(match t with
339-
| RefType (_, t') ->
340-
[ BrOnNull (0l @@ at, t') @@ at ]
340+
| RefType _ ->
341+
[ BrOnNull (0l @@ at) @@ at ]
341342
| _ ->
342343
[ Br (0l @@ at) @@ at ]
343344
)

‎interpreter/syntax/ast.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ and instr' =
8787
| Br of idx (* break to n-th surrounding label *)
8888
| BrIf of idx (* conditional break *)
8989
| BrTable of idx list * idx (* indexed break *)
90-
| BrOnNull of idx * heap_type (* break on null *)
90+
| BrOnNull of idx (* break on null *)
9191
| Return (* break from function body *)
9292
| Call of idx (* call function *)
9393
| CallRef (* call function through reference *)
@@ -117,7 +117,7 @@ and instr' =
117117
| DataDrop of idx (* drop passive data segment *)
118118
| RefNull of heap_type (* null reference *)
119119
| RefIsNull (* null test *)
120-
| RefAsNonNull of heap_type (* null cast *)
120+
| RefAsNonNull (* null cast *)
121121
| RefFunc of idx (* function reference *)
122122
| Const of num (* constant *)
123123
| Test of testop (* numeric test *)

‎interpreter/syntax/free.ml

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ let num_type = function
6969
| I32Type | I64Type | F32Type | F64Type -> empty
7070

7171
let heap_type = function
72-
| FuncHeapType | ExternHeapType -> empty
72+
| FuncHeapType | ExternHeapType | BotHeapType -> empty
7373
| DefHeapType x -> var_type x
7474

7575
let ref_type = function
@@ -97,18 +97,17 @@ let rec instr (e : instr) =
9797
match e.it with
9898
| Unreachable | Nop | Drop -> empty
9999
| Select tso -> list value_type (Lib.Option.get tso [])
100-
| RefIsNull -> empty
101-
| RefNull t | RefAsNonNull t -> heap_type t
100+
| RefIsNull | RefAsNonNull -> empty
101+
| RefNull t -> heap_type t
102102
| RefFunc x -> funcs (idx x)
103103
| Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
104104
| Block (bt, es) | Loop (bt, es) -> block_type bt ++ block es
105105
| If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
106106
| Let (bt, ts, es) ->
107107
let free = block_type bt ++ block es in
108108
{free with locals = Lib.Fun.repeat (List.length ts) shift free.locals}
109-
| Br x | BrIf x -> labels (idx x)
109+
| Br x | BrIf x | BrOnNull x -> labels (idx x)
110110
| BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
111-
| BrOnNull (x, t) -> labels (idx x) ++ heap_type t
112111
| Return | CallRef | ReturnCallRef -> empty
113112
| Call x -> funcs (idx x)
114113
| CallIndirect (x, y) -> tables (idx x) ++ types (idx y)

‎interpreter/syntax/operators.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ let f64_const n = Const (F64 n.it @@ n.at)
1111
let ref_func x = RefFunc x
1212
let ref_null t = RefNull t
1313
let ref_is_null = RefIsNull
14-
let ref_as_non_null t = RefAsNonNull t
14+
let ref_as_non_null = RefAsNonNull
1515

1616
let unreachable = Unreachable
1717
let nop = Nop
@@ -26,7 +26,7 @@ let let_ bt ts es = Let (bt, ts, es)
2626
let br x = Br x
2727
let br_if x = BrIf x
2828
let br_table xs x = BrTable (xs, x)
29-
let br_on_null x t = BrOnNull (x, t)
29+
let br_on_null x = BrOnNull x
3030

3131
let return = Return
3232
let call x = Call x

‎interpreter/syntax/types.ml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ and var = SynVar of syn_var | SemVar of sem_var
99
and nullability = NonNullable | Nullable
1010
and num_type = I32Type | I64Type | F32Type | F64Type
1111
and ref_type = nullability * heap_type
12-
and heap_type = FuncHeapType | ExternHeapType | DefHeapType of var
12+
and heap_type =
13+
FuncHeapType | ExternHeapType | DefHeapType of var | BotHeapType
1314

1415
and value_type = NumType of num_type | RefType of ref_type | BotType
1516
and stack_type = value_type list
@@ -113,6 +114,7 @@ let sem_heap_type c = function
113114
| FuncHeapType -> FuncHeapType
114115
| ExternHeapType -> ExternHeapType
115116
| DefHeapType x -> DefHeapType (sem_var_type c x)
117+
| BotHeapType -> BotHeapType
116118

117119
let sem_ref_type c = function
118120
| (nul, t) -> (nul, sem_heap_type c t)
@@ -206,6 +208,7 @@ and string_of_heap_type = function
206208
| FuncHeapType -> "func"
207209
| ExternHeapType -> "extern"
208210
| DefHeapType x -> "(type " ^ string_of_var x ^ ")"
211+
| BotHeapType -> "unreachable"
209212

210213
and string_of_ref_type = function
211214
| (nul, t) ->

‎interpreter/text/arrange.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,7 @@ let rec instr e =
249249
| BrIf x -> "br_if " ^ var x, []
250250
| BrTable (xs, x) ->
251251
"br_table " ^ String.concat " " (list var (xs @ [x])), []
252-
| BrOnNull (x, t) -> "br_on_null " ^ var x, [Atom (heap_type t)]
252+
| BrOnNull x -> "br_on_null " ^ var x, []
253253
| Return -> "return", []
254254
| Call x -> "call " ^ var x, []
255255
| CallRef -> "call_ref", []
@@ -280,7 +280,7 @@ let rec instr e =
280280
| DataDrop x -> "data.drop " ^ var x, []
281281
| RefNull t -> "ref.null", [Atom (heap_type t)]
282282
| RefIsNull -> "ref.is_null", []
283-
| RefAsNonNull t -> "ref.as_non_null", [Atom (heap_type t)]
283+
| RefAsNonNull -> "ref.as_non_null", []
284284
| RefFunc x -> "ref.func " ^ var x, []
285285
| Const n -> constop n ^ " " ^ num n, []
286286
| Test op -> testop op, []

‎interpreter/text/parser.mly

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -370,7 +370,7 @@ plain_instr :
370370
| BR_TABLE var var_list
371371
{ fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in
372372
br_table xs x }
373-
| BR_ON_NULL var heap_type { fun c -> br_on_null ($2 c label) ($3 c) }
373+
| BR_ON_NULL var { fun c -> br_on_null ($2 c label) }
374374
| RETURN { fun c -> return }
375375
| CALL var { fun c -> call ($2 c func) }
376376
| CALL_REF { fun c -> call_ref }
@@ -407,7 +407,7 @@ plain_instr :
407407
| DATA_DROP var { fun c -> data_drop ($2 c data) }
408408
| REF_NULL heap_type { fun c -> ref_null ($2 c) }
409409
| REF_IS_NULL { fun c -> ref_is_null }
410-
| REF_AS_NON_NULL heap_type { fun c -> ref_as_non_null ($2 c) }
410+
| REF_AS_NON_NULL { fun c -> ref_as_non_null }
411411
| REF_FUNC var { fun c -> ref_func ($2 c func) }
412412
| CONST num { fun c -> fst (num $1 $2) }
413413
| TEST { fun c -> $1 }

‎interpreter/valid/match.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ and match_heap_type c a t1 t2 =
106106
| FuncDefType _ -> true
107107
)
108108
| DefHeapType x1, DefHeapType x2 -> match_var_type c a x1 x2
109+
| BotHeapType, _ -> true
109110
| _, _ -> eq_heap_type c [] t1 t2
110111

111112
and match_ref_type c a t1 t2 =

0 commit comments

Comments
 (0)