Spectec and rst for custom descriptors execution

document/core/exec/instructions.rst

@@ -125,6 +125,20 @@ $${rule-prose: Step_read/br_on_cast_fail}
 $${rule: {Step_read/br_on_cast_fail-*}}
 
 
+.. _exec-br_on_cast_desc_eq:
+
+$${rule-prose: Step_read/br_on_cast_desc_eq}
+
+$${rule: {Step_read/br_on_cast_desc_eq-*}}
+
+
+.. _exec-br_on_cast_desc_eq_fail:
+
+$${rule-prose: Step_read/br_on_cast_desc_eq_fail}
+
+$${rule: {Step_read/br_on_cast_desc_eq_fail-*}}
+
+
 .. _exec-return:
 
 $${rule-prose: Step_pure/return}
@@ -730,6 +744,20 @@ $${rule-prose: Step_read/ref.cast}
 $${rule: {Step_read/ref.cast-*}}
 
 
+.. _exec-ref.get_desc:
+
+$${rule-prose: Step_read/ref.get_desc}
+
+$${rule: {Step_read/ref.get_desc-*}}
+
+
+.. _exec-ref.cast_desc_eq:
+
+$${rule-prose: Step_read/ref.cast_desc_eq}
+
+$${rule: {Step_read/ref.cast_desc_eq-*}}
+
+
 .. _exec-ref.i31:
 
 $${rule-prose: Step_pure/ref.i31}
@@ -758,6 +786,20 @@ $${rule-prose: Step_read/struct.new_default}
 $${rule: {Step_read/struct.new_default}}
 
 
+.. _exec-struct.new_desc:
+
+$${rule-prose: Step/struct.new_desc}
+
+$${rule: {Step/struct.new_desc-*}}
+
+
+.. _exec-struct.new_default_desc:
+
+$${rule-prose: Step_read/struct.new_default_desc}
+
+$${rule: {Step_read/struct.new_default_desc}}
+
+
 .. _exec-struct.get:
 .. _exec-struct.get_sx:
 

document/core/exec/runtime.rst

@@ -432,6 +432,7 @@ Aggregate Instances
 A *structure instance* is the runtime representation of a heap object allocated from a :ref:`structure type <syntax-structtype>`.
 Likewise, an *array instance* is the runtime representation of a heap object allocated from an :ref:`array type <syntax-arraytype>`.
 Both record their respective :ref:`defined type <syntax-deftype>` and hold a list of the values of their *fields*.
+A structure instance additionally holds an optional :ref:`structure address <syntax-structaddr>` for its :ref:`descriptor <syntax-descriptor>`.
 
 $${syntax: {structinst arrayinst fieldval packval}}
 

document/core/util/macros.def

@@ -1441,6 +1441,7 @@
 
 .. |SITYPE| mathdef:: \xref{exec/runtime}{syntax-structinst}{\K{type}}
 .. |SIFIELDS| mathdef:: \xref{exec/runtime}{syntax-structinst}{\K{fields}}
+.. |SIDESC| mathdef:: \xref{exec/runtime}{syntax-structinst}{\K{desc}}
 
 .. |AITYPE| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\K{type}}
 .. |AIFIELDS| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\K{fields}}
@@ -1480,6 +1481,7 @@
 .. |ZDBYTES| mathdef:: \DIBYTES
 .. |ZSSTRUCTS| mathdef:: \ZSTRUCTS
 .. |ZSFIELDS| mathdef:: \SIFIELDS
+.. |ZSDESC| mathdef:: \SIDESC
 .. |ZAARRAYS| mathdef:: \ZARRAYS
 .. |ZAFIELDS| mathdef:: \AIFIELDS
 

specification/wasm-latest/4.0-execution.configurations.spectec

@@ -89,7 +89,7 @@ syntax fieldval hint(desc "field value") =
   | val | packval
 
 syntax structinst hint(desc "structure instance") hint(macro "%" "SI%") =
-  { TYPE deftype, FIELDS fieldval* }
+  { TYPE deftype, FIELDS fieldval*, DESC structaddr? }
 
 syntax arrayinst hint(desc "array instance") hint(macro "%" "AI%") =
   { TYPE deftype, FIELDS fieldval* }

specification/wasm-latest/4.1-execution.values.spectec

@@ -38,18 +38,16 @@ rule Ref_ok/null:
 rule Ref_ok/i31:
   s |- REF.I31_NUM i : REF I31
 
-;; TODO(tlively): Use EXACT in Ref_ok/struct, Ref_ok/array, and Ref_ok/func so
-;; that Ref_ok/sub can derive exact reference types for casts.
 rule Ref_ok/struct:
-  s |- REF.STRUCT_ADDR a : REF (_HT dt)
+  s |- REF.STRUCT_ADDR a : REF (_HT EXACT dt)
   -- if s.STRUCTS[a].TYPE = dt
 
 rule Ref_ok/array:
-  s |- REF.ARRAY_ADDR a : REF (_HT dt)
+  s |- REF.ARRAY_ADDR a : REF (_HT EXACT dt)
   -- if s.ARRAYS[a].TYPE = dt
 
 rule Ref_ok/func:
-  s |- REF.FUNC_ADDR a : REF (_HT dt)
+  s |- REF.FUNC_ADDR a : REF (_HT EXACT dt)
   -- if s.FUNCS[a].TYPE = dt
 
 rule Ref_ok/exn:

specification/wasm-latest/4.3-execution.instructions.spectec

@@ -164,6 +164,48 @@ rule Step_read/br_on_cast_fail-fail:
   -- otherwise
 
 
+rule Step_read/br_on_cast_desc_eq-null:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ l rt_1 (REF null? ht))  ~>  TRAP
+  -- if ref_2 = REF.NULL_ADDR
+
+rule Step_read/br_on_cast_desc_eq-succeed-null:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ l rt_1 (REF NULL ht))  ~>  ref_1 (BR l)
+  -- otherwise
+  -- if ref_1 = REF.NULL_ADDR
+
+rule Step_read/br_on_cast_desc_eq-succeed-addr:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ l rt_1 (REF null? ht))  ~>  ref_1 (BR l)
+  -- otherwise
+  -- if ref_1 = REF.STRUCT_ADDR a
+  -- if $structinst(z)[a].DESC = a'
+  -- if ref_2 = REF.STRUCT_ADDR a'
+
+rule Step_read/br_on_cast_desc_eq-fail:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ l rt_1 (REF null? ht))  ~>  ref_1
+  -- otherwise
+
+
+rule Step_read/br_on_cast_desc_eq_fail-null:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF null? ht))  ~>  TRAP
+  -- if ref_2 = REF.NULL_ADDR
+
+rule Step_read/br_on_cast_desc_eq_fail-succeed-null:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF NULL ht))  ~>  ref_1
+  -- otherwise
+  -- if ref_1 = REF.NULL_ADDR
+
+rule Step_read/br_on_cast_desc_eq_fail-succeed-addr:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF null? ht))  ~>  ref_1
+  -- otherwise
+  -- if ref_1 = REF.STRUCT_ADDR a
+  -- if $structinst(z)[a].DESC = a'
+  -- if ref_2 = REF.STRUCT_ADDR a'
+
+rule Step_read/br_on_cast_desc_eq_fail-fail:
+  z; ref_1 ref_2 (BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF null? ht))  ~>  ref_1 (BR l)
+  -- otherwise
+
+
 ;; Function instructions
 
 rule Step_read/call:
@@ -693,6 +735,35 @@ rule Step_read/ref.cast-fail:
   -- otherwise
 
 
+rule Step_read/ref.get_desc-null:
+  z; (REF.NULL_ADDR) (REF.GET_DESC x)  ~>  TRAP
+
+rule Step_read/ref.get_desc-struct:
+  z; (REF.STRUCT_ADDR a) (REF.GET_DESC x)  ~>  (REF.STRUCT_ADDR a')
+  -- if $structinst(z)[a].DESC = a'
+
+
+rule Step_read/ref.cast_desc_eq-null:
+  z; ref_1 ref_2 (REF.CAST_DESC_EQ (REF null? ht))  ~>  TRAP
+  -- if ref_2 = REF.NULL_ADDR
+
+rule Step_read/ref.cast_desc_eq-succeed-null:
+  z; ref_1 ref_2 (REF.CAST_DESC_EQ (REF NULL ht))  ~>  ref_1
+  -- otherwise
+  -- if ref_1 = REF.NULL_ADDR
+
+rule Step_read/ref.cast_desc_eq-succeed-addr:
+  z; ref_1 ref_2 (REF.CAST_DESC_EQ (REF null? ht))  ~>  ref_1
+  -- otherwise
+  -- if ref_1 = REF.STRUCT_ADDR a
+  -- if $structinst(z)[a].DESC = a'
+  -- if ref_2 = REF.STRUCT_ADDR a'
+
+rule Step_read/ref.cast_desc_eq-fail:
+  z; ref_1 ref_2 (REF.CAST_DESC_EQ (REF null? ht))  ~>  TRAP
+  -- otherwise
+
+
 ;; Scalar reference instructions
 
 rule Step_pure/i31.get-null:
@@ -708,13 +779,28 @@ rule Step/struct.new:
   z; val^n (STRUCT.NEW x)  ~>  $add_structinst(z, si); (REF.STRUCT_ADDR a)
   -- Expand: $type(z, x) ~~ STRUCT (mut? zt)^n
   -- if a = |$structinst(z)|
-  -- if si = {TYPE $type(z, x), FIELDS ($packfield_(zt, val))^n}
+  -- if si = {TYPE $type(z, x), FIELDS ($packfield_(zt, val))^n, DESC eps}
 
 rule Step_read/struct.new_default:
   z; (STRUCT.NEW_DEFAULT x)  ~>  val* (STRUCT.NEW x)
   -- Expand: $type(z, x) ~~ STRUCT (mut? zt)*
   -- (if $default_($unpack(zt)) = val)*
 
+rule Step/struct.new_desc-null:
+  z; val^n (REF.NULL_ADDR) (STRUCT.NEW_DESC x)  ~>  z; TRAP
+  -- Expand: $type(z, x) ~~ STRUCT (mut? zt)^n
+
+rule Step/struct.new_desc-struct:
+  z; val^n (REF.STRUCT_ADDR a') (STRUCT.NEW_DESC x)  ~>  $add_structinst(z, si); (REF.STRUCT_ADDR a)
+  -- Expand: $type(z, x) ~~ STRUCT (mut? zt)^n
+  -- if a = |$structinst(z)|
+  -- if si = {TYPE $type(z, x), FIELDS ($packfield_(zt, val))^n, DESC a'}
+
+rule Step_read/struct.new_default_desc:
+  z; ref (STRUCT.NEW_DEFAULT_DESC x)  ~>  val* ref (STRUCT.NEW_DESC x)
+  -- Expand: $type(z, x) ~~ STRUCT (mut? zt)*
+  -- (if $default_($unpack(zt)) = val)*
+
 
 rule Step_read/struct.get-null:
   z; (REF.NULL_ADDR) (STRUCT.GET sx? x i)  ~>  TRAP