Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update array.copy semantics to handle packed types #416

Merged
merged 5 commits into from
Sep 9, 2023
Merged

Update array.copy semantics to handle packed types #416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
028daa2
Update array.copy semantics to handle packed types
tlively Aug 24, 2023
8e3581d
getfield meta function
tlively Sep 8, 2023
e04ecbd
move auxiliary function
tlively Sep 9, 2023
31444ad
pop i32.const fixes
tlively Sep 9, 2023
aa173f6
format conditions on single line
tlively Sep 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
80 changes: 48 additions & 32 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <valid-array.copy>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]` exists.

1. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack.
2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]`.

2. Pop the value :math:`n` from the stack.

3. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack.
3. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.

4. Pop the value :math:`s` from the stack.
4. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded <aux-expand-deftype>` :ref:`array type <syntax-arraytype>` :math:`\deftype`.

5. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~y)` is on the top of the stack.
5. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :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 <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :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 <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :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 <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :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 <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~x)` is on the top of the stack.
13. Assert: due to :ref:`validation <valid-array.copy>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :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 <valid-array.copy>`, :math:`\reff_1` is an :ref:`array reference <syntax-ref.array>`.
16. Assert: due to :ref:`validation <valid-array.copy>`, :math:`\reff_1` is an :ref:`array reference <syntax-ref.array>`.

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 <valid-array.copy>`, :math:`\reff_2` is an :ref:`array reference <syntax-ref.array>`.
19. Assert: due to :ref:`validation <valid-array.copy>`, :math:`\reff_2` is an :ref:`array reference <syntax-ref.array>`.

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 <valid-array.copy>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a_1]` exists.
21. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a_1]` exists.

18. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a_2]` exists.
22. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`array instance <syntax-arrayinst>` :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.

Expand All @@ -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`.

Expand All @@ -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.

Expand All @@ -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`.

Expand All @@ -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]
Expand All @@ -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:

Expand Down
1 change: 0 additions & 1 deletion document/core/syntax/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
5 changes: 5 additions & 0 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
.. -------------
Expand Down