Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Small fixes on formal spec overview/examples #204

Merged
merged 2 commits into from
Feb 17, 2022
Merged

Small fixes on formal spec overview/examples #204

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
55480a9
Small fixes on formal spec overview/examples
aheejin Feb 16, 2022
098ed09
Remove trailing whitespaces
aheejin Feb 16, 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
98 changes: 49 additions & 49 deletions proposals/exception-handling/Exceptions-formal-examples.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Note that the block contexts and throw contexts given for the reductions are the

The only example with an almost full reduction trace, and all new instructions. Such explicit reduction steps are only shown in Example 4 and Example 5, to highlight the reduction step of the administrative `delegate`.

In the following reduction, we don't show the first 4 steps, which just reduce the several `try`s and the `throw x` to their respective administrative instructions. The type of the tag `$x` here is `[]→[]`.
In the following reduction, we don't show the first 4 steps, which just reduce the several `try`s and the `throw $x` to their respective administrative instructions. The type of the tag `$x` here is `[]→[]`.

```
(tag $x)
Expand Down Expand Up @@ -63,31 +63,31 @@ Take the frame `F = (locals i32.const 0, module m)`. We have:
```
↪ ↪ ↪
↪ F; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
(delegate{ 0 }
(label_0{}
(catch_0{ ε (local.set 0 (i32.const 27)) (rethrow 0) }
(catch{ ε (local.set 0 (i32.const 27)) (rethrow 0) }
(throw a_x) end) end) end) end) end) end)
```

For the trivial throw context `T = [_]` the above is the same as

```
↪ F; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
(delegate{ 0 }
(label_0{}
(catch_0{ ε (local.set 0 (i32.const 27)) (rethrow 0) }
(catch{ ε (local.set 0 (i32.const 27)) (rethrow 0) }
T[(throw a_x)]) end) end) end) end) end)

↪ F; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
(delegate{ 0 }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
(local.set 0 (i32.const 27))
(rethrow 0) end) end) end) end) end) end)
```
Expand All @@ -96,48 +96,48 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]` to

```
↪ F'; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
(delegate{ 0 }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
B^0[ (rethrow 0) ] end) end) end) end) end) end)

↪ F'; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
(delegate{ 0 }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
(throw a_x) end) end) end) end) end) end)
```

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.
Let `T' = (label_0{} (caught{ a_x ε } [_] end) end)` and use the same `B^0` as above to reduce the throw with the delegate.

```
↪ F'; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
(label_0{}
B^0[ (delegate{ 0 } T'[ (throw a_x) ] end) ] end) end) end)

↪ F'; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ 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_1`.
Use the trivial throw context `T` again, this time to match the throw to the `catch`.

```
↪ F'; (label_1{}
(catch_1{ a_x (local.get 0) }
(catch{ a_x (local.get 0) }
T[ (throw a_x) ] end) end)

↪ F'; (label_1{}
(caught_1{ a_x ε }
(caught{ a_x ε }
(local.get 0) end) end)

↪ F'; (label_1{}
(caught_1{ a_x ε }
(caught{ a_x ε }
(i32.const 27) end) end)

↪ F'; (label_1{}
Expand All @@ -153,11 +153,11 @@ Use the trivial throw context `T` again, this time to match the throw to the `ca
Location of a rethrown exception. Let `x, y, z` be tag indices of tags with type `[t_x]→[]`, `[t_y]→[]`, and `[t_z]→[]` respectively. Let `val_p : t_p` for every `p` among `x, y, z`.

```
try
try $label2
Copy link
Member Author

Choose a reason for hiding this comment

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

I think$label2 should be here, given that it points to this try's corresponding catch.. No?

val_x
throw x
catch x
try $label2
throw $x
catch $x
try
val_y
throw y
catch_all
Expand All @@ -177,8 +177,8 @@ Folded it looks as follows.
(try
(do
val_x
(throw x))
(catch x ;; <--- (rethrow 2) targets this catch.
(throw $x))
(catch $x ;; <--- (rethrow 2) targets this catch.
(try
(do
val_y
Expand All @@ -196,13 +196,13 @@ In the above example, all thrown exceptions get caught and the first one gets re

```
(label_0{}
(caught_0{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below.
(caught{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below.
val_x
(label_0{}
(caught_0{ a_y val_y }
(caught{ a_y val_y }
;; The catch_all does not leave val_y here.
(label_0{}
(caught_0{ a_z val_z }
(caught{ a_z val_z }
val_z
;; (rethrow 2) puts val_x and the throw below.
val_x
Expand All @@ -222,7 +222,7 @@ This reduces to `val_x (throw a_x)`, throwing to the caller.
(func
try $label0
rethrow $label0 ;; cannot be done, because it's not within catch below
catch x
catch $x
end)
```

Expand All @@ -237,7 +237,7 @@ This is a validation error (no catch block at given rethrow depth).
```
(try $l
(do
(throw x))
(throw $x))
(delegate $l))
```

Expand All @@ -252,23 +252,23 @@ try $label1
try
try $label0
try
throw x
throw $x
delegate $label0 ;; delegate 0
delegate $label1 ;; delegate 1
catch_all
end
catch x
catch $x
instr*
end
```

In folded form and reduced to the point `throw x` is called, this is:
In folded form and reduced to the point `throw $x` is called, this is:

```
(label_0{}
(catch_0{ a_x instr* }
(catch{ a_x instr* }
(label_0{}
(catch_0{ ε ε }
(catch{ ε ε }
(label_0{}
(delegate{ 1 }
(label_0{}
Expand All @@ -280,26 +280,26 @@ The `delegate{ 0 }` reduces using the trivial throw and block contexts to:

```
(label_0{}
(catch_0{ a_x instr* }
(catch{ a_x instr* }
(label_0{}
(catch_0{ ε ε }
(catch{ ε ε }
(label_0{}
(delegate{ 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_0{ ε ε } (label_0{} [_] end) end)` to the following:
The `delegate{ 1 }` reduces using the trivial throw context and the block context `B^1 := (catch{ ε ε } (label_0{} [_] end) end)` to the following:

```
(label_0{}
(catch_0{ a_x instr* }
(catch{ 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.
The thrown exception is (eventually) caught by the outer try's `catch $x`, so the above reduces to the following.

```
(label_0 {}
(caught_0{a_x}
(caught{a_x}
instr* end) end)
```

Expand All @@ -310,7 +310,7 @@ The thrown exception is (eventually) caught by the outer try's `catch x`, so the
```
try (result i32)
try $label0
throw x
throw $x
catch_all
try
throw y
Expand All @@ -328,7 +328,7 @@ In folded form this is:
(do
(try
(do
(throw x))
(throw $x))
(catch_all
(try
(do
Expand All @@ -342,9 +342,9 @@ When it's time to reduce `(throw y)`, the reduction looks as follows.

```
(label_1{}
(catch_1{ ε (i32.const 4) }
(catch{ ε (i32.const 4) }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
(label_0{}
(delegate{ 0 }
(throw a_y) end) end) end) end) end) end)
Expand All @@ -354,17 +354,17 @@ For `B^0 := [_] := T`, the above is the same as the following.

```
(label_1{}
(catch_1{ ε (i32.const 4) }
(catch{ ε (i32.const 4) }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
(label_0{}
B^0 [(delegate{ 0 } T[ (throw a_y) ] end)] end) end) end) end) end)

↪ (label_1{}
(catch_1{ ε (i32.const 4) }
(catch{ ε (i32.const 4) }
(label_0{}
(caught_0{ a_x ε }
(caught{ a_x ε }
(throw a_y) end) end) end) end)
```

So `throw a_y` gets correctly caught by `catch_1{ ε (i32.const 4) }` and this example reduces to `(i32.const 4)`.
So `throw a_y` gets correctly caught by `catch{ ε (i32.const 4) }` and this example reduces to `(i32.const 4)`.
4 changes: 2 additions & 2 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 @@ -185,11 +185,11 @@ label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end
↪ val^n (throw a)
```

Note that the last reduction step above is similar to the reduction of `br l` [1](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-l), if we look at the entire `delegate{l}...end` as the `br l`, but also doing a throw after it breaks.
Note that the last reduction step above is similar to the reduction of `br l` [1], if we look at the entire `delegate{l}...end` as the `br l`, but also doing a throw after it breaks.

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` we end up breaking inside the `l+1`th surrounding block, and throwing there. So if that `l+1`th surrounding block is a try, we end up throwing in its "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)
- [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`.

### Typing Rules for Administrative Instructions
Expand Down