Fix rules for switch statement exhaustiveness (#620)

checker/tests/nullness/java21/FlowSwitch.java

@@ -82,8 +82,8 @@ void test3(Pair<I> p2) {
     String s = null;
     I e = null;
     switch (p2) {
-      case Pair<I>(I i, C c) -> {e = c; s="";}
-      case Pair<I>(I i, D d) -> {e = d; s="";}
+      case Pair<I>(I i, C c) -> { e = c; s = ""; }
+      case Pair<I>(I i, D d) -> { e = d; s = ""; }
     }
     s.toString();
     e.toString();
@@ -94,5 +94,6 @@ void test3(Pair<I> p2) {
       case Pair<I>(D d, C c) -> e2 = d;
       case Pair<I>(D d1, D d2) -> e2 = d2;
     }
+    e2.toString();
   }
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

@@ -46,7 +46,6 @@
 import com.sun.source.tree.SynchronizedTree;
 import com.sun.source.tree.ThrowTree;
 import com.sun.source.tree.Tree;
-import com.sun.source.tree.Tree.Kind;
 import com.sun.source.tree.TryTree;
 import com.sun.source.tree.TypeCastTree;
 import com.sun.source.tree.TypeParameterTree;
@@ -2448,6 +2447,14 @@ private SwitchBuilder(Tree switchTree) {
                                 env.getTypeUtils()));
             }
 
+            // JSL 14.11.2
+            // https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2
+            // states "For compatibility reasons, switch statements that are not enhanced switch
+            // statements are not required to be exhaustive".
+            // Switch expressions and enhanced switch statements are exhaustive.
+            boolean switchExprOrEnhanced =
+                    !TreeUtils.isSwitchStatement(switchTree)
+                            || TreeUtils.isEnhancedSwitchStatement((SwitchTree) switchTree);
             // Build CFG for the cases.
             int defaultIndex = -1;
             for (int i = 0; i < numCases; ++i) {
@@ -2458,8 +2465,9 @@ private SwitchBuilder(Tree switchTree) {
                     // build the default case last.
                     defaultIndex = i;
                 } else if (i == numCases - 1 && defaultIndex == -1) {
-                    // This is the last case, and it's not a default case.
-                    buildCase(caseTree, i, exhaustiveIgnoreDefault());
+                    // This is the last case, and there is no default case.
+                    // Switch expressions and enhanced switch statements are exhaustive.
+                    buildCase(caseTree, i, switchExprOrEnhanced);
                 } else {
                     buildCase(caseTree, i, false);
                 }
@@ -2672,50 +2680,6 @@ private void buildCase(CaseTree caseTree, int index, boolean isLastCaseOfExhaust
             assert breakTargetLC != null : "no target for case statement";
             extendWithExtendedNode(new UnconditionalJump(breakTargetLC.accessLabel()));
         }
-
-        /**
-         * Returns true if the switch is exhaustive; ignoring any default case
-         *
-         * @return true if the switch is exhaustive; ignoring any default case
-         */
-        private boolean exhaustiveIgnoreDefault() {
-            // Switch expressions are always exhaustive, but they might have a default case, which
-            // is why the above loop is not fused with the below loop.
-            if (!TreeUtils.isSwitchStatement(switchTree)) {
-                return true;
-            }
-
-            int enumCaseLabels = 0;
-            for (CaseTree caseTree : caseTrees) {
-                for (Tree caseLabel : CaseUtils.getLabels(caseTree)) {
-                    // Java guarantees that if one of the cases is the null literal, the switch is
-                    // exhaustive.
-                    // Also if certain other constructs exist.
-                    if (caseLabel.getKind() == Kind.NULL_LITERAL
-                            || TreeUtils.isBindingPatternTree(caseLabel)
-                            || TreeUtils.isDeconstructionPatternTree(caseLabel)) {
-                        return true;
-                    }
-                    if (caseLabel.getKind() == Kind.IDENTIFIER) {
-                        enumCaseLabels++;
-                    }
-                }
-            }
-
-            TypeMirror selectorTypeMirror = TreeUtils.typeOf(selectorExprTree);
-            if (selectorTypeMirror.getKind() == TypeKind.DECLARED) {
-                DeclaredType declaredType = (DeclaredType) selectorTypeMirror;
-                TypeElement declaredTypeElement = (TypeElement) declaredType.asElement();
-                if (declaredTypeElement.getKind() == ElementKind.ENUM) {
-                    // The switch expression's type is an enumerated type.
-                    List<VariableElement> enumConstants =
-                            ElementUtils.getEnumConstants(declaredTypeElement);
-                    return enumConstants.size() == enumCaseLabels;
-                }
-            }
-
-            return false;
-        }
     }
 
     @Override

docs/CHANGELOG.md

@@ -5,8 +5,13 @@ Version 3.39.0-eisop2 (October ??, 2023)
 
 **Implementation details:**
 
+New method `TreeUtils#isEnhancedSwitchStatement` to determine if a switch statement tree
+is an enhanced switch statement.
+
 **Closed issues:**
 
+eisop#609.
+
 
 Version 3.39.0-eisop1 (October 22, 2023)
 ----------------------------------------

framework/tests/all-systems/EnumSwitch.java

@@ -0,0 +1,21 @@
+// Test case for EISOP issue #609:
+// https://github.com/eisop/checker-framework/issues/609
+enum EnumSwitch {
+    FOO;
+
+    EnumSwitch getIt() {
+        return FOO;
+    }
+
+    String go() {
+        EnumSwitch e = getIt();
+        switch (e) {
+            case FOO:
+                return "foo";
+        }
+        // This location is reachable in general: the enum could evolve and add a new constant.
+        // This cannot be the case here, because this code is in the enum declaration.
+        // javac does not special case this and I do not see a reason to do so here.
+        throw new AssertionError(e);
+    }
+}

javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java

@@ -25,6 +25,7 @@
 import com.sun.source.tree.ParenthesizedTree;
 import com.sun.source.tree.PrimitiveTypeTree;
 import com.sun.source.tree.StatementTree;
+import com.sun.source.tree.SwitchTree;
 import com.sun.source.tree.Tree;
 import com.sun.source.tree.TreeVisitor;
 import com.sun.source.tree.TypeCastTree;
@@ -2411,6 +2412,39 @@ public static boolean isSwitchStatement(Tree tree) {
         return tree.getKind() == Tree.Kind.SWITCH;
     }
 
+    /**
+     * Returns true if the given switch statement tree is an enhanced switch statement, as described
+     * in <a href="https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2">JSL
+     * 14.11.2</a>.
+     *
+     * @param switchTree the switch statement to check
+     * @return true if the given tree is an enhanced switch statement
+     */
+    public static boolean isEnhancedSwitchStatement(SwitchTree switchTree) {
+        TypeMirror exprType = typeOf(switchTree.getExpression());
+        // TODO: this should be only char, byte, short, int, Character, Byte, Short, Integer. Is the
+        // over-approximation a problem?
+        Element exprElem = TypesUtils.getTypeElement(exprType);
+        boolean isNotEnum = exprElem == null || exprElem.getKind() != ElementKind.ENUM;
+        if (!TypesUtils.isPrimitiveOrBoxed(exprType)
+                && !TypesUtils.isString(exprType)
+                && isNotEnum) {
+            return true;
+        }
+
+        for (CaseTree caseTree : switchTree.getCases()) {
+            for (Tree caseLabel : CaseUtils.getLabels(caseTree)) {
+                if (caseLabel.getKind() == Tree.Kind.NULL_LITERAL
+                        || TreeUtils.isBindingPatternTree(caseLabel)
+                        || TreeUtils.isDeconstructionPatternTree(caseLabel)) {
+                    return true;
+                }
+            }
+        }
+
+        return false;
+    }
+
     /**
      * Returns the value (expression) for {@code yieldTree}.
      *