From 1d143333f74d73c57670bd5f7cc4de614bafb639 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 29 Jan 2026 13:51:26 -0800 Subject: [PATCH 1/4] Stub new type handling to fix the SpecTec build Update backend-interpreter/construct.ml to avoid compile errors in the due to the changes to the type system in the reference interpreter. Stub out most of the handling of new functionality and leave TODOs so we can easily find the places to update later. --- spectec/src/backend-interpreter/construct.ml | 37 ++++++++++++++------ 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml index d5d9538df..a17fa2990 100644 --- a/spectec/src/backend-interpreter/construct.ml +++ b/spectec/src/backend-interpreter/construct.ml @@ -130,9 +130,12 @@ and al_to_comptype: value -> comptype = function FuncT (al_to_resulttype rt1, (al_to_resulttype rt2)) | v -> error_value "comptype" v +and al_to_desctype: value-> desctype = function + | v -> DescT (None, None, al_to_comptype v) (* TODO *) + and al_to_subtype: value -> subtype = function | CaseV ("SUB", [ fin; tul; st ]) -> - SubT (al_to_final fin, al_to_list al_to_typeuse tul, al_to_comptype st) + SubT (al_to_final fin, al_to_list al_to_typeuse tul, al_to_desctype st) | v -> error_value "subtype" v and al_to_rectype: value -> rectype = function @@ -172,7 +175,7 @@ and al_to_heaptype: value -> heaptype = function | "EXTERN" | "EXTERNREF" -> ExternHT | "NOEXTERN" -> NoExternHT | _ -> error_value "absheaptype" v) - | CaseV (("_IDX" | "REC" | "_DEF"), _) as v -> UseHT (al_to_typeuse v) + | CaseV (("_IDX" | "REC" | "_DEF"), _) as v -> UseHT (Inexact, al_to_typeuse v) (* TODO: exactness *) | v -> error_value "heaptype" v and al_to_reftype: value -> reftype = function @@ -825,8 +828,10 @@ and al_to_instr': value -> Ast.instr' = function | CaseV ("REF.EQ", []) -> RefEq | CaseV ("REF.I31", []) -> RefI31 | CaseV ("I31.GET", [ sx ]) -> I31Get (al_to_sx sx) - | CaseV ("STRUCT.NEW", [ idx ]) -> StructNew (al_to_idx idx, Explicit) - | CaseV ("STRUCT.NEW_DEFAULT", [ idx ]) -> StructNew (al_to_idx idx, Implicit) + | CaseV ("STRUCT.NEW", [ idx ]) -> StructNew (al_to_idx idx, Explicit, NoDesc) + | CaseV ("STRUCT.NEW_DEFAULT", [ idx ]) -> StructNew (al_to_idx idx, Implicit, NoDesc) + | CaseV ("STRUCT.NEW_DESC", [ idx ]) -> StructNew (al_to_idx idx, Explicit, Desc) + | CaseV ("STRUCT.NEW_DEFAULT_DESC", [ idx ]) -> StructNew (al_to_idx idx, Implicit, Desc) | CaseV ("STRUCT.GET", [ sx_opt; idx1; idx2 ]) -> StructGet (al_to_idx idx1, al_to_nat32 idx2, al_to_opt al_to_sx sx_opt) | CaseV ("STRUCT.SET", [ idx1; idx2 ]) -> StructSet (al_to_idx idx1, al_to_nat32 idx2) @@ -914,7 +919,7 @@ let al_to_data': value -> data' = function let al_to_data: value -> data = al_to_phrase al_to_data' let al_to_externtype = function - | CaseV ("FUNC", [typeuse]) -> ExternFuncT (al_to_typeuse typeuse) + | CaseV ("FUNC", [typeuse]) -> ExternFuncT (Inexact, al_to_typeuse typeuse) (* TODO: exactness *) | CaseV ("GLOBAL", [globaltype]) -> ExternGlobalT (al_to_globaltype globaltype) | CaseV ("TABLE", [tabletype]) -> ExternTableT (al_to_tabletype tabletype) | CaseV ("MEM", [memtype]) -> ExternMemoryT (al_to_memorytype memtype) @@ -990,7 +995,8 @@ and al_to_struct: value -> Aggr.struct_ = function | StrV r when Record.mem "TYPE" r && Record.mem "FIELDS" r -> Aggr.Struct ( al_to_deftype (Record.find "TYPE" r), - al_to_list al_to_field (Record.find "FIELDS" r) + al_to_list al_to_field (Record.find "FIELDS" r), + None (* TODO: descriptors *) ) | v -> error_value "struct" v @@ -1145,9 +1151,12 @@ and al_of_comptype = function else CaseV ("FUNC", [ al_of_resulttype rt1; al_of_resulttype rt2 ]) +and al_of_desctype = function + | DescT (_, _, ct) -> al_of_comptype ct (* TODO *) + and al_of_subtype = function | SubT (fin, tul, st) -> - CaseV ("SUB", [ al_of_final fin; al_of_list al_of_typeuse tul; al_of_comptype st ]) + CaseV ("SUB", [ al_of_final fin; al_of_list al_of_typeuse tul; al_of_desctype st ]) and al_of_rectype = function | RecT stl -> CaseV ("REC", [ al_of_list al_of_subtype stl ]) @@ -1166,7 +1175,7 @@ and al_of_typeuse_of_idx = function | idx -> CaseV ("_IDX", [ al_of_idx idx ]) and al_of_heaptype = function - | UseHT tu -> al_of_typeuse tu + | UseHT (_, tu) -> al_of_typeuse tu (* TODO: exactness *) | BotHT -> nullary "BOT" | FuncHT | ExternHT as ht when !version <= 2 -> string_of_heaptype ht ^ "REF" |> nullary @@ -1818,6 +1827,10 @@ let rec al_of_instr instr = CaseV ("BR_ON_CAST", [ al_of_idx idx; al_of_reftype rt1; al_of_reftype rt2 ]) | BrOnCastFail (idx, rt1, rt2) -> CaseV ("BR_ON_CAST_FAIL", [ al_of_idx idx; al_of_reftype rt1; al_of_reftype rt2 ]) + | BrOnCastDescEq (idx, rt1, rt2) -> + CaseV ("BR_ON_CAST_DESC_EQ", [ al_of_idx idx; al_of_reftype rt1; al_of_reftype rt2 ]) + | BrOnCastDescEqFail (idx, rt1, rt2) -> + CaseV ("BR_ON_CAST_DESC_EQ_FAIL", [ al_of_idx idx; al_of_reftype rt1; al_of_reftype rt2 ]) | Return -> nullary "RETURN" | Call idx -> CaseV ("CALL", [ al_of_idx idx ]) | CallRef idx -> CaseV ("CALL_REF", [ al_of_typeuse_of_idx idx ]) @@ -1851,11 +1864,13 @@ let rec al_of_instr instr = | RefAsNonNull -> nullary "REF.AS_NON_NULL" | RefTest rt -> CaseV ("REF.TEST", [ al_of_reftype rt ]) | RefCast rt -> CaseV ("REF.CAST", [ al_of_reftype rt ]) + | RefCastDescEq rt -> CaseV ("REF.CAST_DESC_EQ", [ al_of_reftype rt ]) + | RefGetDesc idx -> CaseV ("REF.GET_DESC", [ al_of_idx idx ]) | RefEq -> nullary "REF.EQ" | RefI31 -> nullary "REF.I31" | I31Get sx -> CaseV ("I31.GET", [ al_of_sx sx ]) - | StructNew (idx, Explicit) -> CaseV ("STRUCT.NEW", [ al_of_idx idx ]) - | StructNew (idx, Implicit) -> CaseV ("STRUCT.NEW_DEFAULT", [ al_of_idx idx ]) + | StructNew (idx, Explicit, _) -> CaseV ("STRUCT.NEW", [ al_of_idx idx ]) (* TODO: descriptors *) + | StructNew (idx, Implicit, _) -> CaseV ("STRUCT.NEW_DEFAULT", [ al_of_idx idx ]) (* TODO: descriptors *) | StructGet (idx1, idx2, sx_opt) -> CaseV ("STRUCT.GET", [ al_of_opt al_of_sx sx_opt; @@ -1978,7 +1993,7 @@ let al_of_data data = let al_of_externtype = function - | ExternFuncT (typeuse) -> CaseV ("FUNC", [al_of_typeuse typeuse]) + | ExternFuncT (_, typeuse) -> CaseV ("FUNC", [al_of_typeuse typeuse]) (* TODO: exactness *) | ExternGlobalT (globaltype) -> CaseV ("GLOBAL", [al_of_globaltype globaltype]) | ExternTableT (tabletype) -> CaseV ("TABLE", [al_of_tabletype tabletype]) | ExternMemoryT (memtype) -> CaseV ("MEM", [al_of_memorytype memtype]) From 3ab96b3a63bda7b4b0fa6208bf9705c74d90a808 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 29 Jan 2026 16:47:48 -0800 Subject: [PATCH 2/4] [spec] Update br_on_cast validation As described in the overview, relax validation so that the input and output types need only be in the same hierarchy rather than requiring that the output type be a subtype of the input type. In addition to updating the SpecTec source of truth, add notes about what the extra supertypes in the formal rules are achieving. These notes are modeled on the similar note that already exists for ref.cast_desc. --- document/core/valid/instructions.rst | 6 ++++++ .../wasm-3.0/2.3-validation.instructions.spectec | 8 ++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index d92dd7d19..6013d4de2 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -235,6 +235,9 @@ $${rule-prose: Instr_ok/br_on_cast} $${rule: Instr_ok/br_on_cast} +.. note:: + The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy. + .. _valid-br_on_cast_fail: @@ -245,6 +248,9 @@ $${rule-prose: Instr_ok/br_on_cast_fail} $${rule: Instr_ok/br_on_cast_fail} +.. note:: + The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy. + .. _valid-call: diff --git a/specification/wasm-3.0/2.3-validation.instructions.spectec b/specification/wasm-3.0/2.3-validation.instructions.spectec index a89f98c09..967bc37b2 100644 --- a/specification/wasm-3.0/2.3-validation.instructions.spectec +++ b/specification/wasm-3.0/2.3-validation.instructions.spectec @@ -98,7 +98,9 @@ rule Instr_ok/br_on_cast: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_sub: C |- rt_2 <: rt_1 + -- Reftype_ok: C |- rt_3 : OK + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- rt_2 <: rt rule Instr_ok/br_on_cast_fail: @@ -106,7 +108,9 @@ rule Instr_ok/br_on_cast_fail: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_sub: C |- rt_2 <: rt_1 + -- Reftype_ok: C |- rt_3 : OK + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt From 1b8d0213c21f04a0f08ab1d53bf955880040d8c2 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 2 Feb 2026 21:50:26 -0800 Subject: [PATCH 3/4] move changes to wasm-latest --- .../wasm-3.0/2.3-validation.instructions.spectec | 8 ++------ .../wasm-latest/2.3-validation.instructions.spectec | 8 ++++++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/specification/wasm-3.0/2.3-validation.instructions.spectec b/specification/wasm-3.0/2.3-validation.instructions.spectec index b5e28139f..e57e5d90f 100644 --- a/specification/wasm-3.0/2.3-validation.instructions.spectec +++ b/specification/wasm-3.0/2.3-validation.instructions.spectec @@ -98,9 +98,7 @@ rule Instr_ok/br_on_cast: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_ok: C |- rt_3 : OK - -- Reftype_sub: C |- rt_1 <: rt_3 - -- Reftype_sub: C |- rt_2 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_1 -- Reftype_sub: C |- rt_2 <: rt rule Instr_ok/br_on_cast_fail: @@ -108,9 +106,7 @@ rule Instr_ok/br_on_cast_fail: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_ok: C |- rt_3 : OK - -- Reftype_sub: C |- rt_1 <: rt_3 - -- Reftype_sub: C |- rt_2 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_1 -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index e57e5d90f..b5e28139f 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -98,7 +98,9 @@ rule Instr_ok/br_on_cast: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_sub: C |- rt_2 <: rt_1 + -- Reftype_ok: C |- rt_3 : OK + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- rt_2 <: rt rule Instr_ok/br_on_cast_fail: @@ -106,7 +108,9 @@ rule Instr_ok/br_on_cast_fail: -- if C.LABELS[l] = t* rt -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK - -- Reftype_sub: C |- rt_2 <: rt_1 + -- Reftype_ok: C |- rt_3 : OK + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt From 01eee4ba8c0836b213253f9a00aa5781025037b8 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 2 Feb 2026 21:57:06 -0800 Subject: [PATCH 4/4] line breaks --- specification/wasm-latest/2.3-validation.instructions.spectec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index b5e28139f..aa012b18f 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -99,6 +99,7 @@ rule Instr_ok/br_on_cast: -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK -- Reftype_ok: C |- rt_3 : OK + ---- -- Reftype_sub: C |- rt_1 <: rt_3 -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- rt_2 <: rt @@ -109,6 +110,7 @@ rule Instr_ok/br_on_cast_fail: -- Reftype_ok: C |- rt_1 : OK -- Reftype_ok: C |- rt_2 : OK -- Reftype_ok: C |- rt_3 : OK + ---- -- Reftype_sub: C |- rt_1 <: rt_3 -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt