From 8d84e15bd861591da87fbd22f87cd85d06f8d0d1 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 13 Jun 2024 15:23:52 +0200 Subject: [PATCH] Convert binary modules --- document/core/appendix/changes.rst | 2 +- document/core/binary/modules.rst | 258 +++++---------------- document/core/binary/types.rst | 13 +- document/core/util/macros.def | 8 +- spectec/spec/wasm-3.0/A-binary.watsup | 31 +-- spectec/spec/wasm-3.0/C-conventions.watsup | 3 +- spectec/src/backend-latex/render.ml | 17 +- spectec/test-latex/TEST.md | 29 ++- spectec/test-splice/TEST.md | 2 + 9 files changed, 129 insertions(+), 234 deletions(-) diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index f7a73686aa..e60e6fd02d 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -99,7 +99,7 @@ Added instructions that modify ranges of memory or table entries. [#proposal-ref * New :ref:`passive ` form of :ref:`element segment ` -* New :ref:`data count section ` in binary format +* New :ref:`data count section ` in binary format * Active data and element segments boundaries are no longer checked at compile time but may trap instead diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 68cea1c8ec..eeef8a886d 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -30,26 +30,22 @@ except that :ref:`function definitions ` are split into two section .. _binary-localidx: .. _binary-labelidx: .. _binary-fieldidx: +.. _binary-externidx: .. _binary-index: Indices ~~~~~~~ -All :ref:`indices ` are encoded with their respective value. +All basic :ref:`indices ` are encoded with their respective value. -.. math:: - \begin{array}{llclll} - \production{type index} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{element index} & \Belemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{data index} & \Bdataidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ - \production{field index} & \Bfieldidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \end{array} +$${grammar: { + Btypeidx Bfuncidx Btableidx Bmemidx Bglobalidx Belemidx Bdataidx + Blocalidx Blabelidx +}} + +:ref:`External indices ` are encoded by a distiguishing byte followed by an encoding of their respective value. + +$${grammar: Bexternidx} .. index:: ! section @@ -62,28 +58,22 @@ Sections Each section consists of * a one-byte section *id*, -* the |U32| *size* of the contents, in bytes, +* the ${:u32} *length* of the contents, in bytes, * the actual *contents*, whose structure is dependent on the section id. Every section is optional; an omitted section is equivalent to the section being present with empty contents. -The following parameterized grammar rule defines the generic structure of a section with id :math:`N` and contents described by the grammar :math:`\B{B}`. +The following parameterized grammar rule defines the generic structure of a section with id ${:N} and contents described by the grammar ${grammar-case: X}. -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{section} & \Bsection_N(\B{B}) &::=& - N{:}\Bbyte~~\X{size}{:}\Bu32~~\X{cont}{:}\B{B} - &\Rightarrow& \X{cont} & (\iff \X{size} = ||\B{B}||) \\ &&|& - \epsilon &\Rightarrow& \epsilon - \end{array} +$${grammar: Bsection_} -For most sections, the contents :math:`\B{B}` encodes a :ref:`list `. -In these cases, the empty result :math:`\epsilon` is interpreted as the empty list. +For most sections, the contents ${grammar-case: X} encodes a :ref:`list `. +In these cases, the empty result ${:eps} is interpreted as the empty list. .. note:: Other than for unknown :ref:`custom sections `, - the :math:`\X{size}` is not required for decoding, but can be used to skip sections when navigating through a binary. - The module is malformed if the size does not match the length of the binary contents :math:`\B{B}`. + the ${:size} is not required for decoding, but can be used to skip sections when navigating through a binary. + The module is malformed if the size does not match the length of the binary contents ${grammar-case: X}. The following section ids are used: @@ -102,7 +92,7 @@ Id Section 9 :ref:`element section ` 10 :ref:`code section ` 11 :ref:`data section ` -12 :ref:`data count section ` +12 :ref:`data count section ` == =============================================== .. note:: @@ -121,13 +111,7 @@ Custom Section They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. Their contents consist of a :ref:`name ` further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use. -.. math:: - \begin{array}{llclll} - \production{custom section} & \Bcustomsec &::=& - \Bsection_0(\Bcustom) \\ - \production{custom data} & \Bcustom &::=& - \Bname~~\Bbyte^\ast \\ - \end{array} +$${grammar: {Bcustomsec Bcustom}} .. note:: If an implementation interprets the data of a custom section, then errors in that data, or the placement of the section, must not invalidate the module. @@ -136,20 +120,16 @@ Their contents consist of a :ref:`name ` further identifying the cu .. index:: ! type section, type definition, recursive type pair: binary format; type section pair: section; type -.. _binary-typedef: +.. _binary-type: .. _binary-typesec: Type Section ~~~~~~~~~~~~ The *type section* has the id 1. -It decodes into a list of :ref:`recursive types ` that represent the |MTYPES| component of a :ref:`module `. +It decodes into the list of :ref:`recursive types ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{type section} & \Btypesec &::=& - \X{rt}^\ast{:\,}\Bsection_1(\Blist(\Brectype)) &\Rightarrow& \X{rt}^\ast \\ - \end{array} +$${grammar: {Btypesec Btype}} .. index:: ! import section, import, name, function type, table type, memory type, global type @@ -163,21 +143,9 @@ Import Section ~~~~~~~~~~~~~~ The *import section* has the id 2. -It decodes into a list of :ref:`imports ` that represent the |MIMPORTS| component of a :ref:`module `. +It decodes into the list of :ref:`imports ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{import section} & \Bimportsec &::=& - \X{im}^\ast{:}\Bsection_2(\Blist(\Bimport)) &\Rightarrow& \X{im}^\ast \\ - \production{import} & \Bimport &::=& - \X{mod}{:}\Bname~~\X{nm}{:}\Bname~~d{:}\Bimportdesc - &\Rightarrow& \{ \IMODULE~\X{mod}, \INAME~\X{nm}, \IDESC~d \} \\ - \production{import description} & \Bimportdesc &::=& - \hex{00}~~x{:}\Btypeidx &\Rightarrow& \IDFUNC~x \\ &&|& - \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& - \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|& - \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ - \end{array} +$${grammar: {Bimportsec Bimport}} .. index:: ! function section, function, type index, function type @@ -189,14 +157,10 @@ Function Section ~~~~~~~~~~~~~~~~ The *function section* has the id 3. -It decodes into a list of :ref:`type indices ` that represent the |FTYPE| fields of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. -The |FLOCALS| and |FBODY| fields of the respective functions are encoded separately in the :ref:`code section `. +It decodes into a list of :ref:`type indices ` that classify the :ref:`functions ` of a :ref:`module `. +The bodies of the respective functions are encoded separately in the :ref:`code section `. -.. math:: - \begin{array}{llclll} - \production{function section} & \Bfuncsec &::=& - x^\ast{:}\Bsection_3(\Blist(\Btypeidx)) &\Rightarrow& x^\ast \\ - \end{array} +$${grammar: {Bfuncsec}} .. index:: ! table section, table, table type @@ -209,22 +173,12 @@ Table Section ~~~~~~~~~~~~~ The *table section* has the id 4. -It decodes into a list of :ref:`tables ` that represent the |MTABLES| component of a :ref:`module `. +It decodes into the list of :ref:`tables ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{table section} & \Btablesec &::=& - \X{tab}^\ast{:}\Bsection_4(\Blist(\Btable)) &\Rightarrow& \X{tab}^\ast \\ - \production{table} & \Btable &::=& - \X{tt}{:}\Btabletype - &\Rightarrow& \{ \TTYPE~\X{tt}, \TINIT~(\REFNULL~\X{ht}) \} - \qquad \iff \X{tt} = \limits~(\REF~\NULL^?~\X{ht}) \\ &&|& - \hex{40}~~\hex{00}~~\X{tt}{:}\Btabletype~~e{:}\Bexpr - &\Rightarrow& \{ \TTYPE~\X{tt}, \TINIT~e \} \\ - \end{array} +$${grammar: {Btablesec Btable}} .. note:: - The encoding of a table type cannot start with byte :math:`\hex{40}`, + The encoding of a table type cannot start with byte ${:0x40}`, hence decoding is unambiguous. The zero byte following it is reserved for future extensions. @@ -239,15 +193,9 @@ Memory Section ~~~~~~~~~~~~~~ The *memory section* has the id 5. -It decodes into a list of :ref:`memories ` that represent the |MMEMS| component of a :ref:`module `. +It decodes into the list of :ref:`memories ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{memory section} & \Bmemsec &::=& - \X{mem}^\ast{:}\Bsection_5(\Blist(\Bmem)) &\Rightarrow& \X{mem}^\ast \\ - \production{memory} & \Bmem &::=& - \X{mt}{:}\Bmemtype &\Rightarrow& \{ \MTYPE~\X{mt} \} \\ - \end{array} +$${grammar: {Bmemsec Bmem}} .. index:: ! global section, global, global type, expression @@ -260,16 +208,9 @@ Global Section ~~~~~~~~~~~~~~ The *global section* has the id 6. -It decodes into a list of :ref:`globals ` that represent the |MGLOBALS| component of a :ref:`module `. +It decodes into the list of :ref:`globals ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{global section} & \Bglobalsec &::=& - \X{glob}^\ast{:}\Bsection_6(\Blist(\Bglobal)) &\Rightarrow& \X{glob}^\ast \\ - \production{global} & \Bglobal &::=& - \X{gt}{:}\Bglobaltype~~e{:}\Bexpr - &\Rightarrow& \{ \GTYPE~\X{gt}, \GINIT~e \} \\ - \end{array} +$${grammar: {Bglobalsec Bglobal}} .. index:: ! export section, export, name, index, function index, table index, memory index, global index @@ -283,21 +224,9 @@ Export Section ~~~~~~~~~~~~~~ The *export section* has the id 7. -It decodes into a list of :ref:`exports ` that represent the |MEXPORTS| component of a :ref:`module `. +It decodes into the list of :ref:`exports ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{export section} & \Bexportsec &::=& - \X{ex}^\ast{:}\Bsection_7(\Blist(\Bexport)) &\Rightarrow& \X{ex}^\ast \\ - \production{export} & \Bexport &::=& - \X{nm}{:}\Bname~~d{:}\Bexportdesc - &\Rightarrow& \{ \ENAME~\X{nm}, \EDESC~d \} \\ - \production{export description} & \Bexportdesc &::=& - \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \EDFUNC~x \\ &&|& - \hex{01}~~x{:}\Btableidx &\Rightarrow& \EDTABLE~x \\ &&|& - \hex{02}~~x{:}\Bmemidx &\Rightarrow& \EDMEM~x \\ &&|& - \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ - \end{array} +$${grammar: {Bexportsec Bexport}} .. index:: ! start section, start function, function index @@ -311,15 +240,9 @@ Start Section ~~~~~~~~~~~~~ The *start section* has the id 8. -It decodes into an optional :ref:`start function ` that represents the |MSTART| component of a :ref:`module `. +It decodes into the optional :ref:`start function ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{start section} & \Bstartsec &::=& - \X{st}^?{:}\Bsection_8(\Bstart) &\Rightarrow& \X{st}^? \\ - \production{start function} & \Bstart &::=& - x{:}\Bfuncidx &\Rightarrow& \{ \SFUNC~x \} \\ - \end{array} +$${grammar: {Bstartsec Bstart}} .. index:: ! element section, element, table index, expression, function index @@ -335,40 +258,9 @@ Element Section ~~~~~~~~~~~~~~~ The *element section* has the id 9. -It decodes into a list of :ref:`element segments ` that represent the |MELEMS| component of a :ref:`module `. +It decodes into the list of :ref:`element segments ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{element section} & \Belemsec &::=& - \X{seg}^\ast{:}\Bsection_9(\Blist(\Belem)) &\Rightarrow& \X{seg}^\ast \\ - \production{element segment} & \Belem &::=& - 0{:}\Bu32~~e{:}\Bexpr~~y^\ast{:}\Blist(\Bfuncidx) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~(\REF~\FUNC), \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& - 1{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Blist(\Bfuncidx) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|& - 2{:}\Bu32~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Blist(\Bfuncidx) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& - 3{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Blist(\Bfuncidx) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARE \} \\ &&|& - 4{:}\Bu32~~e{:}\Bexpr~~\X{el}^\ast{:}\Blist(\Bexpr) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& - 5{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Blist(\Bexpr) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|& - 6{:}\Bu32~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Breftype~~\X{el}^\ast{:}\Blist(\Bexpr) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& - 7{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Blist(\Bexpr) - &\Rightarrow& \\&&&\quad - \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARE \} \\ - \production{element kind} & \Belemkind &::=& - \hex{00} &\Rightarrow& (\REF~\FUNC) \\ - \end{array} +$${grammar: {Belemsec Belemkind Belem}} .. note:: The initial integer can be interpreted as a bitfield. @@ -392,13 +284,13 @@ Code Section ~~~~~~~~~~~~ The *code section* has the id 10. -It decodes into a list of *code* entries that are pairs of :ref:`value type ` lists and :ref:`expressions `. -They represent the |FLOCALS| and |FBODY| field of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. -The |FTYPE| fields of the respective functions are encoded separately in the :ref:`function section `. +It decodes into the list of *code* entries that are pairs of lists of :ref:`locals ` and :ref:`expressions `. +They represent the body of the :ref:`functions ` of a :ref:`module `. +The types of the respective functions are encoded separately in the :ref:`function section `. The encoding of each code entry consists of -* the |U32| *size* of the function code in bytes, +* the ${:u32} *length* of the function code in bytes, * the actual *function code*, which in turn consists of * the declaration of *locals*, @@ -406,33 +298,18 @@ The encoding of each code entry consists of Local declarations are compressed into a list whose entries consist of -* a |U32| *count*, +* a ${:u32} *count*, * a :ref:`value type `, denoting *count* locals of the same value type. -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{code section} & \Bcodesec &::=& - \X{code}^\ast{:}\Bsection_{10}(\Blist(\Bcode)) - &\Rightarrow& \X{code}^\ast \\ - \production{code} & \Bcode &::=& - \X{size}{:}\Bu32~~\X{code}{:}\Bfunc - &\Rightarrow& \X{code} & (\iff \X{size} = ||\Bfunc||) \\ - \production{function} & \Bfunc &::=& - (\local^\ast)^\ast{:}\Blist(\Blocals)~~e{:}\Bexpr - &\Rightarrow& \concat((\local^\ast)^\ast), e - & (\iff |\concat((\local^\ast)^\ast)| < 2^{32}) \\ - \production{locals} & \Blocals &::=& - n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& \{ \LTYPE~t \}^n \\ - \end{array} +$${grammar: {Bcodesec Bcode Bfunc Blocals}} -Here, :math:`\X{code}` ranges over pairs :math:`(\valtype^\ast, \expr)`. -The meta function :math:`\concat((\local^\ast)^\ast)` concatenates all sequences :math:`\local_i^\ast` in :math:`(\local^\ast)^\ast`. +Here, ${:code} ranges over pairs ${:(local*, expr)}. Any code for which the length of the resulting sequence is out of bounds of the maximum size of a :ref:`list ` is malformed. .. note:: - Like with :ref:`sections `, the code :math:`\X{size}` is not needed for decoding, but can be used to skip functions when navigating through a binary. + Like with :ref:`sections `, the code ${:size} is not needed for decoding, but can be used to skip functions when navigating through a binary. The module is malformed if a size does not match the length of the respective function code. @@ -448,52 +325,35 @@ Data Section ~~~~~~~~~~~~ The *data section* has the id 11. -It decodes into a list of :ref:`data segments ` that represent the |MDATAS| component of a :ref:`module `. +It decodes into the list of :ref:`data segments ` of a :ref:`module `. -.. math:: - \begin{array}{llclll} - \production{data section} & \Bdatasec &::=& - \X{seg}^\ast{:}\Bsection_{11}(\Blist(\Bdata)) &\Rightarrow& \X{seg}^\ast \\ - \production{data segment} & \Bdata &::=& - 0{:}\Bu32~~e{:}\Bexpr~~b^\ast{:}\Blist(\Bbyte) - &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DACTIVE~\{ \DMEM~0, \DOFFSET~e \} \} \\ &&|& - 1{:}\Bu32~~b^\ast{:}\Blist(\Bbyte) - &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DPASSIVE \} \\ &&|& - 2{:}\Bu32~~x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Blist(\Bbyte) - &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DACTIVE~\{ \DMEM~x, \DOFFSET~e \} \} \\ - \end{array} +$${grammar: {Bdatasec Bdata}} .. note:: The initial integer can be interpreted as a bitfield. Bit 0 indicates a passive segment, bit 1 indicates the presence of an explicit memory index for an active segment. - In the current version of WebAssembly, at most one memory may be defined or - imported in a single module, so all valid :ref:`active ` data - segments have a |DMEM| value of :math:`0`. - .. index:: ! data count section, data count, data segment pair: binary format; data count pair: section; data count -.. _binary-datacountsec: +.. _binary-datacntsec: +.. _binary-datacnt: Data Count Section ~~~~~~~~~~~~~~~~~~ The *data count section* has the id 12. -It decodes into an optional :ref:`u32 ` that represents the number of :ref:`data segments ` in the :ref:`data section `. If this count does not match the length of the data segment list, the module is malformed. +It decodes into an optional ${:u32} count that represents the number of :ref:`data segments ` in the :ref:`data section `. +If this count does not match the length of the data segment list, the module is malformed. -.. math:: - \begin{array}{llclll} - \production{data count section} & \Bdatacountsec &::=& - \X{n}^?{:}\Bsection_{12}(\Bu32) &\Rightarrow& \X{n}^? \\ - \end{array} +$${grammar: {Bdatacntsec Bdatacnt}} .. note:: The data count section is used to simplify single-pass validation. Since the - data section occurs after the code section, the :math:`\MEMORYINIT` and - :math:`\DATADROP` instructions would not be able to check whether the data + data section occurs after the code section, the ${:MEMORY.INIT} and + ${:DATA.DROP} instructions would not be able to check whether the data segment index is valid until the data section is read. The data count section occurs before the code section, so a single-pass validator can use this count instead of deferring validation. @@ -521,6 +381,8 @@ The lengths of lists produced by the (possibly empty) :ref:`function ` list. Furthermore, it must be present if any :ref:`data index ` occurs in the code section. +$${grammar: {Bmagic Bversion Bmodule}} + .. math:: \begin{array}{llcllll} \production{magic} & \Bmagic &::=& @@ -549,7 +411,7 @@ Furthermore, it must be present if any :ref:`data index ` occurs \Bcustomsec^\ast \\ &&& \elem^\ast{:\,}\Belemsec \\ &&& \Bcustomsec^\ast \\ &&& - m^?{:\,}\Bdatacountsec \\ &&& + m^?{:\,}\Bdatacntsec \\ &&& \Bcustomsec^\ast \\ &&& \X{code}^n{:\,}\Bcodesec \\ &&& \Bcustomsec^\ast \\ &&& diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index d71ee317c3..bf552bc0d5 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -1,6 +1,5 @@ .. index:: type pair: binary format; type -.. _binary-type: Types ----- @@ -181,3 +180,15 @@ Global Types :ref:`Global types ` are encoded by their :ref:`value type ` and a flag for their :ref:`mutability `. $${grammar: Bglobaltype} + + +.. index:: external type + pair: binary format; external type +.. _binary-externtype: + +External Types +~~~~~~~~~~~~~~ + +:ref:`External types ` are encoded by a distiguishing byte followed by an encoding of the respective form of type. + +$${grammar: Bexterntype} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 10f6fa5b48..497b0eaea0 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -824,6 +824,7 @@ .. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}} .. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}} .. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}} +.. |Bexterntype| mathdef:: \xref{binary/types}{binary-externtype}{\B{externtype}} .. Indices, non-terminals @@ -840,6 +841,8 @@ .. |Blabelidx| mathdef:: \xref{binary/modules}{binary-labelidx}{\B{labelidx}} .. |Bfieldidx| mathdef:: \xref{binary/modules}{binary-fieldidx}{\B{fieldidx}} +.. |Bexternidx| mathdef:: \xref{binary/modules}{binary-externidx}{\B{externidx}} + .. Modules, non-terminals @@ -860,10 +863,10 @@ .. |Belemsec| mathdef:: \xref{binary/modules}{binary-elemsec}{\B{elemsec}} .. |Bdatasec| mathdef:: \xref{binary/modules}{binary-datasec}{\B{datasec}} .. |Bstartsec| mathdef:: \xref{binary/modules}{binary-startsec}{\B{startsec}} -.. |Bdatacountsec| mathdef:: \xref{binary/modules}{binary-datacountsec}{\B{datacountsec}} +.. |Bdatacntsec| mathdef:: \xref{binary/modules}{binary-datacntsec}{\B{datacntsec}} .. |Bcustom| mathdef:: \xref{binary/modules}{binary-customsec}{\B{custom}} -.. |Btype| mathdef:: \xref{binary/modules}{binary-typedef}{\B{type}} +.. |Btype| mathdef:: \xref{binary/modules}{binary-type}{\B{type}} .. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}} .. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}} .. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}} @@ -879,6 +882,7 @@ .. |Blocals| mathdef:: \xref{binary/modules}{binary-local}{\B{locals}} .. |Bdata| mathdef:: \xref{binary/modules}{binary-data}{\B{data}} .. |Bstart| mathdef:: \xref{binary/modules}{binary-start}{\B{start}} +.. |Bdatacnt| mathdef:: \xref{binary/modules}{binary-datacnt}{\B{datacnt}} .. Instructions, non-terminals diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup index cefe7bb41f..e6de9385d5 100644 --- a/spectec/spec/wasm-3.0/A-binary.watsup +++ b/spectec/spec/wasm-3.0/A-binary.watsup @@ -78,7 +78,7 @@ grammar Bmemidx : memidx = x:Bu32 => x grammar Belemidx : elemidx = x:Bu32 => x grammar Bdataidx : dataidx = x:Bu32 => x grammar Blocalidx : localidx = x:Bu32 => x -grammar Blabelidx : labelidx = x:Bu32 => x +grammar Blabelidx : labelidx = l:Bu32 => l grammar Bexternidx : externidx = | 0x00 x:Bfuncidx => FUNC x @@ -1031,7 +1031,8 @@ grammar Bfuncsec : typeidx* hint(desc "function section") = ;; Table section grammar Btable : table = - | tt:Btabletype e:Bexpr => TABLE tt e + | tt:Btabletype => TABLE tt (REF.NULL ht) -- if tt = lim (REF NULL? ht) + | 0x40 0x00 tt:Btabletype e:Bexpr => TABLE tt e grammar Btablesec : table* hint(desc "table section") = | tab*:Bsection_(4, Blist(Btable)) => tab* @@ -1058,7 +1059,7 @@ grammar Bglobalsec : global* hint(desc "global section") = ;; Export section grammar Bexport : export = - | nm:Bname ux:Bexternidx => EXPORT nm ux + | nm:Bname xx:Bexternidx => EXPORT nm xx grammar Bexportsec : export* hint(desc "export section") = | ex*:Bsection_(7, Blist(Bexport)) => ex* @@ -1080,19 +1081,19 @@ grammar Belemkind : reftype hint(desc "element kind") = grammar Belem : elem = | 0:Bu32 e_o:Bexpr y*:Blist(Bfuncidx) => - ELEM (REF NULL FUNC) (REF.FUNC y)* (ACTIVE 0 e_o) + ELEM (REF FUNC) (REF.FUNC y)* (ACTIVE 0 e_o) | 1:Bu32 rt:Belemkind y*:Blist(Bfuncidx) => ELEM rt (REF.FUNC y)* PASSIVE - | 2:Bu32 x:Btableidx expr:Bexpr rt:Belemkind y*:Blist(Bfuncidx) => - ELEM rt (REF.FUNC y)* (ACTIVE x expr) + | 2:Bu32 x:Btableidx e:Bexpr rt:Belemkind y*:Blist(Bfuncidx) => + ELEM rt (REF.FUNC y)* (ACTIVE x e) | 3:Bu32 rt:Belemkind y*:Blist(Bfuncidx) => ELEM rt (REF.FUNC y)* DECLARE - | 4:Bu32 e_o:Bexpr e*:Blist(Bexpr) => - ELEM (REF NULL FUNC) e* (ACTIVE 0 e_o) + | 4:Bu32 e_O:Bexpr e*:Blist(Bexpr) => + ELEM (REF NULL FUNC) e* (ACTIVE 0 e_O) | 5:Bu32 rt:Breftype e*:Blist(Bexpr) => ELEM rt e* PASSIVE - | 6:Bu32 x:Btableidx expr:Bexpr e*:Blist(Bexpr) => - ELEM (REF NULL FUNC) e* (ACTIVE x expr) + | 6:Bu32 x:Btableidx e_O:Bexpr e*:Blist(Bexpr) => + ELEM (REF NULL FUNC) e* (ACTIVE x e_O) | 7:Bu32 rt:Breftype e*:Blist(Bexpr) => ELEM rt e* DECLARE @@ -1102,13 +1103,14 @@ grammar Belemsec : elem* hint(desc "element section") = ;; Code section -syntax code = (local*, expr) +syntax code hint(macro none) = (local*, expr) grammar Blocals : local* hint(desc "local") = | n:Bu32 t:Bvaltype => (LOCAL t)^n grammar Bfunc : code = - | local**:Blist(Blocals) expr:Bexpr => ($concat_(local, local**), expr) + | loc**:Blist(Blocals) e:Bexpr => ($concat_(local, loc**), e) + -- if $(|$concat_(local, loc**)| < 2^32) grammar Bcode : code = | len:Bu32 code:Bfunc => code -- if len = ||Bfunc|| @@ -1139,8 +1141,11 @@ grammar Bdatacntsec : u32* hint(desc "data count section") = ;; Modules +grammar Bmagic : () = 0x00 0x61 0x73 0x6D => () +grammar Bversion : () = 0x01 0x00 0x00 0x00 => () grammar Bmodule : module = - | 0x00 0x61 0x73 0x6D 1:Bu32 + | Bmagic + Bversion Bcustomsec* diff --git a/spectec/spec/wasm-3.0/C-conventions.watsup b/spectec/spec/wasm-3.0/C-conventions.watsup index bf1d03d29c..68d93a9d85 100644 --- a/spectec/spec/wasm-3.0/C-conventions.watsup +++ b/spectec/spec/wasm-3.0/C-conventions.watsup @@ -109,5 +109,4 @@ def $allocXs2(syntax X, syntax Y, s*[0], X^n, Y^n) = (s*[n], a^n) grammar Btypewriter : () hint(macro none) = 0x00 => () def $symdots : A hint(show `...) hint(macro none) -grammar Bsym : A hint(macro none) = - $(B_1) => A_1 | $($symdots) | $(B_n) => A_n +grammar Bsym : A hint(macro none) = $(B_1) => A_1 | $($symdots) | $(B_n) => A_n diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index c30dcb214e..cb0f5ac2ef 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -1241,8 +1241,11 @@ and render_syms sep env gs = and render_prod arrow env prod = let (g, e, prems) = prod.it in - render_sym env g ^ " " ^ arrow ^ " " ^ - render_conditions env (render_exp env e) "&&&&&" prems + match e.it, prems with + | (TupE [] | ParenE ({it = SeqE []; _}, _)), [] -> render_sym env g + | _ -> + render_sym env g ^ " " ^ arrow ^ " " ^ + render_conditions env (render_exp env e) "&&&&&" prems and render_gram arrow env gram = let (dots1, prods, dots2) = gram.it in @@ -1323,7 +1326,7 @@ let render_typdeco env id = let render_typdef env d = match d.it with - | TypD (id1, _id2, args, t, _) -> + | TypD (id1, _id2, args, t, _hints) -> render_typdeco env id1 ^ render_apply render_typid render_exp env env.show_typ env.macro_typ id1 args ^ " &::=& " ^ render_typ env t @@ -1331,9 +1334,13 @@ let render_typdef env d = let render_gramdef env d = match d.it with - | GramD (id1, _id2, ps, _t, ({it = (_, prods, _); _} as gram), _) -> + | GramD (id1, _id2, ps, _t, gram, _hints) -> let args = List.map arg_of_param ps in - let arrow = if has_nl prods then "&\\quad\\Rightarrow&\\quad" else "~\\Rightarrow~" in + let arrow = + if env.config.display && has_nl (let _, prods, _ = gram.it in prods) + then "&\\quad\\Rightarrow&\\quad" + else "~\\Rightarrow~" + in "& " ^ render_apply render_gramid render_exp_as_sym env env.show_gram env.macro_gram id1 args ^ " &::=& " ^ render_gram arrow env gram diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 29eee36cce..3ee681b15d 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8214,7 +8214,7 @@ $$ & {\mathtt{elemidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\ & {\mathtt{dataidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\ & {\mathtt{localidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\ -& {\mathtt{labelidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\ +& {\mathtt{labelidx}} &::=& l{:}{\mathtt{u32}} ~\Rightarrow~ l \\ & {\mathtt{externidx}} &::=& \mathtt{0x00}~~x{:}{\mathtt{funcidx}} &\quad\Rightarrow&\quad \mathsf{func}~x \\ &&|& \mathtt{0x01}~~x{:}{\mathtt{tableidx}} &\quad\Rightarrow&\quad \mathsf{table}~x \\ &&|& \mathtt{0x02}~~x{:}{\mathtt{memidx}} &\quad\Rightarrow&\quad \mathsf{mem}~x \\ &&|& @@ -8920,8 +8920,8 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} -& {\mathtt{custom}} &::=& {\mathtt{name}}~~{{\mathtt{byte}}^\ast} ~\Rightarrow~ () \\ -& {\mathtt{customsec}} &::=& {{\mathtt{section}}}_{0}({\mathtt{custom}}) ~\Rightarrow~ () \\ +& {\mathtt{custom}} &::=& {\mathtt{name}}~~{{\mathtt{byte}}^\ast} \\ +& {\mathtt{customsec}} &::=& {{\mathtt{section}}}_{0}({\mathtt{custom}}) \\ \end{array} $$ @@ -8955,7 +8955,9 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} -& {\mathtt{table}} &::=& {\mathit{tt}}{:}{\mathtt{tabletype}}~~e{:}{\mathtt{expr}} ~\Rightarrow~ \mathsf{table}~{\mathit{tt}}~e \\ +& {\mathtt{table}} &::=& {\mathit{tt}}{:}{\mathtt{tabletype}} &\quad\Rightarrow&\quad \mathsf{table}~{\mathit{tt}}~(\mathsf{ref{.}null}~{\mathit{ht}}) + &\qquad \mbox{if}~{\mathit{tt}} = {\mathit{lim}}~(\mathsf{ref}~{\mathsf{null}^?}~{\mathit{ht}}) \\ &&|& +\mathtt{0x40}~~\mathtt{0x00}~~{\mathit{tt}}{:}{\mathtt{tabletype}}~~e{:}{\mathtt{expr}} &\quad\Rightarrow&\quad \mathsf{table}~{\mathit{tt}}~e \\ & {\mathtt{tablesec}} &::=& {{\mathit{tab}}^\ast}{:}{{\mathtt{section}}}_{4}({\mathtt{list}}({\mathtt{table}})) ~\Rightarrow~ {{\mathit{tab}}^\ast} \\ \end{array} $$ @@ -8982,7 +8984,7 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} -& {\mathtt{export}} &::=& {\mathit{nm}}{:}{\mathtt{name}}~~{\mathit{ux}}{:}{\mathtt{externidx}} ~\Rightarrow~ \mathsf{export}~{\mathit{nm}}~{\mathit{ux}} \\ +& {\mathtt{export}} &::=& {\mathit{nm}}{:}{\mathtt{name}}~~{\mathit{xx}}{:}{\mathtt{externidx}} ~\Rightarrow~ \mathsf{export}~{\mathit{nm}}~{\mathit{xx}} \\ & {\mathtt{exportsec}} &::=& {{\mathit{ex}}^\ast}{:}{{\mathtt{section}}}_{7}({\mathtt{list}}({\mathtt{export}})) ~\Rightarrow~ {{\mathit{ex}}^\ast} \\ \end{array} $$ @@ -9001,13 +9003,13 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} & {\mathtt{elemkind}} &::=& \mathtt{0x00} ~\Rightarrow~ \mathsf{ref}~\mathsf{null}~\mathsf{func} \\ -& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) \\ &&|& +& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) \\ &&|& 1{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{passive} \\ &&|& -2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~{\mathit{expr}}{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~{\mathit{expr}}) \\ &&|& +2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~e) \\ &&|& 3{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{declare} \\ &&|& -4{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_o) \\ &&|& +4{:}{\mathtt{u32}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_{\mathsf{o}}) \\ &&|& 5{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{passive} \\ &&|& -6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~{\mathit{expr}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~{\mathit{expr}}) \\ &&|& +6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~e_{\mathsf{o}}) \\ &&|& 7{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{declare} \\ & {\mathtt{elemsec}} &::=& {{\mathit{elem}}^\ast}{:}{{\mathtt{section}}}_{9}({\mathtt{list}}({\mathtt{elem}})) ~\Rightarrow~ {{\mathit{elem}}^\ast} \\ \end{array} @@ -9024,7 +9026,8 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} & {\mathtt{locals}} &::=& n{:}{\mathtt{u32}}~~t{:}{\mathtt{valtype}} ~\Rightarrow~ {(\mathsf{local}~t)^{n}} \\ -& {\mathtt{func}} &::=& {{{\mathit{local}}^\ast}^\ast}{:}{\mathtt{list}}({\mathtt{locals}})~~{\mathit{expr}}{:}{\mathtt{expr}} ~\Rightarrow~ ({\mathrm{concat}}({{{\mathit{local}}^\ast}^\ast}), {\mathit{expr}}) \\ +& {\mathtt{func}} &::=& {{{\mathit{loc}}^\ast}^\ast}{:}{\mathtt{list}}({\mathtt{locals}})~~e{:}{\mathtt{expr}} ~\Rightarrow~ ({\mathrm{concat}}({{{\mathit{loc}}^\ast}^\ast}), e) + &\qquad \mbox{if}~{|{\mathrm{concat}}({{{\mathit{loc}}^\ast}^\ast})|} < {2^{32}} \\ & {\mathtt{code}} &::=& {\mathit{len}}{:}{\mathtt{u32}}~~{\mathit{code}}{:}{\mathtt{func}} ~\Rightarrow~ {\mathit{code}} &\qquad \mbox{if}~{\mathit{len}} = ||{\mathtt{func}}|| \\ & {\mathtt{codesec}} &::=& {{\mathit{code}}^\ast}{:}{{\mathtt{section}}}_{10}({\mathtt{list}}({\mathtt{code}})) ~\Rightarrow~ {{\mathit{code}}^\ast} \\ @@ -9055,7 +9058,9 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} -& {\mathtt{module}} &::=& \mathtt{0x00}~~\mathtt{0x61}~~\mathtt{0x73}~~\mathtt{0x6D}~~1{:}{\mathtt{u32}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{type}}^\ast}{:}{\mathtt{typesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{import}}^\ast}{:}{\mathtt{importsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{table}}^\ast}{:}{\mathtt{tablesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{mem}}^\ast}{:}{\mathtt{memsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{global}}^\ast}{:}{\mathtt{globalsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{export}}^\ast}{:}{\mathtt{exportsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{start}}^\ast}{:}{\mathtt{startsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{m'}^\ast}{:}{\mathtt{datacntsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{data}}^{m}}{:}{\mathtt{datasec}}~~{{\mathtt{customsec}}^\ast} ~\Rightarrow~ \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast} +& {\mathtt{magic}} &::=& \mathtt{0x00}~~\mathtt{0x61}~~\mathtt{0x73}~~\mathtt{0x6D} \\ +& {\mathtt{version}} &::=& \mathtt{0x01}~~\mathtt{0x00}~~\mathtt{0x00}~~\mathtt{0x00} \\ +& {\mathtt{module}} &::=& {\mathtt{magic}}~~{\mathtt{version}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{type}}^\ast}{:}{\mathtt{typesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{import}}^\ast}{:}{\mathtt{importsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{table}}^\ast}{:}{\mathtt{tablesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{mem}}^\ast}{:}{\mathtt{memsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{global}}^\ast}{:}{\mathtt{globalsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{export}}^\ast}{:}{\mathtt{exportsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{start}}^\ast}{:}{\mathtt{startsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{m'}^\ast}{:}{\mathtt{datacntsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{data}}^{m}}{:}{\mathtt{datasec}}~~{{\mathtt{customsec}}^\ast} ~\Rightarrow~ \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast} &\qquad \mbox{if}~{{m'}^\ast} = \epsilon \lor {\mathrm{dataidx}}({{\mathit{func}}^{n}}) = \epsilon \\ &&&&&&\qquad {\land}~m = {\mathrm{sum}}({{m'}^\ast}) \\ &&&&&&\qquad {\land}~(({\mathit{func}} = \mathsf{func}~{\mathit{typeidx}}~{{\mathit{local}}^\ast}~{\mathit{expr}}))^{n} \\ @@ -9180,7 +9185,7 @@ $$ $$ \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}} -& {\mathtt{typewriter}} &::=& \mathtt{0x00} ~\Rightarrow~ () \\ +& {\mathtt{typewriter}} &::=& \mathtt{0x00} \\ \end{array} $$ diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 272172e910..340c2a35da 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -643,6 +643,7 @@ warning: grammar `Blimits` was never spliced warning: grammar `Blist` was never spliced warning: grammar `Blocalidx` was never spliced warning: grammar `Blocals` was never spliced +warning: grammar `Bmagic` was never spliced warning: grammar `Bmem` was never spliced warning: grammar `Bmemarg` was never spliced warning: grammar `Bmemidx` was never spliced @@ -677,6 +678,7 @@ warning: grammar `Bu64` was never spliced warning: grammar `BuN` was never spliced warning: grammar `Bvaltype` was never spliced warning: grammar `Bvectype` was never spliced +warning: grammar `Bversion` was never spliced warning: rule `Blocktype_ok/valtype` was never spliced warning: rule `Blocktype_ok/typeidx` was never spliced warning: rule `Comptype_ok/struct` was never spliced