Skip to content
This repository has been archived by the owner on Nov 3, 2021. It is now read-only.

[spec] Adapt OOB behaviour in spec; store typing #129

Merged
merged 12 commits into from
Nov 23, 2019
Merged

[spec] Adapt OOB behaviour in spec; store typing #129

merged 12 commits into from
Nov 23, 2019

Conversation

rossberg
Copy link
Member

@rossberg rossberg commented Nov 21, 2019

This does the necessary spec changes to address #127 and #128:

  • Spec new OOB behaviour with early checks and trapping on size 0 (again).
  • Extend store typing and store extension to element and data instances.
  • Some streamlining.

Baseline is #126; all changes outside spec dir are from that PR.

Any volunteers for reviewing?

Copy link
Contributor

@eqrion eqrion left a comment

Choose a reason for hiding this comment

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

Thanks for doing this! Overall it looks great.

I did an amateur pass through here in order to keep this moving. I believe I understand the execution semantics part of the spec fairly well. I have less of solid understanding of store typing and extension semantics, so I only verified that the new text matched the existing text's form well.

document/core/appendix/index-rules.rst Outdated Show resolved Hide resolved
document/core/appendix/index-rules.rst Outdated Show resolved Hide resolved
\\ \qquad
(\otherwise)
\\[1ex]
S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~\MEMORYFILL
Copy link
Contributor

Choose a reason for hiding this comment

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

Out of curiosity, why the choice of 'n+1' and 'n' here? As opposed to 'n' and 'n-1'.

Copy link
Member Author

Choose a reason for hiding this comment

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

Ah, because that avoids having to put n > 0 as an extra side condition and it makes the inductive nature of the definition more apparent.

@@ -722,13 +716,15 @@ Memory Instructions

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[\X{ma}]`.

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
Copy link
Contributor

Choose a reason for hiding this comment

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

I believe this should be dropped.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done.


25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
24. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
Copy link
Contributor

Choose a reason for hiding this comment

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

Numbering needs to be corrected here.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done.


c. Push the value :math:`\I32.\CONST~1` to the stack.
e. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack.
Copy link
Contributor

Choose a reason for hiding this comment

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

Ditto the store stack argument ordering issue from above.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done.


a. Push the value :math:`\I32.\CONST~dst` to the stack.
d. Execute the instruction :math:`\TABLESET`.
Copy link
Contributor

Choose a reason for hiding this comment

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

I don't think table.set has a full definition in this spec yet, but if it will match reftypes then we need to push the destination offset first. Like with i32.store.

Copy link
Member Author

Choose a reason for hiding this comment

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

It actually has a temporary one below as and administrative instruction. But yes, this is superceded by the reftype proposal.

Copy link
Contributor

Choose a reason for hiding this comment

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

Oh nice, I missed there was an entry in execution for it. I took a look at it and it does first pop funcelem, then the offset. So we need to push the dest offset before source offset here, like with memory.copy. This needs a change in the 'else' branch and the formal semantics as well.

Copy link
Member Author

Choose a reason for hiding this comment

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

Indeed. Done!


14. If :math:`d \leq s`, then:

a. Push the value :math:`\I32.\CONST~d` to the stack.
Copy link
Contributor

Choose a reason for hiding this comment

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

I believe you meant to load from the source offset here.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done.


25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
24. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
Copy link
Contributor

Choose a reason for hiding this comment

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

Numbering needs to be corrected here.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done.


19. Push the value :math:`\I32.\CONST~dst` to the stack.
20. Push the value :math:`\funcelem` to the stack.
Copy link
Contributor

Choose a reason for hiding this comment

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

It may be more clear to reorder to 18, 20, then 19 so that the use of the funcelem value is right next to the definition.

Additionally, it's a bit odd to use funcelem here as a value, but I understand that's due to reftypes being a separate proposal. Is the intention for this to be an administrative instruction like table.get/set in the mean time?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, exactly. This is all a temporary hack. We screwed up the dependencies for these proposals.

rossberg and others added 2 commits November 22, 2019 07:42
Co-Authored-By: Ryan Hunt <rhunt@eqrion.net>
@rossberg
Copy link
Member Author

Thanks for that thorough review!

@eqrion
Copy link
Contributor

eqrion commented Nov 22, 2019

I took another look and left one more comment. After that, this and the interpreter change should be ready to go!

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants