Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
53 changes: 37 additions & 16 deletions TypeSystem/flow-analysis/reachability_A08_t01.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,31 +2,52 @@
// 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 Variable or getter: If N is an expression of the form x where the
/// type of x is T then:
/// @assertion operator== If `N` is an expression of the form `E1 == E2`, where
/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
/// - Let `before(E1) = before(N)`.
/// - Let `before(E2) = after(E1)`.
/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = unreachable(after(E2))`.
/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or
/// `equivalentToNull(T2)` and `T1` is non-nullable, then:
/// - Let `true(N) = unreachable(after(E2))`.
/// - Let `false(N) = after(E2)`.
/// - Otherwise, if `stripParens(E1)` is a `null` literal, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = promoteToNonNull(E2, after(E2))`.
/// - Otherwise, if `stripParens(E2)` is a `null` literal, then:
/// - Let `true(N) = after(E1)`.
/// - Let `false(N) = promoteToNonNull(E1, after(E2))`.
/// - Otherwise:
/// - Let after(N) = after(E2).
/// Note that it is tempting to generalize the two `null` literal cases to apply
/// to any expression whose type is `Null`, but this would be unsound in cases
/// where `E2` assigns to `x`. (Consider, for example,
/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call
/// `null.isEven` in the event of a non-null input).
///
/// If T <: Never then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T <: Null then:
/// Let null(N) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T is non-nullable then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = before(N).
///
/// @description Checks reachability after variable or getter. Test variable of
/// type Null
/// @description Checks that if `equivalentToNull(T1)` and
/// `equivalentToNull(T2)`, then `true(N) = after(E2)` and
/// `false(N) = unreachable(after(E2))`.
/// @author sgrekhov@unipro.ru
/// @issue 41985

// Requirements=nnbd-strong

main() {
int i;
Null n = null;
if (n == null) {
late int j;
Null n1 = null;
Null n2 = null;
if (n1 == n2) {
i = 42; // condition is always true therefore `i` must be definitely assigned
} else {
j = 42;
}
i; // It's not an error to read local non-nullable variable if it is definitely assigned
j; // Still definitely unassigned
//^
// [analyzer] unspecified
// [cfe] unspecified
}
53 changes: 37 additions & 16 deletions TypeSystem/flow-analysis/reachability_A08_t02.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,32 +2,53 @@
// 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 Variable or getter: If N is an expression of the form x where the
/// type of x is T then:
/// @assertion operator== If `N` is an expression of the form `E1 == E2`, where
/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
/// - Let `before(E1) = before(N)`.
/// - Let `before(E2) = after(E1)`.
/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = unreachable(after(E2))`.
/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or
/// `equivalentToNull(T2)` and `T1` is non-nullable, then:
/// - Let `true(N) = unreachable(after(E2))`.
/// - Let `false(N) = after(E2)`.
/// - Otherwise, if `stripParens(E1)` is a `null` literal, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = promoteToNonNull(E2, after(E2))`.
/// - Otherwise, if `stripParens(E2)` is a `null` literal, then:
/// - Let `true(N) = after(E1)`.
/// - Let `false(N) = promoteToNonNull(E1, after(E2))`.
/// - Otherwise:
/// - Let after(N) = after(E2).
/// Note that it is tempting to generalize the two `null` literal cases to apply
/// to any expression whose type is `Null`, but this would be unsound in cases
/// where `E2` assigns to `x`. (Consider, for example,
/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call
/// `null.isEven` in the event of a non-null input).
///
/// If T <: Never then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T <: Null then:
/// Let null(N) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T is non-nullable then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = before(N).
///
/// @description Checks reachability after variable or getter. Test getter of
/// type Null
/// @description Checks that if `equivalentToNull(T1)` and
/// `equivalentToNull(T2)`, then `true(N) = after(E2)` and
/// `false(N) = unreachable(after(E2))`. Test getter of type `Null`.
/// @author sgrekhov@unipro.ru
/// @issue 41985

// Requirements=nnbd-strong

Null get n => null;
Null get n1 => null;

main() {
int i;
if (n == null) {
late int j;
Null n2;
if (n1 == n2) {
i = 42; // condition is always true therefore `i` must be definitely assigned
} else {
j = 42;
}
i; // It's not an error to read local non-nullable variable if it is definitely assigned
j; // Still definitely unassigned
//^
// [analyzer] unspecified
// [cfe] unspecified
}
73 changes: 73 additions & 0 deletions TypeSystem/flow-analysis/reachability_A08_t03.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
// 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 operator== If `N` is an expression of the form `E1 == E2`, where
/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
/// - Let `before(E1) = before(N)`.
/// - Let `before(E2) = after(E1)`.
/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = unreachable(after(E2))`.
/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or
/// `equivalentToNull(T2)` and `T1` is non-nullable, then:
/// - Let `true(N) = unreachable(after(E2))`.
/// - Let `false(N) = after(E2)`.
/// - Otherwise, if `stripParens(E1)` is a `null` literal, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = promoteToNonNull(E2, after(E2))`.
/// - Otherwise, if `stripParens(E2)` is a `null` literal, then:
/// - Let `true(N) = after(E1)`.
/// - Let `false(N) = promoteToNonNull(E1, after(E2))`.
/// - Otherwise:
/// - Let after(N) = after(E2).
/// Note that it is tempting to generalize the two `null` literal cases to apply
/// to any expression whose type is `Null`, but this would be unsound in cases
/// where `E2` assigns to `x`. (Consider, for example,
/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call
/// `null.isEven` in the event of a non-null input).
///
/// @description Checks that if `equivalentToNull(T1)` and `T2` is non-nullable,
/// or `equivalentToNull(T2)` and `T1` is non-nullable then
/// `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`.
/// @author sgrekhov22@gmail.com
/// @issue 60114

// Requirements=nnbd-strong

test1<T extends Null>(T t) {
late int i;
int j;
String s = "";
if (s == t) { // ignore: unnecessary_null_comparison
i = 42; // `i` is definitely unassigned
} else {
j = 42;
}
i;
//^
// [analyzer] unspecified
// [cfe] unspecified
j; // Definitely assigned
}

test2<T extends Null>(T t) {
late int i;
int j;
String s = "";
if (t == s) { // ignore: unnecessary_null_comparison
i = 42;
} else {
j = 42;
}
i;
//^
// [analyzer] unspecified
// [cfe] unspecified
j;
}

main() {
print(test1);
print(test2);
}
62 changes: 37 additions & 25 deletions TypeSystem/flow-analysis/reachability_A08_t04.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,39 +2,51 @@
// 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 Variable or getter: If N is an expression of the form x where the
/// type of x is T then:
/// @assertion operator== If `N` is an expression of the form `E1 == E2`, where
/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
/// - Let `before(E1) = before(N)`.
/// - Let `before(E2) = after(E1)`.
/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = unreachable(after(E2))`.
/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or
/// `equivalentToNull(T2)` and `T1` is non-nullable, then:
/// - Let `true(N) = unreachable(after(E2))`.
/// - Let `false(N) = after(E2)`.
/// - Otherwise, if `stripParens(E1)` is a `null` literal, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = promoteToNonNull(E2, after(E2))`.
/// - Otherwise, if `stripParens(E2)` is a `null` literal, then:
/// - Let `true(N) = after(E1)`.
/// - Let `false(N) = promoteToNonNull(E1, after(E2))`.
/// - Otherwise:
/// - Let after(N) = after(E2).
/// Note that it is tempting to generalize the two `null` literal cases to apply
/// to any expression whose type is `Null`, but this would be unsound in cases
/// where `E2` assigns to `x`. (Consider, for example,
/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call
/// `null.isEven` in the event of a non-null input).
///
/// If T <: Never then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T <: Null then:
/// Let null(N) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T is non-nullable then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = before(N).
///
/// @description Checks reachability after variable or getter. Test non-nullable
/// type
/// @description Checks that if `equivalentToNull(T2)` and `T1` is non-nullable,
/// then `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`.
/// @author sgrekhov@unipro.ru
/// @issue 41981
/// @issue 60114

// Requirements=nnbd-strong

import "../../Utils/expect.dart";

main() {
late int i;
int j;
String s = "";
if (s == null) {
i = 42; // `i` is not definitely unassigned because in a weak mode the
// condition may be true
}
try {
i;
Expect.fail("Error expected");
} on Error catch(e) {
// Ok
if (s == null) { // ignore: unnecessary_null_comparison
i = 42; // `i` is definitely unassigned
} else {
j = 42;
}
i;
//^
// [analyzer] unspecified
// [cfe] unspecified
j;
}
62 changes: 37 additions & 25 deletions TypeSystem/flow-analysis/reachability_A08_t05.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,40 +2,52 @@
// 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 Variable or getter: If N is an expression of the form x where the
/// type of x is T then:
/// @assertion operator== If `N` is an expression of the form `E1 == E2`, where
/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
/// - Let `before(E1) = before(N)`.
/// - Let `before(E2) = after(E1)`.
/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = unreachable(after(E2))`.
/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or
/// `equivalentToNull(T2)` and `T1` is non-nullable, then:
/// - Let `true(N) = unreachable(after(E2))`.
/// - Let `false(N) = after(E2)`.
/// - Otherwise, if `stripParens(E1)` is a `null` literal, then:
/// - Let `true(N) = after(E2)`.
/// - Let `false(N) = promoteToNonNull(E2, after(E2))`.
/// - Otherwise, if `stripParens(E2)` is a `null` literal, then:
/// - Let `true(N) = after(E1)`.
/// - Let `false(N) = promoteToNonNull(E1, after(E2))`.
/// - Otherwise:
/// - Let after(N) = after(E2).
/// Note that it is tempting to generalize the two `null` literal cases to apply
/// to any expression whose type is `Null`, but this would be unsound in cases
/// where `E2` assigns to `x`. (Consider, for example,
/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call
/// `null.isEven` in the event of a non-null input).
///
/// If T <: Never then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T <: Null then:
/// Let null(N) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise if T is non-nullable then:
/// Let null(N) = unreachable(before(N)).
/// Let notNull(N) = before(N).
///
/// @description Checks reachability after variable or getter. Test getter of
/// non-nullable type
/// @description Checks that if `equivalentToNull(T1)` and `T2` is non-nullable,
/// then `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`.
/// @author sgrekhov@unipro.ru
/// @issue 41981
/// @issue 60114

// Requirements=nnbd-strong

import "../../Utils/expect.dart";

String get s => "Lily was here";

main() {
late int i;
if (s == null) {
i = 42; // `i` is not definitely unassigned because in a weak mode the
// condition may be true
}
try {
i;
Expect.fail("Error expected");
} on Error catch(e) {
// Ok
int j;
if (null == s) { // ignore: unnecessary_null_comparison
i = 42; // `i` is definitely unassigned
} else {
j = 42;
}
i;
//^
// [analyzer] unspecified
// [cfe] unspecified
j; // Definitely assigned
}
Loading