From 98880374e961a4ca1d9a36df8f6bb602ec357ec1 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 7 Sep 2022 16:24:51 +0200 Subject: [PATCH 01/14] Add prose for reduction rules involving thrown exceptions, i.e., explaining 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](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md). --- document/core/appendix/properties.rst | 7 ++- document/core/exec/instructions.rst | 90 +++++++++++++++++++++++++-- 2 files changed, 88 insertions(+), 9 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index c9d831bc..7e14c72b 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -624,6 +624,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. index:: delegate, throw context +.. _valid-delegate-admin: :math:`\DELEGATEadm\{l\}~\instr^\ast~\END` .......................................... @@ -633,11 +634,11 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. math:: \frac{ - S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C \vdashinstrseq \instr^\ast : [] \to [t^\ast] \qquad - C.\CLABELS[l] = [t_0^\ast] + C.\CLABELS[l+1] = [t_0^\ast] }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] + S; C \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] } diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c775c937..de2518cd 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3016,26 +3016,104 @@ When the end of a :ref:`try ` instruction is reached without a jump, Throwing an exception with :ref:`tag address ` :math:`a` ........................................................................ +When an administrative throw occurs, then values, labels, |CAUGHTadm| instructions, +and call frames are popped if necessary, until an appropriate exception handler is found +on the top of the stack. + + 1. Assert: due to validation, :math:`S.\STAGS[a]` exists. + + 2. Let :math:`[t^n] \to []` be the :ref:`tag type ` :math:`S.\STAGS[a].\TAGITYPE`. + + 3. Assert: due to :ref:`validation `, there are :math:`n` values on the top of the stack. + + 4. Pop the :math:`n` values :math:`\val^n` from the stack. + + 5. While the stack is not empty and the top of the stack is not an :ref:`exception handler `, do: + + a. Pop the top element from the stack, prepending it to the :ref:`throw context ` of the exception: :math:`\XT[\val^n~(\THROWadm~a)]`. + + 6. Assert: The stack is now either empty, or there is an exception handler on the top of the stack. + + 7. If the stack is empty, then: + + a. **TODO** *Return a result value representing the uncaught exception (will probably just be the same as 11.a.i. below).* + .. todo:: - Add prose for the following execution steps. + After PR #221 is resolved, this step should be filled in with a PR to specify uncaught exception results. + +8. Else there is an :ref:`exception handler ` :math:`H` on the top of the stack. + +9. Pop the exception handler :math:`H` from the stack. + +10. Assert: :math:`H` is either of the form :math:`\CATCHadm\{a^?~\instr^\ast\}^k` or :math:`\DELEGATEadm\{l\}.` + +11. If :math:`H` is of the form :math:`\CATCHadm\{a^?~\instr^\ast\}^k`, then: + + a. If :math:`k = 0`, then: + + i. Push the throw context that we collected so far :math:`\XT[\val^n~(\THROWadm~a)]` onto the stack. + + b. Else :math:`H` is of the form :math:`\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast`. + + c. If :math:`a_1^? = \epsilon`, then: + + i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. + ii. Jump to the start of the instruction sequence :math:`\instr^\ast`. + + d. Else if :math:`a_1 = a`, then: + + i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. + + ii. Push the values :math:`\val^n` back to the stack. + + iii. Jump to the start of the instruction sequence :math:`\instr^\ast`. + + e. Else, repeat step 11 for :math:`H = \CATCHadm\{a'^?~\instr'^\ast\}^\ast`. + +12. Else the handler :math:`H` has the form :math:`\DELEGATEadm\{l\}`. + +13. Assert: due to :ref:`validation `, 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. + +15. Repeat :math:`l+1` times: + + 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|. + + b. Assert: due to :ref:`validation `, the top of the stack now is a label. + + 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. + +17. Jump to the continuation of :math:`L`. .. math:: \begin{array}{rcl} - \CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[(\THROWadm~a)]~\END &\stepto& - \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[(\THROWadm~a)]~\END \\ + \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 \\ && (\iff a_1^? \neq \epsilon \land a_1^? \neq a) \\ S;~\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& S;~\CAUGHTadm\{a~\val^n\}~(\val^n)?~\instr^\ast~\END \\ && (\iff~(a_1^? = \epsilon \lor a_1^? = a)~\land\\ && \ S.\STAGS[a].\TAGITYPE = [t^n]\to[]) \\ - \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[(\THROWadm~a)]~\END]~\END &\stepto& - \XT[(\THROWadm~a)] \\ + \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[\val^n~(\THROWadm~a)]~\END]~\END &\stepto& + \XT[\val^n~(\THROWadm~a)] \\ \end{array} +.. 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 + until the exception is caught inside a |CAUGHTadm| instruction, in which point it's discarded. .. todo:: - Add explainer note. + Add explainer note for the reduction of |DELEGATEadm|, when PR #221 is settled. + .. _exec-caughtadm: From a1eafea043c56e3f78798b90fe6352f9b5f963f6 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 16 Sep 2022 03:18:16 +0200 Subject: [PATCH 02/14] Reverted unrelated changes as per review suggestion. --- document/core/appendix/properties.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 7e14c72b..a6c22595 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -634,11 +634,11 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. math:: \frac{ - S; C \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \qquad - C.\CLABELS[l+1] = [t_0^\ast] + C.\CLABELS[l] = [t_0^\ast] }{ - S; C \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] } From 96c4cef56c3f2ca4997666a9c60f831eb2f203ba Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 16 Sep 2022 03:26:47 +0200 Subject: [PATCH 03/14] Apply suggestions from code review Co-authored-by: Heejin Ahn --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index de2518cd..836c39c3 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3020,7 +3020,7 @@ When an administrative throw occurs, then values, labels, |CAUGHTadm| instructio and call frames are popped if necessary, until an appropriate exception handler is found on the top of the stack. - 1. Assert: due to validation, :math:`S.\STAGS[a]` exists. + 1. Assert: due to :ref:`validation `,, :math:`S.\STAGS[a]` exists. 2. Let :math:`[t^n] \to []` be the :ref:`tag type ` :math:`S.\STAGS[a].\TAGITYPE`. @@ -3061,7 +3061,7 @@ on the top of the stack. ii. Jump to the start of the instruction sequence :math:`\instr^\ast`. - d. Else if :math:`a_1 = a`, then: + d. Else if :math:`a_1^? = a`, then: i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. From fce7d16547d835b13795ca5b0ac15a21b70381e3 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 21 Oct 2022 14:03:58 +0200 Subject: [PATCH 04/14] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 836c39c3..11a162e3 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3016,7 +3016,7 @@ When the end of a :ref:`try ` instruction is reached without a jump, Throwing an exception with :ref:`tag address ` :math:`a` ........................................................................ -When an administrative throw occurs, then values, labels, |CAUGHTadm| instructions, +When a throw occurs, then values, labels, active catch clauses, and call frames are popped if necessary, until an appropriate exception handler is found on the top of the stack. @@ -3107,9 +3107,9 @@ on the top of the stack. \end{array} .. note:: - Note that the reduction step resulting in a |CAUGHTadm| instruction is the only one that does not preserve the throw context. + The reduction step activating a catch clause |CAUGHTadm| is the only one that does not preserve the throw context. While a |THROWadm| propagates through the stack, the throw context |XT| is collected - until the exception is caught inside a |CAUGHTadm| instruction, in which point it's discarded. + until the exception is caught inside a |CAUGHTadm| instruction, at which point it is discarded. .. todo:: Add explainer note for the reduction of |DELEGATEadm|, when PR #221 is settled. From a027b13d7d8d059a060bcbbe94b4396bf5af51c6 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 18 Nov 2022 21:23:09 +0100 Subject: [PATCH 05/14] Fixed typo in the CACTCHadm->CAUGHTadm execution step --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 11a162e3..6db240d9 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3099,7 +3099,7 @@ on the top of the stack. \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END \\ && (\iff a_1^? \neq \epsilon \land a_1^? \neq a) \\ S;~\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& - S;~\CAUGHTadm\{a~\val^n\}~(\val^n)?~\instr^\ast~\END \\ + S;~\CAUGHTadm\{a~\val^n\}~(\val^n)^?~\instr^\ast~\END \\ && (\iff~(a_1^? = \epsilon \lor a_1^? = a)~\land\\ && \ S.\STAGS[a].\TAGITYPE = [t^n]\to[]) \\ \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[\val^n~(\THROWadm~a)]~\END]~\END &\stepto& From c71f62eb71c5ef10a762966fd5a77f077e445c13 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 25 Nov 2022 21:57:24 +0100 Subject: [PATCH 06/14] Rephrased explicit mentions of administrative instructions 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. --- document/core/exec/instructions.rst | 24 ++++++++++++++++-------- document/core/exec/runtime.rst | 12 ++++++------ 2 files changed, 22 insertions(+), 14 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6db240d9..e33fe130 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3045,21 +3045,19 @@ on the top of the stack. 9. Pop the exception handler :math:`H` from the stack. -10. Assert: :math:`H` is either of the form :math:`\CATCHadm\{a^?~\instr^\ast\}^k` or :math:`\DELEGATEadm\{l\}.` +10. Assert: :math:`H` is either of the a catching or a delegating :ref:`exception handler `. -11. If :math:`H` is of the form :math:`\CATCHadm\{a^?~\instr^\ast\}^k`, then: +11. If :math:`H` is a catching exception handler, let :math:`\{a^?~\instr^\ast\}^k` be its clauses. Then: a. If :math:`k = 0`, then: i. Push the throw context that we collected so far :math:`\XT[\val^n~(\THROWadm~a)]` onto the stack. - b. Else :math:`H` is of the form :math:`\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast`. + b. Else :math:`H`'s clauses are of the form :math:`\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast`. c. If :math:`a_1^? = \epsilon`, then: - i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. - - ii. Jump to the start of the instruction sequence :math:`\instr^\ast`. + i. :ref:`Enter ` :math:`\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. d. Else if :math:`a_1^? = a`, then: @@ -3071,7 +3069,7 @@ on the top of the stack. e. Else, repeat step 11 for :math:`H = \CATCHadm\{a'^?~\instr'^\ast\}^\ast`. -12. Else the handler :math:`H` has the form :math:`\DELEGATEadm\{l\}`. +12. Else the handler :math:`H` is a delegating handler, let :math:`l` be its label index. 13. Assert: due to :ref:`validation `, the stack contains at least :math:`l+1` labels. @@ -3107,7 +3105,7 @@ on the top of the stack. \end{array} .. note:: - The reduction step activating a catch clause |CAUGHTadm| is the only one that does not preserve the throw context. + The reduction step entering a catch clause |CAUGHTadm| is the only one that does not preserve the throw context. While a |THROWadm| propagates through the stack, the throw context |XT| is collected until the exception is caught inside a |CAUGHTadm| instruction, at which point it is discarded. @@ -3115,6 +3113,16 @@ on the top of the stack. Add explainer note for the reduction of |DELEGATEadm|, when PR #221 is settled. +.. _exec-caughtadm-enter: + +Entering :math:`\instr^\ast` with catch clause holding a caught exception :math:`\{a~\val^n\}` +.............................................................................................. + +1. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. + +2. Jump to the start of the instruction sequence :math:`\instr^\ast`. + + .. _exec-caughtadm: Holding a caught exception with |CAUGHTadm| diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index d3df56ae..8a3b4e3f 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -539,8 +539,8 @@ Exception handlers Exception handlers are installed by |TRY| instructions and are either *catching handlers* or *delegating handlers*. -Catching handlers start with the identifier |CATCHadm| and carry a mapping from :ref:`tag addresses ` -to their associated branch *targets*, each of which is expressed syntactically as a possibly empty sequence of +Catching handlers start with the identifier |CATCHadm| and contain catch clauses, which are mappings from :ref:`tag addresses ` +to their associated branch *targets*. Each catch clause is expressed syntactically as a possibly empty sequence of :ref:`instructions ` possibly following a :ref:`tag address `. If there is no :ref:`tag address `, the instructions of that target correspond to a |CATCHALL| clause. @@ -552,10 +552,10 @@ If there is no :ref:`tag address `, the instructions of that tar \production{(handler)} & \handler &::=& \CATCHadm\{\tagaddr^?~\instr^\ast\}^\ast &|& \DELEGATEadm\{l\} \end{array} -Intuitively, for each target :math:`\{\tagaddr^?~\instr^\ast\}` of a |CATCHadm|, :math:`\instr^\ast` is the *continuation* to execute -when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a target specifies no tag address. -In that case, we say that the exception is handled by the exception handler |CATCHadm|. -If this list of targets is empty, or if the tag address of the thrown exception is not in the handler's mapping and there is no |CATCHALL| clause, then the exception will be rethrown. +Intuitively, for each catch clause :math:`\{\tagaddr^?~\instr^\ast\}` of a catching handler, :math:`\instr^\ast` is the *continuation* to execute +when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a catch clause specifies no tag address. +In that case, the exception is handled, and that catch clause :ref:`entered `. +If this list of targets is empty, or if the tag address of the thrown exception is not in any of the catch clauses and there is no |CATCHALL| clause, then the exception will be rethrown. .. todo:: Add prose with intuition on delegating handlers. From bd742592321ba31ab790c618e3b5de3215c83792 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 9 Dec 2022 23:05:04 +0100 Subject: [PATCH 07/14] Removed throw contexts, fixed loop in delegating handlers, fixed CAUGHTadm 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 | 47 +++++++++++++++-------------- 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index f121093a..e7c0d4da 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3077,18 +3077,17 @@ 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 `, do: - a. Pop the top element from the stack, prepending it to the :ref:`throw context ` of the exception: :math:`\XT[\val^n~(\THROWadm~a)]`. + a. Pop the top element from the stack. 6. Assert: The stack is now either empty, or there is an exception handler on the top of the stack. 7. If the stack is empty, then: - a. **TODO** *Return a result value representing the uncaught exception (will probably just be the same as 11.a.i. below).* + a. Return the uncaught exception :math:`\val^n~(\THROWadm~a)` as a value. -.. todo:: - After PR #221 is resolved, this step should be filled in with a PR to specify uncaught exception results. +8. Else: -8. Else there is an :ref:`exception handler ` :math:`H` on the top of the stack. + a. Assert: there is an :ref:`exception handler ` :math:`H` on the top of the stack. 9. Pop the exception handler :math:`H` from the stack. @@ -3098,43 +3097,49 @@ on the top of the stack. a. If :math:`k = 0`, then: - i. Push the throw context that we collected so far :math:`\XT[\val^n~(\THROWadm~a)]` onto the stack. + i. Put the values :math:`\val^n` back onto the stack. + + ii. :ref:`Throw ` an exception with tag address :math:`a`. b. Else :math:`H`'s clauses are of the form :math:`\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast`. c. If :math:`a_1^? = \epsilon`, then: - i. :ref:`Enter ` :math:`\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. + i. :ref:`Enter ` :math:`\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. d. Else if :math:`a_1^? = a`, then: - i. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. + i. :ref:`Enter ` :math:`\val^n~\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. + + e. Else: + + i. Let :math:`H'` be the catching exception handler with clauses :math:`\{a'^?~\instr'^\ast\}^\ast`. - ii. Push the values :math:`\val^n` back to the stack. + ii. Repeat step 11 for :math:`H'`. - iii. Jump to the start of the instruction sequence :math:`\instr^\ast`. +12. Else: - e. Else, repeat step 11 for :math:`H = \CATCHadm\{a'^?~\instr'^\ast\}^\ast`. + a. Assert: :math:`H` is a delegating exception handler. -12. Else the handler :math:`H` is a delegating handler, let :math:`l` be its label index. +13. Let :math:`l` be the label index of :math:`H`. -13. Assert: due to :ref:`validation `, the stack contains at least :math:`l+1` labels. +14. Assert: due to :ref:`validation `, the stack contains at least :math:`l` labels. -14. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. +15. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. -15. Repeat :math:`l+1` times: +15. Repeat :math:`l` times: - a. While the instruction on the top of the stack is not a label, do: + a. While the top of the stack is not a label, do: - i. Pop the instruction from the stack, without pushing it to |XT|. + i. Pop the top element from the stack. b. Assert: due to :ref:`validation `, the top of the stack now is a label. 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. +16. Push the values :math:`\val^n` onto the stack. -17. Jump to the continuation of :math:`L`. +17. :ref:`Throw ` an exception with tag address :math:`a`. .. math:: \begin{array}{rcl} @@ -3153,11 +3158,9 @@ on the top of the stack. .. note:: The reduction step entering a catch clause |CAUGHTadm| is the only one that does not preserve the throw context. - While a |THROWadm| propagates through the stack, the throw context |XT| is collected - until the exception is caught inside a |CAUGHTadm| instruction, at which point it is discarded. .. todo:: - Add explainer note for the reduction of |DELEGATEadm|, when PR #221 is settled. + Explain why or what's the meaning of apparently preserving the throw context in the other rules. .. _exec-caughtadm-enter: From fbb0c959233d171e8dba3acb51d3da31b64a11f0 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Tue, 10 Jan 2023 01:34:16 +0100 Subject: [PATCH 08/14] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 2 +- document/core/exec/runtime.rst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index e7c0d4da..5f7edbdb 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3083,7 +3083,7 @@ on the top of the stack. 7. If the stack is empty, then: - a. Return the uncaught exception :math:`\val^n~(\THROWadm~a)` as a value. + a. Return the uncaught exception :math:`\val^n~(\THROWadm~a)` as a result. 8. Else: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 07e5616f..14e56208 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -552,7 +552,7 @@ If there is no :ref:`tag address `, the instructions of that han \end{array} Intuitively, for each catch clause :math:`\{\tagaddr^?~\instr^\ast\}` of a catching handler, :math:`\instr^\ast` is the *continuation* to execute -when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a catch clause specifies no tag address. +when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when the catch clause specifies no tag address. In that case, the exception is handled, and that catch clause :ref:`entered `. If this list of targets is empty, or if the tag address of the thrown exception is not in any of the catch clauses and there is no |CATCHALL| clause, then the exception will be rethrown. From 77144721f081172d66a407585066d60549ad927a Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 15 Feb 2023 16:41:38 +0100 Subject: [PATCH 09/14] Apply suggestions from code review and email communication. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 #244. --- document/core/appendix/properties.rst | 38 ++--- document/core/exec/instructions.rst | 137 ++++++++---------- document/core/exec/runtime.rst | 78 +++++----- document/core/util/macros.def | 4 +- .../Exceptions-formal-overview.md | 73 +++++----- 5 files changed, 161 insertions(+), 169 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index d3fa6957..3b26bf76 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -606,65 +606,65 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera } -.. index:: catch, throw context +.. index:: handler, throw context -:math:`\CATCHadm\{\tagaddr^?~\instr_1^\ast\}^\ast~\instr_2^\ast~\END` -..................................................................... +:math:`\HANDLERadm_n\{(\tagaddr^?~\instr_1^\ast)^\ast\}~\instr_2^\ast~\END` +........................................................................... * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^\ast]`. + the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^n]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`(\LCATCH~[t_2^\ast])` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`(\LCATCH~[t_2^n])` prepended to the |CLABELS| vector. * Under context :math:`C''`, for every :math:`\tagaddr^?` and associated instruction sequence :math:`\instr_1^\ast`: - * If :math:`\tagaddr^? = \epsilon`, then :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^\ast]`. + * If :math:`\tagaddr^? = \epsilon`, then :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^n]`. * Else: * The :ref:`external tag value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external tag type ` :math:`\ETTAG~[t_1^\ast] \to []`. - * The instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + * The instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^n]`. -* Then the compound instruction is valid under context :math:`C'` with type :math:`[] \to [t_2^\ast]`. +* Then the compound instruction is valid under context :math:`C'` with type :math:`[] \to [t_2^n]`. .. math:: \frac{ \begin{array}{@{}c@{}} ((S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_1^\ast]\to[])^? \\ - ~~S; C,\CLABELS\,(\LCATCH~[t_2^\ast]) \vdashinstrseq \instr_1^\ast : [(t_1^\ast)^?] \to [t_2^\ast])^\ast \\ - S; C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_2^\ast : [] \to [t_2^\ast] \\ + ~~S; C,\CLABELS\,(\LCATCH~[t_2^n]) \vdashinstrseq \instr_1^\ast : [(t_1^\ast)^?] \to [t_2^n])^\ast \\ + S; C,\CLABELS\,[t_2^n] \vdashinstrseq \instr_2^\ast : [] \to [t_2^n] \\ \end{array} }{ - S; C,\CLABELS\,[t_2^\ast] \vdashadmininstr \CATCHadm\{\tagaddr^?~{\instr_1}^\ast\}^\ast~\instr_2^\ast~\END : [] \to [t_2^\ast] + S; C,\CLABELS\,[t_2^n] \vdashadmininstr \HANDLERadm_n\{(\tagaddr^?~{\instr_1}^\ast)^\ast\}~\instr_2^\ast~\END : [] \to [t_2^n] } -.. index:: delegate, throw context -.. _valid-delegate-admin: +.. index:: handler, throw context +.. _valid-handleradm: -:math:`\DELEGATEadm\{l\}~\instr^\ast~\END` -.......................................... +:math:`\HANDLERadm_n\{l\}~\instr^\ast~\END` +........................................... * The label :math:`C.\CLABELS[l]` must be defined in the context. * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[]\to[t^\ast]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[]\to[t^n]`. -* Then the compound instruction is valid under context :math:`C'` with type :math:`[] \to [t^\ast]`. +* Then the compound instruction is valid under context :math:`C'` with type :math:`[] \to [t^n]`. .. math:: \frac{ - S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS\,[t^n] \vdashinstrseq \instr^\ast : [] \to [t^n] \qquad C.\CLABELS[l] = [t_0^\ast] }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] + S; C,\CLABELS\,[t^n] \vdashadmininstr \HANDLERadm_n\{l\}~\instr^\ast~\END : [] \to [t^n] } diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 5f7edbdb..6a92417d 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2643,26 +2643,26 @@ Control Instructions b. Let :math:`a_i` be the tag address :math:`F.\AMODULE.\MITAGS[x_i]`. - c. Let :math:`H_i` be the handler clause :math:`\{a_i~\instr_{2i}^\ast\}`. + c. Let :math:`H_i` be the handler :math:`(a_i~\instr_{2i}^\ast)`. 8. If there is a catch all clause :math:`(\CATCHALL~\instr_3^\ast)`, then: - a. Let :math:`H'^?` be the handler clause :math:`\{\epsilon~\instr_3^\ast\}`. + a. Let :math:`H'^?` be the handler :math:`(\epsilon~\instr_3^\ast)`. 9. Else: - a. Let :math:`H'^?` be the empty handler clause :math:`\epsilon`. + a. Let :math:`H'^?` be the empty handler :math:`\epsilon`. -10. Let :math:`H^\ast` be the :ref:`catching exception handler ` containing the concatenation of the handler clauses :math:`H_i` and :math:`H'^?`. +10. Let :math:`H^\ast` be the concatenation of :math:`H_i` and :math:`H'^?`. -11. :ref:`Enter ` the block :math:`\val^m~\instr_1^\ast` with label :math:`L` and exception handler :math:`H`. +11. :ref:`Enter ` the block :math:`\val^m~\instr_1^\ast` with label :math:`L` and exception handler :math:`H^\ast`. .. math:: ~\\[-1ex] \begin{array}{l} F; \val^m~(\TRY~\X{bt}~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END \quad \stepto \\ - \qquad F; \LABEL_n\{\epsilon\}~(\CATCHadm\{a_x~\instr_2^\ast\}^\ast\{\epsilon~\instr_3\ast\}^?~\val^m~\instr_1^\ast~\END)~\END \\ + \qquad F; \LABEL_n\{\epsilon\}~(\HANDLERadm_n\{(a_x~\instr_2^\ast)^\ast~(\epsilon~\instr_3^\ast)^?\}~\val^m~\instr_1^\ast~\END)~\END \\ (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n] \land (F.\AMODULE.\MITAGS[x]=a_x)^\ast) \end{array} @@ -2678,21 +2678,19 @@ Control Instructions 3. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the |TRY| instruction. -4. Let :math:`H` be the :ref:`delegating exception handler ` :math:`\DELEGATEadm\{l\}`, targeting the :math:`l`-th surrounding block. +4. Let :math:`H` be the :ref:`exception handler ` :math:`l`, targeting the :math:`l`-th surrounding block. 5. Assert: due to :ref:`validation `, there are at least :math:`m` values on the top of the stack. 6. Pop the values :math:`\val^m` from the stack. -7. :ref:`Enter ` the block :math:`H~(\val^n~\instr^\ast)~\END` with label :math:`L`. - -8. :ref:`Install ` the exception handler `H` containing :math:`\val^m~\instr^\ast`. +7. :ref:`Enter ` the block :math:`\val^m~\instr^\ast` with label :math:`L` and exception handler `H`. .. math:: ~\\[-1ex] \begin{array}{lcl} F; \val^m~(\TRY~\X{bt}~\instr^\ast~\DELEGATE~l) &\stepto& - F; \LABEL_n\{\epsilon\}~(\DELEGATEadm\{l\}~\val^m~\instr^\ast~\END)~\END \\ + F; \LABEL_n\{\epsilon\}~(\HANDLERadm_n\{l\}~\val^m~\instr^\ast~\END)~\END \\ && (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \end{array} @@ -2728,8 +2726,8 @@ Control Instructions .. math:: ~\\[-1ex] \begin{array}{lclr@{\qquad}} - \CAUGHTadm\{a~\val^n\}~\XB^l[\RETHROW~l]~\END &\stepto& - \CAUGHTadm\{a~\val^n\}~\XB^l[\val^n~(\THROWadm~a)]~\END \\ + \CAUGHTadm_n\{a~\val^n\}~\XB^l[\RETHROW~l]~\END &\stepto& + \CAUGHTadm_n\{a~\val^n\}~\XB^l[\val^n~(\THROWadm~a)]~\END \\ \end{array} @@ -3053,8 +3051,7 @@ When the end of a :ref:`try ` instruction is reached without a jump, .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \CATCHadm\{a^?~\instr^\ast\}^\ast~\val^m~\END &\stepto& \val^m \\ - \DELEGATEadm\{l\}~\val^m~\END &\stepto& \val^m + \HANDLERadm_m\{\handler\}~\val^m~\END &\stepto& \val^m \\ \end{array} @@ -3067,7 +3064,7 @@ When a throw occurs, then values, labels, active catch clauses, and call frames are popped if necessary, until an appropriate exception handler is found on the top of the stack. - 1. Assert: due to :ref:`validation `,, :math:`S.\STAGS[a]` exists. + 1. Assert: due to :ref:`validation `, :math:`S.\STAGS[a]` exists. 2. Let :math:`[t^n] \to []` be the :ref:`tag type ` :math:`S.\STAGS[a].\TAGITYPE`. @@ -3079,126 +3076,112 @@ on the top of the stack. a. Pop the top element from the stack. - 6. Assert: The stack is now either empty, or there is an exception handler on the top of the stack. + 6. Assert: the stack is now either empty, or there is an exception handler on the top of the stack. 7. If the stack is empty, then: - a. Return the uncaught exception :math:`\val^n~(\THROWadm~a)` as a result. - -8. Else: + a. Return the uncaught exception :math:`\val^n~(\THROWadm~a)` as a :ref:`result `. - a. Assert: there is an :ref:`exception handler ` :math:`H` on the top of the stack. +8. Else assert: there is an :ref:`exception handler ` :math:`H` on the top of the stack. 9. Pop the exception handler :math:`H` from the stack. -10. Assert: :math:`H` is either of the a catching or a delegating :ref:`exception handler `. - -11. If :math:`H` is a catching exception handler, let :math:`\{a^?~\instr^\ast\}^k` be its clauses. Then: - - a. If :math:`k = 0`, then: - - i. Put the values :math:`\val^n` back onto the stack. - - ii. :ref:`Throw ` an exception with tag address :math:`a`. - - b. Else :math:`H`'s clauses are of the form :math:`\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast`. +10. If :math:`H` is list of handlers, then: - c. If :math:`a_1^? = \epsilon`, then: + a. While :math:`H` is not empty, do: - i. :ref:`Enter ` :math:`\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. + i. Let :math:`(a_1^?~\instr^\ast)` be the first handler in :math:`H`. - d. Else if :math:`a_1^? = a`, then: + ii. If :math:`a_1^? = \epsilon`, then: - i. :ref:`Enter ` :math:`\val^n~\instr^\ast` with catch clause holding the caught exception :math:`\{a~\val^n\}`. + * :ref:`Enter ` the block :math:`\instr^\ast` with caught exception :math:`a~\val^n`. - e. Else: + iii. Else if :math:`a_1^? = a`, then: - i. Let :math:`H'` be the catching exception handler with clauses :math:`\{a'^?~\instr'^\ast\}^\ast`. + * :ref:`Enter ` the block :math:`\val^n~\instr^\ast` with caught exception :math:`a~\val^n`. - ii. Repeat step 11 for :math:`H'`. + iv. Else, pop the first handler from :math:`H`. -12. Else: + b. Else, the exception was not caught by :math:`H`: - a. Assert: :math:`H` is a delegating exception handler. + i. Put the values :math:`\val^n` back onto the stack. -13. Let :math:`l` be the label index of :math:`H`. + ii. :ref:`Throw ` an exception with tag address :math:`a`. -14. Assert: due to :ref:`validation `, the stack contains at least :math:`l` labels. +11. Else :math:`H` is a label index :math:`l`. -15. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. + a. Assert: due to :ref:`validation `, the stack contains at least :math:`l` labels. -15. Repeat :math:`l` times: + b. Repeat :math:`l` times: - a. While the top of the stack is not a label, do: + i. While the top of the stack is not a label, do: - i. Pop the top element from the stack. + * Pop the top element from the stack. - b. Assert: due to :ref:`validation `, the top of the stack now is a label. + c. Assert: due to :ref:`validation `, the top of the stack now is a label. - c. Pop the label from the stack. + d. Pop the label from the stack. -16. Push the values :math:`\val^n` onto the stack. + e. Push the values :math:`\val^n` onto the stack. -17. :ref:`Throw ` an exception with tag address :math:`a`. + f. :ref:`Throw ` an exception with tag address :math:`a`. .. math:: \begin{array}{rcl} - \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 \\ + \HANDLERadm_n\{\}~\XT[(\THROWadm~a)]~\END &\stepto& + \XT[(\THROWadm~a)] \\ + \HANDLERadm_n\{(a_1^?~\instr^\ast)~(a'^?~\instr'^\ast)^\ast\}~\XT[(\THROWadm~a)]~\END &\stepto& + \HANDLERadm_n\{(a'^?~\instr'^\ast)^\ast~\XT[(\THROWadm~a)]~\END \\ && (\iff a_1^? \neq \epsilon \land a_1^? \neq a) \\ - S;~\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& - S;~\CAUGHTadm\{a~\val^n\}~(\val^n)^?~\instr^\ast~\END \\ + S;~\HANDLERadm_n\{(a_1^?~\instr^\ast)~(a'^?~\instr'^\ast)^\ast\}~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& + S;~\CAUGHTadm_n\{a~\val^n\}~(\val^n)^?~\instr^\ast~\END \\ && (\iff~(a_1^? = \epsilon \lor a_1^? = a)~\land\\ && \ S.\STAGS[a].\TAGITYPE = [t^n]\to[]) \\ - \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[\val^n~(\THROWadm~a)]~\END]~\END &\stepto& - \XT[\val^n~(\THROWadm~a)] \\ + \LABEL_n\{\}~\XB^l[\HANDLERadm_n\{l\}~\XT[(\THROWadm~a)]~\END]~\END &\stepto& + \XT[(\THROWadm~a)] \\ \end{array} .. note:: - The reduction step entering a catch clause |CAUGHTadm| is the only one that does not preserve the throw context. - -.. todo:: - Explain why or what's the meaning of apparently preserving the throw context in the other rules. + The rules are formulated in this way to allow looking up the exception values in the throw context, + only when a thrown exception is caught. .. _exec-caughtadm-enter: -Entering :math:`\instr^\ast` with catch clause holding a caught exception :math:`\{a~\val^n\}` -.............................................................................................. +Entering :math:`\instr^\ast` with caught exception :math:`\{\exn\}` +................................................................... -1. Push :math:`\CAUGHTadm\{a~\val^n\}` onto the stack. +1. Push the caught exception |exn| onto the stack. 2. Jump to the start of the instruction sequence :math:`\instr^\ast`. -.. _exec-caughtadm: +.. _exec-caughtadm-exit: -Exiting a catch clause -...................... +Exiting a block with a caught exception +....................................... -When the |END| of a catch clause is reached without a jump, exception, or trap, then the following steps are performed. +When the |END| of a block with a caught exception is reached without a jump, thrown exception, or trap, then the following steps are performed. -1. Let :math:`\val^\ast` be the values on the top of the stack. +1. Let :math:`\val^m` be the values on the top of the stack. -2. Pop the values :math:`\val^\ast` from the stack. +2. Pop the values :math:`\val^m` from the stack. -3. Assert: due to :ref:`validation `, a caught exception :math:`\{a~\val_0^\ast\}` is now on the top of the stack. +3. Assert: due to :ref:`validation `, a caught exception is now on the top of the stack. 4. Pop the caught exception from the stack. -5. Push :math:`\val^\ast` back to the stack. +5. Push :math:`\val^m` back to the stack. -6. Jump to the position after the |END| of the administrative instruction associated with the catch clause. +6. Jump to the position after the |END| of the administrative instruction associated with the caught exception. .. math:: \begin{array}{rcl} - \CAUGHTadm\{a~\val_0^\ast\}~\val^\ast~\END &\stepto& \val^\ast + \CAUGHTadm_n\{\exn\}~\val^m~\END &\stepto& \val^m \end{array} .. note:: - An exception can only be rethrown from the scope of the |CAUGHTadm| administrative instruction holding it, i.e., from the scope of the |CATCH| or |CATCHALL| block of a :ref:`try-catch ` instruction that caught it. Upon exit from a |CAUGHTadm|, the exception it holds is discarded. + A caught exception can only be rethrown from the scope of the administrative instruction associated with it, i.e., from the scope of the |CATCH| or |CATCHALL| block of a :ref:`try-catch ` instruction that caught it. Upon exit from that block, the caught exception is discarded. .. index:: ! call, function, function instance, label, frame diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 14e56208..a5d6eb10 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -74,14 +74,14 @@ Results ~~~~~~~ A *result* is the outcome of a computation. -It is either a sequence of :ref:`values `, a :ref:`trap `, or an uncaught exception wrapped in its :ref:`throw context `. +It is either a sequence of :ref:`values `, a :ref:`trap `, or an :ref:`uncaught exception `. .. math:: \begin{array}{llcl} \production{(result)} & \result &::=& \val^\ast \\&&|& \TRAP \\&&|& - \XT[\val^\ast~(\THROWadm~\tagaddr)] + \val^\ast~(\THROWadm~\tagaddr) \end{array} .. note:: @@ -448,7 +448,7 @@ It filters out entries of a specific kind in an order-preserving fashion: -.. index:: ! stack, ! frame, ! label, ! handler, instruction, store, activation, function, call, local, module instance, exception handler +.. index:: ! stack, ! frame, ! label, ! handler, instruction, store, activation, function, call, local, module instance, exception handler, exception pair: abstract syntax; frame pair: abstract syntax; label pair: abstract syntax; handler @@ -457,6 +457,7 @@ It filters out entries of a specific kind in an order-preserving fashion: .. _frame: .. _label: .. _handler: +.. _exn: .. _stack: Stack @@ -473,6 +474,8 @@ The stack contains three kinds of entries: * *Handlers*: active exception handlers. +* *Exceptions*: caught exceptions. + These entries can occur on the stack in any order during the execution of a program. Stack entries are described by abstract syntax as follows. @@ -531,30 +534,35 @@ and a reference to the function's own :ref:`module instance ` The values of the locals are mutated by respective :ref:`variable instructions `. .. _syntax-handler: +.. _syntax-exn: -Exception handlers -.................. - -Exception handlers are installed by |TRY| instructions and are either *catching handlers* or *delegating handlers*. +Exception handlers and exceptions +................................. -Catching handlers start with the identifier |CATCHadm| and contain catch clauses, which are mappings from :ref:`tag addresses ` -to their associated branch *targets*. Each catch clause is expressed syntactically as a possibly empty sequence of +Exception handlers are installed by |TRY| instructions and are either a list of handlers or a label index. +A list of handlers is a mapping from :ref:`tag addresses ` +to their associated branch *targets*. A single handler is expressed syntactically as a possibly empty sequence of :ref:`instructions ` possibly following a :ref:`tag address `. -If there is no :ref:`tag address `, the instructions of that handler clause correspond to a |CATCHALL| clause. +If there is no :ref:`tag address `, the instructions of that handler correspond to a |CATCHALL| clause. .. todo:: Add prose for delegating handlers. +An exception may be temporarily pushed onto the stack when it is :ref:`thrown and caught ` by a handler. + .. math:: \begin{array}{llllll} - \production{(handler)} & \handler &::=& \CATCHadm\{\tagaddr^?~\instr^\ast\}^\ast &|& \DELEGATEadm\{l\} + \production{(handler)} & \handler &::=& (\tagaddr^?~\instr^\ast)^\ast &|& \labelidx\\ + \production{(exception)} & \exn &::=& \tagaddr~\val^\ast && \end{array} -Intuitively, for each catch clause :math:`\{\tagaddr^?~\instr^\ast\}` of a catching handler, :math:`\instr^\ast` is the *continuation* to execute -when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when the catch clause specifies no tag address. -In that case, the exception is handled, and that catch clause :ref:`entered `. -If this list of targets is empty, or if the tag address of the thrown exception is not in any of the catch clauses and there is no |CATCHALL| clause, then the exception will be rethrown. +Intuitively, for each individual handler :math:`(\tagaddr^?~\instr^\ast)`, the instruction block :math:`\instr^\ast` is the *continuation* to execute +when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when that handler specifies no tag address. +If the list of handlers is empty, or if the tag address of the thrown exception is not in any of the handlers in the list, and there is no |CATCHALL| clause, then the exception will be rethrown. + +When a thrown exception is caught by a handler, the caught exception is pushed onto the stack and the block of that handler's target is :ref:`entered `. +When exiting a block with a caught exception, the exception is discarded. .. todo:: @@ -581,14 +589,13 @@ Conventions \end{array} -.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment, tag, tag instance, tag address, exceptions, reftype, catch, delegate, handler, caught +.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment, tag, tag instance, tag address, exception, reftype, handler, caught, caught exception pair:: abstract syntax; administrative instruction .. _syntax-trap: .. _syntax-reffuncaddr: .. _syntax-invoke: .. _syntax-throwadm: -.. _syntax-catchadm: -.. _syntax-delegateadm: +.. _syntax-handleradm: .. _syntax-caughtadm: .. _syntax-instr-admin: @@ -610,9 +617,8 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `. It unifies the different forms of throwing exceptions. -The |LABEL|, |FRAME|, |CATCHadm|, |DELEGATEadm|, and |CAUGHTadm| instructions model :ref:`labels `, :ref:`frames `, active :ref:`catching exception handlers `, active :ref:`delegating exception handlers `, and :ref:`caught exceptions `, respectively, :ref:`"on the stack" `. +The |LABEL|, |FRAME|, |HANDLERadm|, and |CAUGHTadm| instructions model :ref:`labels `, :ref:`frames `, active :ref:`exception handlers `, and :ref:`caught exceptions `, respectively, :ref:`"on the stack" `. Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction ` or :ref:`function body ` and their :ref:`instruction sequences ` with an |END| marker. That way, the end of the inner instruction sequence is known when part of an outer sequence. @@ -683,8 +689,8 @@ In order to be able to break jumping over exception handlers and caught exceptio .. math:: \begin{array}{llll} - \production{(control contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\ - & & | & \CAUGHTadm~\{\tagaddr~\val^\ast\}~\XB^k~\END \\ + \production{(control contexts)} & \XC^{k} &::=& \HANDLERadm_n\{\handler\}~\XB^k~\END \\ + & & | & \CAUGHTadm_n~\{\exn\}~\XB^k~\END \\ \production{(block contexts)} & \XB^0 &::=& \dots ~|~ \val^\ast~\XC^0~\instr^\ast\\ \production{(block contexts)} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\ \end{array} @@ -708,7 +714,7 @@ Throw Contexts .............. In order to specify the reduction of |TRY| blocks -with the help of the administrative instructions |THROWadm|, |CATCHadm|, |DELEGATEadm|, and |CAUGHTadm|, +with the help of the administrative instructions |THROWadm|, |HANDLERadm|, and |CAUGHTadm|, the following syntax of *throw contexts* is defined, as well as associated structural rules: .. math:: @@ -717,18 +723,16 @@ the following syntax of *throw contexts* is defined, as well as associated struc [\_] \\ &&|& \val^\ast~\XT~\instr^\ast \\ &&|& \LABEL_n\{\instr^\ast\}~\XT~\END \\ &&|& - \CAUGHTadm\{\tagaddr~\val^\ast\}~\XT~\END \\ &&|& + \CAUGHTadm_n\{\exn\}~\XT~\END \\ &&|& \FRAME_n\{F\}~\XT~\END \\ \end{array} -Throw contexts allow matching the program context around a throw instruction up to the innermost enclosing |CATCHadm| or |DELEGATEadm|, thereby selecting the exception |handler| responsible for an exception, if one exists. -If no exception :ref:`handler that catches the exception ` is found, the computation :ref:`results ` in an uncaught exception result value, which contains the exception's entire throw context. +Throw contexts allow matching the program context around a throw instruction up to the innermost enclosing |HANDLERadm|, thereby selecting the exception |handler| responsible for an exception, if one exists. +If no exception :ref:`handler that catches the exception ` is found, the computation :ref:`results ` in an uncaught exception result value. .. note:: Contrary to block contexts, throw contexts don't skip over handlers. - Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. - |CAUGHTadm| blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block. .. note:: @@ -741,24 +745,24 @@ If no exception :ref:`handler that catches the exception ` is fo .. math:: \begin{array}{ll} & \hspace{-5ex} F;~\val_{i32}~\val_{f32}~\val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ - \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon\}~\val_{i32}~\val_{f32}~\val_{i64}~(\THROW~x)~\END)~\END \\ + \stepto & F;~\LABEL_2\{\} (\HANDLERadm_2\{(a~\epsilon)\}~\val_{i32}~\val_{f32}~\val_{i64}~(\THROW~x)~\END)~\END \\ \end{array} :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context - :math:`T=[\val_{i32}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\epsilon\}` gives: + :math:`T=[\val_{i32}\_]`, with the exception handler :math:`H=(a~\epsilon)` gives: .. math:: \begin{array}{lll} - \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~\val_{f32}~\val_{i64}\}~\val_{f32}~\val_{i64}~\END)~\END & \hspace{9ex}\ \\ + \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm_2\{a~\val_{f32}~\val_{i64}\}~\val_{f32}~\val_{i64}~\END)~\END & \hspace{9ex}\ \\ \stepto & F;~\LABEL_2\{\}~\val_{f32}~\val_{i64}~\END & \hspace{9ex}\ \\ \stepto & \val_{f32}~\val_{i64} & \\ \end{array} - When a throw of the form :math:`\val^m (\THROWadm~a)` occurs, search for the maximal surrounding throw context :math:`T` is performed, - which means any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`\val^m (\THROWadm~a)` are popped, - until a :ref:`handler ` for the exception is found. - Then a new |CAUGHTadm| instruction, containing the tag address :math:`a` and the values :math:`\val^m`, is pushed onto the stack. + When a throw of the form :math:`\val^m (\THROWadm~a)` occurs, search for an enclosing exception handler is performed, + which means any throw context (that is any other values, labels, frames, and |CAUGHTadm| instructions) surrounding the throw :math:`\val^m (\THROWadm~a)` is popped, + until a :ref:`handler ` for the exception tag :math:`a` is found. + Then the :ref:`caught exception ` containing the tag address :math:`a` and the values :math:`\val^m`, is pushed onto the stack. In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1fc2991f..e78d430f 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1090,6 +1090,7 @@ .. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}} .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}} .. |handler| mathdef:: \xref{exec/runtime}{syntax-handler}{\X{handler}} +.. |exn| mathdef:: \xref{exec/runtime}{syntax-exn}{\X{exn}} .. Stack, meta functions @@ -1103,8 +1104,7 @@ .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} .. |THROWadm| mathdef:: \xref{exec/runtime}{syntax-throwadm}{\K{throw}} -.. |CATCHadm| mathdef:: \xref{exec/runtime}{syntax-catchadm}{\K{catch}} -.. |DELEGATEadm| mathdef:: \xref{exec/runtime}{syntax-delegateadm}{\K{delegate}} +.. |HANDLERadm| mathdef:: \xref{exec/runtime}{syntax-handleradm}{\K{handler}} .. |CAUGHTadm| mathdef:: \xref{exec/runtime}{syntax-caughtadm}{\K{caught}} diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index c5d349cf..d7e1ed51 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -110,12 +110,18 @@ taginst ::= {'type' tagtype} ``` m ::= {..., 'tags' tagaddr*} ``` +#### Stack + +``` +handler ::= (tagaddr? instr*)* | labelidx +exn ::= tagaddr val* +``` #### Administrative Instructions ``` -instr ::= ... | 'throw' tagaddr | 'catch'{ tagaddr? instr* }* instr* 'end' - | 'delegate'{ labelidx } instr* 'end' | 'caught'{ tagaddr val* } instr* 'end' +instr ::= ... | 'throw' tagaddr | 'handler'_n{handler} instr* 'end' + | 'handler'_n{ labelidx } instr* 'end' | 'caught'_n{exn} instr* 'end' ``` #### Block Contexts and Label Kinds @@ -125,73 +131,72 @@ So far block contexts are only used in the reduction of `br l` and `return`, and ``` B^0 ::= val* '[_]' instr* | val* C^0 instr* B^{k+1} ::= val* ('label'_n{instr*} B^k 'end') instr* | val* C^{k+1} instr* -C^k ::= 'catch'{ tagaddr? instr* }* B^k 'end' - | 'caught'{ tagaddr val* } B^k 'end' - | 'delegate'{ labelidx } B^k 'end' +C^k ::= 'handler'_n{ handler } B^k 'end' + | 'caught'_n{ exn } B^k 'end' ``` Note the `C` in `C^k` above stands for `control`, because the related administrative instructions are in some ways modeling [control frame opcodes](https://webassembly.github.io/spec/core/appendix/algorithm.html?highlight=control#data-structures) "on the stack". #### Throw Contexts -Throw contexts don't skip over handlers (administrative `catch` or `delegate` instructions). +Throw contexts don't skip over handlers. Throw contexts are used to match a thrown exception with the innermost handler. ``` T ::= '[_]' | val* T instr* | 'label'_n{instr*} T 'end' - | 'caught'{ tagaddr val* } T 'end' + | 'caught'_n{exn} T 'end' | 'frame'_n{F} T 'end' ``` -Note that because `catch` and `delegate` instructions are not included above, there is always a unique maximal throw context to match the reduction rules. Note that this basically means that `caught{..} instr* end` is not a potential catching block for exceptions thrown by `instr*`. The instruction sequence `instr*` is inside a `catch` or `catch_all` block. +Note that because handlers are not included above, popping the throw context stops when the innermost handler is found, if any. Note that this also means that `caught_n{exn} instr* end` is not a potential catching block for exceptions thrown by `instr*`. The instruction sequence `instr*` is inside a `catch` or `catch_all` block. ### Reduction of Instructions Reduction steps for the new instructions or administrative instructions. -An absent tag address in a `catch` administrative instruction (i.e., `a? = ε`) represents a `catch_all`. +An absent tag address in a handler (i.e., `a? = ε`) represents a `catch_all`. ``` F; throw x ↪ F; throw a (if F.module.tagaddrs[x]=a) -caught{a val*} B^l[rethrow l] end - ↪ caught{a val*} B^l[val* (throw a)] end +caught_n{a val*} B^l[rethrow l] end + ↪ caught_n{a val*} B^l[val* (throw a)] end -caught{a val0*} val* end ↪ val* +caught_n{a val0*} val^n end ↪ val^n F; val^n (try bt instr1* (catch x instr2*)* (catch_all instr3*)? end) - ↪ F; label_m{} (catch{a instr2*}*{ε instr3*}? val^n instr1* end) end + ↪ F; label_m{} (handler_m{(a instr2*)*(ε instr3*)?} val^n instr1* end) end (if expand_F(bt) = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) -catch{a? instr*}* val* end ↪ val* +handler_m{(a? instr*)*} val^m end ↪ val^m -S; F; catch{a1? instr1*}{a0? instr0*}* T[val^n (throw a)] end - ↪ S; F; caught{a val^n} (val^n)? instr1* end +S; F; handler_m{(a1? instr1*)(a0? instr0*)*} T[val^n (throw a)] end + ↪ S; F; caught_m{a val^n} (val^n)? instr1* end (if (a1? = ε ∨ a1? = a) ∧ S.tags(a).type = [t^n]→[]) -catch{a1? instr*}{a0? instr0*}* T[val^n (throw a)] end - ↪ catch{a0? instr0*}* T[val^n (throw a)] end +handler_m{(a1? instr*)(a0? instr0*)*} T[(throw a)] end + ↪ handler_m{(a0? instr0*)*} T[(throw a)] end (if a1? ≠ ε ∧ a1? ≠ a) -catch T[val^n (throw a)] end ↪ val^n (throw a) +handler_m{} T[(throw a)] end ↪ T[(throw a)] (if S.tags(a).type = [t^n]→[]) F; val^n (try bt instr* delegate l) - ↪ F; label_m{} (delegate{l} val^n instr* end) end + ↪ F; label_m{} (handler_m{l} val^n instr* end) end (if expand_F(bt) = [t1^n]→[t2^m]) -delegate{l} val* end ↪ val* +handler_m{l} val^m end ↪ val^m -label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end - ↪ val^n (throw a) +label_m{} B^l[ handler_m{l} T[(throw a)] end ] end + ↪ T[(throw a)] ``` -Note that the last reduction step above is similar to the reduction of `br l` [1], the entire `delegate{l}...end` is seen as a `br l` immediately followed by a throw. +Note that the last reduction step above is similar to the reduction of `br l` [1], the entire `handler_m{l}...end` is seen as a `br l` immediately followed by a throw. -There is a subtle difference though. The instruction `br l` searches for the `l+1`th surrounding block and breaks out after that block. Because `delegate{l}` is always wrapped in its own `label_n{} ... end` [2], with the same lookup as for `br l` the instruction ends up breaking inside the `l+1`th surrounding block, and throwing there. So if that `l+1`th surrounding block is a try, the exception is thrown in the "try code", and thus correctly getting delegated to that try's catches. +There is a subtle difference though. The instruction `br l` searches for the `l+1`th surrounding block and breaks out after that block. Because `handler_m{l}` is always wrapped in its own `label_m{} ... end` [2], with the same lookup as for `br l` the instruction ends up breaking inside the `l+1`th surrounding block, and throwing there. So if that `l+1`th surrounding block is a try, the exception is thrown in the "try code", and thus correctly getting delegated to that try's catches. - [1] [The execution step for `br l`](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-l) - [2] The label that always wraps `delegate{l}...end` can be thought of as "level -1" and cannot be referred to by the delegate's label index `l`. @@ -205,21 +210,21 @@ S ⊢ tag a : tag [t*]→[] S;C ⊢ throw a : [t1* t*]→[t2*] ((S ⊢ tag a : tag [t1*]→[])? - S;C, labels (catch [t2*]) ⊢ instr2* : [t1*?]→[t2*])* -S;C, labels [t2*] ⊢ instr1* : []→[t2*] + S;C, labels (catch [t2^m]) ⊢ instr2* : [t1*?]→[t2^m])* +S;C, labels [t2^m] ⊢ instr1* : []→[t2^m] ----------------------------------------------------------- -S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*] +S;C, labels [t2^m] ⊢ handler_m{(a? instr2*)*} instr1* end : []→[t2^m] -S;C ⊢ instr* : []→[t*] +S;C ⊢ instr* : []→[t^m] C.labels[l+1] = [t0*] ------------------------------------------------------ -S;C ⊢ delegate{l} instr* end : []→[t*] +S;C ⊢ handler_m{l} instr* end : []→[t^m] S ⊢ tag a : tag [t0*]→[] (val:t0)* -S;C, labels (catch [t*]) ⊢ instr* : []→[t*] ----------------------------------------------------------- -S;C, labels [t*] ⊢ caught{a val^*} instr* end : []→[t*] +S;C, labels (catch [t^n]) ⊢ instr* : []→[t^n] +------------------------------------------------------------ +S;C, labels [t^n] ⊢ caught_n{a val^*} instr* end : []→[t^n] ``` ## Uncaught Exceptions @@ -228,6 +233,6 @@ A new [result](https://webassembly.github.io/spec/core/exec/runtime.html#syntax- ``` result ::= val* | trap - | T[val* (throw tagaddr)] + | val* (throw tagaddr) ``` From 99a72e24ba5bcb420714f6a9da77df070fc5b35f Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 15 Feb 2023 18:48:41 +0100 Subject: [PATCH 10/14] Added the missing prose here after all as it doesn't make sense on its own in #246. --- document/core/exec/runtime.rst | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index b425228b..f899bcc3 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -543,11 +543,11 @@ to their associated branch *targets*. A single handler is expressed syntacticall :ref:`instructions ` possibly following a :ref:`tag address `. If there is no :ref:`tag address `, the instructions of that handler correspond to a |CATCHALL| clause. -.. todo:: - Add prose for delegating handlers. - An exception may be temporarily pushed onto the stack when it is :ref:`thrown and caught ` by a handler. +A |labelidx| handler points to the outer block in which any exceptions thrown from its scope, will be rethrown (delegated to). +This handler does not catch exceptions, but only rethrows them. + .. math:: \begin{array}{llllll} \production{(handler)} & \handler &::=& (\tagaddr^?~\instr^\ast)^\ast &|& \labelidx\\ @@ -561,9 +561,7 @@ If the list of handlers is empty, or if the tag address of the thrown exception When a thrown exception is caught by a handler, the caught exception is pushed onto the stack and the block of that handler's target is :ref:`entered `. When exiting a block with a caught exception, the exception is discarded. - -.. todo:: - Add prose with intuition on delegating handlers. +A handler pointing to a |labelidx| :math:`l` can be thought of as a break to the :math:`l` th label on exception, followed by a rethrow of the exception. .. _exec-expand: From 8c66cbec973955bebc705edbdb13bb2fec845f59 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 17 Feb 2023 18:21:27 +0100 Subject: [PATCH 11/14] Fix the "formal examples" to use the updated administrative instructions. --- .../Exceptions-formal-examples.md | 92 +++++++++---------- 1 file changed, 46 insertions(+), 46 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 10571d85..5beb6d9a 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -63,11 +63,11 @@ Take the frame `F = (locals i32.const 0, module m)`. We have: ``` ↪ ↪ ↪ ↪ F; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (label_0{} - (catch{ ε (local.set 0 (i32.const 27)) (rethrow 0) } + (handler_0{ (ε (local.set 0 (i32.const 27)) (rethrow 0)) } (throw a_x) end) end) end) end) end) end) ``` @@ -75,19 +75,19 @@ For the trivial throw context `T = [_]` the above is the same as ``` ↪ F; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (label_0{} - (catch{ ε (local.set 0 (i32.const 27)) (rethrow 0) } + (handler_0{ (ε (local.set 0 (i32.const 27)) (rethrow 0)) } T[(throw a_x)]) end) end) end) end) end) ↪ F; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } (local.set 0 (i32.const 27)) (rethrow 0) end) end) end) end) end) end) ``` @@ -96,48 +96,48 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]` to ``` ↪ F'; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } B^0[ (rethrow 0) ] end) end) end) end) end) end) ↪ F'; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } (throw a_x) end) end) end) end) end) end) ``` -Let `T' = (label_0{} (caught{ a_x ε } [_] end) end)` and use the same `B^0` as above to reduce the throw with the delegate. +Let `T' = (label_0{} (caught_0{ a_x ε } [_] end) end)` and use the same `B^0` as above to reduce the throw with the delegate. ``` ↪ F'; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (label_0{} - B^0[ (delegate{ 0 } T'[ (throw a_x) ] end) ] end) end) end) + B^0[ (handler_0{ 0 } T'[ (throw a_x) ] end) ] end) end) end) ↪ F'; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } (throw a_x) end) end) ``` -Use the trivial throw context `T` again, this time to match the throw to the `catch`. +Use the trivial throw context `T` again, this time to match the throw to the `handler_1{(...)}`. ``` ↪ F'; (label_1{} - (catch{ a_x (local.get 0) } + (handler_1{ (a_x (local.get 0)) } T[ (throw a_x) ] end) end) ↪ F'; (label_1{} - (caught{ a_x ε } + (caught_0{ a_x ε } (local.get 0) end) end) ↪ F'; (label_1{} - (caught{ a_x ε } + (caught_0{ a_x ε } (i32.const 27) end) end) ↪ F'; (label_1{} @@ -196,13 +196,13 @@ In the above example, all thrown exceptions get caught and the first one gets re ``` (label_0{} - (caught{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below. + (caught_0{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below. val_x (label_0{} - (caught{ a_y val_y } + (caught_0{ a_y val_y } ;; The catch_all does not leave val_y here. (label_0{} - (caught{ a_z val_z } + (caught_0{ a_z val_z } val_z ;; (rethrow 2) puts val_x and the throw below. val_x @@ -266,40 +266,40 @@ In folded form and reduced to the point `throw $x` is called, this is: ``` (label_0{} - (catch{ a_x instr* } + (handler_0{ (a_x instr*) } (label_0{} - (catch{ ε ε } + (handler_0{ (ε ε) } (label_0{} - (delegate{ 1 } + (handler_0{ 1 } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (throw a_x) end) end) end) end) end) end) end) end) ``` -The `delegate{ 0 }` reduces using the trivial throw and block contexts to: +The `handler_0{ 0 }` reduces using the trivial throw and block contexts to: ``` (label_0{} - (catch{ a_x instr* } + (handler_0{ (a_x instr*) } (label_0{} - (catch{ ε ε } + (handler_0{ (ε ε) } (label_0{} - (delegate{ 1 } + (handler_0{ 1 } (throw a_x) end) end) end) end) end) end) ``` -The `delegate{ 1 }` reduces using the trivial throw context and the block context `B^1 := (catch{ ε ε } (label_0{} [_] end) end)` to the following: +The `handler_0{ 1 }` reduces using the trivial throw context and the block context `B^1 := (handler_0{ (ε ε) } (label_0{} [_] end) end)` to the following: ``` (label_0{} - (catch{ a_x instr* } + (handler_0{ (a_x instr*) } (throw a_x) end) end) ``` The thrown exception is (eventually) caught by the outer try's `catch $x`, so the above reduces to the following. ``` (label_0 {} - (caught{a_x} + (caught_0{a_x} instr* end) end) ``` @@ -342,11 +342,11 @@ When it's time to reduce `(throw y)`, the reduction looks as follows. ``` (label_1{} - (catch{ ε (i32.const 4) } + (handler_1{ (ε (i32.const 4)) } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } (label_0{} - (delegate{ 0 } + (handler_0{ 0 } (throw a_y) end) end) end) end) end) end) ``` @@ -354,17 +354,17 @@ For `B^0 := [_] := T`, the above is the same as the following. ``` (label_1{} - (catch{ ε (i32.const 4) } + (handler_1{ (ε (i32.const 4)) } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } (label_0{} - B^0 [(delegate{ 0 } T[ (throw a_y) ] end)] end) end) end) end) end) + B^0 [(handler_0{ 0 } T[ (throw a_y) ] end)] end) end) end) end) end) ↪ (label_1{} - (catch{ ε (i32.const 4) } + (handler_1{ (ε (i32.const 4)) } (label_0{} - (caught{ a_x ε } + (caught_0{ a_x ε } (throw a_y) end) end) end) end) ``` -So `throw a_y` gets correctly caught by `catch{ ε (i32.const 4) }` and this example reduces to `(i32.const 4)`. +So `throw a_y` gets correctly caught by `handler_1{ (ε (i32.const 4)) }` and this example reduces to `(i32.const 4)`. From 544fb7dabcbd0d4767bae72f727e847adbf4945a Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 22 Feb 2023 22:20:41 +0100 Subject: [PATCH 12/14] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/exec/runtime.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index f899bcc3..a19c867a 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -545,7 +545,7 @@ If there is no :ref:`tag address `, the instructions of that han An exception may be temporarily pushed onto the stack when it is :ref:`thrown and caught ` by a handler. -A |labelidx| handler points to the outer block in which any exceptions thrown from its scope, will be rethrown (delegated to). +A handler can also consist of a single |labelidx|, which denotes an outer block to which every caught exception will be delegated, by implicitly rethrowing inside that block. This handler does not catch exceptions, but only rethrows them. .. math:: @@ -561,7 +561,7 @@ If the list of handlers is empty, or if the tag address of the thrown exception When a thrown exception is caught by a handler, the caught exception is pushed onto the stack and the block of that handler's target is :ref:`entered `. When exiting a block with a caught exception, the exception is discarded. -A handler pointing to a |labelidx| :math:`l` can be thought of as a break to the :math:`l` th label on exception, followed by a rethrow of the exception. +A handler consisting of a |labelidx| :math:`l` can be thought of as a branch to that label that happens in case an exception occurs, immediately followed by a rethrow of the exception at the target site. .. _exec-expand: From 701f52be55d7fa4e589599563802dd8da6d25597 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 22 Feb 2023 22:27:37 +0100 Subject: [PATCH 13/14] removed explicit parens from productions --- document/core/exec/runtime.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index a19c867a..8a9b0c9b 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -550,8 +550,8 @@ This handler does not catch exceptions, but only rethrows them. .. math:: \begin{array}{llllll} - \production{(handler)} & \handler &::=& (\tagaddr^?~\instr^\ast)^\ast &|& \labelidx\\ - \production{(exception)} & \exn &::=& \tagaddr~\val^\ast && + \production{handler} & \handler &::=& (\tagaddr^?~\instr^\ast)^\ast &|& \labelidx\\ + \production{exception} & \exn &::=& \tagaddr~\val^\ast && \end{array} Intuitively, for each individual handler :math:`(\tagaddr^?~\instr^\ast)`, the instruction block :math:`\instr^\ast` is the *continuation* to execute @@ -684,10 +684,10 @@ In order to be able to break jumping over exception handlers and caught exceptio .. math:: \begin{array}{llll} - \production{(control contexts)} & \XC^{k} &::=& \HANDLERadm_n\{\handler\}~\XB^k~\END \\ + \production{control contexts} & \XC^{k} &::=& \HANDLERadm_n\{\handler\}~\XB^k~\END \\ & & | & \CAUGHTadm_n~\{\exn\}~\XB^k~\END \\ - \production{(block contexts)} & \XB^0 &::=& \dots ~|~ \val^\ast~\XC^0~\instr^\ast\\ - \production{(block contexts)} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\ + \production{block contexts} & \XB^0 &::=& \dots ~|~ \val^\ast~\XC^0~\instr^\ast\\ + \production{block contexts} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\ \end{array} .. note:: From 87a41f8523d9589852ffd994a6ac4ea37a5f8772 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Thu, 23 Feb 2023 18:07:35 +0100 Subject: [PATCH 14/14] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/exec/runtime.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index c7b13b01..443ee150 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -75,14 +75,14 @@ Results ~~~~~~~ A *result* is the outcome of a computation. -It is either a sequence of :ref:`values `, a :ref:`trap `, or an :ref:`uncaught exception `. +It is either a sequence of :ref:`values `, a :ref:`trap `, or an :ref:`exception `. .. math:: \begin{array}{llcl} \production{result} & \result &::=& \val^\ast \\&&|& \TRAP \\&&|& - \val^\ast~(\THROWadm~\tagaddr) + \XT[(\THROWadm~\tagaddr)] \end{array} .. index:: ! store, function instance, table instance, memory instance, tag instance, global instance, module, allocation