Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Attempt to put the try-delegate label after delegate{l} (failing tests) #220

Closed

Commits on Sep 2, 2022

  1. Attempt to have the try-delegate label after delegate{l} (failing t…

    …ests)
    
    [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](WebAssembly#205 (comment))
    [discussions](https://github.com/WebAssembly/exception-handling/pull/143/files#r812476148) of WebAssembly#205 and WebAssembly#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.
    ioannad committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    01c1253 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2022

  1. Apply suggestions from code review

    Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
    ioannad and rossberg committed Oct 7, 2022
    Configuration menu
    Copy the full SHA
    47acd18 View commit details
    Browse the repository at this point in the history