diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 7a93f1d59..516e02a67 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -231,6 +231,7 @@ The ${:DATA.DROP} instruction prevents further use of a passive data segment. Th .. _syntax-ref.is_null: .. _syntax-ref.as_non_null: .. _syntax-ref.eq: +.. _syntax-ref.get_desc: .. _syntax-ref.test: .. _syntax-ref.cast: .. _syntax-instr-ref: @@ -247,7 +248,9 @@ The ${:REF.NULL} and ${:REF.FUNC} instructions produce a :ref:`null ` to a non-null one, and :ref:`traps ` if it encounters null. -The ${:REF.EQ} compares two references. +The instruction ${:REF.EQ} compares two references. + +The instruction ${:REF.GET_DESC} gets the :ref:`descriptor ` of an allocated value. The instructions ${:REF.TEST} and ${:REF.CAST} test the :ref:`dynamic type ` of a reference operand. The former merely returns the result of the test, diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 8676c91fe..36e6965dc 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -551,6 +551,7 @@ .. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} .. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}} .. |REFEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}eq}} +.. |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}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index c49fc727a..1da2143a7 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -803,6 +803,16 @@ $${rule-prose: Instr_ok/ref.eq} $${rule: Instr_ok/ref.eq} +.. _valid-ref.get_desc: + +:math:`\REFGETDESC~x` +..................... + +$${rule-prose: Instr_ok/ref.get_desc} + +$${rule: Instr_ok/ref.get_desc Instr_ok/ref.get_desc-exact} + + .. _valid-ref.test: :math:`\REFTEST~\X{rt}` diff --git a/specification/wasm-latest/1.3-syntax.instructions.spectec b/specification/wasm-latest/1.3-syntax.instructions.spectec index 6228dce91..3a586db75 100644 --- a/specification/wasm-latest/1.3-syntax.instructions.spectec +++ b/specification/wasm-latest/1.3-syntax.instructions.spectec @@ -306,6 +306,7 @@ syntax instr/ref hint(desc "reference instruction") = ... | REF.IS_NULL | REF.AS_NON_NULL | REF.EQ + | REF.GET_DESC typeidx | REF.TEST reftype | REF.CAST reftype | ... diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index d9692abf0..da7d20e5f 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -231,6 +231,14 @@ rule Instr_ok/ref.as_non_null: rule Instr_ok/ref.eq: C |- REF.EQ : (REF NULL EQ) (REF NULL EQ) -> I32 +rule Instr_ok/ref.get_desc: + C |- REF.GET_DESC x : (REF NULL (_IDX x)) -> (REF (_IDX y)) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + +rule Instr_ok/ref.get_desc-exact: + C |- REF.GET_DESC x : (REF NULL (EXACT (_IDX x))) -> (REF (EXACT (_IDX y))) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + rule Instr_ok/ref.test: C |- REF.TEST rt : rt' -> I32 -- Reftype_ok: C |- rt : OK