[interpreter] Revive heaptype on ref.null script literals (#2129)

Author: rossberg

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 <heap_type> )                   ;; null reference
   ( ref.host <nat> )                         ;; host reference
   ( ref.extern <nat> )                       ;; external host reference
 

interpreter/script/js.ml

@@ -390,30 +390,33 @@ let abs_mask_of = function
   | I32T | F32T -> I32 Int32.max_int
   | I64T | F64T -> I64 Int64.max_int
 
-let value v t =
-  match v.it, t with
-  | Num n, _ -> [Const (n @@ v.at) @@ v.at]
-  | Vec s, _ -> [VecConst (s @@ v.at) @@ v.at]
-  | Ref NullRef, (RefT (_, ht)) ->
-    [ RefNull (Match.bot_of_heaptype [] ht) @@ v.at ]
-  | Ref (HostRef n), _ ->
-    [ Const (I32 n @@ v.at) @@ v.at;
-      Call (hostref_idx @@ v.at) @@ v.at;
+let value v at =
+  match v with
+  | Num n -> [Const (n @@ at) @@ at]
+  | Vec s -> [VecConst (s @@ at) @@ at]
+  | Ref (HostRef n) ->
+    [ Const (I32 n @@ at) @@ at;
+      Call (hostref_idx @@ at) @@ at;
     ]
-  | Ref (Extern.ExternRef (HostRef n)), _ ->
-    [ Const (I32 n @@ v.at) @@ v.at;
-      Call (hostref_idx @@ v.at) @@ v.at;
-      ExternConvert Externalize @@ v.at;
+  | Ref (Extern.ExternRef (HostRef n)) ->
+    [ Const (I32 n @@ at) @@ at;
+      Call (hostref_idx @@ at) @@ at;
+      ExternConvert Externalize @@ at;
     ]
-  | Ref _, _ -> assert false
+  | Ref _ -> assert false
+
+let literal lit =
+  match lit.it with
+  | ValLit v -> value v lit.at
+  | NullLit ht -> [RefNull (Match.bot_of_heaptype [] ht) @@ lit.at]
 
-let invoke dt vs ts at =
+let invoke dt lits at =
   let dummy = RecT [SubT (Final, [], FuncT ([], []))] in
   let rts0 = Lib.List32.init subject_type_idx (fun i -> dummy, (dummy, i)) in
   let rts, i = statify_deftype rts0 dt in
   List.map (fun (_, (rt, _)) -> rt @@ at) (Lib.List32.drop subject_type_idx rts),
   ExternFuncT (Idx i),
-  List.concat (List.map2 value vs ts) @ [Call (subject_idx @@ at) @@ at]
+  List.concat (List.map literal lits) @ [Call (subject_idx @@ at) @@ at]
 
 let get t at =
   [], ExternGlobalT t, [GlobalGet (subject_idx @@ at) @@ at]
@@ -435,6 +438,7 @@ let type_of_vec_pat = function
 let type_of_ref_pat = function
   | RefPat ref -> type_of_ref ref.it
   | RefTypePat ht -> (NoNull, ht)
+  | NullPat ht -> (Null, ht)
 
 let rec type_of_result res =
   match res.it with
@@ -554,6 +558,10 @@ let assert_return ress ts at =
       [ RefTest (NoNull, t) @@ at;
         Test (I32 I32Op.Eqz) @@ at;
         BrIf (0l @@ at) @@ at ]
+    | RefResult (NullPat _) ->
+      [ RefIsNull @@ at;
+        Test (I32 I32Op.Eqz) @@ at;
+        BrIf (0l @@ at) @@ at ]
     | EitherResult ress ->
       let idx = Lib.List32.length !locals in
       locals := !locals @ [Local t @@ res.at];
@@ -704,12 +712,17 @@ let of_ref r =
   | HostRef n | Extern.ExternRef (HostRef n) -> "hostref(" ^ Int32.to_string n ^ ")"
   | _ -> assert false
 
-let of_value v =
-  match v.it with
+let of_val v =
+  match v with
   | Num n -> of_num n
   | Vec v -> of_vec v
   | Ref r -> of_ref r
 
+let of_lit lit =
+  match lit.it with
+  | ValLit v -> of_val v
+  | NullLit _ -> "null"
+
 let of_nan = function
   | CanonicalNan -> "\"nan:canonical\""
   | ArithmeticNan -> "\"nan:arithmetic\""
@@ -728,6 +741,7 @@ let of_vec_pat = function
 let of_ref_pat = function
   | RefPat r -> of_ref r.it
   | RefTypePat t -> "\"ref." ^ string_of_heaptype t ^ "\""
+  | NullPat t -> "\"ref.null\""
 
 let rec of_result res =
   match res.it with
@@ -753,16 +767,16 @@ let of_wrapper env x_opt name wrap_action wrap_assertion at =
 
 let of_action env act =
   match act.it with
-  | Invoke (x_opt, name, vs) ->
+  | Invoke (x_opt, name, lits) ->
     "call(" ^ of_inst_opt env x_opt ^ ", " ^ of_name name ^ ", " ^
-      "[" ^ String.concat ", " (List.map of_value vs) ^ "])",
+      "[" ^ String.concat ", " (List.map of_lit lits) ^ "])",
     (match lookup_export env x_opt name act.at with
     | ExternFuncT (Def dt) ->
-      let (ins, out) as ft = functype_of_comptype (expand_deftype dt) in
+      let (_, ts) as ft = functype_of_comptype (expand_deftype dt) in
       if is_js_functype ft then
         None
       else
-        Some (of_wrapper env x_opt name (invoke dt vs ins), out)
+        Some (of_wrapper env x_opt name (invoke dt lits), ts)
     | _ -> None
     )
   | Get (x_opt, name) ->

interpreter/script/runner.ml

@@ -265,6 +265,7 @@ let string_of_ref_pat (p : ref_pat) =
   match p with
   | RefPat r -> Value.string_of_ref r.it
   | RefTypePat t -> Types.string_of_heaptype t
+  | NullPat t -> "null"
 
 let rec string_of_result r =
   match r.it with
@@ -285,6 +286,7 @@ let rec type_of_result r =
   | VecResult (VecPat v) -> Types.VecT (Value.type_of_vec v)
   | RefResult (RefPat r) -> Types.RefT (Value.type_of_ref r.it)
   | RefResult (RefTypePat t) -> Types.(RefT (NoNull, t))  (* assume closed *)
+  | RefResult (NullPat t) -> Types.(RefT (Null, t))
   | EitherResult rs ->
     let ts = List.map type_of_result rs in
     List.fold_left (fun t1 t2 ->
@@ -357,6 +359,16 @@ let register_instance name inst =
 
 (* Running *)
 
+let value_of_lit lit =
+  match lit.it with
+  | ValLit v -> v
+  | NullLit ht -> Value.(Ref NullRef)
+
+let type_of_lit lit =
+  match lit.it with
+  | ValLit v -> Value.type_of_value v
+  | NullLit ht -> Types.RefT (Types.Null, ht)
+
 let validity = function
   | Ok t -> ()
   | Error (at, msg) -> Invalid.error at msg
@@ -389,20 +401,20 @@ let run_instantiation m =
 
 let run_action act : Value.t list =
   match act.it with
-  | Invoke (x_opt, name, vs) ->
+  | Invoke (x_opt, name, lits) ->
     trace ("Invoking function \"" ^ Types.string_of_name name ^ "\"...");
     let inst = lookup_instance x_opt act.at in
     (match Engine.module_export inst name with
     | Some (Engine.ExternFunc f) ->
       let (ts1, _ts2) =
         Types.(functype_of_comptype (expand_deftype (Engine.func_type f))) in
-      if List.length vs <> List.length ts1 then
+      if List.length lits <> List.length ts1 then
         Script.error act.at "wrong number of arguments";
-      List.iter2 (fun v t ->
-        if not (Match.match_valtype [] (Value.type_of_value v.it) t) then
-          Script.error v.at "wrong type of argument"
-      ) vs ts1;
-      result (Engine.func_call f (List.map (fun v -> v.it) vs))
+      List.iter2 (fun lit t ->
+        if not (Match.match_valtype [] (type_of_lit lit) t) then
+          Script.error lit.at "wrong type of argument"
+      ) lits ts1;
+      result (Engine.func_call f (List.map value_of_lit lits))
     | Some _ -> Assert.error act.at "export is not a function"
     | None -> Assert.error act.at "undefined export"
     )
@@ -461,6 +473,7 @@ let assert_ref_pat r p =
   | RefTypePat Types.FuncHT, Instance.FuncRef _
   | RefTypePat Types.ExnHT, Exn.ExnRef _
   | RefTypePat Types.ExternHT, _ -> true
+  | NullPat _, Value.NullRef -> true
   | _ -> false
 
 let rec assert_result v r =

interpreter/script/script.ml

@@ -3,7 +3,11 @@ type var = string Source.phrase
 type Value.ref_ += HostRef of int32
 type num = Value.num Source.phrase
 type ref_ = Value.ref_ Source.phrase
-type literal = Value.t Source.phrase
+
+type literal = literal' Source.phrase
+and literal' =
+  | ValLit of Value.t
+  | NullLit of Types.heaptype
 
 type definition = definition' Source.phrase
 and definition' =
@@ -30,6 +34,7 @@ type vec_pat =
 type ref_pat =
   | RefPat of ref_
   | RefTypePat of Types.heaptype
+  | NullPat of Types.heaptype
 
 type result = result' Source.phrase
 and result' =

interpreter/text/arrange.ml

@@ -771,17 +771,22 @@ let num mode = if mode = `Binary then hex_string_of_num else string_of_num
 let vec mode = if mode = `Binary then hex_string_of_vec else string_of_vec
 
 let ref_ = function
-  | NullRef -> Node ("ref.null", [])
+  | Value.NullRef -> Node ("ref.null", [])
   | Script.HostRef n -> Node ("ref.host " ^ nat32 n, [])
   | Extern.ExternRef (Script.HostRef n) -> Node ("ref.extern " ^ nat32 n, [])
   | _ -> assert false
 
-let literal mode lit =
-  match lit.it with
+let value mode v =
+  match v with
   | Num n -> Node (constop n ^ " " ^ num mode n, [])
   | Vec v -> Node (vconstop v ^ " " ^ vec mode v, [])
   | Ref r -> ref_ r
 
+let literal mode lit =
+  match lit.it with
+  | ValLit v -> value mode v
+  | NullLit t -> Node ("ref.null " ^ heaptype t, [])
+
 let definition mode isdef x_opt def =
   try
     match mode with
@@ -830,7 +835,7 @@ let nanop (n : nanop) =
   | _ -> .
 
 let num_pat mode = function
-  | NumPat n -> literal mode (Value.Num n.it @@ n.at)
+  | NumPat n -> literal mode (ValLit (Value.Num n.it) @@ n.at)
   | NanPat nan -> Node (constop nan.it ^ " " ^ nanop nan, [])
 
 let lane_pat mode pat shape =
@@ -851,6 +856,7 @@ let vec_pat mode = function
 let ref_pat = function
   | RefPat r -> ref_ r.it
   | RefTypePat t -> Node ("ref." ^ heaptype t, [])
+  | NullPat t -> Node ("ref.null " ^ heaptype t, [])
 
 let rec result mode res =
   match res.it with

interpreter/text/parser.mly

@@ -1500,14 +1500,17 @@ literal_vec :
   | LPAR VEC_CONST VECSHAPE list(num) RPAR { snd (vec $2 $3 $4 $sloc) }
 
 literal_ref :
-  | LPAR REF_NULL heaptype? RPAR { Value.NullRef }
   | LPAR REF_HOST NAT RPAR { Script.HostRef (nat32 $3 $loc($3)) }
   | LPAR REF_EXTERN NAT RPAR { Extern.ExternRef (Script.HostRef (nat32 $3 $loc($3))) }
 
+literal_null :
+  | LPAR REF_NULL heaptype RPAR { $3 (empty_context ()) }
+
 literal :
-  | literal_num { Value.Num $1 @@ $sloc }
-  | literal_vec { Value.Vec $1 @@ $sloc }
-  | literal_ref { Value.Ref $1 @@ $sloc }
+  | literal_num { ValLit (Value.Num $1) @@ $sloc }
+  | literal_vec { ValLit (Value.Vec $1) @@ $sloc }
+  | literal_ref { ValLit (Value.Ref $1) @@ $sloc }
+  | literal_null { NullLit $1 @@ $sloc }
 
 numpat :
   | num { fun sh -> vec_lane_lit sh $1.it $1.at }
@@ -1517,6 +1520,8 @@ result :
   | literal_num { NumResult (NumPat ($1 @@ $sloc)) @@ $sloc }
   | LPAR CONST NAN RPAR { NumResult (NanPat (nanop $2 ($3 @@ $loc($3)))) @@ $sloc }
   | literal_ref { RefResult (RefPat ($1 @@ $sloc)) @@ $sloc }
+  | LPAR REF_NULL RPAR { RefResult (RefPat (Value.NullRef @@ $sloc)) @@ $sloc }
+  | LPAR REF_NULL heaptype RPAR { RefResult (NullPat ($3 (empty_context ()))) @@ $sloc }
   | LPAR REF RPAR { RefResult (RefTypePat AnyHT) @@ $sloc }
   | LPAR REF_EQ RPAR { RefResult (RefTypePat EqHT) @@ $sloc }
   | LPAR REF_I31 RPAR { RefResult (RefTypePat I31HT) @@ $sloc }

spectec/src/backend-interpreter/runner.ml

@@ -128,11 +128,16 @@ let err_exit = ref true
 
 (** Main functions **)
 
+let value_of_arg = function
+  | ValLit v -> v
+  | NullLit _ -> Value.(Ref NullRef)
+
 let invoke module_name funcname args =
-  log "[Invoking %s %s...]\n" funcname (Value.string_of_values args);
+  let values = List.map value_of_arg args in
+  log "[Invoking %s %s...]\n" funcname (Value.string_of_values values);
 
   let funcaddr = get_export_addr funcname module_name in
-  Interpreter.invoke [funcaddr; al_of_list al_of_value args]
+  Interpreter.invoke [funcaddr; al_of_list al_of_value values]
 
 
 let get_global_value module_name globalname =
@@ -296,10 +301,10 @@ let run_wasm' args module_ =
   (* TODO: Only Int32 arguments/results are acceptable *)
   match args with
   | funcname :: args' ->
-    let make_value s = Value.Num (I32 (Int32.of_string s)) in
+    let make_lit s = ValLit (Value.Num (I32 (Int32.of_string s))) in
 
     (* Invoke *)
-    invoke (Register.get_module_name None) funcname (List.map make_value args')
+    invoke (Register.get_module_name None) funcname (List.map make_lit args')
     (* Print invocation result *)
     |> al_to_list al_to_value
     |> Value.string_of_values