Check exhaustiveness of function-ending match statements (#882)

Co-authored-by: Jon Meow <46229924+jonmeow@users.noreply.github.com>

executable_semantics/interpreter/type_checker.cpp

@@ -982,6 +982,21 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s, TypeEnv types,
   }  // switch
 }
 
+// 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 {
+  for (const Match::Clause& clause : match.clauses()) {
+    // A pattern consisting of a single variable binding is guaranteed to match.
+    if (clause.pattern().kind() == Pattern::Kind::BindingPattern) {
+      return true;
+    }
+  }
+  return false;
+}
+
 void TypeChecker::ExpectReturnOnAllPaths(
     std::optional<Nonnull<Statement*>> opt_stmt, SourceLocation source_loc) {
   if (!opt_stmt) {
@@ -993,6 +1008,11 @@ void TypeChecker::ExpectReturnOnAllPaths(
   switch (stmt->kind()) {
     case Statement::Kind::Match: {
       auto& match = cast<Match>(*stmt);
+      if (!IsExhaustive(match)) {
+        FATAL_COMPILATION_ERROR(source_loc)
+            << "non-exhaustive match may allow control-flow to reach the end "
+               "of a function that provides a `->` return type";
+      }
       std::vector<Match::Clause> new_clauses;
       for (auto& clause : match.clauses()) {
         ExpectReturnOnAllPaths(&clause.statement(), stmt->source_loc());

executable_semantics/testdata/function/fail_non_exhaustive_match.carbon

@@ -0,0 +1,18 @@
+// 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 executable_semantics %s 2>&1 | \
+// RUN:   FileCheck --match-full-lines --allow-unused-prefixes=false %s
+// RUN: not executable_semantics --trace %s 2>&1 | \
+// RUN:   FileCheck --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: executable_semantics %s
+// CHECK: COMPILATION ERROR: {{.*}}/executable_semantics/testdata/function/fail_non_exhaustive_match.carbon:18: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+
+package ExecutableSemanticsTest api;
+
+fn main() -> i32 {
+  match (0) {
+    case 1 => return 0;
+  }
+}

executable_semantics/testdata/function/return_exhaustive_match.carbon

@@ -0,0 +1,19 @@
+// 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: executable_semantics %s 2>&1 | \
+// RUN:   FileCheck --match-full-lines --allow-unused-prefixes=false %s
+// RUN: executable_semantics --trace %s 2>&1 | \
+// RUN:   FileCheck --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: executable_semantics %s
+// CHECK: result: 1
+
+package ExecutableSemanticsTest api;
+
+fn main() -> i32 {
+  match (0) {
+    case _: auto => return 1;
+  }
+  // We don't need a `return` here because the match is exhaustive.
+}

executable_semantics/testdata/match/placeholder.carbon

@@ -17,4 +17,5 @@ fn main() -> i32 {
     case (_: i32, _: auto, x: i32, y: auto) =>
       return y - x - 1;
   }
+  return 1;
 }

executable_semantics/testdata/struct/empty.carbon

@@ -22,4 +22,5 @@ fn main() -> i32 {
       return 0;
     }
   }
+  return 1;
 }

executable_semantics/testdata/tuple/match.carbon

@@ -17,4 +17,5 @@ fn main() -> i32 {
     case (a: auto, b: auto) =>
       return a + b - 7;
   }
+  return 1;
 }

executable_semantics/testdata/tuple/match_nested.carbon

@@ -19,4 +19,5 @@ fn main() -> i32 {
     case ((a: auto, b: auto), c: auto) =>
       return a - b + c[0] - c[1] + 2;
   }
+  return 1;
 }

executable_semantics/testdata/tuple/match_with_named.carbon

@@ -19,4 +19,5 @@ fn main() -> i32 {
     case (a: auto, .x = b: auto) =>
       return a - b + 3;
   }
+  return 1;
 }