From f9646325986b6ffbaf02dd57c4fff98b6e2ffe43 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 30 Mar 2026 17:24:42 +0200 Subject: [PATCH 1/3] [interpreter] Revive heaptype on ref.null script literals --- interpreter/README.md | 2 +- interpreter/script/js.ml | 58 ++++++++++++++--------- interpreter/script/runner.ml | 27 ++++++++--- interpreter/script/script.ml | 7 ++- interpreter/text/arrange.ml | 13 +++-- interpreter/text/parser.mly | 12 +++-- spectec/src/backend-interpreter/runner.ml | 13 +++-- 7 files changed, 89 insertions(+), 43 deletions(-) diff --git a/interpreter/README.md b/interpreter/README.md index 0693b445f9..cade098659 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -453,7 +453,7 @@ action: const: ( .const ) ;; number value ( + ) ;; vector value - ( ref.null ? ) ;; null reference + ( ref.null ) ;; null reference ( ref.host ) ;; host reference ( ref.extern ) ;; external host reference diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index b92d88525d..7b4f3a8238 100644 --- a/interpreter/script/js.ml +++ b/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 -> (Null, BotHT) 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 -> "\"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) -> diff --git a/interpreter/script/runner.ml b/interpreter/script/runner.ml index b559472148..00e88c7905 100644 --- a/interpreter/script/runner.ml +++ b/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 -> "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) -> Types.(RefT (Null, ExternHT)) | 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 = diff --git a/interpreter/script/script.ml b/interpreter/script/script.ml index f1379c0242..d7167ec011 100644 --- a/interpreter/script/script.ml +++ b/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 type result = result' Source.phrase and result' = diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 811f8b48eb..b238f930f6 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -771,17 +771,21 @@ 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", []) | 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 ht -> Node ("ref.null " ^ heaptype ht, []) + let definition mode isdef x_opt def = try match mode with @@ -830,7 +834,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 +855,7 @@ let vec_pat mode = function let ref_pat = function | RefPat r -> ref_ r.it | RefTypePat t -> Node ("ref." ^ heaptype t, []) + | NullPat -> Node ("ref.null", []) let rec result mode res = match res.it with diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 1bcc33393c..2187afc525 100644 --- a/interpreter/text/parser.mly +++ b/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,7 @@ 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 heaptype? RPAR { RefResult NullPat @@ $sloc } | LPAR REF RPAR { RefResult (RefTypePat AnyHT) @@ $sloc } | LPAR REF_EQ RPAR { RefResult (RefTypePat EqHT) @@ $sloc } | LPAR REF_I31 RPAR { RefResult (RefTypePat I31HT) @@ $sloc } diff --git a/spectec/src/backend-interpreter/runner.ml b/spectec/src/backend-interpreter/runner.ml index babfc26d43..e5a925b3e2 100644 --- a/spectec/src/backend-interpreter/runner.ml +++ b/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 From 23c5ab53c758828706e4a75d9cb3b4dde2248370 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 30 Mar 2026 17:40:49 +0200 Subject: [PATCH 2/3] Preserve heaptype on NullPat as well --- interpreter/script/js.ml | 6 +++--- interpreter/script/runner.ml | 6 +++--- interpreter/script/script.ml | 2 +- interpreter/text/arrange.ml | 5 +++-- interpreter/text/parser.mly | 3 ++- 5 files changed, 12 insertions(+), 10 deletions(-) diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 7b4f3a8238..b2a1aa1e1b 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -438,7 +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 -> (Null, BotHT) + | NullPat ht -> (Null, ht) let rec type_of_result res = match res.it with @@ -558,7 +558,7 @@ let assert_return ress ts at = [ RefTest (NoNull, t) @@ at; Test (I32 I32Op.Eqz) @@ at; BrIf (0l @@ at) @@ at ] - | RefResult NullPat -> + | RefResult (NullPat _) -> [ RefIsNull @@ at; Test (I32 I32Op.Eqz) @@ at; BrIf (0l @@ at) @@ at ] @@ -741,7 +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 -> "\"ref.null\"" + | NullPat t -> "\"ref.null\"" let rec of_result res = match res.it with diff --git a/interpreter/script/runner.ml b/interpreter/script/runner.ml index 00e88c7905..0ff9fc0c0b 100644 --- a/interpreter/script/runner.ml +++ b/interpreter/script/runner.ml @@ -265,7 +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 -> "null" + | NullPat t -> "null" let rec string_of_result r = match r.it with @@ -286,7 +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) -> Types.(RefT (Null, ExternHT)) + | RefResult (NullPat t) -> Types.(RefT (Null, t)) | EitherResult rs -> let ts = List.map type_of_result rs in List.fold_left (fun t1 t2 -> @@ -473,7 +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 + | NullPat _, Value.NullRef -> true | _ -> false let rec assert_result v r = diff --git a/interpreter/script/script.ml b/interpreter/script/script.ml index d7167ec011..c2ece6ac87 100644 --- a/interpreter/script/script.ml +++ b/interpreter/script/script.ml @@ -34,7 +34,7 @@ type vec_pat = type ref_pat = | RefPat of ref_ | RefTypePat of Types.heaptype - | NullPat + | NullPat of Types.heaptype type result = result' Source.phrase and result' = diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index b238f930f6..54d5c71fdc 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -771,6 +771,7 @@ 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 + | 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 @@ -784,7 +785,7 @@ let value mode v = let literal mode lit = match lit.it with | ValLit v -> value mode v - | NullLit ht -> Node ("ref.null " ^ heaptype ht, []) + | NullLit t -> Node ("ref.null " ^ heaptype t, []) let definition mode isdef x_opt def = try @@ -855,7 +856,7 @@ let vec_pat mode = function let ref_pat = function | RefPat r -> ref_ r.it | RefTypePat t -> Node ("ref." ^ heaptype t, []) - | NullPat -> Node ("ref.null", []) + | NullPat t -> Node ("ref.null " ^ heaptype t, []) let rec result mode res = match res.it with diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 2187afc525..8d0cfdd1e3 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -1520,7 +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 heaptype? RPAR { RefResult NullPat @@ $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 } From 81162f07017e0101ac749343c57ed206e7a93d16 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 30 Mar 2026 17:43:02 +0200 Subject: [PATCH 3/3] Update README --- interpreter/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interpreter/README.md b/interpreter/README.md index cade098659..d631791bfa 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -453,7 +453,7 @@ action: const: ( .const ) ;; number value ( + ) ;; vector value - ( ref.null ) ;; null reference + ( ref.null ) ;; null reference ( ref.host ) ;; host reference ( ref.extern ) ;; external host reference