#3057. Add more try-finally tests #3145
Conversation
There was a problem hiding this comment.
Here's a comment from Paul about finally blocks that we should keep in mind: dart-lang/sdk#60503 (comment). See also dart-lang/language#4327 that I created in order clarify the situation.
I think it would be useful to block several of these tests for a little while because they depend in such a detailed manner on the flow analysis of try/catch/finally.
Perhaps the most convenient approach would be to make them part of a separate PR.
| /// @description Checks that `before(B2) = split(join(drop(after(B1)), | ||
| /// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`. Test that if | ||
| /// some variable is assigned in a `catch` part of `B1` then it is | ||
| /// "possibly assigned" in `B2`. |
There was a problem hiding this comment.
Same issue: This is try-catch-finally, which needs a separate rule that isn't written at this time.
There was a problem hiding this comment.
I created dart-lang/language#4327 in order to clarify how to deal with try/catch/finally.
| test1() { | ||
| late int i; | ||
| try { | ||
| print("To avoid empty body"); |
There was a problem hiding this comment.
This is new, why would that suddenly be needed?
| test1() { | ||
| late int i; | ||
| try { | ||
| print("To avoid empty body"); |
There was a problem hiding this comment.
This is new, why would that suddenly be needed? It would make sense to have it if we have any indications that an empty try block would be treated differently than a non-empty one (e.g., it might be accepted as a guaranteed property of the empty try block that it won't throw—except that I don't think we have any rules of that nature, it's simply not a likely situation).
There was a problem hiding this comment.
Here i is initialized in a catch block with is guaranteed to be dead code in case of an empty try block. To avoid side effects I made a body of try a non-empty. But probably better approach is not to do this but add a separate test checking empty body of try. I'll update this.
| foo(); | ||
| i = 42; | ||
| } finally { | ||
| i; // Possibly assigned |
There was a problem hiding this comment.
I'd expect before(Si) (each of the "catch bodies") to be a conservativeJoin in the same way as with the try/catch statement, and before(F) where F is the finally block would then be a join of after(B1) and after(Sj) for j in 1 .. k where k is the number of catch clauses (yes, I vaguely prefer numbering 1 .. k over 0 .. k because k is then the number of elements in the list and starting from zero really has no benefit other than in the special case where the index can be the offset into raw memory layout. So it's OK that the first element of an array is [0], but the first (not "zeroth") parameter of a function should be number 1).
So we'd not use conservativeJoin with each catch block, only with the try block. This means that we do not ignore the control flow in each catch block.
Note that Paul also mentioned that there is no join and merge pair, there is only a single operation (I think it's called join), and it does take reachability into account (like the current spec in the case of merge, and unlike the current spec of join).
However, in the finally block we have to take into account that we could arrive there from a normal, returning, continuing, or breaking completion of the try block (that is: nothing was thrown), in which case the finally block will be followed by the same completion. But if the try block did throw then the control flow will include one of the catch blocks (which might throw or complete normally, etc.) or it might not include any catch blocks because none of them is a match (based on the on clause). So there's a lot of complexity in try-catch-finally.
Right now I'll just try to use informal reasoning about which classification should apply (such as 'assigned' or not, or 'unreachable', whatever the test is focusing on).
There was a problem hiding this comment.
With this, I'd say that i = 42 is unreachable code and there is no conservative join, so i is definitely not assigned when we reach finally.
I can see that the analyzer and CFE think otherwise, though. I don't really understand why there would be a need for a conservative join involving each of the catch blocks, but this seems to be what the implementation is doing. I created dart-lang/language#4327 in order to clarify the situation.
There was a problem hiding this comment.
This means that the outcome of the following cases is similarly in need of a clarification.
| /// @description Checks that `before(B2) = split(join(drop(after(B1)), | ||
| /// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`. Test that if | ||
| /// some variable is assigned in a `catch` part of `B1` then it is | ||
| /// "possibly assigned" in `B2`. |
There was a problem hiding this comment.
I think the try/catch/finally tests would need to be blocked for a little while as we're clarifying how they are treated.
There was a problem hiding this comment.
This would apply for all the following test libraries as well.
sgrekhov
added
the
status-blocked
|
Blocked by dart-lang/language#4327 |
No description provided.