From d63e8334ca2546ecb2a203677ba7f3d90cbab09a Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Sun, 20 Feb 2022 19:39:37 +0100 Subject: [PATCH 1/4] Addressed the minor review comments on merged PR #143. --- .../Exceptions-formal-overview.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 20159d21..3e54abdf 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -36,14 +36,14 @@ mod ::= 'module' ... tag* ## Validation (Typing) -#### Modification to Labels + +### Validation Contexts: Tagtypes and modified Labels To verify that the `rethrow l` instruction refers to a label surrounding the instructions of a catch block (call this a catch-label), we introduce a `kind` attribute to labels in the validation context, which is set to `catch` when the label is a catch-label and empty otherwise. ``` labelkind ::= 'catch' labeltype ::= 'catch'? resulttype -C ::= {..., 'labels' labeltype} ``` The original notation `labels [t*]` is now an abbreviation for: @@ -52,11 +52,11 @@ The original notation `labels [t*]` is now an abbreviation for: 'labels' [t*] ::= 'labels' ε [t*] ``` -### Validation Contexts +The `labels` entry of validation contexts is modified to use the above definition of labels. +Moreover, validation contexts now hold a list of tag types, one for each tag known to them. -Validation contexts now hold a list of tag types, one for each tag known to them. ``` -C ::= { ..., 'tags' tagtype*} +C ::= { ..., 'labels' labeltype, 'tags' tagtype*} ``` ### Validation Rules for Instructions @@ -76,8 +76,8 @@ C ⊢ rethrow l : [t1*]→[t2*] C ⊢ bt : [t1*]→[t2*] C, labels [t2*] ⊢ instr* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ - C, labels catch [t2*] ⊢ instr'* : [t*]→[t2*])* -(C, labels catch [t2*] ⊢ instr''* : []→[t2*])? + C, 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*] @@ -200,7 +200,7 @@ S.tags[a].type = [t*]→[] S;C ⊢ throw a : [t1* t*]→[t2*] ((S.tags[a].type = [t'*]→[])? - S;C, labels catch [t*] ⊢ instr'* : [t'*?]→[t*])* + S;C, labels (catch [t*]) ⊢ instr'* : [t'*?]→[t*])* S;C, labels [t*] ⊢ instr* : []→[t*] ----------------------------------------------------------- S;C, labels [t*] ⊢ catch{a? instr'*}* instr* end : []→[t*] @@ -212,7 +212,7 @@ S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] S.tags[a].type = [t'*]→[] (val:t')* -S;C, labels catch [t*] ⊢ instr* : []→[t*] +S;C, labels (catch [t*]) ⊢ instr* : []→[t*] ---------------------------------------------------------- S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] ``` From f59557e00a759a095d10cf9b61553e1858172a89 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 24 Feb 2022 18:30:55 +0100 Subject: [PATCH 2/4] More minor corrections, notation readability, "control" prose in block contexts. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Switching to "S ⊢ ..." notation for premises of typing rules for administrative instructions, to match the spec document. Readability: Changing quotes to number indices, and removing unnecessary explicit exponent variables. Suggesting prose for the new constructs in block contexts, connoting the new structured administrative instructions with control frame opcodes. --- .../Exceptions-formal-overview.md | 55 ++++++++++--------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 3e54abdf..4ee90e11 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -74,12 +74,12 @@ C ⊢ rethrow l : [t1*]→[t2*] C ⊢ bt : [t1*]→[t2*] -C, labels [t2*] ⊢ instr* : [t1*]→[t2*] +C, labels [t2*] ⊢ instr1* : [t1*]→[t2*] (C.tags[x] = [t*]→[] ∧ - C, labels (catch [t2*]) ⊢ instr'* : [t*]→[t2*])* -(C, labels (catch [t2*]) ⊢ instr''* : []→[t2*])? + C, labels (catch [t2*]) ⊢ instr2* : [t*]→[t2*])* +(C, labels (catch [t2*]) ⊢ instr3* : []→[t2*])? ----------------------------------------------------------------------------- -C ⊢ try bt instr* (catch x instr'*)* (catch_all instr''*)? end : [t1*]→[t2*] +C ⊢ try bt instr1* (catch x instr2*)* (catch_all instr3*)? end : [t1*]→[t2*] C ⊢ bt : [t1*]→[t2*] @@ -130,6 +130,8 @@ C^k ::= 'catch'{ tagaddr? instr* }* B^k 'end' | 'delegate'{ labelidx } B^k 'end' ``` +Note the `C` in `C^k` above stands for `control`, because the related administrative instructions are in some ways modelling [control frame opcodes](https://webassembly.github.io/spec/core/appendix/algorithm.html?highlight=control#data-structures) "on the stack". + #### Throw Contexts Throw contexts don't skip over handlers (administrative `catch` or `delegate` instructions). @@ -152,34 +154,34 @@ An absent tag address in a `catch` administrative instruction (i.e., `a? = ε`) ``` F; throw x ↪ F; throw a (if F.module.tagaddrs[x]=a) -caught{a val^n} B^l[rethrow l] end - ↪ caught{a val^n} B^l[val^n (throw a)] end +caught{a val*} B^l[rethrow l] end + ↪ caught{a val*} B^l[val* (throw a)] end -caught{a val^n} val^m end ↪ val^m +caught{a val0*} val* end ↪ val* -F; val^n (try bt instr* (catch x instr'*)* (catch_all instr''*)? end) - ↪ F; label_m{} (catch{a instr'*}*{ε instr''*}? val^n instr* end) end +F; val^n (try bt instr1* (catch x instr2*)* (catch_all instr3*)? end) + ↪ F; label_m{} (catch{a instr2*}*{ε instr3*}? val^n instr1* end) end (if expand_F(bt) = [t1^n]→[t2^m] ∧ (F.module.tagaddrs[x]=a)*) -catch{a? instr*}* val^m end ↪ val^m +catch{a? instr*}* val* end ↪ val* -S; F; catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end - ↪ S; F; caught{a val^n} (val^n)? instr* end +S; F; catch{a1? instr1*}{a0? instr0*}* T[val^n (throw a)] end + ↪ S; F; caught{a val^n} (val^n)? instr1* end (if (a1? = ε ∨ a1? = a) ∧ S.tags(a).type = [t^n]→[]) -catch{a1? instr*}{a'? instr'*}* T[val^n (throw a)] end - ↪ catch{a'? instr'*}* T[val^n (throw a)] end +catch{a1? instr*}{a0? instr0*}* T[val^n (throw a)] end + ↪ catch{a0? instr0*}* T[val^n (throw a)] end (if a1? ≠ ε ∧ a1? ≠ a) -catch T[val^n (throw a)] end ↪ val^n (throw a) +catch T[val* (throw a)] end ↪ val* (throw a) F; val^n (try bt instr* delegate l) ↪ F; label_m{} (delegate{l} val^n instr* end) end - (if expand_F(bt) = [t^n]→[t^m]) + (if expand_F(bt) = [t1^n]→[t2^m]) -delegate{l} val^n end ↪ val^n +delegate{l} val* end ↪ val* label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end ↪ val^n (throw a) @@ -194,24 +196,25 @@ There is a subtle difference though. The instruction `br l` searches for the `l+ ### Typing Rules for Administrative Instructions + ``` -S.tags[a].type = [t*]→[] --------------------------------- +S ⊢ tag a : tag [t*]→[] +------------------------------- S;C ⊢ throw a : [t1* t*]→[t2*] -((S.tags[a].type = [t'*]→[])? - S;C, labels (catch [t*]) ⊢ instr'* : [t'*?]→[t*])* -S;C, labels [t*] ⊢ instr* : []→[t*] +((S ⊢ tag a : tag [t*]→[])? + S;C, labels (catch [t2*]) ⊢ instr2* : [t1*?]→[t2*])* +S;C, labels [t2*] ⊢ instr1* : []→[t2*] ----------------------------------------------------------- -S;C, labels [t*] ⊢ catch{a? instr'*}* instr* end : []→[t*] +S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*] S;C, labels [t*] ⊢ instr* : []→[t*] -C.labels[l] = [t'*] +C.labels[l] = [t0*] ------------------------------------------------------ S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*] -S.tags[a].type = [t'*]→[] -(val:t')* +S ⊢ tag a : tag [t0*]→[] +(val:t0)* S;C, labels (catch [t*]) ⊢ instr* : []→[t*] ---------------------------------------------------------- S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] From e45f09d93a81dbf04973be017a3d7afffd99c9dc Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 6 May 2022 19:24:57 +0200 Subject: [PATCH 3/4] Apply suggestions from code review This commit will be soon moved to a PR with the minor (non-delegate specific) changes. Co-authored-by: Heejin Ahn --- proposals/exception-handling/Exceptions-formal-overview.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 4ee90e11..209df6ec 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -36,7 +36,6 @@ mod ::= 'module' ... tag* ## Validation (Typing) - ### Validation Contexts: Tagtypes and modified 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. @@ -130,7 +129,7 @@ C^k ::= 'catch'{ tagaddr? instr* }* B^k 'end' | 'delegate'{ labelidx } B^k 'end' ``` -Note the `C` in `C^k` above stands for `control`, because the related administrative instructions are in some ways modelling [control frame opcodes](https://webassembly.github.io/spec/core/appendix/algorithm.html?highlight=control#data-structures) "on the stack". +Note the `C` in `C^k` above stands for `control`, because the related administrative instructions are in some ways modeling [control frame opcodes](https://webassembly.github.io/spec/core/appendix/algorithm.html?highlight=control#data-structures) "on the stack". #### Throw Contexts @@ -202,7 +201,7 @@ S ⊢ tag a : tag [t*]→[] ------------------------------- S;C ⊢ throw a : [t1* t*]→[t2*] -((S ⊢ tag a : tag [t*]→[])? +((S ⊢ tag a : tag [t1*]→[])? S;C, labels (catch [t2*]) ⊢ instr2* : [t1*?]→[t2*])* S;C, labels [t2*] ⊢ instr1* : []→[t2*] ----------------------------------------------------------- From c1d0c129bab5e7f4b0098df9a1bacb84faa9fe49 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 10 May 2022 18:11:58 +0200 Subject: [PATCH 4/4] Addressed review comment https://github.com/WebAssembly/exception-handling/pull/208/files#r868964603 by @rossberg > Oh, I think this rule needs to look up the arity of a, in order to know > how many values to keep, because T may contain an arbitrary prefix of > additional values that makes the decomposition ambiguous otherwise. --- proposals/exception-handling/Exceptions-formal-overview.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 209df6ec..5630083b 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -173,7 +173,8 @@ catch{a1? instr*}{a0? instr0*}* T[val^n (throw a)] end ↪ catch{a0? instr0*}* T[val^n (throw a)] end (if a1? ≠ ε ∧ a1? ≠ a) -catch T[val* (throw a)] end ↪ val* (throw a) +catch T[val^n (throw a)] end ↪ val^n (throw a) + (if S.tags(a).type = [t^n]→[]) F; val^n (try bt instr* delegate l)