From 05f400bd2b0d3e7cb1bbc39a32a8c62bfb15fca0 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 10 Nov 2020 11:46:32 +0100 Subject: [PATCH] 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 000000000..a90f75f1c --- /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 +```