Execution

Runtime Structure

Stack

Exception Handlers

Legacy exception handlers are installed by $\mathsf{try}$ instructions. Instead of branch labels, their catch clauses have instruction blocks associated with them. Furthermore, a $\mathsf{delegate}$ handler is associated with a label index to implicitly rewthrow to:

$$\begin{array}{r}\begin{array}{llll}& \mathit{catch}& ::=& \dots \\ & & |& \mathsf{catch}\mathit{tagidx}{\mathit{instr}}^{\ast }\\ & & |& \mathsf{catch}\mathsf{\_}\mathsf{all}\mathit{tagidx}{\mathit{instr}}^{\ast }\\ & & |& \mathsf{delegate}\mathit{labelidx}\end{array}\end{array}$$

Administrative Instructions

Administrative instructions are extended with the $\mathsf{caught}$ instruction that models exceptions caught by legacy exception handlers.

$$\begin{array}{r}\begin{array}{llcl}& \mathit{instr}& ::=& \dots \\ & & |& {\mathsf{caught}}_n\{\mathit{exnaddr}\}{\mathit{instr}}^{\ast }\mathsf{end}\end{array}\end{array}$$

Block Contexts

Block contexts are extended to include $\mathsf{caught}$ instructions:

$$\begin{array}{r}\begin{array}{llll}& B^k& ::=& \dots \\ & & |& {\mathsf{caught}}_n\{\mathit{exnaddr}\}{B}^k\mathsf{end}\end{array}\end{array}$$

Throw Contexts

Throw contexts are also extended to include $\mathsf{caught}$ instructions:

$$\begin{array}{r}\begin{array}{llll}& T& ::=& \dots \\ & & |& {\mathsf{caught}}_n\{\mathit{exnaddr}\}T\mathsf{end}\end{array}\end{array}$$

Instructions

Control Instructions

$\mathsf{try}\mathit{blocktype}{\mathit{instr}}_1^{\ast }(\mathsf{catch}x{\mathit{instr}}_2^{\ast }{)}^{\ast }(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}\mathsf{end}$

1. Assert: due to validation, ${\mathrm{expand}}_F(\mathit{blocktype})$ is defined.

2. Let $[t_1^m]\to [t_2^n]$ be the function type ${\mathrm{expand}}_F(\mathit{blocktype})$.

3. Let $L$ be the label whose arity is $n$ and whose continuation is the end of the $\mathsf{try}$ instruction.

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

5. Pop the values ${\mathit{val}}^m$ from the stack.

6. Let $F$ be the current frame.

7. For each catch clause $(\mathsf{catch}{x}_i{\mathit{instr}}_{2i}^{\ast })$ do:

   1. Assert: due to validation, $F.\mathsf{module}.\mathsf{tagaddrs}[x_i]$ exists.

   2. Let $a_i$ be the tag address $F.\mathsf{module}.\mathsf{tagaddrs}[x_i]$.

   3. Let ${\mathit{catch}}_i$ be the catch clause $(\mathsf{catch}{a}_i{\mathit{instr}}_{2i}^{\ast })$.

8. If there is a catch-all clause $(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast })$, then:

   1. Let ${\mathit{catch}}^{\prime ?}$ be the handler $(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast })$.

9. Else:

   1. Let ${\mathit{catch}}^{\prime ?}$ be empty.

10. Let ${\mathit{catch}}^{\ast }$ be the concatenation of ${\mathit{catch}}_i$ and ${\mathit{catch}}^{\prime ?}$.

11. Enter the block ${\mathit{val}}^m{\mathit{instr}}_1^{\ast }$ with label $L$ and exception handler ${\mathsf{handler}}_n\{{\mathit{catch}}^{\ast }{\}}^{\ast }$.

$$\begin{array}{r}\\ \begin{array}{l}F;{\mathit{val}}^m(\mathsf{try}\mathit{bt}{\mathit{instr}}_1^{\ast }(\mathsf{catch}x{\mathit{instr}}_2^{\ast }{)}^{\ast }(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}\mathsf{end}\hookrightarrow \\ F;{\mathsf{label}}_n\{ϵ\}({\mathsf{handler}}_n\{(\mathsf{catch}{a}_x{\mathit{instr}}_2^{\ast }{)}^{\ast }(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}\}{\mathit{val}}^m{\mathit{instr}}_1^{\ast }\mathsf{end})\mathsf{end}\\ (\text{if}{\mathrm{expand}}_F(\mathit{bt})=[t_1^m]\to [t_2^n]\wedge (F.\mathsf{module}.\mathsf{tagaddrs}[x]=a_x{)}^{\ast })\end{array}\end{array}$$

$\mathsf{try}\mathit{blocktype}{\mathit{instr}}^{\ast }\mathsf{delegate}l$

1. Assert: due to validation, ${\mathrm{expand}}_F(\mathit{blocktype})$ is defined.

2. Let $[t_1^m]\to [t_2^n]$ be the function type ${\mathrm{expand}}_F(\mathit{blocktype})$.

3. Let $L$ be the label whose arity is $n$ and whose continuation is the end of the $\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 ${\mathit{val}}^m$ from the stack.

7. Enter the block ${\mathit{val}}^m{\mathit{instr}}^{\ast }$ with label $L$ and exception handler HANDLER_n{DELEGATE~l}.

$$\begin{array}{r}\\ \begin{array}{lcl}F;{\mathit{val}}^m(\mathsf{try}\mathit{bt}{\mathit{instr}}^{\ast }\mathsf{delegate}l)& \hookrightarrow & F;{\mathsf{label}}_n\{ϵ\}({\mathsf{handler}}_n\{\mathsf{delegate}l\}{\mathit{val}}^m{\mathit{instr}}^{\ast }\mathsf{end})\mathsf{end}\\ & & (\text{if}{\mathrm{expand}}_F(\mathit{bt})=[t_1^m]\to [t_2^n])\end{array}\end{array}$$

$\mathsf{throw}\mathsf{\_}\mathsf{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 $\mathit{ref}$ from the stack.

4. If $\mathit{ref}$ is $\mathsf{ref}\mathsf{.}\mathsf{null}\mathit{ht}$, then:

   1. Trap.

5. Assert: due to validation, $\mathit{ref}$ is an exception reference.

6. Let $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ be $\mathit{ref}$.

7. Assert: due to validation, $S.\mathsf{exns}[\mathit{ea}]$ exists.

8. Let $\mathit{exn}$ be the exception instance $S.\mathsf{exns}[\mathit{ea}]$.

9. Let $a$ be the tag address $\mathit{exn}.\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 $(\mathsf{ref}\mathsf{.}\mathsf{exn}a)$ as a result.

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

14. Pop the exception handler ${\mathsf{handler}}_n\{{\mathit{catch}}^{\ast }\}$ from the stack.

15. If ${\mathit{catch}}^{\ast }$ is empty, then:

    1. Push the exception reference $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ back to the stack.

    2. Execute the instruction $\mathsf{throw}\mathsf{\_}\mathsf{ref}$ again.

16. Else:

    1. Let ${\mathit{catch}}_1$ be the first catch clause in ${\mathit{catch}}^{\ast }$ and ${{\mathit{catch}}^{\prime }}^{\ast }$ the remaining clauses.

    2. If ${\mathit{catch}}_1$ is of the form $\mathsf{catch}xl$ and the exception address $a$ equals $F.\mathsf{module}.\mathsf{tagaddrs}[x]$, then:

       1. Push the values $\mathit{exn}.\mathsf{fields}$ to the stack.

       2. Execute the instruction $\mathsf{br}l$.

    3. Else if ${\mathit{catch}}_1$ is of the form $\mathsf{catch}\mathsf{\_}\mathsf{ref}xl$ and the exception address $a$ equals $F.\mathsf{module}.\mathsf{tagaddrs}[x]$, then:

       1. Push the values $\mathit{exn}.\mathsf{fields}$ to the stack.

       2. Push the exception reference $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ to the stack.

       3. Execute the instruction $\mathsf{br}l$.

    4. Else if ${\mathit{catch}}_1$ is of the form $\mathsf{catch}\mathsf{\_}\mathsf{all}l$, then:

       1. Execute the instruction $\mathsf{br}l$.

    5. Else if ${\mathit{catch}}_1$ is of the form $\mathsf{catch}\mathsf{\_}\mathsf{all}\mathsf{\_}\mathsf{ref}l$, then:

       1. Push the exception reference $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ to the stack.

       2. Execute the instruction $\mathsf{br}l$.

    6. Else if ${\mathit{catch}}_1$ is of the form $\mathsf{catch}x{\mathit{instr}}^{\ast }$ and the exception address $a$ equals $F.\mathsf{module}.\mathsf{tagaddrs}[x]$, then:

       1. Push the caught exception ${\mathsf{caught}}_n\{\mathit{ea}\}$ to the stack.

       2. Push the values $\mathit{exn}.\mathsf{fields}$ to the stack.

       3. Enter the catch block ${\mathit{instr}}^{\ast }$.

    7. Else if ${\mathit{catch}}_1$ is of the form $\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}^{\ast }$, then:

       1. Push the caught exception ${\mathsf{caught}}_n\{\mathit{ea}\}$ to the stack.

       2. Enter the catch block ${\mathit{instr}}^{\ast }$.

    8. Else if ${\mathit{catch}}_1$ is of the form $\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 $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ back to the stack.

       6. Execute the instruction $\mathsf{throw}\mathsf{\_}\mathsf{ref}$ again.

    9. Else:

       1. Push the modified handler ${\mathsf{handler}}_n\{{{\mathit{catch}}^{\prime }}^{\ast }\}$ back to the stack.

       2. Push the exception reference $\mathsf{ref}\mathsf{.}\mathsf{exn}\mathit{ea}$ back to the stack.

       3. Execute the instruction $\mathsf{throw}\mathsf{\_}\mathsf{ref}$ again.

$$\begin{array}{r}\\ \begin{array}{r}\dots \\ {\mathsf{handler}}_n\{(\mathsf{catch}x{\mathit{instr}}^{\ast }){\mathit{catch}}^{\ast }\}T[(\mathsf{ref}\mathsf{.}\mathsf{exn}a)\mathsf{throw}\mathsf{\_}\mathsf{ref}]\mathsf{end}& \hookrightarrow & {\mathsf{caught}}_n\{a\}\mathit{exn}.\mathsf{fields}{\mathit{instr}}^{\ast }\mathsf{end}\\ & & (\begin{array}{rl}\text{if}& \mathit{exn}=S.\mathsf{exns}[a]\\ \wedge & \mathit{exn}.\mathsf{tag}=F.\mathsf{module}.\mathsf{tagaddrs}[x])\end{array}\\ {\mathsf{handler}}_n\{(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}^{\ast }){\mathit{catch}}^{\ast }\}T[(\mathsf{ref}\mathsf{.}\mathsf{exn}a)\mathsf{throw}\mathsf{\_}\mathsf{ref}]\mathsf{end}& \hookrightarrow & {\mathsf{caught}}_n\{a\}{\mathit{instr}}^{\ast }\mathsf{end}\\ B^l[{\mathsf{handler}}_n\{(\mathsf{delegate}l){\mathit{catch}}^{\ast }\}T[(\mathsf{ref}\mathsf{.}\mathsf{exn}a)\mathsf{throw}\mathsf{\_}\mathsf{ref}]\mathsf{end}]& \hookrightarrow & (\mathsf{ref}\mathsf{.}\mathsf{exn}a)\mathsf{throw}\mathsf{\_}\mathsf{ref}\end{array}\end{array}$$

$\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 $(\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 $\mathsf{ref}\mathsf{.}\mathsf{exn}a$ onto the stack.

6. Execute the instruction $\mathsf{throw}\mathsf{\_}\mathsf{ref}$.

$$\begin{array}{r}\\ \begin{array}{lcl}{\mathsf{caught}}_n\{a\}{B}^l[\mathsf{rethrow}l]\mathsf{end}& \hookrightarrow & {\mathsf{caught}}_n\{a\}{B}^l[(\mathsf{ref}\mathsf{.}\mathsf{exn}a)\mathsf{throw}\mathsf{\_}\mathsf{ref}]\mathsf{end}\end{array}\end{array}$$

Entering a catch block

1. Jump to the start of the instruction sequence ${\mathit{instr}}^{\ast }$.

Exiting a catch block

When the $\mathsf{end}$ of a catch block is reached without a jump, thrown exception, or trap, then the following steps are performed.

1. Let ${\mathit{val}}^m$ be the values on the top of the stack.

2. Pop the values ${\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 ${\mathit{val}}^m$ back to the stack.

6. Jump to the position after the $\mathsf{end}$ of the administrative instruction associated with the caught exception.

$$\begin{array}{rcl}{\mathsf{caught}}_n\{a\}{\mathit{val}}^m\mathsf{end}& \hookrightarrow & {\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 $\mathsf{catch}$ or $\mathsf{catch}\mathsf{\_}\mathsf{all}$ block of a legacy $\mathsf{try}$ instruction. Upon exit from that block, the caught exception is discarded.