From 9c0c1a8f3840382a0090fc42809df7e556ee5120 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 10 Nov 2020 11:46:32 +0100 Subject: [PATCH 01/24] formal spec overview for the 3rd exception handling proposal This is an attempt to formally describe @aheejin's 3rd proposal, which she presented to the Wasm CG, and which was voted to be the new EH proposal, on September 18, 2020. This is not formal spec that I have developed, but a formal description of this 3rd proposal. This is a reworked form of my [first attempt on this formal spec overview](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-702323595) edited with my new understanding of the spec based on the discussion below, and in other issues, and according to @aheejin 's [3rd proposal overview](https://github.com/WebAssembly/exception-handling/blob/f7a4f60d11fb6326fc13f84d3889b11d3873f08a/proposals/Exceptions.md) in PR #137. This is in the form of a document as @tlively [requested](https://github.com/WebAssembly/exception-handling/issues/142#issuecomment-724246117), to make discussion on specific points easier. I wrote this formal spec overview roughly in the style of the 2nd proposal's [formal spec overview](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-517216137) by @rossberg. Particular points of interest: - In this I assume `rethrow` does have an immediate, as it is now described in #137. - The instruction `unwind` now reduces to `catch_all ... rethrow` as specified in Heejin's overview. - Because unwind is much simpler in this MVP, there is no `throw_point` anymore and `caught_m` is much simpler. - The introduction of `caught_m` now also introduces a label around the catch instructions, which label a rethrow instruction can reference. - Added explanation of the peculiar side condition in try's execution rule - just trying to make the rules more compact. I would be happy if anyone could point out things that are wrong or that I misunderstood. --- .../Exceptions-formal-overview.md | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 proposals/exception-handling/Exceptions-formal-overview.md diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md new file mode 100644 index 00000000..a90f75f1 --- /dev/null +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -0,0 +1,165 @@ +# 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 + +Exception Types + +``` +exntype ::= [t*] -> [] +``` + +### Instructions + +``` +instr ::= ... | throw x | rethrow l + | try bt instr* (catch x instr*)+ end + | try bt instr* (catch x instr*)* catch_all instr* end + | try bt instr* delegate l + | try bt instr* unwind instr* end +``` + +### Modules + +Exceptions (definitions) + +``` +exn ::= export* exception exntype | export* exception exntype import +``` + +Modules + + +``` +mod ::= module ... exn* +``` + +## Validation (Typing) + +To verify that a `try...delegate l` instruction refers to a label introduced by a try block (I'll call this a try-label), introduce a type attribute to labels in the validation context, which type attribute is set to `try` when the label is a try-label. The original notation `label [t*]` will then be a shortcut for `label {result [t*], type ε}`. + +Moreover, to verify that the `rethrow l` instruction refers to a label introduced by a catch block (call this a catch-label), we allow this type attribute of labels in the validation context to be set to `catch` when the label is a catch label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the instructions of the catching try-block's catch instructions. + + +### Instructions + + +``` +C_exn(x) = [t*] -> [] +-------------------------------- +C |- throw x : [t1* t*] -> [t2*] + + +C_label(l).type = catch +------------------------------- +C |- rethrow l : [t1*] -> [t2*] + + +bt = [t1*] -> [t2*] +C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*] +(C_exn(x_i) = [t'_i*] -> [])^n +(C, label {result [t2*], type catch} |- instr_i* : [t'_i*] -> [t2*])^n +(C, label {result [t2*], type catch} |- instr'* : [] -> [t2*])? +---------------------------------------------------------------------- +try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)? end : bt + + +bt = [t1*] -> [t2*] +C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*] +C_label(l).type = try +------------------------------------------------------------ +try bt instr* delegate l : bt + + +bt = [t1*] -> [t2*] +C, label {result [t2*], type try} |- instr_1* : [t1*] -> [t2*] +C, label {result [t2*], type catch} |- instr_2* : [] -> [t2*] +-------------------------------------------------------------- +try bt instr_1* unwind instr_2* : bt +``` + +## Execution (Reduction) + +### Runtime structure + +Stores + +``` +S ::= {..., exn exninst*} +``` + +Exception Instances + +``` +exninst ::= {type exntype} +``` + +Module Instances + +``` +m ::= {..., (exn a)*} +``` + +Administrative Instructions + +``` +instr ::= ... | throw a | catch_n{a instr*}*{instr*} instr* end + | delegate{l} instr* end | caught_m{a val^n} instr* end +``` + +Throw Contexts + +``` +T ::= v* [_] e* | label_n{e*} T end | caught_m{a val^n} T end | frame_n{F} T end +``` + +### Instructions + +In the following reduction rules, note that `caught_m` introduces a label around the catching instructions. This corresponds to the label a `rethrow l` would target. + + +``` +F; throw x --> F; throw a (iff F_exn(x) = a) + +caught_m{a val^n} label_m{} B^l[rethrow l] end end + --> caught_m{a val^n} label_m{} B^l[val^n (throw a)] end end + +caught_m{a val^n} val^m end --> val^m +``` + +The requirements below involving `k` are to distinguish between a missing `catch_all` and an existing `catch_all` with no instructions (`nop` is added to the empty instruction set of an existing `catch_all`). + +``` +F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)^k end) + --> F; catch_m{a_i instr_i*}*{instr''*} (label_m{} val^n instr* end) end + (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)* and + (if k=1 and instr'*=ε then instr''* = nop) + and (if k=1 and inst'*=/=ε then instr''* = instr'*) and (if k=0 then instr''*=ε). + +catch_m{a_i instr_i*}*{instr'*} val^m end --> val^m + +S; F; catch_m{a_i instr_i*}*{instr'*} T[val^n (throw a)] end + --> S; F; caught_m{a val^n} label_m{} val^n instr_i* end end + (iff S_exn(a) = {type [t^n]->[]} and a_i = a) + +S; F; catch_m{a_i instr_i*}*{instr*} T[val^n (throw a)] end + --> S; F; caught_m{a val^n} label_m{} instr* end end + (iff S_exn(a) = {type [t^n]->[]} and instr =/= ε and for every i, a_i =/= a) + +S; F; catch_m{a_i instr_i*}*{ε} T[val^n (throw a)] end + --> S; F; val^n (throw a) + (iff for every i, a_i =/= a) + + +val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end + (iff bt = [t^n] -> [t^m]) + +catch_m{a_i instr_i*}*{instr*} (label_m{} B^l[ delegate{l} (T[val^n (throw a)]) end ] end) end + --> catch_m{a_i instr_i*}*{instr*} label_m{} val^n (throw a) end end + + +try bt instr* unwind instr'* end --> try bt instr* catch_all instr'* rethrow 0 end +``` From 2dc31f8719e1d54682fe384be8098d4117a3c0c4 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 26 Nov 2020 17:40:40 +0100 Subject: [PATCH 02/24] Removes catch-labels for rethrow Adds caught-stack to the runtime and to validation contexts. Question: Should the administrative instruction `caught` be removed from the right hand side of rethrow's execution step? --- .../Exceptions-formal-overview.md | 31 ++++++++++--------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index a90f75f1..9a55b32a 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -41,8 +41,7 @@ mod ::= module ... exn* To verify that a `try...delegate l` instruction refers to a label introduced by a try block (I'll call this a try-label), introduce a type attribute to labels in the validation context, which type attribute is set to `try` when the label is a try-label. The original notation `label [t*]` will then be a shortcut for `label {result [t*], type ε}`. -Moreover, to verify that the `rethrow l` instruction refers to a label introduced by a catch block (call this a catch-label), we allow this type attribute of labels in the validation context to be set to `catch` when the label is a catch label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the instructions of the catching try-block's catch instructions. - +To verify that the `rethrow l` instruction refers to a surrounding catch block, we introduce a stack `caught` to validation contexts, which gets an exception index or the keywork `all` prepended whenever we enter instructions inside a `catch exnidx` or `catch_all` block, respectively. This addition is reflected in the execution rules, by the administrative instruction `caught` which models the stack of caught exceptions on the wasm stack. ### Instructions @@ -53,7 +52,7 @@ C_exn(x) = [t*] -> [] C |- throw x : [t1* t*] -> [t2*] -C_label(l).type = catch +C_caught(l) =/= ε ------------------------------- C |- rethrow l : [t1*] -> [t2*] @@ -61,9 +60,9 @@ C |- rethrow l : [t1*] -> [t2*] bt = [t1*] -> [t2*] C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*] (C_exn(x_i) = [t'_i*] -> [])^n -(C, label {result [t2*], type catch} |- instr_i* : [t'_i*] -> [t2*])^n -(C, label {result [t2*], type catch} |- instr'* : [] -> [t2*])? ----------------------------------------------------------------------- +(C, label [t2*], caught x_i |- instr_i* : [t'_i*] -> [t2*])^n +(C, label [t2*], caught all |- instr'* : [] -> [t2*])? +------------------------------------------------------------------ try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)? end : bt @@ -76,7 +75,7 @@ try bt instr* delegate l : bt bt = [t1*] -> [t2*] C, label {result [t2*], type try} |- instr_1* : [t1*] -> [t2*] -C, label {result [t2*], type catch} |- instr_2* : [] -> [t2*] +C, label [t2*], caught all |- instr_2* : [] -> [t2*] -------------------------------------------------------------- try bt instr_1* unwind instr_2* : bt ``` @@ -110,6 +109,13 @@ instr ::= ... | throw a | catch_n{a instr*}*{instr*} instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` +Caught exceptions stack + +``` +C^0 ::= val^m [_] instr +C^{n+1} ::= caught{exnaddr val^k} C^n end +``` + Throw Contexts ``` @@ -118,14 +124,12 @@ T ::= v* [_] e* | label_n{e*} T end | caught_m{a val^n} T end | frame_n{F} T end ### Instructions -In the following reduction rules, note that `caught_m` introduces a label around the catching instructions. This corresponds to the label a `rethrow l` would target. - ``` F; throw x --> F; throw a (iff F_exn(x) = a) -caught_m{a val^n} label_m{} B^l[rethrow l] end end - --> caught_m{a val^n} label_m{} B^l[val^n (throw a)] end end +caught_m{a val^n} C^l[rethrow l] end + --> caught_m{a val^n} C^l[val^n (throw a)] end caught_m{a val^n} val^m end --> val^m ``` @@ -142,18 +146,17 @@ F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)^k end) catch_m{a_i instr_i*}*{instr'*} val^m end --> val^m S; F; catch_m{a_i instr_i*}*{instr'*} T[val^n (throw a)] end - --> S; F; caught_m{a val^n} label_m{} val^n instr_i* end end + --> S; F; caught_m{a val^n} val^n instr_i* end (iff S_exn(a) = {type [t^n]->[]} and a_i = a) S; F; catch_m{a_i instr_i*}*{instr*} T[val^n (throw a)] end - --> S; F; caught_m{a val^n} label_m{} instr* end end + --> S; F; caught_m{a val^n} instr* end (iff S_exn(a) = {type [t^n]->[]} and instr =/= ε and for every i, a_i =/= a) S; F; catch_m{a_i instr_i*}*{ε} T[val^n (throw a)] end --> S; F; val^n (throw a) (iff for every i, a_i =/= a) - val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end (iff bt = [t^n] -> [t^m]) From 57c41e5881677e5da57f3665d7a2d1c05b10b368 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 26 Nov 2020 17:53:54 +0100 Subject: [PATCH 03/24] Allows try blocks without catches. --- .../Exceptions-formal-overview.md | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 9a55b32a..8d57d86e 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -16,8 +16,7 @@ exntype ::= [t*] -> [] ``` instr ::= ... | throw x | rethrow l - | try bt instr* (catch x instr*)+ end - | try bt instr* (catch x instr*)* catch_all instr* end + | try bt instr* (catch x instr*)* (catch_all instr*)? end | try bt instr* delegate l | try bt instr* unwind instr* end ``` @@ -105,7 +104,7 @@ m ::= {..., (exn a)*} Administrative Instructions ``` -instr ::= ... | throw a | catch_n{a instr*}*{instr*} instr* end +instr ::= ... | throw a | catch_n{a instr*}*{instr*}? instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` @@ -134,34 +133,33 @@ caught_m{a val^n} C^l[rethrow l] end caught_m{a val^n} val^m end --> val^m ``` -The requirements below involving `k` are to distinguish between a missing `catch_all` and an existing `catch_all` with no instructions (`nop` is added to the empty instruction set of an existing `catch_all`). +A keyword `all` is introduced to simplify the requirements for the `try` execution step below. ``` -F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)^k end) - --> F; catch_m{a_i instr_i*}*{instr''*} (label_m{} val^n instr* end) end - (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)* and - (if k=1 and instr'*=ε then instr''* = nop) - and (if k=1 and inst'*=/=ε then instr''* = instr'*) and (if k=0 then instr''*=ε). +F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)? end) + --> F; catch_m{a_i instr_i*}*{all instr'*}? (label_m{} val^n instr* end) end + (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)*) -catch_m{a_i instr_i*}*{instr'*} val^m end --> val^m +catch_m{a_i instr_i*}*{all instr'*}? val^m end --> val^m -S; F; catch_m{a_i instr_i*}*{instr'*} T[val^n (throw a)] end +S; F; catch_m{a_i instr_i*}*{all instr'*}? T[val^n (throw a)] end --> S; F; caught_m{a val^n} val^n instr_i* end - (iff S_exn(a) = {type [t^n]->[]} and a_i = a) + (iff S_exn(a) = {type [t^n]->[]} and i is the least such that a_i = a) -S; F; catch_m{a_i instr_i*}*{instr*} T[val^n (throw a)] end +S; F; catch_m{a_i instr_i*}*{all instr*} T[val^n (throw a)] end --> S; F; caught_m{a val^n} instr* end - (iff S_exn(a) = {type [t^n]->[]} and instr =/= ε and for every i, a_i =/= a) + (iff S_exn(a) = {type [t^n]->[]} and for every i, a_i =/= a) -S; F; catch_m{a_i instr_i*}*{ε} T[val^n (throw a)] end +S; F; catch_m{a_i instr_i*}* T[val^n (throw a)] end --> S; F; val^n (throw a) (iff for every i, a_i =/= a) + val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end (iff bt = [t^n] -> [t^m]) -catch_m{a_i instr_i*}*{instr*} (label_m{} B^l[ delegate{l} (T[val^n (throw a)]) end ] end) end - --> catch_m{a_i instr_i*}*{instr*} label_m{} val^n (throw a) end end +catch_m{a_i instr_i*}*{instr*}? (label_m{} B^l[ delegate{l} (T[val^n (throw a)]) end ] end) end + --> catch_m{a_i instr_i*}*{instr*}? label_m{} val^n (throw a) end end try bt instr* unwind instr'* end --> try bt instr* catch_all instr'* rethrow 0 end From 51c360b2e2254e29bb3075f184449d9cb0506ee6 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 26 Nov 2020 18:00:30 +0100 Subject: [PATCH 04/24] Removes auxiliary type for labels and allows delegate to reference any label. --- .../Exceptions-formal-overview.md | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 8d57d86e..ca89e5f3 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -38,13 +38,13 @@ mod ::= module ... exn* ## Validation (Typing) -To verify that a `try...delegate l` instruction refers to a label introduced by a try block (I'll call this a try-label), introduce a type attribute to labels in the validation context, which type attribute is set to `try` when the label is a try-label. The original notation `label [t*]` will then be a shortcut for `label {result [t*], type ε}`. - To verify that the `rethrow l` instruction refers to a surrounding catch block, we introduce a stack `caught` to validation contexts, which gets an exception index or the keywork `all` prepended whenever we enter instructions inside a `catch exnidx` or `catch_all` block, respectively. This addition is reflected in the execution rules, by the administrative instruction `caught` which models the stack of caught exceptions on the wasm stack. + ### Instructions + ``` C_exn(x) = [t*] -> [] -------------------------------- @@ -57,7 +57,7 @@ C |- rethrow l : [t1*] -> [t2*] bt = [t1*] -> [t2*] -C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*] +C, label [t2*] |- instr* : [t1*] -> [t2*] (C_exn(x_i) = [t'_i*] -> [])^n (C, label [t2*], caught x_i |- instr_i* : [t'_i*] -> [t2*])^n (C, label [t2*], caught all |- instr'* : [] -> [t2*])? @@ -66,16 +66,16 @@ try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)? end : bt bt = [t1*] -> [t2*] -C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*] -C_label(l).type = try ------------------------------------------------------------- +C, label [t2*] |- instr* : [t1*] -> [t2*] +C_label(l) =/= ε +----------------------------------------- try bt instr* delegate l : bt bt = [t1*] -> [t2*] -C, label {result [t2*], type try} |- instr_1* : [t1*] -> [t2*] +C, label [t2*] |- instr_1* : [t1*] -> [t2*] C, label [t2*], caught all |- instr_2* : [] -> [t2*] --------------------------------------------------------------- +---------------------------------------------------- try bt instr_1* unwind instr_2* : bt ``` @@ -158,8 +158,8 @@ S; F; catch_m{a_i instr_i*}* T[val^n (throw a)] end val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end (iff bt = [t^n] -> [t^m]) -catch_m{a_i instr_i*}*{instr*}? (label_m{} B^l[ delegate{l} (T[val^n (throw a)]) end ] end) end - --> catch_m{a_i instr_i*}*{instr*}? label_m{} val^n (throw a) end end +B^l[ delegate{l} (T[val^n (throw a)]) end ] end + --> val^n (throw a) try bt instr* unwind instr'* end --> try bt instr* catch_all instr'* rethrow 0 end From 5a988d527e638c5f4b270c7e61393cf80000b082 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 16 Dec 2020 22:58:32 +0100 Subject: [PATCH 05/24] Revert making catchless `try`s possible, keeping the simpler execution rules for try. The execution rules don't need to refer to "catchful" trys, checking during validation suffices. --- .../exception-handling/Exceptions-formal-overview.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index ca89e5f3..5742400b 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -16,7 +16,8 @@ exntype ::= [t*] -> [] ``` instr ::= ... | throw x | rethrow l - | try bt instr* (catch x instr*)* (catch_all instr*)? end + | try bt instr* (catch x instr*)+ end + | try bt instr* (catch x instr*)* catch_all instr* end | try bt instr* delegate l | try bt instr* unwind instr* end ``` @@ -60,9 +61,10 @@ bt = [t1*] -> [t2*] C, label [t2*] |- instr* : [t1*] -> [t2*] (C_exn(x_i) = [t'_i*] -> [])^n (C, label [t2*], caught x_i |- instr_i* : [t'_i*] -> [t2*])^n -(C, label [t2*], caught all |- instr'* : [] -> [t2*])? +(C, label [t2*], caught all |- instr'* : [] -> [t2*])^k +(k=0 and n>0) or (k=1 and n≥0) ------------------------------------------------------------------ -try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)? end : bt +try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)^k end : bt bt = [t1*] -> [t2*] From aafc4b11f60dca389575a5ae1982e26f968b847c Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 17 Feb 2021 22:33:41 +0100 Subject: [PATCH 06/24] Apply suggestions from code review Co-authored-by: Heejin Ahn Co-authored-by: Ross Tate --- proposals/exception-handling/Exceptions-formal-overview.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 5742400b..fcf0b8de 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -39,7 +39,7 @@ mod ::= module ... exn* ## Validation (Typing) -To verify that the `rethrow l` instruction refers to a surrounding catch block, we introduce a stack `caught` to validation contexts, which gets an exception index or the keywork `all` prepended whenever we enter instructions inside a `catch exnidx` or `catch_all` block, respectively. This addition is reflected in the execution rules, by the administrative instruction `caught` which models the stack of caught exceptions on the wasm stack. +To verify that the `rethrow l` instruction refers to a surrounding catch block, we introduce a stack `caught` to validation contexts, which gets an exception index or the keyword `all` prepended whenever we enter instructions inside a `catch exnidx` or `catch_all` block, respectively. This addition is reflected in the execution rules, by the administrative instruction `caught` which models the stack of caught exceptions on the wasm stack. ### Instructions @@ -76,9 +76,9 @@ try bt instr* delegate l : bt bt = [t1*] -> [t2*] C, label [t2*] |- instr_1* : [t1*] -> [t2*] -C, label [t2*], caught all |- instr_2* : [] -> [t2*] +C, label [t2*] |- instr_2* : [] -> [] ---------------------------------------------------- -try bt instr_1* unwind instr_2* : bt +try bt instr_1* unwind instr_2* end : bt ``` ## Execution (Reduction) From 4bb9f844cb43162ef484c8967cd8fda22822dfd7 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Fri, 19 Feb 2021 23:11:52 +0100 Subject: [PATCH 07/24] Updated validation rules to match latest semantics of #137 As of commit 275c449e9063c1d3d02bbbffda4b9ab1f8869a68 - `rethrow` is as in the first proposal. - Labels do get a new attribute `kind` which is set to `try` or `catch' for labels surrounding instructions which start with `try` or `catch` respectively, and empty otherwise. This is used to validate `delegate` and `rethrow`/`unwind` respectively. - `unwind` can no longer be a target of `rethrow`'s immediate - The `Caught` stack is removed. I also added a file with Wasm code examples from comments (referenced), and what they reduce to according to these semantics. The first example is the only one with a full reduction, and it uses all new instructions, so it's hopefully easy to get an idea of how this works, even for readers without much formal spec involvement. --- .../Exceptions-formal-examples.md | 239 ++++++++++++++++++ .../Exceptions-formal-overview.md | 71 +++--- 2 files changed, 274 insertions(+), 36 deletions(-) create mode 100644 proposals/exception-handling/Exceptions-formal-examples.md diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md new file mode 100644 index 00000000..03b49499 --- /dev/null +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -0,0 +1,239 @@ +# 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". + +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. Some times/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 index, then `a_x` denotes its exception tag, i.e., `F_exn(x) = a_x`, where `F` is the current frame. + +## example 0 + +The only example with an almost full reduction trace, and all new instructions (`rethrow` is hidden in `unwind`'s reduct). The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. + +``` +(func (result i32) (local i32) + try + try + try + throw x + unwind + i32.const 27 + local.set 0 + end + delegate 0 + catch x + local.get 0 + end) +``` + +Take the frame `F = (locals i32.const 0, module m)`. We have: + +``` +↪ ↪ ↪ F; catch_1{a_x local.get 0} (label_1{} + (delegate{0} (label_0{} + (catch_0{all i32.const 27 local.set 0 rethrow 0} (label_0{} ;; the try-unwind + throw a_x end) end) end) end) end) end + +``` + +For the throw context `T = label_0{}[_]end` the above is the same as + +``` +F; catch_1{a_x local.get 0} (label_1{} + (delegate{0} (label_0{} + (catch_0{all i32.const 27 local.set 0 rethrow 0} + T[throw a_x] end) end) end) end) end + +↪ F; catch_1{a_x local.get 0} (label_1{} + (delegate{0} (label_0{} + (caught{a_x} (label_0{} i32.const 27 local.set 0 rethrow 0 + end) end) end) end) end) end +``` + +Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^1 = label_0{} [_] end`. + +``` +↪ F'; catch_1{a_x local.get 0} (label_1{} + (delegate{0} (label_0{} + (caught{a_x} B^1 [rethrow 0] end) end) end) end) end + +↪ F'; catch_1{a_x local.get 0} (label_1{} + (delegate{0} (label_0{} + (caught{a_x} B^1 [throw a_x] end) end) end) end) end +``` + +Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`. + +``` +↪ F'; catch_1{a_x local.get 0} (label_1{} throw a_x end) end + +↪ F'; caught_1{a_x} (label_1{} local.get 0 end) end + +↪ ↪ ↪ i32.const 27 +``` + +## behaviour of `rethrow` + +### example 1 + +Interaction of `rethrow` with `unwind`. Taken from [this comment](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-705586912) by @rossberg. + +``` +try + throw x +catch x + try + instr1* + rethrow 0 + unwind + instr2* + end +end +``` + +Reduces to + +``` +caught_0{a_x} (label_0 {} (caught_0{a_x} (label_0 {} instr2* throw a_x end) end) end) end +``` + +which in turn reduces to `throw a_x`. + +Note that any global state changes due to `instr1*` or `instr2*` will take place. + +### 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) + +``` +try $label0 + rethrow $label0 ;; cannot be done, because it's not within catch below +catch +end +``` + +This is a validation error (no catch block at given rethrow depth). + +## target of `delegate`'s immediate (label depth) + +@aheejin gave the following +[examples in this comment](https://github.com/WebAssembly/exception-handling/pull/143#discussion_r522673735) + +### example 3 + +`delegate` inside a catch is a validation error. + +``` +try $label0 +catch + try + ... + delegate $label0 ;; cannot be done, because $label0's catch is not below but above here +end +``` + +This is a validation error because `delegate`'s `$label0` refers to the catch-label `label { result ε, type catch}`, not to a try-label. + +### example 4 + +`delegate` correctly targetting a `try-delegate` and a `try-catch`. + +``` +try $label1 + try $label0 + try + throw x + delegate $label0 + delegate $label1 +catch x + instr* +end +``` + +The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to + +``` +caught_0{a_x} (label_0 {} instr* end) end +``` + + +## interaction of `delegate` and `unwind` + +Two examples from issue #130. + +### example 5 + +The [opening example](https://github.com/WebAssembly/exception-handling/issues/130#issue-713113953) +of issue #130. + +``` +i32.const 11 +global.set 0 +try $l + try + try + throw x + delegate 1 + unwind + i32.const 27 + global.set 0 + end +catch_all +end +global.get 0 +``` + +Here, `delegate 1` targets the label `$l` (so it would be the same if we wrote `delegate $l` instead). + +This example returns `11`, because `delegate` skips everything up to and not including `try $l`. + +### example 6 + +This example +[appears to keep](https://github.com/WebAssembly/exception-handling/issues/130#issuecomment-704249682) +the issue #130 open. + +@RossTate expressed concerns with respect to an example possibly equivalent to +the one below. "Possibly", because the original example in the comment refers to +an `unwinding` branch, first presented in issue #124, so I attempted to rewrite +the example to match the current syntax as best I could. + +``` +try $t + try $l + try $u + try + throw x + delegate $t + unwind + instr1* + end + catch x + instr2* + end + instr3* +catch_all + instr4* +end +``` + +The thrown exception tag `a_x` is delegated to the outer `try $l - catch_all`, ignoring the `try $u - unwind` and `try - catch x` in between. So this example reduces to + +``` +caught_0{a_x} (label_0{} instr4* end) end +``` + +During the above reduction, `instr1*`, `instr2*`, and `instr3*` are never executed. + + diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index fcf0b8de..9e7f07c2 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -39,46 +39,52 @@ mod ::= module ... exn* ## Validation (Typing) -To verify that the `rethrow l` instruction refers to a surrounding catch block, we introduce a stack `caught` to validation contexts, which gets an exception index or the keyword `all` prepended whenever we enter instructions inside a `catch exnidx` or `catch_all` block, respectively. This addition is reflected in the execution rules, by the administrative instruction `caught` which models the stack of caught exceptions on the wasm stack. +To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. -### Instructions +Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the catching try-block. + +The original notation `label [t*]` is now a shortcut for `label {result [t*], kind ε}`. +### Instructions + ``` C_exn(x) = [t*] -> [] -------------------------------- -C |- throw x : [t1* t*] -> [t2*] +C ⊢ throw x : [t1* t*] -> [t2*] -C_caught(l) =/= ε +C_label(l) =/= ε +C_label(l).kind = catch ------------------------------- -C |- rethrow l : [t1*] -> [t2*] +C ⊢ rethrow l : [t1*] -> [t2*] bt = [t1*] -> [t2*] -C, label [t2*] |- instr* : [t1*] -> [t2*] +C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] (C_exn(x_i) = [t'_i*] -> [])^n -(C, label [t2*], caught x_i |- instr_i* : [t'_i*] -> [t2*])^n -(C, label [t2*], caught all |- instr'* : [] -> [t2*])^k +(C, label { result [t2*], kind catch } ⊢ instr_i* : [t'_i*] -> [t2*])^n +(C, label { result [t2*], kind catch } ⊢ instr'* : [] -> [t2*])^k (k=0 and n>0) or (k=1 and n≥0) ------------------------------------------------------------------ -try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)^k end : bt +C ⊢ try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)^k end : bt bt = [t1*] -> [t2*] -C, label [t2*] |- instr* : [t1*] -> [t2*] +C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] C_label(l) =/= ε ------------------------------------------ -try bt instr* delegate l : bt +C_label(l).kind = try +------------------------------------------------------------ +C ⊢ try bt instr* delegate l : bt bt = [t1*] -> [t2*] -C, label [t2*] |- instr_1* : [t1*] -> [t2*] -C, label [t2*] |- instr_2* : [] -> [] ----------------------------------------------------- -try bt instr_1* unwind instr_2* end : bt +C, label {result [t2*], kind try} ⊢ instr_1* : [t1*] -> [t2*] +C, label [t2*] ⊢ instr_2* : [] -> [] +-------------------------------------------------------------- +C ⊢ try bt instr_1* unwind instr_2* end : bt ``` ## Execution (Reduction) @@ -110,59 +116,52 @@ instr ::= ... | throw a | catch_n{a instr*}*{instr*}? instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` -Caught exceptions stack - -``` -C^0 ::= val^m [_] instr -C^{n+1} ::= caught{exnaddr val^k} C^n end -``` - Throw Contexts ``` -T ::= v* [_] e* | label_n{e*} T end | caught_m{a val^n} T end | frame_n{F} T end +T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end | frame_n{F} T end ``` ### Instructions ``` -F; throw x --> F; throw a (iff F_exn(x) = a) +F; throw x ↪ F; throw a (iff F_exn(x) = a) -caught_m{a val^n} C^l[rethrow l] end - --> caught_m{a val^n} C^l[val^n (throw a)] end +caught_m{a val^n} B^{l+1}[rethrow l] end + ↪ caught_m{a val^n} B^{l+1}[val^n (throw a)] end -caught_m{a val^n} val^m end --> val^m +caught_m{a val^n} val^m end ↪ val^m ``` A keyword `all` is introduced to simplify the requirements for the `try` execution step below. ``` F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)? end) - --> F; catch_m{a_i instr_i*}*{all instr'*}? (label_m{} val^n instr* end) end + ↪ F; catch_m{a_i instr_i*}*{all instr'*}? (label_m{} val^n instr* end) end (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)*) -catch_m{a_i instr_i*}*{all instr'*}? val^m end --> val^m +catch_m{a_i instr_i*}*{all instr'*}? val^m end ↪ val^m S; F; catch_m{a_i instr_i*}*{all instr'*}? T[val^n (throw a)] end - --> S; F; caught_m{a val^n} val^n instr_i* end + ↪ S; F; caught_m{a val^n} (label_m{} val^n instr_i* end) end (iff S_exn(a) = {type [t^n]->[]} and i is the least such that a_i = a) S; F; catch_m{a_i instr_i*}*{all instr*} T[val^n (throw a)] end - --> S; F; caught_m{a val^n} instr* end + ↪ S; F; caught_m{a val^n} (label_m instr* end) end (iff S_exn(a) = {type [t^n]->[]} and for every i, a_i =/= a) S; F; catch_m{a_i instr_i*}* T[val^n (throw a)] end - --> S; F; val^n (throw a) + ↪ S; F; val^n (throw a) (iff for every i, a_i =/= a) -val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end +val^n (try bt instr* delegate l) ↪ delegate{l} (label_m{} val^n instr* end) end (iff bt = [t^n] -> [t^m]) B^l[ delegate{l} (T[val^n (throw a)]) end ] end - --> val^n (throw a) + ↪ val^n (throw a) -try bt instr* unwind instr'* end --> try bt instr* catch_all instr'* rethrow 0 end +try bt instr* unwind instr'* end ↪ try bt instr* catch_all instr'* rethrow 0 end ``` From 1afd21afdb835156c5129a5e1f7cc7a7f4b03bb0 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Fri, 19 Feb 2021 23:42:00 +0100 Subject: [PATCH 08/24] Added forgotten reduction step and comment for example 1 --- proposals/exception-handling/Exceptions-formal-examples.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 03b49499..8b17e3bb 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -73,6 +73,9 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^1 = label_0{ Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`. ``` +↪ F'; catch_1{a_x local.get 0} (label_1{} + (delegate{0} T'[throw a_x] end) end) end + ↪ F'; catch_1{a_x local.get 0} (label_1{} throw a_x end) end ↪ F'; caught_1{a_x} (label_1{} local.get 0 end) end @@ -99,7 +102,7 @@ catch x end ``` -Reduces to +Assuming `instr1*` and `instr2*` don't throw another exception, this example reduces to ``` caught_0{a_x} (label_0 {} (caught_0{a_x} (label_0 {} instr2* throw a_x end) end) end) end From 4ff1c38cb851c6ec53c98774902f635fe1d0bef1 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 24 Feb 2021 01:49:26 +0100 Subject: [PATCH 09/24] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- .../Exceptions-formal-overview.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 9e7f07c2..0ca61f5f 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -106,7 +106,7 @@ exninst ::= {type exntype} Module Instances ``` -m ::= {..., (exn a)*} +m ::= {..., exn a*} ``` Administrative Instructions @@ -143,17 +143,16 @@ F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)? end) catch_m{a_i instr_i*}*{all instr'*}? val^m end ↪ val^m -S; F; catch_m{a_i instr_i*}*{all instr'*}? T[val^n (throw a)] end - ↪ S; F; caught_m{a val^n} (label_m{} val^n instr_i* end) end - (iff S_exn(a) = {type [t^n]->[]} and i is the least such that a_i = a) +S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ S; F; caught_m{a val^n} (label_m{} val^n instr* end) end + (iff (a1? = eps \/ a1? = a) /\ S_exn(a) = {type [t^n]->[]}) -S; F; catch_m{a_i instr_i*}*{all instr*} T[val^n (throw a)] end - ↪ S; F; caught_m{a val^n} (label_m instr* end) end - (iff S_exn(a) = {type [t^n]->[]} and for every i, a_i =/= a) +S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end + (iff a1? =/= eps /\ a1? =/= a) -S; F; catch_m{a_i instr_i*}* T[val^n (throw a)] end +S; F; catch_m T[val^n (throw a)] end ↪ S; F; val^n (throw a) - (iff for every i, a_i =/= a) val^n (try bt instr* delegate l) ↪ delegate{l} (label_m{} val^n instr* end) end From fbe87b00109a0d1f19d01f4ac0fe9218e27e0312 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 24 Feb 2021 14:48:26 +0100 Subject: [PATCH 10/24] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- proposals/exception-handling/Exceptions-formal-overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 0ca61f5f..a23e1a9c 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -141,7 +141,7 @@ F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)? end) ↪ F; catch_m{a_i instr_i*}*{all instr'*}? (label_m{} val^n instr* end) end (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)*) -catch_m{a_i instr_i*}*{all instr'*}? val^m end ↪ val^m +catch_m{a? instr*}* val^m end ↪ val^m S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; caught_m{a val^n} (label_m{} val^n instr* end) end From fa5a237e0994995eb3f444207f383c7101a0c8d5 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Wed, 24 Feb 2021 14:59:15 +0100 Subject: [PATCH 11/24] Applied comments from @rossberg 's review and some typesetting. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In particular: - Removed superfluous C_label(l) =/= ε. - Made try-catch and catch_m syntax compact in other places of the text as well and adjusted the reduction of example 0. - Adjusted some typesetting and wording. --- .../Exceptions-formal-examples.md | 12 +++--- .../Exceptions-formal-overview.md | 40 ++++++++++--------- 2 files changed, 28 insertions(+), 24 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 8b17e3bb..a1daf1c2 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -16,7 +16,7 @@ If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F_exn ## example 0 -The only example with an almost full reduction trace, and all new instructions (`rethrow` is hidden in `unwind`'s reduct). The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. +The only example with an almost full reduction trace, and all new instructions (`rethrow` and `catch_all` are hidden in `unwind`'s reduct). The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. ``` (func (result i32) (local i32) @@ -39,7 +39,7 @@ Take the frame `F = (locals i32.const 0, module m)`. We have: ``` ↪ ↪ ↪ F; catch_1{a_x local.get 0} (label_1{} (delegate{0} (label_0{} - (catch_0{all i32.const 27 local.set 0 rethrow 0} (label_0{} ;; the try-unwind + (catch_0{i32.const 27 local.set 0 rethrow 0} (label_0{} ;; the try-unwind throw a_x end) end) end) end) end) end ``` @@ -49,7 +49,7 @@ For the throw context `T = label_0{}[_]end` the above is the same as ``` F; catch_1{a_x local.get 0} (label_1{} (delegate{0} (label_0{} - (catch_0{all i32.const 27 local.set 0 rethrow 0} + (catch_0{i32.const 27 local.set 0 rethrow 0} T[throw a_x] end) end) end) end) end ↪ F; catch_1{a_x local.get 0} (label_1{} @@ -105,7 +105,9 @@ end Assuming `instr1*` and `instr2*` don't throw another exception, this example reduces to ``` -caught_0{a_x} (label_0 {} (caught_0{a_x} (label_0 {} instr2* throw a_x end) end) end) end +caught_0{a_x} (label_0 {} + (caught_0{a_x} (label_0 {} + instr2* throw a_x end) end) end) end ``` which in turn reduces to `throw a_x`. @@ -135,7 +137,7 @@ This is a validation error (no catch block at given rethrow depth). ### example 3 -`delegate` inside a catch is a validation error. +`delegate` targetting a catch is a validation error. ``` try $label0 diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index a23e1a9c..f9f3033d 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -44,7 +44,7 @@ To verify that a `try...delegate l` instruction refers to a label surrounding th Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the catching try-block. -The original notation `label [t*]` is now a shortcut for `label {result [t*], kind ε}`. +The original notation `label [t*]` is now an abbreviation for `label {result [t*], kind ε}`. ### Instructions @@ -56,7 +56,6 @@ C_exn(x) = [t*] -> [] C ⊢ throw x : [t1* t*] -> [t2*] -C_label(l) =/= ε C_label(l).kind = catch ------------------------------- C ⊢ rethrow l : [t1*] -> [t2*] @@ -64,17 +63,15 @@ C ⊢ rethrow l : [t1*] -> [t2*] bt = [t1*] -> [t2*] C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] -(C_exn(x_i) = [t'_i*] -> [])^n -(C, label { result [t2*], kind catch } ⊢ instr_i* : [t'_i*] -> [t2*])^n -(C, label { result [t2*], kind catch } ⊢ instr'* : [] -> [t2*])^k -(k=0 and n>0) or (k=1 and n≥0) ------------------------------------------------------------------- -C ⊢ try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)^k end : bt +(C_exn(x) = [t*] -> [])* +(C, label { result [t2*], kind catch } ⊢ instr* : [t1*] -> [t2*])* +(C, label { result [t2*], kind catch } ⊢ instr'* : [] -> [t2*])? +----------------------------------------------------------------------- +C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : bt bt = [t1*] -> [t2*] C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] -C_label(l) =/= ε C_label(l).kind = try ------------------------------------------------------------ C ⊢ try bt instr* delegate l : bt @@ -112,14 +109,15 @@ m ::= {..., exn a*} Administrative Instructions ``` -instr ::= ... | throw a | catch_n{a instr*}*{instr*}? instr* end +instr ::= ... | throw a | catch_n{a? instr*}* instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` Throw Contexts ``` -T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end | frame_n{F} T end +T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end + | frame_n{F} T end ``` ### Instructions @@ -134,33 +132,37 @@ caught_m{a val^n} B^{l+1}[rethrow l] end caught_m{a val^n} val^m end ↪ val^m ``` -A keyword `all` is introduced to simplify the requirements for the `try` execution step below. +A missing exception address in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. ``` -F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)? end) - ↪ F; catch_m{a_i instr_i*}*{all instr'*}? (label_m{} val^n instr* end) end - (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)*) +F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) + ↪ F; catch_m{a instr'*}*{instr''*}? (label_m{} val^n instr* end) end + (iff bt = [t1^n] -> [t2^m] ∧ (F_exn(x) = a)*) catch_m{a? instr*}* val^m end ↪ val^m S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; caught_m{a val^n} (label_m{} val^n instr* end) end - (iff (a1? = eps \/ a1? = a) /\ S_exn(a) = {type [t^n]->[]}) + (iff (a1? = ε ∨ a1? = a) ∧ S_exn(a) = {type [t^n]->[]}) S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end - (iff a1? =/= eps /\ a1? =/= a) + (iff a1? ≠ ε ∧ a1? ≠ a) S; F; catch_m T[val^n (throw a)] end ↪ S; F; val^n (throw a) -val^n (try bt instr* delegate l) ↪ delegate{l} (label_m{} val^n instr* end) end +val^n (try bt instr* delegate l) + ↪ delegate{l} (label_m{} val^n instr* end) end (iff bt = [t^n] -> [t^m]) +delegate{l} val^n end ↪ val^n + B^l[ delegate{l} (T[val^n (throw a)]) end ] end ↪ val^n (throw a) -try bt instr* unwind instr'* end ↪ try bt instr* catch_all instr'* rethrow 0 end +try bt instr* unwind instr'* end + ↪ try bt instr* catch_all instr'* rethrow 0 end ``` From 83872edafa848090084f7bffcda3637d976e1df2 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 12 Mar 2021 22:41:01 +0100 Subject: [PATCH 12/24] Adds typing rules for the administrative instructions and fixes rules to ensure type preservation. (Also minor fixes in premises, and did some typesetting, couldn't look at the ->s any more) These typing rules preserve types, because the manipulated labels (e.g. during `kind`-change) are included in the conclusions of such type rules. So for example one could see - `caught_m{...} (label_m {} ... end) end` as the catch-label (holding the caught exception), - `catch_m{}*label_m{} ... end end` as a try-label (holding all its handlers), and - `delegate{l} (label_m{} instr* end) end` as a try-label holding the destination (depth) to another try-label. --- .../Exceptions-formal-overview.md | 110 ++++++++++++------ 1 file changed, 76 insertions(+), 34 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index f9f3033d..cea8c364 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -9,7 +9,7 @@ This is an overview of the 3rd proposal's formal spec additions, to aid in discu Exception Types ``` -exntype ::= [t*] -> [] +exntype ::= [t*]→[] ``` ### Instructions @@ -39,49 +39,54 @@ mod ::= module ... exn* ## Validation (Typing) +#### Modification to labels To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the catching try-block. -The original notation `label [t*]` is now an abbreviation for `label {result [t*], kind ε}`. +The original notation `label [t*]` is now an abbreviation for: + +```` +label {result [t*], kind ε} +``` ### Instructions ``` -C_exn(x) = [t*] -> [] --------------------------------- -C ⊢ throw x : [t1* t*] -> [t2*] +C.exns(x) = [t*]→[] +----------------------------- +C ⊢ throw x : [t1* t*]→[t2*] -C_label(l).kind = catch -------------------------------- -C ⊢ rethrow l : [t1*] -> [t2*] +C.labels(l).kind = catch +---------------------------- +C ⊢ rethrow l : [t1*]→[t2*] -bt = [t1*] -> [t2*] -C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] -(C_exn(x) = [t*] -> [])* -(C, label { result [t2*], kind catch } ⊢ instr* : [t1*] -> [t2*])* -(C, label { result [t2*], kind catch } ⊢ instr'* : [] -> [t2*])? ------------------------------------------------------------------------ -C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : bt +C.types(bt) = [t1*]→[t2*] +C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] +(C.exns(x) = [t*]→[] ∧ + C, labels { result [t2*], kind catch } ⊢ instr* : [t*]→[t2*])* +(C, labels { result [t2*], kind catch } ⊢ instr'* : []→[t2*])? +----------------------------------------------------------------------------- +C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] -bt = [t1*] -> [t2*] -C, label {result [t2*], kind try} ⊢ instr* : [t1*] -> [t2*] -C_label(l).kind = try ------------------------------------------------------------- -C ⊢ try bt instr* delegate l : bt +C.types(bt) = [t1*]→[t2*] +C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] +C.labels(l).kind = try +---------------------------------------------------------- +C ⊢ try bt instr* delegate l : [t1*]→[t2*] -bt = [t1*] -> [t2*] -C, label {result [t2*], kind try} ⊢ instr_1* : [t1*] -> [t2*] -C, label [t2*] ⊢ instr_2* : [] -> [] --------------------------------------------------------------- -C ⊢ try bt instr_1* unwind instr_2* end : bt +C.types(bt) = [t1*]→[t2*] +C, labels {result [t2*], kind try} ⊢ instr1* : [t1*]→[t2*] +C, labels [t2*] ⊢ instr2* : []→[] +----------------------------------------------------------- +C ⊢ try bt instr1* unwind instr2* end : [t1*]→[t2*] ``` ## Execution (Reduction) @@ -91,7 +96,7 @@ C ⊢ try bt instr_1* unwind instr_2* end : bt Stores ``` -S ::= {..., exn exninst*} +S ::= {..., exns exninst*} ``` Exception Instances @@ -103,7 +108,7 @@ exninst ::= {type exntype} Module Instances ``` -m ::= {..., exn a*} +m ::= {..., exns a*} ``` Administrative Instructions @@ -124,7 +129,7 @@ T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end ``` -F; throw x ↪ F; throw a (iff F_exn(x) = a) +F; throw x ↪ F; throw a (if F.module.exnaddrs[x]=a) caught_m{a val^n} B^{l+1}[rethrow l] end ↪ caught_m{a val^n} B^{l+1}[val^n (throw a)] end @@ -137,13 +142,17 @@ A missing exception address in a `catch_m` clause (i.e., `a? = ε`) represents a ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) ↪ F; catch_m{a instr'*}*{instr''*}? (label_m{} val^n instr* end) end - (iff bt = [t1^n] -> [t2^m] ∧ (F_exn(x) = a)*) + (iff bt = [t1^n]→[t2^m] ∧ (val:t1)^n ∧ (F.module.exnaddrs[x]=a)*) catch_m{a? instr*}* val^m end ↪ val^m +``` -S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end - ↪ S; F; caught_m{a val^n} (label_m{} val^n instr* end) end - (iff (a1? = ε ∨ a1? = a) ∧ S_exn(a) = {type [t^n]->[]}) +In the below reduction, a try-label is replaced by a catch label (see comment in the end of this file). + +``` +S; F; catch_m{a1? instr*}{a'? instr'*}* (label_m T[val^n (throw a)] end) end + ↪ S; F; caught_m{a val^n} (label_m{} (val^n)? instr* end) end + (iff (a1? = ε ∨ a1? = a) ∧ S.exceptions(a).type = [t^n]→[]) S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end @@ -155,14 +164,47 @@ S; F; catch_m T[val^n (throw a)] end val^n (try bt instr* delegate l) ↪ delegate{l} (label_m{} val^n instr* end) end - (iff bt = [t^n] -> [t^m]) + (iff bt = [t^n]→[t^m]) delegate{l} val^n end ↪ val^n -B^l[ delegate{l} (T[val^n (throw a)]) end ] end +B^l[ delegate{l} T[val^n (throw a)] end ] end ↪ val^n (throw a) try bt instr* unwind instr'* end ↪ try bt instr* catch_all instr'* rethrow 0 end ``` + +### Typing rules for administrative instructions + +``` +S.exceptions(a).type = [t*]→[] +------------------------------- +S;C ⊢ throw a : [t1* t*]→[t2*] + +(S.exceptions(a).type = [t'*]→[] ∧ + S;C, labels {result [t*], kind catch} ⊢ instr1* : [t'*]→[t*])* +(S;C, labels {result [t*], kind catch} ⊢ instr2* : []→[t*])? +S;C, labels {result [t*], kind try} ⊢ instr3* : []→[t*] +--------------------------------------------------------------------------- +S;C ⊢ catch_n{a instr1*}*{instr2*}? (label_n {} instr3* end) end : []→[t*] + +S;C, label {result [t*], kind try} ⊢ instr* : []→[t*] +C_label(l).kind = try +------------------------------------------------------- +S;C ⊢ delegate{l} (label_m{} instr* end) end : []→[t*] + +S.exceptions(a).type = [t*]→[] +(val:t)* +S;C, labels {result [t'*], kind catch} ⊢ instr* : []→[t'*] +--------------------------------------------------------------- [T-caught-adm] +S;C ⊢ caught_m{a val^n} (label_m{} instr* end) end : []→[t'*] +``` + +The above typing rules preserve types, because the manipulated labels (e.g. during `kind`-change) +are included in the conclusions of such type rules. So for example one could see + +- `caught_m{...} (label_m {} ... end) end` as the catch-label (holding the caught exception), +- `catch_m{}*label_m{} ... end end` as a try-label (holding all its handlers), and +- `delegate{l} (label_m{} instr* end) end` as a try-label holding the destination (depth) to another try-label. From 4552306e6b8cae5627ae1e202b0956439b3d5910 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 8 Jun 2021 13:04:30 +0200 Subject: [PATCH 13/24] Implemented latest review comments and updated. In particular: - The labels surrounding try-catch and try-delegate now get a standard label in the first step, which is then refined to catch-labels and/or try-labels per subblock. + For that I allowed the new administrative instructions to appear nested directly inside a label_n{} in block contexts. + Also added a validation rule to the administrative label_n{}. + Due to this, all block contexts appear now without a successor exponent. - Updated to latest try-catch syntax described in issue #157. - Corrected some previously wrong syntax. - Removed try-unwind (...) as per issue #156 - Updated Exceptions-formal-examples.md similarly. --- .../Exceptions-formal-examples.md | 176 ++++++------------ .../Exceptions-formal-overview.md | 133 ++++++------- 2 files changed, 129 insertions(+), 180 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index a1daf1c2..36c3827e 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -12,11 +12,11 @@ If anyone would like that I add another reduction trace, or other examples, plea ### notation -If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F_exn(x) = a_x`, where `F` is the current frame. +If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F.exception[x] = a_x`, where `F` is the current frame. ## example 0 -The only example with an almost full reduction trace, and all new instructions (`rethrow` and `catch_all` are hidden in `unwind`'s reduct). The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. +The only example with an almost full reduction trace, and all new instructions. The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. ``` (func (result i32) (local i32) @@ -24,9 +24,10 @@ The only example with an almost full reduction trace, and all new instructions ( try try throw x - unwind + catch_all i32.const 27 local.set 0 + rethrow 0 end delegate 0 catch x @@ -37,48 +38,59 @@ The only example with an almost full reduction trace, and all new instructions ( Take the frame `F = (locals i32.const 0, module m)`. We have: ``` -↪ ↪ ↪ F; catch_1{a_x local.get 0} (label_1{} - (delegate{0} (label_0{} - (catch_0{i32.const 27 local.set 0 rethrow 0} (label_0{} ;; the try-unwind +↪ ↪ ↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + (label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0} throw a_x end) end) end) end) end) end - ``` -For the throw context `T = label_0{}[_]end` the above is the same as +For the empty throw context `T = [_]` the above is the same as ``` -F; catch_1{a_x local.get 0} (label_1{} - (delegate{0} (label_0{} - (catch_0{i32.const 27 local.set 0 rethrow 0} +F; label_1{} (catch_1{a_x local.get 0} + label_0{} (delegate{0} + label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0} T[throw a_x] end) end) end) end) end -↪ F; catch_1{a_x local.get 0} (label_1{} - (delegate{0} (label_0{} - (caught{a_x} (label_0{} i32.const 27 local.set 0 rethrow 0 +↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + (label_0{} (caught{a_x} i32.const 27 local.set 0 rethrow 0 end) end) end) end) end) end ``` -Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^1 = label_0{} [_] end`. +Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]`. ``` -↪ F'; catch_1{a_x local.get 0} (label_1{} - (delegate{0} (label_0{} - (caught{a_x} B^1 [rethrow 0] end) end) end) end) end +↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + (label_0{} (caught{a_x} B^0 [rethrow 0] + end) end) end) end) end) end -↪ F'; catch_1{a_x local.get 0} (label_1{} - (delegate{0} (label_0{} - (caught{a_x} B^1 [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{a_x} B^0 [throw a_x] + end) end) end) end) end) end ``` -Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`. +Let `T' = label_0{} (caught{a_x} B^0 [_] end) end`. ``` -↪ F'; catch_1{a_x local.get 0} (label_1{} - (delegate{0} T'[throw a_x] end) end) end +↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + T'[throw a_x] end) end) end) end -↪ F'; catch_1{a_x local.get 0} (label_1{} throw a_x end) end +↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + T'[throw a_x] end) end) end) end -↪ F'; caught_1{a_x} (label_1{} local.get 0 end) end +↪ F; label_1{} (catch_1{a_x local.get 0} + (label_0{} (delegate{0} + T'[throw a_x] end) end) end) end + +↪ 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 ↪ ↪ ↪ i32.const 27 ``` @@ -87,32 +99,38 @@ Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`. ### example 1 -Interaction of `rethrow` with `unwind`. Taken from [this comment](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-705586912) by @rossberg. +Location of a rethrown exception. ``` try + val1 throw x catch x try - instr1* - rethrow 0 - unwind - instr2* + val2 + throw y + catch_all + try + val3 + throw z + catch z + rethrow 2 + end end end ``` -Assuming `instr1*` and `instr2*` don't throw another exception, this example reduces to +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 ``` -caught_0{a_x} (label_0 {} - (caught_0{a_x} (label_0 {} - instr2* throw a_x end) end) end) end +label_0{} caught{a_x val1} + val1 (label_0{} caught{a_y val2} + (label_0{} caught{a_z val3} + val3 val1 (throw a_x) end end) + end end) end end) ``` -which in turn reduces to `throw a_x`. - -Note that any global state changes due to `instr1*` or `instr2*` will take place. +which in this case is the same as `val1 (throw a_x)`. ### example 2 @@ -137,7 +155,7 @@ This is a validation error (no catch block at given rethrow depth). ### example 3 -`delegate` targetting a catch is a validation error. +`delegate` targeting a catch is a validation error. ``` try $label0 @@ -152,93 +170,23 @@ This is a validation error because `delegate`'s `$label0` refers to the catch-la ### example 4 -`delegate` correctly targetting a `try-delegate` and a `try-catch`. +`delegate` correctly targeting a `try-delegate` and a `try-catch`. ``` try $label1 try $label0 try throw x - delegate $label0 - delegate $label1 + delegate $label0 ;; delegate 0 + delegate $label1 ;; delegate 1 catch x instr* end ``` -The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to +The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to the following. ``` -caught_0{a_x} (label_0 {} instr* end) end -``` - - -## interaction of `delegate` and `unwind` - -Two examples from issue #130. - -### example 5 - -The [opening example](https://github.com/WebAssembly/exception-handling/issues/130#issue-713113953) -of issue #130. - -``` -i32.const 11 -global.set 0 -try $l - try - try - throw x - delegate 1 - unwind - i32.const 27 - global.set 0 - end -catch_all -end -global.get 0 +label_0 {} (caught_0{a_x} (label_0 {} instr* end) end ``` -Here, `delegate 1` targets the label `$l` (so it would be the same if we wrote `delegate $l` instead). - -This example returns `11`, because `delegate` skips everything up to and not including `try $l`. - -### example 6 - -This example -[appears to keep](https://github.com/WebAssembly/exception-handling/issues/130#issuecomment-704249682) -the issue #130 open. - -@RossTate expressed concerns with respect to an example possibly equivalent to -the one below. "Possibly", because the original example in the comment refers to -an `unwinding` branch, first presented in issue #124, so I attempted to rewrite -the example to match the current syntax as best I could. - -``` -try $t - try $l - try $u - try - throw x - delegate $t - unwind - instr1* - end - catch x - instr2* - end - instr3* -catch_all - instr4* -end -``` - -The thrown exception tag `a_x` is delegated to the outer `try $l - catch_all`, ignoring the `try $u - unwind` and `try - catch x` in between. So this example reduces to - -``` -caught_0{a_x} (label_0{} instr4* end) end -``` - -During the above reduction, `instr1*`, `instr2*`, and `instr3*` are never executed. - - diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index cea8c364..6478d5de 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -16,10 +16,8 @@ exntype ::= [t*]→[] ``` instr ::= ... | throw x | rethrow l - | try bt instr* (catch x instr*)+ end - | try bt instr* (catch x instr*)* catch_all instr* end + | try bt instr* (catch x instr*)* (catch_all instr*)? end | try bt instr* delegate l - | try bt instr* unwind instr* end ``` ### Modules @@ -27,14 +25,13 @@ instr ::= ... | throw x | rethrow l Exceptions (definitions) ``` -exn ::= export* exception exntype | export* exception exntype import +exception ::= export* exception exntype | export* exception exntype import ``` Modules - ``` -mod ::= module ... exn* +mod ::= module ... exception* ``` ## Validation (Typing) @@ -43,12 +40,12 @@ mod ::= module ... exn* To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. -Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the catching try-block. +Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. -The original notation `label [t*]` is now an abbreviation for: +The original notation `labels [t*]` is now an abbreviation for: -```` -label {result [t*], kind ε} +``` +labels {result [t*], kind ε} ``` @@ -56,37 +53,30 @@ label {result [t*], kind ε} ``` -C.exns(x) = [t*]→[] +C.exceptions[x] = [t*]→[] ----------------------------- C ⊢ throw x : [t1* t*]→[t2*] -C.labels(l).kind = catch +C.labels[l].kind = catch ---------------------------- C ⊢ rethrow l : [t1*]→[t2*] -C.types(bt) = [t1*]→[t2*] +C.types[bt] = [t1*]→[t2*] C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] -(C.exns(x) = [t*]→[] ∧ +(C.exceptions[x] = [t*]→[] ∧ C, labels { result [t2*], kind catch } ⊢ instr* : [t*]→[t2*])* (C, labels { result [t2*], kind catch } ⊢ instr'* : []→[t2*])? ----------------------------------------------------------------------------- -C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] +C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] -C.types(bt) = [t1*]→[t2*] +C.types[bt] = [t1*]→[t2*] C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] -C.labels(l).kind = try +C.labels[l].kind = try ---------------------------------------------------------- C ⊢ try bt instr* delegate l : [t1*]→[t2*] - - -C.types(bt) = [t1*]→[t2*] -C, labels {result [t2*], kind try} ⊢ instr1* : [t1*]→[t2*] -C, labels [t2*] ⊢ instr2* : []→[] ------------------------------------------------------------ -C ⊢ try bt instr1* unwind instr2* end : [t1*]→[t2*] ``` ## Execution (Reduction) @@ -96,7 +86,7 @@ C ⊢ try bt instr1* unwind instr2* end : [t1*]→[t2*] Stores ``` -S ::= {..., exns exninst*} +S ::= {..., exceptions exninst*} ``` Exception Instances @@ -108,7 +98,7 @@ exninst ::= {type exntype} Module Instances ``` -m ::= {..., exns a*} +m ::= {..., exceptions a*} ``` Administrative Instructions @@ -118,6 +108,22 @@ instr ::= ... | throw a | catch_n{a? instr*}* instr* end | delegate{l} instr* end | caught_m{a 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 above 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, mirroring the label kinds of labels in validation contexts. + +``` +label_kind ::= try_label_kind | catch_label_kind +try_label_kind ::= catch_m{a? instr*}* | delegate{l} +catch_label_kind ::= caught_m{a val*} +B^0 ::= val* [_] instr* +B^{k+1} ::= val* label_n{instr*} label_kind? B^k end? end instr* +``` + +Note that `label_n{instr*} label_kind? [_] end? end` could be seen as a simplified control frame. + +(Alternatively, we could have the above `label_kind`s be also labels, remove the additional `label_m` from the execution rules below, and remove the execution rules below where the new administrative instructions only contain `val*`. This would make labels even more similar to control frames.) + Throw Contexts ``` @@ -131,80 +137,75 @@ T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end ``` F; throw x ↪ F; throw a (if F.module.exnaddrs[x]=a) -caught_m{a val^n} B^{l+1}[rethrow l] end - ↪ caught_m{a val^n} B^{l+1}[val^n (throw a)] end +caught_m{a val^n} B^l[rethrow l] end + ↪ caught_m{a val^n} B^l[val^n (throw a)] end caught_m{a val^n} val^m end ↪ val^m ``` -A missing exception address in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. +A missing exception tag (exnaddr) in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) - ↪ F; catch_m{a instr'*}*{instr''*}? (label_m{} val^n instr* end) end - (iff bt = [t1^n]→[t2^m] ∧ (val:t1)^n ∧ (F.module.exnaddrs[x]=a)*) + ↪ F; label_m{} (catch_m{a instr'*}*{instr''*}? val^n instr* end) end + (if bt = [t1^n]→[t2^m] ∧ (val:t1)^n ∧ (F.module.exnaddrs[x]=a)*) catch_m{a? instr*}* val^m end ↪ val^m -``` - -In the below reduction, a try-label is replaced by a catch label (see comment in the end of this file). -``` -S; F; catch_m{a1? instr*}{a'? instr'*}* (label_m T[val^n (throw a)] end) end - ↪ S; F; caught_m{a val^n} (label_m{} (val^n)? instr* end) end - (iff (a1? = ε ∨ a1? = a) ∧ S.exceptions(a).type = [t^n]→[]) +S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ S; F; caught_m{a val^n} (val^n)? instr* end + (if (a1? = ε ∨ a1? = a) ∧ S.exceptions(a).type = [t^n]→[]) S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end - (iff a1? ≠ ε ∧ a1? ≠ a) + (if a1? ≠ ε ∧ a1? ≠ a) S; F; catch_m T[val^n (throw a)] end ↪ S; F; val^n (throw a) val^n (try bt instr* delegate l) - ↪ delegate{l} (label_m{} val^n instr* end) end - (iff bt = [t^n]→[t^m]) + ↪ label_m{} (delegate{l} val^n instr* end) end + (if bt = [t^n]→[t^m]) delegate{l} val^n end ↪ val^n -B^l[ delegate{l} T[val^n (throw a)] end ] end +B^l[ delegate{l} T[val^n (throw a)] end ] ↪ val^n (throw a) - - -try bt instr* unwind instr'* end - ↪ try bt instr* catch_all instr'* rethrow 0 end ``` ### Typing rules for administrative instructions ``` -S.exceptions(a).type = [t*]→[] -------------------------------- -S;C ⊢ throw a : [t1* t*]→[t2*] +S.exceptions[a].type = [t2*]→[] +-------------------------------- +S;C ⊢ throw a : [t1* t2*]→[t*] -(S.exceptions(a).type = [t'*]→[] ∧ +(S.exceptions[a].type = [t'*]→[] ∧ S;C, labels {result [t*], kind catch} ⊢ instr1* : [t'*]→[t*])* (S;C, labels {result [t*], kind catch} ⊢ instr2* : []→[t*])? S;C, labels {result [t*], kind try} ⊢ instr3* : []→[t*] ---------------------------------------------------------------------------- -S;C ⊢ catch_n{a instr1*}*{instr2*}? (label_n {} instr3* end) end : []→[t*] +----------------------------------------------------------------------- +S;C, labels [t*] ⊢ catch_n{a instr1*}*{instr2*}? instr3* end : []→[t*] -S;C, label {result [t*], kind try} ⊢ instr* : []→[t*] -C_label(l).kind = try -------------------------------------------------------- -S;C ⊢ delegate{l} (label_m{} instr* end) end : []→[t*] +S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] +C.labels[l].kind = try +----------------------------------------------------------------------- +S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] -S.exceptions(a).type = [t*]→[] -(val:t)* -S;C, labels {result [t'*], kind catch} ⊢ instr* : []→[t'*] ---------------------------------------------------------------- [T-caught-adm] -S;C ⊢ caught_m{a val^n} (label_m{} instr* end) end : []→[t'*] +S.exceptions[a].type = [t'*]→[] +(val:t')* +S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] +-------------------------------------------------------------------------------- +S;C, labels {result [t*], kind catch} ⊢ caught_m{a val^n} instr* end : []→[t'*] ``` -The above typing rules preserve types, because the manipulated labels (e.g. during `kind`-change) -are included in the conclusions of such type rules. So for example one could see +By adding the attribute `kind` to labels, we are creating situations in the proof of type preservation, where we have a derivation of some `S;C, label [t*] ⊢ instr* : []→[t*]` but we need to have that `S;C, label {result [t*], kind } ⊢ instr* : []→[t*]` for some ` ::= try | catch`. To resolve this we add the following typing rule for labels in the context, which ensures our newly introduced `try` and `catch` blocks can contain any instructions a regular block can. + +``` +S;C, label [t*] ⊢ instr* : []→[t*] +labelkind = try ∨ labelkind = catch +----------------------------------------------------------- +S;C, label {result [t*], kind labelkind} ⊢ instr* : []→[t*] +``` -- `caught_m{...} (label_m {} ... end) end` as the catch-label (holding the caught exception), -- `catch_m{}*label_m{} ... end end` as a try-label (holding all its handlers), and -- `delegate{l} (label_m{} instr* end) end` as a try-label holding the destination (depth) to another try-label. From 8cfa1b64a24fdc2ba629adfcc5b285b0a159fef4 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 25 Jun 2021 16:45:50 +0200 Subject: [PATCH 14/24] Renamed Exceptions to Tags As per #161 --- .../Exceptions-formal-examples.md | 2 +- .../Exceptions-formal-overview.md | 34 +++++++++---------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 36c3827e..cefad0a6 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -12,7 +12,7 @@ If anyone would like that I add another reduction trace, or other examples, plea ### notation -If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F.exception[x] = a_x`, where `F` is the current frame. +If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `F.exception[x] = a_x`, where `F` is the current frame. ## example 0 diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 6478d5de..20d3f117 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -6,10 +6,10 @@ This is an overview of the 3rd proposal's formal spec additions, to aid in discu ### Types -Exception Types +Tag Types ``` -exntype ::= [t*]→[] +tagtype ::= [t*]→[] ``` ### Instructions @@ -22,16 +22,16 @@ instr ::= ... | throw x | rethrow l ### Modules -Exceptions (definitions) +Tags ``` -exception ::= export* exception exntype | export* exception exntype import +tag ::= export* tag exntype | export* tag tagtype import ``` Modules ``` -mod ::= module ... exception* +mod ::= module ... tag* ``` ## Validation (Typing) @@ -53,7 +53,7 @@ labels {result [t*], kind ε} ``` -C.exceptions[x] = [t*]→[] +C.tags[x] = [t*]→[] ----------------------------- C ⊢ throw x : [t1* t*]→[t2*] @@ -65,7 +65,7 @@ C ⊢ rethrow l : [t1*]→[t2*] C.types[bt] = [t1*]→[t2*] C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] -(C.exceptions[x] = [t*]→[] ∧ +(C.tags[x] = [t*]→[] ∧ C, labels { result [t2*], kind catch } ⊢ instr* : [t*]→[t2*])* (C, labels { result [t2*], kind catch } ⊢ instr'* : []→[t2*])? ----------------------------------------------------------------------------- @@ -86,19 +86,19 @@ C ⊢ try bt instr* delegate l : [t1*]→[t2*] Stores ``` -S ::= {..., exceptions exninst*} +S ::= {..., tags exninst*} ``` -Exception Instances +Tag Instances ``` -exninst ::= {type exntype} +taginst ::= {type tagtype} ``` Module Instances ``` -m ::= {..., exceptions a*} +m ::= {..., tags a*} ``` Administrative Instructions @@ -108,7 +108,7 @@ instr ::= ... | throw a | catch_n{a? instr*}* instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` -Block Contexts and label kinds +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 above 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, mirroring the label kinds of labels in validation contexts. @@ -143,7 +143,7 @@ caught_m{a val^n} B^l[rethrow l] end caught_m{a val^n} val^m end ↪ val^m ``` -A missing exception tag (exnaddr) in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. +A missing tagaddr in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) @@ -154,7 +154,7 @@ catch_m{a? instr*}* val^m end ↪ val^m S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; caught_m{a val^n} (val^n)? instr* end - (if (a1? = ε ∨ a1? = a) ∧ S.exceptions(a).type = [t^n]→[]) + (if (a1? = ε ∨ a1? = a) ∧ S.tags(a).type = [t^n]→[]) S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end @@ -177,11 +177,11 @@ B^l[ delegate{l} T[val^n (throw a)] end ] ### Typing rules for administrative instructions ``` -S.exceptions[a].type = [t2*]→[] +S.tags[a].type = [t2*]→[] -------------------------------- S;C ⊢ throw a : [t1* t2*]→[t*] -(S.exceptions[a].type = [t'*]→[] ∧ +(S.tags[a].type = [t'*]→[] ∧ S;C, labels {result [t*], kind catch} ⊢ instr1* : [t'*]→[t*])* (S;C, labels {result [t*], kind catch} ⊢ instr2* : []→[t*])? S;C, labels {result [t*], kind try} ⊢ instr3* : []→[t*] @@ -193,7 +193,7 @@ C.labels[l].kind = try ----------------------------------------------------------------------- S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] -S.exceptions[a].type = [t'*]→[] +S.tags[a].type = [t'*]→[] (val:t')* S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] -------------------------------------------------------------------------------- From 7d122dd504a45f832e41277623faa927a3b5024f Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Tue, 13 Jul 2021 15:28:07 +0200 Subject: [PATCH 15/24] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- .../Exceptions-formal-examples.md | 3 +- .../Exceptions-formal-overview.md | 38 +++++++++---------- 2 files changed, 19 insertions(+), 22 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index cefad0a6..1f8e2b2c 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -12,7 +12,7 @@ If anyone would like that I add another reduction trace, or other examples, plea ### notation -If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `F.exception[x] = a_x`, where `F` is the current frame. +If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `F.tag[x] = a_x`, where `F` is the current frame. ## example 0 @@ -189,4 +189,3 @@ The thrown exception is (eventually) caught by the outer try's `catch x`, so the ``` label_0 {} (caught_0{a_x} (label_0 {} instr* end) end ``` - diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 20d3f117..ff13b8b8 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -25,7 +25,7 @@ instr ::= ... | throw x | rethrow l Tags ``` -tag ::= export* tag exntype | export* tag tagtype import +tag ::= export* tag tagtype | export* tag tagtype import ``` Modules @@ -41,7 +41,9 @@ mod ::= module ... tag* To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. - +labelkind ::= try | catch +labeltype ::= {result resulttype, kind labelkind?} +C ::= {..., labels labeltype} The original notation `labels [t*]` is now an abbreviation for: ``` @@ -86,7 +88,7 @@ C ⊢ try bt instr* delegate l : [t1*]→[t2*] Stores ``` -S ::= {..., tags exninst*} +S ::= {..., tags taginst*} ``` Tag Instances @@ -113,11 +115,9 @@ 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 above 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, mirroring the label kinds of labels in validation contexts. ``` -label_kind ::= try_label_kind | catch_label_kind -try_label_kind ::= catch_m{a? instr*}* | delegate{l} -catch_label_kind ::= caught_m{a val*} -B^0 ::= val* [_] instr* -B^{k+1} ::= val* label_n{instr*} label_kind? B^k end? end instr* +B^k ::= val* B'^k instr* +B'^0 ::= [_] +B'^{k+1} ::= label_n{instr*} B^k end | catch_m{a? instr*}* B^{k+1} end | caught_m{a val*} B^{k+1} end | delegate{l} B^{k+1} end ``` Note that `label_n{instr*} label_kind? [_] end? end` could be seen as a simplified control frame. @@ -135,7 +135,7 @@ T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end ``` -F; throw x ↪ F; throw a (if F.module.exnaddrs[x]=a) +F; throw x ↪ F; throw a (if F.module.tagaddrs[x]=a) caught_m{a val^n} B^l[rethrow l] end ↪ caught_m{a val^n} B^l[val^n (throw a)] end @@ -143,12 +143,12 @@ caught_m{a val^n} B^l[rethrow l] end caught_m{a val^n} val^m end ↪ val^m ``` -A missing tagaddr in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. +An absent tagaddr in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) ↪ F; label_m{} (catch_m{a instr'*}*{instr''*}? val^n instr* end) end - (if bt = [t1^n]→[t2^m] ∧ (val:t1)^n ∧ (F.module.exnaddrs[x]=a)*) + (if bt = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) catch_m{a? instr*}* val^m end ↪ val^m @@ -177,16 +177,15 @@ B^l[ delegate{l} T[val^n (throw a)] end ] ### Typing rules for administrative instructions ``` -S.tags[a].type = [t2*]→[] +S.tags[a].type = [t*]→[] -------------------------------- -S;C ⊢ throw a : [t1* t2*]→[t*] +S;C ⊢ throw a : [t1* t*]→[t2*] -(S.tags[a].type = [t'*]→[] ∧ - S;C, labels {result [t*], kind catch} ⊢ instr1* : [t'*]→[t*])* -(S;C, labels {result [t*], kind catch} ⊢ instr2* : []→[t*])? -S;C, labels {result [t*], kind try} ⊢ instr3* : []→[t*] +((S.tags[a].type = [t'*]→[])? + S;C, labels {result [t*], kind catch} ⊢ instr'* : [t'*?]→[t*])* +S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] ----------------------------------------------------------------------- -S;C, labels [t*] ⊢ catch_n{a instr1*}*{instr2*}? instr3* end : []→[t*] +S;C, labels [t*] ⊢ catch_n{a? instr'*}* instr* end : []→[t*] S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] C.labels[l].kind = try @@ -197,7 +196,7 @@ S.tags[a].type = [t'*]→[] (val:t')* S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] -------------------------------------------------------------------------------- -S;C, labels {result [t*], kind catch} ⊢ caught_m{a val^n} instr* end : []→[t'*] +S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t'*] ``` By adding the attribute `kind` to labels, we are creating situations in the proof of type preservation, where we have a derivation of some `S;C, label [t*] ⊢ instr* : []→[t*]` but we need to have that `S;C, label {result [t*], kind } ⊢ instr* : []→[t*]` for some ` ::= try | catch`. To resolve this we add the following typing rule for labels in the context, which ensures our newly introduced `try` and `catch` blocks can contain any instructions a regular block can. @@ -208,4 +207,3 @@ labelkind = try ∨ labelkind = catch ----------------------------------------------------------- S;C, label {result [t*], kind labelkind} ⊢ instr* : []→[t*] ``` - From d874fcd06574a481ab4a1d8f972b6bd0acbf1ee7 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 26 Aug 2021 00:43:27 +0200 Subject: [PATCH 16/24] Addressed latest review and added the missing +1 to the adm. delegate. The latter matches the interpreter implementation in PR #175 --- .../Exceptions-formal-examples.md | 26 +++++++------------ .../Exceptions-formal-overview.md | 12 ++------- 2 files changed, 11 insertions(+), 27 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 1f8e2b2c..5e29caa7 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -39,7 +39,7 @@ 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{} (delegate{1} (label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0} throw a_x end) end) end) end) end) end ``` @@ -48,12 +48,12 @@ For the empty 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{} (delegate{1} label_0{} (catch_0{i32.const 27 local.set 0 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{} (delegate{1} (label_0{} (caught{a_x} i32.const 27 local.set 0 rethrow 0 end) end) end) end) end) end ``` @@ -62,33 +62,25 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]`. ``` ↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{0} + (label_0{} (delegate{1} (label_0{} (caught{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{} (delegate{1} (label_0{} (caught{a_x} B^0 [throw a_x] end) end) end) end) end) end ``` -Let `T' = label_0{} (caught{a_x} B^0 [_] end) end`. +Let `T' = label_0{} (caught{a_x} [_] end) end`, and `B^1 = label_0 [_] end`. ``` ↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{0} - T'[throw a_x] end) end) end) end + (B^1 [delegate{1} + T'[throw a_x] end] end) end ↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{0} - T'[throw a_x] end) end) end) end - -↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{0} - T'[throw a_x] end) end) end) end - -↪ F; label_1{} (catch_1{a_x local.get 0} - T'[throw a_x] end) end + (throw a_x) end) end ↪ F; label_1{} (caught_1{a_x} local.get 0 end) end diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index ff13b8b8..8c3c4a87 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -165,7 +165,7 @@ S; F; catch_m T[val^n (throw a)] end val^n (try bt instr* delegate l) - ↪ label_m{} (delegate{l} val^n instr* end) end + ↪ label_m{} (delegate{l+1} val^n instr* end) end (if bt = [t^n]→[t^m]) delegate{l} val^n end ↪ val^n @@ -190,7 +190,7 @@ S;C, labels [t*] ⊢ catch_n{a? instr'*}* instr* end : []→[t*] S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] C.labels[l].kind = try ----------------------------------------------------------------------- -S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] +S;C, labels [t*] ⊢ delegate{l+1} instr* end : []→[t*] S.tags[a].type = [t'*]→[] (val:t')* @@ -199,11 +199,3 @@ S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t'*] ``` -By adding the attribute `kind` to labels, we are creating situations in the proof of type preservation, where we have a derivation of some `S;C, label [t*] ⊢ instr* : []→[t*]` but we need to have that `S;C, label {result [t*], kind } ⊢ instr* : []→[t*]` for some ` ::= try | catch`. To resolve this we add the following typing rule for labels in the context, which ensures our newly introduced `try` and `catch` blocks can contain any instructions a regular block can. - -``` -S;C, label [t*] ⊢ instr* : []→[t*] -labelkind = try ∨ labelkind = catch ------------------------------------------------------------ -S;C, label {result [t*], kind labelkind} ⊢ instr* : []→[t*] -``` From c98ff33c3286ed0da9fde8ec1efdca5caca3ab03 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Tue, 31 Aug 2021 21:43:35 +0200 Subject: [PATCH 17/24] Apply suggestions from code review Co-authored-by: Heejin Ahn --- .../exception-handling/Exceptions-formal-overview.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 8c3c4a87..8fdc7da7 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -41,9 +41,11 @@ mod ::= module ... tag* To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. +``` labelkind ::= try | catch labeltype ::= {result resulttype, kind labelkind?} C ::= {..., labels labeltype} +``` The original notation `labels [t*]` is now an abbreviation for: ``` @@ -68,10 +70,10 @@ C ⊢ rethrow l : [t1*]→[t2*] C.types[bt] = [t1*]→[t2*] C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ - C, labels { result [t2*], kind catch } ⊢ instr* : [t*]→[t2*])* -(C, labels { result [t2*], kind catch } ⊢ instr'* : []→[t2*])? + C, labels { result [t2*], kind catch } ⊢ instr'* : [t*]→[t2*])* +(C, labels { result [t2*], kind catch } ⊢ instr''* : []→[t2*])? ----------------------------------------------------------------------------- -C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] +C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] C.types[bt] = [t1*]→[t2*] From 72bf4f3550f154f4243eeb76b21bb5cf7d8ba872 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Thu, 9 Sep 2021 01:42:57 +0200 Subject: [PATCH 18/24] Apply suggestions from code review Co-authored-by: Heejin Ahn --- .../Exceptions-formal-examples.md | 40 +++++++++---------- .../Exceptions-formal-overview.md | 20 +++++----- 2 files changed, 30 insertions(+), 30 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 5e29caa7..71b6ced6 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -1,4 +1,4 @@ -# 3rd proposal formal spec examples +# 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". @@ -10,24 +10,24 @@ For all other examples just the result of the reduction is given. These examples If anyone would like that I add another reduction trace, or other examples, please let me know, I'd be happy to. -### notation +### Notation If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `F.tag[x] = a_x`, where `F` is the current frame. -## example 0 +## Example 0 The only example with an almost full reduction trace, and all new instructions. The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. ``` (func (result i32) (local i32) - try + try (result i32) try try throw x catch_all i32.const 27 local.set 0 - rethrow 0 + rethrow 0 end delegate 0 catch x @@ -54,42 +54,42 @@ F; label_1{} (catch_1{a_x local.get 0} ↪ F; label_1{} (catch_1{a_x local.get 0} (label_0{} (delegate{1} - (label_0{} (caught{a_x} i32.const 27 local.set 0 rethrow 0 + (label_0{} (caught_0{a_x} i32.const 27 local.set 0 rethrow 0 end) end) end) end) end) end ``` Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]`. ``` -↪ F; label_1{} (catch_1{a_x local.get 0} +↪ F'; label_1{} (catch_1{a_x local.get 0} (label_0{} (delegate{1} - (label_0{} (caught{a_x} B^0 [rethrow 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} +↪ F'; label_1{} (catch_1{a_x local.get 0} (label_0{} (delegate{1} - (label_0{} (caught{a_x} B^0 [throw a_x] + (label_0{} (caught_0{a_x} B^0 [throw a_x] end) end) end) end) end) end ``` -Let `T' = label_0{} (caught{a_x} [_] end) end`, and `B^1 = label_0 [_] end`. +Let `T' = label_0{} (caught_0{a_x} [_] end) end`, and `B^1 = label_0 [_] end`. ``` -↪ F; label_1{} (catch_1{a_x local.get 0} +↪ F'; label_1{} (catch_1{a_x local.get 0} (B^1 [delegate{1} T'[throw a_x] end] end) end -↪ F; label_1{} (catch_1{a_x local.get 0} +↪ F'; label_1{} (catch_1{a_x local.get 0} (throw a_x) end) end -↪ F; label_1{} (caught_1{a_x} local.get 0 end) end +↪ F'; label_1{} (caught_1{a_x} local.get 0 end) end ↪ ↪ ↪ i32.const 27 ``` -## behaviour of `rethrow` +## Behavior of `rethrow` -### example 1 +### Example 1 Location of a rethrown exception. @@ -124,7 +124,7 @@ label_0{} caught{a_x val1} which in this case is the same as `val1 (throw a_x)`. -### example 2 +### Example 2 `rethrow`'s immediate validation error. @@ -140,12 +140,12 @@ end This is a validation error (no catch block at given rethrow depth). -## target of `delegate`'s immediate (label depth) +## Target of `delegate`'s Immediate (Label Depth) @aheejin gave the following [examples in this comment](https://github.com/WebAssembly/exception-handling/pull/143#discussion_r522673735) -### example 3 +### Example 3 `delegate` targeting a catch is a validation error. @@ -160,7 +160,7 @@ end This is a validation error because `delegate`'s `$label0` refers to the catch-label `label { result ε, type catch}`, not to a try-label. -### example 4 +### Example 4 `delegate` correctly targeting a `try-delegate` and a `try-catch`. diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 8fdc7da7..21b98e7a 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -6,7 +6,7 @@ This is an overview of the 3rd proposal's formal spec additions, to aid in discu ### Types -Tag Types +#### Tag Types ``` tagtype ::= [t*]→[] @@ -22,13 +22,13 @@ instr ::= ... | throw x | rethrow l ### Modules -Tags +#### Tags ``` tag ::= export* tag tagtype | export* tag tagtype import ``` -Modules +#### Modules ``` mod ::= module ... tag* @@ -87,32 +87,32 @@ C ⊢ try bt instr* delegate l : [t1*]→[t2*] ### Runtime structure -Stores +#### Stores ``` S ::= {..., tags taginst*} ``` -Tag Instances +#### Tag Instances ``` taginst ::= {type tagtype} ``` -Module Instances +#### Module Instances ``` m ::= {..., tags a*} ``` -Administrative Instructions +#### Administrative Instructions ``` instr ::= ... | throw a | catch_n{a? instr*}* instr* end | delegate{l} instr* end | caught_m{a val^n} instr* end ``` -Block contexts and label kinds +#### 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 above 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, mirroring the label kinds of labels in validation contexts. @@ -126,7 +126,7 @@ Note that `label_n{instr*} label_kind? [_] end? end` could be seen as a simplifi (Alternatively, we could have the above `label_kind`s be also labels, remove the additional `label_m` from the execution rules below, and remove the execution rules below where the new administrative instructions only contain `val*`. This would make labels even more similar to control frames.) -Throw Contexts +#### Throw Contexts ``` T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end @@ -198,6 +198,6 @@ S.tags[a].type = [t'*]→[] (val:t')* S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] -------------------------------------------------------------------------------- -S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t'*] +S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t*] ``` From 4606660d9b97479548d5f8286f151cef8b76e4f1 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Mon, 22 Nov 2021 20:16:02 +0100 Subject: [PATCH 19/24] Removed try-labels and removed +1 from the administrative delegate. - All occurrences of try-labels are removed. - Adjusted the last execution step of the administrative `delegate` to be similar to that of `br 0`. Due to this, I could remove the +1 from the execution step of `try-delegate` reducing to the administrative `delegate`. - Adjusted the examples to these changes: + Example 3 which checked that `try-delegate` does not target a catch is replaced with a check that delegate cannot refer to its own label. + Example 4 has an extra try block added between the outermost try-delegate and its target, to show that the reduction skips the try in between correctly. + Added Example 5 to show how try-delegate reduces when it targets a catch (shows that the throw placed by `delegate` is skipping the catch block). + Folded forms of Wasm-code are added, not only because it may be easier to parse for some people and programs. --- .../Exceptions-formal-examples.md | 308 ++++++++++++++---- .../Exceptions-formal-overview.md | 59 ++-- 2 files changed, 278 insertions(+), 89 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index 71b6ced6..efa4577e 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -12,11 +12,15 @@ If anyone would like that I add another reduction trace, or other examples, plea ### Notation -If `x` is an exception tag index, then `a_x` denotes its exception tag address, i.e., `F.tag[x] = a_x`, where `F` is the current frame. +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. -## Example 0 +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. -The only example with an almost full reduction trace, and all new instructions. The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown. +## 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. ``` (func (result i32) (local i32) @@ -35,56 +39,110 @@ The only example with an almost full reduction trace, and all new instructions. end) ``` -Take the frame `F = (locals i32.const 0, module m)`. We have: +We write the body of this function in folded form, because it is easier to parse. ``` -↪ ↪ ↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{1} - (label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0} - throw a_x end) end) end) end) end) end +(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))) ``` -For the empty throw context `T = [_]` the above is the same as +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{1} - label_0{} (catch_0{i32.const 27 local.set 0 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{} + (catch_0{ ε (local.set 0 (i32.const 27)) (rethrow 0) } + (throw a_x) end) end) end) end) end) end) +``` -↪ F; label_1{} (catch_1{a_x local.get 0} - (label_0{} (delegate{1} - (label_0{} (caught_0{a_x} i32.const 27 local.set 0 rethrow 0 - 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 = [_]`. +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{1} - (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 ε } + 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{} (delegate{1} - (label_0{} (caught_0{a_x} B^0 [throw a_x] - end) end) end) end) end) end +``` +↪ 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) ``` -Let `T' = label_0{} (caught_0{a_x} [_] end) end`, and `B^1 = label_0 [_] 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} - (B^1 [delegate{1} - T'[throw a_x] end] end) end +↪ 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{} (catch_1{a_x local.get 0} - (throw a_x) end) end +↪ F'; (label_1{} + (caught_1{ a_x ε } + (i32.const 27) end) end) -↪ F'; label_1{} (caught_1{a_x} local.get 0 end) end +↪ F'; (label_1{} + (i32.const 27) end) -↪ ↪ ↪ i32.const 27 +↪ F'; (i32.const 27) ``` ## Behavior of `rethrow` @@ -112,17 +170,45 @@ catch x end ``` +Folded it looks as follows. + +``` +(try + (do + val1 + (throw x)) + (catch x ;; <--- (rethrow 2) targets this catch. + (try + (do + val2 + (throw y)) + (catch_all + (try + (do + val3 + (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{a_x val1} - val1 (label_0{} caught{a_y val2} - (label_0{} caught{a_z val3} - val3 val1 (throw a_x) end end) - end end) end end) +(label_0{} + (caught_0{ a_x val1 } + val1 + (label_0{} + (caught_0{ a_y val2 } + ;; The catch_all does not leave val2 here. + (label_0{} + (caught_0{ a_z val3 } + val3 + ;; (rethrow 2) puts val1 and the throw below. + val1 + (throw a_x) end) end) end) end) end) end) ``` -which in this case is the same as `val1 (throw a_x)`. +This reduces to `val1 (throw a_x)`, throwing to the caller. ### Example 2 @@ -132,33 +218,29 @@ which in this case is the same as `val1 (throw a_x)`. [example in this comment](https://github.com/WebAssembly/exception-handling/pull/143#discussion_r522673735) ``` -try $label0 - rethrow $label0 ;; cannot be done, because it's not within catch below -catch -end +(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) -@aheejin gave the following -[examples in this comment](https://github.com/WebAssembly/exception-handling/pull/143#discussion_r522673735) - ### Example 3 -`delegate` targeting a catch is a validation error. +`delegate 0` target. ``` -try $label0 -catch - try - ... - delegate $label0 ;; cannot be done, because $label0's catch is not below but above here -end +(try $l + (do + (throw x)) + (delegate $l)) ``` -This is a validation error because `delegate`'s `$label0` refers to the catch-label `label { result ε, type catch}`, not to a try-label. +This is a validation error, a `delegate` always refers to an outer block. ### Example 4 @@ -166,18 +248,122 @@ This is a validation error because `delegate`'s `$label0` refers to the catch-la ``` try $label1 - try $label0 - try - throw x - delegate $label0 ;; delegate 0 - delegate $label1 ;; delegate 1 + 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} (label_0 {} instr* end) end +(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 index 21b98e7a..83cf2311 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -38,18 +38,18 @@ mod ::= module ... tag* #### Modification to labels -To verify that a `try...delegate l` instruction refers to a label surrounding the instructions of a try block (call this a try-label), introduce a `kind` attribute to labels in the validation context, which is set to `try` when the label is a try-label. +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. -Similarly, to verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we allow the `kind` attribute of labels in the validation context to be set to `catch` when the label is a catch-label. ``` -labelkind ::= try | catch +labelkind ::= catch labeltype ::= {result resulttype, kind labelkind?} C ::= {..., labels labeltype} ``` + The original notation `labels [t*]` is now an abbreviation for: ``` -labels {result [t*], kind ε} +labels [t*] ::= labels {result [t*], kind ε} ``` @@ -68,7 +68,7 @@ C ⊢ rethrow l : [t1*]→[t2*] C.types[bt] = [t1*]→[t2*] -C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] +C, labels [t2*] ⊢ instr* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ C, labels { result [t2*], kind catch } ⊢ instr'* : [t*]→[t2*])* (C, labels { result [t2*], kind catch } ⊢ instr''* : []→[t2*])? @@ -77,9 +77,9 @@ C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] C.types[bt] = [t1*]→[t2*] -C, labels {result [t2*], kind try} ⊢ instr* : [t1*]→[t2*] -C.labels[l].kind = try ----------------------------------------------------------- +C, labels [t2*] ⊢ instr* : [t1*]→[t2*] +C.labels[l] = [t*] +------------------------------------------- C ⊢ try bt instr* delegate l : [t1*]→[t2*] ``` @@ -114,27 +114,28 @@ instr ::= ... | throw a | catch_n{a? instr*}* 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 above 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, mirroring the label kinds of labels in validation contexts. +So far block contexts are only used in the reduction of `br l` and `return`, and only include labels or values on the stack above 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^k ::= val* B'^k instr* -B'^0 ::= [_] -B'^{k+1} ::= label_n{instr*} B^k end | catch_m{a? instr*}* B^{k+1} end | caught_m{a val*} B^{k+1} end | delegate{l} B^{k+1} end +B^0 ::= val* [_] instr* +B^k ::= catch_m{a^? instr*}* B^k end | caught_m{a val*} B^k end | delegate{l} B^k end +B^{k+1} ::= val* (label_n{instr*} B^k end) instr* ``` -Note that `label_n{instr*} label_kind? [_] end? end` could be seen as a simplified control frame. - -(Alternatively, we could have the above `label_kind`s be also labels, remove the additional `label_m` from the execution rules below, and remove the execution rules below where the new administrative instructions only contain `val*`. This would make labels even more similar to control frames.) - #### Throw Contexts +Throw contexts don't skip over handlers, they are used to match a thrown exception with the innermost handler. + ``` T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end | frame_n{F} T end ``` -### Instructions +Note that because `catch_n` instructions are not included above, there is always a unique maximal throw context. + +### Reduction of instructions +Reduction steps for the new instructions or administrative instructions. ``` F; throw x ↪ F; throw a (if F.module.tagaddrs[x]=a) @@ -145,11 +146,11 @@ caught_m{a val^n} B^l[rethrow l] end caught_m{a val^n} val^m end ↪ val^m ``` -An absent tagaddr in a `catch_m` clause (i.e., `a? = ε`) represents a `catch_all`. +An absent tag address in a `handler` clause (i.e., `a? = ε`) represents a `catch_all`. ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) - ↪ F; label_m{} (catch_m{a instr'*}*{instr''*}? val^n instr* end) end + ↪ F; label_m{} (catch_m{a instr'*}*{ε instr''*}? val^n instr* end) end (if bt = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) catch_m{a? instr*}* val^m end ↪ val^m @@ -167,15 +168,17 @@ S; F; catch_m T[val^n (throw a)] end val^n (try bt instr* delegate l) - ↪ label_m{} (delegate{l+1} val^n instr* end) end + ↪ label_m{} (delegate{l} val^n instr* end) end (if bt = [t^n]→[t^m]) delegate{l} val^n end ↪ val^n -B^l[ delegate{l} T[val^n (throw a)] end ] +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`. + ### Typing rules for administrative instructions ``` @@ -185,19 +188,19 @@ S;C ⊢ throw a : [t1* t*]→[t2*] ((S.tags[a].type = [t'*]→[])? S;C, labels {result [t*], kind catch} ⊢ instr'* : [t'*?]→[t*])* -S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] ------------------------------------------------------------------------ +S;C, labels [t*] ⊢ instr* : []→[t*] +----------------------------------------------------------------- S;C, labels [t*] ⊢ catch_n{a? instr'*}* instr* end : []→[t*] -S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*] -C.labels[l].kind = try ------------------------------------------------------------------------ -S;C, labels [t*] ⊢ delegate{l+1} 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 {result [t*], kind catch} ⊢ instr* : []→[t*] --------------------------------------------------------------------------------- +---------------------------------------------------------- S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t*] ``` From b12eec9384f55d9d4f49eb895622006d771f4e2b Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 23 Nov 2021 00:55:17 +0100 Subject: [PATCH 20/24] Adjusted interpreter to the simplified reduction rule for delegate. - Removed +1 from the reduction to the administrative delegate. - Adjusted reduction of the administrative delegate. --- interpreter/exec/eval.ml | 6 +----- test/core/try_delegate.wast | 30 ++++++++++++++++++++++++++++-- 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index b7cbce45..d9c3e444 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', [] @@ -575,9 +574,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/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)))") From 9b02debf6a3bb03f64373eb0e56f6f857fc1e68d Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 23 Nov 2021 12:18:46 +0100 Subject: [PATCH 21/24] Fixed grammar definitions. --- .../Exceptions-formal-overview.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 83cf2311..da60e9c5 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -15,9 +15,9 @@ tagtype ::= [t*]→[] ### Instructions ``` -instr ::= ... | throw x | rethrow l - | try bt instr* (catch x instr*)* (catch_all instr*)? end - | try bt instr* delegate l +instr ::= ... | throw tagidx | rethrow labelidx + | try blocktype instr* (catch tagidx instr*)* (catch_all instr*)? end + | try blocktype instr* delegate labelidx ``` ### Modules @@ -102,14 +102,14 @@ taginst ::= {type tagtype} #### Module Instances ``` -m ::= {..., tags a*} +m ::= {..., tags tagaddr*} ``` #### Administrative Instructions ``` -instr ::= ... | throw a | catch_n{a? instr*}* instr* end - | delegate{l} instr* end | caught_m{a val^n} instr* end +instr ::= ... | throw tagaddr | catch_n{ tagaddr? instr* }* instr* end + | delegate{ labelidx } instr* end | caught_m{ tagaddr val^n } instr* end ``` #### Block contexts and label kinds @@ -118,7 +118,8 @@ So far block contexts are only used in the reduction of `br l` and `return`, and ``` B^0 ::= val* [_] instr* -B^k ::= catch_m{a^? instr*}* B^k end | caught_m{a val*} B^k end | delegate{l} B^k end +B^k ::= catch_m{ tagaddr^? instr* }* B^k end | caught_m{ tagaddr val* } B^k end + | delegate{ labelidx } B^k end B^{k+1} ::= val* (label_n{instr*} B^k end) instr* ``` @@ -127,7 +128,7 @@ B^{k+1} ::= val* (label_n{instr*} B^k end) instr* Throw contexts don't skip over handlers, they are used to match a thrown exception with the innermost handler. ``` -T ::= val* [_] instr* | label_n{instr*} T end | caught_m{a val^n} T end +T ::= val* [_] instr* | label_n{instr*} T end | caught_m{ tagaddr val^n } T end | frame_n{F} T end ``` From bb0a6230d092e7365399f1768336a0abc0c2d3c0 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Thu, 2 Dec 2021 14:58:08 +0100 Subject: [PATCH 22/24] Apply suggestions from code review Co-authored-by: Heejin Ahn Co-authored-by: Andreas Rossberg --- .../Exceptions-formal-examples.md | 8 ++-- .../Exceptions-formal-overview.md | 38 +++++++++---------- 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index efa4577e..f06e0317 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -1,12 +1,12 @@ # 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". +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. Some times/often the examples are modified to fit the current syntax. +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. @@ -16,7 +16,7 @@ If `x` is an exception tag index, then `a_x` denotes its exception tag address, 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. +## 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`. @@ -107,7 +107,7 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]` to (label_0{} (delegate{ 0 } (label_0{} - (caught_0{ a_x } + (caught_0{ a_x ε } (throw a_x) end) end) end) end) end) end) ``` diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index da60e9c5..aecebc01 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -1,4 +1,4 @@ -# 3rd proposal formal spec overview +# 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. @@ -9,15 +9,15 @@ This is an overview of the 3rd proposal's formal spec additions, to aid in discu #### Tag Types ``` -tagtype ::= [t*]→[] +tagtype ::= [valtype*]→[] ``` ### Instructions ``` -instr ::= ... | throw tagidx | rethrow labelidx - | try blocktype instr* (catch tagidx instr*)* (catch_all instr*)? end - | try blocktype instr* delegate labelidx +instr ::= ... | 'throw' tagidx | 'rethrow' labelidx + | 'try' blocktype instr* ('catch' tagidx instr*)* ('catch_all' instr*)? 'end' + | 'try' blocktype instr* 'delegate' labelidx ``` ### Modules @@ -25,18 +25,18 @@ instr ::= ... | throw tagidx | rethrow labelidx #### Tags ``` -tag ::= export* tag tagtype | export* tag tagtype import +tag ::= export* 'tag' tagtype | export* 'tag' tagtype import ``` #### Modules ``` -mod ::= module ... tag* +mod ::= 'module' ... tag* ``` ## Validation (Typing) -#### Modification to labels +#### 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. @@ -67,7 +67,7 @@ C.labels[l].kind = catch C ⊢ rethrow l : [t1*]→[t2*] -C.types[bt] = [t1*]→[t2*] +C ⊢ bt : [t1*]→[t2*] C, labels [t2*] ⊢ instr* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ C, labels { result [t2*], kind catch } ⊢ instr'* : [t*]→[t2*])* @@ -76,7 +76,7 @@ C, labels [t2*] ⊢ instr* : [t1*]→[t2*] C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] -C.types[bt] = [t1*]→[t2*] +C ⊢ bt : [t1*]→[t2*] C, labels [t2*] ⊢ instr* : [t1*]→[t2*] C.labels[l] = [t*] ------------------------------------------- @@ -85,7 +85,7 @@ C ⊢ try bt instr* delegate l : [t1*]→[t2*] ## Execution (Reduction) -### Runtime structure +### Runtime Structure #### Stores @@ -108,17 +108,17 @@ m ::= {..., tags tagaddr*} #### Administrative Instructions ``` -instr ::= ... | throw tagaddr | catch_n{ tagaddr? instr* }* instr* end +instr ::= ... | 'throw' tagaddr | 'catch'_n{ tagaddr? instr* }* instr* 'end' | delegate{ labelidx } instr* end | caught_m{ tagaddr val^n } instr* end ``` -#### Block contexts and label kinds +#### 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 above 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* -B^k ::= catch_m{ tagaddr^? instr* }* B^k end | caught_m{ tagaddr val* } B^k end +B^k ::= catch_m{ tagaddr? instr* }* B^k end | caught_m{ tagaddr val* } B^k end | delegate{ labelidx } B^k end B^{k+1} ::= val* (label_n{instr*} B^k end) instr* ``` @@ -132,9 +132,9 @@ T ::= val* [_] instr* | label_n{instr*} T end | caught_m{ tagaddr val^n } T end | frame_n{F} T end ``` -Note that because `catch_n` instructions are not included above, there is always a unique maximal throw context. +Note that because `catch_n` and `delegate` instructions are not included above, there is always a unique maximal throw context. -### Reduction of instructions +### Reduction of Instructions Reduction steps for the new instructions or administrative instructions. @@ -152,7 +152,7 @@ An absent tag address in a `handler` clause (i.e., `a? = ε`) represents a `catc ``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) ↪ F; label_m{} (catch_m{a instr'*}*{ε instr''*}? val^n instr* end) end - (if bt = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) + (if expand_F(bt) = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) catch_m{a? instr*}* val^m end ↪ val^m @@ -170,7 +170,7 @@ S; F; catch_m T[val^n (throw a)] end val^n (try bt instr* delegate l) ↪ label_m{} (delegate{l} val^n instr* end) end - (if bt = [t^n]→[t^m]) + (if expand_F(bt) = [t^n]→[t^m]) delegate{l} val^n end ↪ val^n @@ -180,7 +180,7 @@ label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end Note that the last reduction step above is similar to the reduction of `br`. -### Typing rules for administrative instructions +### Typing Rules for Administrative Instructions ``` S.tags[a].type = [t*]→[] From 5457b7a99d8967f6295fdcff4fa5d0943b699fa2 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 28 Jan 2022 16:02:51 +0100 Subject: [PATCH 23/24] Addressed latest reviews --- .../Exceptions-formal-examples.md | 47 ++++----- .../Exceptions-formal-overview.md | 98 +++++++++++-------- 2 files changed, 79 insertions(+), 66 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-examples.md b/proposals/exception-handling/Exceptions-formal-examples.md index f06e0317..48ea8ece 100644 --- a/proposals/exception-handling/Exceptions-formal-examples.md +++ b/proposals/exception-handling/Exceptions-formal-examples.md @@ -20,21 +20,22 @@ 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. +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 + throw $x catch_all i32.const 27 local.set 0 rethrow 0 end delegate 0 - catch x + catch $x local.get 0 end) ``` @@ -48,12 +49,12 @@ We write the body of this function in folded form, because it is easier to parse (do (try (do - (throw x)) + (throw $x)) (catch_all (local.set 0 (i32.const 27)) (rethrow 0)))) (delegate 0))) - (catch x + (catch $x (local.get 0))) ``` @@ -149,22 +150,22 @@ Use the trivial throw context `T` again, this time to match the throw to the `ca ### Example 1 -Location of a rethrown exception. +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 - val1 + val_x throw x catch x - try - val2 + try $label2 + val_y throw y catch_all try - val3 + val_z throw z catch z - rethrow 2 + rethrow $label2 ;; This is rethrow 2. end end end @@ -175,17 +176,17 @@ Folded it looks as follows. ``` (try (do - val1 + val_x (throw x)) (catch x ;; <--- (rethrow 2) targets this catch. (try (do - val2 + val_y (throw y)) (catch_all (try (do - val3 + val_z (throw z)) (catch z (rethrow 2))))))) @@ -195,20 +196,20 @@ In the above example, all thrown exceptions get caught and the first one gets re ``` (label_0{} - (caught_0{ a_x val1 } - val1 + (caught_0{ a_x val_x } ;; <---- The exception rethrown by `rethrow 2` below. + val_x (label_0{} - (caught_0{ a_y val2 } - ;; The catch_all does not leave val2 here. + (caught_0{ a_y val_y } + ;; The catch_all does not leave val_y here. (label_0{} - (caught_0{ a_z val3 } - val3 - ;; (rethrow 2) puts val1 and the throw below. - val1 + (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 `val1 (throw a_x)`, throwing to the caller. +This reduces to `val_x (throw a_x)`, throwing to the caller. ### Example 2 diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index aecebc01..4f6599ab 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -41,19 +41,25 @@ mod ::= 'module' ... tag* 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 ::= {result resulttype, kind labelkind?} -C ::= {..., labels labeltype} +labelkind ::= 'catch' +labeltype ::= 'catch'? resulttype +C ::= {..., 'labels' labeltype} ``` The original notation `labels [t*]` is now an abbreviation for: ``` -labels [t*] ::= labels {result [t*], kind ε} +'labels' [t*] ::= 'labels' ε [t*] ``` +### Validation Contexts -### Instructions +Validation contexts now hold a list of tag types, one for each tag known to them. +``` +C ::= { ..., 'tags' tagtype*} +``` + +### Validation Rules for Instructions ``` @@ -70,8 +76,8 @@ C ⊢ rethrow l : [t1*]→[t2*] C ⊢ bt : [t1*]→[t2*] C, labels [t2*] ⊢ instr* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ - C, labels { result [t2*], kind catch } ⊢ instr'* : [t*]→[t2*])* -(C, labels { result [t2*], kind catch } ⊢ instr''* : []→[t2*])? + 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*] @@ -90,86 +96,87 @@ C ⊢ try bt instr* delegate l : [t1*]→[t2*] #### Stores ``` -S ::= {..., tags taginst*} +S ::= {..., 'tags' taginst*} ``` #### Tag Instances ``` -taginst ::= {type tagtype} +taginst ::= {'type' tagtype} ``` #### Module Instances ``` -m ::= {..., tags tagaddr*} +m ::= {..., 'tags' tagaddr*} ``` #### Administrative Instructions ``` -instr ::= ... | 'throw' tagaddr | 'catch'_n{ tagaddr? instr* }* instr* 'end' - | delegate{ labelidx } instr* end | caught_m{ tagaddr val^n } instr* end +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 above 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. +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* -B^k ::= catch_m{ tagaddr? instr* }* B^k end | caught_m{ tagaddr val* } B^k end - | delegate{ labelidx } B^k end -B^{k+1} ::= val* (label_n{instr*} B^k end) instr* +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, they are used to match a thrown exception with the innermost handler. +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_m{ tagaddr val^n } T end - | frame_n{F} T end +T ::= val* '[_]' instr* | 'label'_n{instr*} T 'end' + | 'caught'{ tagaddr val^n } T 'end' + | 'frame'_n{F} T end ``` -Note that because `catch_n` and `delegate` instructions are not included above, there is always a unique maximal throw context. +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_m{a val^n} B^l[rethrow l] end - ↪ caught_m{a val^n} B^l[val^n (throw a)] end +caught{a val^n} B^l[rethrow l] end + ↪ caught{a val^n} B^l[val^n (throw a)] end -caught_m{a val^n} val^m end ↪ val^m -``` +caught{a val^n} val^m end ↪ val^m -An absent tag address in a `handler` clause (i.e., `a? = ε`) represents a `catch_all`. -``` F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) - ↪ F; label_m{} (catch_m{a instr'*}*{ε instr''*}? val^n instr* end) 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_m{a? instr*}* val^m end ↪ val^m +catch{a? instr*}* val^m end ↪ val^m -S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end - ↪ S; F; caught_m{a val^n} (val^n)? instr* end +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]→[]) -S; F; catch_m{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end - ↪ S; F; catch_m{a'? instr'*}* T[val^n (throw a)] end +catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end + ↪ catch{a'? instr'*}* T[val^n (throw a)] end (if a1? ≠ ε ∧ a1? ≠ a) -S; F; catch_m T[val^n (throw a)] end - ↪ S; F; val^n (throw a) +catch T[val^n (throw a)] end ↪ val^n (throw a) -val^n (try bt instr* delegate l) - ↪ label_m{} (delegate{l} val^n instr* end) end +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 @@ -178,7 +185,12 @@ 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`. +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 @@ -188,10 +200,10 @@ S.tags[a].type = [t*]→[] S;C ⊢ throw a : [t1* t*]→[t2*] ((S.tags[a].type = [t'*]→[])? - S;C, labels {result [t*], kind catch} ⊢ instr'* : [t'*?]→[t*])* + S;C, labels catch [t*] ⊢ instr'* : [t'*?]→[t*])* S;C, labels [t*] ⊢ instr* : []→[t*] ------------------------------------------------------------------ -S;C, labels [t*] ⊢ catch_n{a? instr'*}* instr* end : []→[t*] +----------------------------------------------------------- +S;C, labels [t*] ⊢ catch{a? instr'*}* instr* end : []→[t*] S;C, labels [t*] ⊢ instr* : []→[t*] C.labels[l] = [t'*] @@ -200,8 +212,8 @@ S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] S.tags[a].type = [t'*]→[] (val:t')* -S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*] +S;C, labels catch [t*] ⊢ instr* : []→[t*] ---------------------------------------------------------- -S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t*] +S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] ``` From 315fe155d9718f89b3c30e1acc4af536edc53a14 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Fri, 4 Feb 2022 16:34:28 +0100 Subject: [PATCH 24/24] Added TODO item for uncaught exceptions --- proposals/exception-handling/Exceptions-formal-overview.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 4f6599ab..b3af11b0 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -217,3 +217,6 @@ 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.