From 01c1253f9463a74e500cfe149f98b7ed07aba3d3 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Wed, 31 Aug 2022 05:17:07 +0200 Subject: [PATCH 1/2] Attempt to have the try-delegate label after `delegate{l}` (failing tests) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit [Currently](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md) `(try ... delegate l)` reduces to `(label_n{} ( delegate{l} ... end ) end)`, so by putting a label outside (i.e., before) the administrative `delegate{l}`. An idea proposed in past [unresolved](https://github.com/WebAssembly/exception-handling/pull/205#issuecomment-1055173912) [discussions](https://github.com/WebAssembly/exception-handling/pull/143/files#r812476148) of #205 and #143, is to simplify and improve the formalism by instead putting the delegate label inside (i.e., after) the `delegate{l}`. So instead to reduce to `(delegate{l} ( label_n{} ... end ) end)`. TL;DR ----- I can't seem to make it work. This PR explored an approach to implement this idea, in the [formal overview file ](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md), as well as in the interpreter, but had failing tests which I wasn't able to fix. Perhaps I'm overseeing some other solution or approach, or there is some mistake in the interpreter implementation and/or argumentation below. Details ------- I think the problem is as follows. With the current [definition of block contexts](https://webassembly.github.io/exception-handling/core/exec/runtime.html#block-contexts), the instruction sequence `B^l[ delegate{l} T[val^n (throw a)] end ]` not only is ambiguous, but doesn't work with a try-catch label located outside of the try-catch. Take for example the following possible reduction. ``` (try (try (throw x) delegate 0) catch x end) ↪ (label_0{} (catch{a_x ε} (delegate{0} (label_0{} (throw a_x) end) end) end) end) ``` The intention for this delegate is to throw inside the handler `catch{a_x ε}` and be caught there. However, a possible `B^0` for the reduction of `delegate{0}` is `B^0 = [_] catch{a_x ε}`, in which case the reduction rule gives the following. ``` ↪ (label_0{} (throw a_x) end) ↪ (throw a_x) ``` The issue here seems to be that there is no label between the `delegate{l}` and the `catch{...}`. Perhaps there is a different change we can easily make it work, for example changing control contexts or block contexts? Failing tests ............. We can observe the above wrong behaviour also in the interpreter tests, although this could be fixable somehow. In particular, the first commit of this PR has the formal overview changes also implemented in the execution steps of the interpreter (in `interpreter/exec/eval.ml`): - The reduction of `try ... delegate l` puts the `label{}` after the `delegate{l}`. - The reduction of `delegate{l}` does not pattern match for an initial label. I tried to minimise a failing test from `test/core/try_delegate.wast` in the file `test/core/try_delegate_minimal_fail.wast`. To reproduce the failure build the interpreter and run the above test file as follows, for example from a Linux terminal in the base directory of the repository: ``` cd interpreter make ./wasm ../test/core/try_delegate_minimal_fail.wast ``` See also comments in the test file. --- interpreter/exec/eval.ml | 7 ++-- .../Exceptions-formal-overview.md | 15 +++++---- test/core/try_delegate_minimal_fail.wast | 33 +++++++++++++++++++ 3 files changed, 46 insertions(+), 9 deletions(-) create mode 100644 test/core/try_delegate_minimal_fail.wast 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)) From 47acd18e914f367db3e92f8edcd25154dc11a67c Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 7 Oct 2022 16:58:38 +0200 Subject: [PATCH 2/2] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- proposals/exception-handling/Exceptions-formal-overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 28136ca1..5db955e6 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -211,7 +211,7 @@ S;C, labels [t2*] ⊢ instr1* : []→[t2*] ----------------------------------------------------------- S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*] -S;C, labels [t*] ⊢ instr* : []→[t*] +S;C ⊢ instr* : []→[t*] C.labels[l] = [t0*] --------------------------------------- S;C ⊢ delegate{l} instr* end : []→[t*]