From 4056ff9582da36059c794ee54b3e825f76828bb1 Mon Sep 17 00:00:00 2001 From: Ben Visness Date: Fri, 18 Oct 2024 11:09:25 +0100 Subject: [PATCH] Rename "index type" to "address type" across the spec (#90) * Rename "index type" to "address type" across the spec * Update "index type" to "address type" in the spec interpreter * Update section underlines It is very important that you have precisely the correct number of dots. It would be too much work for the computer otherwise. * Rename "address type" to "addr type" in the spec interpreter * Revert one stray interpreter update --- document/core/appendix/properties.rst | 24 +- document/core/binary/types.rst | 6 +- document/core/exec/instructions.rst | 342 +++++++++++++------------- document/core/exec/modules.rst | 32 +-- document/core/syntax/types.rst | 30 +-- document/core/text/modules.rst | 8 +- document/core/text/types.rst | 20 +- document/core/util/macros.def | 6 +- document/core/valid/instructions.rst | 232 ++++++++--------- document/core/valid/matching.rst | 14 +- document/core/valid/types.rst | 18 +- document/js-api/index.bs | 78 +++--- interpreter/binary/decode.ml | 6 +- interpreter/binary/encode.ml | 10 +- interpreter/exec/eval.ml | 8 +- interpreter/host/spectest.ml | 6 +- interpreter/runtime/memory.ml | 18 +- interpreter/runtime/memory.mli | 2 +- interpreter/runtime/table.ml | 22 +- interpreter/runtime/table.mli | 2 +- interpreter/runtime/value.ml | 8 +- interpreter/syntax/free.ml | 4 +- interpreter/syntax/types.ml | 26 +- interpreter/text/arrange.ml | 10 +- interpreter/text/parser.mly | 52 ++-- interpreter/valid/match.ml | 8 +- interpreter/valid/valid.ml | 118 ++++----- proposals/memory64/Overview.md | 136 +++++----- test/core/table.wast | 2 +- test/js-api/table/constructor.any.js | 4 +- 30 files changed, 626 insertions(+), 626 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 2413b638f..79a530edd 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -513,10 +513,10 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow .. index:: table type, table instance, limits, function address .. _valid-tableinst: -:ref:`Table Instances ` :math:`\{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^\ast \}` -...................................................................................................... +:ref:`Table Instances ` :math:`\{ \TITYPE~\addrtype~\limits~t, \TIELEM~\reff^\ast \}` +....................................................................................................... -* The :ref:`table type ` :math:`\idxtype~\limits~t` must be :ref:`valid ` under the empty :ref:`context `. +* The :ref:`table type ` :math:`\addrtype~\limits~t` must be :ref:`valid ` under the empty :ref:`context `. * The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`. @@ -526,11 +526,11 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow * The :ref:`reference type ` :math:`t'_i` must :ref:`match ` the :ref:`reference type ` :math:`t`. -* Then the table instance is valid with :ref:`table type ` :math:`\idxtype~\limits~t`. +* Then the table instance is valid with :ref:`table type ` :math:`\addrtype~\limits~t`. .. math:: \frac{ - \vdashtabletype \idxtype~\limits~t \ok + \vdashtabletype \addrtype~\limits~t \ok \qquad n = \limits.\LMIN \qquad @@ -538,29 +538,29 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow \qquad (\vdashreftypematch t' \matchesvaltype t)^n }{ - S \vdashtableinst \{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^n \} : \idxtype~\limits~t + S \vdashtableinst \{ \TITYPE~\addrtype~\limits~t, \TIELEM~\reff^n \} : \addrtype~\limits~t } .. index:: memory type, memory instance, limits, byte .. _valid-meminst: -:ref:`Memory Instances ` :math:`\{ \MITYPE~\idxtype~\limits, \MIDATA~b^\ast \}` -............................................................................................... +:ref:`Memory Instances ` :math:`\{ \MITYPE~\addrtype~\limits, \MIDATA~b^\ast \}` +................................................................................................ -* The :ref:`memory type ` :math:`\idxtype~\limits` must be :ref:`valid ` under the empty :ref:`context `. +* The :ref:`memory type ` :math:`\addrtype~\limits` must be :ref:`valid ` under the empty :ref:`context `. * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size ` :math:`64\,\F{Ki}`. -* Then the memory instance is valid with :ref:`memory type ` :math:`\idxtype~\limits`. +* Then the memory instance is valid with :ref:`memory type ` :math:`\addrtype~\limits`. .. math:: \frac{ - \vdashmemtype \idxtype~\limits \ok + \vdashmemtype \addrtype~\limits \ok \qquad n = \limits.\LMIN \cdot 64\,\F{Ki} }{ - S \vdashmeminst \{ \MITYPE~\idxtype~\limits, \MIDATA~b^n \} : \idxtype~\limits + S \vdashmeminst \{ \MITYPE~\addrtype~\limits, \MIDATA~b^n \} : \addrtype~\limits } diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 2df479d38..d5501ec48 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 corresponsing index type. +:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and the corresponding :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{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\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{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\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 2b8cc7494..9cab86746 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2725,11 +2725,11 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~i` from the stack. +8. 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: @@ -2743,12 +2743,12 @@ Table Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \val + S; F; (\X{at}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \val \end{array} \\ \qquad (\iff S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \val) \\ \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2770,15 +2770,15 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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. 8. Pop the value :math:`\val` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{it}.\CONST~i` from the stack. +10. 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: @@ -2790,12 +2790,12 @@ Table Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S'; F; \epsilon + S; F; (\X{at}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S'; F; \epsilon \end{array} \\ \qquad (\iff S' = S \with \STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \val) \\ \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2817,16 +2817,16 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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:`\X{tab}.\TIELEM`. -8. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. +8. Push the value :math:`\X{at}.\CONST~\X{sz}` to the stack. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\TABLESIZE~x) &\stepto& S; F; (\X{it}.\CONST~\X{sz}) + 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}) \\ @@ -2849,39 +2849,39 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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]`. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{it}.\CONST~n` from the stack. +9. Pop the value :math:`\X{at}.\CONST~n` from the stack. 10. 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. -12. Let :math:`\X{err}` be the :math:`\X{it}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +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`. 13. Either: a. If :ref:`growing ` :math:`\X{tab}` by :math:`n` entries with initialization value :math:`\val` succeeds, then: - i. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. + i. Push the value :math:`\X{at}.\CONST~\X{sz}` to the stack. b. Else: - i. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. + i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. 14. Or: - a. push the value :math:`\X{it}.\CONST~\X{err}` to the stack. + a. push the value :math:`\X{at}.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \val~(\X{it}.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\X{it}.\CONST~\X{sz}) + S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -2891,7 +2891,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; \val~(\X{it}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{it}.\CONST~\signed_{32}^{-1}(-1)) + S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -2919,19 +2919,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~n` from the stack. +8. Pop the value :math:`\X{at}.\CONST~n` from 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. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +11. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -12. Pop the value :math:`\X{it}.\CONST~i` from the stack. +12. 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: @@ -2941,40 +2941,40 @@ Table Instructions a. Return. -14. Push the value :math:`\X{it}.\CONST~i` to the stack. +14. Push the value :math:`\X{at}.\CONST~i` to the stack. 15. Push the value :math:`\val` to the stack. 16. Execute the instruction :math:`\TABLESET~x`. -17. Push the value :math:`\X{it}.\CONST~(i+1)` to the stack. +17. Push the value :math:`\X{at}.\CONST~(i+1)` to the stack. 18. Push the value :math:`\val` to the stack. -19. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. +19. Push the value :math:`\X{at}.\CONST~(n-1)` to the stack. 20. Execute the instruction :math:`\TABLEFILL~x`. .. math:: \begin{array}{l} - S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~n)~(\TABLEFILL~x) + S; F; (\X{at}.\CONST~i)~\val~(\X{at}.\CONST~n)~(\TABLEFILL~x) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & i + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~0)~(\TABLEFILL~x) + S; F; (\X{at}.\CONST~i)~\val~(\X{at}.\CONST~0)~(\TABLEFILL~x) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~n+1)~(\TABLEFILL~x) + S; F; (\X{at}.\CONST~i)~\val~(\X{at}.\CONST~n+1)~(\TABLEFILL~x) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}.\CONST~i)~\val~(\TABLESET~x) \\ - (\X{it}.\CONST~i+1)~\val~(\X{it}.\CONST~n)~(\TABLEFILL~x) \\ + (\X{at}.\CONST~i)~\val~(\TABLESET~x) \\ + (\X{at}.\CONST~i+1)~\val~(\X{at}.\CONST~n)~(\TABLEFILL~x) \\ \end{array} \\ \qquad (\otherwise) \\ @@ -3004,23 +3004,23 @@ Table Instructions 9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. -10. Let :math:`\X{it}_x~\limits_x` be the :ref:`table type ` :math:`\X{tab}_x.\TITYPE`. +10. Let :math:`\X{at}_x~\limits_x` be the :ref:`table type ` :math:`\X{tab}_x.\TITYPE`. -11. Let :math:`\X{it}_y~\limits_y` be the :ref:`table type ` :math:`\X{tab}_y.\TITYPE`. +11. Let :math:`\X{at}_y~\limits_y` be the :ref:`table type ` :math:`\X{tab}_y.\TITYPE`. -12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. +12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_x` and :math:`\X{at}_y`. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_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. -14. Pop the value :math:`\X{it}_n.\CONST~n` from the stack. +14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_y` 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. -16. Pop the value :math:`\X{it}_y.\CONST~s` from the stack. +16. Pop the value :math:`\X{at}_y.\CONST~s` from the stack. -17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_x` 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. -18. Pop the value :math:`\X{it}_x.\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: @@ -3032,9 +3032,9 @@ Table Instructions 21. If :math:`d \leq s`, then: - a. Push the value :math:`\X{it}_x.\CONST~d` to the stack. + a. Push the value :math:`\X{at}_x.\CONST~d` to the stack. - b. Push the value :math:`\X{it}_y.\CONST~s` to the stack. + b. Push the value :math:`\X{at}_y.\CONST~s` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. @@ -3042,38 +3042,38 @@ Table Instructions e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\X{it}_x.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{at}_x.\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{it}_y.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{at}_y.\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{it}_x.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{at}_x.\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{it}_y.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{at}_y.\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{it}_x.\CONST~d` to the stack. + g. Push the value :math:`\X{at}_x.\CONST~d` to the stack. - h. Push the value :math:`\X{it}_y.\CONST~s` to the stack. + h. Push the value :math:`\X{at}_y.\CONST~s` to the stack. -23. Push the value :math:`\X{it}_n.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. 24. Execute the instruction :math:`\TABLECOPY~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3081,27 +3081,27 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~0)~(\TABLECOPY~x~y) + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~0)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{it}_x.\CONST~d+1)~(\X{it}_y.\CONST~s+1)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\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) \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}_x.\CONST~d+n)~(\X{it}_y.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\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) \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -3123,7 +3123,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +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. @@ -3141,9 +3141,9 @@ Table Instructions 14. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{it}.\CONST~d` from the stack. +16. 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: @@ -3155,7 +3155,7 @@ Table Instructions 19. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. -20. Push the value :math:`\X{it}.\CONST~d` to the stack. +20. Push the value :math:`\X{at}.\CONST~d` to the stack. 21. Push the value :math:`\val` to the stack. @@ -3163,7 +3163,7 @@ Table Instructions 23. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. +24. 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}`. @@ -3176,7 +3176,7 @@ Table Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3184,17 +3184,17 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}.\CONST~d)~\val~(\TABLESET~x) \\ - (\X{it}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\ + (\X{at}.\CONST~d)~\val~(\TABLESET~x) \\ + (\X{at}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff \val = S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM[s]) \\ @@ -3260,11 +3260,11 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~i` from the stack. +8. Pop the value :math:`\X{at}.\CONST~i` from the stack. 9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3294,7 +3294,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\LOAD~x~\memarg) &\stepto& S; F; (t.\CONST~c) + S; F; (\X{at}.\CONST~i)~(t.\LOAD~x~\memarg) &\stepto& S; F; (t.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3304,7 +3304,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\LOAD{N}\K{\_}\sx~x~\memarg) &\stepto& + S; F; (\X{at}.\CONST~i)~(t.\LOAD{N}\K{\_}\sx~x~\memarg) &\stepto& S; F; (t.\CONST~\extend^{\sx}_{N,|t|}(n)) \end{array} \\ \qquad @@ -3315,7 +3315,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3337,11 +3337,11 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~i` from the stack. +8. Pop the value :math:`\X{at}.\CONST~i` from the stack. 9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3365,7 +3365,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\_\sx~x~\memarg) &\stepto& + S; F; (\X{at}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\_\sx~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad @@ -3378,7 +3378,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3400,11 +3400,11 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~i` from the stack. +8. Pop the value :math:`\X{at}.\CONST~i` from the stack. 9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3426,7 +3426,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{at}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3437,7 +3437,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3459,11 +3459,11 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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{it}` 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. -8. Pop the value :math:`\X{it}.\CONST~i` from the stack. +8. Pop the value :math:`\X{at}.\CONST~i` from the stack. 9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3483,7 +3483,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{at}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3494,7 +3494,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3516,15 +3516,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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. 8. Pop the value :math:`\V128.\CONST~v` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{it}.\CONST~i` from the stack. +10. Pop the value :math:`\X{at}.\CONST~i` from the stack. 11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3548,7 +3548,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\CONST~v)~(\V128\K{.}\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{at}.\CONST~i)~(\V128.\CONST~v)~(\V128\K{.}\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3560,7 +3560,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3583,15 +3583,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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. 8. Pop the value :math:`t.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{it}.\CONST~i` from the stack. +10. Pop the value :math:`\X{at}.\CONST~i` from the stack. 11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3619,7 +3619,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE~x~\memarg) &\stepto& S'; F; \epsilon + S; F; (\X{at}.\CONST~i)~(t.\CONST~c)~(t.\STORE~x~\memarg) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3629,7 +3629,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}~x~\memarg) &\stepto& S'; F; \epsilon + S; F; (\X{at}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}~x~\memarg) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3639,7 +3639,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3661,15 +3661,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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. 8. Pop the value :math:`\V128.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{it}.\CONST~i` from the stack. +10. Pop the value :math:`\X{at}.\CONST~i` from the stack. 11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. @@ -3689,7 +3689,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S'; F; \epsilon + S; F; (\X{at}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3700,7 +3700,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP + S; F; (\X{at}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3722,16 +3722,16 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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:`\X{mem}.\MIDATA` divided by the :ref:`page size `. -8. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. +8. Push the value :math:`\X{at}.\CONST~\X{sz}` to the stack. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\MEMORYSIZE~x) &\stepto& S; F; (\X{it}.\CONST~\X{sz}) + 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}) \\ @@ -3754,35 +3754,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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 `. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{it}.\CONST~n` from the stack. +9. Pop the value :math:`\X{at}.\CONST~n` from the stack. -10. Let :math:`\X{err}` be the :math:`\X{it}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +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`. 11. Either: a. If :ref:`growing ` :math:`\X{mem}` by :math:`n` :ref:`pages ` succeeds, then: - i. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. + i. Push the value :math:`\X{at}.\CONST~\X{sz}` to the stack. b. Else: - i. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. + i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. 12. Or: - a. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. + a. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S'; F; (\X{it}.\CONST~\X{sz}) + S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S'; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3792,7 +3792,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{it}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{it}.\CONST~\signed_{32}^{-1}(-1)) + S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -3820,19 +3820,19 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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{it}` 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{it}.\CONST~n` from 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. 9. Pop the value :math:`\val` from the stack. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -11. Pop the value :math:`\X{it}.\CONST~d` from the stack. +11. Pop the value :math:`\X{at}.\CONST~d` from the stack. 12. If :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: @@ -3846,37 +3846,37 @@ Memory Instructions 15. Push the value :math:`\val` to the stack. -16. Execute the instruction :math:`\X{it}\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. +16. Execute the instruction :math:`\X{at}\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. 17. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -18. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. +18. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. 19. Push the value :math:`\val` to the stack. -20. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. +20. Push the value :math:`\X{at}.\CONST~(n-1)` to the stack. 21. Execute the instruction :math:`\MEMORYFILL~x`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~n)~\MEMORYFILL~x + S; F; (\X{at}.\CONST~d)~\val~(\X{at}.\CONST~n)~\MEMORYFILL~x \quad\stepto\quad S; F; \TRAP \\ \qquad (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\[1ex] - S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~0)~\MEMORYFILL~x + S; F; (\X{at}.\CONST~d)~\val~(\X{at}.\CONST~0)~\MEMORYFILL~x \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~n+1)~\MEMORYFILL~x + S; F; (\X{at}.\CONST~d)~\val~(\X{at}.\CONST~n+1)~\MEMORYFILL~x \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}.\CONST~d)~\val~(\X{it}\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\X{it}.\CONST~d+1)~\val~(\X{it}.\CONST~n)~\MEMORYFILL~x \\ + (\X{at}.\CONST~d)~\val~(\X{at}\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{at}.\CONST~d+1)~\val~(\X{at}.\CONST~n)~\MEMORYFILL~x \\ \end{array} \\ \qquad (\otherwise) \\ @@ -3906,23 +3906,23 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Let :math:`\X{it}_d~\limits_d` be the :ref:`memory type ` :math:`\X{mem}_d.\MITYPE`. +10. Let :math:`\X{at}_d~\limits_d` be the :ref:`memory type ` :math:`\X{mem}_d.\MITYPE`. -11. Let :math:`\X{it}_s~\limits_s` be the :ref:`memory type ` :math:`\X{mem}_s.\MITYPE`. +11. Let :math:`\X{at}_s~\limits_s` be the :ref:`memory type ` :math:`\X{mem}_s.\MITYPE`. -12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. +12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_s` and :math:`\X{at}_d`. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_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. -14. Pop the value :math:`\X{it}_n.\CONST~n` from the stack. +14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_s` 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. -16. Pop the value :math:`\X{it}_s.\CONST~s` 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{it}_d` is on the top of 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{it}_d.\CONST~d` from 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: @@ -3934,9 +3934,9 @@ Memory Instructions 21. If :math:`d \leq s`, then: - a. Push the value :math:`\X{it}_d.\CONST~d` to the stack. + a. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - b. Push the value :math:`\X{it}_s.\CONST~s` to the stack. + b. Push the value :math:`\X{at}_s.\CONST~s` to the stack. c. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. @@ -3944,38 +3944,38 @@ Memory Instructions e. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\X{it}_d.\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 memory size, :math:`s+1 < 2^{32}`. - h. Push the value :math:`\X{it}_s.\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 memory size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\X{it}_d.\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 memory size, :math:`s+n-1 < 2^{32}`. - d. Push the value :math:`\X{it}_s.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{at}_s.\CONST~(s+n-1)` to the stack. e. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. f. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. - g. Push the value :math:`\X{it}_d.\CONST~d` to the stack. + g. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - h. Push the value :math:`\X{it}_s.\CONST~s` to the stack. + h. Push the value :math:`\X{at}_s.\CONST~s` to the stack. -23. Push the value :math:`\X{it}_n.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. 24. Execute the instruction :math:`\MEMORYCOPY~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~\MEMORYCOPY~x~y \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3983,31 +3983,31 @@ Memory Instructions \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|)) \\ \end{array} \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~0)~\MEMORYCOPY~x~y + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~0)~\MEMORYCOPY~x~y \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~\MEMORYCOPY~x~y + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~\MEMORYCOPY~x~y \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}_x.\CONST~d) \\ - (\X{it}_y.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{at}_x.\CONST~d) \\ + (\X{at}_y.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\X{it}_x.\CONST~d+1)~(\X{it}_y.\CONST~s+1)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y \\ + (\X{at}_x.\CONST~d+1)~(\X{at}_y.\CONST~s+1)~(\X{at}_n.\CONST~n)~\MEMORYCOPY~x~y \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~\MEMORYCOPY~x~y + S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~\MEMORYCOPY~x~y \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}_x.\CONST~d+n) \\ - (\X{it}_y.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{at}_x.\CONST~d+n) \\ + (\X{at}_y.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y \\ + (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~\MEMORYCOPY~x~y \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -4029,7 +4029,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +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. @@ -4047,9 +4047,9 @@ Memory Instructions 14. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. +15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{it}.\CONST~d` from the stack. +16. 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: @@ -4061,7 +4061,7 @@ Memory Instructions 19. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. -20. Push the value :math:`\X{it}.\CONST~d` to the stack. +20. Push the value :math:`\X{at}.\CONST~d` to the stack. 21. Push the value :math:`\I32.\CONST~b` to the stack. @@ -4069,7 +4069,7 @@ Memory Instructions 23. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. +24. 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}`. @@ -4082,7 +4082,7 @@ Memory Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -4090,17 +4090,17 @@ Memory Instructions \vee & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\MIDATA|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x~y) + S; F; (\X{at}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{it}.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\X{it}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \\ + (\X{at}.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{at}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff b = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s]) \\ diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 85dbdb2b1..d40a22cfa 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -94,7 +94,7 @@ are *allocated* in a :ref:`store ` :math:`S`, as defined by the fo 1. Let :math:`\tabletype` be the :ref:`table type ` of the table to allocate and :math:`\reff` the initialization value. -2. Let :math:`(\idxtype~\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type ` :math:`\tabletype`. +2. Let :math:`(\addrtype~\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type ` :math:`\tabletype`. 3. Let :math:`a` be the first free :ref:`table address ` in :math:`S`. @@ -108,7 +108,7 @@ are *allocated* in a :ref:`store ` :math:`S`, as defined by the fo \begin{array}{rlll} \alloctable(S, \tabletype, \reff) &=& S', \tableaddr \\[1ex] \mbox{where:} \hfill \\ - \tabletype &=& \idxtype~\{\LMIN~n, \LMAX~m^?\}~\reftype \\ + \tabletype &=& \addrtype~\{\LMIN~n, \LMAX~m^?\}~\reftype \\ \tableaddr &=& |S.\STABLES| \\ \tableinst &=& \{ \TITYPE~\tabletype, \TIELEM~\reff^n \} \\ S' &=& S \compose \{\STABLES~\tableinst\} \\ @@ -123,7 +123,7 @@ are *allocated* in a :ref:`store ` :math:`S`, as defined by the fo 1. Let :math:`\memtype` be the :ref:`memory type ` of the memory to allocate. -2. Let :math:`(\idxtype~\{\LMIN~n, \LMAX~m^?\})` be the structure of :ref:`memory type ` :math:`\memtype`. +2. Let :math:`(\addrtype~\{\LMIN~n, \LMAX~m^?\})` be the structure of :ref:`memory type ` :math:`\memtype`. 3. Let :math:`a` be the first free :ref:`memory address ` in :math:`S`. @@ -137,7 +137,7 @@ are *allocated* in a :ref:`store ` :math:`S`, as defined by the fo \begin{array}{rlll} \allocmem(S, \memtype) &=& S', \memaddr \\[1ex] \mbox{where:} \hfill \\ - \memtype &=& \idxtype~\{\LMIN~n, \LMAX~m^?\} \\ + \memtype &=& \addrtype~\{\LMIN~n, \LMAX~m^?\} \\ \memaddr &=& |S.\SMEMS| \\ \meminst &=& \{ \MITYPE~\memtype, \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \} \\ S' &=& S \compose \{\SMEMS~\meminst\} \\ @@ -284,25 +284,25 @@ Growing :ref:`tables ` 2. Let :math:`\X{len}` be :math:`n` added to the length of :math:`\tableinst.\TIELEM`. -3. Let :math:`(\idxtype~\limits~\reftype)` be the structure of :ref:`table type ` :math:`\tableinst.\TITYPE`. +3. Let :math:`(\addrtype~\limits~\reftype)` be the structure of :ref:`table type ` :math:`\tableinst.\TITYPE`. 4. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`. -5. If the :ref:`table type ` :math:`(\idxtype~\limits'~\reftype)` is not :ref:`valid `, then fail. +5. If the :ref:`table type ` :math:`(\addrtype~\limits'~\reftype)` is not :ref:`valid `, then fail. 6. Append :math:`\reff^n` to :math:`\tableinst.\TIELEM`. -7. Set :math:`\tableinst.\TITYPE` to the :ref:`table type ` :math:`(\idxtype~\limits'~\reftype)`. +7. Set :math:`\tableinst.\TITYPE` to the :ref:`table type ` :math:`(\addrtype~\limits'~\reftype)`. .. math:: \begin{array}{rllll} - \growtable(\tableinst, n, \reff) &=& \tableinst \with \TITYPE = \idxtype~\limits'~\reftype \with \TIELEM = \tableinst.\TIELEM~\reff^n \\ + \growtable(\tableinst, n, \reff) &=& \tableinst \with \TITYPE = \addrtype~\limits'~\reftype \with \TIELEM = \tableinst.\TIELEM~\reff^n \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \iff & \X{len} = n + |\tableinst.\TIELEM| \\ - \wedge & \idxtype~\limits~\reftype = \tableinst.\TITYPE \\ + \wedge & \addrtype~\limits~\reftype = \tableinst.\TITYPE \\ \wedge & \limits' = \limits \with \LMIN = \X{len} \\ - \wedge & \vdashtabletype \idxtype~\limits'~\reftype \ok) \\ + \wedge & \vdashtabletype \addrtype~\limits'~\reftype \ok) \\ \end{array} \\ \end{array} @@ -319,25 +319,25 @@ Growing :ref:`memories ` 3. Let :math:`\X{len}` be :math:`n` added to the length of :math:`\meminst.\MIDATA` divided by the :ref:`page size ` :math:`64\,\F{Ki}`. -4. Let :math:`(\idxtype~\limits)` be the structure of :ref:`memory type ` :math:`\meminst.\MITYPE`. +4. Let :math:`(\addrtype~\limits)` be the structure of :ref:`memory type ` :math:`\meminst.\MITYPE`. 5. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`. -6. If the :ref:`memory type ` :math:`(\idxtype~\limits')` is not :ref:`valid `, then fail. +6. If the :ref:`memory type ` :math:`(\addrtype~\limits')` is not :ref:`valid `, then fail. 7. Append :math:`n` times :math:`64\,\F{Ki}` :ref:`bytes ` with value :math:`\hex{00}` to :math:`\meminst.\MIDATA`. -8. Set :math:`\meminst.\MITYPE` to the :ref:`memory type ` :math:`(\idxtype~\limits')`. +8. Set :math:`\meminst.\MITYPE` to the :ref:`memory type ` :math:`(\addrtype~\limits')`. .. math:: \begin{array}{rllll} - \growmem(\meminst, n) &=& \meminst \with \MITYPE = \idxtype~\limits' \with \MIDATA = \meminst.\MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \\ + \growmem(\meminst, n) &=& \meminst \with \MITYPE = \addrtype~\limits' \with \MIDATA = \meminst.\MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \iff & \X{len} = n + |\meminst.\MIDATA| / 64\,\F{Ki} \\ - \wedge & \idxtype~\limits = \meminst.\MITYPE \\ + \wedge & \addrtype~\limits = \meminst.\MITYPE \\ \wedge & \limits' = \limits \with \LMIN = \X{len} \\ - \wedge & \vdashmemtype \idxtype~\limits' \ok) \\ + \wedge & \vdashmemtype \addrtype~\limits' \ok) \\ \end{array} \\ \end{array} diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index b9b3b73d2..5e17179f2 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -357,36 +357,36 @@ In a :ref:`module `, each member of a recursive type is assigned The syntax of sub types is :ref:`generalized ` for the purpose of specifying :ref:`validation ` and :ref:`execution `. -.. _index:: ! index type - pair: abstract syntax; index type - single: memory; index type - single: table; index type -.. _syntax-idxtype: +.. _index:: ! address type + pair: abstract syntax; address type + single: memory; address type + single: table; address type +.. _syntax-addrtype: -Index Type -~~~~~~~~~~ +Address Type +~~~~~~~~~~~~ -*Index types* classify the values that can be used to index into +*Address types* classify the values that can be used to index into :ref:`memories ` and :ref:`tables `. .. math:: \begin{array}{llll} - \production{index type} & \idxtype &::=& + \production{address type} & \addrtype &::=& \I32 ~|~ \I64 \\ \end{array} -.. _aux-idxtype-min: +.. _aux-addrtype-min: Conventions ........... -The *minimum* of two index types is defined as |I32| if either of the types are +The *minimum* of two address types is defined as |I32| if either of the types are |I32|, and |I64| otherwise. .. math:: \begin{array}{llll} - \itmin(\I64, \I64) &=& \I64 \\ - \itmin(\X{it}_1, \X{it}_2) &=& \I32 & (\otherwise) \\ + \atmin(\I64, \I64) &=& \I64 \\ + \atmin(\X{at}_1, \X{at}_2) &=& \I32 & (\otherwise) \\ \end{array} @@ -424,7 +424,7 @@ Memory Types .. math:: \begin{array}{llrl} \production{memory type} & \memtype &::=& - ~\idxtype~\limits \\ + ~\addrtype~\limits \\ \end{array} The limits constrain the minimum and optionally the maximum size of a memory. @@ -445,7 +445,7 @@ Table Types .. math:: \begin{array}{llrl} \production{table type} & \tabletype &::=& - ~\idxtype~\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 c0cdc5e4f..3178332dd 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -378,12 +378,12 @@ A :ref:`data segment ` can be given inline with a memory definition, .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{memory}~~\Tid^?~~\X{it}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{memory}~~\Tid'~~\X{it}^?~~m~~m~\text{)} \\ & \qquad - \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{it}'\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} + \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{)} \\ & \qquad\qquad (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad - \iff it^? \neq \epsilon \wedge \X{it}' = \X{it}^? \vee \X{it}^? = \epsilon \wedge \X{it}' = \text{i32}, \\ & \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})), \\ \end{array} diff --git a/document/core/text/types.rst b/document/core/text/types.rst index 779d1c249..5c7e7386b 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -286,16 +286,16 @@ Similarly, final sub types with no super-types can omit the |Tsub| keyword and a \end{array} -.. index:: index type - pair: text format; index type -.. _text-idxtype: +.. index:: address type + pair: text format; address type +.. _text-addrtype: -Index Type -~~~~~~~~~~ +Address Types +~~~~~~~~~~~~~ .. math:: \begin{array}{llclll} - \production{index type} & \Tidxtype &::=& + \production{address type} & \Taddrtype &::=& \text{i32} &\Rightarrow& \I32 \\ &&|& \text{i64} &\Rightarrow& \I64 \\ \end{array} @@ -303,11 +303,11 @@ Index Type Abbreviations ............. -The index type can be omited, in which case it defaults :math:`\I32`: +The address type can be omited, in which case it defaults :math:`\I32`: .. math:: \begin{array}{llclll} - \production{index type} & + \production{address type} & \text{} &\equiv& \text{i32} \end{array} @@ -337,7 +337,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{memory type} & \Tmemtype_I &::=& - \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits &\Rightarrow& \X{it}~\X{lim} \\ + \X{at}{:}\Taddrtype~~\X{lim}{:}\Tlimits &\Rightarrow& \X{at}~\X{lim} \\ \end{array} @@ -351,7 +351,7 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Ttabletype_I &::=& - \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{it}~\X{lim}~\X{et} \\ + \X{at}{:}\Taddrtype~~\X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{at}~\X{lim}~\X{et} \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 30516d8ef..8aae38810 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -286,7 +286,7 @@ .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} -.. |idxtype| mathdef:: \xref{syntax/types}{syntax-idxtype}{\X{idxtype}} +.. |addrtype| mathdef:: \xref{syntax/types}{syntax-addrtype}{\X{addrtype}} .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}} .. |tagtype| mathdef:: \xref{syntax/types}{syntax-tagtype}{\X{tagtype}} @@ -311,7 +311,7 @@ .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}} -.. |itmin| mathdef:: \xref{syntax/types}{aux-idxtype-min}{\F{itmin}} +.. |atmin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{atmin}} .. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} @@ -972,7 +972,7 @@ .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}} .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}} -.. |Tidxtype| mathdef:: \xref{text/types}{text-idxtype}{\T{idxtype}} +.. |Taddrtype| mathdef:: \xref{text/types}{text-addrtype}{\T{addrtype}} .. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}} .. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 9f7b29c04..01e09d93c 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1395,15 +1395,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [t]`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t }{ - C \vdashinstr \TABLEGET~x : [\X{it}] \to [t] + C \vdashinstr \TABLEGET~x : [\X{at}] \to [t] } @@ -1414,15 +1414,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~t] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t }{ - C \vdashinstr \TABLESET~x : [\X{it}~t] \to [] + C \vdashinstr \TABLESET~x : [\X{at}~t] \to [] } @@ -1433,15 +1433,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[] \to [\X{it}]`. +* Then the instruction is valid with type :math:`[] \to [\X{at}]`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t }{ - C \vdashinstr \TABLESIZE~x : [] \to [\X{it}] + C \vdashinstr \TABLESIZE~x : [] \to [\X{at}] } @@ -1452,15 +1452,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[t~\X{it}] \to [\X{it}]`. +* Then the instruction is valid with type :math:`[t~\X{at}] \to [\X{at}]`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t }{ - C \vdashinstr \TABLEGROW~x : [t~\X{it}] \to [\X{it}] + C \vdashinstr \TABLEGROW~x : [t~\X{at}] \to [\X{at}] } @@ -1471,15 +1471,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\X{it}~t~\X{it}] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~t~\X{at}] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t }{ - C \vdashinstr \TABLEFILL~x : [\X{it}~t~\X{it}] \to [] + C \vdashinstr \TABLEFILL~x : [\X{at}~t~\X{at}] \to [] } @@ -1490,27 +1490,27 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}_1~\limits_1~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}_1~\limits_1~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The table :math:`C.\CTABLES[y]` must be defined in the context. -* Let :math:`\X{it}_2~\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. +* Let :math:`\X{at}_2~\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. -* Let :math:`\X{it}` be the :ref:`minimum ` of :math:`\X{it}_1` and :math:`\X{it}_2` +* 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{it}_1~\X{it}_2~\itmin(\X{it}_1, \X{it}_2)] \to []`. +* Then the instruction is valid with type :math:`[\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits_1~t_1 + C.\CTABLES[x] = \X{at}~\limits_1~t_1 \qquad - C.\CTABLES[y] = \X{it}~\limits_2~t_2 + C.\CTABLES[y] = \X{at}~\limits_2~t_2 \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLECOPY~x~y : [\X{it}_1~\X{it}_2~\itmin(\X{it}_1, \X{it}_2)] \to [] + C \vdashinstr \TABLECOPY~x~y : [\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to [] } @@ -1521,7 +1521,7 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The element segment :math:`C.\CELEMS[y]` must be defined in the context. @@ -1529,17 +1529,17 @@ Table Instructions * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\X{it}~\I32~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~\I32~\I32] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t_1 + C.\CTABLES[x] = \X{at}~\limits~t_1 \qquad C.\CELEMS[y] = t_2 \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLEINIT~x~y : [\X{it}~\I32~\I32] \to [] + C \vdashinstr \TABLEINIT~x~y : [\X{at}~\I32~\I32] \to [] } @@ -1576,23 +1576,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. -* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [t]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdashinstr t\K{.load}~x~\memarg : [\X{it}] \to [t] + C \vdashinstr t\K{.load}~x~\memarg : [\X{at}] \to [t] } @@ -1603,23 +1603,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [t]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\X{it}] \to [t] + C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\X{at}] \to [t] } @@ -1628,23 +1628,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. -* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~t] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdashinstr t\K{.store}~x~\memarg : [\X{it}~t] \to [] + C \vdashinstr t\K{.store}~x~\memarg : [\X{at}~t] \to [] } @@ -1655,23 +1655,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~t] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr t\K{.store}N~x~\memarg : [\X{it}~t] \to [] + C \vdashinstr t\K{.store}N~x~\memarg : [\X{at}~t] \to [] } @@ -1682,23 +1682,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8 \cdot M`. -* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [\V128]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 \cdot M }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\X{it}] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\X{at}] \to [\V128] } @@ -1709,23 +1709,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [\V128]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\X{it}] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\X{at}] \to [\V128] } @@ -1736,23 +1736,23 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [\V128]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\X{it}] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\X{at}] \to [\V128] } @@ -1763,27 +1763,27 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. * The lane index :math:`\laneidx` must be smaller than :math:`128/N`. -* Then the instruction is valid with type :math:`[\X{it}~\V128] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{at}~\V128] \to [\V128]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 \qquad \laneidx < 128/N }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx : [\X{it}~\V128] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx : [\X{at}~\V128] \to [\V128] } @@ -1794,27 +1794,27 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`. +* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{at}|}`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. * The lane index :math:`\laneidx` must be smaller than :math:`128/N`. -* Then the instruction is valid with type :math:`[\X{it}~\V128] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{at}~\V128] \to [\V128]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad - \memarg.\OFFSET < 2^{|\X{it}|} + \memarg.\OFFSET < 2^{|\X{at}|} \qquad 2^{\memarg.\ALIGN} \leq N/8 \qquad \laneidx < 128/N }{ - C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx : [\X{it}~\V128] \to [] + C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx : [\X{at}~\V128] \to [] } @@ -1825,15 +1825,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* Then the instruction is valid with type :math:`[] \to [\X{it}]`. +* Then the instruction is valid with type :math:`[] \to [\X{at}]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits }{ - C \vdashinstr \MEMORYSIZE~x : [] \to [\X{it}] + C \vdashinstr \MEMORYSIZE~x : [] \to [\X{at}] } @@ -1844,15 +1844,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* Then the instruction is valid with type :math:`[\X{it}] \to [\X{it}]`. +* Then the instruction is valid with type :math:`[\X{at}] \to [\X{at}]`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits }{ - C \vdashinstr \MEMORYGROW~x : [\X{it}] \to [\X{it}] + C \vdashinstr \MEMORYGROW~x : [\X{at}] \to [\X{at}] } @@ -1863,15 +1863,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* Then the instruction is valid with type :math:`[\X{it}~\I32~\X{it}] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~\I32~\X{at}] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits }{ - C \vdashinstr \MEMORYFILL~x : [\X{it}~\I32~\X{it}] \to [] + C \vdashinstr \MEMORYFILL~x : [\X{at}~\I32~\X{at}] \to [] } @@ -1884,21 +1884,21 @@ Memory Instructions * The memory :math:`C.\CMEMS[y]` must be defined in the context. -* Let :math:`\X{it}_x~\limits_x` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}_x~\limits_x` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* Let :math:`\X{it}_y~\limits_y` be the :ref:`memory type ` :math:`C.\CMEMS[y]`. +* Let :math:`\X{at}_y~\limits_y` be the :ref:`memory type ` :math:`C.\CMEMS[y]`. -* Let :math:`\X{it}` be the :ref:`minimum ` of :math:`\X{it}_x` and :math:`\X{it}_y` +* 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{it}_x~\X{it}_y~\itmin(\X{it}_x, \X{it}_y)] \to []`. +* Then the instruction is valid with type :math:`[\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}_x~\limits_y + C.\CMEMS[x] = \X{at}_x~\limits_y \qquad - C.\CMEMS[y] = \X{it}_y~\limits_y + C.\CMEMS[y] = \X{at}_y~\limits_y }{ - C \vdashinstr \MEMORYCOPY~x~y : [\X{it}_x~\X{it}_y~\itmin(\X{it}_x, \X{it}_y)] \to [] + C \vdashinstr \MEMORYCOPY~x~y : [\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to [] } @@ -1909,19 +1909,19 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. +* Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. * The data segment :math:`C.\CDATAS[y]` must be defined in the context. -* Then the instruction is valid with type :math:`[\X{it}~\I32~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{at}~\I32~\I32] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it}~\limits + C.\CMEMS[x] = \X{at}~\limits \qquad C.\CDATAS[y] = {\ok} }{ - C \vdashinstr \MEMORYINIT~x~y : [\X{it}~\I32~\I32] \to [] + C \vdashinstr \MEMORYINIT~x~y : [\X{at}~\I32~\I32] \to [] } @@ -2474,7 +2474,7 @@ Control Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. @@ -2482,17 +2482,17 @@ Control Instructions * The :ref:`expansion ` of :math:`C.\CTYPES[y]` must be a :ref:`function type ` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. -* Then the instruction is valid with type :math:`[t_1^\ast~\X{it}] \to [t_2^\ast]`. +* Then the instruction is valid with type :math:`[t_1^\ast~\X{at}] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t \qquad C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad \expanddt(C.\CTYPES[y]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ - C \vdashinstr \CALLINDIRECT~x~y : [t_1^\ast~\X{it}] \to [t_2^\ast] + C \vdashinstr \CALLINDIRECT~x~y : [t_1^\ast~\X{at}] \to [t_2^\ast] } @@ -2563,7 +2563,7 @@ Control Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{at}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. @@ -2573,11 +2573,11 @@ Control Instructions * The :ref:`result type ` :math:`[t_2^\ast]` must :ref:`match ` :math:`C.\CRETURN`. -* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast]`, for any sequences of :ref:`value types ` :math:`t_3^\ast` and :math:`t_4^\ast`. +* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\X{at}] \to [t_4^\ast]`, for any sequences of :ref:`value types ` :math:`t_3^\ast` and :math:`t_4^\ast`. .. math:: \frac{ - C.\CTABLES[x] = \X{it}~\limits~t + C.\CTABLES[x] = \X{at}~\limits~t \qquad C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad @@ -2587,7 +2587,7 @@ Control Instructions \qquad C \vdashinstrtype [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast] \ok }{ - C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast] + C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\X{at}] \to [t_4^\ast] } .. note:: diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index c4dda45b4..75ff8c08e 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -502,9 +502,9 @@ Limits Table Types ~~~~~~~~~~~ -A :ref:`table type ` :math:`(\idxtype_1~\limits_1~\reftype_1)` matches :math:`(\idxtype_2~\limits_2~\reftype_2)` if and only if: +A :ref:`table type ` :math:`(\addrtype_1~\limits_1~\reftype_1)` matches :math:`(\addrtype_2~\limits_2~\reftype_2)` if and only if: -* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same. +* Address types :math:`\addrtype_1` and :math:`\addrtype_2` are the same. * Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. @@ -513,7 +513,7 @@ A :ref:`table type ` :math:`(\idxtype_1~\limits_1~\reftype_1)` .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2 + C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 \qquad @@ -521,7 +521,7 @@ A :ref:`table type ` :math:`(\idxtype_1~\limits_1~\reftype_1)` \qquad C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1 }{ - C \vdashtabletypematch \idxtype_1~\limits_1~\reftype_1 \matchestabletype \idxtype_2~\limits_2~\reftype_2 + C \vdashtabletypematch \addrtype_1~\limits_1~\reftype_1 \matchestabletype \addrtype_2~\limits_2~\reftype_2 } @@ -531,9 +531,9 @@ A :ref:`table type ` :math:`(\idxtype_1~\limits_1~\reftype_1)` Memory Types ~~~~~~~~~~~~ -A :ref:`memory type ` :math:`(\idxtype_1~\limits_1)` matches :math:`(\idxtype_2~\limits_2)` if and only if: +A :ref:`memory type ` :math:`(\addrtype_1~\limits_1)` matches :math:`(\addrtype_2~\limits_2)` if and only if: -* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same. +* Address types :math:`\addrtype_1` and :math:`\addrtype_2` are the same. * Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. @@ -541,7 +541,7 @@ A :ref:`memory type ` :math:`(\idxtype_1~\limits_1)` matches :ma .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2 + C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 }{ diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 1eab64635..c1a97cb07 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -501,10 +501,10 @@ Limits Table Types ~~~~~~~~~~~ -:math:`\idxtype~\limits~\reftype` -................................. +:math:`\addrtype~\limits~\reftype` +.................................. -* The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{|\idxtype|}-1`. +* The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{|\addrtype|}-1`. * The reference type :math:`\reftype` must be :ref:`valid `. @@ -512,11 +512,11 @@ Table Types .. math:: \frac{ - C \vdashlimits \limits : 2^{|\idxtype|}-1 + C \vdashlimits \limits : 2^{|\addrtype|}-1 \qquad C \vdashreftype \reftype \ok }{ - C \vdashtabletype \idxtype~\limits~\reftype \ok + C \vdashtabletype \addrtype~\limits~\reftype \ok } @@ -528,16 +528,16 @@ Table Types Memory Types ~~~~~~~~~~~~ -:math:`\idxtype~\limits` -........................ +:math:`\addrtype~\limits` +......................... -* The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{|\idxtype|-16}`. +* The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{|\addrtype|-16}`. * Then the memory type is valid. .. math:: \frac{ - C \vdashlimits \limits : 2^{|\idxtype|-16} + C \vdashlimits \limits : 2^{|\addrtype|-16} }{ C \vdashmemtype \limits \ok } diff --git a/document/js-api/index.bs b/document/js-api/index.bs index a14b5559a..65233ca9f 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -124,7 +124,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df text: match_valtype; url: appendix/embedding.html#embed-match-valtype text: error; url: appendix/embedding.html#embed-error text: store; url: exec/runtime.html#syntax-store - text: index type; url: syntax/types.html#syntax-idxtype + text: address type; url: syntax/types.html#syntax-addrtype text: table type; url: syntax/types.html#syntax-tabletype text: table address; url: exec/runtime.html#syntax-tableaddr text: function address; url: exec/runtime.html#syntax-funcaddr @@ -566,12 +566,12 @@ enum ImportExportKind { "tag" }; -enum IndexType { +enum AddressType { "i32", "i64", }; -typedef any IndexValue; +typedef any AddressValue; dictionary ModuleExportDescriptor { required USVString name; @@ -677,15 +677,15 @@ Note: The use of this synchronous API is discouraged, as some implementations so 
 dictionary MemoryDescriptor {
-  required IndexValue initial;
-  IndexValue maximum;
-  IndexType index;
+  required AddressValue initial;
+  AddressValue maximum;
+  AddressType addressType;
 };
 
 [LegacyNamespace=WebAssembly, Exposed=*]
 interface Memory {
   constructor(MemoryDescriptor descriptor);
-  IndexValue grow(IndexValue delta);
+  AddressValue grow(AddressValue delta);
   ArrayBuffer toFixedLengthBuffer();
   ArrayBuffer toResizableBuffer();
   readonly attribute ArrayBuffer buffer;
@@ -748,11 +748,11 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
 
 

     The Memory(|descriptor|) constructor, when invoked, performs the following steps:
-    1. If |descriptor|["index"] [=map/exists=], let |indextype| be |descriptor|["index"]; otherwise, let |indextype| be "i32".
-    1. Let |initial| be [=?=] [=IndexValueToU64=](|descriptor|["initial"], |indextype|).
-    1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=IndexValueToU64=](|descriptor|["maximum"], |indextype|); otherwise, let |maximum| be empty.
+    1. If |descriptor|["addressType"] [=map/exists=], let |addrtype| be |descriptor|["addressType"]; otherwise, let |addrtype| be "i32".
+    1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|).
+    1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty.
     1. If |maximum| is not empty and |maximum| < |initial|, throw a {{RangeError}} exception.
-    1. Let |memtype| be |indextype| { **min** |initial|, **max** |maximum| }.
+    1. Let |memtype| be |addrtype| { **min** |initial|, **max** |maximum| }.
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
     1. Let (|store|, |memaddr|) be [=mem_alloc=](|store|, |memtype|). If allocation fails, throw a {{RangeError}} exception.
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
@@ -792,10 +792,10 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
     The grow(|delta|) method, when invoked, performs the following steps:
     1. Let |memaddr| be **this**.\[[Memory]].
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |indextype| be the [=index type=] in [=mem_type=](|store|, |memaddr|).
-    1. Let |delta64| be [=?=] [=IndexValueToU64=](|delta|, |indextype|).
+    1. Let |addrtype| be the [=address type=] in [=mem_type=](|store|, |memaddr|).
+    1. Let |delta64| be [=?=] [=AddressValueToU64=](|delta|, |addrtype|).
     1. Let |ret| be the result of [=grow the memory buffer|growing the memory buffer=] associated with |memaddr| by |delta64|.
-    1. Return [=U64ToIndexValue=](|ret|, |indextype|).
+    1. Return [=U64ToAddressValue=](|ret|, |addrtype|).
 

 
 Immediately after a WebAssembly [=memory.grow=] instruction executes, perform the following steps:
@@ -873,18 +873,18 @@ enum TableKind {
 
 dictionary TableDescriptor {
   required TableKind element;
-  required IndexValue initial;
-  IndexValue maximum;
-  IndexType index;
+  required AddressValue initial;
+  AddressValue maximum;
+  AddressType addressType;
 };
 
 [LegacyNamespace=WebAssembly, Exposed=*]
 interface Table {
   constructor(TableDescriptor descriptor, optional any value);
-  IndexValue grow(IndexValue delta, optional any value);
-  any get(IndexValue index);
-  undefined set(IndexValue index, optional any value);
-  readonly attribute IndexValue length;
+  AddressValue grow(AddressValue delta, optional any value);
+  any get(AddressValue index);
+  undefined set(AddressValue index, optional any value);
+  readonly attribute AddressValue length;
 };
@@ -915,16 +915,16 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address 1. Let |elementtype| be [=ToValueType=](|descriptor|["element"]). 1. If |elementtype| is not a [=reftype=], 1. [=Throw=] a {{TypeError}} exception. - 1. If |descriptor|["index"] [=map/exists=], let |indextype| be |descriptor|["index"]; otherwise, let |indextype| be "i32". - 1. Let |initial| be [=?=] [=IndexValueToU64=](|descriptor|["initial"], |indextype|). - 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=IndexValueToU64=](|descriptor|["maximum"], |indextype|); otherwise, let |maximum| be empty. + 1. If |descriptor|["addressType"] [=map/exists=], let |addrtype| be |descriptor|["addressType"]; otherwise, let |addrtype| be "i32". + 1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|). + 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty. 1. If |maximum| is not empty and |maximum| < |initial|, throw a {{RangeError}} exception. 1. If |value| is missing, 1. Let |ref| be [=DefaultValue=](|elementtype|). 1. Assert: |ref| is not [=error=]. 1. Otherwise, 1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementtype|). - 1. Let |type| be the [=table type=] (|indextype|, { **min** |initial|, **max** |maximum| }, |elementtype|). + 1. Let |type| be the [=table type=] (|addrtype|, { **min** |initial|, **max** |maximum| }, |elementtype|). 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|, |ref|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. @@ -936,8 +936,8 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address 1. Let |tableaddr| be **this**.\[[Table]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |initialSize| be [=table_size=](|store|, |tableaddr|). - 1. Let (|indextype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). - 1. Let |delta64| be [=?=] [=IndexValueToU64=](|delta|, |indextype|). + 1. Let (|addrtype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). + 1. Let |delta64| be [=?=] [=AddressValueToU64=](|delta|, |addrtype|). 1. If |value| is missing, 1. Let |ref| be [=DefaultValue=](|elementtype|). 1. If |ref| is [=error=], throw a {{TypeError}} exception. @@ -956,19 +956,19 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address The getter of the length attribute of {{Table}}, when invoked, performs the following steps: 1. Let |tableaddr| be **this**.\[[Table]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let |indextype| be the [=index type=] in [=table_type=](|store|, |tableaddr|). + 1. Let |addrtype| be the [=address type=] in [=table_type=](|store|, |tableaddr|). 1. Let |length64| be [=table_size=](|store|, |tableaddr|). - 1. Return [=U64ToIndexValue=](|length64|, |indextype|). + 1. Return [=U64ToAddressValue=](|length64|, |addrtype|).
The get(|index|) method, when invoked, performs the following steps: 1. Let |tableaddr| be **this**.\[[Table]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let (|indextype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). + 1. Let (|addrtype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). 1. If |elementtype| is [=exnref=], 1. Throw a {{TypeError}} exception. - 1. Let |index64| be [=?=] [=IndexValueToU64=](|index|, |indextype|). + 1. Let |index64| be [=?=] [=AddressValueToU64=](|index|, |addrtype|). 1. Let |result| be [=table_read=](|store|, |tableaddr|, |index64|). 1. If |result| is [=error=], throw a {{RangeError}} exception. 1. Return [=ToJSValue=](|result|). @@ -978,10 +978,10 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address The set(|index|, |value|) method, when invoked, performs the following steps: 1. Let |tableaddr| be **this**.\[[Table]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let (|indextype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). + 1. Let (|addrtype|, limits, |elementtype|) be [=table_type=](|store|, |tableaddr|). 1. If |elementtype| is [=exnref=], 1. Throw a {{TypeError}} exception. - 1. Let |index64| be [=?=] [=IndexValueToU64=](|index|, |indextype|). + 1. Let |index64| be [=?=] [=AddressValueToU64=](|index|, |addrtype|). 1. If |value| is missing, 1. Let |ref| be [=DefaultValue=](|elementtype|). 1. If |ref| is [=error=], throw a {{TypeError}} exception. @@ -1358,14 +1358,14 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va
-The algorithm IndexValueToU64(|v|, |indextype|) converts a JavaScript value to a WebAssembly [=u64=] for use in embedding operations. It is designed to act like [=[EnforceRange]=] [=unsigned long=] for {{IndexType}} "i32", and to extend these semantics to {{IndexType}} "i64", by performing the following steps: +The algorithm AddressValueToU64(|v|, |addrtype|) converts a JavaScript value to a WebAssembly [=u64=] for use in embedding operations. It is designed to act like [=[EnforceRange]=] [=unsigned long=] for {{AddressType}} "i32", and to extend these semantics to {{AddressType}} "i64", by performing the following steps: -1. If |indextype| is "i32", +1. If |addrtype| is "i32", 1. Let |n| be [=?=] [$ConvertToInt$](|v|, 32, "unsigned"), where the destination type is associated with [=[EnforceRange]=]. Note: This is equivalent to the [=js-unsigned-long|JS conversion rules=] for [=[EnforceRange]=] [=unsigned long=]. 1. Return [=ℝ=](|n|) as a WebAssembly [=u64=]. -1. If |indextype| is "i64", +1. If |addrtype| is "i64", 1. Let |n| be [=?=] [$ToBigInt$](|v|). 1. If |n| < 0 or |n| > 264 − 1, [=throw=] a {{TypeError}}. @@ -1376,10 +1376,10 @@ The algorithm IndexValueToU64(|v|, |indextype|) converts a JavaScript
-The algorithm U64ToIndexValue(|v|, |indextype|) converts a [=u64=] value from a WebAssembly embedding operation to the correct variant of {{IndexValue}} for an {{IndexType}}, by performing the following steps: +The algorithm U64ToAddressValue(|v|, |addrtype|) converts a [=u64=] value from a WebAssembly embedding operation to the correct variant of {{AddressValue}} for an {{AddressType}}, by performing the following steps: -1. If |indextype| is "i32", return [=𝔽=](|v| interpreted as a [=mathematical value=]). -1. Else if |indextype| is "i64", return [=ℤ=](|v| interpreted as a [=mathematical value=]). +1. If |addrtype| is "i32", return [=𝔽=](|v| interpreted as a [=mathematical value=]). +1. Else if |addrtype| is "i64", return [=ℤ=](|v| interpreted as a [=mathematical value=]). 1. Assert: This step is not reached.
diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 4ca94d68b..1db0dce4f 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -289,11 +289,11 @@ let limits uN s = let table_type s = let t = ref_type s in let lim, is64 = limits u64 s in - TableT (lim, (if is64 then I64IndexType else I32IndexType), t) + TableT (lim, (if is64 then I64AddrType else I32AddrType), t) let memory_type s = let lim, is64 = limits u64 s in - MemoryT (lim, if is64 then I64IndexType else I32IndexType) + MemoryT (lim, if is64 then I64AddrType else I32AddrType) let global_type s = let t = val_type s in @@ -1099,7 +1099,7 @@ let table s = ); (fun s -> let at = region s (pos s) (pos s) in - let TableT (_, _it, (_, ht)) as ttype = table_type s in + let TableT (_, _at, (_, ht)) as ttype = table_type s in {ttype; tinit = [RefNull ht @@ at] @@ at} ); ] s diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index aca2a5454..3e7003a89 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} it = - let flags = flag (max <> None) 0 + flag (it = I64IndexType) 2 in + 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 table_type = function - | TableT (lim, it, t) -> ref_type t; limits u64 lim it + | TableT (lim, at, t) -> ref_type t; limits u64 lim at let memory_type = function - | MemoryT (lim, it) -> limits u64 lim it + | MemoryT (lim, at) -> limits u64 lim at let global_type = function | GlobalT (mut, t) -> val_type t; mutability mut @@ -972,7 +972,7 @@ struct let table tab = let {ttype; tinit} = tab.it in match ttype, tinit.it with - | TableT (_, _it, (_, ht1)), [{it = RefNull ht2; _}] when ht1 = ht2 -> + | TableT (_, _at, (_, ht1)), [{it = RefNull ht2; _}] when ht1 = ht2 -> table_type ttype | _ -> op 0x40; op 0x00; table_type ttype; const tinit diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 2d632dc9f..c5631d1ba 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -385,7 +385,7 @@ let rec step (c : config) : config = | TableSize x, vs -> let tab = table c.frame.inst x in - value_of_index (Table.index_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] + value_of_addr (Table.addr_type_of tab) (Table.size (table c.frame.inst x)) :: vs, [] | TableGrow x, Num delta :: Ref r :: vs' -> let tab = table c.frame.inst x in @@ -393,7 +393,7 @@ let rec step (c : config) : config = let result = try Table.grow tab (Table.index_of_num delta) r; old_size with Table.SizeOverflow | Table.SizeLimit | Table.OutOfMemory -> -1L - in (value_of_index (Table.index_type_of tab) result) :: vs', [] + in (value_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 @@ -552,7 +552,7 @@ let rec step (c : config) : config = | MemorySize x, vs -> let mem = memory c.frame.inst x in - value_of_index (Memory.index_type_of mem) (Memory.size mem) :: vs, [] + value_of_addr (Memory.addr_type_of mem) (Memory.size mem) :: vs, [] | MemoryGrow x, Num delta :: vs' -> let mem = memory c.frame.inst x in @@ -560,7 +560,7 @@ let rec step (c : config) : config = let result = try Memory.grow mem (Memory.address_of_num delta); old_size with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1L - in (value_of_index (Memory.index_type_of mem) result) :: vs', [] + in (value_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 diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index 0ab23ec4c..aaf8f0665 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}, I32IndexType, (Null, FuncHT)) in + let tt = TableT ({min = 10L; max = Some 20L}, I32AddrType, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let table64 = - let tt = TableT ({min = 10L; max = Some 20L}, I64IndexType, (Null, FuncHT)) in + let tt = TableT ({min = 10L; max = Some 20L}, I64AddrType, (Null, FuncHT)) in ExternTable (Table.alloc tt (NullRef FuncHT)) let memory = - let mt = MemoryT ({min = 1L; max = Some 2L}, I32IndexType) in + let mt = MemoryT ({min = 1L; max = Some 2L}, I32AddrType) in ExternMemory (Memory.alloc mt) let func f ft = diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 03571a730..113a9cd25 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -25,8 +25,8 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let create n it = - if I64.gt_u n 0x10000L && it = I32IndexType then raise SizeOverflow else +let create n at = + if I64.gt_u n 0x10000L && at = I32AddrType then raise SizeOverflow else try let size = Int64.(mul n page_size) in let mem = Array1_64.create Int8_unsigned C_layout size in @@ -34,10 +34,10 @@ let create n it = mem with Out_of_memory -> raise OutOfMemory -let alloc (MemoryT (lim, it) as ty) = +let alloc (MemoryT (lim, at) as ty) = assert Free.((memory_type ty).types = Set.empty); if not (valid_limits lim) then raise Type; - {ty; content = create lim.min it} + {ty; content = create lim.min at} let bound mem = Array1_64.dim mem.content @@ -48,8 +48,8 @@ let size mem = let type_of mem = mem.ty -let index_type_of mem = - let (MemoryT (_, it)) = type_of mem in it +let addr_type_of mem = + let (MemoryT (_, at)) = type_of mem in at let address_of_num x = match x with @@ -63,17 +63,17 @@ let address_of_value x = | _ -> raise Type let grow mem delta = - let MemoryT (lim, it) = mem.ty in + let MemoryT (lim, at) = 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_limits lim') then raise SizeLimit else - let after = create new_size (index_type_of mem) in + let after = create new_size (addr_type_of mem) 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', it); + mem.ty <- MemoryT (lim', at); mem.content <- after let load_byte mem a = diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index ab06999d3..da9f468f8 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -19,7 +19,7 @@ val page_size : int64 val alloc : memory_type -> memory (* raises Type, SizeOverflow, OutOfMemory *) val type_of : memory -> memory_type -val index_type_of : memory -> index_type +val addr_type_of : memory -> addr_type val size : memory -> size val bound : memory -> address val address_of_value : value -> address diff --git a/interpreter/runtime/table.ml b/interpreter/runtime/table.ml index 0db065c90..b18dbd5df 100644 --- a/interpreter/runtime/table.ml +++ b/interpreter/runtime/table.ml @@ -19,16 +19,16 @@ let valid_limits {min; max} = | None -> true | Some m -> I64.le_u min m -let valid_index it i = - match it with - | I32IndexType -> I64.le_u i 0xffff_ffffL - | I64IndexType -> true +let valid_addr at i = + match at with + | I32AddrType -> I64.le_u i 0xffff_ffffL + | I64AddrType -> true let create size r = try Lib.Array64.make size r with Out_of_memory | Invalid_argument _ -> raise OutOfMemory -let alloc (TableT (lim, it, t) as ty) r = +let alloc (TableT (lim, at, t) as ty) r = assert Free.((ref_type t).types = Set.empty); if not (valid_limits lim) then raise Type; {ty; content = create lim.min r} @@ -39,8 +39,8 @@ let size tab = let type_of tab = tab.ty -let index_type_of tab = - let (TableT (_, it, _)) = type_of tab in it +let addr_type_of tab = + let (TableT (_, at, _)) = type_of tab in at let index_of_num x = match x with @@ -49,17 +49,17 @@ let index_of_num x = | _ -> raise Type let grow tab delta r = - let TableT (lim, it, t) = tab.ty in + let TableT (lim, at, 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_index it new_size) then raise SizeOverflow else + if not (valid_addr 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', it, t); + tab.ty <- TableT (lim', at, 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, _it, t) = tab.ty in + let TableT (_lim, _at, 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 07e84d5b6..6ebba6068 100644 --- a/interpreter/runtime/table.mli +++ b/interpreter/runtime/table.mli @@ -16,7 +16,7 @@ exception OutOfMemory val alloc : table_type -> ref_ -> table (* raises Type, OutOfMemory *) val type_of : table -> table_type -val index_type_of : table -> index_type +val addr_type_of : table -> addr_type val size : table -> size val index_of_num : num -> index val grow : table -> size -> ref_ -> unit diff --git a/interpreter/runtime/value.ml b/interpreter/runtime/value.ml index 5988336ad..5381b67f1 100644 --- a/interpreter/runtime/value.ml +++ b/interpreter/runtime/value.ml @@ -281,10 +281,10 @@ let storage_bits_of_val st v = let value_of_bool b = Num (I32 (if b then 1l else 0l)) -let value_of_index it x = - match it with - | I64IndexType -> Num (I64 x) - | I32IndexType -> Num (I32 (Int64.to_int32 x)) +let value_of_addr at x = + match at with + | I64AddrType -> Num (I64 x) + | I32AddrType -> Num (I32 (Int64.to_int32 x)) 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 72314487f..efbbd58da 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, _it, t)) = ref_type t -let memory_type (MemoryT (_lim, _it)) = empty +let table_type (TableT (_lim, _at, t)) = ref_type t +let memory_type (MemoryT (_lim, _at)) = empty let tag_type (TagT dt) = def_type dt let extern_type = function diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 729a564ad..fb5246445 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -25,7 +25,7 @@ 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 index_type = I32IndexType | I64IndexType +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 * index_type * ref_type -type memory_type = MemoryT of Int64.t limits * index_type +type table_type = TableT of Int64.t limits * addr_type * ref_type +type memory_type = MemoryT of Int64.t limits * addr_type type global_type = GlobalT of mut * val_type type tag_type = TagT of def_type type local_type = LocalT of init * val_type @@ -147,11 +147,11 @@ 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_index_type = function - | I32IndexType -> I32T - | I64IndexType -> I64T +let num_type_of_addr_type = function + | I32AddrType -> I32T + | I64AddrType -> I64T -let value_type_of_index_type t = NumT (num_type_of_index_type t) +let value_type_of_addr_type t = NumT (num_type_of_addr_type t) (* Substitution *) @@ -228,10 +228,10 @@ let subst_def_type s = function let subst_memory_type s = function - | MemoryT (lim, it) -> MemoryT (lim, it) + | MemoryT (lim, at) -> MemoryT (lim, at) let subst_table_type s = function - | TableT (lim, it, t) -> TableT (lim, it, subst_ref_type s t) + | TableT (lim, at, t) -> TableT (lim, at, subst_ref_type s t) let subst_global_type s = function | GlobalT (mut, t) -> GlobalT (mut, subst_val_type s t) @@ -365,8 +365,8 @@ and string_of_val_type = function | RefT t -> string_of_ref_type t | BotT -> "bot" -and string_of_index_type t = - string_of_val_type (value_type_of_index_type t) +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 +418,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, it) -> string_of_num_type (num_type_of_index_type it) ^ " " ^ string_of_limits lim + | MemoryT (lim, at) -> string_of_num_type (num_type_of_addr_type at) ^ " " ^ string_of_limits lim let string_of_table_type = function - | TableT (lim, it, t) -> string_of_num_type (num_type_of_index_type it) ^ " " ^ string_of_limits lim ^ " " ^ string_of_ref_type t + | TableT (lim, at, t) -> string_of_num_type (num_type_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 fe9fbf2a4..6f7eccdaa 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -77,7 +77,7 @@ let ref_type t = | (Null, ExnHT) -> "exnref" | t -> string_of_ref_type t -let index_type t = string_of_val_type (value_type_of_index_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,14 +657,14 @@ let tag off i tag = ) let table off i tab = - let {ttype = TableT (lim, it, t); tinit} = tab.it in - Node ("table $" ^ nat (off + i) ^ " " ^ index_type it ^ " " ^ limits nat64 lim, + let {ttype = TableT (lim, at, 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, it)} = mem.it in - Node ("memory $" ^ nat (off + i) ^ " " ^ index_type it ^ " " ^ limits nat64 lim, []) + let {mtype = MemoryT (lim, at)} = mem.it in + Node ("memory $" ^ nat (off + i) ^ " " ^ addr_type at ^ " " ^ limits nat64 lim, []) let is_elem_kind = function | (NoNull, FuncHT) -> true diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index bd5d205ac..df2ec4057 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -264,37 +264,37 @@ let inline_func_type_explicit (c : context) x ft loc = error (at loc) "inline function type does not match explicit type"; x -let index_type_of_num_type t loc = +let addr_type_of_num_type t loc = match t with - | I32T -> I32IndexType - | I64T -> I64IndexType - | _ -> error (at loc) "illegal index type" + | I32T -> I32AddrType + | I64T -> I64AddrType + | _ -> error (at loc) "illegal address type" -let index_type_of_value_type t loc = +let addr_type_of_value_type t loc = match t with - | NumT t -> index_type_of_num_type t loc - | _ -> error (at loc) "illegal index type" + | NumT t -> addr_type_of_num_type t loc + | _ -> error (at loc) "illegal address type" -let memory_data init it c x loc = +let memory_data init at c x loc = let size = Int64.(div (add (of_int (String.length init)) 65535L) 65536L) in - let instr = match it with - | I32IndexType -> i32_const (0l @@ loc) - | I64IndexType -> i64_const (0L @@ loc) 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}, it)} @@ loc], + [{mtype = MemoryT ({min = size; max = Some size}, at)} @@ loc], [{dinit = init; dmode = Active {index = x; offset} @@ loc} @@ loc], [], [] -let table_data tinit init it etype c x loc = - let instr = match it with - | I32IndexType -> i32_const (0l @@ loc) - | I64IndexType -> i64_const (0L @@ loc) in +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}, it, etype); tinit} @@ loc], + [{ttype = TableT ({min = size64; max = Some size64}, at, etype); tinit} @@ loc], [{etype; einit; emode} @@ loc], [], [] @@ -501,12 +501,12 @@ 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, index_type_of_value_type ($1 c) $sloc, $3 c) } - | limits ref_type { fun c -> TableT ($1, I32IndexType, $2 c) } + | 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) } memory_type : - | val_type limits { fun c -> MemoryT ($2, index_type_of_value_type ($1 c) $sloc) } - | limits { fun c -> MemoryT ($1, I32IndexType) } + | val_type limits { fun c -> MemoryT ($2, addr_type_of_value_type ($1 c) $sloc) } + | limits { fun c -> MemoryT ($1, I32AddrType) } limits : | NAT { {min = nat64 $1 $loc($1); max = None} } @@ -1165,19 +1165,19 @@ table_fields : let emode = Active {index = x; offset} @@ loc in let (_, ht) as etype = $1 c in let tinit = [RefNull ht @@ loc] @@ loc in - [{ttype = TableT ({min = size64; max = Some size64}, I32IndexType, etype); tinit} @@ loc], + [{ttype = TableT ({min = size64; max = Some size64}, I32AddrType, 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 I32IndexType etype c x loc } + table_data tinit $4 I32AddrType etype c x loc } | val_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 (index_type_of_value_type ($1 c) loc) etype c x loc } + table_data tinit $5 (addr_type_of_value_type ($1 c) loc) etype c x loc } data : | LPAR DATA bind_var_opt string_list RPAR @@ -1209,9 +1209,9 @@ memory_fields : { 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 I32IndexType } + { memory_data $3 I32AddrType } | val_type LPAR DATA string_list RPAR /* Sugar */ - { fun c x loc -> memory_data $4 (index_type_of_value_type ($1 c) $sloc) c x loc } + { fun c x loc -> memory_data $4 (addr_type_of_value_type ($1 c) $sloc) c x loc } tag : | LPAR TAG bind_var_opt tag_fields RPAR diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index 77c9c4f57..b2cc26630 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -161,11 +161,11 @@ 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, it1, t1)) (TableT (lim2, it2, t2)) = - match_limits c lim1 lim2 && it1 = it2 && match_ref_type c t1 t2 && match_ref_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_memory_type c (MemoryT (lim1, it1)) (MemoryT (lim2, it2)) = - match_limits c lim1 lim2 && it1 = it2 +let match_memory_type c (MemoryT (lim1, at1)) (MemoryT (lim2, at2)) = + match_limits c lim1 lim2 && at1 = at2 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 511c34b09..6fc75ace7 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -151,23 +151,23 @@ 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, it, t) = tt in + let TableT (lim, _at, t) = tt in check_ref_type c t at; - match it with - | I64IndexType -> + match _at with + | I64AddrType -> check_limits I64.le_u lim 0xffff_ffff_ffff_ffffL at "table size must be at most 2^64-1" - | I32IndexType -> + | I32AddrType -> check_limits I64.le_u lim 0xffff_ffffL at "table size must be at most 2^32-1" let check_memory_type (c : context) (mt : memory_type) at = - let MemoryT (lim, it) = mt in - match it with - | I32IndexType -> + 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)" - | I64IndexType -> + | I64AddrType -> check_limits I64.le_u lim 0x1_0000_0000_0000L at "memory size must be at most 48 bits of pages" @@ -370,8 +370,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, it) = memory c (0l @@ at) in - if it = I32IndexType then + let MemoryT (_lim, _at) = memory c (0l @@ at) in + if _at = I32AddrType then require (I64.lt_u memop.offset 0x1_0000_0000L) at "offset out of range"; memop.ty @@ -518,12 +518,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, it, t) = table c x in + let TableT (lim, at, 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_index_type it]) --> ts2, [] + (ts1 @ [value_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 +542,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, it, t) = table c x in + let TableT (_lim, at, 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_index_type it]) -->... [], [] + (ts1 @ [value_type_of_addr_type at]) -->... [], [] | Throw x -> let TagT dt = tag c x in @@ -588,102 +588,102 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in [t] --> [], [] | TableGet x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it] --> [RefT rt], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_addr_type at] --> [RefT rt], [] | TableSet x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it; RefT rt] --> [], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_addr_type at; RefT rt] --> [], [] | TableSize x -> - let TableT (_lim, it, _rt) = table c x in - [] --> [value_type_of_index_type it], [] + let TableT (_lim, at, _rt) = table c x in + [] --> [value_type_of_addr_type at], [] | TableGrow x -> - let TableT (_lim, it, rt) = table c x in - [RefT rt; value_type_of_index_type it] --> [value_type_of_index_type it], [] + let TableT (_lim, at, rt) = table c x in + [RefT rt; value_type_of_addr_type at] --> [value_type_of_addr_type at], [] | TableFill x -> - let TableT (_lim, it, rt) = table c x in - [value_type_of_index_type it; RefT rt; value_type_of_index_type it] --> [], [] + let TableT (_lim, at, rt) = table c x in + [value_type_of_addr_type at; RefT rt; value_type_of_addr_type at] --> [], [] | TableCopy (x, y) -> - let TableT (_lim1, it1, t1) = table c x in - let TableT (_lim2, it2, t2) = table c y in - let it_min = min it1 it2 in + 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 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_index_type it1; value_type_of_index_type it2; value_type_of_index_type it_min] --> [], [] + [value_type_of_addr_type at1; value_type_of_addr_type at2; value_type_of_addr_type at_min] --> [], [] | TableInit (x, y) -> - let TableT (_lim1, it, t1) = table c x in + let TableT (_lim1, at, 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_index_type it; NumT I32T; NumT I32T] --> [], [] + [value_type_of_addr_type at; NumT I32T; NumT I32T] --> [], [] | ElemDrop x -> ignore (elem c x); [] --> [], [] | Load (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop num_size (Lib.Option.map fst) e.at in - [value_type_of_index_type it] --> [NumT t], [] + [value_type_of_addr_type at] --> [NumT t], [] | Store (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop num_size (fun sz -> sz) e.at in - [value_type_of_index_type it; NumT t] --> [], [] + [value_type_of_addr_type at; NumT t] --> [], [] | VecLoad (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (Lib.Option.map fst) e.at in - [value_type_of_index_type it] --> [VecT t], [] + [value_type_of_addr_type at] --> [VecT t], [] | VecStore (x, memop) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = memory c x in let t = check_memop c memop vec_size (fun _ -> None) e.at in - [value_type_of_index_type it; VecT t] --> [], [] + [value_type_of_addr_type at; VecT t] --> [], [] | VecLoadLane (x, memop, i) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = 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_index_type it; VecT t] --> [VecT t], [] + [value_type_of_addr_type at; VecT t] --> [VecT t], [] | VecStoreLane (x, memop, i) -> - let MemoryT (_lim, it) = memory c x in + let MemoryT (_lim, at) = 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_index_type it; VecT t] --> [], [] + [value_type_of_addr_type at; VecT t] --> [], [] | MemorySize x -> - let MemoryT (_lim, it) = memory c x in - [] --> [value_type_of_index_type it], [] + let MemoryT (_lim, at) = memory c x in + [] --> [value_type_of_addr_type at], [] | MemoryGrow x -> - let MemoryT (_lim, it) = memory c x in - [value_type_of_index_type it] --> [value_type_of_index_type it], [] + let MemoryT (_lim, at) = memory c x in + [value_type_of_addr_type at] --> [value_type_of_addr_type at], [] | MemoryFill x -> - let MemoryT (_lim, it) = memory c x in - [value_type_of_index_type it; NumT I32T; value_type_of_index_type it] --> [], [] + let MemoryT (_lim, at) = memory c x in + [value_type_of_addr_type at; NumT I32T; value_type_of_addr_type at] --> [], [] | MemoryCopy (x, y)-> - let MemoryT (_lib1, it1) = memory c x in - let MemoryT (_lib2, it2) = memory c y in - let it_min = min it1 it2 in - [value_type_of_index_type it1; value_type_of_index_type it2; value_type_of_index_type it_min] --> [], [] + 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] --> [], [] | MemoryInit (x, y) -> - let MemoryT (_lib, it) = memory c x in + let MemoryT (_lib, at) = memory c x in let () = data c y in - [value_type_of_index_type it; NumT I32T; NumT I32T] --> [], [] + [value_type_of_addr_type at; NumT I32T; NumT I32T] --> [], [] | DataDrop x -> let () = data c x in @@ -1029,7 +1029,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, _it, rt) = ttype in + let TableT (_lim, _at, rt) = ttype in check_table_type c ttype tab.at; check_const c tinit (RefT rt); {c with tables = c.tables @ [ttype]} @@ -1048,11 +1048,11 @@ let check_elem_mode (c : context) (t : ref_type) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let TableT (_lim, it, et) = table c index in + let TableT (_lim, at, 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_index_type it) + check_const c offset (value_type_of_addr_type at) | Declarative -> () let check_elem (c : context) (seg : elem_segment) : context = @@ -1066,8 +1066,8 @@ let check_data_mode (c : context) (mode : segment_mode) = match mode.it with | Passive -> () | Active {index; offset} -> - let MemoryT (_, it) = memory c index in - check_const c offset (value_type_of_index_type it) + let MemoryT (_, at) = memory c index in + check_const c offset (value_type_of_addr_type at) | Declarative -> assert false let check_data (c : context) (seg : data_segment) : context = diff --git a/proposals/memory64/Overview.md b/proposals/memory64/Overview.md index 70874aab3..3e947b582 100644 --- a/proposals/memory64/Overview.md +++ b/proposals/memory64/Overview.md @@ -62,20 +62,20 @@ have to support 32-bit memory addresses in their ABI. * The [limits][syntax limits] structure is changed to use `u64`  - `limits ::= {min u64, max u64?}` -* A new `idxtype` can be either `i32` or `i64` - - `idxtype ::= i32 | i64` +* A new `addrtype` can be either `i32` or `i64` + - `addrtype ::= i32 | i64` * The [memory type][syntax memtype] and [table type][syntax tabletype] - structures are extended to include an index type - - `memtype ::= idxtype limits` - - `tabletype ::= idxtype limits reftype` + structures are extended to include an address type + - `memtype ::= addrtype limits` + - `tabletype ::= addrtype limits reftype` * The [memarg][syntax memarg] immediate is changed to allow a 64-bit offset - `memarg ::= {offset u64, align u32}` ### Validation -* Index types are classified by their value range: +* Address types are classified by their value range: - ``` ---------------- ⊦ i32 : 2**16 @@ -86,7 +86,7 @@ have to support 32-bit memory addresses in their ABI. ``` * [Memory page limits][valid limits] and [Table entry limits][valid limits] are - classified by their respective index types + classified by their respective address types - ``` ⊦ it : k n <= k (m <= k)? (n < m)? ------------------------------------------- @@ -100,112 +100,112 @@ have to support 32-bit memory addresses in their ABI. ⊦ it limits ok ``` -* All [memory instructions][valid meminst] are changed to use the index type, - and the offset must also be in range of the index type +* All [memory instructions][valid meminst] are changed to use the address type, + and the offset must also be in range of the address type - t.load memarg - ``` - C.mems[0] = it limits 2**memarg.align <= |t|/8 memarg.offset < 2**|it| + C.mems[0] = at limits 2**memarg.align <= |t|/8 memarg.offset < 2**|at| -------------------------------------------------------------------------- - C ⊦ t.load memarg : [it] → [t] + C ⊦ t.load memarg : [at] → [t] ``` - t.loadN_sx memarg - ``` - C.mems[0] = it limits 2**memarg.align <= N/8 memarg.offset < 2**|it| + C.mems[0] = at limits 2**memarg.align <= N/8 memarg.offset < 2**|at| ------------------------------------------------------------------------ - C ⊦ t.loadN_sx memarg : [it] → [t] + C ⊦ t.loadN_sx memarg : [at] → [t] ``` - t.store memarg - ``` - C.mems[0] = it limits 2**memarg.align <= |t|/8 memarg.offset < 2**|it| + C.mems[0] = at limits 2**memarg.align <= |t|/8 memarg.offset < 2**|at| -------------------------------------------------------------------------- - C ⊦ t.store memarg : [it t] → [] + C ⊦ t.store memarg : [at t] → [] ``` - t.storeN_sx memarg - ``` - C.mems[0] = it limits 2**memarg.align <= N/8 memarg.offset < 2**|it| + C.mems[0] = at limits 2**memarg.align <= N/8 memarg.offset < 2**|t| ------------------------------------------------------------------------ - C ⊦ t.storeN_sx memarg : [it t] → [] + C ⊦ t.storeN_sx memarg : [at t] → [] ``` - memory.size - ``` - C.mems[0] = it limits + C.mems[0] = at limits --------------------------- - C ⊦ memory.size : [] → [it] + C ⊦ memory.size : [] → [at] ``` - memory.grow - ``` - C.mems[0] = it limits + C.mems[0] = at limits ----------------------------- - C ⊦ memory.grow : [it] → [it] + C ⊦ memory.grow : [at] → [at] ``` - memory.fill - ``` - C.mems[0] = it limits + C.mems[0] = at limits ----------------------------- - C ⊦ memory.fill : [it i32 it] → [] + C ⊦ memory.fill : [at i32 at] → [] ``` - memory.copy - ``` - C.mems[0] = it limits + C.mems[0] = at limits ----------------------------- - C ⊦ memory.copy : [it it it] → [] + C ⊦ memory.copy : [at at at] → [] ``` - memory.init x - ``` - C.mems[0] = it limits C.datas[x] = ok + C.mems[0] = at limits C.datas[x] = ok ------------------------------------------- - C ⊦ memory.init : [it i32 i32] → [] + C ⊦ memory.init : [at i32 i32] → [] ``` - (and similar for memory instructions from other proposals) -* [Table instructions][valid tableinst] are changed to use the index type +* [Table instructions][valid tableinst] are changed to use the address type - call_indirect x y - ``` - C.tables[x] = it limits t C.types[y] = [t1*] → [t2*] + C.tables[x] = at limits t C.types[y] = [t1*] → [t2*] ------------------------------------------------------- - C ⊦ call_indirect x y : [t1* it] → [t2*] + C ⊦ call_indirect x y : [t1* at] → [t2*] ``` - table.get x - ``` - C.tables[x] = it limits t + C.tables[x] = at limits t ------------------------------ - C ⊦ table.get x : [it] → [t] + C ⊦ table.get x : [at] → [t] ``` - table.set x - ``` - C.tables[x] = it limits t + C.tables[x] = at limits t ------------------------------ - C ⊦ table.set x : [it t] → [] + C ⊦ table.set x : [at t] → [] ``` - table.size x - ``` - C.tables[x] = it limits t + C.tables[x] = at limits t ------------------------------ - C ⊦ table.size x : [] → [it] + C ⊦ table.size x : [] → [at] ``` - table.grow x - ``` - C.tables[x] = it limits t + C.tables[x] = at limits t ------------------------------- - C ⊦ table.grow x : [t it] → [it] + C ⊦ table.grow x : [t at] → [at] ``` - table.fill x - ``` - C.tables[x] = it limits t + C.tables[x] = at limits t ---------------------------------- - C ⊦ tables.fill x : [it t it] → [] + C ⊦ tables.fill x : [at t at] → [] ``` - table.copy x y - ``` - C.tables[d] = iN limits t C.tables[s] = iM limits t K = min {N, M} + C.tables[d] = aN limits t C.tables[s] = aM limits t K = min {aN, AM} ----------------------------------------------------------------------------- - C ⊦ table.copy d s : [iN iM iK] → [] + C ⊦ table.copy d s : [aN aM aK] → [] ``` - table.init x y - ``` - C.tables[x] = it limits t C.elems[y] = ok + C.tables[x] = at limits t C.elems[y] = ok ----------------------------------------------- - C ⊦ table.init x y : [it i32 i32] → [] + C ⊦ table.init x y : [at i32 i32] → [] ``` * The [SIMD proposal][simd] extends `t.load memarg` and `t.store memarg` @@ -266,27 +266,27 @@ have to support 32-bit memory addresses in their ABI. 64-bit memory. * The [Multi-memory proposal][multi memory] extends each of these instructions - with one or two memory index immediates. The index type for that memory will + with one or two memory index immediates. The address type for that memory will be used. For example, - memory.size x - ``` - C.mems[x] = it limits + C.mems[x] = at limits --------------------------- - C ⊦ memory.size x : [] → [it] + C ⊦ memory.size x : [] → [at] ``` `memory.copy` has two memory index immediates, so will have multiple possible signatures: - memory.copy d s - ``` - C.mems[d] = iN limits C.mems[s] = iM limits K = min {N, M} + C.mems[d] = aN limits C.mems[s] = aM limits K = min {aN, aM} --------------------------------------------------------------- - C ⊦ memory.copy d s : [iN iM iK] → [] + C ⊦ memory.copy d s : [aN aM aK] → [] ``` -* [Data segment validation][valid data] uses the index type +* [Data segment validation][valid data] uses the address type - ``` - C.mems[0] = it limits C ⊦ expr: [it] C ⊦ expr const + C.mems[0] = at limits C ⊦ expr: [at] C ⊦ expr const ------------------------------------------------------- C ⊦ {data x, offset expr, init b*} ok ``` @@ -298,7 +298,7 @@ have to support 32-bit memory addresses in their ABI. max size - `meminst ::= { data vec64(byte), max u64? }` -* [Memory instructions][exec meminst] use the index type instead of `i32` +* [Memory instructions][exec meminst] use the address type instead of `i32` - `t.load memarg` - `t.loadN_sx memarg` - `t.store memarg` @@ -307,31 +307,31 @@ have to support 32-bit memory addresses in their ABI. - `memory.grow` - (spec text omitted) -* [memory.grow][exec memgrow] has behavior that depends on the index type: +* [memory.grow][exec memgrow] has behavior that depends on the address type: - for `i32`: no change - for `i64`: check for a size greater than 264 - 1, and return 264 - 1 when `memory.grow` fails. -* [Memory import matching][exec memmatch] requires that the index type matches +* [Memory import matching][exec memmatch] requires that the address type matches - ``` - it_1 = it_2 ⊦ limits_1 <= limits_2 + at_1 = at_2 ⊦ limits_1 <= limits_2 ---------------------------------------- - ⊦ mem it_1 limits_1 <= mem it_2 limits_2 + ⊦ mem at_1 limits_1 <= mem at_2 limits_2 ``` * Bounds checking is required to be the same as for 32-bit memories, that is, - the index + offset (a `u65`) of a load or store operation is required to be + the address + offset (a `u65`) of a load or store operation is required to be checked against the current memory size and trap if out of range. It is expected that the cost of this check remains low, if an implementation - can implement the index check with a branch, and the offset separately using a - guard page for all smaller offsets. Repeated accesses over the same index and + can implement the address check with a branch, and the offset separately using a + guard page for all smaller offsets. Repeated accesses over the same address and different offsets allow simple elimination of subsequent checks. ### Binary format * The [limits][binary limits] structure also encodes an additional value to - indicate the index type + indicate the address type - ``` limits ::= 0x00 n:u32 ⇒ i32, {min n, max ϵ}, 0 | 0x01 n:u32 m:u32 ⇒ i32, {min n, max m}, 0 @@ -346,7 +346,7 @@ have to support 32-bit memory addresses in their ABI. * The [memory type][binary memtype] structure is extended to use this limits encoding - ``` - memtype ::= (it, lim, _):limits ⇒ it lim + memtype ::= (at, lim, _):limits ⇒ at lim ``` * The [memarg][binary memarg]'s offset is read as `u64` @@ -354,23 +354,23 @@ have to support 32-bit memory addresses in their ABI. ### Text format -* There is a new index type: +* There is a new address type: - ``` - idxtype ::= 'i32' ⇒ i32 - | 'i64' ⇒ i64 + addrtype ::= 'i32' ⇒ i32 + | 'i64' ⇒ i64 ``` * The [memory type][text memtype] definition is extended to allow an optional - index type, which must be either `i32` or `i64` + address type, which must be either `i32` or `i64` - ``` memtype ::= lim:limits ⇒ i32 lim - | it:idxtype lim:limits ⇒ it lim + | at:addrtype lim:limits ⇒ at lim ``` * The [memory abbreviation][text memabbrev] definition is extended to allow an - optional index type too, which must be either `i32` or `i64` + optional address type too, which must be either `i32` or `i64` - ``` - '(' 'memory' id? index_type? '(' 'data' b_n:datastring ')' ')' === ... + '(' 'memory' id? address_type? '(' 'data' b_n:datastring ')' ')' === ... ``` diff --git a/test/core/table.wast b/test/core/table.wast index 1b6afe9b9..8648df070 100644 --- a/test/core/table.wast +++ b/test/core/table.wast @@ -44,7 +44,7 @@ "table size must be at most 2^32-1" ) -;; Same as above but with i64 index types +;; Same as above but with i64 address types (module (table i64 0 funcref)) (module (table i64 1 funcref)) diff --git a/test/js-api/table/constructor.any.js b/test/js-api/table/constructor.any.js index a4c26a289..9053b6f7c 100644 --- a/test/js-api/table/constructor.any.js +++ b/test/js-api/table/constructor.any.js @@ -223,7 +223,7 @@ test(() => { const argument = { "element": "anyfunc", "initial": 3, "index": "i32" }; const table = new WebAssembly.Table(argument); // Once this is merged with the type reflection proposal we should check the - // index type of `table`. + // address type of `table`. assert_equals(table.length, 3); }, "Table with i32 index constructor"); @@ -231,7 +231,7 @@ test(() => { const argument = { "element": "anyfunc", "initial": 3n, "index": "i64" }; const table = new WebAssembly.Table(argument); // Once this is merged with the type reflection proposal we should check the - // index type of `table`. + // address type of `table`. assert_equals(table.length, 3); }, "Table with i64 index constructor");