diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 673102aa..622852aa 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -25,10 +25,10 @@ Construct Judgement :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` -:ref:`Element segment ` :math:`C \vdashelem \elem : \segtype` -:ref:`Element mode ` :math:`C \vdashelemmode \elemmode : \segtype` -:ref:`Data segment ` :math:`C \vdashdata \data : \segtype` -:ref:`Data mode ` :math:`C \vdashdatamode \datamode : \segtype` +:ref:`Element segment ` :math:`C \vdashelem \elem \ok` +:ref:`Element mode ` :math:`C \vdashelemmode \elemmode \ok` +:ref:`Data segment ` :math:`C \vdashdata \data \ok` +:ref:`Data mode ` :math:`C \vdashdatamode \datamode \ok` :ref:`Start function ` :math:`C \vdashstart \start \ok` :ref:`Export ` :math:`C \vdashexport \export : \externtype` :ref:`Export description ` :math:`C \vdashexportdesc \exportdesc : \externtype` diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 330f42dc..b875c1a9 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -485,54 +485,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera } -.. index:: element, table, table address, module instance, function index - -:math:`\INITELEM~\tableaddr~o~x^n` -.................................. - -* The :ref:`external table value ` :math:`\EVTABLE~\tableaddr` must be :ref:`valid ` with some :ref:`external table type ` :math:`\ETTABLE~\limits~\FUNCREF`. - -* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`. - -* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`context ` :math:`C`. - -* Each :ref:`function index ` :math:`x_i` in :math:`x^n` must be defined in the context :math:`C`. - -* Then the instruction is valid. - -.. math:: - \frac{ - S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\FUNCREF - \qquad - o + n \leq \limits.\LMIN - \qquad - (C.\CFUNCS[x] = \functype)^n - }{ - S; C \vdashadmininstr \INITELEM~\tableaddr~o~x^n \ok - } - - -.. index:: data, memory, memory address, byte - -:math:`\INITDATA~\memaddr~o~b^n` -................................ - -* The :ref:`external memory value ` :math:`\EVMEM~\memaddr` must be :ref:`valid ` with some :ref:`external memory type ` :math:`\ETMEM~\limits`. - -* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN` divided by the :ref:`page size ` :math:`64\,\F{Ki}`. - -* Then the instruction is valid. - -.. math:: - \frac{ - S \vdashexternval \EVMEM~\memaddr : \ETMEM~\limits - \qquad - o + n \leq \limits.\LMIN \cdot 64\,\F{Ki} - }{ - S; C \vdashadmininstr \INITDATA~\memaddr~o~b^n \ok - } - - .. index:: label, instruction, result type :math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END` diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 0cc7905a..36c1c993 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -321,7 +321,7 @@ Element Section ~~~~~~~~~~~~~~~ The *element section* has the id 9. -It decodes into a vector of :ref:`element segments ` that represent the |MELEM| component of a :ref:`module `. +It decodes into a vector of :ref:`element segments ` that represent the |MELEMS| component of a :ref:`module `. .. math:: \begin{array}{llclll} @@ -354,7 +354,7 @@ It decodes into a vector of :ref:`element segments ` that represent bit 2 indicates the use of element type and element expressions instead of element kind and element indices. In the current version of WebAssembly, at most one table may be defined or - imported in a single module, so all valid :ref:`active ` + imported in a single module, so all valid :ref:`active ` element segments have a |ETABLE| value of :math:`0`. Additional element kinds may be added in future versions of WebAssembly. @@ -429,7 +429,7 @@ Data Section ~~~~~~~~~~~~ The *data section* has the id 11. -It decodes into a vector of :ref:`data segments ` that represent the |MDATA| component of a :ref:`module `. +It decodes into a vector of :ref:`data segments ` that represent the |MDATAS| component of a :ref:`module `. .. math:: \begin{array}{llclll} @@ -450,7 +450,7 @@ It decodes into a vector of :ref:`data segments ` that represent th 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 + imported in a single module, so all valid :ref:`active ` data segments have a |DMEM| value of :math:`0`. @@ -543,8 +543,8 @@ Furthermore, it must be present if any :math:`data index ` occur \MTABLES~\table^\ast, \\ \MMEMS~\mem^\ast, \\ \MGLOBALS~\global^\ast, \\ - \MELEM~\elem^\ast, \\ - \MDATA~\data^m, \\ + \MELEMS~\elem^\ast, \\ + \MDATAS~\data^m, \\ \MSTART~\start^?, \\ \MIMPORTS~\import^\ast, \\ \MEXPORTS~\export^\ast ~\} \\ diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 91ffa3d5..1e083a00 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -488,10 +488,10 @@ Growing :ref:`memories ` .................................. The allocation function for :ref:`modules ` requires a suitable list of :ref:`external values ` that are assumed to :ref:`match ` the :ref:`import ` vector of the module, -and a list of initialization :ref:`values ` for the module's :ref:`globals `. +a list of initialization :ref:`values ` for the module's :ref:`globals `, +and list of :ref:`function element ` vectors for the module's :ref:`element segments `. -1. Let :math:`\module` be the :ref:`module ` to allocate and :math:`\externval_{\F{im}}^\ast` the vector of :ref:`external values ` providing the module's imports, -and :math:`\val^\ast` the initialization :ref:`values ` of the module's :ref:`globals `. +1. Let :math:`\module` be the :ref:`module ` to allocate and :math:`\externval_{\F{im}}^\ast` the vector of :ref:`external values ` providing the module's imports, :math:`\val^\ast` the initialization :ref:`values ` of the module's :ref:`globals `, and :math:`(\funcelem^\ast)^\ast` the :ref:`function element ` vectors of the module's :ref:`element segments `. 2. For each :ref:`function ` :math:`\func_i` in :math:`\module.\MFUNCS`, do: @@ -509,23 +509,35 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul a. Let :math:`\globaladdr_i` be the :ref:`global address ` resulting from :ref:`allocating ` :math:`\global_i.\GTYPE` with initializer value :math:`\val^\ast[i]`. -6. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. +6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, do: -7. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. + a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` a :ref:`element instance ` with contents :math:`(\funcelem^\ast)^\ast[i]`. -8. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. +7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS`, do: -9. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. + a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` a :ref:`data instance ` with contents :math:`\data_i.\DINIT`. -10. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. +8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. -11. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. +9. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. -12. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. +10. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. -13. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. +11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. -14. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: +12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. + +13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. + +14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. + +15. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. + +16. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. + +17. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. + +18. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: a. If :math:`\export_i` is a function export for :ref:`function index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVFUNC~(\funcaddr_{\F{mod}}^\ast[x])`. @@ -537,17 +549,17 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul e. Let :math:`\exportinst_i` be the :ref:`export instance ` :math:`\{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}`. -15. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. +19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -16. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. +20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. -17. Return :math:`\moduleinst`. +21. Return :math:`\moduleinst`. .. math:: ~\\ \begin{array}{rlll} - \allocmodule(S, \module, \externval_{\F{im}}^\ast, \val^\ast) &=& S', \moduleinst \end{array} + \allocmodule(S, \module, \externval_{\F{im}}^\ast, \val^\ast, (\funcelem^\ast)^\ast) &=& S', \moduleinst \end{array} where: @@ -560,6 +572,8 @@ where: \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ + \MIELEMS~\elemaddr^\ast, \\ + \MIDATAS~\dataaddr^\ast, \\ \MIEXPORTS~\exportinst^\ast ~\} \end{array} \\[1ex] S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ @@ -567,8 +581,11 @@ where: \qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES) \\ S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\ - S', \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) + S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\ + S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, (\funcelem^\ast)^\ast) \\ + S', \dataaddr^\ast &=& \allocdata^\ast(S_5, (\data.\DINIT)^\ast) + \qquad\qquad\qquad~ (\where \data^\ast = \module.\MDATAS) \\ \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex] \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast @@ -614,8 +631,6 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals), Instantiation ~~~~~~~~~~~~~ -.. todo:: Adjust for passive segments. - Given a :ref:`store ` :math:`S`, a :ref:`module ` :math:`\module` is instantiated with a list of :ref:`external values ` :math:`\externval^n` supplying the required imports as follows. Instantiation checks that the module is :ref:`valid ` and the provided imports :ref:`match ` the declared types, @@ -661,121 +676,110 @@ It is up to the :ref:`embedder ` to define how such conditions are rep f. Pop the frame :math:`F_{\F{im}}` from the stack. -6. Let :math:`\moduleinst` be a new module instance :ref:`allocated ` from :math:`\module` in store :math:`S` with imports :math:`\externval^n` and global initializer values :math:`\val^\ast`, and let :math:`S'` be the extended store produced by module allocation. - -7. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`. + g. Let :math:`\val^\ast` be the conatenation of :math:`\val_i` in index order. -8. Push the frame :math:`F` to the stack. +6. Let :math:`(\funcelem^\ast)^\ast` be the list of :ref:`function element ` vectors determined by the :ref:`element segments ` in :math:`\module`. These may be calculated as follows. -9. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM` whose :ref:`mode ` :math:`\elem_i.\EMODE` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{eoexpr}_i \}`, do: + a. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, and for each :ref:`element expression ` :math:`\elemexpr_{ij}` in :math:`\elem_i.\EINIT`, do: - a. Assert: due to :ref:`validation `, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists. + i. If :math:`\elemexpr_{ij}` is of the form :math:`\REFNULL`, then let the :ref:`function element ` :math:`\funcelem_{ij}` be :math:`\epsilon`. - b. Let :math:`\tableaddr_i` be the :ref:`table address ` :math:`\moduleinst.\MITABLES[\tableidx_i]`. + ii. Else, :math:`\elemexpr_{ij}` is of the form is :math:`\REFFUNC~\funcidx_{ij}`. - c. Assert: due to :ref:`validation `, :math:`S'.\STABLES[\tableaddr_i]` exists. + iii. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]` exists. - d. Let :math:`\tableinst_i` be the :ref:`table instance ` :math:`S'.\STABLES[\tableaddr_i]`. + iv. Let the :ref:`function element ` :math:`\funcelem_{ij}` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`. - e. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating ` the expression :math:`\X{eoexpr}_i`. + b. Let :math:`\funcelem^\ast_i` be the concatenation of function elements :math:`\funcelem_{ij}` in order of index :math:`j`. - f. Assert: due to :ref:`validation `, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`. + c. Let :math:`(\funcelem^\ast)^\ast` be the concatenation of function element vectors :math:`\funcelem^\ast_i` in order of index :math:`i`. - g. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`. +7. Let :math:`\moduleinst` be a new module instance :ref:`allocated ` from :math:`\module` in store :math:`S` with imports :math:`\externval^n`, global initializer values :math:`\val^\ast`, and element segment contents :math:`(\funcelem^\ast)^\ast`, and let :math:`S'` be the extended store produced by module allocation. - h. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then: +8. Let :math:`F` be the auxiliary :ref:`frame ` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`. - i. Fail. +9. Push the frame :math:`F` to the stack. -10. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA` whose :ref:`mode ` :math:`\data_i.\DMODE` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{doexpr}_i \}`, do: +10. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: - a. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists. + a. Assert: :math:`\tableidx_i` is :math:`0`. - b. Let :math:`\memaddr_i` be the :ref:`memory address ` :math:`\moduleinst.\MIMEMS[\memidx_i]`. + b. Let :math:`n` be the length of the vector :math:`\elem_i.\EINIT`. - c. Assert: due to :ref:`validation `, :math:`S'.\SMEMS[\memaddr_i]` exists. + c. :ref:`Execute ` the instruction sequence :math:`\X{einstr}^\ast_i`. - d. Let :math:`\meminst_i` be the :ref:`memory instance ` :math:`S'.\SMEMS[\memaddr_i]`. + d. :ref:`Execute ` the instruction :math:`\I32.\CONST~0`. - e. Let :math:`\X{doval}_i` be the result of :ref:`evaluating ` the expression :math:`\data_i.\DOFFSET`. + e. :ref:`Execute ` the instruction :math:`\I32.\CONST~n`. - f. Assert: due to :ref:`validation `, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`. + f. :ref:`Execute ` the instruction :math:`\TABLEINIT~i`. - g. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`. + g. :ref:`Execute ` the instruction :math:`\ELEMDROP~i`. - h. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then: +11. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do: - i. Fail. + a. Assert: :math:`\memidx_i` is :math:`0`. -11. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. + b. Let :math:`n` be the length of the vector :math:`\data_i.\DINIT`. -12. Pop the frame from the stack. + c. :ref:`Execute ` the instruction sequence :math:`\X{dinstr}^\ast_i`. -13. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM` whose :ref:`mode ` :math:`\elem_i.\EMODE` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{eoexpr}_i \}`, do: + d. :ref:`Execute ` the instruction :math:`\I32.\CONST~0`. - a. For each :ref:`function index ` :math:`\funcidx_{ij}` in :math:`\elem_i.\EINIT` (starting with :math:`j = 0`), do: + e. :ref:`Execute ` the instruction :math:`\I32.\CONST~n`. - i. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]` exists. + f. :ref:`Execute ` the instruction :math:`\MEMORYINIT~i`. - ii. Let :math:`\funcaddr_{ij}` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`. + g. :ref:`Execute ` the instruction :math:`\DATADROP~i`. - iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`. +12. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: -14. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA` whose :ref:`mode ` :math:`\data_i.\DMODE` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{doexpr}_i \}`, do: + a. Let :math:`\start` be the :ref:`start function ` :math:`\module.\MSTART`. - a. For each :ref:`byte ` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do: + b. :ref:`Execute ` the instruction :math:`\CALL~\start.\SFUNC`. - i. Replace :math:`\meminst_i.\MIDATA[\X{do}_i + j]` with :math:`b_{ij}`. +13. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. -15. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: - - a. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\module.\MSTART.\SFUNC]` exists. - - b. Let :math:`\funcaddr` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\module.\MSTART.\SFUNC]`. - - c. :ref:`Invoke ` the function instance at :math:`\funcaddr`. +14. Pop the frame :math:`F` from the stack. .. math:: ~\\ \begin{array}{@{}rcll} - \instantiate(S, \module, \externval^n) &=& S'; F; + \instantiate(S, \module, \externval^k) &=& S'; F; \begin{array}[t]{@{}l@{}} - (\INITELEM~\tableaddr~\X{eo}~\elem.\EINIT)^\ast \\ - (\INITDATA~\memaddr~\X{do}~\data.\DINIT)^\ast \\ - (\INVOKE~\funcaddr)^? \\ + \F{runelem}_0(\elem^n[0])~\dots~\F{runelem}_{n-1}(\elem^n[n-1]) \\ + \F{rundata}_0(\data^m[0])~\dots~\F{rundata}_{m-1}(\data^m[m-1]) \\ + (\CALL~\start.\SFUNC)^? \\ \end{array} \\ &(\iff - & \vdashmodule \module : \externtype_{\F{im}}^n \to \externtype_{\F{ex}}^\ast \\ - &\wedge& (S \vdashexternval \externval : \externtype)^n \\ - &\wedge& (\vdashexterntypematch \externtype \matches \externtype_{\F{im}})^n \\[1ex] + & \vdashmodule \module : \externtype_{\F{im}}^k \to \externtype_{\F{ex}}^\ast \\ + &\wedge& (S \vdashexternval \externval : \externtype)^k \\ + &\wedge& (\vdashexterntypematch \externtype \matches \externtype_{\F{im}})^k \\[1ex] &\wedge& \module.\MGLOBALS = \global^\ast \\ - &\wedge& \module.\MELEM = \elem^\ast \\ - &\wedge& \module.\MDATA = \data^\ast \\ + &\wedge& \module.\MELEMS = \elem^n \\ + &\wedge& \module.\MDATAS = \data^m \\ &\wedge& \module.\MSTART = \start^? \\[1ex] - &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^n, \val^\ast) \\ + &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^k, \val^\ast) \\ &\wedge& F = \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \} \\[1ex] &\wedge& (S'; F; \global.\GINIT \stepto^\ast S'; F; \val~\END)^\ast \\ &\wedge& (S'; F; \elem.\EOFFSET \stepto^\ast S'; F; \I32.\CONST~\X{eo}~\END)^\ast \\ &\wedge& (S'; F; \data.\DOFFSET \stepto^\ast S'; F; \I32.\CONST~\X{do}~\END)^\ast \\[1ex] - &\wedge& (\X{eo} + |\elem.\EINIT| \leq |S'.\STABLES[\tableaddr].\TIELEM|)^\ast \\ - &\wedge& (\X{do} + |\data.\DINIT| \leq |S'.\SMEMS[\memaddr].\MIDATA|)^\ast - \\[1ex] &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\ &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\ &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^?) - \\[2ex] - S; F; \INITELEM~a~i~\epsilon &\stepto& - S; F; \epsilon \\ - S; F; \INITELEM~a~i~(x_0~x^\ast) &\stepto& - S'; F; \INITELEM~a~(i+1)~x^\ast \\ && - (\iff S' = S \with \STABLES[a].\TIELEM[i] = F.\AMODULE.\MIFUNCS[x_0]) - \\[1ex] - S; F; \INITDATA~a~i~\epsilon &\stepto& - S; F; \epsilon \\ - S; F; \INITDATA~a~i~(b_0~b^\ast) &\stepto& - S'; F; \INITDATA~a~(i+1)~b^\ast \\ && - (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b_0) + \end{array} + +where: + +.. math:: + \begin{array}{@{}l} + \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\funcelem^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\ + \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\funcelem^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad + \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\[1ex] + \F{rundata}_i(\{\DINIT~b^n, DMODE~\DPASSIVE\}) \quad=\quad \epsilon \\ + \F{rundata}_i(\{\DINIT~b^n, DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad + \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\MEMORYINIT~i)~(\DATADROP~i) \\ \end{array} .. note:: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 0b66c091..414a8baf 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -489,8 +489,6 @@ Conventions pair:: abstract syntax; administrative instruction .. _syntax-trap: .. _syntax-invoke: -.. _syntax-init_elem: -.. _syntax-init_data: .. _syntax-table_get: .. _syntax-table_set: .. _syntax-instr-admin: @@ -509,8 +507,6 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, identified by its :ref:`address `. It unifies the handling of different forms of calls. -The |INITELEM| and |INITDATA| instructions perform initialization of :ref:`element ` and :ref:`data ` segments during module :ref:`instantiation `. - -.. note:: - The reason for splitting instantiation into individual reduction steps is to provide a semantics that is compatible with future extensions like threads. - The |TABLEGET| and |TABLESET| instructions are used to simplify the specification of the |TABLEINIT| and |TABLECOPY| instructions. .. note:: diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 8f2037ec..83616445 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -9,7 +9,7 @@ WebAssembly programs are organized into *modules*, which are the unit of deployment, loading, and compilation. A module collects definitions for :ref:`types `, :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals `. In addition, it can declare :ref:`imports ` and :ref:`exports ` -and provide initialization in the form of :ref:`active ` and :ref:`passive ` :ref:`data ` and :ref:`element ` segments, or a :ref:`start function `. +and provide initialization in the form of :ref:`data ` and :ref:`element ` segments, or a :ref:`start function `. .. math:: \begin{array}{lllll} @@ -19,8 +19,8 @@ and provide initialization in the form of :ref:`active ` and :ref \MTABLES~\vec(\table), \\&&&& \MMEMS~\vec(\mem), \\&&&& \MGLOBALS~\vec(\global), \\&&&& - \MELEM~\vec(\elem), \\&&&& - \MDATA~\vec(\data), \\&&&& + \MELEMS~\vec(\elem), \\&&&& + \MDATAS~\vec(\data), \\&&&& \MSTART~\start^?, \\&&&& \MIMPORTS~\vec(\import), \\&&&& \MEXPORTS~\vec(\export) \quad\} \\ @@ -255,10 +255,10 @@ Element Segments The initial contents of a table is uninitialized. *Element segments* can be used to initialize a subrange of a table from a static :ref:`vector ` of elements. -The |MELEM| component of a module defines a vector of element segments. +The |MELEMS| component of a module defines a vector of element segments. Each element segment defines an :ref:`element type ` and a corresponding list of :ref:`element expressions `. -Element segments have a mode that identifies them as either :ref:`passive ` or :ref:`active `. +Element segments have a mode that identifies them as either *passive* or *active*. A passive element segment's elements can be copied to a table using the |TABLEINIT| instruction. An active element segment copies its elements into a table during :ref:`instantiation `, as specified by a :ref:`table index ` and a :ref:`constant ` :ref:`expression ` defining an offset into that table. @@ -295,9 +295,9 @@ Data Segments The initial contents of a :ref:`memory ` are zero bytes. *Data segments* can be used to initialize a range of memory from a static :ref:`vector ` of :ref:`bytes `. -The |MDATA| component of a module defines a vector of data segments. +The |MDATAS| component of a module defines a vector of data segments. -Like element segments, data segments have a mode that identifies them as either :ref:`passive ` or :ref:`active `. +Like element segments, data segments have a mode that identifies them as either *passive* or *active*. A passive data segment's contents can be copied into a memory using the |MEMORYINIT| instruction. An active data segment copies its contents into a memory during :ref:`instantiation `, as specified by a :ref:`memory index ` and a :ref:`constant ` :ref:`expression ` defining an offset into that memory. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 9f045ba4..be810636 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -181,25 +181,6 @@ Global Types \end{array} -.. index:: ! segtype, ! active, ! passive - pair: abstract syntax; segtype -.. _syntax-segtype: -.. _syntax-active: -.. _syntax-passive: - -Segment Types -~~~~~~~~~~~~~ - -*Segment types* classify :ref:`data segments ` and :ref:`element segments `, which can either be *passive* or *active*. - -.. math:: - \begin{array}{llll} - \production{segment type} & \segtype &::=& - \SPASSIVE ~|~ - \SACTIVE \\ - \end{array} - - .. index:: ! external type, function type, table type, memory type, global type, import, external value pair: abstract syntax; external type pair: external; type diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 114d6b17..91ebbd56 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -641,8 +641,8 @@ The name serves a documentary role only. \X{gl}{:}\Tglobal_I &\Rightarrow& \{\MGLOBALS~\X{gl}\} \\ |& \X{ex}{:}\Texport_I &\Rightarrow& \{\MEXPORTS~\X{ex}\} \\ |& \X{st}{:}\Tstart_I &\Rightarrow& \{\MSTART~\X{st}\} \\ |& - \X{el}{:}\Telem_I &\Rightarrow& \{\MELEM~\X{el}\} \\ |& - \X{da}{:}\Tdata_I &\Rightarrow& \{\MDATA~\X{da}\} \\ + \X{el}{:}\Telem_I &\Rightarrow& \{\MELEMS~\X{el}\} \\ |& + \X{da}{:}\Tdata_I &\Rightarrow& \{\MDATAS~\X{da}\} \\ \end{array} \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 5756c05a..967c4d0b 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -179,9 +179,6 @@ .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}} .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}} -.. |SACTIVE| mathdef:: \xref{syntax/types}{syntax-segtype}{\K{active}} -.. |SPASSIVE| mathdef:: \xref{syntax/types}{syntax-segtype}{\K{passive}} - .. |ETFUNC| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{func}} .. |ETTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}} .. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}} @@ -197,7 +194,6 @@ .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} .. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}} .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}} -.. |segtype| mathdef:: \xref{syntax/types}{syntax-segtype}{\X{segtype}} .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}} @@ -248,8 +244,8 @@ .. |MGLOBALS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{globals}} .. |MIMPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{imports}} .. |MEXPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{exports}} -.. |MDATA| mathdef:: \xref{syntax/modules}{syntax-module}{\K{data}} -.. |MELEM| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elem}} +.. |MDATAS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{datas}} +.. |MELEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elems}} .. |MSTART| mathdef:: \xref{syntax/modules}{syntax-module}{\K{start}} .. |FTYPE| mathdef:: \xref{syntax/modules}{syntax-func}{\K{type}} @@ -764,8 +760,8 @@ .. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}} .. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}} .. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}} -.. |CELEM| mathdef:: \xref{valid/conventions}{context}{\K{elem}} -.. |CDATA| mathdef:: \xref{valid/conventions}{context}{\K{data}} +.. |CELEMS| mathdef:: \xref{valid/conventions}{context}{\K{elems}} +.. |CDATAS| mathdef:: \xref{valid/conventions}{context}{\K{datas}} .. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}} .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} @@ -934,8 +930,6 @@ .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} -.. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}} -.. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}} .. |TABLEGET| mathdef:: \xref{exec/runtime}{syntax-table_get}{\K{table.get}} .. |TABLESET| mathdef:: \xref{exec/runtime}{syntax-table_set}{\K{table.set}} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 4e04ce28..7f132d7e 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -38,8 +38,8 @@ which collects relevant information about the surrounding :ref:`module ` :math: & \CTABLES & \tabletype^\ast, \\ & \CMEMS & \memtype^\ast, \\ & \CGLOBALS & \globaltype^\ast, \\ - & \CELEM & \segtype^\ast, \\ - & \CDATA & \segtype^\ast, \\ + & \CELEMS & {\ok}^\ast, \\ + & \CDATAS & {\ok}^\ast, \\ & \CLOCALS & \valtype^\ast, \\ & \CLABELS & \resulttype^\ast, \\ & \CRETURN & \resulttype^? ~\} \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 6aef34ab..806dde71 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -330,7 +330,7 @@ Table Instructions * The table :math:`C.\CTABLES[0]` must be defined in the context. -* The element segment :math:`C.\CELEM[x]` must be defined in the context. +* The element segment :math:`C.\CELEMS[x]` must be defined in the context. * Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. @@ -338,7 +338,7 @@ Table Instructions \frac{ C.\CTABLES[0] = \tabletype \qquad - C.\CELEM[x] = \segtype + C.\CELEMS[x] = {\ok} }{ C \vdashinstr \TABLEINIT~x : [\I32~\I32~\I32] \to [] } @@ -349,13 +349,13 @@ Table Instructions :math:`\ELEMDROP~x` ................... -* The element segment :math:`C.\CELEM[x]` must be defined in the context. +* The element segment :math:`C.\CELEMS[x]` must be defined in the context. * Then the instruction is valid with type :math:`[] \to []`. .. math:: \frac{ - C.\CELEM[x] = \segtype + C.\CELEMS[x] = {\ok} }{ C \vdashinstr \ELEMDROP~x : [] \to [] } @@ -527,7 +527,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The data segment :math:`C.\CDATA[x]` must be defined in the context. +* The data segment :math:`C.\CDATAS[x]` must be defined in the context. * Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. @@ -535,7 +535,7 @@ Memory Instructions \frac{ C.\CMEMS[0] = \memtype \qquad - C.\CDATA[x] = \segtype + C.\CDATAS[x] = {\ok} }{ C \vdashinstr \MEMORYINIT~x : [\I32~\I32~\I32] \to [] } @@ -546,13 +546,13 @@ Memory Instructions :math:`\DATADROP~x` ................... -* The data segment :math:`C.\CDATA[x]` must be defined in the context. +* The data segment :math:`C.\CDATAS[x]` must be defined in the context. * Then the instruction is valid with type :math:`[] \to []`. .. math:: \frac{ - C.\CDATA[x] = \segtype + C.\CDATAS[x] = {\ok} }{ C \vdashinstr \DATADROP~x : [] \to [] } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 408ae813..cd65e527 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -145,7 +145,7 @@ Globals :math:`\global` are classified by :ref:`global types Element Segments ~~~~~~~~~~~~~~~~ -Element segments :math:`\elem` are classified by :ref:`segment types `, as determined by their :ref:`mode `. +Element segments :math:`\elem` are not classified by any type but merely checked for well-formedness. :math:`\{ \ETYPE~et, \EINIT~e^\ast, \EMODE~\elemmode \}` ........................................................ @@ -154,18 +154,18 @@ Element segments :math:`\elem` are classified by :ref:`segment types `. -* The element mode :math:`\elemmode` must valid with type :math:`\segtype`. +* The element mode :math:`\elemmode` must be valid. -* Then the element segment is valid with type :math:`\segtype`. +* Then the element segment is valid. .. math:: \frac{ (C \vdashelemexpr e \ok)^\ast \qquad - C; \X{et} \vdashelemmode \elemmode : \segtype + C; \X{et} \vdashelemmode \elemmode \ok }{ - C \vdashelem \{ \ETYPE~et, \EINIT~e^\ast, \EMODE~\elemmode \} : \segtype + C \vdashelem \{ \ETYPE~et, \EINIT~e^\ast, \EMODE~\elemmode \} \ok } @@ -198,12 +198,12 @@ Element segments :math:`\elem` are classified by :ref:`segment types `. -* Then the element mode is valid with type |SACTIVE|. +* Then the element mode is valid. .. math:: \frac{ @@ -232,7 +232,7 @@ Element segments :math:`\elem` are classified by :ref:`segment types `, as determined by their :ref:`mode `. +Data segments :math:`\data` are not classified by any type but merely checked for well-formedness. :math:`\{ \DINIT~b^\ast, \DMODE~\datamode \}` .................................................... -* The data mode :math:`\datamode` must valid with type :math:`\segtype`. +* The data mode :math:`\datamode` must be valid. -* Then the data segment is valid with type :math:`\segtype`. +* Then the data segment is valid. .. math:: \frac{ - C \vdashdatamode \datamode : \segtype + C \vdashdatamode \datamode \ok }{ - C \vdashdata \{ \DINIT~b^\ast, \DMODE~\datamode \} : \segtype + C \vdashdata \{ \DINIT~b^\ast, \DMODE~\datamode \} \ok } @@ -268,12 +268,12 @@ Data segments :math:`\data` are classified by :ref:`segment types `. -* Then the data mode is valid with type |SACTIVE|. +* Then the data mode is valid. .. math:: \frac{ @@ -296,7 +296,7 @@ Data segments :math:`\data` are classified by :ref:`segment types ` :math:`\X{it}^\ast` and the internal :ref:`global types ` :math:`\X{gt}^\ast` as determined below, - * :math:`C.\CELEM` is :math:`\X{est}^\ast`, with :ref:`segment types ` :math:`\X{est}^\ast` as determined below, + * :math:`C.\CELEMS` is :math:`{\ok}^{N_e}`, where :math:`N_e` is the length of the vector :math:`\module.\MELEMS`, - * :math:`C.\CDATA` is :math:`\X{dst}^\ast`, with :ref:`segment types ` :math:`\X{dst}^\ast` as determined below, + * :math:`C.\CDATAS` is :math:`{\ok}^{N_d}`, where :math:`N_d` is the length of the vector :math:`\module.\MDATAS`, * :math:`C.\CLOCALS` is empty, @@ -568,11 +568,11 @@ Instead, the context :math:`C` for validation of the module's content is constru * Under the context :math:`C'`, the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. - * For each :math:`\elem_i` in :math:`\module.\MELEM`, - the segment :math:`\elem_i` must be :ref:`valid ` with a :ref:`segment type ` :math:`\X{est}_i`. + * For each :math:`\elem_i` in :math:`\module.\MELEMS`, + the segment :math:`\elem_i` must be :ref:`valid `. - * For each :math:`\data_i` in :math:`\module.\MDATA`, - the segment :math:`\data_i` must be :ref:`valid ` with a :ref:`segment type ` :math:`\X{dst}_i`. + * For each :math:`\data_i` in :math:`\module.\MDATAS`, + the segment :math:`\data_i` must be :ref:`valid `. * If :math:`\module.\MSTART` is non-empty, then :math:`\module.\MSTART` must be :ref:`valid `. @@ -597,10 +597,6 @@ Instead, the context :math:`C` for validation of the module's content is constru * Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types ` :math:`\X{gt}_i`, in index order. -* Let :math:`\X{est}^\ast` be the concatenation of the :ref:`segment types ` :math:`\X{est}_i`, in index order. - -* Let :math:`\X{dst}^\ast` be the concatenation of the :ref:`segment types ` :math:`\X{dst}_i`, in index order. - * Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types ` :math:`\X{it}_i` of the imports, in index order. * Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types ` :math:`\X{et}_i` of the exports, in index order. @@ -620,9 +616,9 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C' \vdashglobal \global : \X{gt})^\ast \\ - (C \vdashelem \elem : \X{est})^\ast + (C \vdashelem \elem \ok)^{N_e} \quad - (C \vdashdata \data : \X{dst})^\ast + (C \vdashdata \data \ok)^{N_d} \quad (C \vdashstart \start \ok)^? \quad @@ -638,7 +634,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \qquad \X{igt}^\ast = \etglobals(\X{it}^\ast) \\ - C = \{ \CTYPES~\functype^\ast, \CFUNCS~\X{ift}^\ast~\X{ft}^\ast, \CTABLES~\X{itt}^\ast~\X{tt}^\ast, \CMEMS~\X{imt}^\ast~\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast~\X{gt}^\ast, \CELEM~\X{est}^\ast, \CDATA~\X{dst}^\ast \} + C = \{ \CTYPES~\functype^\ast, \CFUNCS~\X{ift}^\ast~\X{ft}^\ast, \CTABLES~\X{itt}^\ast~\X{tt}^\ast, \CMEMS~\X{imt}^\ast~\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast~\X{gt}^\ast, \CELEMS~{\ok}^{N_e}, \CDATAS~{\ok}^{N_d} \} \\ C' = \{ \CGLOBALS~\X{igt}^\ast \} \qquad @@ -656,8 +652,8 @@ Instead, the context :math:`C` for validation of the module's content is constru \MTABLES~\table^\ast, \MMEMS~\mem^\ast, \MGLOBALS~\global^\ast, \\ - \MELEM~\elem^\ast, - \MDATA~\data^\ast, + \MELEMS~\elem^\ast, + \MDATAS~\data^\ast, \MSTART~\start^?, \MIMPORTS~\import^\ast, \MEXPORTS~\export^\ast \} : \X{it}^\ast \to \X{et}^\ast \\ diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 90c0ddcd..5aaf42ad 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -405,11 +405,6 @@ let eval_const (inst : module_inst) (const : const) : value = | [v] -> v | vs -> Crash.error const.at "wrong number of results on stack" -let i32 (v : value) at = - match v with - | I32 i -> i - | _ -> Crash.error at "type error: i32 value expected" - (* Modules *) @@ -447,45 +442,12 @@ let elem_list inst init = in List.map to_elem init let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst = - let {etype; einit; emode} = seg.it in - match emode.it with - | Passive -> ref (Some (elem_list inst einit)) - | Active _ -> ref None + let {etype; einit; _} = seg.it in + ref (Some (elem_list inst einit)) let create_data (inst : module_inst) (seg : data_segment) : data_inst = - let {dinit; dmode} = seg.it in - match dmode.it with - | Passive -> ref (Some dinit) - | Active _ -> ref None - - -let init_func (inst : module_inst) (func : func_inst) = - match func with - | Func.AstFunc (_, inst_ref, _) -> inst_ref := inst - | _ -> assert false - -let init_table (inst : module_inst) (seg : elem_segment) = - let {etype; einit; emode} = seg.it in - match emode.it with - | Passive -> () - | Active {index; offset} -> - let refs = elem_list inst einit in - let tab = table inst index in - let i = i32 (eval_const inst offset) offset.at in - let n = Int32.of_int (List.length einit) in - (try Table.init tab refs i 0l n - with Table.Bounds -> Link.error seg.at "elements segment does not fit table") - -let init_memory (inst : module_inst) (seg : data_segment) = - let {dinit; dmode} = seg.it in - match dmode.it with - | Passive -> () - | Active {index; offset} -> - let mem = memory inst index in - let i = i32 (eval_const inst offset) offset.at in - let n = Int32.of_int (String.length dinit) in - (try Memory.init mem dinit (I64_convert.extend_i32_u i) 0L n - with Memory.Bounds -> Link.error seg.at "data segment does not fit memory") + let {dinit; _} = seg.it in + ref (Some dinit) let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst) @@ -498,6 +460,40 @@ let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst) | ExternMemory mem -> {inst with memories = mem :: inst.memories} | ExternGlobal glob -> {inst with globals = glob :: inst.globals} +let init_func (inst : module_inst) (func : func_inst) = + match func with + | Func.AstFunc (_, inst_ref, _) -> inst_ref := inst + | _ -> assert false + +let run_elem i elem = + match elem.it.emode.it with + | Passive -> [] + | Active {index; offset} -> + let at = elem.it.emode.at in + let x = i @@ at in + offset.it @ [ + Const (I32 0l @@ at) @@ at; + Const (I32 (Lib.List32.length elem.it.einit) @@ at) @@ at; + TableInit x @@ at; + ElemDrop x @@ at + ] + +let run_data i data = + match data.it.dmode.it with + | Passive -> [] + | Active {index; offset} -> + let at = data.it.dmode.at in + let x = i @@ at in + offset.it @ [ + Const (I32 0l @@ at) @@ at; + Const (I32 (Int32.of_int (String.length data.it.dinit)) @@ at) @@ at; + MemoryInit x @@ at; + DataDrop x @@ at + ] + +let run_start start = + [Call start @@ start.at] + let init (m : module_) (exts : extern list) : module_inst = let { imports; tables; memories; globals; funcs; types; @@ -527,7 +523,8 @@ let init (m : module_) (exts : extern list) : module_inst = } in List.iter (init_func inst) fs; - List.iter (init_table inst) elems; - List.iter (init_memory inst) datas; - Lib.Option.app (fun x -> ignore (invoke (func inst x) [])) start; + let es_elem = List.concat (Lib.List32.mapi run_elem elems) in + let es_data = List.concat (Lib.List32.mapi run_data datas) in + let es_start = Lib.Option.get (Lib.Option.map run_start start) [] in + ignore (eval (config inst [] (List.map plain (es_elem @ es_data @ es_start)))); inst diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index ea59848b..00b76f6c 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -10,7 +10,6 @@ type mutability = Immutable | Mutable type table_type = TableType of Int32.t limits * elem_type type memory_type = MemoryType of Int32.t limits type global_type = GlobalType of value_type * mutability -type segment_type = PassiveType | ActiveType type extern_type = | ExternFuncType of func_type | ExternTableType of table_type diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml index d8c33a1a..eeb198d3 100644 --- a/interpreter/util/lib.ml +++ b/interpreter/util/lib.ml @@ -125,6 +125,11 @@ struct | 0l, _ -> xs | n, _::xs' when n > 0l -> drop (Int32.sub n 1l) xs' | _ -> failwith "drop" + + let rec mapi f xs = mapi' f 0l xs + and mapi' f i = function + | [] -> [] + | x::xs -> f i x :: mapi' f (Int32.add i 1l) xs end module Array32 = diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli index de24c295..a152e6e4 100644 --- a/interpreter/util/lib.mli +++ b/interpreter/util/lib.mli @@ -30,6 +30,7 @@ sig val nth : 'a list -> int32 -> 'a (* raises Failure *) val take : int32 -> 'a list -> 'a list (* raises Failure *) val drop : int32 -> 'a list -> 'a list (* raises Failure *) + val mapi : (int32 -> 'a -> 'b) -> 'a list -> 'b list end module Array32 : diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 1a33d35d..76e0d715 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -21,8 +21,8 @@ type context = tables : table_type list; memories : memory_type list; globals : global_type list; - datas : segment_type list; - elems : segment_type list; + datas : unit list; + elems : unit list; locals : value_type list; results : value_type list; labels : stack_type list; @@ -493,11 +493,6 @@ let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t = require (not (NameSet.mem name set)) ex.at "duplicate export name"; NameSet.add name set -let segment_type mode = - match mode.it with - | Passive -> PassiveType - | Active _ -> ActiveType - let check_module (m : module_) = let { types; imports; tables; memories; globals; funcs; start; elems; datas; @@ -512,8 +507,8 @@ let check_module (m : module_) = funcs = c0.funcs @ List.map (fun f -> type_ c0 f.it.ftype) funcs; tables = c0.tables @ List.map (fun tab -> tab.it.ttype) tables; memories = c0.memories @ List.map (fun mem -> mem.it.mtype) memories; - elems = List.map (fun elem -> segment_type elem.it.emode) elems; - datas = List.map (fun data -> segment_type data.it.dmode) datas; + elems = List.map (fun _ -> ()) elems; + datas = List.map (fun _ -> ()) datas; } in let c = diff --git a/test/core/data.wast b/test/core/data.wast index bc94a8f2..80a2704e 100644 --- a/test/core/data.wast +++ b/test/core/data.wast @@ -158,28 +158,28 @@ ;; Invalid bounds for data -(assert_unlinkable +(assert_trap (module (memory 0) (data (i32.const 0) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 0 0) (data (i32.const 0) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 0 1) (data (i32.const 0) "a") ) - "data segment does not fit" + "out of bounds" ) ;; Writing 0 bytes outside of bounds is allowed now. @@ -199,77 +199,77 @@ (memory 0x10000) (data (i32.const 0xffffffff) "ab") ) - "" ;; either out of memory or segment does not fit + "" ;; either out of memory or out of bounds ;) -(assert_unlinkable +(assert_trap (module (global (import "spectest" "global_i32") i32) (memory 0) (data (global.get 0) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 1 2) (data (i32.const 0x1_0000) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "memory" (memory 1)) (data (i32.const 0x1_0000) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 2) (data (i32.const 0x2_0000) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 2 3) (data (i32.const 0x2_0000) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 1) (data (i32.const -1) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "memory" (memory 1)) (data (i32.const -1) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (memory 2) (data (i32.const -100) "a") ) - "data segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "memory" (memory 1)) (data (i32.const -100) "a") ) - "data segment does not fit" + "out of bounds" ) ;; Data without memory diff --git a/test/core/elem.wast b/test/core/elem.wast index 4dd3e782..7d2e4249 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -162,31 +162,31 @@ ;; Invalid bounds for elements -(assert_unlinkable +(assert_trap (module (table 0 funcref) (func $f) (elem (i32.const 0) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (table 0 0 funcref) (func $f) (elem (i32.const 0) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (table 0 1 funcref) (func $f) (elem (i32.const 0) $f) ) - "elements segment does not fit" + "out of bounds" ) ;; Writing 0 elems outside of bounds is allowed now. @@ -195,72 +195,72 @@ (elem (i32.const 1)) ) -(assert_unlinkable +(assert_trap (module (table 10 funcref) (func $f) (elem (i32.const 10) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "table" (table 10 funcref)) (func $f) (elem (i32.const 10) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (table 10 20 funcref) (func $f) (elem (i32.const 10) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "table" (table 10 funcref)) (func $f) (elem (i32.const 10) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (table 10 funcref) (func $f) (elem (i32.const -1) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "table" (table 10 funcref)) (func $f) (elem (i32.const -1) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (table 10 funcref) (func $f) (elem (i32.const -10) $f) ) - "elements segment does not fit" + "out of bounds" ) -(assert_unlinkable +(assert_trap (module (import "spectest" "table" (table 10 funcref)) (func $f) (elem (i32.const -10) $f) ) - "elements segment does not fit" + "out of bounds" ) ;; Element without table diff --git a/test/core/linking.wast b/test/core/linking.wast index 5edb6eb8..2d92078f 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -203,13 +203,13 @@ ) (assert_return (get $G2 "g") (i32.const 5)) -(assert_unlinkable +(assert_trap (module (table (import "Mt" "tab") 0 funcref) (elem (i32.const 10) $f) (func $f) ) - "elements segment does not fit" + "out of bounds" ) (assert_unlinkable @@ -226,26 +226,26 @@ ;; Unlike in the v1 spec, the elements stored before an out-of-bounds access ;; persist after the instantiation failure. -(assert_unlinkable +(assert_trap (module (table (import "Mt" "tab") 10 funcref) (func $f (result i32) (i32.const 0)) (elem (i32.const 7) $f) (elem (i32.const 12) $f) ;; out of bounds ) - "elements segment does not fit" + "out of bounds" ) (assert_return (invoke $Mt "call" (i32.const 7)) (i32.const 0)) -(assert_unlinkable +(assert_trap (module (table (import "Mt" "tab") 10 funcref) (func $f (result i32) (i32.const 0)) (elem (i32.const 7) $f) (memory 1) - (data (i32.const 0x10000) "d") ;; out of bounds + (data (i32.const 0x10000) "d") ;; out of bounds ) - "data segment does not fit" + "out of bounds" ) (assert_return (invoke $Mt "call" (i32.const 7)) (i32.const 0)) @@ -297,12 +297,12 @@ (data (i32.const 0xffff) "a") ) -(assert_unlinkable +(assert_trap (module (memory (import "Mm" "mem") 0) (data (i32.const 0x10000) "a") ) - "data segment does not fit" + "out of bounds" ) (module $Pm @@ -335,25 +335,25 @@ ;; Unlike in v1 spec, bytes written before an out-of-bounds access persist ;; after the instantiation failure. -(assert_unlinkable +(assert_trap (module (memory (import "Mm" "mem") 1) (data (i32.const 0) "abc") (data (i32.const 0x50000) "d") ;; out of bounds ) - "data segment does not fit" + "out of bounds" ) (assert_return (invoke $Mm "load" (i32.const 0)) (i32.const 97)) -(assert_unlinkable +(assert_trap (module (memory (import "Mm" "mem") 1) (data (i32.const 0) "abc") (table 0 funcref) (func) - (elem (i32.const 0) 0) ;; out of bounds + (elem (i32.const 0) 0) ;; out of bounds ) - "elements segment does not fit" + "out of bounds" ) (assert_return (invoke $Mm "load" (i32.const 0)) (i32.const 97))