From 4cc25505ad2f6889797dc0818a27af7b38577b66 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Jun 2025 15:44:55 +0200
Subject: [PATCH] [interpreter/spec] Consistent nullability for br_on_non_null

---
 document/core/valid/instructions.rst |  2 +-
 interpreter/valid/valid.ml           | 11 +++++------
 test/core/br_on_non_null.wast        | 18 ++++++++++++++++--
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 21632d6afb..e5f952aa02 100644
--- a/document/core/valid/instructions.rst
+++ b/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]
    }
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 759da3c5a8..c62dabd098 100644
--- a/interpreter/valid/valid.ml
+++ b/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) ->
diff --git a/test/core/br_on_non_null.wast b/test/core/br_on_non_null.wast
index 43800194fe..e25dd4f020 100644
--- a/test/core/br_on_non_null.wast
+++ b/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))