This repository was archived by the owner on Apr 25, 2025. It is now read-only.
Fixes the typing rule of CAUGHTadm #244
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Fixes the typing rule of CAUGHTadm as suggested in: WebAssembly#229 (comment)
ioannad
added a commit
to ioannad/exception-handling
that referenced
this pull request
Nov 26, 2022
Changes to this rule are now done in PR WebAssembly#244
rossberg
approved these changes
Dec 15, 2022
Comment on lines
683
to
685
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the first label popped from the |CLABELS| vector. | ||
|
|
||
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. | ||
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C'`, but with the label type :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. |
There was a problem hiding this comment.
I think you can merge these:
Suggested change
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the first label popped from the |CLABELS| vector. | |
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. | |
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C'`, but with the label type :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. | |
| * Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label type :math:`(\LCATCH~[t^\ast])` replacing the first element of the |CLABELS| vector. |
There was a problem hiding this comment.
For some reason I couldn't apply the suggestions but I added these changes to the latest commit I just pushed.
| }{ | ||
| S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] | ||
| S; C',\CLABELS\,(\LCATCH^?~[t^\ast]) \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] |
There was a problem hiding this comment.
I don't think we can or want to allow this to be a catch label beforehand already.
Suggested change
| S; C',\CLABELS\,(\LCATCH^?~[t^\ast]) \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] | |
| S; C',\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] |
ioannad
added a commit
that referenced
this pull request
Dec 23, 2022
#241) This addresses additional review comments to PR #222, that were made after it was merged. The last review comment in the discussion suggests to adjust all validation labels to use label types instead of just result types. Should address all occurrences of validation labels. Additionally adds a boolean catch_label to control frames in the validation algorithm, and some related functionality, fixing the cases for opcodes `catch` and `catch_all`. * Apply suggestions from code review Co-authored-by: Andreas Rossberg <[email protected]> Co-authored-by: Heejin Ahn <[email protected]> * Reverting changes to typing of CAUGHTadm. Changes to this rule are now done in PR #244
ioannad
added a commit
to ioannad/exception-handling
that referenced
this pull request
Feb 15, 2023
In particular:
- Switched to
handler ::= (tagaddr? instr*)* | labelidx
exn ::= tagaddr val*
instr ::= … | handler_n{handler} instr* end | caught_n{exn} instr* end
removing DELEGATEadm
- Changed prose to just push and pop handlers and exceptions, in the runtime,
in the execution steps of the instructions, in the formal overview,
and partly in appendix/properties.
Not done:
- Did not change the notation and prose for CAUGHTadm
in appendix/properties.rst, this will be done in PR WebAssembly#244.
- Also added the missing _n to CAUGHTadm. The subscript is introduced by the changes in PR WebAssembly#226
|
Applied the suggestions manually, it seemed impossible otherwise. Merging. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Addresses review comment on merged #229:
#229 (comment)