diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 74bbcc634..7a93f1d59 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -265,6 +265,8 @@ while the latter performs a downcast and :ref:`traps ` if the operand's ty .. _syntax-struct.new: .. _syntax-struct.new_default: +.. _syntax-struct.new_desc: +.. _syntax-struct.new_default_desc: .. _syntax-struct.get: .. _syntax-struct.get_s: .. _syntax-struct.get_u: @@ -301,7 +303,8 @@ Instructions in this group are concerned with creating and accessing :ref:`refer $${syntax: {instr/struct instr/array instr/i31 instr/extern}} -The instructions ${:STRUCT.NEW} and ${:STRUCT.NEW_DEFAULT} allocate a new :ref:`structure `, initializing them either with operands or with default values. +The instructions ${:STRUCT.NEW}, ${:STRUCT.NEW_DEFAULT} allocate a new :ref:`structure `, initializing them either with operands or with default values. +The instructions ${:STRUCT.NEW_DESC} and ${:STRUCT.NEW_DEFAULT_DESC} do the same, but additionally take the :ref:`descriptor ` operand necessary to allocate types with descriptors. The remaining instructions on structs access individual fields, allowing for different sign extension modes in the case of :ref:`packed ` storage types. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1a81d68af..35413fb95 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -342,8 +342,10 @@ .. |rolldt| mathdef:: \xref{valid/conventions}{aux-roll-deftype}{\F{roll}} .. |unrolldt| mathdef:: \xref{valid/conventions}{aux-unroll-deftype}{\F{unroll}} .. |expanddt| mathdef:: \xref{valid/conventions}{aux-expand-deftype}{\F{expand}} +.. |expanddttodesctype| mathdef:: \xref{valid/conventions}{aux-expand-deftype-to-desctype}{\F{expand}} .. |approxexpanddt| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-deftype}{\approx}} .. |approxexpandyy| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-typeuse}{\approx}} +.. |approxexpanddttodesctype| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-deftype-to-desctype}{\approx}} .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}} @@ -551,6 +553,8 @@ .. |STRUCTNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new}} .. |STRUCTNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default}} +.. |STRUCTNEWDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_desc}} +.. |STRUCTNEWDEFAULTDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default\_desc}} .. |STRUCTGET| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get}} .. |STRUCTGETS| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_s}} .. |STRUCTGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_u}} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 7164062ed..8ec31b468 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -138,6 +138,7 @@ Conventions .. _aux-roll-deftype: .. _aux-unroll-deftype: .. _aux-expand-deftype: +.. _aux-expand-deftype-to-desctype: .. _aux-expand-typeuse: Rolling and Unrolling @@ -169,6 +170,10 @@ $${rule: Expand {Expand_use/*}} $${relation-ignore: Expand Expand_use} $${definition-ignore: expanddt} +We use the same notation to denote the expansion of a :ref:`defined type ` or :ref:`type use ` to a :ref:`desctype ` as well. + +$${rule: ExpandDesc} + .. index:: ! instruction type, value type, result type, instruction, local, local index pair: abstract syntax; instruction type diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 6013d4de2..c49fc727a 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -854,6 +854,26 @@ $${rule-prose: Instr_ok/struct.new_default} $${rule: Instr_ok/struct.new_default} +.. _valid-struct.new_desc: + +:math:`\STRUCTNEWDESC~x` +........................ + +$${rule-prose: Instr_ok/struct.new_desc} + +$${rule: Instr_ok/struct.new_desc} + + +.. _valid-struct.new_default_desc: + +:math:`\STRUCTNEWDEFAULTDESC~x` +............................... + +$${rule-prose: Instr_ok/struct.new_default_desc} + +$${rule: Instr_ok/struct.new_default_desc} + + .. _valid-struct.get: .. _valid-struct.get_u: .. _valid-struct.get_s: @@ -1421,6 +1441,7 @@ $${rule: {Instr_const/const Instr_const/vconst Instr_const/binop} {Instr_const/ref.null Instr_const/ref.i31 Instr_const/ref.func} {Instr_const/struct.new Instr_const/struct.new_default} + {Instr_const/struct.new_desc Instr_const/struct.new_default_desc} {Instr_const/array.new Instr_const/array.new_default Instr_const/array.new_fixed} {Instr_const/any.convert_extern Instr_const/extern.convert_any} {Instr_const/global.get} diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index a4b2249e7..25990998e 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -474,7 +474,7 @@ def $rollrt(typeidx, rectype) : rectype hint(show $roll_(%, %)) hint(macro "r def $unrollrt(rectype) : rectype hint(show $unroll(%)) hint(macro "unrollrt") def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%)*#((%))) hint(macro "rolldt") def $unrolldt(deftype) : subtype hint(show $unroll(%)) hint(macro "unrolldt") -def $expanddt_to_desctype(deftype) : desctype hint(show $expand_desc(%)) +def $expanddt_to_desctype(deftype) : desctype hint(show $expand_desc(%)) hint(macro "expanddttodesctype") def $expanddt(deftype) : comptype hint(show $expand(%)) hint(macro "expanddt") def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i` of %1 is %2") ;; TODO(3, ?): avoid hardcoding reST + +rule ExpandDesc: deftype ~~ desctype -- if $expanddt_to_desctype(deftype) = desctype + ;; Type definitions diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index aa012b18f..2e042e76f 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -251,11 +251,20 @@ rule Instr_ok/i31.get: rule Instr_ok/struct.new: C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_IDX x)) - -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* + -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* rule Instr_ok/struct.new_default: C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_IDX x)) - -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* + -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* + -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* + +rule Instr_ok/struct.new_desc: + C |- STRUCT.NEW_DESC x : $unpack(zt)* (REF NULL (EXACT (_IDX y))) -> (REF (EXACT (_IDX x))) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) + +rule Instr_ok/struct.new_default_desc: + C |- STRUCT.NEW_DEFAULT_DESC x : (REF NULL (EXACT (_IDX y))) -> (REF (EXACT (_IDX x))) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type") @@ -673,6 +682,12 @@ rule Instr_const/struct.new: rule Instr_const/struct.new_default: C |- (STRUCT.NEW_DEFAULT x) CONST +rule Instr_const/struct.new_desc: + C |- (STRUCT.NEW_DESC x) CONST + +rule Instr_const/struct.new_default_desc: + C |- (STRUCT.NEW_DEFAULT_DESC x) CONST + rule Instr_const/array.new: C |- (ARRAY.NEW x) CONST diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 4c88ce6b0..9b966ce22 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -32,7 +32,7 @@ let flatten_rec def = let is_validation_helper_relation def = match def.it with - | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" + | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" || id.it = "ExpandDesc" | _ -> false (* NOTE: Assume validation relation is `|-` *) let is_validation_relation def =