From 2389371eac0f7001736a8c18a462b0080872a289 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 13 Oct 2025 16:25:50 -0700 Subject: [PATCH 1/3] [interpreter] Return a desctype from expand_deftype This will be useful for the validation of new instructions. That validation requires being able to look up the descriptor and described types of expanded deftypes. Update existing uses of expand_deftype to add an additional comptype_of_desctype. --- interpreter/exec/eval.ml | 18 ++++++++++++------ interpreter/runtime/aggr.ml | 6 ++++-- interpreter/runtime/exn.ml | 4 ++-- interpreter/runtime/func.ml | 4 ++-- interpreter/script/js.ml | 3 ++- interpreter/script/run.ml | 4 ++-- interpreter/syntax/types.ml | 8 ++++---- interpreter/text/parser.mly | 4 ++-- interpreter/valid/match.ml | 16 +++++++++++----- interpreter/valid/valid.ml | 27 +++++++++++++++------------ 10 files changed, 56 insertions(+), 38 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index dc36be500..10de1971c 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -110,7 +110,8 @@ let data (inst : moduleinst) x = lookup "data segment" inst.datas x let elem (inst : moduleinst) x = lookup "element segment" inst.elems x let local (frame : frame) x = lookup "local" frame.locals x -let comp_type (inst : moduleinst) x = expand_deftype (type_ inst x) +let desc_type (inst : moduleinst) x = expand_deftype (type_ inst x) +let comp_type (inst : moduleinst) x = comptype_of_desctype (desc_type inst x) let struct_type (inst : moduleinst) x = structtype_of_comptype (comp_type inst x) let array_type (inst : moduleinst) x = arraytype_of_comptype (comp_type inst x) let func_type (inst : moduleinst) x = functype_of_comptype (comp_type inst x) @@ -309,7 +310,8 @@ let rec step (c : config) : config = let t = tag c.frame.inst x in let TagT ut = Tag.type_of t in let dt = deftype_of_typeuse ut in - let (ts, _) = functype_of_comptype (expand_deftype dt) in + let ct = comptype_of_desctype (expand_deftype dt) in + let (ts, _) = functype_of_comptype ct in let n = List.length ts in let args, vs' = split n vs e.at in vs', [Throwing (t, args) @@ e.at] @@ -811,8 +813,9 @@ let rec step (c : config) : config = else if n = 0l then vs', [] else + let dt = expand_deftype (Aggr.type_of_array sa) in let exto = - match arraytype_of_comptype (expand_deftype (Aggr.type_of_array sa)) with + match arraytype_of_comptype (comptype_of_desctype dt) with | FieldT (_, PackStorageT _) -> Some U | _ -> None in @@ -1071,7 +1074,8 @@ let rec step (c : config) : config = take n vs0 e.at @ vs, [] | Frame (n, frame', (vs', {it = ReturningInvoke (vs0, f); at} :: es')), vs -> - let (ts1, _ts2) = functype_of_comptype (expand_deftype (Func.type_of f)) in + let ct = comptype_of_desctype (expand_deftype (Func.type_of f)) in + let (ts1, _ts2) = functype_of_comptype ct in take (List.length ts1) vs0 e.at @ vs, [Invoke f @@ at] | Frame (n, frame', (vs', e' :: es')), vs when is_jumping e' -> @@ -1116,7 +1120,8 @@ let rec step (c : config) : config = Exhaustion.error e.at "call stack exhausted" | Invoke f, vs -> - let (ts1, ts2) = functype_of_comptype (expand_deftype (Func.type_of f)) in + let ct = comptype_of_desctype (expand_deftype (Func.type_of f)) in + let (ts1, ts2) = functype_of_comptype ct in let n1, n2 = List.length ts1, List.length ts2 in let args, vs' = split n1 vs e.at in (match f with @@ -1161,7 +1166,8 @@ let at_func = function let invoke (func : funcinst) (vs : value list) : value list = let at = at_func func in - let (ts1, _ts2) = functype_of_comptype (expand_deftype (Func.type_of func)) in + let ct = comptype_of_desctype (expand_deftype (Func.type_of func)) in + let (ts1, _ts2) = functype_of_comptype ct in if List.length vs <> List.length ts1 then Crash.error at "wrong number of arguments"; if not (List.for_all2 (fun v -> Match.match_valtype [] (type_of_value v)) vs ts1) then diff --git a/interpreter/runtime/aggr.ml b/interpreter/runtime/aggr.ml index 54ef49909..32f53ad27 100644 --- a/interpreter/runtime/aggr.ml +++ b/interpreter/runtime/aggr.ml @@ -42,12 +42,14 @@ let array_length (Array (_, fs)) = Lib.List32.length fs let alloc_struct dt vs = assert Free.((deftype dt).types = Set.empty); - let fts = structtype_of_comptype (expand_deftype dt) in + let ct = comptype_of_desctype (expand_deftype dt) in + let fts = structtype_of_comptype ct in Struct (dt, List.map2 alloc_field fts vs) let alloc_array dt vs = assert Free.((deftype dt).types = Set.empty); - let ft = arraytype_of_comptype (expand_deftype dt) in + let ct = comptype_of_desctype (expand_deftype dt) in + let ft = arraytype_of_comptype ct in Array (dt, List.map (alloc_field ft) vs) diff --git a/interpreter/runtime/exn.ml b/interpreter/runtime/exn.ml index bd341469b..e369050ac 100644 --- a/interpreter/runtime/exn.ml +++ b/interpreter/runtime/exn.ml @@ -8,8 +8,8 @@ type ref_ += ExnRef of exn_ let alloc_exn tag vs = let TagT ut = Tag.type_of tag in assert Free.((typeuse ut).types = Set.empty); - let dt = deftype_of_typeuse ut in - let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in + let dt = expand_deftype (deftype_of_typeuse ut) in + let (ts1, ts2) = functype_of_comptype (comptype_of_desctype dt) in assert (List.length vs = List.length ts1); assert (ts2 = []); Exn (tag, vs) diff --git a/interpreter/runtime/func.ml b/interpreter/runtime/func.ml index 174b922d0..41b6a17f7 100644 --- a/interpreter/runtime/func.ml +++ b/interpreter/runtime/func.ml @@ -7,12 +7,12 @@ and 'inst func = | HostFunc of deftype * (value list -> value list) let alloc dt inst f = - ignore (functype_of_comptype (expand_deftype dt)); + ignore (functype_of_comptype (comptype_of_desctype (expand_deftype dt))); assert Free.((deftype dt).types = Set.empty); AstFunc (dt, inst, f) let alloc_host dt f = - ignore (functype_of_comptype (expand_deftype dt)); + ignore (functype_of_comptype (comptype_of_desctype (expand_deftype dt))); HostFunc (dt, f) let type_of = function diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 38d1c0fc6..df5078fc3 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -771,7 +771,8 @@ let of_action env act = "[" ^ String.concat ", " (List.map of_value vs) ^ "])", (match lookup_export env x_opt name act.at with | ExternFuncT (Def dt) -> - let (_, out) as ft = functype_of_comptype (expand_deftype dt) in + let ct = comptype_of_desctype (expand_deftype dt) in + let (_, out) as ft = functype_of_comptype ct in if is_js_functype ft then None else diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml index e5e420355..19302cdb6 100644 --- a/interpreter/script/run.ml +++ b/interpreter/script/run.ml @@ -348,8 +348,8 @@ let run_action act : Value.t list = let inst = lookup_instance x_opt act.at in (match Instance.export inst name with | Some (Instance.ExternFunc f) -> - let (ts1, _ts2) = - Types.(functype_of_comptype (expand_deftype (Func.type_of f))) in + let ct = Types.(comptype_of_desctype (expand_deftype (Func.type_of f))) in + let (ts1, _ts2) = Types.(functype_of_comptype ct) in if List.length vs <> List.length ts1 then Script.error act.at "wrong number of arguments"; List.iter2 (fun v t -> diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 548cc83f6..755ec8512 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -127,6 +127,7 @@ let deftype_of_typeuse = function Def dt -> dt | _ -> assert false let structtype_of_comptype = function StructT fts -> fts | _ -> assert false let arraytype_of_comptype = function ArrayT ft -> ft | _ -> assert false let functype_of_comptype = function FuncT rt2 -> rt2 | _ -> assert false +let comptype_of_desctype = function DescT (_, _, ct) -> ct let externtype_of_importtype = function ImportT (_, _, xt) -> xt let externtype_of_exporttype = function ExportT (_, xt) -> xt @@ -282,10 +283,9 @@ let unroll_deftype (dt : deftype) : subtype = let RecT sts = unroll_rectype rt in Lib.List32.nth sts i -(* TODO: consider returning a desctype here. *) -let expand_deftype (dt : deftype) : comptype = - let SubT (_, _, DescT (_, _, st)) = unroll_deftype dt in - st +let expand_deftype (dt : deftype) : desctype = + let SubT (_, _, dt') = unroll_deftype dt in + dt' (* String conversion *) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index c14fa34b1..f96604a30 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -168,7 +168,7 @@ let field x (c : context) y = lookup "field " (Lib.List32.nth c.types.fields x) y let func_type (c : context) x = - match expand_deftype (Lib.List32.nth c.types.ctx x.it) with + match comptype_of_desctype (expand_deftype (Lib.List32.nth c.types.ctx x.it)) with | FuncT (ts1, ts2) -> ts1, ts2 | _ -> error x.at ("non-function type " ^ Int32.to_string x.it) | exception Failure _ -> error x.at ("unknown type " ^ Int32.to_string x.it) @@ -247,7 +247,7 @@ let inline_functype_explicit (c : context) x ft = let (ts1, _ts2) = func_type c x in bind "local" c.locals (Lib.List32.length ts1) x.at ) - else if ft <> func_type c x then + else if ft <> func_type c x then error x.at "inline function type does not match explicit type"; x diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index 1aeb1d88d..a7cb424f6 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -17,10 +17,13 @@ let abs_of_comptype _c = function let rec top_of_comptype c ct = top_of_heaptype c (abs_of_comptype c ct) +and top_of_desctype c dt = + top_of_comptype c (comptype_of_desctype dt) + and top_of_typeuse c = function - | Idx x -> top_of_comptype c (expand_deftype (lookup c x)) + | Idx x -> top_of_desctype c (expand_deftype (lookup c x)) | Rec _ -> assert false - | Def dt -> top_of_comptype c (expand_deftype dt) + | Def dt -> top_of_desctype c (expand_deftype dt) and top_of_heaptype c = function | AnyHT | NoneHT | EqHT | StructHT | ArrayHT | I31HT -> AnyHT @@ -40,10 +43,13 @@ let top_of_valtype c = function let rec bot_of_comptype c ct = bot_of_heaptype c (abs_of_comptype c ct) +and bot_of_desctype c dt = + bot_of_comptype c (comptype_of_desctype dt) + and bot_of_typeuse c = function - | Idx x -> bot_of_comptype c (expand_deftype (lookup c x)) + | Idx x -> bot_of_desctype c (expand_deftype (lookup c x)) | Rec _ -> assert false - | Def dt -> bot_of_comptype c (expand_deftype dt) + | Def dt -> bot_of_desctype c (expand_deftype dt) and bot_of_heaptype c = function | AnyHT | NoneHT | EqHT | StructHT | ArrayHT | I31HT -> NoneHT @@ -93,7 +99,7 @@ let rec match_heaptype c t1 t2 = | _, UseHT (Idx x2) -> match_heaptype c t1 (UseHT (Def (lookup c x2))) | UseHT (Def dt1), UseHT (Def dt2) -> match_deftype c dt1 dt2 | UseHT (Def dt), t -> - (match expand_deftype dt, t with + (match comptype_of_desctype (expand_deftype dt), t with | StructT _, AnyHT -> true | StructT _, EqHT -> true | StructT _, StructHT -> true diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 7042b4778..039a7f873 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -64,17 +64,17 @@ let init_locals (c : context) xs = List.fold_left init_local c xs let struct_type (c : context) x = - match expand_deftype (type_ c x) with + match comptype_of_desctype (expand_deftype (type_ c x)) with | StructT fts -> fts | _ -> error x.at ("non-structure type " ^ I32.to_string_u x.it) let array_type (c : context) x = - match expand_deftype (type_ c x) with + match comptype_of_desctype (expand_deftype (type_ c x)) with | ArrayT ft -> ft | _ -> error x.at ("non-array type " ^ I32.to_string_u x.it) let func_type (c : context) x = - match expand_deftype (type_ c x) with + match comptype_of_desctype (expand_deftype (type_ c x)) with | FuncT (ts1, ts2) -> ts1, ts2 | _ -> error x.at ("non-function type " ^ I32.to_string_u x.it) @@ -535,7 +535,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins c.results -->... [], [] | Call x -> - let (ts1, ts2) = functype_of_comptype (expand_deftype (func c x)) in + let ct = comptype_of_desctype (expand_deftype (func c x)) in + let (ts1, ts2) = functype_of_comptype ct in ts1 --> ts2, [] | CallRef x -> @@ -551,7 +552,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins (ts1 @ [NumT (numtype_of_addrtype at)]) --> ts2, [] | ReturnCall x -> - let (ts1, ts2) = functype_of_comptype (expand_deftype (func c x)) in + let ct = comptype_of_desctype (expand_deftype (func c x)) in + let (ts1, ts2) = functype_of_comptype ct in require (match_resulttype c.types ts2 c.results) e.at ("type mismatch: current function requires result type " ^ string_of_resulttype c.results ^ @@ -580,8 +582,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins | Throw x -> let TagT ut = tag c x in - let dt = deftype_of_typeuse ut in - let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in + let dt = expand_deftype (deftype_of_typeuse ut) in + let (ts1, ts2) = functype_of_comptype (comptype_of_desctype dt) in ts1 -->... [], [] | ThrowRef -> @@ -985,13 +987,13 @@ and check_catch (c : context) (cc : catch) (ts : valtype list) at = match cc.it with | Catch (x1, x2) -> let TagT ut = tag c x1 in - let dt = deftype_of_typeuse ut in - let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in + let dt = expand_deftype (deftype_of_typeuse ut) in + let (ts1, ts2) = functype_of_comptype (comptype_of_desctype dt) in match_target c ts1 (label c x2) cc.at | CatchRef (x1, x2) -> let TagT ut = tag c x1 in - let dt = deftype_of_typeuse ut in - let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in + let dt = expand_deftype (deftype_of_typeuse ut) in + let (ts1, ts2) = functype_of_comptype (comptype_of_desctype dt) in match_target c (ts1 @ [RefT (NoNull, ExnHT)]) (label c x2) cc.at | CatchAll x -> match_target c [] (label c x) cc.at @@ -1118,7 +1120,8 @@ let check_type (c : context) (t : type_) : context = let check_start (c : context) (start : start) = let Start x = start.it in - let ft = functype_of_comptype (expand_deftype (func c x)) in + let ct = comptype_of_desctype (expand_deftype (func c x)) in + let ft = functype_of_comptype ct in require (ft = ([], [])) start.at "start function must not have parameters or results" From 0296c5e7c765ee24ac7af01cccb276dae0c84f54 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Oct 2025 17:41:44 -0700 Subject: [PATCH 2/3] problem --- interpreter/text/parser.mly | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index f96604a30..120c1b83c 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -168,7 +168,8 @@ let field x (c : context) y = lookup "field " (Lib.List32.nth c.types.fields x) y let func_type (c : context) x = - match comptype_of_desctype (expand_deftype (Lib.List32.nth c.types.ctx x.it)) with + let dt = expand_deftype (Lib.List32.nth c.types.ctx x.it) in + match comptype_of_desctype dt with | FuncT (ts1, ts2) -> ts1, ts2 | _ -> error x.at ("non-function type " ^ Int32.to_string x.it) | exception Failure _ -> error x.at ("unknown type " ^ Int32.to_string x.it) From 3fe73b9746044bb1f09a6064f6e8ca71c54d2081 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Oct 2025 19:17:30 -0700 Subject: [PATCH 3/3] Revert "problem" This reverts commit 0296c5e7c765ee24ac7af01cccb276dae0c84f54. --- interpreter/text/parser.mly | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 120c1b83c..f96604a30 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -168,8 +168,7 @@ let field x (c : context) y = lookup "field " (Lib.List32.nth c.types.fields x) y let func_type (c : context) x = - let dt = expand_deftype (Lib.List32.nth c.types.ctx x.it) in - match comptype_of_desctype dt with + match comptype_of_desctype (expand_deftype (Lib.List32.nth c.types.ctx x.it)) with | FuncT (ts1, ts2) -> ts1, ts2 | _ -> error x.at ("non-function type " ^ Int32.to_string x.it) | exception Failure _ -> error x.at ("unknown type " ^ Int32.to_string x.it)