pkg/_fe_analyzer_shared/lib/src/exhaustiveness/exhaustive.dart

// Copyright (c) 2022, 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.

import 'static_type.dart';
import 'key.dart';
import 'path.dart';
import 'profile.dart' as profile;
import 'space.dart';
import 'witness.dart';

/// Returns `true` if [caseSpaces] exhaustively covers all possible values of
/// [valueSpace].
bool isExhaustive(
  ObjectPropertyLookup fieldLookup,
  Space valueSpace,
  List<Space> caseSpaces,
) {
  return checkExhaustiveness(fieldLookup, valueSpace, caseSpaces) == null;
}

/// Checks the [caseSpaces] representing a series of switch cases to see if they
/// exhaustively cover all possible values of the matched [valueType]. Also
/// checks to see if any case can't be matched because it's covered by previous
/// cases.
///
/// [caseIsGuarded] should be a list of booleans indicating whether each case in
/// [caseSpaces] has an associated `when` clause.
///
/// If any unreachable cases are found, information about them is appended to
/// [caseUnreachabilities]. (If `null` is passed for [caseUnreachabilities],
/// then no information about unreachable cases is generated).
///
/// If the switch cases are not fully exhaustive, details about how they fail to
/// be exhaustive are returned using a data structure of type
/// [NonExhaustiveness]; otherwise `null` is returned.
///
/// Note that if a non-null value is returned, that doesn't necessarily mean
/// that an error should be reported; the caller still must check whether the
/// switch has a `default` clause and whether the scrutinee type is an "always
/// exhaustive" type.
NonExhaustiveness? computeExhaustiveness(
  ObjectPropertyLookup fieldLookup,
  StaticType valueType,
  List<bool> caseIsGuarded,
  List<Space> caseSpaces, {
  List<CaseUnreachability>? caseUnreachabilities,
}) {
  _Checker checker = new _Checker(fieldLookup);

  Space valuePattern = new Space(const Path.root(), valueType);
  List<List<Space>> caseRows = [];

  for (int i = 0; i < caseSpaces.length; i++) {
    late List<Space> caseRow = [caseSpaces[i]];
    if (caseUnreachabilities != null && i > 0) {
      // See if this case is covered by previous ones.
      if (checker._unmatched(
            caseRows,
            caseRow,
            returnMultipleWitnesses: false,
          ) ==
          null) {
        caseUnreachabilities.add(
          new CaseUnreachability(valueType, caseSpaces, i),
        );
      }
    }
    if (!caseIsGuarded[i]) {
      caseRows.add(caseRow);
    }
  }

  List<Witness>? witnesses = checker._unmatched(caseRows, [
    valuePattern,
  ], returnMultipleWitnesses: true);
  if (witnesses != null) {
    return new NonExhaustiveness(valueType, caseSpaces, witnesses);
  } else {
    return null;
  }
}

/// Determines if [cases] is exhaustive over all values contained by
/// [valueSpace]. If so, returns `null`. Otherwise, returns a list of [Witness]s
/// of values that aren't matched by anything in [cases].
List<Witness>? checkExhaustiveness(
  ObjectPropertyLookup fieldLookup,
  Space valueSpace,
  List<Space> cases,
) {
  _Checker checker = new _Checker(fieldLookup);

  // TODO(johnniwinther): Perform reachability checking.
  List<List<Space>> caseRows = cases.map((space) => [space]).toList();

  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);

  return witnesses;
}

class _Checker {
  final ObjectPropertyLookup _propertyLookup;

  _Checker(this._propertyLookup);

  /// Tries to find a pattern containing at least one value matched by
  /// [valuePatterns] that is not matched by any of the patterns in [caseRows].
  ///
  /// If found, returns it. This is a witness example showing that [caseRows] is
  /// not exhaustive over all values in [valuePatterns]. If it returns `null`,
  /// then [caseRows] exhaustively covers [valuePatterns].
  List<Witness>? _unmatched(
    List<List<Space>> caseRows,
    List<Space> valuePatterns, {
    List<Predicate> witnessPredicates = const [],
    required bool returnMultipleWitnesses,
  }) {
    assert(
      caseRows.every((element) => element.length == valuePatterns.length),
      "Value patterns: $valuePatterns, case rows: $caseRows.",
    );
    profile.count('_unmatched');
    // If there are no more columns, then we've tested all the predicates we
    // have to test.
    if (valuePatterns.isEmpty) {
      // If there are still any rows left, then it means every remaining value
      // will go to one of those rows' bodies, so we have successfully matched.
      if (caseRows.isNotEmpty) return null;

      // If we ran out of rows too, then it means [witnessPredicates] is now a
      // 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.
    Space firstValuePatterns = valuePatterns[0];

    Set<Key> keysOfInterest = {};
    for (List<Space> caseRow in caseRows) {
      for (SingleSpace singleSpace in caseRow.first.singleSpaces) {
        keysOfInterest.addAll(singleSpace.additionalProperties.keys);
      }
    }
    for (SingleSpace firstValuePattern in firstValuePatterns.singleSpaces) {
      StaticType contextType = firstValuePattern.type;
      List<StaticType> stack = [firstValuePattern.type];
      List<Witness>? witnesses;
      while (stack.isNotEmpty) {
        StaticType type = stack.removeAt(0);
        if (type.isSubtypeOf(StaticType.neverType)) {
          // Don't try to exhaust the Never type.
          continue;
        }
        if (type.isSealed) {
          List<Witness>? result = _filterByType(
            contextType,
            type,
            caseRows,
            firstValuePattern,
            valuePatterns,
            witnessPredicates,
            firstValuePatterns.path,
            // We don't use the witnesses, so only compute one.
            returnMultipleWitnesses: false,
          );
          if (result == null) {
            // This type was fully handled so no need to test its
            // subtypes.
          } else {
            // The type was not fully handled so we must allow for
            // handling of individual subtypes.
            stack.addAll(type.getSubtypes(keysOfInterest));
          }
        } else {
          List<Witness>? result = _filterByType(
            contextType,
            type,
            caseRows,
            firstValuePattern,
            valuePatterns,
            witnessPredicates,
            firstValuePatterns.path,
            // Don't collect multiple witnesses for to avoid combinatorial
            // explosion. For instance returning
            //
            //    (E.a, E.b), (E.a, E.c) ... (E.z, E.z) // 675 witnesses
            //
            // for
            //
            //    enum E { a, b, ..., z }
            //    method((E, E) r) => switch (r) { (E.a, E.a) => 0, };
            //
            returnMultipleWitnesses: false,
          );

          // If we found a witness for a subtype that no rows match, then we
          // can stop. There may be others but we don't need to find more.
          if (result != null) {
            (witnesses ??= []).addAll(result);
            if (!returnMultipleWitnesses) {
              return witnesses;
            }
          }
        }
      }
      if (witnesses != null) {
        return witnesses;
      }
    }

    // If we get here, no subtype yielded a witness, so we must have matched
    // everything.
    return null;
  }

  List<Witness>? _filterByType(
    StaticType contextType,
    StaticType type,
    List<List<Space>> caseRows,
    SingleSpace firstSingleSpaceValue,
    List<Space> valueSpaces,
    List<Predicate> witnessPredicates,
    Path path, {
    required bool returnMultipleWitnesses,
  }) {
    profile.count('_filterByType');
    // Extend the witness with the type we're matching.
    List<Predicate> extendedWitness = [
      ...witnessPredicates,
      new Predicate(path, contextType, type),
    ];

    // 1) Discard any rows that might not match because the column's type isn't
    // a subtype of the value's type.  We only keep rows that *must* match
    // because a row that could potentially fail to match will not help us prove
    // exhaustiveness.
    //
    // 2) Expand any unions in the first column. This can (deliberately) produce
    // duplicate rows in remainingRows.
    List<SingleSpace> remainingRowFirstSingleSpaces = [];
    List<List<Space>> remainingRows = [];
    for (List<Space> row in caseRows) {
      Space firstSpace = row[0];

      for (SingleSpace firstSingleSpace in firstSpace.singleSpaces) {
        // If the row's type is a supertype of the value pattern's type then it
        // must match.
        if (type.isSubtypeOf(firstSingleSpace.type)) {
          remainingRowFirstSingleSpaces.add(firstSingleSpace);
          remainingRows.add(row);
        }
      }
    }

    // We have now filtered by the type test of the first column of patterns,
    // but some of those may also have field subpatterns. If so, lift those out
    // so we can recurse into them.
    Set<Key> propertyKeys = {
      ...firstSingleSpaceValue.properties.keys,
      for (SingleSpace firstPattern in remainingRowFirstSingleSpaces)
        ...firstPattern.properties.keys,
    };

    Set<Key> additionalPropertyKeys = {
      ...firstSingleSpaceValue.additionalProperties.keys,
      for (SingleSpace firstPattern in remainingRowFirstSingleSpaces)
        ...firstPattern.additionalProperties.keys,
    };

    // Sorting isn't necessary, but makes the behavior deterministic.
    List<Key> sortedPropertyKeys = propertyKeys.toList()..sort();
    List<Key> sortedAdditionalPropertyKeys = additionalPropertyKeys.toList()
      ..sort();

    // Remove the first column from the value list and replace it with any
    // expanded fields.
    valueSpaces = [
      ..._expandProperties(
        sortedPropertyKeys,
        sortedAdditionalPropertyKeys,
        firstSingleSpaceValue,
        type,
        path,
      ),
      ...valueSpaces.skip(1),
    ];

    // Remove the first column from each row and replace it with any expanded
    // fields.
    for (int i = 0; i < remainingRows.length; i++) {
      remainingRows[i] = [
        ..._expandProperties(
          sortedPropertyKeys,
          sortedAdditionalPropertyKeys,
          remainingRowFirstSingleSpaces[i],
          remainingRowFirstSingleSpaces[i].type,
          path,
        ),
        ...remainingRows[i].skip(1),
      ];
    }

    // Proceed to the next column.
    return _unmatched(
      remainingRows,
      valueSpaces,
      witnessPredicates: extendedWitness,
      returnMultipleWitnesses: returnMultipleWitnesses,
    );
  }

  /// Given a list of [propertyKeys] and [additionalPropertyKeys], and a
  /// [singleSpace], generates a list of single spaces, one for each named
  /// property and additional property key.
  ///
  /// When [singleSpace] contains a property with that name or an additional
  /// property with the key, extracts it into the resulting list. Otherwise, the
  /// [singleSpace] doesn't care about that property, so inserts a default
  /// [Space] that matches all values for the property. If the [type] doesn't
  /// know about the property, the static type of the property is read from
  /// [Key].
  ///
  /// In other words, this unpacks a set of properties so that the main
  /// algorithm can add them to the worklist.
  List<Space> _expandProperties(
    List<Key> propertyKeys,
    List<Key> additionalPropertyKeys,
    SingleSpace singleSpace,
    StaticType type,
    Path path,
  ) {
    profile.count('_expandProperties');
    List<Space> result = <Space>[];
    for (Key key in propertyKeys) {
      Space? property = singleSpace.properties[key];
      if (property != null) {
        result.add(property);
      } else {
        // This pattern doesn't test this property, so add a pattern for the
        // property that matches all values. This way the columns stay aligned.
        StaticType? propertyType = type.getPropertyType(_propertyLookup, key);
        if (propertyType == null && key is ExtensionKey) {
          propertyType = key.type;
        }
        // TODO(johnniwinther): Enable this assert when extension members are
        // handled.
        /*assert(propertyType != null,
            "Type $type does not have a type for property $key");*/
        result.add(
          new Space(path.add(key), propertyType ?? StaticType.nullableObject),
        );
      }
    }
    for (Key key in additionalPropertyKeys) {
      Space? property = singleSpace.additionalProperties[key];
      if (property != null) {
        result.add(property);
      } else {
        // This pattern doesn't test this property, so add a pattern for the
        // property that matches all values. This way the columns stay aligned.
        // TODO(johnniwinther): Enable this assert when extension members are
        // handled.
        // assert(type.getAdditionalPropertyType(key) != null,
        //    "Type $type does not have a type for additional property $key");
        result.add(
          new Space(
            path.add(key),
            type.getAdditionalPropertyType(key) ?? StaticType.nullableObject,
          ),
        );
      }
    }
    return result;
  }
}

/// Recursively expands [type] with its subtypes if it's sealed.
///
/// Otherwise, just returns [type].
List<StaticType> expandSealedSubtypes(
  StaticType type,
  Set<Key> keysOfInterest,
) {
  profile.count('expandSealedSubtypes');
  if (!type.isSealed) {
    return [type];
  } else {
    return {
      for (StaticType subtype in type.getSubtypes(keysOfInterest))
        ...expandSealedSubtypes(subtype, keysOfInterest),
    }.toList();
  }
}

List<StaticType> checkingOrder(StaticType type, Set<Key> keysOfInterest) {
  List<StaticType> result = [];
  List<StaticType> pending = [type];
  while (pending.isNotEmpty) {
    StaticType type = pending.removeAt(0);
    result.add(type);
    if (type.isSealed) {
      pending.addAll(type.getSubtypes(keysOfInterest));
    }
  }
  return result;
}

class NonExhaustiveness {
  final StaticType valueType;

  final List<Space> cases;

  final List<Witness> witnesses;

  NonExhaustiveness(this.valueType, this.cases, this.witnesses);

  @override
  String toString() =>
      '$valueType is not exhaustively matched by ${cases.join('|')}.';
}

class CaseUnreachability {
  final StaticType valueType;
  final List<Space> cases;
  final int index;

  CaseUnreachability(this.valueType, this.cases, this.index);

  @override
  String toString() => 'Case #${index + 1} ${cases[index]} is unreachable.';
}