Add prose for reduction rules involving thrown exceptions, by ioannad · Pull Request #226 · WebAssembly/exception-handling

ioannad · 2022-09-07T18:29:22Z

i.e., prose for some execution steps for THROWadm, CATCHadm, DELEGATEadm.

The parts of this commit that involve DELEGATEadm may change once PR #220 is settled.

Nonetheless, in this commit the typing rule and the reduction rule for DELEGATEadm are both tentatively changed to match the current formal overview.

i.e., explaining some execution steps for `THROWadm`, `CATCHadm`, `DELEGATEadm`. The parts of this commit that involve `DELEGATEadm` may change once PR WebAssembly#220 is settled. Nonetheless, in this commit the typing rule and the reduction rule for `DELEGATEadm` are both tentatively changed to match the current [formal overview](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md).

document/core/appendix/properties.rst

document/core/exec/instructions.rst

aheejin · 2022-09-13T02:08:49Z

Gentle ping :)

Co-authored-by: Heejin Ahn <aheejin@gmail.com>

document/core/exec/instructions.rst

rossberg · 2022-09-16T09:44:31Z

document/core/exec/instructions.rst

+   \CATCHadm~\XT[\val^n~(\THROWadm~a)]~\END &\stepto&
+   \XT[\val^n~(\THROWadm~a)] \\
+   \CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto&
+   \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END  \\


I don't think this formulation works, since you don't know what n is without looking up a's arity in the store in every single rule. You could do that, but the previous formulation instead keeps XT around in the latter rule so that extracting the right number of values from it can be delayed until the handler is found (where you have to look it up again).

Oh, I see, thank you! switching to the previous throw contexts and adding your commend as explainer.

@rossberg
I'm not sure any more what this review comment means, in particular which formulation it refers to. I think I misunderstood when I thought it refers to previous formulation of throw contexts, because IIUC any non-trivial throw context would still have the exception payload values val^n inside the square brackets with the throw (\XT[val^n (throw a)]).

Which previous formulation are you referring to?

I believe you can just use \XT[(throw a)], since the context will cover any val* anyway.

In this case, I'm not sure how to write the reduction for a CATCHadm with an empty list of catch clauses.

\CATCHadm~\XT[\THROWadm~a]~\END & \stepto & ???

Nevermind my last comment, I think I got it right with the latest commits.

rossberg · 2022-09-16T09:44:57Z

document/core/exec/instructions.rst


+.. note::
+   Note that the reduction step resulting in a |CAUGHTadm| instruction is the only one that does not preserve the throw context.
+   While a |THROWadm| propagates through the stack, the throw context |XT| is collected


This does not explain why, but see above.

@rossberg this comment is now removed, but I'm still not sure why the rules keep the throw context, so I added a todo:: to add an explanation why or what's the meaning of apparently preserving the throw context in some of the rules.

Thank you for the explanation via email, I included it as a note.

rossberg · 2022-09-16T09:46:37Z

document/core/exec/instructions.rst

+
+ 5. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:
+
+    a. Pop the top element from the stack, prepending it to the :ref:`throw context <syntax-ctxt-throw>` of the exception: :math:`\XT[\val^n~(\THROWadm~a)]`.


The spec so far carefully avoids to use the notion of contexts in the prose. I think you can reformulate this in a way more similar to branches, where there is no need to mention XT.

Removed everything after ", prepending".

rossberg · 2022-09-16T10:16:37Z

document/core/exec/instructions.rst

+       i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack.

+       ii. Jump to the start of the instruction sequence :math:`\instr^\ast`.


I believe this ought to be formulated in terms of a separate step of "Entering a catch clause", mirroring the exit you have already introduced. (Same below)

rossberg · 2022-09-16T10:21:55Z

document/core/exec/instructions.rst

+
+    a. While the instruction on the top of the stack is not a label, do:
+
+       i. Pop the instruction from the stack, without pushing it to |XT|.


The informal stack does not contain "instructions", only value, labels, frames, and now handlers and catch clauses. We probably need to find a common name for those ("control frames"?).

Also, the formulation of br has to change, since it no longer just skips over values, it also pops EH-related control frames.

Rephrased to a. Pop the top element from the stack.

Should I make a new PR rephrasing document/core/exec/runtime.rst to add control frames anyway?

Just for the record, the formulation of br is now changed by merged PR #233.

I no longer think we need to define "control frame". Just pop the "top element", as you wrote above.

rossberg · 2022-09-16T10:23:09Z

document/core/exec/instructions.rst

+
+   c. Pop the label from the stack.
+
+16. Push the throw context that we collected so far :math:`\XT[\val^n~(\THROWadm~a)]` onto the stack.


Yeah, I'm not sure what that would mean. I think we need a wording without XT.

I'm not sure how to search the stack for a handler without popping stuff from it. So I don't know how to describe keeping the throw context in these rules.

Why do you need to keep the context in the prose? Above, it has already popped the operands val^n, and that's all you need to keep AFAICS.

Don't we need it to return the entire stack if the exception is not handled?

@rossberg I removed this now to just popping the stack, like above. Should the uncaught exceptions be changed to val^n (throw a)?

See my email: you need to allow (uncaught) exceptions as stack elements and push it as that.

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

CATCHadm, DELEGATEadm, and CAUGHTadm in the prose of `exec-throwadm`. Split CAUGHTadm steps into a new section `exec-caughtadm-enter`, as suggested in review. Used the suggested name "catch clause" for `CAUGHTadm`, as well as for the clauses of a catching exception handler, also in the runtime definition of handlers.

…HTadm step, all in the prose of `exec-throwadm`. - All mentions of throw contexts are removed from the prose, which leaves only `val^n (throw a)` in case of an unhandled exception. - The loop of delegating handlers popped the last label too which is wrong, the throw should happen inside the `l+1`th surrounding block. - Forgotten to rephrase the steps pushing CAUGHTadm when section `exec-caughtadm-enter` was added in a previous commit.

document/core/exec/instructions.rst

rossberg · 2022-12-15T13:06:48Z

document/core/exec/instructions.rst

It seems off that this is under else but what follows is not.

I am changing this to

8. Else assert: there is an :ref:`exception handler <syntax-handler>` :math:`H` on the top of the stack.

This way I hope it's clear that everything that follows is under the else, given that the other branch of the "If" (7.a) returns.

Or would you prefer that everything that follows is nested under 8.?

rossberg · 2022-12-15T13:07:30Z

document/core/exec/instructions.rst

Is this assertion needed? That appears to be true by definition of exception handler.

Removing this line.

rossberg · 2022-12-15T13:10:08Z

document/core/exec/instructions.rst

Let's turn this use of goto into a structured while loop. ;)

rossberg · 2022-12-15T13:11:08Z

document/core/exec/instructions.rst

Same nesting oddity here.

Since the other "if" branch does not end with a clear "return", here I am putting the rest of the steps nested under the "Else".

rossberg · 2022-12-15T13:14:19Z

document/core/exec/instructions.rst

What is this step? L doesn't even seem to be used.

rossberg · 2022-12-15T13:19:41Z

document/core/exec/instructions.rst

You defined how to enter it, but not how it is exited.

Perhaps we don't need these auxiliary definitions for something as simple as this. Just push the value, enter the instruction sequence, pop the exception.

Should I rename section _exec-caughtadm to _exec-caughtadm-exit or remove both sections _exec-caughtadm-enter and _exec-caughtadm, and merge their steps into this prose directly?

rossberg · 2022-12-15T13:20:22Z

document/core/exec/instructions.rst

@@ -3077,66 +3077,69 @@ on the top of the stack.

 5. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:


See comment above.

This sounds like the answer to my question above, is to remove both sections _exec-caughtadm-enter and _exec-caughtadm, and merge their steps into the exec-throwadm prose directly?

document/core/exec/runtime.rst

rossberg · 2022-12-15T13:32:50Z

document/core/exec/instructions.rst

+
+13. Assert: due to :ref:`validation <valid-delegate-admin>`, the stack contains at least :math:`l+1` labels.
+
+14. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero.


This would be much simpler to express after the loop below.

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

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

as it doesn't make sense on its own in WebAssembly#246.

* 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

Uses the "current" version of exception results, as it will be changed by WebAssembly#226.

…ons.

document/core/exec/runtime.rst

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

…to spec-prose-exec-throwadm-catchadm-delegateadm

document/core/exec/runtime.rst

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

aheejin reviewed Sep 9, 2022

View reviewed changes

document/core/appendix/properties.rst Outdated Show resolved Hide resolved

document/core/exec/instructions.rst Outdated Show resolved Hide resolved

document/core/exec/instructions.rst Outdated Show resolved Hide resolved

document/core/exec/instructions.rst Outdated Show resolved Hide resolved

ioannad and others added 2 commits September 16, 2022 03:18

Reverted unrelated changes as per review suggestion.

a1eafea

Apply suggestions from code review

96c4cef

Co-authored-by: Heejin Ahn <aheejin@gmail.com>

rossberg suggested changes Sep 16, 2022

View reviewed changes

ioannad and others added 5 commits October 21, 2022 14:03

Apply suggestions from code review

fce7d16

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

Fixed typo in the CACTCHadm->CAUGHTadm execution step

a027b13

Merge branch 'main' into spec-prose-exec-throwadm-catchadm-delegateadm

35f8c5b

rossberg reviewed Dec 15, 2022

View reviewed changes

ioannad and others added 3 commits January 10, 2023 01:34

Apply suggestions from code review

fbb0c95

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

Merge branch 'main' into spec-prose-exec-throwadm-catchadm-delegateadm

34c7fed

ioannad added a commit to ioannad/exception-handling that referenced this pull request Feb 15, 2023

Applied suggestions from code review, fixed notation.

4455a72

- Also added the missing _n to CAUGHTadm. The subscript is introduced by the changes in PR WebAssembly#226

ioannad mentioned this pull request Feb 15, 2023

Adds explanatory prose related to delegate. #246

Merged

ioannad added a commit to ioannad/exception-handling that referenced this pull request Feb 15, 2023

Reverting these changes here, will be added to WebAssembly#226 shortly

160338e

Added the missing prose here after all

99a72e2

as it doesn't make sense on its own in WebAssembly#246.

ioannad added a commit to ioannad/exception-handling that referenced this pull request Feb 16, 2023

Adds validation for exception results.

cbe1701

Uses the "current" version of exception results, as it will be changed by WebAssembly#226.

ioannad mentioned this pull request Feb 16, 2023

Adds validation for exception results. #254

Merged

Fix the "formal examples" to use the updated administrative instructi…

8c66cbe

…ons.

rossberg reviewed Feb 21, 2023

View reviewed changes

document/core/exec/runtime.rst Show resolved Hide resolved

document/core/exec/runtime.rst Outdated Show resolved Hide resolved

document/core/exec/runtime.rst Outdated Show resolved Hide resolved

ioannad and others added 3 commits February 22, 2023 22:20

Apply suggestions from code review

544fb7d

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

removed explicit parens from productions

701f52b

Merge remote-tracking branch 'WebAssembly/exception-handling/main' in…

c8bd77e

…to spec-prose-exec-throwadm-catchadm-delegateadm

rossberg approved these changes Feb 23, 2023

View reviewed changes

document/core/exec/runtime.rst Outdated Show resolved Hide resolved

document/core/exec/runtime.rst Outdated Show resolved Hide resolved

Apply suggestions from code review

87a41f8

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

ioannad merged commit 8f732b8 into WebAssembly:main Mar 1, 2023


		5. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:

		a. Pop the top element from the stack, prepending it to the :ref:`throw context <syntax-ctxt-throw>` of the exception: :math:`\XT[\val^n~(\THROWadm~a)]`.

		i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack.

		ii. Jump to the start of the instruction sequence :math:`\instr^\ast`.


		a. While the instruction on the top of the stack is not a label, do:

		i. Pop the instruction from the stack, without pushing it to \|XT\|.


		c. Pop the label from the stack.

		16. Push the throw context that we collected so far :math:`\XT[\val^n~(\THROWadm~a)]` onto the stack.

		@@ -3077,66 +3077,69 @@ on the top of the stack.

		5. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:


		13. Assert: due to :ref:`validation <valid-delegate-admin>`, the stack contains at least :math:`l+1` labels.

		14. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero.

Conversation

ioannad commented Sep 7, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aheejin commented Sep 13, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ioannad Dec 9, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rossberg Dec 15, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ioannad Nov 30, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ioannad Dec 9, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

ioannad Dec 9, 2022 •

edited

Loading

rossberg Dec 15, 2022 •

edited

Loading

ioannad Nov 30, 2022 •

edited

Loading

ioannad Dec 9, 2022 •

edited

Loading