[interpreter/spec] Consistent nullability for br_on_non_null (#1940)

Author: rossberg

document/core/valid/instructions.rst

@@ -2317,7 +2317,7 @@ Control Instructions
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [t^\ast~(\REF~\X{ht})]
+     C.\CLABELS[l] = [t^\ast~(\REF~\NULL^?~\X{ht})]
    }{
      C \vdashinstr \BRONNONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]
    }

interpreter/valid/valid.ml

@@ -461,15 +461,14 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
     (label c x @ [RefT (Null, ht)]) --> (label c x @ [RefT (NoNull, ht)]), []
 
   | BrOnNonNull x ->
-    let (_nul, ht) = peek_ref 0 s e.at in
-    let t' = RefT (NoNull, ht) in
     require (label c x <> []) e.at
-      ("type mismatch: instruction requires type " ^ string_of_val_type t' ^
+      ("type mismatch: instruction requires reference type" ^
        " but label has " ^ string_of_result_type (label c x));
     let ts0, t1 = Lib.List.split_last (label c x) in
-    require (match_val_type c.types t' t1) e.at
-      ("type mismatch: instruction requires type " ^ string_of_val_type t' ^
-       " but label has " ^ string_of_result_type (label c x));
+    require (is_ref_type t1) e.at
+      ("type mismatch: instruction requires reference type" ^
+       " but label has " ^ string_of_val_type t1);
+    let ht = match t1 with RefT (_nul, ht) -> ht | _ -> assert false in
     (ts0 @ [RefT (Null, ht)]) --> ts0, []
 
   | BrOnCast (x, rt1, rt2) ->

test/core/br_on_non_null.wast

@@ -17,13 +17,25 @@
       )
     )
   )
+  (func $n2 (param $r (ref null $t)) (result i32)
+    (call_ref $t
+      (ref.as_non_null
+        (block $l (result (ref null $t))
+          (br_on_non_null $l (local.get $r))
+          (return (i32.const -2))
+        )
+      )
+    )
+  )
 
   (elem func $f)
   (func $f (result i32) (i32.const 7))
 
-  (func (export "nullable-null") (result i32) (call $n (ref.null $t)))
   (func (export "nonnullable-f") (result i32) (call $nn (ref.func $f)))
+  (func (export "nullable-null") (result i32) (call $n (ref.null $t)))
   (func (export "nullable-f") (result i32) (call $n (ref.func $f)))
+  (func (export "nullable2-null") (result i32) (call $n2 (ref.null $t)))
+  (func (export "nullable2-f") (result i32) (call $n2 (ref.func $f)))
 
   (func (export "unreachable") (result i32)
     (block $l (result (ref $t))
@@ -36,9 +48,11 @@
 
 (assert_trap (invoke "unreachable") "unreachable")
 
-(assert_return (invoke "nullable-null") (i32.const -1))
 (assert_return (invoke "nonnullable-f") (i32.const 7))
+(assert_return (invoke "nullable-null") (i32.const -1))
 (assert_return (invoke "nullable-f") (i32.const 7))
+(assert_return (invoke "nullable2-null") (i32.const -2))
+(assert_return (invoke "nullable2-f") (i32.const 7))
 
 (module
   (type $t (func))