From d793168cf5a3aa217dde9a22059e87e9f3c49636 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 7 Nov 2024 10:24:36 +0100 Subject: [PATCH 1/2] Add back lost text rule --- document/core/syntax/types.rst | 4 ++-- document/core/text/modules.rst | 11 +++++++++++ document/core/util/macros.def | 2 +- document/core/valid/instructions.rst | 4 ++-- 4 files changed, 16 insertions(+), 5 deletions(-) diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 2da8a265fa..450db2bae6 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -384,8 +384,8 @@ The *minimum* of two address types is defined as the address type whose :ref:`bi .. math:: \begin{array}{llll} - \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\ - \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\ + \addrtypemin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\ + \addrtypemin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\ \end{array} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 73bb7182b3..0ce3583bd2 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -304,6 +304,17 @@ A table's initialization :ref:`expression ` can be omitted, in which An :ref:`element segment ` can be given inline with a table definition, in which case its offset is :math:`0` and the :ref:`limits ` of the :ref:`table type ` are inferred from the length of the given segment: +.. math:: + \begin{array}{llclll} + \production{module field} & + \text{(}~\text{table}~~\Tid^?~~\Taddrtype^?~~\Treftype~~\text{(}~\text{elem}~~\expr^n{:}\Tvec(\Telemexpr)~\text{)}~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{table}~~\Tid'~~\Taddrtype^?~~n~~n~~\Treftype~\text{)} \\ & \qquad + \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\Telemexpr)~\text{)} + \\ & \qquad\qquad + (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad + \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}) \\ + \end{array} + .. math:: \begin{array}{llclll} \production{module field} & diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 8aae38810b..2a45188b15 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -301,6 +301,7 @@ .. Types, meta functions +.. |addrtypemin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{min}} .. |reftypediff| mathdef:: \xref{valid/conventions}{aux-reftypediff}{\setminus} .. |rollrt| mathdef:: \xref{valid/conventions}{aux-roll-rectype}{\F{roll}} @@ -311,7 +312,6 @@ .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}} -.. |atmin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{atmin}} .. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 602540d978..8eeaeb094c 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1510,7 +1510,7 @@ Table Instructions \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLECOPY~x~y : [\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to [] + C \vdashinstr \TABLECOPY~x~y : [\X{at}_1~\X{at}_2~\addrtypemin(\X{at}_1, \X{at}_2)] \to [] } @@ -1898,7 +1898,7 @@ Memory Instructions \qquad C.\CMEMS[y] = \X{at}_y~\limits_y }{ - C \vdashinstr \MEMORYCOPY~x~y : [\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to [] + C \vdashinstr \MEMORYCOPY~x~y : [\X{at}_x~\X{at}_y~\addrtypemin(\X{at}_x, \X{at}_y)] \to [] } From d8b7fcd2b910dddf7681ed61a28332906823f6f3 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 7 Nov 2024 10:35:37 +0100 Subject: [PATCH 2/2] [interpreter] Remove unnecessary type parameter from limits --- interpreter/syntax/types.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index f6a7fe2455..6deb708d7f 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -8,7 +8,7 @@ type null = NoNull | Null type mut = Cons | Var type init = Set | Unset type final = NoFinal | Final -type 'a limits = {min : 'a; max : 'a option} +type limits = {min : int64; max : int64 option} type var = StatX of type_idx | RecX of int32 @@ -45,8 +45,8 @@ and sub_type = SubT of final * heap_type list * str_type and rec_type = RecT of sub_type list and def_type = DefT of rec_type * int32 -type table_type = TableT of addr_type * Int64.t limits * ref_type -type memory_type = MemoryT of addr_type * Int64.t limits +type table_type = TableT of addr_type * limits * ref_type +type memory_type = MemoryT of addr_type * limits type global_type = GlobalT of mut * val_type type tag_type = TagT of def_type type local_type = LocalT of init * val_type