Skip to content

Commit b0aa23f

Browse files
authored
[interpreter/spec] Consistent nullability for br_on_non_null (#1940)
1 parent e40554f commit b0aa23f

File tree

3 files changed

+22
-9
lines changed

3 files changed

+22
-9
lines changed

document/core/valid/instructions.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2317,7 +2317,7 @@ Control Instructions
23172317

23182318
.. math::
23192319
\frac{
2320-
C.\CLABELS[l] = [t^\ast~(\REF~\X{ht})]
2320+
C.\CLABELS[l] = [t^\ast~(\REF~\NULL^?~\X{ht})]
23212321
}{
23222322
C \vdashinstr \BRONNONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]
23232323
}

interpreter/valid/valid.ml

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -461,15 +461,14 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
461461
(label c x @ [RefT (Null, ht)]) --> (label c x @ [RefT (NoNull, ht)]), []
462462

463463
| BrOnNonNull x ->
464-
let (_nul, ht) = peek_ref 0 s e.at in
465-
let t' = RefT (NoNull, ht) in
466464
require (label c x <> []) e.at
467-
("type mismatch: instruction requires type " ^ string_of_val_type t' ^
465+
("type mismatch: instruction requires reference type" ^
468466
" but label has " ^ string_of_result_type (label c x));
469467
let ts0, t1 = Lib.List.split_last (label c x) in
470-
require (match_val_type c.types t' t1) e.at
471-
("type mismatch: instruction requires type " ^ string_of_val_type t' ^
472-
" but label has " ^ string_of_result_type (label c x));
468+
require (is_ref_type t1) e.at
469+
("type mismatch: instruction requires reference type" ^
470+
" but label has " ^ string_of_val_type t1);
471+
let ht = match t1 with RefT (_nul, ht) -> ht | _ -> assert false in
473472
(ts0 @ [RefT (Null, ht)]) --> ts0, []
474473

475474
| BrOnCast (x, rt1, rt2) ->

test/core/br_on_non_null.wast

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,25 @@
1717
)
1818
)
1919
)
20+
(func $n2 (param $r (ref null $t)) (result i32)
21+
(call_ref $t
22+
(ref.as_non_null
23+
(block $l (result (ref null $t))
24+
(br_on_non_null $l (local.get $r))
25+
(return (i32.const -2))
26+
)
27+
)
28+
)
29+
)
2030

2131
(elem func $f)
2232
(func $f (result i32) (i32.const 7))
2333

24-
(func (export "nullable-null") (result i32) (call $n (ref.null $t)))
2534
(func (export "nonnullable-f") (result i32) (call $nn (ref.func $f)))
35+
(func (export "nullable-null") (result i32) (call $n (ref.null $t)))
2636
(func (export "nullable-f") (result i32) (call $n (ref.func $f)))
37+
(func (export "nullable2-null") (result i32) (call $n2 (ref.null $t)))
38+
(func (export "nullable2-f") (result i32) (call $n2 (ref.func $f)))
2739

2840
(func (export "unreachable") (result i32)
2941
(block $l (result (ref $t))
@@ -36,9 +48,11 @@
3648

3749
(assert_trap (invoke "unreachable") "unreachable")
3850

39-
(assert_return (invoke "nullable-null") (i32.const -1))
4051
(assert_return (invoke "nonnullable-f") (i32.const 7))
52+
(assert_return (invoke "nullable-null") (i32.const -1))
4153
(assert_return (invoke "nullable-f") (i32.const 7))
54+
(assert_return (invoke "nullable2-null") (i32.const -2))
55+
(assert_return (invoke "nullable2-f") (i32.const 7))
4256

4357
(module
4458
(type $t (func))

0 commit comments

Comments
 (0)