diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index b8390ade..90683994 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -236,7 +236,7 @@ let rec step (c : config) : config = let n1 = Lib.List32.length ts1 in let n2 = Lib.List32.length ts2 in let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n2, [], ([], [Delegate (x.it, (args, List.map plain es')) @@ e.at])) @@ e.at] + vs', [Delegate (x.it, (args, [Label (n2, [], ([], List.map plain es')) @@ e.at])) @@ e.at] | Drop, v :: vs' -> vs', [] @@ -639,7 +639,10 @@ let rec step (c : config) : config = | Rethrowing _, _ -> Crash.error e.at "undefined catch label" - | Delegating _, _ -> + | Delegating (0l, a, vs0), vs -> + vs, [Throwing (a, vs0) @@ e.at] + + | Delegating (k,_, _), _ -> Crash.error e.at "undefined delegate label" | Label (n, es0, (vs', [])), vs -> diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 027a4720..28136ca1 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -180,21 +180,22 @@ catch T[val^n (throw a)] end ↪ val^n (throw a) F; val^n (try bt instr* delegate l) - ↪ F; label_m{} (delegate{l} val^n instr* end) end + ↪ F; delegate{l} (label_m{} val^n instr* end) end (if expand_F(bt) = [t1^n]→[t2^m]) delegate{l} val* end ↪ val* -label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end +B^l[ delegate{l} T[val^n (throw a)] end ] ↪ val^n (throw a) ``` Note that the last reduction step above is similar to the reduction of `br l` [1], 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. +There is a subtle difference though. The instruction `br l` searches for the `l+1` surrounding block and breaks out after that block. +On the contrary, `delegate{l}` should "break and throw" _inside_ the `l+1` label, so we should break one label earlier. +This is why the reduction step for `delegate{l}` has one label less. - [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 @@ -210,9 +211,9 @@ S;C, labels [t2*] ⊢ instr1* : []→[t2*] ----------------------------------------------------------- S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*] -S;C ⊢ instr* : []→[t*] -C.labels[l+1] = [t0*] ------------------------------------------------------- +S;C, labels [t*] ⊢ instr* : []→[t*] +C.labels[l] = [t0*] +--------------------------------------- S;C ⊢ delegate{l} instr* end : []→[t*] S ⊢ tag a : tag [t0*]→[] diff --git a/test/core/try_delegate_minimal_fail.wast b/test/core/try_delegate_minimal_fail.wast new file mode 100644 index 00000000..d8c346bf --- /dev/null +++ b/test/core/try_delegate_minimal_fail.wast @@ -0,0 +1,33 @@ +;; This test fails with the first approach to changing the position of the +;; delegate label. We could ommit the outermost try-catch_all, and get the +;; error: +;; +;; uncaught exception: uncaught exception with args ([]) +;; +;; As it is now, the error is: +;; +;; Result: 27 : i32 +;; Expect: 2 : i32 +;; ../test/core/try_delegate_minimal_fail.wast:22.1-22.77: assertion failure: wrong return values +;; +;; These errors indicate that the delegated exception escaped its target and was +;; caught by the one surrounding it. + + +(module + (tag $tag) + (func (export "delegate-throw-direct") (param i32) (result i32) + (try $outermost (result i32) + (do + (try $innermost (result i32) + (do + (try (result i32) + (do + (local.get 0) + (if (then (throw $tag)) (else)) + (i32.const 1)) + (delegate $innermost))) ;; delegate 0 + (catch $tag (i32.const 2)))) ;; end innermost + (catch $tag (i32.const 27))))) ;; end outermost + +(assert_return (invoke "delegate-throw-direct" (i32.const 1)) (i32.const 2))