From ed1fc5324b18cf709d076aa18378eaa398d5e816 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 6 Nov 2024 14:58:13 -0800 Subject: [PATCH 1/3] Update appendix for memory64 (#97) Split out from https://github.com/WebAssembly/spec/pull/1839 --- document/core/appendix/changes.rst | 41 ++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index 352bc504a9..e5ffa79ae3 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -389,6 +389,44 @@ Added the ability to use multiple memories per module. [#proposal-multimem]_ * :ref:`Data segments ` take a :ref:`memory index ` +.. index:: address type, number type, table, memory, instruction + +64-bit Address Space +.................... + +Added the ability to declare an :math:`\I64` :ref:`address type ` for :ref:`tables ` and :ref:`memories `. [#proposal-addr64]_ + +* :ref:`Address types ` denote a subset of the integral :ref:`number types ` + +* :ref:`Table types ` include an :ref:`address type ` + +* :ref:`Memory types ` include an :ref:`address type ` + +* Operand types of :ref:`table ` and :ref:`memory ` instructions now depend on the subject's declared address type: + + - |TABLEGET| + - |TABLESET| + - |TABLESIZE| + - |TABLEGROW| + - |TABLEFILL| + - |TABLECOPY| + - |TABLEINIT| + - |MEMORYSIZE| + - |MEMORYGROW| + - |MEMORYFILL| + - |MEMORYCOPY| + - |MEMORYINIT| + - :math:`t\K{.load}` + - :math:`t\K{.store}` + - :math:`t\K{.load}\!N\!\K{\_}\sx` + - :math:`t\K{.store}\!N` + - :math:`\K{v128.load}\!N\!\K{x}\!M\!\K{\_}\sx` + - :math:`\K{v128.load}\!N\!\K{\_zero}` + - :math:`\K{v128.load}\!N\!\K{\_splat}` + - :math:`\K{v128.load}\!N\!\K{\_lane}` + - :math:`\K{v128.store}\!N\!\K{\_lane}` + + .. index:: reference, reference type, heap type, value type, local, local type, instruction, instruction type, table, function, function type, matching, subtyping Typeful References @@ -595,6 +633,9 @@ mirroring the role of custom sections in the binary format. [#proposal-annot]_ .. [#proposal-multimem] https://github.com/WebAssembly/spec/blob/main/proposals/multi-memory/ +.. [#proposal-addr64] + https://github.com/WebAssembly/spec/blob/main/proposals/memory64/ + .. [#proposal-typedref] https://github.com/WebAssembly/spec/tree/main/proposals/function-references/ From ace09470a6aab8e31710c6835a70a344cbec051b Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 6 Nov 2024 14:58:53 -0800 Subject: [PATCH 2/3] Memory64 spec tweaks and fixes from @rossberg (#98) - Removed unnecessary/mismatching lookup of table/memory type in execution prose - Added missing result type lookup in formal rule for table.size and memory.size - Fixed computation of -1 result value for table.grow and table.size to work for i64 - Some fixes around specification of text format for inline elements/data shorthand - Fixed matching rules for tabletype/memtype to enforce same address type Split out from https://github.com/WebAssembly/spec/pull/1839 --- document/core/binary/types.rst | 6 +- document/core/exec/instructions.rst | 420 ++++++++++++--------------- document/core/syntax/types.rst | 13 +- document/core/text/modules.rst | 29 +- document/core/valid/instructions.rst | 8 +- document/core/valid/matching.rst | 8 +- 6 files changed, 217 insertions(+), 267 deletions(-) diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index d5501ec487..3ab538a09d 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -251,7 +251,7 @@ Additional shorthands are recognized for unary recursions and sub types without Limits ~~~~~~ -:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and the corresponding :ref:`address type `. +:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and a flag for the :ref:`address type `. .. math:: \begin{array}{llclll} @@ -275,7 +275,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{memory type} & \Bmemtype &::=& - (\X{at}, \X{lim}){:}\Blimits &\Rightarrow& \X{at}~~\X{lim} \\ + (\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim} \\ \end{array} @@ -291,7 +291,7 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Btabletype &::=& - \X{et}{:}\Breftype~~(\X{at}, \X{lim}){:}\Blimits &\Rightarrow& \X{at}~~\X{lim}~\X{et} \\ + \X{et}{:}\Breftype~~(\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim}~\X{et} \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3a23b045e6..d6a16b84a3 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2725,19 +2725,17 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +8. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -10. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. +9. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. -11. Push the value :math:`\val` to the stack. +10. Push the value :math:`\val` to the stack. .. math:: ~\\[-1ex] @@ -2770,21 +2768,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +6. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -8. Pop the value :math:`\val` from the stack. +7. Pop the value :math:`\val` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -12. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. +11. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. .. math:: ~\\[-1ex] @@ -2829,7 +2825,10 @@ Table Instructions S; F; (\TABLESIZE~x) &\stepto& S; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad - (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\ + \begin{array}[t]{@{}r@{~}l@{}} + (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz} \\ + \wedge S.\STABLES[F.\AMODULE.\MITABLES[x]].\TITYPE = \X{at}~\X{lim}~t) + \end{array} \\ \end{array} @@ -2849,21 +2848,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. +6. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Pop the value :math:`t.\CONST~n` from the stack. -10. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +9. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -11. Pop the value :math:`\val` from the stack. +10. Pop the value :math:`\val` from the stack. -12. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +11. Let :math:`\X{err}` be the value :math:`2^{|\X{at}|}-1`, for which :math:`\signed_{|\X{at}|}(\X{err})` is :math:`-1`. -13. Either: +12. Either: a. If :ref:`growing ` :math:`\X{tab}` by :math:`n` entries with initialization value :math:`\val` succeeds, then: @@ -2873,7 +2870,7 @@ Table Instructions i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. -14. Or: +13. Or: a. push the value :math:`\X{at}.\CONST~\X{err}` to the stack. @@ -2891,7 +2888,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) + S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{|\X{at}|}^{-1}(-1)) \end{array} \end{array} @@ -2919,21 +2916,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Pop the value :math:`\X{at}.\CONST~n` from the stack. -8. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -9. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. - -10. Pop the value :math:`\val` from the stack. +9. Pop the value :math:`\val` from the stack. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`address type ` :math:`\X{at}` is on the top of the stack. -12. Pop the value :math:`\X{at}.\CONST~i` from the stack. +11. Pop the value :math:`\X{at}.\CONST~i` from the stack. -13. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +12. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. @@ -3004,25 +2999,19 @@ Table Instructions 9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. -10. Let :math:`\X{at}_x~\limits_x` be the :ref:`table type ` :math:`\X{tab}_x.\TITYPE`. - -11. Let :math:`\X{at}_y~\limits_y` be the :ref:`table type ` :math:`\X{tab}_y.\TITYPE`. - -12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_x` and :math:`\X{at}_y`. +10. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_n` is on the top of the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_n` is on the top of the stack. +11. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. +12. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_s` is on the top of the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_y` is on the top of the stack. +13. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. -16. Pop the value :math:`\X{at}_y.\CONST~s` from the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_d` is on the top of the stack. -17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_x` is on the top of the stack. +15. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. -18. Pop the value :math:`\X{at}_x.\CONST~d` from the stack. - -19. 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: +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. @@ -3032,9 +3021,9 @@ Table Instructions 21. If :math:`d \leq s`, then: - a. Push the value :math:`\X{at}_x.\CONST~d` to the stack. + a. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - b. Push the value :math:`\X{at}_y.\CONST~s` to the stack. + b. Push the value :math:`\X{at}_s.\CONST~s` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. @@ -3042,29 +3031,29 @@ Table Instructions e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\X{at}_x.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{at}_d.\CONST~(d+1)` to the stack. g. Assert: due to the earlier check against the table size, :math:`s+1 < 2^{32}`. - h. Push the value :math:`\X{at}_y.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{at}_s.\CONST~(s+1)` to the stack. 22. Else: a. Assert: due to the earlier check against the table size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\X{at}_x.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{at}_d.\CONST~(d+n-1)` to the stack. c. Assert: due to the earlier check against the table size, :math:`s+n-1 < 2^{32}`. - d. Push the value :math:`\X{at}_y.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{at}_s.\CONST~(s+n-1)` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. f. Execute the instruction :math:`\TABLESET~x`. - g. Push the value :math:`\X{at}_x.\CONST~d` to the stack. + g. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - h. Push the value :math:`\X{at}_y.\CONST~s` to the stack. + h. Push the value :math:`\X{at}_s.\CONST~s` to the stack. 23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. @@ -3073,7 +3062,7 @@ Table Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3081,27 +3070,27 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~0)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~0)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{at}_x.\CONST~d+1)~(\X{at}_y.\CONST~s+1)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{at}_d.\CONST~d+1)~(\X{at}_s.\CONST~s+1)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{at}_x.\CONST~d+n)~(\X{at}_y.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{at}_d.\CONST~d+n)~(\X{at}_s.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -3123,55 +3112,53 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. -8. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. +7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. -9. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. -10. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. +9. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\I32` is on the top of the stack. -12. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -14. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{at}.\CONST~d` from the stack. +15. Pop the value :math:`\X{at}.\CONST~d` from the stack. -17. If :math:`s + n` is larger than the length of :math:`\X{elem}.\EIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{elem}.\EIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -18. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -19. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. +18. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. -20. Push the value :math:`\X{at}.\CONST~d` to the stack. +19. Push the value :math:`\X{at}.\CONST~d` to the stack. -21. Push the value :math:`\val` to the stack. +20. Push the value :math:`\val` to the stack. -22. Execute the instruction :math:`\TABLESET~x`. +21. Execute the instruction :math:`\TABLESET~x`. -23. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. +22. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. +23. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. -25. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. +24. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. -26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -28. Execute the instruction :math:`\TABLEINIT~x~y`. +27. Execute the instruction :math:`\TABLEINIT~x~y`. .. math:: ~\\[-1ex] @@ -3260,35 +3247,33 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`N` is not part of the instruction, then: +9. If :math:`N` is not part of the instruction, then: a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. -11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -12. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -13. If :math:`N` and :math:`\sx` are part of the instruction, then: +12. If :math:`N` and :math:`\sx` are part of the instruction, then: a. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. b. Let :math:`c` be the result of computing :math:`\extend^{\sx}_{N,|t|}(n)`. -14. Else: +13. Else: a. Let :math:`c` be the constant for which :math:`\bytes_t(c) = b^\ast`. -15. Push the value :math:`t.\CONST~c` to the stack. +14. Push the value :math:`t.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3337,29 +3322,27 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`\X{ea} + M \cdot N /8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + M \cdot N /8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /8]`. -12. Let :math:`m_k` be the integer for which :math:`\bytes_{\iM}(m_k) = b^\ast[k \cdot M/8 \slice M/8]`. +11. Let :math:`m_k` be the integer for which :math:`\bytes_{\iM}(m_k) = b^\ast[k \cdot M/8 \slice M/8]`. -13. Let :math:`W` be the integer :math:`M \cdot 2`. +12. Let :math:`W` be the integer :math:`M \cdot 2`. -14. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. +13. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. -15. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. +14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. -16. Push the value :math:`\V128.\CONST~c` to the stack. +15. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3400,27 +3383,25 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -13. Let :math:`L` be the integer :math:`128 / N`. +12. Let :math:`L` be the integer :math:`128 / N`. -14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. +13. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. -15. Push the value :math:`\V128.\CONST~c` to the stack. +14. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3459,25 +3440,23 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. - -10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -13. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. +12. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. -14. Push the value :math:`\V128.\CONST~c` to the stack. +13. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3516,33 +3495,31 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -8. Pop the value :math:`\V128.\CONST~v` from the stack. +7. Pop the value :math:`\V128.\CONST~v` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -13. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +12. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -14. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. +13. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. -15. Let :math:`L` be :math:`128 / N`. +14. Let :math:`L` be :math:`128 / N`. -16. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. +15. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. -17. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. +16. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. -18. Push the value :math:`\V128.\CONST~c` to the stack. +17. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3583,37 +3560,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. -8. Pop the value :math:`t.\CONST~c` from the stack. +7. Pop the value :math:`t.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`N` is not part of the instruction, then: +11. If :math:`N` is not part of the instruction, then: a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. -13. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -14. If :math:`N` is part of the instruction, then: +13. If :math:`N` is part of the instruction, then: a. Let :math:`n` be the result of computing :math:`\wrap_{|t|,N}(c)`. b. Let :math:`b^\ast` be the byte sequence :math:`\bytes_{\iN}(n)`. -15. Else: +14. Else: a. Let :math:`b^\ast` be the byte sequence :math:`\bytes_t(c)`. -16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] @@ -3661,29 +3636,27 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. -8. Pop the value :math:`\V128.\CONST~c` from the stack. +7. Pop the value :math:`\V128.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -13. Let :math:`L` be :math:`128/N`. +12. Let :math:`L` be :math:`128/N`. -14. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. +13. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. -15. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. +14. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. -16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] @@ -3734,7 +3707,10 @@ Memory Instructions S; F; (\MEMORYSIZE~x) &\stepto& S; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad - (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| = \X{sz}\cdot64\,\F{Ki}) \\ + \begin{array}[t]{@{}r@{~}l@{}} + (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| = \X{sz}\cdot64\,\F{Ki} \\ + \wedge S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MITYPE = \X{at}~\X{lim}) + \end{array} \\ \end{array} @@ -3754,17 +3730,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. +6. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Pop the value :math:`\X{at}.\CONST~n` from the stack. -10. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +9. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{|\X{at}|}-1`, for which :math:`\signed_{|\X{at}|}(\X{err})` is :math:`-1`. -11. Either: +10. Either: a. If :ref:`growing ` :math:`\X{mem}` by :math:`n` :ref:`pages ` succeeds, then: @@ -3774,7 +3748,7 @@ Memory Instructions i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. -12. Or: +11. Or: a. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. @@ -3792,7 +3766,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) + S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{|\X{at}|}^{-1}(-1)) \end{array} \end{array} @@ -3820,17 +3794,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. 7. Pop the value :math:`\X{at}.\CONST~n` from the stack. -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 `, a value is on the top of the stack. 9. Pop the value :math:`\val` from the stack. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`address type ` :math:`\X{at}` is on the top of the stack. 11. Pop the value :math:`\X{at}.\CONST~d` from the stack. @@ -3906,33 +3878,27 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Let :math:`\X{at}_d~\limits_d` be the :ref:`memory type ` :math:`\X{mem}_d.\MITYPE`. +10. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_n` is on the top of the stack. -11. Let :math:`\X{at}_s~\limits_s` be the :ref:`memory type ` :math:`\X{mem}_s.\MITYPE`. +11. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_s` and :math:`\X{at}_d`. +12. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_s` is on the top of the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_n` is on the top of the stack. +13. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. -14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_d` is on the top of the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_s` is on the top of the stack. +15. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. -16. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. - -17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_d` is on the top of the stack. - -18. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. - -19. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then: a. Trap. -20. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -21. If :math:`d \leq s`, then: +18. If :math:`d \leq s`, then: a. Push the value :math:`\X{at}_d.\CONST~d` to the stack. @@ -3950,7 +3916,7 @@ Memory Instructions h. Push the value :math:`\X{at}_s.\CONST~(s+1)` to the stack. -22. Else: +19. Else: a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. @@ -3968,9 +3934,9 @@ Memory Instructions h. Push the value :math:`\X{at}_s.\CONST~s` to the stack. -23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. +20. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. -24. Execute the instruction :math:`\MEMORYCOPY~x~y`. +21. Execute the instruction :math:`\MEMORYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -4029,55 +3995,53 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. -8. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. +7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. -9. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. -10. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. +9. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -12. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -14. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{at}.\CONST~d` from the stack. +15. Pop the value :math:`\X{at}.\CONST~d` from the stack. -17. If :math:`s + n` is larger than the length of :math:`\X{data}.\DIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{data}.\DIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -18. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -19. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. +18. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. -20. Push the value :math:`\X{at}.\CONST~d` to the stack. +19. Push the value :math:`\X{at}.\CONST~d` to the stack. -21. Push the value :math:`\I32.\CONST~b` to the stack. +20. Push the value :math:`\I32.\CONST~b` to the stack. -22. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. +21. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. -23. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. +22. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. +23. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. -25. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. +24. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. -26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -28. Execute the instruction :math:`\MEMORYINIT~x~y`. +27. Execute the instruction :math:`\MEMORYINIT~x~y`. .. math:: ~\\[-1ex] diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 5e17179f20..2da8a265fa 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -366,7 +366,7 @@ The syntax of sub types is :ref:`generalized ` for the purp Address Type ~~~~~~~~~~~~ -*Address types* classify the values that can be used to index into +*Address types* are a subset of :ref:`number types ` that classify the values that can be used as offsets into :ref:`memories ` and :ref:`tables `. .. math:: @@ -380,13 +380,12 @@ Address Type Conventions ........... -The *minimum* of two address types is defined as |I32| if either of the types are -|I32|, and |I64| otherwise. +The *minimum* of two address types is defined as the address type whose :ref:`bit width ` is the minimum of the two. .. math:: \begin{array}{llll} - \atmin(\I64, \I64) &=& \I64 \\ - \atmin(\X{at}_1, \X{at}_2) &=& \I32 & (\otherwise) \\ + \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\ + \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\ \end{array} @@ -424,7 +423,7 @@ Memory Types .. math:: \begin{array}{llrl} \production{memory type} & \memtype &::=& - ~\addrtype~\limits \\ + \addrtype~\limits \\ \end{array} The limits constrain the minimum and optionally the maximum size of a memory. @@ -445,7 +444,7 @@ Table Types .. math:: \begin{array}{llrl} \production{table type} & \tabletype &::=& - ~\addrtype~\limits ~\reftype \\ + \addrtype~\limits~\reftype \\ \end{array} Like memories, tables are constrained by limits for their minimum and optionally maximum size. diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 3178332dd4..73bb7182b3 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -307,21 +307,12 @@ An :ref:`element segment ` can be given inline with a table definitio .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~\expr^n{:}\Tvec(\Telemexpr)~\text{)}~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad - \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\Telemexpr)~\text{)} + \text{(}~\text{table}~~\Tid^?~~\Taddrtype^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{table}~~\Tid'~~\Taddrtype^?~~n~~n~~\Treftype~\text{)} \\ & \qquad + \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\text{(}~\text{ref.func}~~\Tfuncidx~\text{)})~\text{)} \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \production{module field} & - \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad - \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\text{(}~\text{ref.func}~~\Tfuncidx~\text{)})~\text{)} - \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\ + (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad + \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}) \\ \end{array} Tables can be defined as :ref:`imports ` or :ref:`exports ` inline: @@ -378,13 +369,13 @@ A :ref:`data segment ` can be given inline with a memory definition, .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{memory}~~\Tid^?~~\X{at}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{memory}~~\Tid'~~\X{at}^?~~m~~m~\text{)} \\ & \qquad - \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{at}'\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\Taddrtype^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{memory}~~\Tid'~~\Taddrtype^?~~m~~m~\text{)} \\ & \qquad + \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} \\ & \qquad\qquad (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad - \iff \X{at}^? \neq \epsilon \wedge \X{at}' = \X{at}^? \vee \X{at}^? = \epsilon \wedge \X{at}' = \text{i32}, \\ & \qquad\qquad - m = \F{ceil}(n / 64\,\F{Ki})), \\ + \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}, \\ & \qquad\qquad + m = \F{ceil}(n / 64\,\F{Ki})) \\ \end{array} Memories can be defined as :ref:`imports ` or :ref:`exports ` inline: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 01e09d93c7..602540d978 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1496,11 +1496,11 @@ Table Instructions * Let :math:`\X{at}_2~\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. -* Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_1` and :math:`\X{at}_2` - * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to []`. +* Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_1` and :math:`\X{at}_2` + +* Then the instruction is valid with type :math:`[\X{at}_1~\X{at}_2~\X{at}] \to []`. .. math:: \frac{ @@ -1890,7 +1890,7 @@ Memory Instructions * Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_x` and :math:`\X{at}_y` -* Then the instruction is valid with type :math:`[\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to []`. +* Then the instruction is valid with type :math:`[\X{at}_x~\X{at}_y~\X{at}] \to []`. .. math:: \frac{ diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 75ff8c08ea..12457adf82 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -513,15 +513,13 @@ A :ref:`table type ` :math:`(\addrtype_1~\limits_1~\reftype_1) .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 - \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 \qquad C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2 \qquad C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1 }{ - C \vdashtabletypematch \addrtype_1~\limits_1~\reftype_1 \matchestabletype \addrtype_2~\limits_2~\reftype_2 + C \vdashtabletypematch \addrtype~\limits_1~\reftype_1 \matchestabletype \addrtype~\limits_2~\reftype_2 } @@ -541,11 +539,9 @@ A :ref:`memory type ` :math:`(\addrtype_1~\limits_1)` matches :m .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 - \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 }{ - C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2 + C \vdashmemtypematch \addrtype~\limits_1 \matchesmemtype \addrtype~\limits_2 } From 906d452282a9615fa99067b3cd3d4587402489a8 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 6 Nov 2024 15:10:58 -0800 Subject: [PATCH 3/3] Intepreter and test updates from @rossberg (#99) Interpreter: - Fixed evaluation of v128 load/store instructions to work with i64 - Reworked bulk operation execution to still reduce to well-typed instructions for i32 - Added missing size check to table allocation - Various minor refactorings and clean-ups Tests: - Added tests for size check in i64 table and memory type limits Split out from https://github.com/WebAssembly/spec/pull/1839 --- interpreter/binary/decode.ml | 12 +- interpreter/binary/encode.ml | 10 +- interpreter/exec/eval.ml | 244 +++++++++++++++----------------- interpreter/host/spectest.ml | 6 +- interpreter/runtime/data.ml | 1 - interpreter/runtime/data.mli | 3 +- interpreter/runtime/elem.mli | 2 +- interpreter/runtime/memory.ml | 36 ++--- interpreter/runtime/memory.mli | 5 +- interpreter/runtime/table.ml | 26 ++-- interpreter/runtime/table.mli | 13 +- interpreter/runtime/value.ml | 20 ++- interpreter/syntax/free.ml | 4 +- interpreter/syntax/operators.ml | 4 + interpreter/syntax/types.ml | 40 +++--- interpreter/text/arrange.ml | 6 +- interpreter/text/parser.mly | 86 ++++------- interpreter/valid/match.ml | 9 +- interpreter/valid/valid.ml | 144 +++++++++---------- test/core/memory.wast | 37 +++-- test/core/memory64.wast | 18 +++ test/core/table.wast | 6 +- 22 files changed, 370 insertions(+), 362 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 1db0dce4f7..53c7294c88 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -281,19 +281,19 @@ let limits uN s = let flags = byte s in require (flags land 0xfa = 0) s (pos s - 1) "malformed limits flags"; let has_max = (flags land 1 = 1) in - let is64 = (flags land 4 = 4) in + let at = if flags land 4 = 4 then I64AT else I32AT in let min = uN s in let max = opt uN has_max s in - {min; max}, is64 + at, {min; max} let table_type s = let t = ref_type s in - let lim, is64 = limits u64 s in - TableT (lim, (if is64 then I64AddrType else I32AddrType), t) + let at, lim = limits u64 s in + TableT (at, lim, t) let memory_type s = - let lim, is64 = limits u64 s in - MemoryT (lim, if is64 then I64AddrType else I32AddrType) + let at, lim = limits u64 s in + MemoryT (at, lim) let global_type s = let t = val_type s in diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 3e7003a898..eb1e729b03 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -194,15 +194,15 @@ struct | RecT [st] -> sub_type st | RecT sts -> s7 (-0x32); vec sub_type sts - let limits vu {min; max} at = - let flags = flag (max <> None) 0 + flag (at = I64AddrType) 2 in - byte flags; vu min; opt vu max + let limits at {min; max} = + let flags = flag (max <> None) 0 + flag (at = I64AT) 2 in + byte flags; u64 min; opt u64 max let table_type = function - | TableT (lim, at, t) -> ref_type t; limits u64 lim at + | TableT (at, lim, t) -> ref_type t; limits at lim let memory_type = function - | MemoryT (lim, at) -> limits u64 lim at + | MemoryT (at, lim) -> limits at lim let global_type = function | GlobalT (mut, t) -> val_type t; mutability mut diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index c5631d1baa..8af47528d4 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -157,48 +157,27 @@ let split n (vs : 'a stack) at = take n vs at, drop n vs at * c : config *) -let inc_address i loc = - match i with - | I32 x -> (I32 (I32.add x 1l) @@ loc) - | I64 x -> (I64 (I64.add x 1L) @@ loc) - | _ -> Crash.error loc ("bad address type") - -let index_of_num x = - match x with - | I64 i -> i - | I32 i -> I64_convert.extend_i32_u i - | _ -> raise Type - let mem_oob frame x i n = let mem = (memory frame.inst x) in - let start = Memory.address_of_num i in - I64.gt_u (I64.add start (Memory.address_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Memory.bound mem) let data_oob frame x i n = - I64.gt_u (I64.add (Memory.address_of_num i) (Memory.address_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Data.size (data frame.inst x)) let table_oob frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (Table.index_of_num n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Table.size (table frame.inst x)) let elem_oob frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (Table.index_of_num n)) - (Elem.size (elem frame.inst x)) - -let elem_oob2 frame x i n = - I64.gt_u (I64.add (Table.index_of_num i) (I64_convert.extend_i32_u n)) + I64.gt_u (I64.add (addr_of_num i) (addr_of_num n)) (Elem.size (elem frame.inst x)) let array_oob a i n = I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n)) (I64_convert.extend_i32_u (Aggr.array_length a)) -let array_oob2 a i n = - I64.gt_u (I64.add (I64_convert.extend_i32_u i) (index_of_num n)) - (I64_convert.extend_i32_u (Aggr.array_length a)) - let rec step (c : config) : config = let vs, es = c.code in let e = List.hd es in @@ -284,9 +263,9 @@ let rec step (c : config) : config = | CallRef _x, Ref (FuncRef f) :: vs -> vs, [Invoke f @@ e.at] - | CallIndirect (x, y), Num n :: vs -> - let i = Table.index_of_num n in - let f = func_ref c.frame.inst x i e.at in + | CallIndirect (x, y), Num i :: vs -> + let i_64 = addr_of_num i in + let f = func_ref c.frame.inst x i_64 e.at in if Match.match_def_type [] (Func.type_of f) (type_ c.frame.inst y) then vs, [Invoke f @@ e.at] else @@ -373,96 +352,96 @@ let rec step (c : config) : config = with Global.NotMutable -> Crash.error e.at "write to immutable global" | Global.Type -> Crash.error e.at "type mismatch at global write") - | TableGet x, Num n :: vs' -> - let i = Table.index_of_num n in - (try Ref (Table.load (table c.frame.inst x) i) :: vs', [] + | TableGet x, Num i :: vs' -> + let i_64 = addr_of_num i in + (try Ref (Table.load (table c.frame.inst x) i_64) :: vs', [] with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) - | TableSet x, Ref r :: Num n :: vs' -> - let i = Table.index_of_num n in - (try Table.store (table c.frame.inst x) i r; vs', [] + | TableSet x, Ref r :: Num i :: vs' -> + let i_64 = addr_of_num i in + (try Table.store (table c.frame.inst x) i_64 r; vs', [] with exn -> vs', [Trapping (table_error e.at exn) @@ e.at]) | TableSize x, vs -> let tab = table c.frame.inst x in - value_of_addr (Table.addr_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] + Num (num_of_addr (Table.addr_type_of tab) (Table.size tab)) :: vs, [] - | TableGrow x, Num delta :: Ref r :: vs' -> + | TableGrow x, Num n :: Ref r :: vs' -> + let n_64 = addr_of_num n in let tab = table c.frame.inst x in let old_size = Table.size tab in let result = - try Table.grow tab (Table.index_of_num delta) r; old_size + try Table.grow tab n_64 r; old_size with Table.SizeOverflow | Table.SizeLimit | Table.OutOfMemory -> -1L - in (value_of_addr (Table.addr_type_of tab) result) :: vs', [] + in Num (num_of_addr (Table.addr_type_of tab) result) :: vs', [] | TableFill x, Num n :: Ref r :: Num i :: vs' -> - let n_64 = Table.index_of_num n in + let n_64 = addr_of_num n in + let i_64 = addr_of_num i in if table_oob c.frame x i n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else - let i_64 = Table.index_of_num i in let _ = assert (I64.lt_u i_64 0xffff_ffff_ffff_ffffL) in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 i_64 @@ e.at)); + Plain (Const (i @@ e.at)); Refer r; Plain (TableSet x); - Plain (Const (I64 (I64.add i_64 1L) @@ e.at)); + Plain (Const (addr_add i 1L @@ e.at)); Refer r; - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableFill x); ] | TableCopy (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Table.index_of_num n in - let s_64 = Table.index_of_num s in - let d_64 = Table.index_of_num d in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in + let d_64 = addr_of_num d in if table_oob c.frame x d n || table_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else if I64.le_u d_64 s_64 then vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); Plain (TableGet y); Plain (TableSet x); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableCopy (x, y)); ] else (* d > s *) let n' = I64.sub n_64 1L in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 (I64.add d_64 n') @@ e.at)); - Plain (Const (I64 (I64.add s_64 n') @@ e.at)); + Plain (Const (addr_add d n' @@ e.at)); + Plain (Const (addr_add s n' @@ e.at)); Plain (TableGet y); Plain (TableSet x); - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); - Plain (Const (I64 n' @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableCopy (x, y)); ] | TableInit (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Table.index_of_num n in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if table_oob c.frame x d n || elem_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else - let d_64 = Table.index_of_num d in - let s_64 = Table.index_of_num s in let seg = elem c.frame.inst y in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); + Plain (Const (d @@ e.at)); Refer (Elem.load seg s_64); Plain (TableSet x); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (TableInit (x, y)); ] @@ -472,98 +451,99 @@ let rec step (c : config) : config = vs, [] | Load (x, {offset; ty; pack; _}), Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = Memory.address_of_num i in (try let n = match pack with - | None -> Memory.load_num mem a offset ty - | Some (sz, ext) -> Memory.load_num_packed sz ext mem a offset ty + | None -> Memory.load_num mem i_64 offset ty + | Some (sz, ext) -> Memory.load_num_packed sz ext mem i_64 offset ty in Num n :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) | Store (x, {offset; pack; _}), Num n :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = Memory.address_of_num i in (try (match pack with - | None -> Memory.store_num mem a offset n - | Some sz -> Memory.store_num_packed sz mem a offset n + | None -> Memory.store_num mem i_64 offset n + | Some sz -> Memory.store_num_packed sz mem i_64 offset n ); vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - | VecLoad (x, {offset; ty; pack; _}), Num (I32 i) :: vs' -> + | VecLoad (x, {offset; ty; pack; _}), Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let a = I64_convert.extend_i32_u i in (try let v = match pack with - | None -> Memory.load_vec mem a offset ty - | Some (sz, ext) -> Memory.load_vec_packed sz ext mem a offset ty + | None -> Memory.load_vec mem i_64 offset ty + | Some (sz, ext) -> Memory.load_vec_packed sz ext mem i_64 offset ty in Vec v :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - | VecStore (x, {offset; _}), Vec v :: Num (I32 i) :: vs' -> + | VecStore (x, {offset; _}), Vec v :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try - Memory.store_vec mem addr offset v; + Memory.store_vec mem i_64 offset v; vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - | VecLoadLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num (I32 i) :: vs' -> + | VecLoadLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try let v = match pack with | Pack8 -> V128.I8x16.replace_lane j v - (I32Num.of_num 0 (Memory.load_num_packed Pack8 SX mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num_packed Pack8 SX mem i_64 offset I32T)) | Pack16 -> V128.I16x8.replace_lane j v - (I32Num.of_num 0 (Memory.load_num_packed Pack16 SX mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num_packed Pack16 SX mem i_64 offset I32T)) | Pack32 -> V128.I32x4.replace_lane j v - (I32Num.of_num 0 (Memory.load_num mem addr offset I32T)) + (I32Num.of_num 0 (Memory.load_num mem i_64 offset I32T)) | Pack64 -> V128.I64x2.replace_lane j v - (I64Num.of_num 0 (Memory.load_num mem addr offset I64T)) + (I64Num.of_num 0 (Memory.load_num mem i_64 offset I64T)) in Vec (V128 v) :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - | VecStoreLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num (I32 i) :: vs' -> + | VecStoreLane (x, {offset; ty; pack; _}, j), Vec (V128 v) :: Num i :: vs' -> + let i_64 = addr_of_num i in let mem = memory c.frame.inst x in - let addr = I64_convert.extend_i32_u i in (try (match pack with | Pack8 -> - Memory.store_num_packed Pack8 mem addr offset (I32 (V128.I8x16.extract_lane_s j v)) + Memory.store_num_packed Pack8 mem i_64 offset (I32 (V128.I8x16.extract_lane_s j v)) | Pack16 -> - Memory.store_num_packed Pack16 mem addr offset (I32 (V128.I16x8.extract_lane_s j v)) + Memory.store_num_packed Pack16 mem i_64 offset (I32 (V128.I16x8.extract_lane_s j v)) | Pack32 -> - Memory.store_num mem addr offset (I32 (V128.I32x4.extract_lane_s j v)) + Memory.store_num mem i_64 offset (I32 (V128.I32x4.extract_lane_s j v)) | Pack64 -> - Memory.store_num mem addr offset (I64 (V128.I64x2.extract_lane_s j v)) + Memory.store_num mem i_64 offset (I64 (V128.I64x2.extract_lane_s j v)) ); vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) | MemorySize x, vs -> let mem = memory c.frame.inst x in - value_of_addr (Memory.addr_type_of mem) (Memory.size mem) :: vs, [] + Num (num_of_addr (Memory.addr_type_of mem) (Memory.size mem)) :: vs, [] - | MemoryGrow x, Num delta :: vs' -> + | MemoryGrow x, Num n :: vs' -> + let n_64 = addr_of_num n in let mem = memory c.frame.inst x in let old_size = Memory.size mem in let result = - try Memory.grow mem (Memory.address_of_num delta); old_size + try Memory.grow mem n_64; old_size with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1L - in (value_of_addr (Memory.addr_type_of mem) result) :: vs', [] + in Num (num_of_addr (Memory.addr_type_of mem) result) :: vs', [] | MemoryFill x, Num n :: Num k :: Num i :: vs' -> - let n_64 = Memory.address_of_num n in + let n_64 = addr_of_num n in if mem_oob c.frame x i n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then @@ -574,67 +554,66 @@ let rec step (c : config) : config = Plain (Const (k @@ e.at)); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (inc_address i e.at)); + Plain (Const (addr_add i 1L @@ e.at)); Plain (Const (k @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryFill x); ] | MemoryCopy (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Memory.address_of_num n in - let s_64 = Memory.address_of_num s in - let d_64 = Memory.address_of_num d in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in + let d_64 = addr_of_num d in if mem_oob c.frame x d n || mem_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else if I64.le_u d_64 s_64 then vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); Plain (Load (y, {ty = I32T; align = 0; offset = 0L; pack = Some (Pack8, ZX)})); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryCopy (x, y)); ] else (* d > s *) let n' = I64.sub n_64 1L in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 (I64.add d_64 n') @@ e.at)); - Plain (Const (I64 (I64.add s_64 n') @@ e.at)); + Plain (Const (addr_add d n' @@ e.at)); + Plain (Const (addr_add s n' @@ e.at)); Plain (Load (y, {ty = I32T; align = 0; offset = 0L; pack = Some (Pack8, ZX)})); Plain (Store (x, {ty = I32T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 s_64 @@ e.at)); - Plain (Const (I64 n' @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (s @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryCopy (x, y)); ] | MemoryInit (x, y), Num n :: Num s :: Num d :: vs' -> - let n_64 = Memory.address_of_num n in + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if mem_oob c.frame x d n || data_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else if n_64 = 0L then vs', [] else let seg = data c.frame.inst y in - let s_64 = Memory.address_of_num s in - let d_64 = Memory.address_of_num d in let b = Data.load_byte seg s_64 in vs', List.map (Lib.Fun.flip (@@) e.at) [ - Plain (Const (I64 d_64 @@ e.at)); - Plain (Const (I64 (I64.of_int_u (Char.code b)) @@ e.at)); + Plain (Const (d @@ e.at)); + Plain (Const (I32 (I32.of_int_u (Char.code b)) @@ e.at)); Plain (Store (x, {ty = I64T; align = 0; offset = 0L; pack = Some Pack8})); - Plain (Const (I64 (I64.add d_64 1L) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add d 1L @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); + Plain (Const (addr_sub n 1L @@ e.at)); Plain (MemoryInit (x, y)); ] @@ -748,12 +727,14 @@ let rec step (c : config) : config = in Ref (Aggr.ArrayRef array) :: vs'', [] | ArrayNewElem (x, y), Num n :: Num s :: vs' -> + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if elem_oob c.frame y s n then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else let seg = elem c.frame.inst y in - let s_64 = Table.index_of_num s in - let rs = Lib.List64.init (Table.index_of_num n) (fun i -> Elem.load seg (Int64.add s_64 i)) in + let rs = Lib.List64.init n_64 + (fun i -> Elem.load seg (Int64.add s_64 i)) in let args = List.map (fun r -> Ref r) rs in let array = try Aggr.alloc_array (type_ c.frame.inst x) args @@ -761,14 +742,16 @@ let rec step (c : config) : config = in Ref (Aggr.ArrayRef array) :: vs', [] | ArrayNewData (x, y), Num n :: Num s :: vs' -> + let n_64 = addr_of_num n in + let s_64 = addr_of_num s in if data_oob c.frame y s n then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] else let ArrayT (FieldT (_mut, st)) = array_type c.frame.inst x in let seg = data c.frame.inst y in - let args = Lib.List64.init (Memory.address_of_num n) + let args = Lib.List64.init n_64 (fun i -> - let a = I64.(add (Memory.address_of_num s) (mul i (I64.of_int_u (storage_size st)))) in + let a = I64.(add s_64 (mul i (I64.of_int_u (storage_size st)))) in Data.load_val_storage seg a st ) in @@ -884,18 +867,17 @@ let rec step (c : config) : config = vs', [Trapping "null array reference" @@ e.at] | ArrayInitData (x, y), - Num n :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> - let n_64 = Memory.address_of_num n in - if array_oob2 a d n then + Num (I32 n) :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> + let s_64 = addr_of_num s in + if array_oob a d n then vs', [Trapping "out of bounds array access" @@ e.at] - else if data_oob c.frame y s n then + else if data_oob c.frame y s (I64 (I64_convert.extend_i32_u n)) then vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at] - else if n_64 = 0L then + else if n = 0l then vs', [] else let ArrayT (FieldT (_mut, st)) = array_type c.frame.inst x in let seg = data c.frame.inst y in - let s_64 = Memory.address_of_num s in let v = Data.load_val_storage seg s_64 st in vs', List.map (Lib.Fun.flip (@@) e.at) [ Refer (Aggr.ArrayRef a); @@ -904,8 +886,8 @@ let rec step (c : config) : config = Plain (ArraySet x); Refer (Aggr.ArrayRef a); Plain (Const (I32 (I32.add d 1l) @@ e.at)); - Plain (Const (I64 (I64.add s_64 (I64.of_int_u (storage_size st))) @@ e.at)); - Plain (Const (I64 (I64.sub n_64 1L) @@ e.at)); + Plain (Const (addr_add s (I64.of_int_u (storage_size st)) @@ e.at)); + Plain (Const (I32 (I32.sub n 1l) @@ e.at)); Plain (ArrayInitData (x, y)); ] @@ -915,15 +897,15 @@ let rec step (c : config) : config = | ArrayInitElem (x, y), Num (I32 n) :: Num s :: Num (I32 d) :: Ref (Aggr.ArrayRef a) :: vs' -> + let s_64 = addr_of_num s in if array_oob a d n then vs', [Trapping "out of bounds array access" @@ e.at] - else if elem_oob2 c.frame y s n then + else if elem_oob c.frame y s (I64 (I64_convert.extend_i32_u n)) then vs', [Trapping (table_error e.at Table.Bounds) @@ e.at] else if n = 0l then vs', [] else let seg = elem c.frame.inst y in - let s_64 = Table.index_of_num s in let v = Ref (Elem.load seg s_64) in vs', List.map (Lib.Fun.flip (@@) e.at) [ Refer (Aggr.ArrayRef a); @@ -932,7 +914,7 @@ let rec step (c : config) : config = Plain (ArraySet x); Refer (Aggr.ArrayRef a); Plain (Const (I32 (I32.add d 1l) @@ e.at)); - Plain (Const (I64 (I64.add s_64 1L) @@ e.at)); + Plain (Const (addr_add s 1L @@ e.at)); Plain (Const (I32 (I32.sub n 1l) @@ e.at)); Plain (ArrayInitElem (x, y)); ] diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index aaf8f06655..8d6c039bf4 100644 --- a/interpreter/host/spectest.ml +++ b/interpreter/host/spectest.ml @@ -20,15 +20,15 @@ let global (GlobalT (_, t) as gt) = in ExternGlobal (Global.alloc gt v) let table = - let tt = TableT ({min = 10L; max = Some 20L}, I32AddrType, (Null, FuncHT)) in + let tt = TableT (I32AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let table64 = - let tt = TableT ({min = 10L; max = Some 20L}, I64AddrType, (Null, FuncHT)) in + let tt = TableT (I64AT, {min = 10L; max = Some 20L}, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let memory = - let mt = MemoryT ({min = 1L; max = Some 2L}, I32AddrType) in + let mt = MemoryT (I32AT, {min = 1L; max = Some 2L}) in ExternMemory (Memory.alloc mt) let func f ft = diff --git a/interpreter/runtime/data.ml b/interpreter/runtime/data.ml index 785dcc6081..66c2ad58db 100644 --- a/interpreter/runtime/data.ml +++ b/interpreter/runtime/data.ml @@ -1,6 +1,5 @@ type data = string ref type t = data -type address = Memory.address exception Bounds diff --git a/interpreter/runtime/data.mli b/interpreter/runtime/data.mli index f0074e366c..86741d5c0e 100644 --- a/interpreter/runtime/data.mli +++ b/interpreter/runtime/data.mli @@ -1,6 +1,7 @@ +open Value + type data type t = data -type address = Memory.address exception Bounds diff --git a/interpreter/runtime/elem.mli b/interpreter/runtime/elem.mli index b9b35a11dd..d614429077 100644 --- a/interpreter/runtime/elem.mli +++ b/interpreter/runtime/elem.mli @@ -7,5 +7,5 @@ exception Bounds val alloc : ref_ list -> elem val size : elem -> Table.size -val load : elem -> Table.index -> ref_ (* raises Bounds *) +val load : elem -> address -> ref_ (* raises Bounds *) val drop : elem -> unit diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 113a9cd25e..3c3742d94d 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -4,8 +4,7 @@ open Bigarray open Lib.Bigarray type size = int64 (* number of pages *) -type address = int64 -type offset = int64 +type offset = address type count = int32 type memory' = (int, int8_unsigned_elt, c_layout) Array1.t @@ -25,8 +24,12 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let create n at = - if I64.gt_u n 0x10000L && at = I32AddrType then raise SizeOverflow else +let valid_size at i = + match at with + | I32AT -> I64.le_u i 0xffffL + | I64AT -> true + +let create n = try let size = Int64.(mul n page_size) in let mem = Array1_64.create Int8_unsigned C_layout size in @@ -34,10 +37,11 @@ let create n at = mem with Out_of_memory -> raise OutOfMemory -let alloc (MemoryT (lim, at) as ty) = +let alloc (MemoryT (at, lim) as ty) = assert Free.((memory_type ty).types = Set.empty); + if not (valid_size at lim.min) then raise SizeOverflow; if not (valid_limits lim) then raise Type; - {ty; content = create lim.min at} + {ty; content = create lim.min} let bound mem = Array1_64.dim mem.content @@ -49,31 +53,21 @@ let type_of mem = mem.ty let addr_type_of mem = - let (MemoryT (_, at)) = type_of mem in at - -let address_of_num x = - match x with - | I32 i -> I64_convert.extend_i32_u i - | I64 i -> i - | _ -> raise Type - -let address_of_value x = - match x with - | Num n -> address_of_num n - | _ -> raise Type + let MemoryT (at, _) = type_of mem in at let grow mem delta = - let MemoryT (lim, at) = mem.ty in + let MemoryT (at, lim) = mem.ty in assert (lim.min = size mem); let old_size = lim.min in let new_size = Int64.add old_size delta in if I64.gt_u old_size new_size then raise SizeOverflow else let lim' = {lim with min = new_size} in + if not (valid_size at new_size) then raise SizeOverflow else if not (valid_limits lim') then raise SizeLimit else - let after = create new_size (addr_type_of mem) in + let after = create new_size in let dim = Array1_64.dim mem.content in Array1.blit (Array1_64.sub mem.content 0L dim) (Array1_64.sub after 0L dim); - mem.ty <- MemoryT (lim', at); + mem.ty <- MemoryT (at, lim'); mem.content <- after let load_byte mem a = diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index da9f468f8b..9f0edc7cd3 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -5,8 +5,7 @@ type memory type t = memory type size = int64 (* number of pages *) -type address = int64 -type offset = int64 +type offset = address type count = int32 exception Type @@ -22,8 +21,6 @@ val type_of : memory -> memory_type val addr_type_of : memory -> addr_type val size : memory -> size val bound : memory -> address -val address_of_value : value -> address -val address_of_num : num -> address val grow : memory -> size -> unit (* raises SizeLimit, SizeOverflow, OutOfMemory *) diff --git a/interpreter/runtime/table.ml b/interpreter/runtime/table.ml index b18dbd5dfd..d87807f4cb 100644 --- a/interpreter/runtime/table.ml +++ b/interpreter/runtime/table.ml @@ -1,9 +1,8 @@ open Types open Value -type size = int64 -type index = int64 -type count = int32 +type size = address +type offset = address type table = {mutable ty : table_type; mutable content : ref_ array} type t = table @@ -19,17 +18,18 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let valid_addr at i = +let valid_size at i = match at with - | I32AddrType -> I64.le_u i 0xffff_ffffL - | I64AddrType -> true + | I32AT -> I64.le_u i 0xffff_ffffL + | I64AT -> true let create size r = try Lib.Array64.make size r with Out_of_memory | Invalid_argument _ -> raise OutOfMemory -let alloc (TableT (lim, at, t) as ty) r = +let alloc (TableT (at, lim, t) as ty) r = assert Free.((ref_type t).types = Set.empty); + if not (valid_size at lim.min) then raise SizeOverflow; if not (valid_limits lim) then raise Type; {ty; content = create lim.min r} @@ -40,26 +40,26 @@ let type_of tab = tab.ty let addr_type_of tab = - let (TableT (_, at, _)) = type_of tab in at + let TableT (at, _, _) = type_of tab in at -let index_of_num x = +let addr_of_num x = match x with | I64 i -> i | I32 i -> I64_convert.extend_i32_u i | _ -> raise Type let grow tab delta r = - let TableT (lim, at, t) = tab.ty in + let TableT (at, lim, t) = tab.ty in assert (lim.min = size tab); let old_size = lim.min in let new_size = Int64.add old_size delta in if I64.gt_u old_size new_size then raise SizeOverflow else let lim' = {lim with min = new_size} in - if not (valid_addr at new_size) then raise SizeOverflow else + if not (valid_size at new_size) then raise SizeOverflow else if not (valid_limits lim') then raise SizeLimit else let after = create new_size r in Array.blit tab.content 0 after 0 (Array.length tab.content); - tab.ty <- TableT (lim', at, t); + tab.ty <- TableT (at, lim', t); tab.content <- after let load tab i = @@ -67,7 +67,7 @@ let load tab i = Lib.Array64.get tab.content i let store tab i r = - let TableT (_lim, _at, t) = tab.ty in + let TableT (_at, _lim, t) = tab.ty in if not (Match.match_ref_type [] (type_of_ref r) t) then raise Type; if i < 0L || i >= Lib.Array64.length tab.content then raise Bounds; Lib.Array64.set tab.content i r diff --git a/interpreter/runtime/table.mli b/interpreter/runtime/table.mli index 6ebba60684..53caf5965e 100644 --- a/interpreter/runtime/table.mli +++ b/interpreter/runtime/table.mli @@ -4,9 +4,8 @@ open Value type table type t = table -type size = int64 -type index = int64 -type count = int32 +type size = address +type offset = address exception Type exception Bounds @@ -18,10 +17,10 @@ val alloc : table_type -> ref_ -> table (* raises Type, OutOfMemory *) val type_of : table -> table_type val addr_type_of : table -> addr_type val size : table -> size -val index_of_num : num -> index +val addr_of_num : num -> address val grow : table -> size -> ref_ -> unit (* raises SizeOverflow, SizeLimit, OutOfMemory *) -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 *) +val load : table -> address -> ref_ (* raises Bounds *) +val store : table -> address -> ref_ -> unit (* raises Type, Bounds *) +val blit : table -> address -> ref_ list -> unit (* raises Bounds *) diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml index 5381b67f1e..75c5cd2c97 100644 --- a/interpreter/runtime/value.ml +++ b/interpreter/runtime/value.ml @@ -19,6 +19,8 @@ type t = value type ref_ += NullRef of heap_type +type address = I64.t + (* Injection & projection *) @@ -281,10 +283,22 @@ let storage_bits_of_val st v = let value_of_bool b = Num (I32 (if b then 1l else 0l)) -let value_of_addr at x = +let num_of_addr at i = match at with - | I64AddrType -> Num (I64 x) - | I32AddrType -> Num (I32 (Int64.to_int32 x)) + | I64AT -> I64 i + | I32AT -> I32 (I32_convert.wrap_i64 i) + +let addr_of_num x = + match x with + | I32 i -> I64_convert.extend_i32_u i + | I64 i -> i + | _ -> raise Type + +let addr_add n i = + num_of_addr (addr_type_of_num_type (type_of_num n)) (I64.add (addr_of_num n) i) +let addr_sub n i = + num_of_addr (addr_type_of_num_type (type_of_num n)) (I64.sub (addr_of_num n) i) + let string_of_num = function | I32 i -> I32.to_string_s i diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index efbbd58dae..37ab763fea 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -121,8 +121,8 @@ let def_type = function | DefT (rt, _i) -> rec_type rt let global_type (GlobalT (_mut, t)) = val_type t -let table_type (TableT (_lim, _at, t)) = ref_type t -let memory_type (MemoryT (_lim, _at)) = empty +let table_type (TableT (_at, _lim, t)) = ref_type t +let memory_type (MemoryT (_at, _lim)) = empty let tag_type (TagT dt) = def_type dt let extern_type = function diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index 2f9879ef8e..b6e65a3601 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -15,6 +15,10 @@ let v128_const n = VecConst (V128 n.it @@ n.at) let ref_null t = RefNull t let ref_func x = RefFunc x +let at_const = function + | I32AT -> fun n -> i32_const (I32_convert.wrap_i64 n.it @@ n.at) + | I64AT -> i64_const + let unreachable = Unreachable let nop = Nop let drop = Drop diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index fb52464458..f6a7fe2455 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -12,6 +12,7 @@ type 'a limits = {min : 'a; max : 'a option} type var = StatX of type_idx | RecX of int32 +type addr_type = I32AT | I64AT type num_type = I32T | I64T | F32T | F64T type vec_type = V128T type heap_type = @@ -25,7 +26,6 @@ type heap_type = and ref_type = null * heap_type and val_type = NumT of num_type | VecT of vec_type | RefT of ref_type | BotT -and addr_type = I32AddrType | I64AddrType and result_type = val_type list and instr_type = InstrT of result_type * result_type * local_idx list @@ -45,8 +45,8 @@ and sub_type = SubT of final * heap_type list * str_type and rec_type = RecT of sub_type list and def_type = DefT of rec_type * int32 -type table_type = TableT of Int64.t limits * addr_type * ref_type -type memory_type = MemoryT of Int64.t limits * addr_type +type table_type = TableT of addr_type * Int64.t limits * ref_type +type memory_type = MemoryT of addr_type * Int64.t limits type global_type = GlobalT of mut * val_type type tag_type = TagT of def_type type local_type = LocalT of init * val_type @@ -111,7 +111,17 @@ let defaultable = function | BotT -> assert false -(* Projections *) +(* Conversions & Projections *) + +let num_type_of_addr_type = function + | I32AT -> I32T + | I64AT -> I64T + +let addr_type_of_num_type = function + | I32T -> I32AT + | I64T -> I64AT + | _ -> assert false + let unpacked_storage_type = function | ValStorageT t -> t @@ -147,11 +157,6 @@ let memories = List.filter_map (function ExternMemoryT mt -> Some mt | _ -> None let globals = List.filter_map (function ExternGlobalT gt -> Some gt | _ -> None) let tags = List.filter_map (function ExternTagT tt -> Some tt | _ -> None) -let num_type_of_addr_type = function - | I32AddrType -> I32T - | I64AddrType -> I64T - -let value_type_of_addr_type t = NumT (num_type_of_addr_type t) (* Substitution *) @@ -161,6 +166,8 @@ let subst_of dts = function | StatX x -> DefHT (Lib.List32.nth dts x) | RecX i -> VarHT (RecX i) +let subst_addr_type s t = t + let subst_num_type s t = t let subst_vec_type s t = t @@ -228,10 +235,10 @@ let subst_def_type s = function let subst_memory_type s = function - | MemoryT (lim, at) -> MemoryT (lim, at) + | MemoryT (at, lim) -> MemoryT (subst_addr_type s at, lim) let subst_table_type s = function - | TableT (lim, at, t) -> TableT (lim, at, subst_ref_type s t) + | TableT (at, lim, t) -> TableT (subst_addr_type s at, lim, subst_ref_type s t) let subst_global_type s = function | GlobalT (mut, t) -> GlobalT (mut, subst_val_type s t) @@ -294,6 +301,7 @@ let expand_def_type (dt : def_type) : str_type = let SubT (_, _, st) = unroll_def_type dt in st + (* String conversion *) let string_of_idx x = @@ -336,6 +344,9 @@ let string_of_num_type = function | F32T -> "f32" | F64T -> "f64" +let string_of_addr_type at = + string_of_num_type (num_type_of_addr_type at) + let string_of_vec_type = function | V128T -> "v128" @@ -365,9 +376,6 @@ and string_of_val_type = function | RefT t -> string_of_ref_type t | BotT -> "bot" -and string_of_addr_type t = - string_of_val_type (value_type_of_addr_type t) - and string_of_result_type = function | ts -> "[" ^ String.concat " " (List.map string_of_val_type ts) ^ "]" @@ -418,10 +426,10 @@ let string_of_limits = function (match max with None -> "" | Some n -> " " ^ I64.to_string_u n) let string_of_memory_type = function - | MemoryT (lim, at) -> string_of_num_type (num_type_of_addr_type at) ^ " " ^ string_of_limits lim + | MemoryT (at, lim) -> string_of_addr_type at ^ " " ^ string_of_limits lim let string_of_table_type = function - | TableT (lim, at, t) -> string_of_num_type (num_type_of_addr_type at) ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t + | TableT (at, lim, t) -> string_of_addr_type at ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t let string_of_global_type = function | GlobalT (mut, t) -> string_of_mut (string_of_val_type t) mut diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 6f7eccdaa8..76c987f949 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -64,6 +64,7 @@ let mutability node = function | Cons -> node | Var -> Node ("mut", [node]) +let addr_type t = string_of_addr_type t let num_type t = string_of_num_type t let vec_type t = string_of_vec_type t let ref_type t = @@ -77,7 +78,6 @@ let ref_type t = | (Null, ExnHT) -> "exnref" | t -> string_of_ref_type t -let addr_type t = string_of_val_type (value_type_of_addr_type t) let heap_type t = string_of_heap_type t let val_type t = string_of_val_type t let storage_type t = string_of_storage_type t @@ -657,13 +657,13 @@ let tag off i tag = ) let table off i tab = - let {ttype = TableT (lim, at, t); tinit} = tab.it in + let {ttype = TableT (at, lim, t); tinit} = tab.it in Node ("table $" ^ nat (off + i) ^ " " ^ addr_type at ^ " " ^ limits nat64 lim, atom ref_type t :: list instr tinit.it ) let memory off i mem = - let {mtype = MemoryT (lim, at)} = mem.it in + let {mtype = MemoryT (at, lim)} = mem.it in Node ("memory $" ^ nat (off + i) ^ " " ^ addr_type at ^ " " ^ limits nat64 lim, []) let is_elem_kind = function diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index df2ec4057c..1fbeeeccc4 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -264,39 +264,6 @@ let inline_func_type_explicit (c : context) x ft loc = error (at loc) "inline function type does not match explicit type"; x -let addr_type_of_num_type t loc = - match t with - | I32T -> I32AddrType - | I64T -> I64AddrType - | _ -> error (at loc) "illegal address type" - -let addr_type_of_value_type t loc = - match t with - | NumT t -> addr_type_of_num_type t loc - | _ -> error (at loc) "illegal address type" - -let memory_data init at c x loc = - let size = Int64.(div (add (of_int (String.length init)) 65535L) 65536L) in - let instr = match at with - | I32AddrType -> i32_const (0l @@ loc) - | I64AddrType -> i64_const (0L @@ loc) in - let offset = [instr @@ loc] @@ loc in - [{mtype = MemoryT ({min = size; max = Some size}, at)} @@ loc], - [{dinit = init; dmode = Active {index = x; offset} @@ loc} @@ loc], - [], [] - -let table_data tinit init at etype c x loc = - let instr = match at with - | I32AddrType -> i32_const (0l @@ loc) - | I64AddrType -> i64_const (0L @@ loc) in - let offset = [instr @@ loc] @@ loc in - let einit = init c in - let size = Lib.List32.length einit in - let size64 = Int64.of_int32 size in - let emode = Active {index = x; offset} @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, at, etype); tinit} @@ loc], - [{etype; einit; emode} @@ loc], - [], [] (* Custom annotations *) @@ -397,6 +364,14 @@ string_list : /* Types */ +%inline addr_type : + | NUM_TYPE + { match $1 with + | I32T -> I32AT + | I64T -> I64AT + | _ -> error (at $sloc) "malformed address type" } + | /* empty */ { I32AT } /* Sugar */ + null_opt : | /* empty */ { NoNull } | NULL { Null } @@ -501,12 +476,10 @@ sub_type : List.map (fun y -> VarHT (StatX y.it)) ($4 c type_), $5 c x) } table_type : - | val_type limits ref_type { fun c -> TableT ($2, addr_type_of_value_type ($1 c) $sloc, $3 c) } - | limits ref_type { fun c -> TableT ($1, I32AddrType, $2 c) } + | addr_type limits ref_type { fun c -> TableT ($1, $2, $3 c) } memory_type : - | val_type limits { fun c -> MemoryT ($2, addr_type_of_value_type ($1 c) $sloc) } - | limits { fun c -> MemoryT ($1, I32AddrType) } + | addr_type limits { fun c -> MemoryT ($1, $2) } limits : | NAT { {min = nat64 $1 $loc($1); max = None} } @@ -1156,28 +1129,28 @@ table_fields : | inline_export table_fields /* Sugar */ { fun c x loc -> let tabs, elems, ims, exs = $2 c x loc in tabs, elems, ims, $1 (TableExport x) c :: exs } - | ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ + | addr_type ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ { fun c x loc -> - let offset = [i32_const (0l @@ loc) @@ loc] @@ loc in - let einit = $4 c :: $5 c in - let size = Lib.List32.length einit in - let size64 = Int64.of_int32 size in + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + let einit = $5 c :: $6 c in + let size = Lib.List64.length einit in let emode = Active {index = x; offset} @@ loc in - let (_, ht) as etype = $1 c in + let (_, ht) as etype = $2 c in let tinit = [RefNull ht @@ loc] @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, I32AddrType, etype); tinit} @@ loc], + [{ttype = TableT ($1, {min = size; max = Some size}, etype); tinit} @@ loc], [{etype; einit; emode} @@ loc], [], [] } - | ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ - { fun c x loc -> - let (_, ht) as etype = $1 c in - let tinit = [RefNull ht @@ loc] @@ loc in - table_data tinit $4 I32AddrType etype c x loc } - | val_type ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ + | addr_type ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ { fun c x loc -> let (_, ht) as etype = $2 c in let tinit = [RefNull ht @@ loc] @@ loc in - table_data tinit $5 (addr_type_of_value_type ($1 c) loc) etype c x loc } + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + let einit = $5 c in + let size = Lib.List64.length einit in + let emode = Active {index = x; offset} @@ loc in + [{ttype = TableT ($1, {min = size; max = Some size}, etype); tinit} @@ loc], + [{etype; einit; emode} @@ loc], + [], [] } data : | LPAR DATA bind_var_opt string_list RPAR @@ -1208,10 +1181,13 @@ memory_fields : | inline_export memory_fields /* Sugar */ { fun c x loc -> let mems, data, ims, exs = $2 c x loc in mems, data, ims, $1 (MemoryExport x) c :: exs } - | LPAR DATA string_list RPAR /* Sugar */ - { memory_data $3 I32AddrType } - | val_type LPAR DATA string_list RPAR /* Sugar */ - { fun c x loc -> memory_data $4 (addr_type_of_value_type ($1 c) $sloc) c x loc } + | addr_type LPAR DATA string_list RPAR /* Sugar */ + { fun c x loc -> + let size = Int64.(div (add (of_int (String.length $4)) 65535L) 65536L) in + let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in + [{mtype = MemoryT ($1, {min = size; max = Some size})} @@ loc], + [{dinit = $4; dmode = Active {index = x; offset} @@ loc} @@ loc], + [], [] } tag : | LPAR TAG bind_var_opt tag_fields RPAR diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index b2cc266305..7d889b899b 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -161,11 +161,12 @@ let match_global_type c (GlobalT (mut1, t1)) (GlobalT (mut2, t2)) = | Cons -> true | Var -> match_val_type c t2 t1 -let match_table_type c (TableT (lim1, at1, t1)) (TableT (lim2, at2, t2)) = - match_limits c lim1 lim2 && at1 = at2 && match_ref_type c t1 t2 && match_ref_type c t2 t1 +let match_table_type c (TableT (at1, lim1, t1)) (TableT (at2, lim2, t2)) = + at1 = at2 && match_limits c lim1 lim2 && + match_ref_type c t1 t2 && match_ref_type c t2 t1 -let match_memory_type c (MemoryT (lim1, at1)) (MemoryT (lim2, at2)) = - match_limits c lim1 lim2 && at1 = at2 +let match_memory_type c (MemoryT (at1, lim1)) (MemoryT (at2, lim2)) = + at1 = at2 && match_limits c lim1 lim2 let match_tag_type c (TagT dt1) (TagT dt2) = match_def_type c dt1 dt2 && match_def_type c dt2 dt1 diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 6fc75ace72..ba4e8bb550 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -89,13 +89,13 @@ let refer_func (c : context) x = refer "function" c.refs.Free.funcs x (* Types *) -let check_limits le_u {min; max} range at msg = - require (le_u min range) at msg; +let check_limits {min; max} range at msg = + require (I64.le_u min range) at msg; match max with | None -> () | Some max -> - require (le_u max range) at msg; - require (le_u min max) at + require (I64.le_u max range) at msg; + require (I64.le_u min max) at "size minimum must not be greater than maximum" let check_num_type (c : context) (t : num_type) at = @@ -151,30 +151,29 @@ let check_func_type (c : context) (ft : func_type) at = check_result_type c ts2 at let check_table_type (c : context) (tt : table_type) at = - let TableT (lim, _at, t) = tt in + let TableT (at_, lim, t) = tt in check_ref_type c t at; - match _at with - | I64AddrType -> - check_limits I64.le_u lim 0xffff_ffff_ffff_ffffL at - "table size must be at most 2^64-1" - | I32AddrType -> - check_limits I64.le_u lim 0xffff_ffffL at - "table size must be at most 2^32-1" + let sz, s = + match at_ with + | I32AT -> 0xffff_ffffL, "2^32-1 for i32" + | I64AT -> 0xffff_ffff_ffff_ffffL, "2^64-1 for i64" + in + check_limits lim sz at ("table size must be at most " ^ s) let check_memory_type (c : context) (mt : memory_type) at = - let MemoryT (lim, _at) = mt in - match _at with - | I32AddrType -> - check_limits I64.le_u lim 0x1_0000L at - "memory size must be at most 65536 pages (4GiB)" - | I64AddrType -> - check_limits I64.le_u lim 0x1_0000_0000_0000L at - "memory size must be at most 48 bits of pages" + let MemoryT (at_, lim) = mt in + let sz, s = + match at_ with + | I32AT -> 0x1_0000L, "2^16 pages (4 GiB) for i32" + | I64AT -> 0x1_0000_0000_0000L, "2^48 pages (256 TiB) for i64" + in + check_limits lim sz at ("memory size must be at most " ^ s) let check_global_type (c : context) (gt : global_type) at = let GlobalT (_mut, t) = gt in check_val_type c t at + let check_str_type (c : context) (st : str_type) at = match st with | DefStructT st -> check_struct_type c st at @@ -370,8 +369,8 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at = in require (1 lsl memop.align >= 1 && 1 lsl memop.align <= size) at "alignment must not be larger than natural"; - let MemoryT (_lim, _at) = memory c (0l @@ at) in - if _at = I32AddrType then + let MemoryT (at_, _lim) = memory c (0l @@ at) in + if at_ = I32AT then require (I64.lt_u memop.offset 0x1_0000_0000L) at "offset out of range"; memop.ty @@ -518,12 +517,12 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in (ts1 @ [RefT (Null, DefHT (type_ c x))]) --> ts2, [] | CallIndirect (x, y) -> - let TableT (lim, at, t) = table c x in + let TableT (at, _lim, t) = table c x in let FuncT (ts1, ts2) = func_type c y in require (match_ref_type c.types t (Null, FuncHT)) x.at ("type mismatch: instruction requires table of function type" ^ " but table has element type " ^ string_of_ref_type t); - (ts1 @ [value_type_of_addr_type at]) --> ts2, [] + (ts1 @ [NumT (num_type_of_addr_type at)]) --> ts2, [] | ReturnCall x -> let FuncT (ts1, ts2) = as_func_str_type (expand_def_type (func c x)) in @@ -542,13 +541,13 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in (ts1 @ [RefT (Null, DefHT (type_ c x))]) -->... [], [] | ReturnCallIndirect (x, y) -> - let TableT (_lim, at, t) = table c x in + let TableT (at, _lim, t) = table c x in let FuncT (ts1, ts2) = func_type c y in require (match_result_type c.types ts2 c.results) e.at ("type mismatch: current function requires result type " ^ string_of_result_type c.results ^ " but callee returns " ^ string_of_result_type ts2); - (ts1 @ [value_type_of_addr_type at]) -->... [], [] + (ts1 @ [NumT (num_type_of_addr_type at)]) -->... [], [] | Throw x -> let TagT dt = tag c x in @@ -588,102 +587,105 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in [t] --> [], [] | TableGet x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at] --> [RefT rt], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at)] --> [RefT rt], [] | TableSet x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at; RefT rt] --> [], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at); RefT rt] --> [], [] | TableSize x -> - let TableT (_lim, at, _rt) = table c x in - [] --> [value_type_of_addr_type at], [] + let TableT (at, _lim, _rt) = table c x in + [] --> [NumT (num_type_of_addr_type at)], [] | TableGrow x -> - let TableT (_lim, at, rt) = table c x in - [RefT rt; value_type_of_addr_type at] --> [value_type_of_addr_type at], [] + let TableT (at, _lim, rt) = table c x in + [RefT rt; NumT (num_type_of_addr_type at)] --> + [NumT (num_type_of_addr_type at)], [] | TableFill x -> - let TableT (_lim, at, rt) = table c x in - [value_type_of_addr_type at; RefT rt; value_type_of_addr_type at] --> [], [] + let TableT (at, _lim, rt) = table c x in + [NumT (num_type_of_addr_type at); RefT rt; + NumT (num_type_of_addr_type at)] --> [], [] | TableCopy (x, y) -> - let TableT (_lim1, at1, t1) = table c x in - let TableT (_lim2, at2, t2) = table c y in - let at_min = min at1 at2 in + let TableT (at1, _lim1, t1) = table c x in + let TableT (at2, _lim2, t2) = table c y in require (match_ref_type c.types t2 t1) x.at ("type mismatch: source element type " ^ string_of_ref_type t1 ^ " does not match destination element type " ^ string_of_ref_type t2); - [value_type_of_addr_type at1; value_type_of_addr_type at2; value_type_of_addr_type at_min] --> [], [] + [NumT (num_type_of_addr_type at1); NumT (num_type_of_addr_type at2); + NumT (num_type_of_addr_type (min at1 at2))] --> [], [] | TableInit (x, y) -> - let TableT (_lim1, at, t1) = table c x in + let TableT (at, _lim1, t1) = table c x in let t2 = elem c y in require (match_ref_type c.types t2 t1) x.at ("type mismatch: element segment's type " ^ string_of_ref_type t1 ^ " does not match table's element type " ^ string_of_ref_type t2); - [value_type_of_addr_type at; NumT I32T; NumT I32T] --> [], [] + [NumT (num_type_of_addr_type at); NumT I32T; NumT I32T] --> [], [] | ElemDrop x -> ignore (elem c x); [] --> [], [] | Load (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop num_size (Lib.Option.map fst) e.at in - [value_type_of_addr_type at] --> [NumT t], [] + [NumT (num_type_of_addr_type at)] --> [NumT t], [] | Store (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop num_size (fun sz -> sz) e.at in - [value_type_of_addr_type at; NumT t] --> [], [] + [NumT (num_type_of_addr_type at); NumT t] --> [], [] | VecLoad (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in - [value_type_of_addr_type at] --> [VecT t], [] + [NumT (num_type_of_addr_type at)] --> [VecT t], [] | VecStore (x, memop) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (fun _ -> None) e.at in - [value_type_of_addr_type at; VecT t] --> [], [] + [NumT (num_type_of_addr_type at); VecT t] --> [], [] | VecLoadLane (x, memop, i) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; - [value_type_of_addr_type at; VecT t] --> [VecT t], [] + [NumT (num_type_of_addr_type at); VecT t] --> [VecT t], [] | VecStoreLane (x, memop, i) -> - let MemoryT (_lim, at) = memory c x in + let MemoryT (at, _lim) = memory c x in let t = check_memop c memop vec_size (fun sz -> Some sz) e.at in require (i < vec_size t / Pack.packed_size memop.pack) e.at "invalid lane index"; - [value_type_of_addr_type at; VecT t] --> [], [] + [NumT (num_type_of_addr_type at); VecT t] --> [], [] | MemorySize x -> - let MemoryT (_lim, at) = memory c x in - [] --> [value_type_of_addr_type at], [] + let MemoryT (at, _lim) = memory c x in + [] --> [NumT (num_type_of_addr_type at)], [] | MemoryGrow x -> - let MemoryT (_lim, at) = memory c x in - [value_type_of_addr_type at] --> [value_type_of_addr_type at], [] + let MemoryT (at, _lim) = memory c x in + [NumT (num_type_of_addr_type at)] --> [NumT (num_type_of_addr_type at)], [] | MemoryFill x -> - let MemoryT (_lim, at) = memory c x in - [value_type_of_addr_type at; NumT I32T; value_type_of_addr_type at] --> [], [] + let MemoryT (at, _lim) = memory c x in + [NumT (num_type_of_addr_type at); NumT I32T; + NumT (num_type_of_addr_type at)] --> [], [] | MemoryCopy (x, y)-> - let MemoryT (_lib1, at1) = memory c x in - let MemoryT (_lib2, at2) = memory c y in - let at_min = min at1 at2 in - [value_type_of_addr_type at1; value_type_of_addr_type at2; value_type_of_addr_type at_min] --> [], [] + let MemoryT (at1, _lib1) = memory c x in + let MemoryT (at2, _lib2) = memory c y in + [NumT (num_type_of_addr_type at1); NumT (num_type_of_addr_type at2); + NumT (num_type_of_addr_type (min at1 at2))] --> [], [] | MemoryInit (x, y) -> - let MemoryT (_lib, at) = memory c x in + let MemoryT (at, _lib) = memory c x in let () = data c y in - [value_type_of_addr_type at; NumT I32T; NumT I32T] --> [], [] + [NumT (num_type_of_addr_type at); NumT I32T; NumT I32T] --> [], [] | DataDrop x -> let () = data c x in @@ -1029,7 +1031,7 @@ let check_global (c : context) (glob : global) : context = let check_table (c : context) (tab : table) : context = let {ttype; tinit} = tab.it in - let TableT (_lim, _at, rt) = ttype in + let TableT (_at, _lim, rt) = ttype in check_table_type c ttype tab.at; check_const c tinit (RefT rt); {c with tables = c.tables @ [ttype]} @@ -1048,11 +1050,11 @@ let check_elem_mode (c : context) (t : ref_type) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let TableT (_lim, at, et) = table c index in + let TableT (at, _lim, et) = table c index in require (match_ref_type c.types t et) mode.at ("type mismatch: element segment's type " ^ string_of_ref_type t ^ " does not match table's element type " ^ string_of_ref_type et); - check_const c offset (value_type_of_addr_type at) + check_const c offset (NumT (num_type_of_addr_type at)) | Declarative -> () let check_elem (c : context) (seg : elem_segment) : context = @@ -1066,8 +1068,8 @@ let check_data_mode (c : context) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let MemoryT (_, at) = memory c index in - check_const c offset (value_type_of_addr_type at) + let MemoryT (at, _) = memory c index in + check_const c offset (NumT (num_type_of_addr_type at)) | Declarative -> assert false let check_data (c : context) (seg : data_segment) : context = diff --git a/test/core/memory.wast b/test/core/memory.wast index 1c57a8f350..e01170a8f4 100644 --- a/test/core/memory.wast +++ b/test/core/memory.wast @@ -50,40 +50,53 @@ ) (assert_invalid (module (memory 65537)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 2147483648)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 4294967295)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 65537)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 2147483648)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid (module (memory 0 4294967295)) - "memory size must be at most 65536 pages (4GiB)" + "memory size" ) (assert_invalid - (module quote "(memory 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0x1_0000_0000)) + "memory size" ) (assert_invalid - (module quote "(memory 0x1_0000_0000 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0x1_0000_0000 0x1_0000_0000)) + "memory size" ) (assert_invalid - (module quote "(memory 0 0x1_0000_0000)") - "memory size must be at most 65536 pages (4GiB)" + (module (memory 0 0x1_0000_0000)) + "memory size" +) + +(assert_invalid + (module (memory (import "M" "m") 0x1_0000_0000)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") 0x1_0000_0000 0x1_0000_0000)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") 0 0x1_0000_0000)) + "memory size" ) (module diff --git a/test/core/memory64.wast b/test/core/memory64.wast index 41e1bf034b..ba3b242335 100644 --- a/test/core/memory64.wast +++ b/test/core/memory64.wast @@ -48,6 +48,24 @@ "size minimum must not be greater than maximum" ) +(assert_invalid + (module (memory i64 0x1_0000_0000_0001)) + "memory size" +) +(assert_invalid + (module (memory i64 0 0x1_0000_0000_0001)) + "memory size" +) + +(assert_invalid + (module (memory (import "M" "m") i64 0x1_0000_0000_0001)) + "memory size" +) +(assert_invalid + (module (memory (import "M" "m") i64 0 0x1_0000_0000_0001)) + "memory size" +) + (module (memory i64 1) (data (i64.const 0) "ABC\a7D") (data (i64.const 20) "WASM") diff --git a/test/core/table.wast b/test/core/table.wast index 8648df0705..a0feefff9c 100644 --- a/test/core/table.wast +++ b/test/core/table.wast @@ -33,15 +33,15 @@ (assert_invalid (module quote "(table 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) (assert_invalid (module quote "(table 0x1_0000_0000 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) (assert_invalid (module quote "(table 0 0x1_0000_0000 funcref)") - "table size must be at most 2^32-1" + "table size" ) ;; Same as above but with i64 address types