Syntax and validation for descriptor casts

document/core/syntax/instructions.rst

@@ -61,6 +61,8 @@ If missing, the operands must be of :ref:`numeric <syntax-numtype>` or :ref:`vec
 .. _syntax-br_on_non_null:
 .. _syntax-br_on_cast:
 .. _syntax-br_on_cast_fail:
+.. _syntax-br_on_cast_desc_eq:
+.. _syntax-br_on_cast_desc_eq_fail:
 .. _syntax-call:
 .. _syntax-call_ref:
 .. _syntax-call_indirect:
@@ -113,6 +115,7 @@ ${:BR_IF} performs a conditional branch,
 and ${:BR_TABLE} performs an indirect branch through an operand indexing into the label list that is an immediate to the instruction, or to a default target if the operand is out of bounds.
 The ${:BR_ON_NULL} and ${:BR_ON_NON_NULL} instructions check whether a reference operand is :ref:`null <syntax-nullref>` and branch if that is the case or not the case, respectively.
 Similarly, ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} attempt a downcast on a reference operand and branch if that succeeds, or fails, respectively.
+The ${:BR_ON_CAST_DESC_EQ} and ${:BR_ON_CAST_DESC_EQ_FAIL} instructions perform a similar cast check but compare the operand's descriptor against a given descriptor value.
 
 The ${:RETURN} instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function.
 Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered.
@@ -234,6 +237,7 @@ The ${:DATA.DROP} instruction prevents further use of a passive data segment. Th
 .. _syntax-ref.get_desc:
 .. _syntax-ref.test:
 .. _syntax-ref.cast:
+.. _syntax-ref.cast_desc_eq:
 .. _syntax-instr-ref:
 
 Reference Instructions
@@ -255,10 +259,12 @@ The instruction ${:REF.GET_DESC} gets the :ref:`descriptor <syntax-desctype>` of
 The instructions ${:REF.TEST} and ${:REF.CAST} test the :ref:`dynamic type <type-inst>` of a reference operand.
 The former merely returns the result of the test,
 while the latter performs a downcast and :ref:`traps <trap>` if the operand's type does not match.
+The instruction ${:REF.CAST_DESC_EQ} performs a similar downcast but checks the operand's descriptor against a given descriptor value instead of checking its dynamic type.
 
 .. note::
    The ${:BR_ON_NULL} and ${:BR_ON_NON_NULL} instructions provide versions of ${:REF.AS_NON_NULL} that branch depending on the success or failure of a null test instead of trapping.
-   Similarly, the ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} instructions provides versions of ${:REF.CAST} that branch depending on the success of the downcast instead of trapping.
+   Similarly, the ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} instructions provides versions of ${:REF.CAST} that branch depending on the success of the downcast instead of trapping,
+   and ${:BR_ON_CAST_DESC_EQ} and ${:BR_ON_CAST_DESC_EQ_FAIL} provide branching versions of ${:REF.CAST_DESC_EQ}.
 
    An additional instruction operating on function references is the :ref:`control instruction <syntax-instr-control>` ${:CALL_REF}.
 

document/core/util/macros.def

@@ -493,6 +493,8 @@
 .. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}}
 .. |BRONCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast}}
 .. |BRONCASTFAIL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_fail}}
+.. |BRONCASTDESCEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_desc\_eq}}
+.. |BRONCASTDESCEQFAIL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_desc\_eq\_fail}}
 
 .. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
 .. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
@@ -552,6 +554,7 @@
 .. |REFGETDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref.get\_desc}}
 .. |REFTEST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}test}}
 .. |REFCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}cast}}
+.. |REFCASTDESCEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}cast\_desc\_eq}}
 
 .. |STRUCTNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new}}
 .. |STRUCTNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default}}

document/core/valid/instructions.rst

@@ -252,6 +252,32 @@ $${rule: Instr_ok/br_on_cast_fail}
    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_desc_eq:
+
+:math:`\BRONCASTDESCEQ~l~\X{rt}_1~\X{rt}_2`
+...........................................
+
+$${rule-prose: Instr_ok/br_on_cast_desc_eq}
+
+$${rule: Instr_ok/br_on_cast_desc_eq}
+
+.. 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_desc_eq_fail:
+
+:math:`\BRONCASTDESCEQFAIL~l~\X{rt}_1~\X{rt}_2`
+................................................
+
+$${rule-prose: Instr_ok/br_on_cast_desc_eq_fail}
+
+$${rule: Instr_ok/br_on_cast_desc_eq_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:
 
 :math:`\CALL~x`
@@ -839,6 +865,16 @@ $${rule: Instr_ok/ref.cast}
    The liberty to pick a supertype ${:rt'} allows typing the instruction with the least precise super type of ${:rt} as input, that is, the top type in the corresponding heap subtyping hierarchy.
 
 
+.. _valid-ref.cast_desc_eq:
+
+:math:`\REFCASTDESCEQ~\X{rt}`
+.............................
+
+$${rule-prose: Instr_ok/ref.cast_desc_eq}
+
+$${rule: Instr_ok/ref.cast_desc_eq}
+
+
 .. index:: aggregate reference
 
 Aggregate Reference Instructions

specification/wasm-latest/1.3-syntax.instructions.spectec

@@ -234,6 +234,8 @@ syntax instr/br hint(desc "branch instruction") = ...
   | BR_ON_NON_NULL labelidx
   | BR_ON_CAST labelidx reftype reftype
   | BR_ON_CAST_FAIL labelidx reftype reftype
+  | BR_ON_CAST_DESC_EQ labelidx reftype reftype
+  | BR_ON_CAST_DESC_EQ_FAIL labelidx reftype reftype
   | ...
 
 syntax instr/call hint(desc "function instruction") = ...
@@ -309,6 +311,7 @@ syntax instr/ref hint(desc "reference instruction") = ...
   | REF.GET_DESC typeidx
   | REF.TEST reftype
   | REF.CAST reftype
+  | REF.CAST_DESC_EQ reftype
   | ...
 
 syntax instr/func hint(desc "function reference instruction") = ...
@@ -448,6 +451,10 @@ def $free_instr(BR_ON_CAST labelidx reftype_1 reftype_2) =
   $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)
 def $free_instr(BR_ON_CAST_FAIL labelidx reftype_1 reftype_2) =
   $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)
+def $free_instr(BR_ON_CAST_DESC_EQ labelidx reftype_1 reftype_2) =
+  $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)
+def $free_instr(BR_ON_CAST_DESC_EQ_FAIL labelidx reftype_1 reftype_2) =
+  $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)
 
 def $free_instr(CALL funcidx) = $free_funcidx(funcidx)
 def $free_instr(CALL_REF typeuse) = $free_typeuse(typeuse)
@@ -501,6 +508,7 @@ def $free_instr(REF.AS_NON_NULL) = {}
 def $free_instr(REF.EQ) = {}
 def $free_instr(REF.TEST reftype) = $free_reftype(reftype)
 def $free_instr(REF.CAST reftype) = $free_reftype(reftype)
+def $free_instr(REF.CAST_DESC_EQ reftype) = $free_reftype(reftype)
 def $free_instr(REF.FUNC funcidx) = $free_funcidx(funcidx)
 def $free_instr(REF.I31) = {}
 

specification/wasm-latest/2.3-validation.instructions.spectec

@@ -115,6 +115,28 @@ rule Instr_ok/br_on_cast_fail:
   -- Reftype_sub: C |- rt_2 <: rt_3
   -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt
 
+rule Instr_ok/br_on_cast_desc_eq:
+  C |- BR_ON_CAST_DESC_EQ l rt_1 (REF null? (_HT exact? _IDX x)) : t* rt_1 (REF NULL (_HT exact? _IDX y)) -> t* ($diffrt(rt_1, (REF null? (_HT exact? _IDX x))))
+  -- if C.LABELS[l] = t* rt
+  -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct
+  -- Reftype_ok: C |- rt_1 : OK
+  -- Reftype_ok: C |- rt_3 : OK
+  ----
+  -- Reftype_sub: C |- rt_1 <: rt_3
+  -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt_3
+  -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt
+
+rule Instr_ok/br_on_cast_desc_eq_fail:
+  C |- BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF null? (_HT exact? _IDX x)) : t* rt_1 (REF NULL (_HT exact? _IDX y)) -> t* (REF null? (_HT exact? _IDX x))
+  -- if C.LABELS[l] = t* rt
+  -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct
+  -- Reftype_ok: C |- rt_1 : OK
+  -- Reftype_ok: C |- rt_3 : OK
+  ----
+  -- Reftype_sub: C |- rt_1 <: rt_3
+  -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt_3
+  -- Reftype_sub: C |- $diffrt(rt_1, (REF null? (_HT exact? _IDX x))) <: rt
+
 
 ;; Function instructions
 
@@ -246,6 +268,12 @@ rule Instr_ok/ref.cast:
   -- Reftype_ok: C |- rt' : OK
   -- Reftype_sub: C |- rt <: rt'
 
+rule Instr_ok/ref.cast_desc_eq:
+  C |- REF.CAST_DESC_EQ (REF null? (_HT exact? _IDX x)) : (REF NULL ht) (REF NULL (_HT exact? _IDX y)) -> (REF null? (_HT exact? _IDX x))
+  -- Heaptype_ok: C |- ht : OK
+  -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct
+  -- Heaptype_sub: C |- (_HT exact? _IDX x) <: ht
+
 
 ;; Scalar reference instructions