diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 9956e528..76e47b74 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -286,8 +286,6 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: element instance, reference .. _valid-eleminst: -.. todo:: TODO: adjust elem instances - :ref:`Element Instances ` :math:`\{ \EIELEM~\X{fa}^\ast \}` ............................................................................ @@ -303,7 +301,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \frac{ (S \vdash \reff : t')^\ast \qquad - (\vdashreftypematch t' \matchesvaltype t)^n + (\vdashreftypematch t' \matchesvaltype t)^\ast }{ S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok } diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst index 3e14d8e8..807239b0 100644 --- a/document/core/exec/conventions.rst +++ b/document/core/exec/conventions.rst @@ -33,7 +33,7 @@ The following conventions are adopted in stating these rules. * The execution rules also assume the presence of an implicit :ref:`stack ` that is modified by *pushing* or *popping* - :ref:`values `, :ref:`function elements `, :ref:`labels `, and :ref:`frames `. + :ref:`values `, :ref:`labels `, and :ref:`frames `. * Certain rules require the stack to contain at least one frame. The most recent frame is referred to as the *current* frame. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ffad9cb3..1b118125 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -633,11 +633,11 @@ Table Instructions 2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. -3. Let :math:`a` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. +3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. -4. Assert: due to :ref:`validation `, :math:`S.\STABLES[a]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}]` exists. -5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. +5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. 6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. @@ -693,50 +693,56 @@ Table Instructions .. _exec-table.copy: -:math:`\TABLECOPY` -.................. - -.. todo:: TODO: multi tables +:math:`\TABLECOPY~x~y` +...................... 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. -3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. +3. Let :math:`\X{ta}_x` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. -4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}_x]` exists. -5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. +5. Let :math:`\X{tab}_x` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_x]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[y]` exists. -7. Pop the value :math:`\I32.\CONST~n` from the stack. +7. Let :math:`\X{ta}_y` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[y]`. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}_y]` exists. -9. Pop the value :math:`\I32.\CONST~s` from the stack. +9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. 10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -11. Pop the value :math:`\I32.\CONST~d` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. + +12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. + +13. Pop the value :math:`\I32.\CONST~s` from the stack. -12. If :math:`s + n` is larger than the length of :math:`\X{tab}.\TIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +14. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. + +15. Pop the value :math:`\I32.\CONST~d` from the stack. + +16. If :math:`s + n` is larger than the length of :math:`\X{tab}_y.\TIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}_x.\TIELEM`, then: a. Trap. -13. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -14. If :math:`d \leq s`, then: +18. If :math:`d \leq s`, then: a. Push the value :math:`\I32.\CONST~d` to the stack. b. Push the value :math:`\I32.\CONST~s` to the stack. - c. Execute the instruction :math:`\TABLEGET`. + c. Execute the instruction :math:`\TABLEGET~y`. - d. Execute the instruction :math:`\TABLESET`. + d. Execute the instruction :math:`\TABLESET~x`. e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. @@ -746,7 +752,7 @@ Table Instructions h. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -15. Else: +19. Else: a. Assert: due to the earlier check against the table size, :math:`d+n-1 < 2^{32}`. @@ -756,48 +762,48 @@ Table Instructions d. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - c. Execute the instruction :math:`\TABLEGET`. + c. Execute the instruction :math:`\TABLEGET~y`. - f. Execute the instruction :math:`\TABLESET`. + f. Execute the instruction :math:`\TABLESET~x`. g. Push the value :math:`\I32.\CONST~d` to the stack. h. Push the value :math:`\I32.\CONST~s` to the stack. -16. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +20. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -17. Execute the instruction :math:`\TABLECOPY`. +21. Execute the instruction :math:`\TABLECOPY~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\TABLECOPY + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & s + n > |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM| \\ - \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM|) \\ + (\iff & s + n > |S.\STABLES[F.\AMODULE.\MITABLES[y]].\TIELEM| \\ + \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\ \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\TABLECOPY + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\TABLECOPY + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~(\I32.\CONST~s)~\TABLEGET~\TABLESET \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~\TABLECOPY \\ + (\I32.\CONST~d)~(\I32.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\TABLECOPY + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~\TABLEGET~\TABLESET \\ - (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\TABLECOPY \\ + (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -806,24 +812,22 @@ Table Instructions .. _exec-table.init: -:math:`\TABLEINIT~x` -.................... - -.. todo:: TODO: multi tables +:math:`\TABLEINIT~x~y` +...................... 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[x]` exists. -3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. +3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[x]`. 4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}]` exists. 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. -7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[x]`. +7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. 8. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. @@ -849,13 +853,13 @@ Table Instructions a. Return. -18. Let :math:`\funcelem` be the :ref:`function element ` :math:`\X{elem}.\EIELEM[s]`. +18. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. 19. Push the value :math:`\I32.\CONST~d` to the stack. -20. Push the value :math:`\funcelem` to the stack. +20. Push the value :math:`\val` to the stack. -21. Execute the instruction :math:`\TABLESET`. +21. Execute the instruction :math:`\TABLESET~x`. 22. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. @@ -867,32 +871,32 @@ Table Instructions 26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -27. Execute the instruction :math:`\TABLEINIT~x`. +27. Execute the instruction :math:`\TABLEINIT~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM| \\ + (\iff & s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM| \\ \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\ \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~\funcelem~(\TABLESET~x) \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x) \\ + (\I32.\CONST~d)~\val~(\TABLESET~x) \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff \funcelem = S.\SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM[s]) \\ + (\otherwise, \iff \val = S.\SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM[s]) \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 1211356d..002964b9 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -630,21 +630,21 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 6. Let :math:`(\reff^\ast)^\ast` be the list of :ref:`reference ` vectors determined by the :ref:`element segments ` in :math:`\module`. These may be calculated as follows. - .. todo:: TODO desugar funcelem + a. Let :math:`\moduleinst_{\F{im}}` be the auxiliary module :ref:`instance ` :math:`\{\MIGLOBALS~\evglobals(\externval^n)\}` that only consists of the imported globals. - a. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, and for each element :ref:`expression ` :math:`\expr_{ij}` in :math:`\elem_i.\EINIT`, do: + b. Let :math:`F_{\F{im}}` be the auxiliary :ref:`frame ` :math:`\{ \AMODULE~\moduleinst_{\F{im}}, \ALOCALS~\epsilon \}`. - i. If :math:`\expr_{ij}` is of the form :math:`\REFNULL`, then let the :ref:`function element ` :math:`\funcelem_{ij}` be :math:`\epsilon`. + c. Push the frame :math:`F_{\F{im}}` to the stack. - ii. Else, :math:`\expr_{ij}` is of the form is :math:`\REFFUNC~\funcidx_{ij}`. + d. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, and for each element :ref:`expression ` :math:`\expr_{ij}` in :math:`\elem_i.\EINIT`, do: - iii. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]` exists. + i. Let :math:`\reff_{ij}` be the result of :ref:`evaluating ` the initializer expression :math:`\expr_{ij}`. - iv. Let the :ref:`function element ` :math:`\funcelem_{ij}` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`. + e. Pop the frame :math:`F_{\F{im}}` from the stack. - b. Let :math:`\funcelem^\ast_i` be the concatenation of function elements :math:`\funcelem_{ij}` in order of index :math:`j`. + f. Let :math:`\reff^\ast_i` be the concatenation of function elements :math:`\reff_{ij}` in order of index :math:`j`. - 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:`(\reff^\ast)^\ast` be the concatenation of function element vectors :math:`\reff^\ast_i` in order of index :math:`i`. 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:`(\reff^\ast)^\ast`, and let :math:`S'` be the extended store produced by module allocation. @@ -711,10 +711,13 @@ It is up to the :ref:`embedder ` to define how such conditions are rep &\wedge& \module.\MGLOBALS = \global^\ast \\ &\wedge& \module.\MELEMS = \elem^n \\ &\wedge& \module.\MDATAS = \data^m \\ - &\wedge& \module.\MSTART = \start^? \\[1ex] - &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^k, \val^\ast) \\ + &\wedge& \module.\MSTART = \start^? \\ + &\wedge& (\expr_{\F{g}} = \global.GINIT)^\ast \\ + &\wedge& (\expr_{\F{e}}^\ast = \elem.EINIT)^n \\[1ex] + &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^k, \val^\ast, (\reff^\ast)^n) \\ &\wedge& F = \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \} \\[1ex] - &\wedge& (S'; F; \global.\GINIT \stepto^\ast S'; F; \val~\END)^\ast \\ + &\wedge& (S'; F; \expr_{\F{g}} \stepto^\ast S'; F; \val~\END)^\ast \\ + &\wedge& ((S'; F; \expr_{\F{e}} \stepto^\ast S'; F; \reff~\END)^\ast)^n \\ &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\ &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\ &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^?) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 594255be..851b088e 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -258,7 +258,6 @@ but within certain :ref:`constraints ` that ensure the integri .. index:: ! table instance, table, function address, table type, embedder, element segment pair: abstract syntax; table instance pair: table; instance -.. _syntax-funcelem: .. _syntax-tableinst: Table Instances @@ -340,7 +339,7 @@ It holds a vector of references and their common :ref:`type `. .. math:: \begin{array}{llll} \production{(element instance)} & \eleminst &::=& - \{ \EITYPE~\reftype, \EIELEM~\vec(\funcelem) \} \\ + \{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\ \end{array} diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 8dfddabb..dad0d02e 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -215,12 +215,30 @@ Table Instructions \text{table.size}~~x{:}\Ttableidx_I &\Rightarrow& \TABLESIZE~x \\ &&|& \text{table.grow}~~x{:}\Ttableidx_I &\Rightarrow& \TABLEGROW~x \\ &&|& \text{table.fill}~~x{:}\Ttableidx_I &\Rightarrow& \TABLEFILL~x \\ - \text{table.copy} &\Rightarrow& \TABLECOPY \\ &&|& - \text{table.init}~~x{:}\Telemidx_I &\Rightarrow& \TABLEINIT~x \\ &&|& + \text{table.copy}~~x{:}\Ttableidx_I~~y{:}\Ttableidx_I &\Rightarrow& \TABLECOPY~x~y \\ &&|& + \text{table.init}~~x{:}\Ttableidx_I~~y{:}\Telemidx_I &\Rightarrow& \TABLEINIT~x~y \\ &&|& \text{elem.drop}~~x{:}\Telemidx_I &\Rightarrow& \ELEMDROP~x \\ \end{array} +Abbreviations +............. + +For backwards compatibility, all :math:`table indices ` may be omitted from table instructions, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{instruction} & + \text{table.get} &\equiv& \text{table.get}~~\text{0} \\ &&|& + \text{table.set} &\equiv& \text{table.set}~~\text{0} \\ &&|& + \text{table.size} &\equiv& \text{table.size}~~\text{0} \\ &&|& + \text{table.grow} &\equiv& \text{table.grow}~~\text{0} \\ &&|& + \text{table.fill} &\equiv& \text{table.fill}~~\text{0} \\ &&|& + \text{table.copy} &\equiv& \text{table.copy}~~\text{0}~~\text{0} \\ &&|& + \text{table.init}~~x{:}\Telemidx_I &\equiv& \text{table.init}~~\text{0}~~x{:}\Telemidx_I \\ &&|& + \end{array} + + .. index:: memory instruction, memory index pair: text format; instruction .. _text-instr-memory: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 57f4c630..ac61429a 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -505,7 +505,7 @@ Element segments allow for an optional :ref:`table index ` to ide \production{element list} & \Telemlist &::=& t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ \production{element expression} & \Telemexpr &::=& - \text{(}~e{:}\Tinstr~\text{)} + \text{(}~\text{item}~~e{:}\Texpr~\text{)} \quad\Rightarrow\quad e \\ \production{table use} & \Ttableuse_I &::=& \text{(}~\text{table}~~x{:}\Ttableidx_I ~\text{)} @@ -516,13 +516,16 @@ Element segments allow for an optional :ref:`table index ` to ide Abbreviations ............. -As an abbreviation, a single instruction may occur in place of the offset of an active element segment: +As an abbreviation, a single instruction may occur in place of the offset of an active element segment or as an element expression: .. math:: \begin{array}{llcll} \production{element offset} & \Tinstr &\equiv& - \text{(}~\text{offset}~~\Tinstr~\text{)} + \text{(}~\text{offset}~~\Tinstr~\text{)} \\ + \production{element item} & + \Tinstr &\equiv& + \text{(}~\text{item}~~\Tinstr~\text{)} \\ \end{array} Also, the element list may be written as just a sequence of :ref:`function indices `: @@ -534,7 +537,7 @@ Also, the element list may be written as just a sequence of :ref:`function indic \text{funcref}~~\Tvec(\text{(}~\text{ref.func}~~\Tfuncidx_I~\text{)}) \end{array} -Also, a table use can be omitted, defaulting to :math:`\T{0}`. +A table use can be omitted, defaulting to :math:`\T{0}`. Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the :math:`\text{func}` keyword can be omitted as well. .. math:: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 87b5ca28..f2ad64f3 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -903,7 +903,6 @@ .. |moduleinst| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\X{moduleinst}} .. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}} .. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}} -.. |funcelem| mathdef:: \xref{exec/runtime}{syntax-funcelem}{\X{funcelem}} .. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}} .. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}} .. |eleminst| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\X{eleminst}} diff --git a/interpreter/README.md b/interpreter/README.md index f38f5720..4a1c937e 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -216,7 +216,7 @@ op: br_table + return call - call_indirect + call_indirect ? drop select local.get @@ -224,13 +224,13 @@ op: local.tee global.get global.set - table.get - table.set - table.size - table.grow - table.fill - table.copy - table.init + table.get ? + table.set ? + table.size ? + table.grow ? + table.fill ? + table.copy ? ? + table.init ? elem.drop .load((8|16|32)_)? ? ? .store(8|16|32)? ? ? @@ -263,15 +263,18 @@ global: ( global ? * ) table: ( table ? ) ( table ? ( export ) <...> ) ;; = (export (table )) (table ? <...>) ( table ? ( import ) ) ;; = (import ? (table )) - ( table ? ( export )* ( elem * ) ) ;; = (table ? ( export )* ) (elem (i32.const 0) *) -elem: ( elem ? (offset * ) * ) - ( elem ? * ) ;; = (elem ? (offset ) *) + ( table ? ( export )* ( elem * ) ) ;; = (table ? ( export )* ) (elem (i32.const 0) *) +elem: ( elem ? ( table )? * ) + ( elem ? ( table )? func * ) ;; = (elem ? ( table )? funcref (ref.func )*) +offset: ( offset * ) + ;; = ( offset ) +item: ( item * ) + ;; = ( item ) memory: ( memory ? ) ( memory ? ( export ) <...> ) ;; = (export (memory ))+ (memory ? <...>) ( memory ? ( import ) ) ;; = (import ? (memory )) ( memory ? ( export )* ( data * ) ) ;; = (memory ? ( export )* ) (data (i32.const 0) *) -data: ( data ? ( offset * ) * ) - ( data ? * ) ;; = (data ? (offset ) *) +data: ( data ? ( memory )? * ) start: ( start ) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 7a9039fe..8fc03360 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -57,6 +57,7 @@ type code = value stack * admin_instr list and admin_instr = admin_instr' phrase and admin_instr' = | Plain of instr' + | Refer of ref_ | Invoke of func_inst | Trapping of string | Returning of value stack @@ -240,20 +241,43 @@ let rec step (c : config) : config = vs', [] else let _ = assert (I32.lt_u i 0xffff_ffffl) in - Ref r :: Num (I32 i) :: Num (I32 (I32.sub n 1l)) :: - Ref r :: Num (I32 (I32.add i 1l)) :: vs', - [Plain (TableSet x) @@ e.at; Plain (TableFill x) @@ e.at] + vs', List.map (at e.at) [ + Plain (Const (I32 i @@ e.at)); + Refer r; + Plain (TableSet x); + Plain (Const (I32 (I32.add i 1l) @@ e.at)); + Refer r; + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); + Plain (TableFill x); + ] | TableCopy (x, y), Num (I32 n) :: Num (I32 s) :: Num (I32 d) :: vs' -> if table_oob frame x d n || table_oob frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n = 0l then vs', [] - else - (* TODO: turn into small-step, but needs reference values *) - let tab = table frame.inst x in (*TODO*) - (try Table.copy tab d s n; vs', [] - with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) + else if d <= s then + vs', List.map (at e.at) [ + Plain (Const (I32 d @@ e.at)); + Plain (Const (I32 s @@ e.at)); + Plain (TableGet y); + Plain (TableSet x); + Plain (Const (I32 (I32.add d 1l) @@ e.at)); + Plain (Const (I32 (I32.add s 1l) @@ e.at)); + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); + Plain (TableCopy (x, y)); + ] + else (* d > s *) + vs', List.map (at e.at) [ + Plain (Const (I32 (I32.add d 1l) @@ e.at)); + Plain (Const (I32 (I32.add s 1l) @@ e.at)); + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); + Plain (TableCopy (x, y)); + Plain (Const (I32 d @@ e.at)); + Plain (Const (I32 s @@ e.at)); + Plain (TableGet y); + Plain (TableSet x); + ] | TableInit (x, y), Num (I32 n) :: Num (I32 s) :: Num (I32 d) :: vs' -> if table_oob frame x d n || elem_oob frame y s n then @@ -261,11 +285,16 @@ let rec step (c : config) : config = else if n = 0l then vs', [] else - (* TODO: turn into small-step, but needs reference values *) - let tab = table frame.inst x in let seg = !(elem frame.inst y) in - (try Table.init tab seg d s n; vs', [] - with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) + vs', List.map (at e.at) [ + Plain (Const (I32 d @@ e.at)); + Refer (List.nth seg (Int32.to_int s)); + Plain (TableSet x); + Plain (Const (I32 (I32.add d 1l) @@ e.at)); + Plain (Const (I32 (I32.add s 1l) @@ e.at)); + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); + Plain (TableInit (x, y)); + ] | ElemDrop x, vs -> let seg = elem frame.inst x in @@ -421,6 +450,9 @@ let rec step (c : config) : config = ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")") ) + | Refer r, vs -> + Ref r :: vs, [] + | Trapping msg, vs -> assert false diff --git a/interpreter/runtime/table.ml b/interpreter/runtime/table.ml index 811edcff..8da0090e 100644 --- a/interpreter/runtime/table.ml +++ b/interpreter/runtime/table.ml @@ -58,26 +58,3 @@ let blit tab offset rs = let data = Array.of_list rs in try Lib.Array32.blit data 0l tab.content offset (Lib.Array32.length data) with Invalid_argument _ -> raise Bounds - -(*TODO: remove*) -let init tab es d s n = - let rec loop es d s n = - match s, n, es with - | s, 0l, _ -> () - | 0l, n, e::es' -> - store tab d e; - loop es' (Int32.add d 1l) 0l (Int32.sub n 1l) - | s, n, _::es' -> loop es' d (Int32.sub s 1l) n - | _ -> raise Bounds - in loop es d s n - -let copy tab d s n = - let rec loop d s n dx = - if I32.gt_u n 0l then begin - store tab d (load tab s); - loop (Int32.add d dx) (Int32.add s dx) (Int32.sub n 1l) dx - end - in (if s < d then - loop Int32.(add d (sub n 1l)) Int32.(add s (sub n 1l)) n (-1l) - else - loop d s n 1l) diff --git a/interpreter/runtime/table.mli b/interpreter/runtime/table.mli index dcc28f68..cf424e35 100644 --- a/interpreter/runtime/table.mli +++ b/interpreter/runtime/table.mli @@ -23,8 +23,3 @@ val grow : table -> size -> ref_ -> unit val load : table -> index -> ref_ (* raises Bounds *) val store : table -> index -> ref_ -> unit (* raises Type, Bounds *) val blit : table -> index -> ref_ list -> unit (* raises Bounds *) - -(*TODO: remove*) -val init : - table -> ref_ list -> index -> index -> count -> unit (* raises Bounds *) -val copy : table -> index -> index -> count -> unit (* raises Bounds *) diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 5926bffd..79181e80 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -63,7 +63,7 @@ type storeop = Memory.pack_size memop (* Expressions *) type var = int32 Source.phrase -type literal = Values.num Source.phrase +type num = Values.num Source.phrase type name = int list type instr = instr' Source.phrase @@ -105,7 +105,7 @@ and instr' = | RefNull (* null reference *) | RefIsNull (* null test *) | RefFunc of var (* function reference *) - | Const of literal (* constant *) + | Const of num (* constant *) | Test of testop (* numeric test *) | Compare of relop (* numeric comparison *) | Unary of unop (* unary numeric operator *) diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 72420679..ce32cc62 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -251,8 +251,8 @@ let rec instr e = | TableSize x -> "table.size " ^ var x, [] | TableGrow x -> "table.grow " ^ var x, [] | TableFill x -> "table.fill " ^ var x, [] - | TableCopy (x, y) -> "table.copy", [] (*TODO*) - | TableInit (x, y) -> "table.init " ^ var y, [] (*TODO*) + | TableCopy (x, y) -> "table.copy " ^ var x ^ " " ^ var y, [] + | TableInit (x, y) -> "table.init " ^ var x ^ " " ^ var y, [] | ElemDrop x -> "elem.drop " ^ var x, [] | Load op -> loadop op, [] | Store op -> storeop op, [] @@ -265,7 +265,7 @@ let rec instr e = | RefNull -> "ref.null", [] | RefIsNull -> "ref.is_null", [] | RefFunc x -> "ref.func " ^ var x, [] - | Const lit -> constop lit ^ " " ^ num lit, [] + | Const n -> constop n ^ " " ^ num n, [] | Test op -> testop op, [] | Compare op -> relop op, [] | Unary op -> unop op, [] diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 9511a8e3..a74a4431 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -349,6 +349,7 @@ rule token = parse | "elem" { ELEM } | "data" { DATA } | "offset" { OFFSET } + | "item" { ITEM } | "import" { IMPORT } | "export" { EXPORT } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 2f36c3f5..8220539a 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -36,7 +36,7 @@ let ati i = (* Literals *) -let literal f s = +let num f s = try f s with Failure _ -> error s.at "constant out of range" let nanop f nan = @@ -176,7 +176,7 @@ let inline_type_explicit (c : context) x ft at = %token CONST UNARY BINARY TEST COMPARE CONVERT %token REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL -%token TABLE ELEM MEMORY DATA OFFSET IMPORT EXPORT +%token TABLE ELEM MEMORY DATA OFFSET ITEM IMPORT EXPORT %token MODULE BIN QUOTE %token SCRIPT REGISTER INVOKE GET %token ASSERT_MALFORMED ASSERT_INVALID ASSERT_SOFT_INVALID ASSERT_UNLINKABLE @@ -274,7 +274,7 @@ type_use : /* Immediates */ -literal : +num : | NAT { $1 @@ at () } | INT { $1 @@ at () } | FLOAT { $1 @@ at () } @@ -352,9 +352,17 @@ plain_instr : | TABLE_SIZE var { fun c -> table_size ($2 c table) } | TABLE_GROW var { fun c -> table_grow ($2 c table) } | TABLE_FILL var { fun c -> table_fill ($2 c table) } - | TABLE_COPY { let at = ati 1 in fun c -> table_copy (0l @@ at) (0l @@ at) } - | TABLE_INIT var /*TODO*/ - { let at = ati 1 in fun c -> table_init (0l @@ at) ($2 c elem) } + | TABLE_COPY var var { fun c -> table_copy ($2 c table) ($3 c table) } + | TABLE_INIT var var { fun c -> table_init ($2 c table) ($3 c elem) } + | TABLE_GET { let at = at () in fun c -> table_get (0l @@ at) } /* Sugar */ + | TABLE_SET { let at = at () in fun c -> table_set (0l @@ at) } /* Sugar */ + | TABLE_SIZE { let at = at () in fun c -> table_size (0l @@ at) } /* Sugar */ + | TABLE_GROW { let at = at () in fun c -> table_grow (0l @@ at) } /* Sugar */ + | TABLE_FILL { let at = at () in fun c -> table_fill (0l @@ at) } /* Sugar */ + | TABLE_COPY /* Sugar */ + { let at = at () in fun c -> table_copy (0l @@ at) (0l @@ at) } + | TABLE_INIT var /* Sugar */ + { let at = at () in fun c -> table_init (0l @@ at) ($2 c elem) } | ELEM_DROP var { fun c -> elem_drop ($2 c elem) } | LOAD offset_opt align_opt { fun c -> $1 $3 $2 } | STORE offset_opt align_opt { fun c -> $1 $3 $2 } @@ -367,7 +375,7 @@ plain_instr : | REF_NULL { fun c -> ref_null } | REF_IS_NULL { fun c -> ref_is_null } | REF_FUNC var { fun c -> ref_func ($2 c func) } - | CONST literal { fun c -> fst (literal $1 $2) } + | CONST num { fun c -> fst (num $1 $2) } | TEST { fun c -> $1 } | COMPARE { fun c -> $1 } | UNARY { fun c -> $1 } @@ -648,7 +656,7 @@ elem_kind : | FUNC { FuncRefType } elem_expr : - /* TODO: | LPAR ITEM const_expr RPAR { $3 } */ + | LPAR ITEM const_expr RPAR { $3 } | expr { let at = at () in fun c -> $1 c @@ at } /* Sugar */ elem_expr_list : @@ -733,16 +741,16 @@ data : { let at = at () in fun c -> ignore ($3 c anon_data bind_data); fun () -> {dinit = $4; dmode = Passive @@ at} @@ at } - | LPAR DATA bind_var_opt memory_use offset string_list RPAR - { let at = at () in - fun c -> ignore ($3 c anon_data bind_data); - fun () -> - {dinit = $6; dmode = Active {index = $4 c memory; offset = $5 c} @@ at} @@ at } - | LPAR DATA bind_var_opt offset string_list RPAR /* Sugar */ - { let at = at () in - fun c -> ignore ($3 c anon_data bind_data); - fun () -> - {dinit = $5; dmode = Active {index = 0l @@ at; offset = $4 c} @@ at} @@ at } + | LPAR DATA bind_var_opt memory_use offset string_list RPAR + { let at = at () in + fun c -> ignore ($3 c anon_data bind_data); + fun () -> + {dinit = $6; dmode = Active {index = $4 c memory; offset = $5 c} @@ at} @@ at } + | LPAR DATA bind_var_opt offset string_list RPAR /* Sugar */ + { let at = at () in + fun c -> ignore ($3 c anon_data bind_data); + fun () -> + {dinit = $5; dmode = Active {index = 0l @@ at; offset = $4 c} @@ at} @@ at } memory : | LPAR MEMORY bind_var_opt memory_fields RPAR @@ -972,7 +980,7 @@ meta : | LPAR OUTPUT script_var_opt RPAR { Output ($3, None) @@ at () } const : - | LPAR CONST literal RPAR { Values.Num (snd (literal $2 $3)) @@ at () } + | LPAR CONST num RPAR { Values.Num (snd (num $2 $3)) @@ at () } | LPAR REF_NULL RPAR { Values.Ref Values.NullRef @@ at () } | LPAR REF_HOST NAT RPAR { Values.Ref (HostRef (nat32 $3 (ati 3))) @@ at () } diff --git a/proposals/reference-types/Overview.md b/proposals/reference-types/Overview.md index e0511129..8e35ab71 100644 --- a/proposals/reference-types/Overview.md +++ b/proposals/reference-types/Overview.md @@ -117,6 +117,8 @@ New/extended instructions: - and `$x : table t'` - and `t' <: funcref` +* In all instructions, table indices can be omitted and default to 0. + Note: - In the binary format, space for the additional table indices is already reserved. - For backwards compatibility, all table indices may be omitted in the text format, in which case they default to 0 (for `table.copy`, both indices must be either present or absent). diff --git a/test/core/elem.wast b/test/core/elem.wast index bb622ee6..b594acd6 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -8,7 +8,7 @@ ;; Passive (elem funcref) - (elem funcref (ref.func $f) (ref.func $f) (ref.null) (ref.func $g)) + (elem funcref (ref.func $f) (item ref.func $f) (item (ref.null)) (ref.func $g)) (elem func) (elem func $f $f $g $g)