[spec] Narrow definition of null ref values (#2093)

Author: rossberg

document/core/exec/instructions.rst

@@ -687,19 +687,9 @@ Reference Instructions
 :math:`\REFNULL~x`
 .......................
 
-1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
-
-2. Assert: due to :ref:`validation <valid-ref.null>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[x]` exists.
-
-3. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[x]`.
+$${rule-prose: Step_read/ref.null}
 
-4. Push the value :math:`\REFNULL~\deftype` to the stack.
-
-$${rule: {Step_read/ref.null-*}}
-
-.. note::
-   No formal reduction rule is required for the case |REFNULL| |ABSHEAPTYPE|,
-   since the instruction form is already a :ref:`value <syntax-val>`.
+$${rule: {Step_read/ref.null}}
 
 
 .. _exec-ref.func:

document/core/exec/runtime.rst

@@ -12,7 +12,6 @@ Runtime Structure
 .. _syntax-num:
 .. _syntax-vec:
 .. _syntax-ref:
-.. _syntax-addrref:
 .. _syntax-ref.i31num:
 .. _syntax-ref.struct:
 .. _syntax-ref.array:
@@ -34,14 +33,15 @@ It is convenient to reuse the same notation as for the ${:CONST} :ref:`instructi
 
 References other than null are represented with additional :ref:`administrative instructions <syntax-instr-admin>`.
 They either are *scalar references*, containing a 31-bit :ref:`integer <syntax-int>`,
+*null references*,
 *structure references*, pointing to a specific :ref:`structure address <syntax-structaddr>`,
 *array references*, pointing to a specific :ref:`array address <syntax-arrayaddr>`,
 *function references*, pointing to a specific :ref:`function address <syntax-funcaddr>`,
 *exception references*, pointing to a specific :ref:`exception address <syntax-exnaddr>`,
 or *host references* pointing to an uninterpreted form of :ref:`host address <syntax-hostaddr>` defined by the :ref:`embedder <embedder>`.
 Any of the aformentioned references can furthermore be wrapped up as an *external reference*.
 
-$${syntax: val num vec ref addrref}
+$${syntax: val num vec ref}
 
 .. note::
    Future versions of WebAssembly may add additional forms of values.
@@ -590,7 +590,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
 
 $${syntax: {instr/admin}}
 
-An :ref:`address reference <syntax-addrref>` represents an allocated :ref:`reference <syntax-ref>` value of respective form :ref:`"on the stack" <exec-notation>`.
+A :ref:`reference <syntax-ref>` represents a :ref:`reference <syntax-ref>` value of respective form :ref:`"on the stack" <exec-notation>`.
 
 The ${:LABEL}, ${:FRAME}, and ${:HANDLER} instructions model :ref:`labels <syntax-label>`, :ref:`frames <syntax-frame>`, and active :ref:`exception handlers <syntax-handler>`, respectively, :ref:`"on the stack" <exec-notation>`.
 Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instrs>`.

document/core/exec/values.rst

@@ -46,11 +46,6 @@ $${rule-prose: Ref_ok/null}
 
 $${rule: Ref_ok/null}
 
-.. note::
-   A null reference can be typed with any smaller type.
-   In particular, that allows it to be typed with the least type in its respective hierarchy.
-   That ensures that the value is compatible with any nullable type in that hierarchy.
-
 
 .. _valid-ref.i31num:
 

document/core/util/macros.def

@@ -1531,6 +1531,7 @@
 .. Administrative Instructions, terminals
 
 .. |REFI31NUM| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}i\scriptstyle31}}
+.. |REFNULLADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}null}}
 .. |REFFUNCADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}func}}
 .. |REFSTRUCTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}struct}}
 .. |REFARRAYADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}array}}
@@ -1545,7 +1546,6 @@
 .. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}}
 .. |vec| mathdef:: \xref{exec/runtime}{syntax-vec}{\X{vec}}
 .. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}}
-.. |addrref| mathdef:: \xref{exec/runtime}{syntax-addrref}{\X{addrref}}
 .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
 .. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}
 

interpreter/README.md

@@ -453,7 +453,7 @@ action:
 const:
   ( <num_type>.const <num> )                 ;; number value
   ( <vec_type> <vec_shape> <num>+ )          ;; vector value
-  ( ref.null <ref_kind> )                    ;; null reference
+  ( ref.null <ref_kind>? )                   ;; null reference
   ( ref.host <nat> )                         ;; host reference
   ( ref.extern <nat> )                       ;; external host reference
 

interpreter/exec/eval.ml

@@ -126,7 +126,7 @@ let any_ref (inst : moduleinst) x i at =
 let func_ref (inst : moduleinst) x i at =
   match any_ref inst x i at with
   | FuncRef f -> f
-  | NullRef _ -> Trap.error at ("uninitialized element " ^ Int64.to_string i)
+  | NullRef -> Trap.error at ("uninitialized element " ^ Int64.to_string i)
   | _ -> Crash.error at ("type mismatch for element " ^ Int64.to_string i)
 
 let blocktype (inst : moduleinst) bt at =
@@ -231,13 +231,13 @@ let rec step (c : config) : config =
         else
           vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at]
 
-      | BrOnNull x, Ref (NullRef _) :: vs' ->
+      | BrOnNull x, Ref NullRef :: vs' ->
         vs', [Plain (Br x) @@ e.at]
 
       | BrOnNull x, Ref r :: vs' ->
         Ref r :: vs', []
 
-      | BrOnNonNull x, Ref (NullRef _) :: vs' ->
+      | BrOnNonNull x, Ref NullRef :: vs' ->
         vs', []
 
       | BrOnNonNull x, Ref r :: vs' ->
@@ -263,7 +263,7 @@ let rec step (c : config) : config =
       | Call x, vs ->
         vs, [Invoke (func c.frame.inst x) @@ e.at]
 
-      | CallRef _x, Ref (NullRef _) :: vs ->
+      | CallRef _x, Ref NullRef :: vs ->
         vs, [Trapping "null function reference" @@ e.at]
 
       | CallRef _x, Ref (FuncRef f) :: vs ->
@@ -285,7 +285,7 @@ let rec step (c : config) : config =
         | _ -> assert false
         )
 
-      | ReturnCallRef _x, Ref (NullRef _) :: vs ->
+      | ReturnCallRef _x, Ref NullRef :: vs ->
         vs, [Trapping "null function reference" @@ e.at]
 
       | ReturnCallRef x, vs ->
@@ -313,7 +313,7 @@ let rec step (c : config) : config =
         let args, vs' = split n vs e.at in
         vs', [Throwing (t, args) @@ e.at]
 
-      | ThrowRef, Ref (NullRef _) :: vs ->
+      | ThrowRef, Ref NullRef :: vs ->
         vs, [Trapping "null exception reference" @@ e.at]
 
       | ThrowRef, Ref (Exn.(ExnRef (Exn (t, args)))) :: vs ->
@@ -627,19 +627,19 @@ let rec step (c : config) : config =
         vs, []
 
       | RefNull t, vs' ->
-        Ref (NullRef (subst_heaptype (subst_of c.frame.inst) t)) :: vs', []
+        Ref NullRef :: vs', []
 
       | RefFunc x, vs' ->
         let f = func c.frame.inst x in
         Ref (FuncRef f) :: vs', []
 
-      | RefIsNull, Ref (NullRef _) :: vs' ->
+      | RefIsNull, Ref NullRef :: vs' ->
         value_of_bool true :: vs', []
 
       | RefIsNull, Ref _ :: vs' ->
         value_of_bool false :: vs', []
 
-      | RefAsNonNull, Ref (NullRef _) :: vs' ->
+      | RefAsNonNull, Ref NullRef :: vs' ->
         vs', [Trapping "null reference" @@ e.at]
 
       | RefAsNonNull, Ref r :: vs' ->
@@ -664,7 +664,7 @@ let rec step (c : config) : config =
       | RefI31, Num (I32 i) :: vs' ->
         Ref (I31.I31Ref (I31.of_i32 i)) :: vs', []
 
-      | I31Get ext, Ref (NullRef _) :: vs' ->
+      | I31Get ext, Ref NullRef :: vs' ->
         vs', [Trapping "null i31 reference" @@ e.at]
 
       | I31Get ext, Ref (I31.I31Ref i) :: vs' ->
@@ -687,7 +687,7 @@ let rec step (c : config) : config =
           with Failure _ -> Crash.error e.at "type mismatch packing value"
         in Ref (Aggr.StructRef struct_) :: vs'', []
 
-      | StructGet (x, i, exto), Ref (NullRef _) :: vs' ->
+      | StructGet (x, i, exto), Ref NullRef :: vs' ->
         vs', [Trapping "null structure reference" @@ e.at]
 
       | StructGet (x, i, exto), Ref Aggr.(StructRef (Struct (_, fs))) :: vs' ->
@@ -698,7 +698,7 @@ let rec step (c : config) : config =
         (try Aggr.read_field f exto :: vs', []
         with Failure _ -> Crash.error e.at "type mismatch reading field")
 
-      | StructSet (x, i), v :: Ref (NullRef _) :: vs' ->
+      | StructSet (x, i), v :: Ref NullRef :: vs' ->
         vs', [Trapping "null structure reference" @@ e.at]
 
       | StructSet (x, i), v :: Ref Aggr.(StructRef (Struct (_, fs))) :: vs' ->
@@ -765,7 +765,7 @@ let rec step (c : config) : config =
             with Failure _ -> Crash.error e.at "type mismatch packing value"
           in Ref (Aggr.ArrayRef array) :: vs', []
 
-      | ArrayGet (x, exto), Num (I32 i) :: Ref (NullRef _) :: vs' ->
+      | ArrayGet (x, exto), Num (I32 i) :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayGet (x, exto), Num (I32 i) :: Ref (Aggr.ArrayRef a) :: vs'
@@ -776,7 +776,7 @@ let rec step (c : config) : config =
         (try Aggr.read_field (Lib.List32.nth fs i) exto :: vs', []
         with Failure _ -> Crash.error e.at "type mismatch reading array")
 
-      | ArraySet x, v :: Num (I32 i) :: Ref (NullRef _) :: vs' ->
+      | ArraySet x, v :: Num (I32 i) :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArraySet x, v :: Num (I32 i) :: Ref (Aggr.ArrayRef a) :: vs'
@@ -787,18 +787,18 @@ let rec step (c : config) : config =
         (try Aggr.write_field (Lib.List32.nth fs i) v; vs', []
         with Failure _ -> Crash.error e.at "type mismatch writing array")
 
-      | ArrayLen, Ref (NullRef _) :: vs' ->
+      | ArrayLen, Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayLen, Ref Aggr.(ArrayRef (Array (_, fs))) :: vs' ->
         Num (I32 (Lib.List32.length fs)) :: vs', []
 
       | ArrayCopy (x, y),
-        Num _ :: Num _ :: Ref (NullRef _) :: Num _ :: Ref _ :: vs' ->
+        Num _ :: Num _ :: Ref NullRef :: Num _ :: Ref _ :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayCopy (x, y),
-        Num _ :: Num _ :: Ref _ :: Num _ :: Ref (NullRef _) :: vs' ->
+        Num _ :: Num _ :: Ref _ :: Num _ :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayCopy (x, y),
@@ -846,7 +846,7 @@ let rec step (c : config) : config =
             Plain (ArraySet x);
           ]
 
-      | ArrayFill x, Num (I32 n) :: v :: Num (I32 i) :: Ref (NullRef _) :: vs' ->
+      | ArrayFill x, Num (I32 n) :: v :: Num (I32 i) :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayFill x, Num (I32 n) :: v :: Num (I32 i) :: Ref (Aggr.ArrayRef a) :: vs' ->
@@ -868,7 +868,7 @@ let rec step (c : config) : config =
           ]
 
       | ArrayInitData (x, y),
-        Num _ :: Num _ :: Num _ :: Ref (NullRef _) :: vs' ->
+        Num _ :: Num _ :: Num _ :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayInitData (x, y),
@@ -899,7 +899,7 @@ let rec step (c : config) : config =
           ]
 
       | ArrayInitElem (x, y),
-        Num _ :: Num _ :: Num _ :: Ref (NullRef _) :: vs' ->
+        Num _ :: Num _ :: Num _ :: Ref NullRef :: vs' ->
         vs', [Trapping "null array reference" @@ e.at]
 
       | ArrayInitElem (x, y),
@@ -926,14 +926,14 @@ let rec step (c : config) : config =
             Plain (ArrayInitElem (x, y));
           ]
 
-      | ExternConvert Internalize, Ref (NullRef _) :: vs' ->
-        Ref (NullRef NoneHT) :: vs', []
+      | ExternConvert Internalize, Ref NullRef :: vs' ->
+        Ref NullRef :: vs', []
 
       | ExternConvert Internalize, Ref (Extern.ExternRef r) :: vs' ->
         Ref r :: vs', []
 
-      | ExternConvert Externalize, Ref (NullRef _) :: vs' ->
-        Ref (NullRef NoExternHT) :: vs', []
+      | ExternConvert Externalize, Ref NullRef :: vs' ->
+        Ref NullRef :: vs', []
 
       | ExternConvert Externalize, Ref r :: vs' ->
         Ref (Extern.ExternRef r) :: vs', []

interpreter/host/spectest.ml

@@ -15,17 +15,17 @@ let global (GlobalT (_, t) as gt) =
     | NumT F32T -> Num (F32 (F32.of_float 666.6))
     | NumT F64T -> Num (F64 (F64.of_float 666.6))
     | VecT V128T -> Vec (V128 (V128.I32x4.of_lanes [666l; 666l; 666l; 666l]))
-    | RefT (_, t) -> Ref (NullRef t)
+    | RefT _ -> Ref NullRef
     | BotT -> assert false
   in Some (ExternGlobal (Global.alloc gt v))
 
 let table =
   let tt = TableT (I32AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in
-  Some (ExternTable (Table.alloc tt (NullRef FuncHT)))
+  Some (ExternTable (Table.alloc tt NullRef))
 
 let table64 =
   let tt = TableT (I64AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in
-  Some (ExternTable (Table.alloc tt (NullRef FuncHT)))
+  Some (ExternTable (Table.alloc tt NullRef))
 
 let memory =
   let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}) in

interpreter/runtime/value.ml

@@ -17,7 +17,7 @@ type ref_ = ..
 type value = Num of num | Vec of vec | Ref of ref_
 type t = value
 
-type ref_ += NullRef of heaptype
+type ref_ += NullRef
 
 type address = I64.t
 
@@ -89,7 +89,7 @@ struct
 end
 
 let is_null_ref = function
-  | NullRef _ -> true
+  | NullRef -> true
   | _ -> false
 
 
@@ -109,7 +109,7 @@ let type_of_vec = type_of_vecop
 
 let type_of_ref' = ref (function _ -> assert false)
 let type_of_ref = function
-  | NullRef t -> (Null, Match.bot_of_heaptype [] t)
+  | NullRef -> (Null, BotHT)
   | r -> (NoNull, !type_of_ref' r)
 
 let type_of_value = function
@@ -124,11 +124,7 @@ let eq_num n1 n2 = n1 = n2
 
 let eq_vec v1 v2 = v1 = v2
 
-let eq_ref' = ref (fun r1 r2 ->
-  match r1, r2 with
-  | NullRef _, NullRef _ -> true
-  | _, _ -> r1 == r2
-)
+let eq_ref' = ref (==)
 
 let eq_ref r1 r2 = !eq_ref' r1 r2
 
@@ -152,7 +148,7 @@ let default_vec = function
   | V128T -> Some (Vec (V128 V128.zero))
 
 let default_ref = function
-  | (Null, t) -> Some (Ref (NullRef t))
+  | (Null, _) -> Some (Ref NullRef)
   | (NoNull, _) -> None
 
 let default_value = function
@@ -323,7 +319,7 @@ let hex_string_of_vec = function
 
 let string_of_ref' = ref (function _ -> "ref")
 let string_of_ref = function
-  | NullRef _ -> "null"
+  | NullRef -> "null"
   | r -> !string_of_ref' r
 
 let string_of_value = function