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.

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

Execution prose for bulk array operations #408

Merged
merged 4 commits into from
Jul 22, 2023
Merged

Conversation

tlively
Copy link
Member

@tlively tlively commented Jul 21, 2023

Add execution prose for array.fill, array.copy, array.init_data, and
array.init_elem. As a drive by consistency fix, also remove unnecessary
parentheses around values in the prose for other GC instructions. These
parentheses do not appear in the prose for any other instruction.

Add execution prose for array.fill, array.copy, array.init_data, and
array.init_elem. As a drive by consistency fix, also remove unnecessary
parentheses around values in the prose for other GC instructions. These
parentheses do not appear in the prose for any other instruction.
@tlively tlively requested a review from rossberg July 21, 2023 17:10
@tlively
Copy link
Member Author

tlively commented Jul 21, 2023

Current dependencies on/for this PR:

This comment was auto-generated by Graphite.


3. Assert: due to :ref:`validation <valid-array.init_data>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.

4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This todo is elsewhere resolved in #406, you can copy from there. (Which also tweaks the wording of the previous bullet.)


a. Trap.

20. Let :math:`z` be the :ref:`bit width <bitwidth-fieldtype>` of :ref:`field type <syntax-fieldtype>` :math:`\X{ft}`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just noticed that the bitwidth of course is in bits, so we need to divide by 8, here and in the formal rules, as well as for array.new_data. Could you fix both?

Also, this could use an assertion that the bitwidth actually is defined (because ft is not a reference).


24. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft})`.

25. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`b^\ast`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here, this is only defined because of validation.


3. Assert: due to :ref:`validation <valid-array.init_elem>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.

4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See above.

@tlively
Copy link
Member Author

tlively commented Jul 22, 2023

Comments addressed. PTAL at the new assertions to see if they make sense.

@tlively tlively merged commit 6019487 into main Jul 22, 2023
@tlively tlively mentioned this pull request Jul 22, 2023
53 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants