diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t03.dart b/TypeSystem/flow-analysis/reachability_for_A01_t03.dart new file mode 100644 index 0000000000..770b152c40 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t03.dart @@ -0,0 +1,46 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that if variable is assigned `after(D)` then it is definitely assigned +/// `before(C)`. +/// @author sgrekhov22@gmail.com + +test1() { + int n; + for (n = 42; n > 0;) { // n definitely assigned + break; + } +} + +test2() { + int n; + [ + for (n = 42; n < 0;) + 0 + ]; +} + +test3() { + int n; + { + for (n = 42; n < 0;) + 0: 0 + }; +} + +main() { + test1(); + test2(); + test3(); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t04.dart b/TypeSystem/flow-analysis/reachability_for_A01_t04.dart new file mode 100644 index 0000000000..f0d5a3ae43 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t04.dart @@ -0,0 +1,70 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that `assignedIn(U)` is detected by flow analysis. +/// @author sgrekhov22@gmail.com + +test1() { + late int n; + for ( + ; + () { + if (1 > 2) { + n; // possibly assigned + } + return true; + }(); + n = 42 + ) {} +} + +test2() { + late int n; + [ + for ( + ; + () { + if (1 > 2) { + n; + } + return true; + }(); + n = 42 + ) + 0, + ]; +} + +test3() { + late int n; + { + for ( + ; + () { + if (1 > 2) { + n; + } + return true; + }(); + n = 42 + ) + 0: 0, + }; +} + +main() { + print(test1); + print(test2); + print(test3); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t05.dart b/TypeSystem/flow-analysis/reachability_for_A01_t05.dart new file mode 100644 index 0000000000..2a29d35299 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t05.dart @@ -0,0 +1,86 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that `assignedIn(S)` is detected by flow analysis. +/// @author sgrekhov22@gmail.com + +test1() { + late int n; + for ( + ; + () { + if (1 > 2) { + n; // possibly assigned + } + return true; + }(); + ) { + n = 42; + } +} + +test2() { + late int n; + [ + for ( + ; + () { + if (1 > 2) { + n; + } + return true; + }(); + ) + n = 42, + ]; +} + +test3() { + late int n; + { + for ( + ; + () { + if (1 > 2) { + n; + } + return true; + }(); + ) + n = 42: 0, + }; +} + +test4() { + late int n; + { + for ( + ; + () { + if (1 > 2) { + n; + } + return true; + }(); + ) + 0: n = 42, + }; +} + +main() { + print(test1); + print(test2); + print(test3); + print(test4); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t06.dart b/TypeSystem/flow-analysis/reachability_for_A01_t06.dart new file mode 100644 index 0000000000..2ba449e6ee --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t06.dart @@ -0,0 +1,52 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that an assignment in `C` doesn't affect value of `before(D)`. +/// @author sgrekhov22@gmail.com + +test1() { + late int n; + for (n; (n = 42) < 0;) { // Definitely unassigned +// ^ +// [analyzer] unspecified +// [cfe] unspecified + break; + } +} + +test2() { + int n; + [ + for (n; (n = 42) < 0;) 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + ]; +} + +test3() { + int n; + { + for (n; (n = 42) < 0;) 0: 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; +} + +main() { + print(test1); + print(test2); + print(test3); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t07.dart b/TypeSystem/flow-analysis/reachability_for_A01_t07.dart new file mode 100644 index 0000000000..4b21d1a78e --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t07.dart @@ -0,0 +1,52 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that an assignment in `U` doesn't affect value of `before(D)`. +/// @author sgrekhov22@gmail.com + +test1() { + late int n; + for (n;; n = 42) { // Definitely unassigned +// ^ +// [analyzer] unspecified +// [cfe] unspecified + break; + } +} + +test2() { + int n; + [ + for (n; ;n = 42) 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + ]; +} + +test3() { + int n; + { + for (n; ;n = 42) 0: 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; +} + +main() { + print(test1); + print(test2); + print(test3); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t08.dart b/TypeSystem/flow-analysis/reachability_for_A01_t08.dart new file mode 100644 index 0000000000..d2b0e12e29 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t08.dart @@ -0,0 +1,64 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that an assignment in `S` doesn't affect value of `before(D)`. +/// @author sgrekhov22@gmail.com + +test1() { + late int n; + for (n;;) { // Definitely unassigned +// ^ +// [analyzer] unspecified +// [cfe] unspecified + n = 42; + break; + } +} + +test2() { + int n; + [ + for (n; ;) n = 42 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + ]; +} + +test3() { + int n; + { + for (n; ;) n = 42: 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; +} + +test4() { + int n; + { + for (n; ;) 0: n = 42 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; +} + +main() { + print(test1); + print(test2); + print(test3); + print(test4); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t09.dart b/TypeSystem/flow-analysis/reachability_for_A01_t09.dart new file mode 100644 index 0000000000..408bda1b2c --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t09.dart @@ -0,0 +1,57 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that if a value of `captured` is `true` in `after(D)` then it is `true` in +/// `before(C)` as well. +/// @author sgrekhov22@gmail.com + +int? x = (2 > 1) ? 1 : null; + +test1(int? n) { + if (n != null) { // n promoted to `int` + for (() {n = x;}; n > 0;) { // n demoted to `int?` +// ^ +// [analyzer] unspecified +// [cfe] unspecified + } + } +} + +test2(int? n) { + if (n != null) { + [ + for (() {n = x;}; n > 0;) 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + ]; + } +} + +test3(int? n) { + if (n != null) { + { + for (() {n = x;}; n > 0;) 0: 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; + } +} + +main() { + print(test1); + print(test2); + print(test3); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t10.dart b/TypeSystem/flow-analysis/reachability_for_A01_t10.dart new file mode 100644 index 0000000000..b1e4ed26c4 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t10.dart @@ -0,0 +1,97 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that `capturedIn(C)` is detected by flow analysis. +/// @author sgrekhov22@gmail.com + +test1(int? n) { + if (n != null) { + // n promoted to `int` + for ( + ; + () { + late int? i = (n = 42); // n demoted to `int?` + return false; + }(); + ) {} + n.isEven; + // ^^^^^^ + // [analyzer] unspecified + // [cfe] unspecified + } +} + +test2(int? n) { + if (n != null) { + [ + for ( + ; + () { + late int? i = (n = 42); + return false; + }(); + ) + 0, + n.isEven, + // ^^^^^^ + // [analyzer] unspecified + // [cfe] unspecified + ]; + } +} + +test3(int? n) { + if (n != null) { + { + for ( + ; + () { + late int? i = (n = 42); + return false; + }(); + ) + 0: 0, + n.isEven: 0, + // ^^^^^^ + // [analyzer] unspecified + // [cfe] unspecified + }; + } +} + +test4(int? n) { + if (n != null) { + { + for ( + ; + () { + late int? i = (n = 42); + return false; + }(); + ) + 0: 0, + 0: n.isEven, + // ^^^^^^ + // [analyzer] unspecified + // [cfe] unspecified + }; + } +} + +main() { + print(test1); + print(test2); + print(test3); + print(test4); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t11.dart b/TypeSystem/flow-analysis/reachability_for_A01_t11.dart new file mode 100644 index 0000000000..7ffe902e2a --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t11.dart @@ -0,0 +1,54 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that `capturedIn(U)` is detected by flow analysis. +/// @author sgrekhov22@gmail.com + +test1(int? n) { + if (n != null) { // n promoted to `int` + for (; n > 0; () {n = 42;}) { // n demoted to `int?` +// ^ +// [analyzer] unspecified +// [cfe] unspecified + } + } +} + +test2(int? n) { + if (n != null) { + [ + for (; n > 0; () {n = 42;}) 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + ]; + } +} + +test3(int? n) { + if (n != null) { + { + for (; n > 0; () {n = 42;}) 0: 0 +// ^ +// [analyzer] unspecified +// [cfe] unspecified + }; + } +} + +main() { + print(test1); + print(test2); + print(test3); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A01_t12.dart b/TypeSystem/flow-analysis/reachability_for_A01_t12.dart new file mode 100644 index 0000000000..46f5fd66bd --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A01_t12.dart @@ -0,0 +1,74 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that +/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test +/// that `capturedIn(S)` is detected by flow analysis. +/// @author sgrekhov22@gmail.com + +int? x = (2 > 1) ? 1 : null; + +test1(int? n) { + if (n != null) { // n promoted to `int` + for (;n > 0 ;) { +// ^ +// [analyzer] unspecified +// [cfe] unspecified + late int? v = (n = x); // n demoted to `int?` + } + } +} + +test2(int? n) { + if (n != null) { + [ + for (;n > 0 ;) +// ^ +// [analyzer] unspecified +// [cfe] unspecified + () { + late int? v = (n = x); + } + ]; + } +} + +test3(int? n) { + if (n != null) { + { + for (; n > 0;) +// ^ +// [analyzer] unspecified +// [cfe] unspecified + () {late int? v = (n = x);}: 0 + }; + } +} + +test4(int? n) { + if (n != null) { + { + for (; n > 0;) +// ^ +// [analyzer] unspecified +// [cfe] unspecified + 0: () {late int? v = (n = x);} + }; + } +} + +main() { + print(test1); + print(test2); + print(test3); + print(test4); +} diff --git a/TypeSystem/flow-analysis/reachability_for_A03_t06.dart b/TypeSystem/flow-analysis/reachability_for_A03_t06.dart new file mode 100644 index 0000000000..c752d476ca --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A03_t06.dart @@ -0,0 +1,26 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that `before(U) = merge(after(S), continue(S))`. Test +/// that if `D`, `C` are empty and `S` breaks, then an assignment in `U` is +/// treated by flow analysis as 'possibly assigned`. +/// @author sgrekhov22@gmail.com + +main() { + late int i; + for (;; i = 42) { // Possibly assigned. https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385 + break; + } + try { + i; // Runtime error, Ok + } catch (_) {} +} diff --git a/TypeSystem/flow-analysis/reachability_for_A03_t07.dart b/TypeSystem/flow-analysis/reachability_for_A03_t07.dart new file mode 100644 index 0000000000..ad593d93ea --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_for_A03_t07.dart @@ -0,0 +1,26 @@ +// 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 for statement: If `N` is a for statement of the form +/// `for (D; C; U) S,` then: +/// - Let `before(D) = before(N)`. +/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))` +/// - Let `before(S) = split(true(C))`. +/// - Let `before(U) = merge(after(S), continue(S))`. +/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))` +/// +/// @description Checks that `before(U) = merge(after(S), continue(S))`. Test +/// that if `D`, `C` are empty and variable is assigned in `S` after `continue`, +/// then this variable is treated in `U` as 'possibly assigned`. +/// @author sgrekhov22@gmail.com + +main() { + late int i; + try { + for (;; i) { // Possibly assigned. https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385 + continue; + i = 42; + } + } catch (_) {} +}