formal spec overview for the 3rd exception handling proposal

proposals/exception-handling/Exceptions-formal-examples.md

@@ -0,0 +1,183 @@
+# 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 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
+
+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
+      try
+        throw x
+      catch_all
+        i32.const 27
+        local.set 0
+      rethrow 0
+      end
+    delegate 0
+  catch x
+    local.get 0
+  end)
+```
+
+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}
+               throw a_x end) end) end) end) end) end
+```
+
+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{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{1}
+         (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^0 = [_]`.
+
+```
+↪ F; label_1{} (catch_1{a_x local.get 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{1}
+         (label_0{} (caught{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`.
+
+```
+↪ 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}
+       (throw a_x) end) end
+
+↪ F; label_1{} (caught_1{a_x} local.get 0 end) end
+
+↪ ↪ ↪ i32.const 27
+```
+
+## behaviour of `rethrow`
+
+### example 1
+
+Location of a rethrown exception.
+
+```
+try
+  val1
+  throw x
+catch x
+  try
+    val2
+    throw y
+  catch_all
+    try
+      val3
+      throw z
+    catch z
+      rethrow 2
+    end
+  end
+end
+```
+
+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)
+```
+
+which in this case is the same as `val1 (throw a_x)`.
+
+### 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` targeting 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 targeting a `try-delegate` and a `try-catch`.
+
+```
+try $label1
+  try $label0
+    try
+      throw x
+    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 following.
+
+```
+label_0 {} (caught_0{a_x}  (label_0 {} instr* end) end
+```

proposals/exception-handling/Exceptions-formal-overview.md

@@ -0,0 +1,201 @@
+# 3rd proposal formal spec overview
+
+This is an overview of the 3rd proposal's formal spec additions, to aid in discussions concerning the proposed semantics.
+
+## Abstract Syntax
+
+### Types
+
+Tag Types
+
+```
+tagtype ::= [t*]→[]
+```
+
+### Instructions
+
+```
+instr ::= ... | throw x | rethrow l
+        | try bt instr* (catch x instr*)* (catch_all instr*)? end
+        | try bt instr* delegate l
+```
+
+### Modules
+
+Tags
+
+```
+tag ::= export* tag tagtype  | export* tag tagtype import
+```
+
+Modules
+
+```
+mod ::= module ... tag*
+```
+
+## 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.
+labelkind ::= try | catch
+labeltype ::= {result resulttype, kind labelkind?}
+C ::= {..., labels labeltype}
+The original notation `labels [t*]` is now an abbreviation for:
+
+```
+labels {result [t*], kind ε}
+```
+
+
+### Instructions
+
+
+```
+C.tags[x] = [t*]→[]
+-----------------------------
+C ⊢ throw x : [t1* t*]→[t2*]
+
+
+C.labels[l].kind = catch
+----------------------------
+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 ⊢ 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 ⊢ try bt instr* delegate l : [t1*]→[t2*]
+```
+
+## Execution (Reduction)
+
+### Runtime structure
+
+Stores
+
+```
+S ::= {..., tags taginst*}
+```
+
+Tag Instances
+
+```
+taginst ::= {type tagtype}
+```
+
+Module Instances
+
+```
+m ::= {..., tags a*}
+```
+
+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
+
+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.
+
+```
+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.
+
+(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
+
+```
+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  (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_m{a val^n} val^m end  ↪  val^m
+```
+
+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] ∧ (F.module.tagaddrs[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} (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
+  (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)
+  ↪ label_m{} (delegate{l+1} 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 ]
+  ↪ val^n (throw a)
+```
+
+### Typing rules for administrative instructions
+
+```
+S.tags[a].type = [t*]→[]
+--------------------------------
+S;C ⊢ throw a : [t1* t*]→[t2*]
+
+((S.tags[a].type = [t'*]→[])?
+ S;C, labels {result [t*], kind catch} ⊢ instr'* : [t'*?]→[t*])*
+S;C, labels {result [t*], kind try} ⊢ 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.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'*]
+```
+