Flow analysis of try/catch/finally seems to use a conservative join too broadly

[eernstg]

The flow analysis feature specification specifies the treatment of a try/catch statement and the treatment of a try/finally statement, but the try/catch/finally statement hasn't been specified yet (I don't think it will work to read any of the two existing rules as a rule that also covers try/catch/finally).

We have an adjusted rule for the try/finally statement:

• try finally: If N is a try/finally statement of the form try B1 finally B2 then:
  • Let before(B1) = before(N)
  • Let before(B2) = join(after(B1), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1)))
  • Let after(N) = attachFinally(after(B1), before(B2), after(B2)).

The attachFinally function is complex, but it basically compares the before and after of B2 (the finally block) and treats that as a flow model increment which is applied to each of the predecessors in the control flow graph, no matter how they're completing.

This would need to be generalized somewhat in order to handle the case where we have both try, catch, and finally.

The try/catch case is handled as follows:

• try catch: If N is a try/catch statement of the form try B alternatives then:
  • Let before(B) = before(N)
  • For each catch block on Ti Si in alternatives:
    • Let before(Si) = conservativeJoin(before(N), assignedIn(B), capturedIn(B))
  • Let after(N) = join(after(B), after(C0), ..., after(Ck))

This seems to imply that the conservative join would be used with the try block in order to take into account that this part may have many different control flow edges out of the block and into any of the catch clauses. However, each catch block is subject to normal flow analysis (there is no need for a conservative join here).

We might then be able to use something along these lines:

• try catch finally: If N is a try/catch/finally statement of the form try B1 alternatives finally F then:
  • Let before(B1) = before(N)
  • Let before(Si) = join(after(B1), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))), where Si is the body of the i'th alternative
  • Let after(N) = join(attachFinally(after(B1), before(F), after(F)), M1 .. Mk) where Mj = attachFinally(after(Sj), before(F), after(F))

@stereotype441, WDYT? It seems likely to me that using attachFinally first and then join would yield a more precise analysis than the opposite ordering. Is this compatible with the existing implementation?

[stereotype441]

Unfortunately, it looks like what's documented in the spec for try/catch also fails to match the implementation. Here's what's currently implemented for try/catch.

• try catch: If N is a try/catch statement of the form try B alternatives then:
  • Let before(B) = split(before(N))
  • For each catch block on Ti Si in alternatives:
    • Let before(Si) = conservativeJoin(before(B), assignedIn(B), capturedIn(B))
  • Let after(N) = unsplit(join(after(B), after(S0), ..., after(Sk)))

(The primary difference is the presence of split and unsplit. Also, the last line mentions S0...Sk instead of C0...Ck; I'm pretty sure that's just a typographical error in the current spec though, because C0...Ck are undefined 😃.)

The way the implementation currently handles try/catch/finally is to desugar them into a try/catch nested inside a try/finally. So if we fuse together the adjusted rules for try/catch and try/finally, the effect is:

• try catch finally: If N is a try/catch/finally statement of the form try B1 alternatives finally F then:
  • Let before(B1) = split(before(N))
  • For each catch block on Ti Si in alternatives:
    • Let before(Si) = conservativeJoin(before(B1), assignedIn(B1), capturedIn(B1)) (B1' represents the implicit nested try/catch statement)
  • Let after(B1') = unsplit(join(after(B1), after(S0), ..., after(Sk)))
  • Let before(F) = join(after(B1'), conservativeJoin(before(N), assignedIn(B1'), capturedIn(B1')))
  • Let after(N) = attachFinally(after(B1'), before(F), after(F)).

Contrasting that with your proposal:

• try catch finally: If N is a try/catch/finally statement of the form try B1 alternatives finally F then:

  • Let before(B1) = before(N)
  • Let before(Si) = join(after(B1), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))), where Si is the body of the i'th alternative
  • Let after(N) = join(attachFinally(after(B1), before(F), after(F)), M1 .. Mk) where Mj = attachFinally(after(Sj), before(F), after(F))

Here are the differences I see:

• Your proposal is missing the split in before(B1). That's easily fixed.
• Your proposal is missing the definition of before(F). Let's assume we take my definition, which is before(F) = join(after(B1'), conservativeJoin(before(N), assignedIn(B1'), capturedIn(B1'))), where after(B1') = unsplit(join(after(B1), after(S0), ..., after(Sk))).
• As you mentioned, your proposal separately uses attachFinally on each exit from the implicit nested try/catch statement, and then joins the results, whereas what was implemented joins the exits from the implicit nested try/catch statement first, and then uses attachFinally on the result.

@stereotype441, WDYT? It seems likely to me that using attachFinally first and then join would yield a more precise analysis than the opposite ordering.

Can you say more about your thoughts here? I'm having trouble coming up with an example where there is an observable difference. But that could just be a failure of imagination on my part!

Is this compatible with the existing implementation?

Depends what you mean by "compatible" I guess. It's different from the existing implementation, that's for sure. But like I said, I'm having trouble coming up with an example where there is an observable difference.

Taking a step back, one of the mistakes I feel like I've made in my past efforts to write a formal spec for flow analysis was that I didn't do a great job in separating the tasks of:

• Writing down how flow analysis behaves today, and
• Thinking about possible improvements to flow analysis we might want to make tomorrow.

And I think the result of my not doing a good job of separating those tasks is that we got into this messy situation we're in today, where the flow analysis spec doesn't match the behavior of any version of Dart we've had in the past, nor does it match the behavior of any version of Dart we expect to have in the future. It's a mishmash of speculations (sometimes correct, sometimes not) about how people thought flow analysis behaved at some point in the past, along with ideas about how flow analysis ought to behave (some of which have been implemented, some of which haven't). Which makes the whole spec really difficult to reason about.

For this specific question of how we handle try/catch/finally, I would like to start by updating the spec to match what the implementation currently does. We could do that pretty simply, e.g.:

• try catch finally: If N is a try/catch/finally statement of the form try B1 alternatives finally F then it is analyzed as though the equivalent statement try { try B1 alternatives } finally F had been written.¹

Once we've updated the spec to match the implementation, I'm open to considering an improvement to try/catch/finally handling, but to be honest, even if we can find some code where there's an observable difference, I suspect it'll probably be tough to convince me that the improvement is worth the implementation effort. The existing desugaring approach has the advantage of being really simple implementation-wise, and I think it does a pretty good job.

Footnotes

1. Note that in the past, I've usually argued pretty strongly that we shouldn't write our specs in terms of desugaring. Why am I having a change of heart here? Because this is one of the rare cases where specifying it as a desugaring is actually a very close approximation of what the implementation does. See for instance https://github.com/dart-lang/sdk/blob/42a55d9d790dcd0eb24f1cb9ee941319f1f3890f/pkg/front_end/lib/src/type_inference/inference_visitor.dart#L9268. Although the implementation doesn't actually create the desugared AST try { try B1 alternatives } finally F, you can see that the calls to flowAnalysis are precisely the same as they would be if it had done so. ↩