Remove type annotations on ref.as_non_null and br_on_null

document/core/appendix/algorithm.rst

@@ -26,7 +26,7 @@ Types are representable as a set of enumerations.
 .. code-block:: pseudo
 
    type num_type = I32 | I64 | F32 | F64
-   type heap_type = Def(idx : nat) | Func | Extern
+   type heap_type = Def(idx : nat) | Func | Extern | Bot
    type ref_type = Ref(heap : heap_type, null : bool)
    type val_type = num_type | ref_type | Bot
 
@@ -52,6 +52,8 @@ Equivalence and subtyping checks can be defined on these types.
          return eq_def(n1, n2)
        case (Def(_), Func)
          return true
+       case (Bot, _)
+         return true
        case (_, _)
          return t1 = t2
 
@@ -111,9 +113,10 @@ However, these variables are not manipulated directly by the main checking funct
      error_if(not is_num(actual))
      return actual
 
-   func pop_ref() : ref_type | Bot =
+   func pop_ref() : ref_type =
      let actual = pop_val()
      error_if(not is_ref(actual))
+     if actual = Bot then return Ref(Bot, false)
      return actual
 
    func pop_val(expect : val_type) : val_type =
@@ -228,9 +231,9 @@ Other instructions are checked in a similar manner.
          pop_ref()
          push_val(I32)
 
-       case (ref.as_non_null ht)
-         pop_ref()
-         push_val(Ref(ht, false))
+       case (ref.as_non_null)
+         let rt = pop_ref()
+         push_val(Ref(rt.heap, false))
 
        case (unreachable)
          unreachable()
@@ -279,16 +282,16 @@ Other instructions are checked in a similar manner.
          pop_vals(label_types(ctrls[m]))
          unreachable()
 
-       case (br_on_null n ht)
+       case (br_on_null n)
          error_if(ctrls.size() < n)
-         pop_ref()
+         let rt = pop_ref()
          pop_vals(label_types(ctrls[n]))
          push_vals(label_types(ctrls[n]))
-         push_val(Ref(ht, false))
+         push_val(Ref(rt.heap, false))
 
        case (call_ref)
          let rt = pop_ref()
-         if (rt =/= Bot)
+         if (rt.heap =/= Bot)
            error_if(not is_def(rt.heap))
            let t1*->t2* = lookup_def(rt.heap.def)  // TODO
            pop_vals(t1*)

interpreter/binary/decode.ml

@@ -495,11 +495,8 @@ let rec instr s =
   | 0xd0 -> ref_null (heap_type s)
   | 0xd1 -> ref_is_null
   | 0xd2 -> ref_func (at var s)
-  | 0xd3 -> ref_as_non_null (heap_type s)
-  | 0xd4 ->
-    let x = at var s in
-    let t = heap_type s in
-    br_on_null x t
+  | 0xd3 -> ref_as_non_null
+  | 0xd4 -> br_on_null (at var s)
 
   | 0xfc as b1 ->
     (match op s with

interpreter/binary/encode.ml

@@ -102,6 +102,7 @@ let encode m =
       | ExternHeapType -> vs7 (-0x11)
       | DefHeapType (SynVar x) -> vs33 x
       | DefHeapType (SemVar _) -> assert false
+      | BotHeapType -> assert false
 
     let ref_type = function
       | (Nullable, FuncHeapType) -> vs32 (-0x10l)
@@ -181,7 +182,7 @@ let encode m =
       | Br x -> op 0x0c; var x
       | BrIf x -> op 0x0d; var x
       | BrTable (xs, x) -> op 0x0e; vec var xs; var x
-      | BrOnNull (x, t) -> op 0xd4; var x; heap_type t
+      | BrOnNull x -> op 0xd4; var x
       | Return -> op 0x0f
       | Call x -> op 0x10; var x
       | CallRef -> op 0x14
@@ -258,7 +259,7 @@ let encode m =
 
       | RefNull t -> op 0xd0; heap_type t
       | RefIsNull -> op 0xd1
-      | RefAsNonNull t -> op 0xd3; heap_type t
+      | RefAsNonNull -> op 0xd3
       | RefFunc x -> op 0xd2; var x
 
       | Const {it = I32 c; _} -> op 0x41; vs32 c

interpreter/exec/eval.ml

@@ -209,7 +209,7 @@ let rec step (c : config) : config =
         else
           vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at]
 
-      | BrOnNull (x, _), Ref r :: vs' ->
+      | BrOnNull x, Ref r :: vs' ->
         (match r with
         | NullRef _ ->
           vs', [Plain (Br x) @@ e.at]
@@ -492,7 +492,7 @@ let rec step (c : config) : config =
           Num (I32 0l) :: vs', []
         )
 
-      | RefAsNonNull _, Ref r :: vs' ->
+      | RefAsNonNull, Ref r :: vs' ->
         (match r with
         | NullRef _ ->
           vs', [Trapping "null reference" @@ e.at]

interpreter/script/js.ml

@@ -330,14 +330,15 @@ let assert_return ress ts at =
         | FuncHeapType -> is_funcref_idx
         | ExternHeapType -> is_externref_idx
         | DefHeapType _ -> is_funcref_idx
+        | BotHeapType -> assert false
       in
       [ Call (is_ref_idx @@ at) @@ at;
         Test (I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
     | NullResult ->
       (match t with
-      | RefType (_, t') ->
-        [ BrOnNull (0l @@ at, t') @@ at ]
+      | RefType _ ->
+        [ BrOnNull (0l @@ at) @@ at ]
       | _ ->
         [ Br (0l @@ at) @@ at ]
       )

interpreter/syntax/ast.ml

@@ -87,7 +87,7 @@ and instr' =
   | Br of idx                         (* break to n-th surrounding label *)
   | BrIf of idx                       (* conditional break *)
   | BrTable of idx list * idx         (* indexed break *)
-  | BrOnNull of idx * heap_type       (* break on null *)
+  | BrOnNull of idx                   (* break on null *)
   | Return                            (* break from function body *)
   | Call of idx                       (* call function *)
   | CallRef                           (* call function through reference *)
@@ -117,7 +117,7 @@ and instr' =
   | DataDrop of idx                   (* drop passive data segment *)
   | RefNull of heap_type              (* null reference *)
   | RefIsNull                         (* null test *)
-  | RefAsNonNull of heap_type         (* null cast *)
+  | RefAsNonNull                      (* null cast *)
   | RefFunc of idx                    (* function reference *)
   | Const of num                      (* constant *)
   | Test of testop                    (* numeric test *)

interpreter/syntax/free.ml

@@ -69,7 +69,7 @@ let num_type = function
   | I32Type | I64Type | F32Type | F64Type -> empty
 
 let heap_type = function
-  | FuncHeapType | ExternHeapType -> empty
+  | FuncHeapType | ExternHeapType | BotHeapType -> empty
   | DefHeapType x -> var_type x
 
 let ref_type = function
@@ -97,18 +97,17 @@ let rec instr (e : instr) =
   match e.it with
   | Unreachable | Nop | Drop -> empty
   | Select tso -> list value_type (Lib.Option.get tso [])
-  | RefIsNull -> empty
-  | RefNull t | RefAsNonNull t -> heap_type t
+  | RefIsNull | RefAsNonNull -> empty
+  | RefNull t -> heap_type t
   | RefFunc x -> funcs (idx x)
   | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
   | Block (bt, es) | Loop (bt, es) -> block_type bt ++ block es
   | If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
   | Let (bt, ts, es) ->
     let free = block_type bt ++ block es in
     {free with locals = Lib.Fun.repeat (List.length ts) shift free.locals}
-  | Br x | BrIf x -> labels (idx x)
+  | Br x | BrIf x | BrOnNull x -> labels (idx x)
   | BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
-  | BrOnNull (x, t) -> labels (idx x) ++ heap_type t
   | Return | CallRef | ReturnCallRef -> empty
   | Call x -> funcs (idx x)
   | CallIndirect (x, y) -> tables (idx x) ++ types (idx y)

interpreter/syntax/operators.ml

@@ -11,7 +11,7 @@ let f64_const n = Const (F64 n.it @@ n.at)
 let ref_func x = RefFunc x
 let ref_null t = RefNull t
 let ref_is_null = RefIsNull
-let ref_as_non_null t = RefAsNonNull t
+let ref_as_non_null = RefAsNonNull
 
 let unreachable = Unreachable
 let nop = Nop
@@ -26,7 +26,7 @@ let let_ bt ts es = Let (bt, ts, es)
 let br x = Br x
 let br_if x = BrIf x
 let br_table xs x = BrTable (xs, x)
-let br_on_null x t = BrOnNull (x, t)
+let br_on_null x = BrOnNull x
 
 let return = Return
 let call x = Call x

interpreter/syntax/types.ml

@@ -9,7 +9,8 @@ and var = SynVar of syn_var | SemVar of sem_var
 and nullability = NonNullable | Nullable
 and num_type = I32Type | I64Type | F32Type | F64Type
 and ref_type = nullability * heap_type
-and heap_type = FuncHeapType | ExternHeapType | DefHeapType of var
+and heap_type =
+  FuncHeapType | ExternHeapType | DefHeapType of var | BotHeapType
 
 and value_type = NumType of num_type | RefType of ref_type | BotType
 and stack_type = value_type list
@@ -113,6 +114,7 @@ let sem_heap_type c = function
   | FuncHeapType -> FuncHeapType
   | ExternHeapType -> ExternHeapType
   | DefHeapType x -> DefHeapType (sem_var_type c x)
+  | BotHeapType -> BotHeapType
 
 let sem_ref_type c = function
   | (nul, t) -> (nul, sem_heap_type c t)
@@ -206,6 +208,7 @@ and string_of_heap_type = function
   | FuncHeapType -> "func"
   | ExternHeapType -> "extern"
   | DefHeapType x -> "(type " ^ string_of_var x ^ ")"
+  | BotHeapType -> "unreachable"
 
 and string_of_ref_type = function
   | (nul, t) ->

interpreter/text/arrange.ml

@@ -249,7 +249,7 @@ let rec instr e =
     | BrIf x -> "br_if " ^ var x, []
     | BrTable (xs, x) ->
       "br_table " ^ String.concat " " (list var (xs @ [x])), []
-    | BrOnNull (x, t) -> "br_on_null " ^ var x, [Atom (heap_type t)]
+    | BrOnNull x -> "br_on_null " ^ var x, []
     | Return -> "return", []
     | Call x -> "call " ^ var x, []
     | CallRef -> "call_ref", []
@@ -280,7 +280,7 @@ let rec instr e =
     | DataDrop x -> "data.drop " ^ var x, []
     | RefNull t -> "ref.null", [Atom (heap_type t)]
     | RefIsNull -> "ref.is_null", []
-    | RefAsNonNull t -> "ref.as_non_null", [Atom (heap_type t)]
+    | RefAsNonNull -> "ref.as_non_null", []
     | RefFunc x -> "ref.func " ^ var x, []
     | Const n -> constop n ^ " " ^ num n, []
     | Test op -> testop op, []

interpreter/text/parser.mly

@@ -370,7 +370,7 @@ plain_instr :
   | BR_TABLE var var_list
     { fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in
       br_table xs x }
-  | BR_ON_NULL var heap_type { fun c -> br_on_null ($2 c label) ($3 c) }
+  | BR_ON_NULL var { fun c -> br_on_null ($2 c label) }
   | RETURN { fun c -> return }
   | CALL var { fun c -> call ($2 c func) }
   | CALL_REF { fun c -> call_ref }
@@ -407,7 +407,7 @@ plain_instr :
   | DATA_DROP var { fun c -> data_drop ($2 c data) }
   | REF_NULL heap_type { fun c -> ref_null ($2 c) }
   | REF_IS_NULL { fun c -> ref_is_null }
-  | REF_AS_NON_NULL heap_type { fun c -> ref_as_non_null ($2 c) }
+  | REF_AS_NON_NULL { fun c -> ref_as_non_null }
   | REF_FUNC var { fun c -> ref_func ($2 c func) }
   | CONST num { fun c -> fst (num $1 $2) }
   | TEST { fun c -> $1 }

interpreter/valid/match.ml

@@ -106,6 +106,7 @@ and match_heap_type c a t1 t2 =
     | FuncDefType _ -> true
     )
   | DefHeapType x1, DefHeapType x2 -> match_var_type c a x1 x2
+  | BotHeapType, _ -> true
   | _, _ -> eq_heap_type c [] t1 t2
 
 and match_ref_type c a t1 t2 =