Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Formal overview: add uncaught exceptions #221

Merged
merged 2 commits into from
Sep 16, 2022
Merged

Formal overview: add uncaught exceptions #221

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9e863ce
Formal overview: add uncaught exceptions
ioannad Sep 6, 2022
3ac9af9
Addressed review comments.
ioannad Sep 9, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 12 additions & 5 deletions proposals/exception-handling/Exceptions-formal-overview.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,9 +139,10 @@ Throw contexts don't skip over handlers (administrative `catch` or `delegate` in
Throw contexts are used to match a thrown exception with the innermost handler.

```
T ::= val* '[_]' instr* | 'label'_n{instr*} T 'end'
| 'caught'{ tagaddr val^n } T 'end'
| 'frame'_n{F} T end
T ::= '[_]' | val* T instr*
| 'label'_n{instr*} T 'end'
| 'caught'{ tagaddr val* } 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.
Expand Down Expand Up @@ -222,6 +223,12 @@ S;C, labels (catch [t*]) ⊢ instr* : []→[t*]
S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*]
```

## TODO Uncaught Exceptions
## Uncaught Exceptions

A new [result](https://webassembly.github.io/spec/core/exec/runtime.html#syntax-result) value is added to describe uncaught exceptions.

```
result ::= val* | trap
| T[val* (throw tagaddr)]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • What @rossberg suggested was val* T[throw e] instr*... Is this different from T[val* (throw tagaddr)]?
  • How are the cases, which a throw context contains not only a throw and vals but other things... such as label, caught, or frame as listed in the throw context section, covered?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What @rossberg suggested was val* T[throw e] instr*... Is this different from T[val* (throw tagaddr)]?

They were different when @rossberg suggested the former formulation, but in this PR I also changed throw contexts from T ::= val* '[_]' instr* | ... to T ::= '[_]' | val* T instr* | ..., so now these two things val* T[throw e] instr* and T[val* (throw tagaddr)] are really the same.

How are the cases, which a throw context contains not only a throw and vals but other things... such as label, caught, or frame as listed in the throw context section, covered?

So now throw contexts surrounded by values and instructions are also throw contexts. Meaning that val* T instr* is a throw context too.

```

We haven't yet described the formalism for an uncaught exception being the result of evaluation.