Skip to content

#3057. Add more try-finally tests #3145

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.

Sign up for GitHub

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

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

#3057. Add more try-finally tests #3145

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
403d439
#3057. Add more try-finally tests
sgrekhov Apr 14, 2025
09b4244
Rename to try_catch_finally_*, change assertions
sgrekhov Apr 16, 2025
b6e6490
Add TODO
sgrekhov Apr 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion TypeSystem/flow-analysis/reachability_try_finally_A02_t04.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ test1(int? n) {
test2(int? n) {
if (n != null) {
try {
() {(n,) = (42,);};
() {(n,) = (42,);};
} finally {
n.isEven;
// ^^^^^^
Expand Down
78 changes: 78 additions & 0 deletions TypeSystem/flow-analysis/reachability_try_finally_A02_t05.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion try finally: If `N` is a try/finally statement of the form
/// `try B1 finally B2` then:
/// - Let `before(B1) = split(before(N))`
/// - Let `before(B2) = split(join(drop(after(B1)),
/// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`
/// - Let `after(N) = restrict(after(B1), after(B2), assignedIn(B2))`
///
/// @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`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same issue: This is try-catch-finally, which needs a separate rule that isn't written at this time.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I created dart-lang/language#4327 in order to clarify how to deal with try/catch/finally.

/// @author [email protected]

class C {
int v;
C(this.v);
}

Never foo() => throw "Never";

test1() {
late int i;
try {
print("To avoid empty body");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is new, why would that suddenly be needed?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

} catch (_) {
foo();
i = 42;
} finally {
i; // Possibly assigned
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This means that the outcome of the following cases is similarly in need of a clarification.

}
}

test2(Never n) {
late int i;
try {
print("To avoid empty body");
} catch (_) {
n;
(i,) = (42,);
} finally {
i;
}
}

test3<T extends Never>(T n) {
late int i;
try {
print("To avoid empty body");
} catch (_) {
n;
(x: i) = (x: 42);
} finally {
i;
}
}

test4() {
late int i;
try {
print("To avoid empty body");
} catch (_) {
foo();
C(v: i) = C(42);
} finally {
i;
}
}

main() {
print(test1);
print(test2);
print(test3);
print(test4);
}
80 changes: 80 additions & 0 deletions TypeSystem/flow-analysis/reachability_try_finally_A02_t06.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion try finally: If `N` is a try/finally statement of the form
/// `try B1 finally B2` then:
/// - Let `before(B1) = split(before(N))`
/// - Let `before(B2) = split(join(drop(after(B1)),
/// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`
/// - Let `after(N) = restrict(after(B1), after(B2), assignedIn(B2))`
///
/// @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`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the try/catch/finally tests would need to be blocked for a little while as we're clarifying how they are treated.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would apply for all the following test libraries as well.

/// @author [email protected]

class C {
int v;
C(this.v);
}

test1() {
late int i;
try {
print("To avoid empty body");
} catch (_) {
if (false) {
i = 42;
}
} finally {
i; // Possibly assigned
}
}

test2() {
late int i;
try {
print("To avoid empty body");
} catch (_) {
if (false) {
(i, ) = (42, );
}
} finally {
i;
}
}

test3() {
late int i;
try {
print("To avoid empty body");
} catch (_) {
if (false) {
(x: i) = (x: 42);
}
} finally {
i;
}
}

test4() {
late int i;
try {
print("To avoid empty body");
} catch (_) {
if (false) {
C(v: i) = C(42);
}
} finally {
i;
}
}

main() {
print(test1);
print(test2);
print(test3);
print(test4);
}
84 changes: 84 additions & 0 deletions TypeSystem/flow-analysis/reachability_try_finally_A02_t07.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion try finally: If `N` is a try/finally statement of the form
/// `try B1 finally B2` then:
/// - Let `before(B1) = split(before(N))`
/// - Let `before(B2) = split(join(drop(after(B1)),
/// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`
/// - Let `after(N) = restrict(after(B1), after(B2), assignedIn(B2))`
///
/// @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`.
/// @author [email protected]

class C {
int v;
C(this.v);
}

test1() {
int i;
try {
print("To avoid empty body");
} catch (_) {
i = 42;
} finally {
i; // Possibly assigned
// ^
// [analyzer] unspecified
// [cfe] unspecified
}
}

test2() {
int i;
try {
print("To avoid empty body");
} catch (_) {
(i,) = (42,);
} finally {
i;
// ^
// [analyzer] unspecified
// [cfe] unspecified
}
}

test3() {
int i;
try {
print("To avoid empty body");
} catch (_) {
(x: i) = (x: 42);
} finally {
i;
// ^
// [analyzer] unspecified
// [cfe] unspecified
}
}

test4() {
int i;
try {
print("To avoid empty body");
} catch (_) {
C(v: i) = C(42);
} finally {
i;
// ^
// [analyzer] unspecified
// [cfe] unspecified
}
}

main() {
print(test1);
print(test2);
print(test3);
print(test4);
}
88 changes: 88 additions & 0 deletions TypeSystem/flow-analysis/reachability_try_finally_A02_t08.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion try finally: If `N` is a try/finally statement of the form
/// `try B1 finally B2` then:
/// - Let `before(B1) = split(before(N))`
/// - Let `before(B2) = split(join(drop(after(B1)),
/// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`
/// - Let `after(N) = restrict(after(B1), after(B2), assignedIn(B2))`
///
/// @description Checks that `before(B2) = split(join(drop(after(B1)),
/// conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))`. Test that if
/// some promoted variable is captured in a `catch` part of `B1` then it is
/// demoted in `B2`.
/// @author [email protected]

class C {
int v;
C(this.v);
}

test1(int? n) {
if (n != null) { // `n` promoted to `int`
try {
print("To avoid empty body");
} catch (_) {
() {n = 42;}; // `n` demoted to `int?`
} finally {
n.isEven;
// ^^^^^^
// [analyzer] unspecified
// [cfe] unspecified
}
}
}

test2(int? n) {
if (n != null) {
try {
print("To avoid empty body");
} catch (_) {
() {(n,) = (42,);};
} finally {
n.isEven;
// ^^^^^^
// [analyzer] unspecified
// [cfe] unspecified
}
}
}

test3(int? n) {
if (n != null) {
try {
print("To avoid empty body");
} catch (_) {
() {(x: n) = (x: 42);};
} finally {
n.isEven;
// ^^^^^^
// [analyzer] unspecified
// [cfe] unspecified
}
}
}

test4(int? n) {
if (n != null) {
try {
print("To avoid empty body");
} catch (_) {
() {C(v: n) = C(42);};
} finally {
n.isEven;
// ^^^^^^
// [analyzer] unspecified
// [cfe] unspecified
}
}
}

main() {
print(test1);
print(test2);
print(test3);
print(test4);
}
Loading