Updated validation rules to match latest semantics of WebAssembly#137

As of commit 275c449

- `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.

Author: ioannad

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.
+
+

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
 ```