implement checking for pattern match exhaustiveness and for unreachable cases (#2164)

When checking for control flow falling off a function after a `match`, determine whether it's possible for no case to have matched. Using the same implementation, also detect whether `case`s in a `match` are unreachable.

For now, the implementation never considers a match against specific values for any type other than tuples, alternatives, and `bool` to be exhaustive. In particular, matching against the sole value `{}` of type `{}` is not considered exhaustive. This is probably best left until explorer supports matching on struct and maybe class types more generally.

This implementation closely follows the algorithm described in the paper [Warnings for pattern matching](http://moscova.inria.fr/~maranget/papers/warn/warn.pdf) by Luc Maranget. Various optimizations are possible, such as reducing the amount of copying done, but for the purposes of explorer, comprehensibility is being favored over efficiency.

The problem is, perhaps surprisingly, co-NP-hard (by reduction to the tautology problem for disjunctive normal form, which is in turn dual to the satisfaction problem for conjunctive normal form, which is well-known to be NP-hard). The algorithm is therefore exponential-time in the worst case, but seems to be well-studied and performs well enough on non-pathological examples. Nonetheless, a depth limit has been imposed to prevent pathological examples such as those generated by a fuzzer from causing long runtimes.

Co-authored-by: Jon Ross-Perkins <jperkins@google.com>

explorer/fuzzing/ast_to_proto.cpp

@@ -13,6 +13,7 @@
 namespace Carbon {
 
 using ::llvm::cast;
+using ::llvm::dyn_cast;
 using ::llvm::isa;
 
 static auto ExpressionToProto(const Expression& expression)
@@ -481,9 +482,16 @@ static auto StatementToProto(const Statement& statement) -> Fuzzing::Statement {
           ExpressionToProto(match.expression());
       for (const Match::Clause& clause : match.clauses()) {
         auto* clause_proto = match_proto->add_clauses();
-        const bool is_default_clause =
-            clause.pattern().kind() == PatternKind::BindingPattern &&
-            cast<BindingPattern>(clause.pattern()).name() == AnonymousName;
+        // TODO: Working out whether we have a default clause after the fact
+        // like this is fragile.
+        bool is_default_clause = false;
+        if (auto* binding = dyn_cast<BindingPattern>(&clause.pattern())) {
+          if (binding->name() == AnonymousName &&
+              isa<AutoPattern>(binding->type()) &&
+              binding->source_loc() == binding->type().source_loc()) {
+            is_default_clause = true;
+          }
+        }
         if (is_default_clause) {
           clause_proto->set_is_default(true);
         } else {

explorer/interpreter/BUILD

@@ -177,6 +177,22 @@ cc_library(
     deps = ["//common:check"],
 )
 
+cc_library(
+    name = "pattern_analysis",
+    srcs = [
+        "pattern_analysis.cpp",
+    ],
+    hdrs = [
+        "pattern_analysis.h",
+    ],
+    deps = [
+        ":action_and_value",
+        "//common:error",
+        "//explorer/ast",
+        "//explorer/common:nonnull",
+        "@llvm-project//llvm:Support",
+    ],
+)
 cc_library(
     name = "type_checker",
     srcs = [
@@ -193,6 +209,7 @@ cc_library(
         ":action_and_value",
         ":dictionary",
         ":interpreter",
+        ":pattern_analysis",
         "//common:error",
         "//common:ostream",
         "//explorer/ast",

explorer/interpreter/pattern_analysis.cpp

@@ -0,0 +1,307 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "explorer/interpreter/pattern_analysis.h"
+
+#include <set>
+
+using llvm::cast;
+using llvm::dyn_cast;
+using llvm::isa;
+
+namespace Carbon {
+
+auto AbstractPattern::kind() const -> Kind {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    return Compound;
+  }
+  if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (isa<TupleValue, AlternativeValue, BoolValue>(value)) {
+      return Compound;
+    }
+    return Primitive;
+  }
+  CARBON_CHECK(value_.is<const WildcardTag*>());
+  return Wildcard;
+}
+
+auto AbstractPattern::discriminator() const -> std::string_view {
+  CARBON_CHECK(kind() == Compound);
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* alt_pattern = dyn_cast<AlternativePattern>(pattern)) {
+      return alt_pattern->alternative_name();
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      return alt->alt_name();
+    } else if (auto* bool_val = dyn_cast<BoolValue>(value)) {
+      return bool_val->value() ? "true" : "false";
+    }
+  }
+  return {};
+}
+
+auto AbstractPattern::elements_size() const -> int {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* tuple_pattern = dyn_cast<TuplePattern>(pattern)) {
+      return tuple_pattern->fields().size();
+    } else if (isa<AlternativePattern>(pattern)) {
+      return 1;
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* tuple = dyn_cast<TupleValue>(value)) {
+      return tuple->elements().size();
+    } else if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      return 1;
+    }
+  }
+  return 0;
+}
+
+void AbstractPattern::AppendElementsTo(
+    std::vector<AbstractPattern>& out) const {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* tuple_pattern = dyn_cast<TuplePattern>(pattern)) {
+      auto fields = tuple_pattern->fields();
+      out.insert(out.end(), fields.begin(), fields.end());
+    } else if (auto* alt_pattern = dyn_cast<AlternativePattern>(pattern)) {
+      out.push_back(&alt_pattern->arguments());
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* tuple = dyn_cast<TupleValue>(value)) {
+      auto* tuple_type = cast<TupleValue>(type_);
+      CARBON_CHECK(tuple->elements().size() == tuple_type->elements().size());
+      for (size_t i = 0; i != tuple->elements().size(); ++i) {
+        out.push_back(
+            AbstractPattern(tuple->elements()[i], tuple_type->elements()[i]));
+      }
+    } else if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      out.push_back(AbstractPattern(
+          &alt->argument(),
+          *cast<ChoiceType>(type_)->FindAlternative(alt->alt_name())));
+    }
+  }
+}
+
+auto AbstractPattern::value() const -> const Value& {
+  CARBON_CHECK(kind() == Primitive);
+  return *value_.get<const Value*>();
+}
+
+auto AbstractPattern::type() const -> const Value& {
+  CARBON_CHECK(kind() != Wildcard);
+  return *type_;
+}
+
+void AbstractPattern::Set(Nonnull<const Pattern*> pattern) {
+  type_ = &pattern->static_type();
+  switch (pattern->kind()) {
+    case PatternKind::AddrPattern:
+    case PatternKind::AutoPattern:
+    case PatternKind::BindingPattern:
+    case PatternKind::GenericBinding:
+      value_ = static_cast<const WildcardTag*>(nullptr);
+      break;
+
+    case PatternKind::TuplePattern:
+    case PatternKind::AlternativePattern:
+      value_ = pattern;
+      break;
+
+    case PatternKind::ExpressionPattern:
+      value_ = &pattern->value();
+      break;
+
+    case PatternKind::VarPattern:
+      Set(&cast<VarPattern>(pattern)->pattern());
+      break;
+  }
+}
+
+auto PatternMatrix::IsUseful(llvm::ArrayRef<AbstractPattern> pattern,
+                             int max_exponential_depth) const -> bool {
+  if (matrix_.empty()) {
+    return true;
+  }
+
+  CARBON_CHECK(pattern.size() == matrix_[0].size());
+  if (matrix_[0].empty()) {
+    return false;
+  }
+
+  switch (pattern[0].kind()) {
+    case AbstractPattern::Wildcard: {
+      auto discrim = FirstColumnDiscriminators();
+      // Check if we hit the depth limit. If so, we act as if the
+      // constructors present in this position are not exhaustive, that is,
+      // as if the type we're matching has some other constructor not
+      // corresponding to anything written in the pattern in this position.
+      // This can lead us to conclude that a pattern is useful if it is not,
+      // and that a set of patterns is not exhaustive when it is.
+      int new_depth =
+          max_exponential_depth - (discrim.found.size() > 1 ? 1 : 0);
+      if (!discrim.any_missing && new_depth >= 0) {
+        for (auto found : discrim.found) {
+          if (Specialize(found).IsUseful(*SpecializeRow(pattern, found),
+                                         new_depth)) {
+            return true;
+          }
+        }
+        return false;
+      }
+      return Default().IsUseful(pattern.slice(1), max_exponential_depth);
+    }
+
+    case AbstractPattern::Compound: {
+      DiscriminatorInfo discrim = {.discriminator = pattern[0].discriminator(),
+                                   .size = pattern[0].elements_size()};
+      return Specialize(discrim).IsUseful(*SpecializeRow(pattern, discrim),
+                                          max_exponential_depth);
+    }
+
+    case AbstractPattern::Primitive: {
+      return Specialize(pattern[0].value())
+          .IsUseful(pattern.slice(1), max_exponential_depth);
+    }
+  }
+}
+
+auto PatternMatrix::FirstColumnDiscriminators() const -> DiscriminatorSet {
+  std::set<std::string_view> discrims;
+  std::optional<int> num_discrims;
+  std::optional<int> elem_size;
+
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        continue;
+      case AbstractPattern::Compound: {
+        const Value& type = row[0].type();
+        if (auto* tuple = dyn_cast<TupleValue>(&type)) {
+          // If we find a tuple match, we've found all constructors (there's
+          // only one!) and none were missing.
+          return {
+              .found = {{.discriminator = {},
+                         .size = static_cast<int>(tuple->elements().size())}},
+              .any_missing = false};
+        } else if (auto* choice = dyn_cast<ChoiceType>(&type)) {
+          num_discrims = choice->declaration().alternatives().size();
+          elem_size = 1;
+        } else if (isa<BoolType>(type)) {
+          // `bool` behaves like a choice type with two alternativs,
+          // and with no nested patterns for either of them.
+          num_discrims = 2;
+          elem_size = 0;
+        } else {
+          llvm_unreachable("unexpected compound type");
+        }
+        discrims.insert(row[0].discriminator());
+        break;
+      }
+      case AbstractPattern::Primitive: {
+        // We assume that primitive value matches are always incomplete, even
+        // for types like `i8` where a covering match might be possible.
+        return {.found = {}, .any_missing = true};
+      }
+    }
+  }
+
+  if (!num_discrims || *num_discrims != static_cast<int>(discrims.size())) {
+    return {.found = {}, .any_missing = true};
+  }
+
+  DiscriminatorSet result = {.found = {}, .any_missing = false};
+  result.found.reserve(discrims.size());
+  for (auto s : discrims) {
+    result.found.push_back({.discriminator = s, .size = *elem_size});
+  }
+  return result;
+}
+
+auto PatternMatrix::SpecializeRow(llvm::ArrayRef<AbstractPattern> row,
+                                  DiscriminatorInfo discriminator)
+    -> std::optional<std::vector<AbstractPattern>> {
+  CARBON_CHECK(!row.empty());
+  std::vector<AbstractPattern> new_row;
+  switch (row[0].kind()) {
+    case AbstractPattern::Wildcard:
+      new_row.reserve(discriminator.size + row.size() - 1);
+      new_row.insert(new_row.end(), discriminator.size,
+                     AbstractPattern::MakeWildcard());
+      break;
+    case AbstractPattern::Compound: {
+      if (row[0].discriminator() != discriminator.discriminator) {
+        return std::nullopt;
+      }
+      CARBON_CHECK(static_cast<int>(row[0].elements_size()) ==
+                   discriminator.size);
+      new_row.reserve(discriminator.size + row.size() - 1);
+      row[0].AppendElementsTo(new_row);
+      break;
+    }
+    case AbstractPattern::Primitive:
+      // These cases should be rejected by the type checker.
+      llvm_unreachable("matched primitive against compound");
+  }
+  new_row.insert(new_row.end(), row.begin() + 1, row.end());
+  return std::move(new_row);
+}
+
+auto PatternMatrix::Specialize(DiscriminatorInfo discriminator) const
+    -> PatternMatrix {
+  PatternMatrix specialized;
+  for (auto& row : matrix_) {
+    // TODO: If we add support for "or" patterns, specialization might
+    // produce multiple rows here.
+    if (auto new_row = SpecializeRow(row, discriminator)) {
+      specialized.Add(std::move(new_row.value()));
+    }
+  }
+  return specialized;
+}
+
+// Specialize the pattern matrix for the case where the first value is known
+// to be `value`, and is not matched.
+auto PatternMatrix::Specialize(const Value& value) const -> PatternMatrix {
+  PatternMatrix specialized;
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        break;
+      case AbstractPattern::Compound:
+        llvm_unreachable("matched compound against primitive");
+      case AbstractPattern::Primitive:
+        // TODO: Use an equality context here?
+        if (!ValueEqual(&row[0].value(), &value, std::nullopt)) {
+          continue;
+        }
+        break;
+    }
+    specialized.Add(std::vector<AbstractPattern>(row.begin() + 1, row.end()));
+  }
+  return specialized;
+}
+
+// Specialize the pattern matrix for the case where the first value uses a
+// discriminator matching none of the non-wildcard patterns.
+auto PatternMatrix::Default() const -> PatternMatrix {
+  PatternMatrix default_matrix;
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        default_matrix.Add(
+            std::vector<AbstractPattern>(row.begin() + 1, row.end()));
+        break;
+      case AbstractPattern::Compound:
+      case AbstractPattern::Primitive:
+        break;
+    }
+  }
+  return default_matrix;
+}
+
+}  // namespace Carbon

explorer/interpreter/pattern_analysis.h

@@ -0,0 +1,162 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_
+#define CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_
+
+#include <vector>
+
+#include "explorer/ast/pattern.h"
+#include "explorer/common/nonnull.h"
+#include "explorer/interpreter/value.h"
+#include "llvm/ADT/PointerUnion.h"
+
+namespace Carbon {
+
+// An abstracted view of a pattern or constant value (which we view as a
+// particular kind of pattern).
+class AbstractPattern {
+ public:
+  enum Kind {
+    // A pattern that matches anything.
+    Wildcard,
+    // A pattern that matches a compound value with sub-patterns to match
+    // elements. A compound value is modeled as a discriminator name applied to
+    // a sequence of nested values: the alternative `Optional.Element(E)` has
+    // discriminator `Element` and nested value `E`, and the tuple `(A,B,C)`
+    // has an empty discriminator and nested values `A`, `B`, and `C`.
+    Compound,
+    // A pattern that matches a particular primitive value.
+    Primitive
+  };
+
+  // This is intentionally implicit to allow easy conversion from a container
+  // of `const Pattern*` to a container of `AbstractPattern`s.
+  // NOLINTNEXTLINE(google-explicit-constructor)
+  AbstractPattern(Nonnull<const Pattern*> pattern) { Set(pattern); }
+
+  AbstractPattern(Nonnull<const Value*> value, Nonnull<const Value*> type)
+      : value_(value), type_(type) {}
+
+  // Make a match-anything wildcard pattern.
+  static auto MakeWildcard() -> AbstractPattern {
+    return AbstractPattern(WildcardTag());
+  }
+
+  // Get the kind for this pattern.
+  auto kind() const -> Kind;
+
+  // Get the type, for a non-wildcard pattern.
+  auto type() const -> const Value&;
+
+  // Get the discriminator used for a compound pattern.
+  auto discriminator() const -> std::string_view;
+
+  // Get the number of nested patterns for a compound pattern.
+  auto elements_size() const -> int;
+
+  // Append the nested patterns in this compound pattern to `out`.
+  void AppendElementsTo(std::vector<AbstractPattern>& out) const;
+
+  // Get the value for a primitive pattern.
+  auto value() const -> const Value&;
+
+ private:
+  // This is aligned so that we can use it in the `PointerUnion` below.
+  struct alignas(8) WildcardTag {};
+  AbstractPattern(WildcardTag)
+      : value_(static_cast<const WildcardTag*>(nullptr)), type_(nullptr) {}
+
+  void Set(Nonnull<const Pattern*> pattern);
+
+  // The underlying pattern: either a syntactic pattern, or a constant value,
+  // or a placeholder indicating that this is a wildcard pattern.
+  llvm::PointerUnion<Nonnull<const Pattern*>, Nonnull<const Value*>,
+                     const WildcardTag*>
+      value_;
+  // Values don't always know their types, so store the type here. We only
+  // really need it for the `const Value*` case but also store it for the
+  // `const Pattern*` case for convenience.
+  const Value* type_;
+};
+
+// A matrix of patterns, used for determining exhaustiveness and redundancy of
+// patterns in a match statement.
+//
+// See http://moscova.inria.fr/~maranget/papers/warn/index.html for details on
+// the algorithm used here.
+class PatternMatrix {
+ public:
+  // Add a pattern vector row to this collection of pattern vectors.
+  void Add(std::vector<AbstractPattern> pattern_vector) {
+    CARBON_CHECK(matrix_.empty() || matrix_[0].size() == pattern_vector.size());
+    matrix_.push_back(std::move(pattern_vector));
+  }
+
+  // Returns true if the given pattern vector is redundant if it appears after
+  // the patterns in this matrix. That is, if it will never match following the
+  // other patterns because everything it matches is matched by some other
+  // pattern.
+  auto IsRedundant(llvm::ArrayRef<AbstractPattern> pattern) const -> bool {
+    return !IsUseful(pattern, MaxExponentialDepth);
+  }
+
+ private:
+  // The maximum number of times we will consider all alternatives when
+  // recursively expanding the pattern. Allowing this to happen an arbitrary
+  // number of times leads to exponential growth in the runtime of the
+  // algorithm.
+  static constexpr int MaxExponentialDepth = 8;
+
+  // Information about a constructor for a compound type.
+  struct DiscriminatorInfo {
+    // For an alternative, the name. Otherwise, empty.
+    std::string_view discriminator;
+    // The number of elements. For a tuple, the size. Always 1 for an
+    // alternative.
+    int size;
+  };
+
+  struct DiscriminatorSet {
+    std::vector<DiscriminatorInfo> found;
+    bool any_missing;
+  };
+
+  // Determine whether the given pattern vector is useful: that is, whether
+  // adding it to the matrix would allow any more values to be matched.
+  auto IsUseful(llvm::ArrayRef<AbstractPattern> pattern,
+                int max_exponential_depth) const -> bool;
+
+  // Find the discriminators used by the first column and check whether we
+  // found all of them.
+  auto FirstColumnDiscriminators() const -> DiscriminatorSet;
+
+  // Specialize the pattern vector `row` for the case that the first value
+  // matched uses `discriminator`.
+  static auto SpecializeRow(llvm::ArrayRef<AbstractPattern> row,
+                            DiscriminatorInfo discriminator)
+      -> std::optional<std::vector<AbstractPattern>>;
+
+  // Specialize the pattern matrix for the case that the first value matched
+  // uses `discriminator`, and its elements are matched.
+  auto Specialize(DiscriminatorInfo discriminator) const -> PatternMatrix;
+
+  // Specialize the pattern matrix for the case where the first value is known
+  // to be `value`, and is not matched.
+  auto Specialize(const Value& value) const -> PatternMatrix;
+
+  // Specialize the pattern matrix for the case where the first value uses a
+  // discriminator matching none of the non-wildcard patterns.
+  auto Default() const -> PatternMatrix;
+
+  // The pattern matrix itself, in row-major order. Each element of `matrix_`
+  // is a distinct sequence of patterns that can be matched against a
+  // corresponding sequence of values. Each such row has the same length and
+  // has elements of the same type.
+  std::vector<std::vector<AbstractPattern>> matrix_;
+};
+
+}  // namespace Carbon
+
+#endif  // CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_

explorer/interpreter/type_checker.cpp

@@ -17,6 +17,7 @@
 #include "explorer/common/error_builders.h"
 #include "explorer/interpreter/impl_scope.h"
 #include "explorer/interpreter/interpreter.h"
+#include "explorer/interpreter/pattern_analysis.h"
 #include "explorer/interpreter/value.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/StringExtras.h"
@@ -2933,6 +2934,7 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
       CARBON_RETURN_IF_ERROR(TypeCheckExp(&match.expression(), impl_scope));
       std::vector<Match::Clause> new_clauses;
       std::optional<Nonnull<const Value*>> expected_type;
+      PatternMatrix patterns;
       for (auto& clause : match.clauses()) {
         ImplScope clause_scope;
         clause_scope.AddParent(&impl_scope);
@@ -2953,6 +2955,12 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
         } else {
           expected_type = &clause.pattern().static_type();
         }
+        if (patterns.IsRedundant({&clause.pattern()})) {
+          return CompilationError(clause.pattern().source_loc())
+                 << "unreachable case: all values matched by this case "
+                 << "are matched by earlier cases";
+        }
+        patterns.Add({&clause.pattern()});
         CARBON_RETURN_IF_ERROR(
             TypeCheckStmt(&clause.statement(), clause_scope));
       }
@@ -3130,17 +3138,12 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
 
 // Returns true if we can statically verify that `match` is exhaustive, meaning
 // that one of its clauses will be executed for any possible operand value.
-//
-// TODO: the current rule is an extremely simplistic placeholder, with
-// many false negatives.
 static auto IsExhaustive(const Match& match) -> bool {
+  PatternMatrix matrix;
   for (const Match::Clause& clause : match.clauses()) {
-    // A pattern consisting of a single variable binding is guaranteed to match.
-    if (clause.pattern().kind() == PatternKind::BindingPattern) {
-      return true;
-    }
+    matrix.Add({&clause.pattern()});
   }
-  return false;
+  return matrix.IsRedundant({AbstractPattern::MakeWildcard()});
 }
 
 auto TypeChecker::ExpectReturnOnAllPaths(

explorer/testdata/function/fail_non_exhaustive_match.carbon

@@ -11,7 +11,8 @@
 package ExplorerTest api;
 
 fn Main() -> i32 {
-  match (0) {
+  var n: i32 = 0;
+  match (n) {
     case 1 => { return 0; }
   }
 // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/function/fail_non_exhaustive_match.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type

explorer/testdata/function/non_exhaustive_match_no_return_type.carbon

@@ -0,0 +1,24 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+fn F(n: i32) {
+  match (n) {
+    case 1 => { return; }
+  }
+  // No diagnostic: this is reachable but that's OK.
+}
+
+fn Main() -> i32 {
+  F(0);
+  return 0;
+}

explorer/testdata/function/non_exhaustive_match_return.carbon

@@ -0,0 +1,20 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 1
+
+package ExplorerTest api;
+
+fn Main() -> i32 {
+  var n: i32 = 0;
+  match (n) {
+    case 1 => { return 0; }
+  }
+  return 1;
+}

explorer/testdata/match/exhaustive.carbon

@@ -0,0 +1,37 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 3
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    case (Opt.None(), Opt.None()) => { return 0; }
+  }
+}
+
+fn B(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.None(), _: auto) => { return 0; }
+    case (Opt.Some(n: i32), Opt.None()) => { return n; }
+    case (Opt.Some(n: i32), Opt.Some(m: i32)) => { return n + m; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1)) + B(Opt.Some(2), Opt.None());
+}

explorer/testdata/match/exhaustive_bool.carbon

@@ -0,0 +1,23 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 2
+
+package ExplorerTest api;
+
+fn A(b: bool) -> i32 {
+  match (b) {
+    case false => { return 1; }
+    case true => { return 2; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(true);
+}

explorer/testdata/match/exhaustive_exponential_8x.carbon

@@ -0,0 +1,33 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  match ((F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 1; }
+    case (_: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 3; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 8; }
+  }
+}

explorer/testdata/match/exhaustive_exponential_series_t.carbon

@@ -0,0 +1,41 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // This is T8 from http://moscova.inria.fr/~maranget/papers/warn/warn014.html
+  match ((F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 1; }
+    case (_: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 3; }
+    case (_: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B()) => { return 9; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A()) => { return 10; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B()) => { return 11; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A()) => { return 12; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B()) => { return 13; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A()) => { return 14; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 15; }
+  }
+}

explorer/testdata/match/fail_exhaustive_exponential_9x.carbon

@@ -0,0 +1,35 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // Note, this match is exhaustive, but it exceeds our depth limit.
+  match ((F(), F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 1; }
+    case (_: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 3; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 9; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_exponential_9x.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}

explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon

@@ -0,0 +1,44 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // This is T9 from http://moscova.inria.fr/~maranget/papers/warn/warn014.html
+  // Note, this match is exhaustive, but it exceeds our depth limit.
+  match ((F(), F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 1; }
+    case (_: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 3; }
+    case (_: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 9; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A()) => { return 10; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B()) => { return 11; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A()) => { return 12; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B()) => { return 13; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A()) => { return 14; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B()) => { return 15; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A()) => { return 16; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 17; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}

explorer/testdata/match/fail_exhaustive_int.carbon

@@ -0,0 +1,23 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+fn A(n: i32) -> i32 {
+  match (n) {
+    case 1 => { return 1; }
+    case 2 => { return 2; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_int.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
+
+fn Main() -> i32 {
+  return A(0);
+}

explorer/testdata/match/fail_not_exhaustive.carbon

@@ -0,0 +1,28 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_exhaustive.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}

explorer/testdata/match/fail_not_reachable.carbon

@@ -0,0 +1,30 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_reachable.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    case (Opt.Some(m: i32), Opt.Some(n: i32)) => { return m + n; }
+  }
+  return 0;
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}

explorer/testdata/match/fail_not_reachable_default.carbon

@@ -0,0 +1,31 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.None(), Opt.None()) => { return 0; }
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_reachable_default.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    default => { return -1; }
+  }
+  return 0;
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}

explorer/testdata/match/fail_redundant_int.carbon

@@ -0,0 +1,24 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+fn A(n: i32) -> i32 {
+  match (n) {
+    case 1 => { return 1; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_redundant_int.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    case 1 => { return 2; }
+    case (_: i32) => { return 3; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(1);
+}