Execution

Runtime Structure

Stack

Exception Handlers

Legacy exception handlers are installed by \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}\) instructions. Instead of branch labels, their catch clauses have instruction blocks associated with them. Furthermore, a \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}\) handler is associated with a label index to implicitly rewthrow to:

\[\begin{split}\begin{array}{llllll} \def\mathdef91#1{{}}\mathdef91{catch} & \href{../syntax/instructions.html#syntax-catch}{\mathit{catch}} &::=& \dots \\ &&|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~\href{../syntax/modules.html#syntax-tagidx}{\mathit{tagidx}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ &&|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/modules.html#syntax-tagidx}{\mathit{tagidx}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ &&|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~\href{../syntax/modules.html#syntax-labelidx}{\mathit{labelidx}} \\ \end{array}\end{split}\]

Administrative Instructions

Administrative instructions are extended with the \(\href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}\) instruction that models exceptions caught by legacy exception handlers.

\[\begin{split}\begin{array}{llcl} \def\mathdef91#1{{}}\mathdef91{administrative instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=& \dots \\ &&|& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{\href{../exec/runtime.html#syntax-exnaddr}{\mathit{exnaddr}}\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \end{array}\end{split}\]

Block Contexts

Block contexts are extended to include \(\href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}\) instructions:

\[\begin{split}\begin{array}{llll} \def\mathdef91#1{{}}\mathdef91{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^k &::=& \dots \\ &&|& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n~\{\href{../exec/runtime.html#syntax-exnaddr}{\mathit{exnaddr}}\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^k~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \end{array}\end{split}\]

Throw Contexts

Throw contexts are also extended to include \(\href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}\) instructions:

\[\begin{split}\begin{array}{llll} \def\mathdef91#1{{}}\mathdef91{throw contexts} & \href{../exec/runtime.html#syntax-ctxt-throw}{T} &::=& \dots \\ &&|& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{\href{../exec/runtime.html#syntax-exnaddr}{\mathit{exnaddr}}\}~\href{../exec/runtime.html#syntax-ctxt-throw}{T}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \end{array}\end{split}\]

Instructions

Control Instructions

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)

1. Assert: due to validation, \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\) is defined.

2. Let \([t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n]\) be the function type \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\).

3. Let \(L\) be the label whose arity is \(n\) and whose continuation is the end of the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}\) instruction.

4. Assert: due to validation, there are at least \(m\) values on the top of the stack.

5. Pop the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\) from the stack.

6. Let \(F\) be the current frame.

7. For each catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x_i~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_{2i}^\ast)\) do:

   1. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x_i]\) exists.

   2. Let \(a_i\) be the tag address \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x_i]\).

   3. Let \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_i\) be the catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~a_i~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_{2i}^\ast)\).

8. If there is a catch-all clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)\), then:

   1. Let \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}'^?\) be the handler \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)\).

9. Else:

   1. Let \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}'^?\) be empty.

10. Let \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\) be the concatenation of \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_i\) and \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}'^?\).

11. Enter the block \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) with label \(L\) and exception handler \(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}^\ast\).

\[\begin{split}~\\[-1ex] \begin{array}{l} F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad \href{../exec/conventions.html#formal-notation}{\hookrightarrow} \\ \qquad F; \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~a_x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \qquad (\mathrel{\mbox{if}} \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\mathit{bt}) = [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n] \land (F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x]=a_x)^\ast) \end{array}\end{split}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l\)

1. Assert: due to validation, \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\) is defined.

2. Let \([t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n]\) be the function type \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\).

3. Let \(L\) be the label whose arity is \(n\) and whose continuation is the end of the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}\) instruction.

4. Let \(H\) be the exception handler \(l\), targeting the \(l\)-th surrounding block.

5. Assert: due to validation, there are at least \(m\) values on the top of the stack.

6. Pop the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\) from the stack.

7. Enter the block \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) with label \(L\) and exception handler HANDLER_n{DELEGATE~l}.

\[\begin{split}~\\[-1ex] \begin{array}{lcl} F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l) &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& F; \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ && (\mathrel{\mbox{if}} \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\mathit{bt}) = [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n]) \end{array}\end{split}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\)

1. Let \(F\) be the current frame.

2. Assert: due to validation, a reference is on the top of the stack.

3. Pop the reference \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) from the stack.

4. If \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) is \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~\mathit{ht}\), then:

   1. Trap.

5. Assert: due to validation, \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) is an exception reference.

6. Let \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) be \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\).

7. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[\mathit{ea}]\) exists.

8. Let \(\mathit{exn}\) be the exception instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[\mathit{ea}]\).

9. Let \(a\) be the tag address \(\mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{tag}}\).

10. While the stack is not empty and the top of the stack is not an exception handler, do:

1. Pop the top element from the stack.

11. Assert: the stack is now either empty, or there is an exception handler on the top of the stack.

12. If the stack is empty, then:

1. Return the exception \((\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)\) as a result.

13. Assert: there is an exception handler on the top of the stack.

14. Pop the exception handler \(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}\) from the stack.

15. If \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\) is empty, then:

    1. Push the exception reference \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) back to the stack.

    2. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\) again.

16. Else:

    1. Let \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) be the first catch clause in \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\) and \({\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}'}^\ast\) the remaining clauses.

    2. If \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~l\) and the exception address \(a\) equals \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x]\), then:

       1. Push the values \(\mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}\) to the stack.

       2. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\).

    3. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_ref}}~x~l\) and the exception address \(a\) equals \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x]\), then:

       1. Push the values \(\mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}\) to the stack.

       2. Push the exception reference \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) to the stack.

       3. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\).

    4. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~l\), then:

       1. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\).

    5. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all\_ref}}~l\), then:

       1. Push the exception reference \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) to the stack.

       2. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\).

    6. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) and the exception address \(a\) equals \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x]\), then:

       1. Push the caught exception \(\href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{\mathit{ea}\}\) to the stack.

       2. Push the values \(\mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}\) to the stack.

       3. Enter the catch block \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\).

    7. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\), then:

       1. Push the caught exception \(\href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{\mathit{ea}\}\) to the stack.

       2. Enter the catch block \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\).

    8. Else if \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_1\) is of the form \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l\), then:

       1. Assert: due to validation, the stack contains at least \(l\) labels.

       2. Repeat \(l\) times:

          • While the top of the stack is not a label, do:

            • Pop the top element from the stack.

       3. Assert: due to validation, the top of the stack now is a label.

       4. Pop the label from the stack.

       5. Push the exception reference \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) back to the stack.

       6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\) again.

    9. Else:

       1. Push the modified handler \(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}'}^\ast\}\) back to the stack.

       2. Push the exception reference \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~\mathit{ea}\) back to the stack.

       3. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\) again.

\[\begin{split}~\\[-1ex] \begin{array}{rcl} \dots \\ \href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast)~\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-throw}{T}[(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{a\}~\mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ && (\begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{exn} = S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[a] \\ \land & \mathit{exn}.\href{../exec/runtime.html#syntax-exninst}{\mathsf{tag}} = F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tagaddrs}}[x]) \\ \end{array} \\ \href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast)~\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-throw}{T}[(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{a\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l)~\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-throw}{T}[(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}] &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& (\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}} \\ \end{array}\end{split}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}~l\)

1. Assert: due to validation, the stack contains at least \(l+1\) labels.

2. Let \(L\) be the \(l\)-th label appearing on the stack, starting from the top and counting from zero.

3. Assert: due to validation, \(L\) is a catch label, i.e., a label of the form \((\href{../valid/conventions.html#context}{\mathsf{catch}}~[t^\ast])\), which is a label followed by a caught exception in an active catch clause.

4. Let \(a\) be the caught exception address.

5. Push the value \(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a\) onto the stack.

6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\).

\[\begin{split}~\\[-1ex] \begin{array}{lclr@{\qquad}} \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{a\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}~l]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{a\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[(\href{../exec/runtime.html#syntax-ref.exn-addr}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \end{array}\end{split}\]

Entering a catch block

1. Jump to the start of the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\).

Exiting a catch block

When the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) of a catch block is reached without a jump, thrown exception, or trap, then the following steps are performed.

1. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\) be the values on the top of the stack.

2. Pop the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\) from the stack.

3. Assert: due to validation, a caught exception is now on the top of the stack.

4. Pop the caught exception from the stack.

5. Push \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\) back to the stack.

6. Jump to the position after the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) of the administrative instruction associated with the caught exception.

\[\begin{array}{rcl} \href{../exec/runtime.html#syntax-caught}{\mathsf{caught}}_n\{a\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^m \end{array}\]

Note

A caught exception can only be rethrown from the scope of the administrative instruction associated with it, i.e., from the scope of the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}\) or \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}\) block of a legacy \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}\) instruction. Upon exit from that block, the caught exception is discarded.