Handle enum constants in switch expressions correctly

src/main/java/org/checkerframework/specimin/JavaParserUtil.java

@@ -22,7 +22,9 @@
 import com.github.javaparser.ast.expr.LambdaExpr;
 import com.github.javaparser.ast.expr.MethodCallExpr;
 import com.github.javaparser.ast.expr.MethodReferenceExpr;
+import com.github.javaparser.ast.expr.NameExpr;
 import com.github.javaparser.ast.expr.ObjectCreationExpr;
+import com.github.javaparser.ast.expr.SwitchExpr;
 import com.github.javaparser.ast.expr.VariableDeclarationExpr;
 import com.github.javaparser.ast.nodeTypes.NodeWithArguments;
 import com.github.javaparser.ast.nodeTypes.NodeWithDeclaration;
@@ -37,6 +39,8 @@
 import com.github.javaparser.ast.stmt.ExpressionStmt;
 import com.github.javaparser.ast.stmt.ReturnStmt;
 import com.github.javaparser.ast.stmt.Statement;
+import com.github.javaparser.ast.stmt.SwitchEntry;
+import com.github.javaparser.ast.stmt.SwitchStmt;
 import com.github.javaparser.ast.type.ClassOrInterfaceType;
 import com.github.javaparser.ast.type.Type;
 import com.github.javaparser.ast.type.TypeParameter;
@@ -179,24 +183,6 @@ public static boolean isAClassName(String string) {
     return Character.isUpperCase(first);
   }
 
-  /**
-   * Returns true if a simple name looks like a constant; i.e., all its characters are either
-   * capital or _. This is a heuristic.
-   *
-   * @param simpleName The simple name to check, should contain no dots
-   * @return If it looks like a constant
-   */
-  public static boolean looksLikeAConstant(String simpleName) {
-    for (int i = 0; i < simpleName.length(); i++) {
-      char character = simpleName.charAt(i);
-      if (!Character.isUpperCase(character) && character != '_') {
-        return false;
-      }
-    }
-
-    return true;
-  }
-
   /**
    * Utility method to check if the given declaration is a local class declaration.
    *
@@ -1053,6 +1039,20 @@ public static int countNumberOfArrayBrackets(String name) {
     return count;
   }
 
+  /**
+   * Checks if the given name is in ALL_CAPS, as is the standard convention for constants. Heuristic
+   * for detecting likely enum constants.
+   */
+  public static boolean isProbablyAConstant(String simpleName) {
+    for (int i = 0; i < simpleName.length(); i++) {
+      char character = simpleName.charAt(i);
+      if (!Character.isUpperCase(character) && character != '_' && !Character.isDigit(character)) {
+        return false;
+      }
+    }
+    return true;
+  }
+
   /**
    * When getting the scope/children of a ClassOrInterfaceType, it returns another
    * ClassOrInterfaceType. However, it does not differentiate between whether this type is a package
@@ -2545,6 +2545,52 @@ public static Node findClosestMethodOrLambdaAncestor(ReturnStmt returnStmt) {
     return ancestor;
   }
 
+  /**
+   * If the given name expression is used as (or within) a case label of an enclosing switch
+   * statement or switch expression, returns the selector expression of that switch. Otherwise
+   * (including when the name appears in the body/statements of a switch entry, or outside of any
+   * switch), returns null.
+   *
+   * <p>This implements Java's special scoping rule for switches over enums: an unqualified enum
+   * constant that is a member of the selector's type may be used as a case label without an
+   * explicit import. The special scoping does <em>not</em> extend to the bodies of the switch
+   * entries, so only names appearing in the labels are treated specially.
+   *
+   * @param nameExpr a possible unqualified enum constant
+   * @return the enclosing switch's selector expression if nameExpr is a case label, or null
+   */
+  public static @Nullable Expression getEnclosingSwitchSelectorIfCaseLabel(NameExpr nameExpr) {
+    SwitchEntry entry = nameExpr.findAncestor(SwitchEntry.class).orElse(null);
+    if (entry == null) {
+      return null;
+    }
+    // The name must appear within one of the entry's labels (i.e., the "case X" part), not within
+    // its statements/body, where unqualified enum constants are not in scope.
+    boolean inLabel = false;
+    for (Expression label : entry.getLabels()) {
+      // Reference equality is intentional: we need to know whether this exact name node is a label,
+      // not whether some structurally-equal name is (the same constant may also appear in the
+      // body). No interning is okay because this is a pointer-equality check.
+      // Extracted into a local variable to minimize suppression scope.
+      @SuppressWarnings({"ReferenceEquality", "not.interned"})
+      boolean equals = label == nameExpr;
+      if (equals || label.isAncestorOf(nameExpr)) {
+        inLabel = true;
+        break;
+      }
+    }
+    if (!inLabel) {
+      return null;
+    }
+    Node switchNode = entry.getParentNode().orElse(null);
+    if (switchNode instanceof SwitchStmt switchStmt) {
+      return switchStmt.getSelector();
+    } else if (switchNode instanceof SwitchExpr switchExpr) {
+      return switchExpr.getSelector();
+    }
+    return null;
+  }
+
   /**
    * This method handles a very specific case: if an unsolved method call has a scope whose type is
    * a supertype of the type this method is being called in, then it will try to find a method with

src/main/java/org/checkerframework/specimin/unsolved/FullyQualifiedNameGenerator.java

@@ -23,6 +23,7 @@
 import com.github.javaparser.ast.expr.MethodReferenceExpr;
 import com.github.javaparser.ast.expr.Name;
 import com.github.javaparser.ast.expr.NameExpr;
+import com.github.javaparser.ast.expr.SwitchExpr;
 import com.github.javaparser.ast.nodeTypes.NodeWithArguments;
 import com.github.javaparser.ast.nodeTypes.NodeWithCondition;
 import com.github.javaparser.ast.nodeTypes.NodeWithExtends;
@@ -32,8 +33,11 @@
 import com.github.javaparser.ast.nodeTypes.NodeWithTraversableScope;
 import com.github.javaparser.ast.nodeTypes.NodeWithType;
 import com.github.javaparser.ast.nodeTypes.NodeWithVariables;
+import com.github.javaparser.ast.stmt.ExpressionStmt;
 import com.github.javaparser.ast.stmt.ForEachStmt;
 import com.github.javaparser.ast.stmt.ReturnStmt;
+import com.github.javaparser.ast.stmt.SwitchEntry;
+import com.github.javaparser.ast.stmt.YieldStmt;
 import com.github.javaparser.ast.type.ClassOrInterfaceType;
 import com.github.javaparser.ast.type.ReferenceType;
 import com.github.javaparser.ast.type.Type;
@@ -1908,6 +1912,23 @@ else if (parentNode instanceof BinaryExpr binary) {
         }
         return Set.of(new FullyQualifiedNameSet(result, notArray.typeArguments()));
       }
+    } else if (parentNode instanceof ExpressionStmt exprStmt
+        && exprStmt.getParentNode().orElse(null) instanceof SwitchEntry arrowEntry
+        && arrowEntry.getParentNode().orElse(null) instanceof SwitchExpr arrowSwitchExpr
+        && isExpressionNotInProgress(arrowSwitchExpr)) {
+      // The value of an arrow-rule switch-expression arm (`case X -> value;`, stored as an
+      // ExpressionStmt directly under the entry) has the type of the enclosing switch expression,
+      // which is itself inferred from its surrounding context (e.g. `int z = switch (m) { ... }`).
+      return getFQNsForExpressionType(arrowSwitchExpr);
+    } else if (parentNode instanceof YieldStmt) {
+      // A `yield value;` yields the value of the enclosing switch expression, so the yielded
+      // expression has that switch expression's type.
+      SwitchEntry entry = parentNode.findAncestor(SwitchEntry.class).orElse(null);
+      if (entry != null
+          && entry.getParentNode().orElse(null) instanceof SwitchExpr switchExpr
+          && isExpressionNotInProgress(switchExpr)) {
+        return getFQNsForExpressionType(switchExpr);
+      }
     }
     return null;
   }

src/main/java/org/checkerframework/specimin/unsolved/UnsolvedSymbolGenerator.java

@@ -499,7 +499,7 @@ private UnsolvedMethodAlternates findOrGenerateAnnotationMemberValueMethod(
                   .next();
         }
       } else if (toLookUpTypeFor instanceof FieldAccessExpr fieldAccess
-          && JavaParserUtil.looksLikeAConstant(fieldAccess.getNameAsString())) {
+          && JavaParserUtil.isProbablyAConstant(fieldAccess.getNameAsString())) {
         // If it looks like an enum, it probably is
         rawFqns =
             fullyQualifiedNameGenerator
@@ -742,6 +742,12 @@ private void handleNameExpr(NameExpr nameExpr, List<UnsolvedSymbolAlternates<?>>
       return;
     }
 
+    // An unqualified enum constant used as a switch case label is a member of the selector's enum
+    // type, not a field of the enclosing class, and requires no import. Handle that special case.
+    if (tryHandleSwitchEnumConstant(nameExpr, result)) {
+      return;
+    }
+
     // class name
     if (JavaParserUtil.isAClassName(nameExpr.getNameAsString())) {
       for (FullyQualifiedNameSet potentialFQNs :
@@ -816,6 +822,69 @@ private void handleNameExpr(NameExpr nameExpr, List<UnsolvedSymbolAlternates<?>>
     }
   }
 
+  /**
+   * Handles the special case of an unqualified enum constant used as a switch case label. Java
+   * permits an unqualified enum constant that is a member of the switch selector's type to be used
+   * as a case label without an explicit import. Such a name is therefore a member of the (possibly
+   * synthetic) enum used as the selector, not a field of the enclosing class.
+   *
+   * @param nameExpr the unsolved name expression
+   * @param result the list of generated/found symbols to add to
+   * @return true if nameExpr was handled as an enum constant (so no further handling is needed)
+   */
+  private boolean tryHandleSwitchEnumConstant(
+      NameExpr nameExpr, List<UnsolvedSymbolAlternates<?>> result) {
+    // Heuristic: enum constants follow the ALL_CAPS convention for constants. This avoids treating,
+    // e.g., a call to a locally-scoped variable in a case label as an enum constant.
+    if (!JavaParserUtil.isProbablyAConstant(nameExpr.getNameAsString())) {
+      return false;
+    }
+    Expression selector = JavaParserUtil.getEnclosingSwitchSelectorIfCaseLabel(nameExpr);
+    if (selector == null) {
+      return false;
+    }
+    // Determine the (possibly synthetic) type of the switch selector.
+    Set<FullyQualifiedNameSet> fqns =
+        fullyQualifiedNameGenerator.getFQNsForExpressionType(selector);
+    // TODO: should we take the possibility of multiple members of fqns here into account? I think
+    // this will almost always return a set of size 0 or 1.
+    Set<String> enumFQNs = fqns.isEmpty() ? null : fqns.iterator().next().erasedFqns();
+    if (enumFQNs == null || enumFQNs.isEmpty() || doesOverlapWithKnownType(enumFQNs)) {
+      // If the selector's type is a known type, it is not a synthetic enum that we control, so fall
+      // back to the normal handling. (In practice, the constants of a known enum would already have
+      // resolved above, so this only guards against unexpected inputs.)
+      return false;
+    }
+
+    // Check to make sure we don't add a duplicate enum constant.
+    Set<String> fieldFQNs =
+        enumFQNs.stream()
+            .map(fqn -> fqn + "#" + nameExpr.getNameAsString())
+            .collect(Collectors.toSet());
+    UnsolvedSymbolAlternates<?> existing = findExistingAndUpdateFQNs(fieldFQNs);
+    if (existing instanceof UnsolvedFieldAlternates) {
+      return true;
+    }
+
+    // Find or create the synthetic enum, mark it as an enum, and add this constant to it.
+    UnsolvedClassOrInterfaceAlternates enumType =
+        findExistingAndUpdateFQNsOrCreateNewType(enumFQNs);
+    enumType.setType(UnsolvedClassOrInterfaceType.ENUM);
+
+    // Enum constants are represented as (static, final) fields of the enum; only the name is used
+    // when the declaring type is an enum, so the field's type is unimportant.
+    UnsolvedFieldAlternates constant =
+        UnsolvedFieldAlternates.create(
+            nameExpr.getNameAsString(),
+            getOrCreateMemberTypeFromFQNs(new FullyQualifiedNameSet(enumFQNs)),
+            List.of(enumType),
+            true,
+            true);
+    addNewSymbolToGeneratedSymbolsMap(constant);
+    result.add(constant);
+    return true;
+  }
+
   /**
    * Helper method for {@link #inferContextImpl(Node, List)}. Adds the existing definition to the
    * result if found, or a new definition if one does not already exist.

src/main/resources/min_program_compile_status.json

@@ -16,7 +16,6 @@
   "cf-691": "PASS",
   "Issue689": "PASS",
   "cf-6388": "PASS",
-  "cf-3025": "PASS",
   "jdk-8288590": "PASS",
   "na-89": "PASS",
   "na-97": "PASS",

src/main/resources/preservation_status.json

@@ -16,7 +16,6 @@
   "cf-691": "PASS",
   "Issue689": "PASS",
   "cf-6388": "PASS",
-  "cf-3025": "PASS",
   "jdk-8319461": "PASS",
   "jdk-8288590": "PASS",
   "na-89": "FAIL",

src/main/resources/target_status.json

@@ -16,7 +16,6 @@
   "cf-691": "PASS",
   "Issue689": "PASS",
   "cf-6388": "PASS",
-  "cf-3025": "PASS",
   "jdk-8319461": "PASS",
   "jdk-8288590": "PASS",
   "na-89": "PASS",

src/test/java/org/checkerframework/specimin/SwitchEnumConstant2Test.java

@@ -0,0 +1,19 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.jupiter.api.Test;
+
+/**
+ * This test checks that Specimin properly handles the scoping of enum constants used in switch
+ * statements and expressions, which have special (weird) rules. This variant checks that only
+ * constants used in the case part of the switch go into the enum.
+ */
+public class SwitchEnumConstant2Test {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "switchenumconstant2",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#bar(MyEnum)"});
+  }
+}

src/test/java/org/checkerframework/specimin/SwitchEnumConstantTest.java

@@ -0,0 +1,18 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.jupiter.api.Test;
+
+/**
+ * This test checks that Specimin properly handles the scoping of enum constants used in switch
+ * statements and expressions, which have special (weird) rules.
+ */
+public class SwitchEnumConstantTest {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "switchenumconstant",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#bar(MyEnum)"});
+  }
+}

src/test/resources/switchenumconstant/expected/com/example/Simple.java

@@ -0,0 +1,24 @@
+package com.example;
+
+import org.example.MyEnum;
+
+class Simple {
+    void bar(MyEnum m) {
+        switch(m) {
+            case CONSTANT1:
+                int x = 5 + 8;
+                break;
+            case CONSTANT2:
+                int y = 3 * 2;
+                break;
+        }
+        int z = switch (m) {
+            case CONSTANT3 ->
+                    5;
+            case CONSTANT4 ->
+                    6;
+            default ->
+                    0;
+        };
+    }
+}

src/test/resources/switchenumconstant/expected/org/example/MyEnum.java

@@ -0,0 +1,5 @@
+package org.example;
+
+public enum MyEnum {
+    CONSTANT4, CONSTANT3, CONSTANT2, CONSTANT1;
+}

src/test/resources/switchenumconstant/input/com/example/Simple.java

@@ -0,0 +1,35 @@
+package com.example;
+
+import org.example.MyEnum;
+
+// The Java scoping rules for switches over enum constants
+// are surprisingly complicated and poorly documented by the JLS.
+// Specifically, Java permits an unqualified enum constant that
+// is a member of the type used as the selector expression in
+// a switch statement to be used either as a rule or as a case,
+// without an explicit import. Specimin needs to correctly
+// identify those cases as enum constants, because otherwise
+// there usually is not _anything_ in scope that matches, which
+// causes us to produce non-sensical output. However, I don't
+// _think_ that the unqualified enum constant names can be used
+// in the bodies of the expressions in the rest of the switch,
+// and have implemented Specimin's logic assuming that is so.
+// This test case checks that we get this right.
+class Simple {
+    // Target method.
+    void bar(MyEnum m) {
+        switch(m) {
+            case CONSTANT1:
+                int x = 5 + 8; // nonsense code
+                break;
+            case CONSTANT2:
+                int y = 3 * 2;
+                break;
+        }
+        int z = switch (m) {
+            case CONSTANT3 -> 5;
+            case CONSTANT4 -> 6;
+            default -> 0;
+        };
+    }
+}

src/test/resources/switchenumconstant2/expected/com/example/Foo.java

@@ -0,0 +1,7 @@
+package com.example;
+
+public class Foo {
+    public int CONSTANT6;
+
+    public int CONSTANT5;
+}