From 3dc715af65975b8946194042529f9819a036e19b Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Tue, 15 Feb 2022 14:46:36 +0100 Subject: [PATCH] formal spec overview for the 3rd exception handling proposal (#143) * formal spec overview for the 3rd exception handling proposal This adds a condensed version of the current core formal spec, and some examples of reductions according to this spec. These files were added to aid in discussions when finalising spec details. After 260 PR comments and suggestions co-authors are: Co-authored-by: Andreas Rossberg Co-authored-by: Heejin Ahn Co-authored-by: Ross Tate --- interpreter/exec/eval.ml | 6 +- .../Exceptions-formal-examples.md | 370 ++++++++++++++++++ .../Exceptions-formal-overview.md | 222 +++++++++++ test/core/try_delegate.wast | 30 +- 4 files changed, 621 insertions(+), 7 deletions(-) create mode 100644 proposals/exception-handling/Exceptions-formal-examples.md create mode 100644 proposals/exception-handling/Exceptions-formal-overview.md diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 045ddeeb..b8390ade 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -236,8 +236,7 @@ let rec step (c : config) : config = let n1 = Lib.List32.length ts1 in let n2 = Lib.List32.length ts2 in let args, vs' = take n1 vs e.at, drop n1 vs e.at in - let k = Int32.succ x.it in - vs', [Label (n2, [], ([], [Delegate (k, (args, List.map plain es')) @@ e.at])) @@ e.at] + vs', [Label (n2, [], ([], [Delegate (x.it, (args, List.map plain es')) @@ e.at])) @@ e.at] | Drop, v :: vs' -> vs', [] @@ -693,9 +692,6 @@ let rec step (c : config) : config = | Catch (n, cts, ca, (vs', [])), vs -> vs' @ vs, [] - | Catch (n, cts, ca, (vs', {it = Delegating (0l, a, vs0); at} :: es')), vs -> - vs, [Catch (n, cts, ca, (vs', (Throwing (a, vs0) @@ at) :: es')) @@ e.at] - | Catch (n, cts, ca, (vs', ({it = Trapping _ | Breaking _ | Returning _ | Delegating _; at} as e) :: es')), vs -> vs, [e] diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md new file mode 100644 index 00000000..48ea8ece --- /dev/null +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -0,0 +1,370 @@ +# 3rd Proposal Formal Spec Examples + +This document contains WebAssembly code examples mentioned in comments on this repository, and what they reduce to, according to the ["3rd proposal formal spec overview"](Exceptions-formal-overview.md). + +Its purpose is to make sure everyone is happy with the implications of the semantics in the current 3rd proposal, or to aid discussions on these semantics. + +The first *example 0* contains all the new instructions, and it is the only one with an almost full reduction displayed. It is meant to easily show how the spec works, even if the reader has not spent much time with the WebAssembly formal spec. + +For all other examples just the result of the reduction is given. These examples are taken from comments in this repository, which are linked. Sometimes/often the examples are modified to fit the current syntax. + +If anyone would like that I add another reduction trace, or other examples, please let me know, I'd be happy to. + +### Notation + +If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `a_x := F.tag[x]`, where `F` is the current frame. + +Note that the block contexts and throw contexts given for the reductions are the largest possible in each case, so the reduction steps are the only possible ones. + +## Example 0 + +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 `[]→[]`. + +``` +(tag $x) +(func (result i32) (local i32) + try (result i32) + try + try + throw $x + catch_all + i32.const 27 + local.set 0 + rethrow 0 + end + delegate 0 + catch $x + local.get 0 + end) +``` + +We write the body of this function in folded form, because it is easier to parse. + +``` +(try (result i32) + (do + (try + (do + (try + (do + (throw $x)) + (catch_all + (local.set 0 (i32.const 27)) + (rethrow 0)))) + (delegate 0))) + (catch $x + (local.get 0))) +``` + +Take the frame `F = (locals i32.const 0, module m)`. We have: + +``` +↪ ↪ ↪ +↪ F; (label_1{} + (catch_1{ a_x (local.get 0) } + (label_0{} + (delegate{ 0 } + (label_0{} + (catch_0{ ε (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) } + (label_0{} + (delegate{ 0 } + (label_0{} + (catch_0{ ε (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) } + (label_0{} + (delegate{ 0 } + (label_0{} + (caught_0{ a_x ε } + (local.set 0 (i32.const 27)) + (rethrow 0) end) end) end) end) end) end) +``` + +Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]` to reduce `rethrow 0`. + +``` +↪ F'; (label_1{} + (catch_1{ a_x (local.get 0) } + (label_0{} + (delegate{ 0 } + (label_0{} + (caught_0{ a_x ε } + B^0[ (rethrow 0) ] end) end) end) end) end) end) + +↪ F'; (label_1{} + (catch_1{ a_x (local.get 0) } + (label_0{} + (delegate{ 0 } + (label_0{} + (caught_0{ 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. + +``` +↪ F'; (label_1{} + (catch_1{ 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) } + (throw a_x) end) end) +``` + +Use the trivial throw context `T` again, this time to match the throw to the `catch_1`. + +``` +↪ F'; (label_1{} + (catch_1{ a_x (local.get 0) } + T[ (throw a_x) ] end) end) + +↪ F'; (label_1{} + (caught_1{ a_x ε } + (local.get 0) end) end) + +↪ F'; (label_1{} + (caught_1{ a_x ε } + (i32.const 27) end) end) + +↪ F'; (label_1{} + (i32.const 27) end) + +↪ F'; (i32.const 27) +``` + +## Behavior of `rethrow` + +### Example 1 + +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 + val_x + throw x +catch x + try $label2 + val_y + throw y + catch_all + try + val_z + throw z + catch z + rethrow $label2 ;; This is rethrow 2. + end + end +end +``` + +Folded it looks as follows. + +``` +(try + (do + val_x + (throw x)) + (catch x ;; <--- (rethrow 2) targets this catch. + (try + (do + val_y + (throw y)) + (catch_all + (try + (do + val_z + (throw z)) + (catch z + (rethrow 2))))))) +``` + +In the above example, all thrown exceptions get caught and the first one gets rethrown from the catching block of the last one. So the above reduces to + +``` +(label_0{} + (caught_0{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below. + val_x + (label_0{} + (caught_0{ a_y val_y } + ;; The catch_all does not leave val_y here. + (label_0{} + (caught_0{ a_z val_z } + val_z + ;; (rethrow 2) puts val_x and the throw below. + val_x + (throw a_x) end) end) end) end) end) end) +``` + +This reduces to `val_x (throw a_x)`, throwing to the caller. + +### Example 2 + +`rethrow`'s immediate validation error. + +@aheejin gave the following +[example in this comment](https://github.com/WebAssembly/exception-handling/pull/143#discussion_r522673735) + +``` +(func + try $label0 + rethrow $label0 ;; cannot be done, because it's not within catch below + catch x + end) +``` + +This is a validation error (no catch block at given rethrow depth). + +## Target of `delegate`'s Immediate (Label Depth) + +### Example 3 + +`delegate 0` target. + +``` +(try $l + (do + (throw x)) + (delegate $l)) +``` + +This is a validation error, a `delegate` always refers to an outer block. + +### Example 4 + +`delegate` correctly targeting a `try-delegate` and a `try-catch`. + +``` +try $label1 + try + try $label0 + try + throw x + delegate $label0 ;; delegate 0 + delegate $label1 ;; delegate 1 + catch_all + end +catch x + instr* +end +``` + +In folded form and reduced to the point `throw x` is called, this is: + +``` +(label_0{} + (catch_0{ a_x instr* } + (label_0{} + (catch_0{ ε ε } + (label_0{} + (delegate{ 1 } + (label_0{} + (delegate{ 0 } + (throw a_x) end) end) end) end) end) end) end) end) +``` + +The `delegate{ 0 }` reduces using the trivial throw and block contexts to: + +``` +(label_0{} + (catch_0{ a_x instr* } + (label_0{} + (catch_0{ ε ε } + (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: + +``` +(label_0{} + (catch_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_0{a_x} + instr* end) end) +``` + +### Example 5 + +`delegate 0` targeting a catch inside a try. + +``` +try (result i32) + try $label0 + throw x + catch_all + try + throw y + delegate $label0 ;; delegate 0 + end +catch_all + i32.const 4 +end +``` + +In folded form this is: + +``` +(try (result i32) + (do + (try + (do + (throw x)) + (catch_all + (try + (do + (throw y) + (delegate 0)))))) + (catch_all + (i32.const 4))) +``` + +When it's time to reduce `(throw y)`, the reduction looks as follows. + +``` +(label_1{} + (catch_1{ ε (i32.const 4) } + (label_0{} + (caught_0{ a_x ε } + (label_0{} + (delegate{ 0 } + (throw a_y) end) end) end) end) end) end) +``` + +For `B^0 := [_] := T`, the above is the same as the following. + +``` +(label_1{} + (catch_1{ ε (i32.const 4) } + (label_0{} + (caught_0{ 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) } + (label_0{} + (caught_0{ 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)`. diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md new file mode 100644 index 00000000..b3af11b0 --- /dev/null +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -0,0 +1,222 @@ +# 3rd Proposal Formal Spec Overview + +This is an overview of the 3rd proposal's formal spec additions, to aid in discussions concerning the proposed semantics. + +## Abstract Syntax + +### Types + +#### Tag Types + +``` +tagtype ::= [valtype*]→[] +``` + +### Instructions + +``` +instr ::= ... | 'throw' tagidx | 'rethrow' labelidx + | 'try' blocktype instr* ('catch' tagidx instr*)* ('catch_all' instr*)? 'end' + | 'try' blocktype instr* 'delegate' labelidx +``` + +### Modules + +#### Tags + +``` +tag ::= export* 'tag' tagtype | export* 'tag' tagtype import +``` + +#### Modules + +``` +mod ::= 'module' ... tag* +``` + +## Validation (Typing) + +#### Modification to Labels + +To verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we introduce a `kind` attribute to labels in the validation context, which is set to `catch` when the label is a catch-label and empty otherwise. + +``` +labelkind ::= 'catch' +labeltype ::= 'catch'? resulttype +C ::= {..., 'labels' labeltype} +``` + +The original notation `labels [t*]` is now an abbreviation for: + +``` +'labels' [t*] ::= 'labels' ε [t*] +``` + +### Validation Contexts + +Validation contexts now hold a list of tag types, one for each tag known to them. +``` +C ::= { ..., 'tags' tagtype*} +``` + +### Validation Rules for Instructions + + +``` +C.tags[x] = [t*]→[] +----------------------------- +C ⊢ throw x : [t1* t*]→[t2*] + + +C.labels[l].kind = catch +---------------------------- +C ⊢ rethrow l : [t1*]→[t2*] + + +C ⊢ bt : [t1*]→[t2*] +C, labels [t2*] ⊢ instr* : [t1*]→[t2*] +(C.tags[x] = [t*]→[] ∧ + C, labels catch [t2*] ⊢ instr'* : [t*]→[t2*])* +(C, labels catch [t2*] ⊢ instr''* : []→[t2*])? +----------------------------------------------------------------------------- +C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] + + +C ⊢ bt : [t1*]→[t2*] +C, labels [t2*] ⊢ instr* : [t1*]→[t2*] +C.labels[l] = [t*] +------------------------------------------- +C ⊢ try bt instr* delegate l : [t1*]→[t2*] +``` + +## Execution (Reduction) + +### Runtime Structure + +#### Stores + +``` +S ::= {..., 'tags' taginst*} +``` + +#### Tag Instances + +``` +taginst ::= {'type' tagtype} +``` + +#### Module Instances + +``` +m ::= {..., 'tags' tagaddr*} +``` + +#### Administrative Instructions + +``` +instr ::= ... | 'throw' tagaddr | 'catch'{ tagaddr? instr* }* instr* 'end' + | 'delegate'{ labelidx } instr* 'end' | 'caught'{ tagaddr val^n } instr* 'end' +``` + +#### Block Contexts and Label Kinds + +So far block contexts are only used in the reduction of `br l` and `return`, and only include labels or values on the stack on the left side of the hole `[_]`. If we want to be able to break jumping over try-catch and try-delegate blocks, we must allow for the new administrative control instructions to appear after labels in block contexts. + +``` +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' +``` + +#### Throw Contexts + +Throw contexts don't skip over handlers (administrative `catch` or `delegate` instructions). +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 +``` + +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. + +### 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`. + +``` +F; throw x ↪ F; throw a (if F.module.tagaddrs[x]=a) + +caught{a val^n} B^l[rethrow l] end + ↪ caught{a val^n} B^l[val^n (throw a)] end + +caught{a val^n} val^m end ↪ val^m + + +F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) + ↪ F; label_m{} (catch{a instr'*}*{ε instr''*}? val^n instr* end) end + (if expand_F(bt) = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) + +catch{a? instr*}* val^m end ↪ val^m + +S; F; catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ S; F; caught{a val^n} (val^n)? instr* end + (if (a1? = ε ∨ a1? = a) ∧ S.tags(a).type = [t^n]→[]) + +catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ catch{a'? instr'*}* T[val^n (throw a)] end + (if a1? ≠ ε ∧ a1? ≠ a) + +catch T[val^n (throw a)] end ↪ val^n (throw a) + + +F; val^n (try bt instr* delegate l) + ↪ F; label_m{} (delegate{l} val^n instr* end) end + (if expand_F(bt) = [t^n]→[t^m]) + +delegate{l} val^n end ↪ val^n + +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. + +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) +- [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 + +``` +S.tags[a].type = [t*]→[] +-------------------------------- +S;C ⊢ throw a : [t1* t*]→[t2*] + +((S.tags[a].type = [t'*]→[])? + S;C, labels catch [t*] ⊢ instr'* : [t'*?]→[t*])* +S;C, labels [t*] ⊢ instr* : []→[t*] +----------------------------------------------------------- +S;C, labels [t*] ⊢ catch{a? instr'*}* instr* end : []→[t*] + +S;C, labels [t*] ⊢ instr* : []→[t*] +C.labels[l] = [t'*] +------------------------------------------------------ +S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] + +S.tags[a].type = [t'*]→[] +(val:t')* +S;C, labels catch [t*] ⊢ instr* : []→[t*] +---------------------------------------------------------- +S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] +``` + +## TODO Uncaught Exceptions + +We haven't yet described the formalism for an uncaught exception being the result of evaluation. diff --git a/test/core/try_delegate.wast b/test/core/try_delegate.wast index bbc5c0a0..8ee864eb 100644 --- a/test/core/try_delegate.wast +++ b/test/core/try_delegate.wast @@ -62,7 +62,12 @@ (catch_all (i32.const 1))) ) - (func (export "delegate-to-caller") + (func (export "delegate-to-caller-trivial") + (try + (do (throw $e0)) + (delegate 0))) + + (func (export "delegate-to-caller-skipping") (try (do (try (do (throw $e0)) (delegate 1))) (catch_all)) ) @@ -92,6 +97,24 @@ (catch $e1 (i32.const 2)) ) ) + + (func (export "delegate-correct-targets") (result i32) + (try (result i32) + (do (try $l3 + (do (try $l2 + (do (try $l1 + (do (try $l0 + (do (try + (do (throw $e0)) + (delegate $l1))) + (catch_all unreachable))) + (delegate $l3))) + (catch_all unreachable))) + (catch_all (try + (do (throw $e0)) + (delegate $l3)))) + unreachable) + (catch_all (i32.const 1)))) ) (assert_return (invoke "delegate-no-throw") (i32.const 1)) @@ -112,7 +135,10 @@ (assert_return (invoke "delegate-to-block") (i32.const 1)) (assert_return (invoke "delegate-to-catch") (i32.const 1)) -(assert_exception (invoke "delegate-to-caller")) +(assert_exception (invoke "delegate-to-caller-trivial")) +(assert_exception (invoke "delegate-to-caller-skipping")) + +(assert_return (invoke "delegate-correct-targets") (i32.const 1)) (assert_malformed (module quote "(module (func (delegate 0)))")