formal spec overview for the 3rd exception handling proposal

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
 

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,11 @@ 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*]
 ```
 
+## TODO Uncaught Exceptions
+
+We haven't yet described the formalism for an uncaught exception being the result of evaluation.