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

[ioannad]

Currently (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 discussions 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 , 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, 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.

[rossberg]

Okay, I think I see the problem. More broadly, when catch and delegate use inconsistent ordering of their associated label, then delegate cannot work correctly for both of them as a target at the same time. So this again is our hack for catch backfiring.

So I suggest leaving it alone. Until I can perhaps think of a way to fix the hack. :)

(I have again been thinking about decoupling the mess by introducing a separate rethrow context, which just records the set of labels that can be targeted by rethrow. That would allow us to eliminate the label kind and order catch/delegate/caught labels in the natural way. However, the trouble with this is that we'd have to shift the indices in this set whenever a label is added to the context. Perhaps that can be factored into a single rule for typing "blocks", though. Still kind of ugly.)

[ioannad]

As mentioned in this comment, I am closing this PR, leaving the spec as it is.