From 3fcdc4e21aabe27c0f5ceb674048c9f90ac746ba Mon Sep 17 00:00:00 2001 From: sgrekhov Date: Sun, 9 Feb 2025 14:25:24 +0200 Subject: [PATCH 1/2] #3057. Add more flow analysis tests for type Never --- .../flow-analysis/reachability_A01_t01.dart | 26 +++++-------- .../flow-analysis/reachability_A01_t02.dart | 25 +++++------- .../flow-analysis/reachability_A01_t11.dart | 34 +++++++++++++++++ .../flow-analysis/reachability_A01_t12.dart | 38 +++++++++++++++++++ .../flow-analysis/reachability_A01_t13.dart | 31 +++++++++++++++ .../flow-analysis/reachability_A01_t14.dart | 35 +++++++++++++++++ .../flow-analysis/reachability_A01_t15.dart | 31 +++++++++++++++ .../flow-analysis/reachability_A01_t16.dart | 31 +++++++++++++++ 8 files changed, 220 insertions(+), 31 deletions(-) create mode 100644 TypeSystem/flow-analysis/reachability_A01_t11.dart create mode 100644 TypeSystem/flow-analysis/reachability_A01_t12.dart create mode 100644 TypeSystem/flow-analysis/reachability_A01_t13.dart create mode 100644 TypeSystem/flow-analysis/reachability_A01_t14.dart create mode 100644 TypeSystem/flow-analysis/reachability_A01_t15.dart create mode 100644 TypeSystem/flow-analysis/reachability_A01_t16.dart diff --git a/TypeSystem/flow-analysis/reachability_A01_t01.dart b/TypeSystem/flow-analysis/reachability_A01_t01.dart index afe3894b66..95696c4a21 100644 --- a/TypeSystem/flow-analysis/reachability_A01_t01.dart +++ b/TypeSystem/flow-analysis/reachability_A01_t01.dart @@ -2,21 +2,16 @@ // 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. /// -/// 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 Never +/// @description Checks that the code is unreachable after a variable of type +/// `Never`. /// @author sgrekhov@unipro.ru void test(Never n) { @@ -35,6 +30,5 @@ void test(Never n) { main() { try { test(throw "Lily was here"); - } catch (_) { - } + } catch (_) {} } diff --git a/TypeSystem/flow-analysis/reachability_A01_t02.dart b/TypeSystem/flow-analysis/reachability_A01_t02.dart index bcf6f4411c..3afcac910d 100644 --- a/TypeSystem/flow-analysis/reachability_A01_t02.dart +++ b/TypeSystem/flow-analysis/reachability_A01_t02.dart @@ -2,21 +2,16 @@ // 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. /// -/// 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 Never +/// @description Checks that the code is unreachable after the invocation of a +/// getter of type `Never`. /// @author sgrekhov@unipro.ru Never get n => throw "Lily was here"; @@ -30,7 +25,7 @@ main() { i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned } i; // It is an error to read a local late variable when it is definitely unassigned. -//^ +// ^ // [analyzer] unspecified // [cfe] unspecified } catch (_) {} diff --git a/TypeSystem/flow-analysis/reachability_A01_t11.dart b/TypeSystem/flow-analysis/reachability_A01_t11.dart new file mode 100644 index 0000000000..b776f5b2e4 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t11.dart @@ -0,0 +1,34 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks that the code is unreachable after a variable of type +/// `T <: Never`. +/// @author sgrekhov22@gmail.com + +void test(T n) { + late int i; + bool b = (() => true)(); + if (b) { + n; // The code after this point is unreachable + i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } + i; // It is an error to read a local late variable when it is definitely unassigned. +//^ +// [analyzer] unspecified +// [cfe] unspecified +} + +main() { + try { + test(throw "Lily was here"); + } catch (_) {} +} diff --git a/TypeSystem/flow-analysis/reachability_A01_t12.dart b/TypeSystem/flow-analysis/reachability_A01_t12.dart new file mode 100644 index 0000000000..624b1d880f --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t12.dart @@ -0,0 +1,38 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks that the code is unreachable after the invocation of a +/// getter of type `T <: Never`. +/// @author sgrekhov22@gmail.com + +class C { + T get n => throw "Lily was here"; + + test() { + try { + late int i; + bool b = (() => true)(); + if (b) { + n; // The code after this point is unreachable + i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } + i; // It is an error to read a local late variable when it is definitely unassigned. +// ^ +// [analyzer] unspecified +// [cfe] unspecified + } catch (_) {} + } +} + +main() { + print(C); +} diff --git a/TypeSystem/flow-analysis/reachability_A01_t13.dart b/TypeSystem/flow-analysis/reachability_A01_t13.dart new file mode 100644 index 0000000000..1054aedd70 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t13.dart @@ -0,0 +1,31 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks whether the code is reachable after a variable of a type +/// other than `T <: Never`. +/// @author sgrekhov22@gmail.com + +void test(T n) { + late int i; + bool b = (() => true)(); + if (b) { + n; + i = 42; + } + i; // Not an error +} + +main() { + try { + test(throw "Lily was here"); + } catch (_) {} +} diff --git a/TypeSystem/flow-analysis/reachability_A01_t14.dart b/TypeSystem/flow-analysis/reachability_A01_t14.dart new file mode 100644 index 0000000000..bb15db5848 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t14.dart @@ -0,0 +1,35 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks whether the code is reachable after invocation of a +/// getter whose type is other than `T <: Never`. +/// @author sgrekhov22@gmail.com + +class C { + T get n => throw "Lily was here"; + + test() { + try { + late int i; + bool b = (() => true)(); + if (b) { + n; + i = 42; + } + i; // Not an error + } catch (_) {} + } +} + +main() { + print(C); +} diff --git a/TypeSystem/flow-analysis/reachability_A01_t15.dart b/TypeSystem/flow-analysis/reachability_A01_t15.dart new file mode 100644 index 0000000000..456b8563ca --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t15.dart @@ -0,0 +1,31 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks whether the code is reachable after a variable of a type +/// other that `Never`. +/// @author sgrekhov22@gmail.com + +void test(Never? n) { + late int i; + bool b = (() => true)(); + if (b) { + n; + i = 42; + } + i; // Not an error +} + +main() { + try { + test(throw "Lily was here"); + } catch (_) {} +} diff --git a/TypeSystem/flow-analysis/reachability_A01_t16.dart b/TypeSystem/flow-analysis/reachability_A01_t16.dart new file mode 100644 index 0000000000..172931743c --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t16.dart @@ -0,0 +1,31 @@ +// 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 +/// - Variable or getter: If `N` is an expression of the form `x` where the +/// type of `x` is `T` then: +/// If `T <: Never` then: +/// - Let `after(N) = unreachable(before(N))`. +/// Otherwise: +/// - Let `after(N) = before(N)`. +/// +/// @description Checks whether the code is reachable after invocation of a +/// getter whose type is other than `Never`. +/// @author sgrekhov22@gmail.com + +import 'dart:async'; + +FutureOr get n => 2 > 1 ? throw 1: Future.value(throw 2); + +main() { + try { + late int i; + bool b = (() => true)(); + if (b) { + n; + i = 42; + } + i; // Not an error + } catch (_) {} +} From 277da73776674aa0e4e01bce3a75ef05eae29f13 Mon Sep 17 00:00:00 2001 From: sgrekhov Date: Mon, 10 Feb 2025 18:12:45 +0200 Subject: [PATCH 2/2] Implement review recommendations --- TypeSystem/flow-analysis/reachability_A01_t13.dart | 4 +--- TypeSystem/flow-analysis/reachability_A01_t15.dart | 4 +--- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/TypeSystem/flow-analysis/reachability_A01_t13.dart b/TypeSystem/flow-analysis/reachability_A01_t13.dart index 1054aedd70..41fede9ee5 100644 --- a/TypeSystem/flow-analysis/reachability_A01_t13.dart +++ b/TypeSystem/flow-analysis/reachability_A01_t13.dart @@ -25,7 +25,5 @@ void test(T n) { } main() { - try { - test(throw "Lily was here"); - } catch (_) {} + test(null); } diff --git a/TypeSystem/flow-analysis/reachability_A01_t15.dart b/TypeSystem/flow-analysis/reachability_A01_t15.dart index 456b8563ca..79b7ef1a30 100644 --- a/TypeSystem/flow-analysis/reachability_A01_t15.dart +++ b/TypeSystem/flow-analysis/reachability_A01_t15.dart @@ -25,7 +25,5 @@ void test(Never? n) { } main() { - try { - test(throw "Lily was here"); - } catch (_) {} + test(null); }