dart-lang#3057. Update operator == tests updated and add new ones

TypeSystem/flow-analysis/reachability_A08_t01.dart

@@ -2,30 +2,44 @@
 // 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 [email protected]
 /// @issue 41985
 
 // Requirements=nnbd-strong
 
 main() {
   int i;
-  Null n = null;
-  if (n == null) {
+  Null n1 = null;
+  Null n2 = null;
+  if (n1 == n2) {
     i = 42; // condition is always true therefore `i` must be definitely assigned
   }
   i; // It's not an error to read local non-nullable variable if it is definitely assigned

TypeSystem/flow-analysis/reachability_A08_t02.dart

@@ -2,31 +2,45 @@
 // 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 [email protected]
 /// @issue 41985
 
 // Requirements=nnbd-strong
 
-Null get n => null;
+Null get n1 => null;
 
 main() {
   int i;
-  if (n == null) {
+  Null n2;
+  if (n1 == n2) {
     i = 42; // condition is always true therefore `i` must be definitely assigned
   }
   i; // It's not an error to read local non-nullable variable if it is definitely assigned

TypeSystem/flow-analysis/reachability_A08_t03.dart

@@ -0,0 +1,65 @@
+// 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 [email protected]
+/// @issue 60114
+
+// Requirements=nnbd-strong
+
+test1<T extends Null>(T t) {
+  late int i;
+  String s = "";
+  if (s == t) {  // ignore: unnecessary_null_comparison
+    i = 42; // `i` is definitely unassigned
+  }
+  i;
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+test2<T extends Null>(T t) {
+  late int i;
+  String s = "";
+  if (t == s) {  // ignore: unnecessary_null_comparison
+    i = 42;
+  }
+  i;
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test1);
+  print(test2);
+}

TypeSystem/flow-analysis/reachability_A08_t04.dart

@@ -2,39 +2,47 @@
 // 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 [email protected]
 /// @issue 41981
+/// @issue 60114
 
 // Requirements=nnbd-strong
 
-import "../../Utils/expect.dart";
-
 main() {
   late int i;
   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
   }
+  i;
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
 }

TypeSystem/flow-analysis/reachability_A08_t05.dart

@@ -2,40 +2,48 @@
 // 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 [email protected]
 /// @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
+  if (null == s) {  // ignore: unnecessary_null_comparison
+    i = 42; // `i` is definitely unassigned
   }
+  i;
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
 }