Skip to content

Commit

Permalink
[_fe_analyzer_shared] Return the shortest witness
Browse files Browse the repository at this point in the history
This updates the exhaustiveness checking to return the shortest witness when no more cases match a value.

This also fixes an exponential case that occurred when checking for reachability.

Closes #59927

Change-Id: I82ede75113ca5d361875620287f7ce3c5fb2f5d2
Reviewed-on: https://dart-review.googlesource.com/c/sdk/+/405120
Reviewed-by: Konstantin Shcheglov <[email protected]>
Commit-Queue: Johnni Winther <[email protected]>
  • Loading branch information
johnniwinther authored and Commit Queue committed Jan 21, 2025
1 parent 762a4c7 commit 7f46b33
Show file tree
Hide file tree
Showing 14 changed files with 226 additions and 48 deletions.
52 changes: 50 additions & 2 deletions pkg/_fe_analyzer_shared/lib/src/exhaustiveness/exhaustive.dart
Original file line number Diff line number Diff line change
Expand Up @@ -79,8 +79,8 @@ List<Witness>? checkExhaustiveness(
// TODO(johnniwinther): Perform reachability checking.
List<List<Space>> caseRows = cases.map((space) => [space]).toList();

List<Witness>? witnesses =
checker._unmatched(caseRows, [valueSpace], returnMultipleWitnesses: true);
List<Witness>? witnesses = checker._unmatched(caseRows, [valueSpace],
returnMultipleWitnesses: true);

// Uncomment this to have it print out the witness for non-exhaustive matches.
// if (witnesses != null) witnesses.forEach(print);
Expand Down Expand Up @@ -117,6 +117,54 @@ class _Checker {
// complete description of at least one value that slipped past all the
// rows.
return [new Witness(witnessPredicates)];
} else if (caseRows.isEmpty && !returnMultipleWitnesses) {
// We have no more cases that can match the witness, so unless we want
// to multiple witnesses, we return directly.
//
// This will return the shortest possible witness and will for instance
// return `(E.b, _)` instead of `(E.b, E.a)` for
//
// enum E { a, b }
// m(E e) => switch (e) { (E.a, _) => 0, };
//
// and `C(f1: int())` instead of `C(f1: int(), f2: int())` for
//
// abstract class C { num f1, f2; }
// m(C c) => switch (e) { C(f1: double(), f2: double()) => 0, };
//
// Additionally, it avoids a degenerate case occurring only when checking
// for unreachable cases. In this mode, the value space is created from
// cases that are not included in the case rows. This means that the
// value space visited with an empty set of case rows left, can be
// exponential in the size of the case. For instance if we have
//
// sealed class S {}
// class S1 extends S {}
// class S2 extends S {
// String? f1, f2, f3, f4, f5, f6, f7, f8;
// }
// m(S s) => {
// S1() => 0,
// S2(:var f1, :var f2, :var f3, :var f4,
// :var f5, :var f6, :var f7, :var f8) => 1,
// };
//
// then in order to check that the second case is not unreachable after
// the first case, we would otherwise check all combinations of `S2` with
// fields values `String` or `null` for fields `f1` to `f8`, instead of
// just stopping with the shortest witness `S2()`.
//
// If we want to compute multiple witness, which we only do for the
// top-most value space, we continue the search for longer witnesses. This
// means that if we have
//
// enum E { a, b }
// m(E e) => switch (e) {};
//
// we do not simply return `_` as the witness, but instead the witnesses
// `E.a` and `E.b`. We want this for the quick-fix that adds all enum
// values or sealed class subclasses in case of an empty switch.
return [new Witness(witnessPredicates)];
}

// Look down the first column of tests.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ intersectSameClass(A o1, A o2, A o3) {
],
};
var c = /*
error=non-exhaustive:A(field1: C(), field2: C()),
error=non-exhaustive:A(field1: C()),
fields={field1:B,field2:B},
type=A
*/
Expand All @@ -73,7 +73,7 @@ intersectSubClass(A o1, A o2, A o3) {
[field1, hashCode],
};
var c = /*
error=non-exhaustive:A(field1: C(), field2: C(), hashCode: int())/A(field1: C(), field2: C()),
error=non-exhaustive:A(field1: C(), field2: C()),
fields={field1:B,field2:B,hashCode:int},
type=A
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -268,7 +268,7 @@ exhaustiveIJ_Multiple(A a) {
nonExhaustiveIJ_MultipleRestricted(A a) {
/*
checkingOrder={A,B,C,D},
error=non-exhaustive:I(member: B(), member2: B(), member3: C()) && J(member: double(), member2: C(), member3: true)/I(member2: B()) && J(member: double(), member2: C(), member3: true),
error=non-exhaustive:I(member: B(), member2: B(), member3: C()) && J(member: double(), member2: C())/I(member2: B()) && J(member: double(), member2: C()),
fields={member:-,C.member:C,I.member:B,I.member2:A,I.member3:C,J.member:num,J.member2:A,J.member3:bool},
subtypes={B,C,D},
type=A
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ exhaustiveSealedListAsList(
SealedList<int>
sl) => /*
checkingOrder={SealedList<int>,ListA<int>,ListB<int>,<int>[],<int>[()],<int>[(), (), ...],<int>[],<int>[()],<int>[(), (), ...]},
error=non-exhaustive:[Object()];[Object(), Object(), ...Object()];[Object()];[Object(), Object(), ...Object()],
error=non-exhaustive:[Object()];[Object(), _, ...];[Object()];[Object(), _, ...],
expandedSubtypes={<int>[],<int>[()],<int>[(), (), ...],<int>[],<int>[()],<int>[(), (), ...]},
subtypes={ListA<int>,ListB<int>},
type=SealedList<int>
Expand All @@ -112,7 +112,7 @@ nonExhaustiveSealedListAsList(
SealedList<int>
sl) => /*
checkingOrder={SealedList<int>,ListA<int>,ListB<int>,<int>[],<int>[()],<int>[(), (), ...],<int>[],<int>[()],<int>[(), (), ...]},
error=non-exhaustive:[_];[Object(), Object(), ...Object()];[_];[Object(), Object(), ...Object()],
error=non-exhaustive:[_];[Object(), _, ...];[_];[Object(), _, ...],
expandedSubtypes={<int>[],<int>[()],<int>[(), (), ...],<int>[],<int>[()],<int>[(), (), ...]},
subtypes={ListA<int>,ListB<int>},
type=SealedList<int>
Expand Down
129 changes: 129 additions & 0 deletions pkg/_fe_analyzer_shared/test/exhaustiveness/data/issue59927.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
// 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.

sealed class State {
const State._();
}

final class StateEmpty extends State {
const StateEmpty() : super._();
}

final class StateWithBunchOfFields extends State {
const StateWithBunchOfFields({
this.value1,
this.value2,
this.value3,
this.value4,
this.value5,
this.value6,
this.value7,
this.value8,
this.value9,
this.value10,
this.value11,
this.value12,
this.value13,
this.value14,
this.value15,
this.value16,
this.value17,
this.value18,
this.value19,
this.value20,
this.value21,
this.value22,
this.value23,
this.value24,
this.value25,
this.value26,
this.value27,
this.value28,
this.value29,
this.value30,
this.value31,
}) : super._();

final String? value1;
final String? value2;
final String? value3;
final String? value4;
final String? value5;
final String? value6;
final String? value7;
final String? value8;
final String? value9;
final String? value10;
final String? value11;
final String? value12;
final String? value13;
final String? value14;
final String? value15;
final String? value16;
final String? value17;
final String? value18;
final String? value19;
final String? value20;
final String? value21;
final String? value22;
final String? value23;
final String? value24;
final String? value25;
final String? value26;
final String? value27;
final String? value28;
final String? value29;
final String? value30;
final String? value31;
}

void handleState(State state) {
/*
checkingOrder={State,StateEmpty,StateWithBunchOfFields},
fields={value1:-,value10:-,value11:-,value12:-,value13:-,value14:-,value15:-,value16:-,value17:-,value18:-,value19:-,value2:-,value20:-,value21:-,value22:-,value23:-,value24:-,value25:-,value26:-,value27:-,value28:-,value29:-,value3:-,value30:-,value31:-,value4:-,value5:-,value6:-,value7:-,value8:-,value9:-},
subtypes={StateEmpty,StateWithBunchOfFields},
type=State
*/
switch (state) {
/*space=StateEmpty*/
case StateEmpty():
print("empty");

/*space=StateWithBunchOfFields(value1: String?, value2: String?, value3: String?, value4: String?, value5: String?, value6: String?, value7: String?, value8: String?, value9: String?, value10: String?, value11: String?, value12: String?, value13: String?, value14: String?, value15: String?, value16: String?, value17: String?, value18: String?, value19: String?, value20: String?, value21: String?, value22: String?, value23: String?, value24: String?, value25: String?, value26: String?, value27: String?, value28: String?, value29: String?, value30: String?, value31: String?)*/
case StateWithBunchOfFields(
:var value1,
:var value2,
:var value3,
:var value4,
:var value5,
:var value6,
:var value7,
:var value8,
:var value9,
:var value10,
:var value11,
:var value12,
:var value13,
:var value14,
:var value15,
:var value16,
:var value17,
:var value18,
:var value19,
:var value20,
:var value21,
:var value22,
:var value23,
:var value24,
:var value25,
:var value26,
:var value27,
:var value28,
:var value29,
:var value30,
:var value31,
):
print("many fields");
}
}
4 changes: 2 additions & 2 deletions pkg/_fe_analyzer_shared/test/exhaustiveness/data/list.dart
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ nonExhaustiveRestrictedHeadElement(List list) {
nonExhaustiveRestrictedTailElement(List list) {
return /*
checkingOrder={List<dynamic>,[],[()],[(), ()],[(), (), ()],[(), (), (), ()],[(), (), (), (), (), ...]},
error=non-exhaustive:[Object(), _, Object(), Object()];[Object(), _, _, ...[...], Object(), Object()]/[Object(), _, _, ..., Object(), Object()],
error=non-exhaustive:[Object(), _, Object(), _];[Object(), _, _, ...[...], Object(), _]/[Object(), _, _, ..., Object(), _],
subtypes={[],[()],[(), ()],[(), (), ()],[(), (), (), ()],[(), (), (), (), (), ...]},
type=List<dynamic>
*/
Expand Down Expand Up @@ -359,7 +359,7 @@ nonExhaustiveRestrictedRest(List list) {
nonExhaustiveRestrictedRestWithTail(List list) {
return /*
checkingOrder={List<dynamic>,[],[()],[(), ()],[(), (), ()],[(), (), (), ()],[(), (), (), (), (), ...]},
error=non-exhaustive:[Object(), _, Object(), Object()];[Object(), _, _, ...[...], Object(), Object()]/[Object(), _, _, ..., Object(), Object()],
error=non-exhaustive:[Object(), _, _, _];[Object(), _, _, _, _, ...[...]]/[Object(), _, _, _, _, ...],
subtypes={[],[()],[(), ()],[(), (), ()],[(), (), (), ()],[(), (), (), (), (), ...]},
type=List<dynamic>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ nonExhaustiveEnumNested2(
Enum,
Enum
) r) => /*
error=non-exhaustive:(Enum.b, Enum.a),
error=non-exhaustive:(Enum.b, _),
fields={$1:Enum,$2:Enum},
type=(Enum, Enum)
*/
Expand All @@ -57,7 +57,7 @@ nonExhaustiveEnumNested3(
Enum,
Enum
) r) => /*
error=non-exhaustive:(Enum.b, Enum.a),
error=non-exhaustive:(Enum.b, _),
fields={$1:Enum,$2:Enum},
type=(Enum, Enum)
*/
Expand Down Expand Up @@ -153,7 +153,7 @@ nonExhaustiveSealedNested3(
S,
S
) r) => /*
error=non-exhaustive:(B(), A()),
error=non-exhaustive:(B(), _),
fields={$1:S,$2:S},
type=(S, S)
*/
Expand Down
1 change: 1 addition & 0 deletions pkg/front_end/test/spell_checking_list_code.txt
Original file line number Diff line number Diff line change
Expand Up @@ -1640,6 +1640,7 @@ shifts
ship
shl
shortening
shortest
showing
shr
shrinking
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ library;
// nonExhaustiveRestrictedType(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:64:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:64:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), ...]'.
// nonExhaustive1aRestrictedValue(List<num> list) => switch (list) {
Expand All @@ -56,9 +56,9 @@ library;
// nonExhaustive1bRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:79:58: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[...[...], double()]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:79:58: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[_, ...[...]]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[..., double()]'.
// Try adding a wildcard pattern or cases that match '[_, ...]'.
// nonExhaustive1bRestrictedType(List<num> list) => switch (list) {
// ^
//
Expand All @@ -68,13 +68,13 @@ library;
// nonExhaustive2aRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:90:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:90:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), _, ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), double(), ...]'.
// Try adding a wildcard pattern or cases that match '[double(), _, ...]'.
// nonExhaustive2bRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:96:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:96:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), double(), ...]'.
// nonExhaustive2cRestrictedValue(List<num> list) => switch (list) {
Expand All @@ -86,9 +86,9 @@ library;
// nonExhaustive2dRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:108:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[_, double()]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:108:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), _]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[_, double()]'.
// Try adding a wildcard pattern or cases that match '[double(), _]'.
// nonExhaustive2eRestrictedValue(List<num> list) => switch (list) {
// ^
//
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ library;
// nonExhaustiveRestrictedType(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:64:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:64:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), ...]'.
// nonExhaustive1aRestrictedValue(List<num> list) => switch (list) {
Expand All @@ -56,9 +56,9 @@ library;
// nonExhaustive1bRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:79:58: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[...[...], double()]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:79:58: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[_, ...[...]]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[..., double()]'.
// Try adding a wildcard pattern or cases that match '[_, ...]'.
// nonExhaustive1bRestrictedType(List<num> list) => switch (list) {
// ^
//
Expand All @@ -68,13 +68,13 @@ library;
// nonExhaustive2aRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:90:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:90:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), _, ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), double(), ...]'.
// Try adding a wildcard pattern or cases that match '[double(), _, ...]'.
// nonExhaustive2bRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:96:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...[...]]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:96:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), double(), ...]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[double(), double(), ...]'.
// nonExhaustive2cRestrictedValue(List<num> list) => switch (list) {
Expand All @@ -86,9 +86,9 @@ library;
// nonExhaustive2dRestrictedValue(List<num> list) => switch (list) {
// ^
//
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:108:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[_, double()]'.
// pkg/front_end/testcases/patterns/exhaustiveness/list.dart:108:59: Error: The type 'List<num>' is not exhaustively matched by the switch cases since it doesn't match '[double(), _]'.
// - 'List' is from 'dart:core'.
// Try adding a wildcard pattern or cases that match '[_, double()]'.
// Try adding a wildcard pattern or cases that match '[double(), _]'.
// nonExhaustive2eRestrictedValue(List<num> list) => switch (list) {
// ^
//
Expand Down
Loading

0 comments on commit 7f46b33

Please sign in to comment.