diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a3e4d7691..82be56270 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1120,61 +1120,67 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -.. todo:: Handle packed fields correctly via array.get_u instead of array.get +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. -1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. -2. Pop the value :math:`n` from the stack. - -3. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Pop the value :math:`s` from the stack. +4. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. +5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -6. Pop the value :math:`\reff_2` from the stack. +6. Pop the value :math:`\I32.\CONST~n` from the stack. 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`d` from the stack. +8. Pop the value :math:`\I32.\CONST~s` from the stack. + +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + +10. Pop the value :math:`\reff_2` from the stack. + +11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +12. Pop the value :math:`\I32.\CONST~d` from the stack. -9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -10. Pop the value :math:`\reff_1` from the stack. +14. Pop the value :math:`\reff_1` from the stack. -11. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +15. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -12. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +16. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -13. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +17. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -14. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +18. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -15. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +19. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -16. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +20. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -17. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +21. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +22. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +23. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -20. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +24. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -21. If :math:`n = 0`, then: +25. If :math:`n = 0`, then: a. Return. -22. If :math:`d \leq s`, then: +26. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1184,7 +1190,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute the instruction :math:`\ARRAYGET~y`. + e. Execute :math:`\getfield(\X{st})`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1200,7 +1206,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -23. Else: +27. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1214,7 +1220,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute the instruction :math:`\ARRAYGET~y`. + g. Execute :math:`\getfield(\X{st})`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1226,9 +1232,9 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -24. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +28. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -25. Execute the instruction :math:`\ARRAYCOPY~x~y`. +29. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -1248,30 +1254,40 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d \leq s) + (\otherwise, \iff d \leq s \land F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \\ \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d > s) + (\otherwise, \iff d > s \land F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \\ \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \\[1ex] S; \val~(\I32.\CONST~d)~(\REFNULL~t)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \end{array} +Where: + +.. _aux-getfield: + +.. math:: + \begin{array}{lll} + \getfield(\valtype) &=& \ARRAYGET \\ + \getfield(\packedtype) &=& \ARRAYGETU \\ + \end{array} + .. _exec-array.init_data: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 8d4efe959..57fafe27e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -541,7 +541,6 @@ The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31 The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. - .. index:: ! parametric instruction, value type pair: abstract syntax; instruction .. _syntax-instr-parametric: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1833fdc98..78ded3620 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -656,6 +656,11 @@ .. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}} +.. Instructions, meta functions + +.. |getfield| mathdef:: \xref{exec/instructions}{aux-getfield}{\F{getfield}} + + .. Binary Format .. -------------