Compute the type of switch expressions and check them. (#4978)

checker/tests/nullness/java17/SwitchExpressionInvariant.java

@@ -0,0 +1,27 @@
+// @below-java17-jdk-skip-test
+import java.util.List;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class SwitchExpressionInvariant {
+  public static boolean flag = false;
+
+  void method(
+      List<@NonNull String> nonnullStrings, List<@Nullable String> nullableStrings, int fenum) {
+
+    List<@NonNull String> list =
+        // :: error: (assignment)
+        switch (fenum) {
+            // :: error: (switch.expression)
+          case 1 -> nonnullStrings;
+          default -> nullableStrings;
+        };
+
+    List<@Nullable String> list2 =
+        switch (fenum) {
+            // :: error: (switch.expression)
+          case 1 -> nonnullStrings;
+          default -> nullableStrings;
+        };
+  }
+}

docs/CHANGELOG.md

@@ -3,6 +3,8 @@ Version 3.21.0 (December 17, 2021)
 
 **User-visible changes:**
 
+The Checker Framework now more precisely computes the type of a switch expression.
+
 **Implementation details:**
 
 **Closed issues:**

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -138,6 +138,8 @@
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.Pair;
+import org.checkerframework.javacutil.SwitchExpressionScanner;
+import org.checkerframework.javacutil.SwitchExpressionScanner.FunctionalSwitchExpressionScanner;
 import org.checkerframework.javacutil.TreePathUtil;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
@@ -342,6 +344,10 @@ public Void scan(@Nullable Tree tree, Void p) {
     if (tree != null && getCurrentPath() != null) {
       this.atypeFactory.setVisitorTreePath(new TreePath(getCurrentPath(), tree));
     }
+    if (tree != null && tree.getKind().name().equals("SWITCH_EXPRESSION")) {
+      visitSwitchExpression17(tree);
+      return null;
+    }
     return super.scan(tree, p);
   }
 
@@ -2117,6 +2123,33 @@ public Void visitConditionalExpression(ConditionalExpressionTree node, Void p) {
     return super.visitConditionalExpression(node, p);
   }
 
+  /**
+   * This method validates the type of the switch expression. It issues an error if the type of a
+   * value that the switch expression can result is not a subtype of the switch type.
+   *
+   * <p>If a subclass overrides this method, it must call {@code super.scan(switchExpressionTree,
+   * null)} so that the blocks and statements in the cases are checked.
+   *
+   * @param switchExpressionTree a {@code SwitchExpressionTree}
+   */
+  public void visitSwitchExpression17(Tree switchExpressionTree) {
+    boolean valid = validateTypeOf(switchExpressionTree);
+    if (valid) {
+      AnnotatedTypeMirror switchType = atypeFactory.getAnnotatedType(switchExpressionTree);
+      SwitchExpressionScanner<Void, Void> scanner =
+          new FunctionalSwitchExpressionScanner<>(
+              (ExpressionTree valueTree, Void unused) -> {
+                BaseTypeVisitor.this.commonAssignmentCheck(
+                    switchType, valueTree, "switch.expression");
+                return null;
+              },
+              (r1, r2) -> null);
+
+      scanner.scanSwitchExpression(switchExpressionTree, null);
+    }
+    super.scan(switchExpressionTree, null);
+  }
+
   // **********************************************************************
   // Check for illegal re-assignment
   // **********************************************************************

framework/src/main/java/org/checkerframework/common/basetype/messages.properties

@@ -13,6 +13,7 @@ vector.copyinto=incompatible component type in Vector.copyinto.%nfound   : %s%nr
 return=incompatible types in return.%ntype of expression: %s%nmethod return type: %s
 annotation=incompatible types in annotation.%nfound   : %s%nrequired: %s
 conditional=incompatible types in conditional expression.%nfound   : %s%nrequired: %s
+switch.expression=incompatible types in switch expression.%nfound   : %s%nrequired: %s
 type.argument=incompatible type argument for type parameter %s of %s.%nfound   : %s%nrequired: %s
 argument=incompatible argument for parameter %s of %s.%nfound   : %s%nrequired: %s
 varargs=incompatible types in varargs.%nfound   : %s%nrequired: %s

framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java

@@ -36,6 +36,8 @@
 import org.checkerframework.framework.util.AnnotatedTypes;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.ElementUtils;
+import org.checkerframework.javacutil.SwitchExpressionScanner;
+import org.checkerframework.javacutil.SwitchExpressionScanner.FunctionalSwitchExpressionScanner;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
 
@@ -176,16 +178,29 @@ public AnnotatedTypeMirror defaultAction(Tree tree, AnnotatedTypeFactory f) {
   /**
    * Compute the type of the switch expression tree.
    *
-   * @param switchExpressionTree SwitchExpressionTree; typed as Tree to be backward-compatible
-   * @param f AnnotatedTypeFactory
+   * @param switchExpressionTree a SwitchExpressionTree; typed as Tree so method signature is
+   *     backward-compatible
+   * @param f an AnnotatedTypeFactory
    * @return the type of the switch expression
    */
   public AnnotatedTypeMirror visitSwitchExpressionTree17(
       Tree switchExpressionTree, AnnotatedTypeFactory f) {
-    // TODO: Properly compute the type from the cases.
-    AnnotatedTypeMirror result = f.type(switchExpressionTree);
-    result.addAnnotations(f.getQualifierHierarchy().getTopAnnotations());
-    return result;
+    TypeMirror switchTypeMirror = TreeUtils.typeOf(switchExpressionTree);
+    SwitchExpressionScanner<AnnotatedTypeMirror, Void> luber =
+        new FunctionalSwitchExpressionScanner<>(
+            // Function applied to each result expression of the switch expression.
+            (valueTree, unused) -> f.getAnnotatedType(valueTree),
+            // Function used to combine the types of each result expression.
+            (type1, type2) -> {
+              if (type1 == null) {
+                return type2;
+              } else if (type2 == null) {
+                return type1;
+              } else {
+                return AnnotatedTypes.leastUpperBound(f, type1, type2, switchTypeMirror);
+              }
+            });
+    return luber.scanSwitchExpression(switchExpressionTree, null);
   }
 
   @Override

framework/tests/value/java17/SwitchExpressionTyping.java

@@ -0,0 +1,100 @@
+// @below-java17-jdk-skip-test
+import org.checkerframework.common.value.qual.IntVal;
+
+public class SwitchExpressionTyping {
+  public static boolean flag = false;
+
+  void method0(String s) {
+    @IntVal({0, 1, 2, 3}) int o =
+        switch (s) {
+          case "Hello?" -> {
+            throw new RuntimeException();
+          }
+          case "Hello" -> 0;
+          case "Bye" -> 1;
+          case "Later" -> 2;
+          case "What?" -> throw new RuntimeException();
+          default -> 3;
+        };
+  }
+
+  void method1(String s) {
+    @IntVal({1, 2, 3}) int o =
+        switch (s) {
+          case "Hello?" -> 1;
+          case "Hello" -> 1;
+          case "Bye" -> 1;
+          case "Later" -> 1;
+          case "What?" -> {
+            if (flag) {
+              yield 2;
+            }
+            yield 3;
+          }
+          default -> 1;
+        };
+
+    @IntVal(1) int o2 =
+        // :: error: (assignment)
+        switch (s) {
+          case "Hello?" -> 1;
+          case "Hello" -> 1;
+          case "Bye" -> 1;
+          case "Later" -> 1;
+          case "What?" -> {
+            if (flag) {
+              yield 2;
+            }
+            yield 3;
+          }
+          default -> 1;
+        };
+  }
+
+  void method2(String s, String r) {
+    @IntVal({0, 1, 2, 3}) int o =
+        switch (s) {
+          case "Hello?" -> {
+            if (flag) {
+              throw new RuntimeException();
+            }
+            yield 2;
+          }
+          case "Hello" -> {
+            int i =
+                switch (r) {
+                  case "Hello" -> 4;
+                  case "Bye" -> 5;
+                  case "Later" -> 6;
+                  default -> 42;
+                };
+            yield 0;
+          }
+          case "Bye" -> 1;
+          case "Later" -> {
+            int i =
+                switch (r) {
+                  case "Hello":
+                    {
+                      yield 4;
+                    }
+                  case "Bye":
+                    {
+                      yield 5;
+                    }
+                  case "Later":
+                    {
+                      yield 6;
+                    }
+                  default:
+                    {
+                      yield 42;
+                    }
+                };
+            yield 2;
+          }
+          case "What?" -> throw new RuntimeException();
+          default -> 3;
+        };
+  }
+}