Add prose for reduction rule of rethrow. #225
Conversation
I think this should be also updated to include handlers and `caught` to match the `rethrow` rule in WebAssembly#225.
There was a problem hiding this comment.
We extended labels to include an optional catch in validation:
label := catch'? resulttype
Is this not used in execution semantics? If we use this, can we this to guarantee there's a catch label on the stack, which is equivalent of having caught? I might be completely confused about different things... in which case please let me know.
I don't think you are confused, my problem is that I don't know how to use it there. So by validation we know that the l'th label of the context C has the form |
document/core/exec/instructions.rst
Outdated
|
|
||
| 3. Assert: due to :ref:`validation <valid-rethrow>`, :math:`L` is a catch label, i.e., a label of the form :math:`(\LCATCH~[t^\ast])`. | ||
|
|
||
| 4. Repeat :math:`l+1` times: |
There was a problem hiding this comment.
I suggest doing it only l times in the loop, so that you haven't skipped over the caught clause already.
There was a problem hiding this comment.
I removed the loop entirely, trying to avoid popping and pushing back the entire block context.
document/core/exec/instructions.rst
Outdated
|
|
||
| c. Pop the label from the stack. | ||
|
|
||
| 5. Assert: due to **TODO**, the last two instructions popped are a |CAUGHTadm| instruction and the :math:`l+1`-th label, in that order. |
There was a problem hiding this comment.
I'd use typing of rethrow as a proxy.
There was a problem hiding this comment.
Can you elaborate a little more?
There was a problem hiding this comment.
I removed the loop as mentioned in the previous comment, and replaced the assertion with:
3. Assert: due to :ref:`validation <valid-rethrow>`, :math:`L` is a catch label, i.e., a label of the form :math:`(\LCATCH~[t^\ast])`, which is a label followed by a caught exception in an active catch clause.
Is that formulation ok @rossberg ?
document/core/exec/instructions.rst
Outdated
|
|
||
| 6. Let :math:`\CAUGHTadm\{a~\val^\ast\}` be the instruction after the label :math:`L`. | ||
|
|
||
| 7. Put all the popped values back on the stack, except the last instruction, the |RETHROW|. |
There was a problem hiding this comment.
That seems really odd. As commented elsewhere, I think we should avoid this.
There was a problem hiding this comment.
How do you think can we avoid this? Can we use a concept of shadow stack or something, so we don't really pop the values in 4-a-i above but just scan through it?
Should we do this looping thing in 4-a-i after all? All other branch-like instructions do it so there must be a reason, but can't we just say, because of validation, we can assert Lth is a catch label with type [t*]->[] and L-1th is a caught instruction because of try-catch execution rule, and just refer to the vals?
There was a problem hiding this comment.
As mentioned above, I just pushed an attempt to avoid all this pushing a popping. WDYT?
document/core/exec/instructions.rst
Outdated
|
|
||
| 8. Push the values :math:`\val^\ast` onto the stack. | ||
|
|
||
| 8. :ref:`Throw <exec-throwadm>` an exception with :ref:`tag address <syntax-tagaddr>` :math:`a`. |
There was a problem hiding this comment.
I think you somehow need to jump to the right point first.
There was a problem hiding this comment.
Where is the right point? Shouldn't we throw the exception in the original location?
document/core/exec/instructions.rst
Outdated
|
|
||
| 6. Let :math:`\CAUGHTadm\{a~\val^\ast\}` be the instruction after the label :math:`L`. | ||
|
|
||
| 7. Put all the popped values back on the stack, except the last instruction, the |RETHROW|. |
There was a problem hiding this comment.
How do you think can we avoid this? Can we use a concept of shadow stack or something, so we don't really pop the values in 4-a-i above but just scan through it?
Should we do this looping thing in 4-a-i after all? All other branch-like instructions do it so there must be a reason, but can't we just say, because of validation, we can assert Lth is a catch label with type [t*]->[] and L-1th is a caught instruction because of try-catch execution rule, and just refer to the vals?
document/core/exec/instructions.rst
Outdated
|
|
||
| c. Pop the label from the stack. | ||
|
|
||
| 5. Assert: due to **TODO**, the last two instructions popped are a |CAUGHTadm| instruction and the :math:`l+1`-th label, in that order. |
There was a problem hiding this comment.
Can you elaborate a little more?
ioannad
changed the title
Why WIP:
--------
I'm not sure how to justify step 5 of the prose, that is
how to assert that the lth label surrounding a rethrow instruction
has a CAUGHTadm{a val*} next to it.
- Also slightly changed notation to match the [formal overview document](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md).
Co-authored-by: Heejin Ahn <[email protected]>
Co-authored-by: Heejin Ahn <[email protected]>
I no longer consider this PR a WIP.
ioannad
force-pushed
the
spec-prose-exec-rethrow
branch
from
1edf74d to
a3ec6f5
Compare
|
The force push was to rebase to the current exception-handling/main, to make sure all checks pass before merging. |
FWIW, instead of rebase you can simply merge |
|
@rossberg sorry about that, it was careless, because the PR is approved. |
Why WIP:I'm not sure how to justify step 5 of the prose, that is how to assert that the lth label surrounding a rethrow instruction has a CAUGHTadm{a val*} next to it.