From c4669054549ba84ac0d69a08b8035b950ba33c0a Mon Sep 17 00:00:00 2001 From: "Sergey G. Grekhov" Date: Mon, 17 Feb 2025 10:24:08 +0200 Subject: [PATCH] #3057. Add more flow analysis tests for type Never (#3070) 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 | 29 ++++++++++++++ .../flow-analysis/reachability_A01_t14.dart | 35 +++++++++++++++++ .../flow-analysis/reachability_A01_t15.dart | 29 ++++++++++++++ .../flow-analysis/reachability_A01_t16.dart | 31 +++++++++++++++ 8 files changed, 216 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..41fede9ee5 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t13.dart @@ -0,0 +1,29 @@ +// 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() { + test(null); +} 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..79b7ef1a30 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A01_t15.dart @@ -0,0 +1,29 @@ +// 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() { + test(null); +} 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 (_) {} +}