diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 2c2c3eea..1f3c1dfa 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -612,64 +612,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 +.. 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] = \LCATCH^?~[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 42318361..b758903e 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2636,26 +2636,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} @@ -2671,21 +2671,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} @@ -2730,8 +2728,8 @@ Control Instructions .. math:: ~\\[-1ex] \begin{array}{lclr@{\qquad}} - \CAUGHTadm\{a~\val^\ast\}~\XB^l[\RETHROW~l]~\END &\stepto& - \CAUGHTadm\{a~\val^\ast\}~\XB^l[\val^\ast~(\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} @@ -3055,8 +3053,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} @@ -3065,53 +3062,128 @@ When the end of a :ref:`try ` instruction is reached without a jump, Throwing an exception with :ref:`tag address ` :math:`a` ........................................................................ -.. todo:: - Add prose for the following execution steps. +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. + + 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. + + 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 :ref:`result `. + +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. If :math:`H` is list of handlers, then: + + a. While :math:`H` is not empty, do: + + i. Let :math:`(a_1^?~\instr^\ast)` be the first handler in :math:`H`. + + ii. If :math:`a_1^? = \epsilon`, then: + + * :ref:`Enter ` the block :math:`\instr^\ast` with caught exception :math:`a~\val^n`. + + iii. Else if :math:`a_1^? = a`, then: + + * :ref:`Enter ` the block :math:`\val^n~\instr^\ast` with caught exception :math:`a~\val^n`. + + iv. Else, pop the first handler from :math:`H`. + + b. Else, the exception was not caught by :math:`H`: + i. Put the values :math:`\val^n` back onto the stack. + + ii. :ref:`Throw ` an exception with tag address :math:`a`. + +11. Else :math:`H` is a label index :math:`l`. + + a. Assert: due to :ref:`validation `, the stack contains at least :math:`l` labels. + + b. Repeat :math:`l` times: + + i. While the top of the stack is not a label, do: + + * Pop the top element from the stack. + + c. Assert: due to :ref:`validation `, the top of the stack now is a label. + + d. Pop the label from the stack. + + e. Push the values :math:`\val^n` onto the stack. + + f. :ref:`Throw ` an exception with tag address :math:`a`. .. 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 \\ + \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[(\THROWadm~a)]~\END]~\END &\stepto& + \LABEL_n\{\}~\XB^l[\HANDLERadm_n\{l\}~\XT[(\THROWadm~a)]~\END]~\END &\stepto& \XT[(\THROWadm~a)] \\ \end{array} +.. note:: + 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. -.. todo:: - Add explainer note. -.. _exec-caughtadm: +.. _exec-caughtadm-enter: -Exiting a catch clause -...................... +Entering :math:`\instr^\ast` with caught exception :math:`\{\exn\}` +................................................................... + +1. Push the caught exception |exn| onto the stack. + +2. Jump to the start of the instruction sequence :math:`\instr^\ast`. -When the |END| of a catch clause is reached without a jump, exception, or trap, then the following steps are performed. -1. Let :math:`\val^\ast` be the values on the top of the stack. +.. _exec-caughtadm-exit: -2. Pop the values :math:`\val^\ast` from the stack. +Exiting a block with a caught exception +....................................... -3. Assert: due to :ref:`validation `, a caught exception :math:`\{a~\val_0^\ast\}` is now on the top of the stack. +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^m` be the values on the top of the stack. + +2. Pop the values :math:`\val^m` from 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 81766713..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 uncaught exception wrapped in its :ref:`throw context `. +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 \\&&|& - \XT[\val^\ast~(\THROWadm~\tagaddr)] + \XT[(\THROWadm~\tagaddr)] \end{array} .. index:: ! store, function instance, table instance, memory instance, tag instance, global instance, module, allocation @@ -445,7 +445,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 @@ -454,6 +454,7 @@ It filters out entries of a specific kind in an order-preserving fashion: .. _frame: .. _label: .. _handler: +.. _exn: .. _stack: Stack @@ -470,6 +471,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. @@ -526,32 +529,37 @@ 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 and exceptions +................................. -Exception handlers are installed by |TRY| instructions and are either *catching handlers* or *delegating handlers*. +Exception handlers are installed by |TRY| instructions and are either a list of handlers or a label index. -Catching handlers start with the identifier |CATCHadm| and contain handler clauses, which are mappings from :ref:`tag addresses ` -to their associated branch *targets*, each of which is expressed syntactically as a possibly empty sequence of +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. + +An exception may be temporarily pushed onto the stack when it is :ref:`thrown and caught ` by a handler. -.. todo:: - Add prose for delegating handlers. +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:: \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 handler clause :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 handler clause specifies no tag address. -In that case, 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 any of the handler's 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. -.. todo:: - Add prose with intuition on delegating handlers. +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 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: @@ -574,14 +582,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: @@ -603,9 +610,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. @@ -676,8 +682,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} @@ -701,7 +707,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:: @@ -710,18 +716,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:: @@ -734,24 +738,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 b6ea4106..5a2ed12d 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1094,6 +1094,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 @@ -1107,8 +1108,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-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)`. 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) ```