Address additional review of #222, also fixing label types everywhere. #241
Conversation
… everywhere. This addresses additional review comments to PR WebAssembly#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`.
document/core/appendix/algorithm.rst
Outdated
| @@ -122,9 +123,16 @@ The control stack is likewise manipulated through auxiliary functions: | |||
| ctrls.pop() | |||
| return frame | |||
|
|
|||
| func label_types(frame : ctrl_frame) : list(val_types) = | |||
| func label_val_types(frame : ctrl_frame) : list(val_type) = | |||
There was a problem hiding this comment.
It was in the spirit of now calling such labeltypes "label types" , as requested in this comment but I see now that I may have overdone it. :) Reverting/removing as suggested.
document/core/appendix/algorithm.rst
Outdated
| @@ -51,6 +51,7 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr | |||
| end_types : list(val_type) | |||
| height : nat | |||
| unreachable : bool | |||
| catch_label : bool | |||
There was a problem hiding this comment.
I don't think we need this flag, given that we already store the opcode.
document/core/appendix/algorithm.rst
Outdated
|
|
||
| func set_catch(catch : bool) = | ||
| error_if(ctrls.is_empty()) | ||
| ctrls[0].catch_label := catch |
document/core/appendix/algorithm.rst
Outdated
| The type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. | ||
| The result type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from. | ||
|
|
||
| Whether a label has :ref:`label type <syntax-labeltype>` with present |LCATCH| is stored with the boolean :math:`catch_label` of the frame, which can be checked with :math:`is_catch`, or modified in the top control frame with :math:`set_catch`. |
document/core/appendix/algorithm.rst
Outdated
| @@ -219,32 +229,34 @@ Other instructions are checked in a similar manner. | |||
| error_if(frame.opcode =/= try || frame.opcode =/= catch) | |||
| let params = tags[x].type.params | |||
| push_ctrl(catch, params , frame.end_types) | |||
| if (frame.opcode =/= try) then set_catch(true) | |||
document/core/appendix/algorithm.rst
Outdated
|
|
||
| case (catch_all) | ||
| let frame = pop_ctrl() | ||
| error_if(frame.opcode =/= try || frame.opcode =/= catch) | ||
| push_ctrl(catch_all, [], frame.end_types) | ||
| if (frame.opcode =/= try) then set_catch(true) |
| }{ | ||
| S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] |
There was a problem hiding this comment.
This does seem misplaced. I was trying to follow the formulation for the typing of \DELEGATEadm in the formal overview, but not only this change is misplaced here, but it seems unnecessary to change this in the appendix, given the latest comment on the DELEGATEadm typing rule.
Reverting this change.
document/core/valid/instructions.rst
Outdated
| @@ -1458,11 +1460,11 @@ Control Instructions | |||
| :math:`\RETHROW~l` | |||
| .................. | |||
|
|
|||
| * The label :math:`C.\CLABELS[l]` must be defined in the context. | |||
| * The label type :math:`C.\CLABELS[l]` must be defined in the context. | |||
There was a problem hiding this comment.
Actually, it is the label that must be defined (with a type). So I'd revert this (similarly several occurrences below).
There was a problem hiding this comment.
Done, for the other occurrences as well.
Co-authored-by: Andreas Rossberg <[email protected]>
| * The label type :math:`C.\CLABELS[0]` must be defined in the context. | ||
|
|
||
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. | ||
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. |
There was a problem hiding this comment.
C is an (implicit) input to the rules, so you'll have to write the prose the other way round, i.e., first check that the last entry is [t*], then define C' to be C with that entry updated. (That means that the C in the prose and the C in the formal rule denote different contexts, but I think that's fine.)
There was a problem hiding this comment.
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :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])` prepended to the |CLABELS| vector. |
Isn't type missing? All other similar clauses have it.
@rossberg Not sure if I understand. Also I wonder if making C's meaning different from that in the equation will be confusing.. Can we change the equation to use the same symbol?
There was a problem hiding this comment.
Yes, we could use C' in the formal rule, though the tick would just be noise there. In general, I have opted to not artificially complicate the formal rules for the sake of the prose, though this case is minor enough.
Adding type sounds okay be me.
There was a problem hiding this comment.
Then can we change the symbol in the prose?
There was a problem hiding this comment.
Actually I'm not sure if I understood your comment correctly:
C is an (implicit) input to the rules, so you'll have to write the prose the other way round, i.e., first check that the last entry is
[t*], then define C' to be C with that entry updated.
Can you elaborate a little more on what this means? And if the symbols don't cause much confusion, that might be fine.
There was a problem hiding this comment.
In the formal rules, the context is always explicit. We just call it C, or something else, and we can even "pattern match" it in the rules, which is what happens in the rule for caught. This implicitly imposes a constraint, because the rule is only applicable if the context has that specific form.
In the prose, the context is treated as a parameter to the "algorithm". And we keep it implicit to avoid more excessive verbosity. That implicit context is available under the fixed name C. This convention is described here. A constraint on that context (e.g., the presence of a certain entry) then has to be checked explicitly.
There was a problem hiding this comment.
Moved these changes to PR #244, reverting these changes to whatever the document had previously.
There was a problem hiding this comment.
Please ignore the last two commits (the second reverting the first) - the changes to the typing of CAUGHTadm were already reverted.
Changes to the typing of CAUGHTadm are now done in PR #244.
| * The label type :math:`C.\CLABELS[0]` must be defined in the context. | ||
|
|
||
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector. | ||
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. |
There was a problem hiding this comment.
| * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :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])` prepended to the |CLABELS| vector. |
Isn't type missing? All other similar clauses have it.
@rossberg Not sure if I understand. Also I wonder if making C's meaning different from that in the equation will be confusing.. Can we change the equation to use the same symbol?
The rule is intended as is, the purpose being that it refines the existing label binding to a catch label, enabling its use for rethrow in the premise. |
Co-authored-by: Heejin Ahn <[email protected]>
Changes to this rule are now done in PR WebAssembly#244
This reverts commit 77090e2.
|
@aheejin @rossberg |
* Fixes the typing rule of CAUGHTadm as suggested in: #229 (comment) * Applying suggestion from PR #241 https://github.com/WebAssembly/exception-handling/pull/241/files/201ff276be6c458e7a819662eb2862bd475f2fcd..f97c9d108a999c3c3fd30f25554a113822bed1b8#r1030097793 * Applied suggestions from code review, fixed notation, also adding the missing _n to CAUGHTadm. The subscript is introduced by the changes in PR #226
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
catchandcatch_all.