Remove type annotation on ref.is_null (#100)

Author: rossberg

document/core/appendix/index-instructions.rst

@@ -221,7 +221,7 @@ Instruction                                Binary Opcode              Type
 (reserved)                                 :math:`\hex{CE}`                                                  
 (reserved)                                 :math:`\hex{CF}`                                                  
 :math:`\REFNULL~t`                         :math:`\hex{D0}`           :math:`[] \to [t]`                             :ref:`validation <valid-ref.null>`        :ref:`execution <exec-ref.null>`
-:math:`\REFISNULL~t`                       :math:`\hex{D1}`           :math:`[t] \to [\I32]`                         :ref:`validation <valid-ref.is_null>`     :ref:`execution <exec-ref.is_null>`
+:math:`\REFISNULL`                         :math:`\hex{D1}`           :math:`[t] \to [\I32]`                         :ref:`validation <valid-ref.is_null>`     :ref:`execution <exec-ref.is_null>`
 :math:`\REFFUNC~x`                         :math:`\hex{D2}`           :math:`[] \to [\FUNCREF]`                      :ref:`validation <valid-ref.func>`        :ref:`execution <exec-ref.func>`
 (reserved)                                 :math:`\hex{D3}`                                                  
 (reserved)                                 :math:`\hex{D4}`                                                  

document/core/binary/instructions.rst

@@ -91,7 +91,7 @@ Reference Instructions
    \begin{array}{llclll}
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
      \hex{D0}~~t{:}\Breftype &\Rightarrow& \REFNULL~t \\ &&|&
-     \hex{D1}~~t{:}\Breftype &\Rightarrow& \REFISNULL~t \\ &&|&
+     \hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
      \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}
 

document/core/exec/instructions.rst

@@ -203,8 +203,8 @@ Reference Instructions
 
 .. _exec-ref.is_null:
 
-:math:`\REFISNULL~t`
-....................
+:math:`\REFISNULL`
+..................
 
 1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
 
@@ -220,9 +220,9 @@ Reference Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \val~\REFISNULL~t &\stepto& \I32.\CONST~1
+   \val~\REFISNULL &\stepto& \I32.\CONST~1
      & (\iff \val = \REFNULL~t) \\
-   \val~\REFISNULL~t &\stepto& \I32.\CONST~0
+   \val~\REFISNULL &\stepto& \I32.\CONST~0
      & (\otherwise) \\
    \end{array}
 

document/core/syntax/instructions.rst

@@ -187,7 +187,7 @@ Instructions in this group are concerned with accessing :ref:`references <syntax
    \production{instruction} & \instr &::=&
      \dots \\&&|&
      \REFNULL~\reftype \\&&|&
-     \REFISNULL~\reftype \\&&|&
+     \REFISNULL \\&&|&
      \REFFUNC~\funcidx \\
    \end{array}
 

document/core/text/instructions.rst

@@ -159,7 +159,7 @@ Reference Instructions
    \begin{array}{llclll}
    \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
      \text{ref.null}~~t{:}\Trefedtype &\Rightarrow& \REFNULL~t \\ &&|&
-     \text{ref.is\_null}~~t{:}\Trefedtype &\Rightarrow& \REFISNULL~t \\ &&|&
+     \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
      \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
    \end{array}
 

document/core/valid/instructions.rst

@@ -182,15 +182,16 @@ Reference Instructions
 
 .. _valid-ref.is_null:
 
-:math:`\REFISNULL~t`
-....................
+:math:`\REFISNULL`
+..................
 
-* The instruction is valid with type :math:`[t] \to [\I32]`.
+* The instruction is valid with type :math:`[t] \to [\I32]`, for any :ref:`reference type <syntax-reftype>` :math:`t`.
 
 .. math::
    \frac{
+     t = \reftype
    }{
-     C \vdashinstr \REFISNULL~t : [t] \to [\I32]
+     C \vdashinstr \REFISNULL : [t] \to [\I32]
    }
 
 .. _valid-ref.func:

interpreter/binary/decode.ml

@@ -453,7 +453,7 @@ let rec instr s =
   | 0xcc | 0xcd | 0xce | 0xcf as b -> illegal s pos b
 
   | 0xd0 -> ref_null (ref_type s)
-  | 0xd1 -> ref_is_null (ref_type s)
+  | 0xd1 -> ref_is_null
   | 0xd2 -> ref_func (at var s)
 
   | 0xfc as b1 ->

interpreter/binary/encode.ml

@@ -230,7 +230,7 @@ let encode m =
       | DataDrop x -> op 0xfc; op 0x09; var x
 
       | RefNull t -> op 0xd0; ref_type t
-      | RefIsNull t -> op 0xd1; ref_type t
+      | RefIsNull -> op 0xd1
       | RefFunc x -> op 0xd2; var x
 
       | Const {it = I32 c; _} -> op 0x41; vs32 c

interpreter/exec/eval.ml

@@ -427,7 +427,7 @@ let rec step (c : config) : config =
       | RefNull t, vs' ->
         Ref (NullRef t) :: vs', []
 
-      | RefIsNull _, Ref r :: vs' ->
+      | RefIsNull, Ref r :: vs' ->
         (match r with
         | NullRef _ ->
           Num (I32 1l) :: vs', []

interpreter/script/js.ml

@@ -287,7 +287,7 @@ let assert_return ress ts at =
         Test (Values.I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
     | LitResult {it = Values.Ref (Values.NullRef t); _} ->
-      [ RefIsNull t @@ at;
+      [ RefIsNull @@ at;
         Test (Values.I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
     | LitResult {it = Values.Ref (ExternRef n); _} ->

interpreter/syntax/ast.ml

@@ -106,7 +106,7 @@ and instr' =
   | MemoryInit of var                 (* initialize memory range from segment *)
   | DataDrop of var                   (* drop passive data segment *)
   | RefNull of ref_type               (* null reference *)
-  | RefIsNull of ref_type             (* null test *)
+  | RefIsNull                         (* null test *)
   | RefFunc of var                    (* function reference *)
   | Const of num                      (* constant *)
   | Test of testop                    (* numeric test *)

interpreter/syntax/free.ml

@@ -62,7 +62,7 @@ let list free xs = List.fold_left union empty (List.map free xs)
 let rec instr (e : instr) =
   match e.it with
   | Unreachable | Nop | Drop | Select _ -> empty
-  | RefNull _ | RefIsNull _ -> empty
+  | RefNull _ | RefIsNull -> empty
   | RefFunc x -> funcs (var x)
   | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
   | Block (_, es) | Loop (_, es) -> block es

interpreter/syntax/operators.ml

@@ -10,7 +10,7 @@ let f32_const n = Const (F32 n.it @@ n.at)
 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 t = RefIsNull t
+let ref_is_null = RefIsNull
 
 let unreachable = Unreachable
 let nop = Nop

interpreter/text/arrange.ml

@@ -271,7 +271,7 @@ let rec instr e =
     | MemoryInit x -> "memory.init " ^ var x, []
     | DataDrop x -> "data.drop " ^ var x, []
     | RefNull t -> "ref.null", [Atom (refed_type t)]
-    | RefIsNull t -> "ref.is_null", [Atom (refed_type t)]
+    | RefIsNull -> "ref.is_null", []
     | RefFunc x -> "ref.func " ^ var x, []
     | Const n -> constop n ^ " " ^ num n, []
     | Test op -> testop op, []

interpreter/text/parser.mly

@@ -376,7 +376,7 @@ plain_instr :
   | MEMORY_INIT var { fun c -> memory_init ($2 c data) }
   | DATA_DROP var { fun c -> data_drop ($2 c data) }
   | REF_NULL ref_kind { fun c -> ref_null $2 }
-  | REF_IS_NULL ref_kind { fun c -> ref_is_null $2 }
+  | REF_IS_NULL { fun c -> ref_is_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/valid.ml

@@ -360,8 +360,12 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
   | RefNull t ->
     [] --> [RefType t]
 
-  | RefIsNull t ->
-    [RefType t] --> [NumType I32Type]
+  | RefIsNull ->
+    let t = peek 1 s in
+    require (match t with None -> true | Some t -> is_ref_type t) e.at
+      ("type mismatch: instruction requires reference type" ^
+       " but stack has " ^ string_of_infer_type t);
+    [t] -~> [Some (NumType I32Type)]
 
   | RefFunc x ->
     let _ft = func c x in

test/core/ref_func.wast

@@ -24,13 +24,13 @@
   (func $ff2)
 
   (func (export "is_null-f") (result i32)
-    (ref.is_null func (ref.func $f))
+    (ref.is_null (ref.func $f))
   )
   (func (export "is_null-g") (result i32)
-    (ref.is_null func (ref.func $g))
+    (ref.is_null (ref.func $g))
   )
   (func (export "is_null-v") (result i32)
-    (ref.is_null func (global.get $v))
+    (ref.is_null (global.get $v))
   )
 
   (func (export "set-f") (global.set $v (ref.func $f)))

test/core/ref_is_null.wast

@@ -1,9 +1,9 @@
 (module
   (func $f1 (export "funcref") (param $x funcref) (result i32)
-    (ref.is_null func (local.get $x))
+    (ref.is_null (local.get $x))
   )
   (func $f2 (export "externref") (param $x externref) (result i32)
-    (ref.is_null extern (local.get $x))
+    (ref.is_null (local.get $x))
   )
 
   (table $t1 2 funcref)

test/core/table_get.wast

@@ -17,7 +17,7 @@
   )
 
   (func (export "is_null-funcref") (param $i i32) (result i32)
-    (ref.is_null func (call $f3 (local.get $i)))
+    (ref.is_null (call $f3 (local.get $i)))
   )
 )
 

test/core/table_grow.wast

@@ -90,7 +90,7 @@
     (block
       (loop
         (local.set 2 (table.get $t (local.get 0)))
-        (br_if 1 (i32.eqz (ref.is_null func (local.get 2))))
+        (br_if 1 (i32.eqz (ref.is_null (local.get 2))))
         (br_if 1 (i32.ge_u (local.get 0) (local.get 1)))
         (local.set 0 (i32.add (local.get 0) (i32.const 1)))
         (br_if 0 (i32.le_u (local.get 0) (local.get 1)))

test/core/table_set.wast

@@ -22,7 +22,7 @@
   )
 
   (func (export "is_null-funcref") (param $i i32) (result i32)
-    (ref.is_null func (call $f3 (local.get $i)))
+    (ref.is_null (call $f3 (local.get $i)))
   )
 )