Correctly handle switches that use an unresolved enum as the selector

JavaParser.astub

@@ -37,3 +37,13 @@ package com.github.javaparser.ast.stmt;
 class IfStmt {
    IfStmt setElseStmt(@Nullable Statement elseStmt);
 }
+
+class SwitchEntry {
+    public SwitchEntry setGuard(@Nullable Expression guard);
+}
+
+package com.github.javaparser.ast;
+
+class Node {
+    public Node setComment(@Nullable Comment comment);
+}

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

@@ -333,7 +333,8 @@ else if (line.contains("void cannot be converted to")) {
         }
 
         if (line.contains("error: incompatible types")
-            || line.contains("error: incomparable types")) {
+            || line.contains("error: incomparable types")
+            || line.contains("cannot be converted to")) {
           if (line.contains("invalid method reference")
               || line.contains("bad return type in method reference")) {
             lookingForInvalidMethodReference = true;
@@ -478,7 +479,15 @@ private void updateTypeToChange(String errorMessage, String filePath) {
      * 1. error: incompatible types: <type1> cannot be converted to <type2>
      */
     if (errorMessage.contains("cannot be converted to")) {
-      String rhs = getTypeFrom(splitErrorMessage, 4, "cannot");
+      // There are two forms of this error message: the typical one (detailed above) and a
+      // special version from bad switch expressions, in which case this part appears on its
+      // own line, like this:
+      // com/example/Simple.java:18: error: incompatible types: bad type in switch expression
+      //                CONSTANT6;
+      //                ^
+      //    SyntheticTypeForCONSTANT6 cannot be converted to int
+      int startIndex = errorMessage.contains("error:") ? 4 : 0;
+      String rhs = getTypeFrom(splitErrorMessage, startIndex, "cannot");
       int toIndex = splitErrorMessage.indexOf("to");
       String lhs = getTypeFrom(splitErrorMessage, toIndex + 1, null);
       if ("Throwable".equals(lhs)) {

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

@@ -12,8 +12,9 @@
 import org.checkerframework.checker.signature.qual.ClassGetSimpleName;
 
 /**
- * An UnsolvedClassOrInterface instance is a representation of a class or an interface that can not
- * be solved by SymbolSolver. The reason is that the class file is not in the root directory.
+ * An UnsolvedClassOrInterface instance is a representation of a class, enum, or an interface that
+ * can not be solved by SymbolSolver. The reason is that the class file is not in the root
+ * directory.
  */
 public class UnsolvedClassOrInterface {
   /**
@@ -58,6 +59,15 @@ public class UnsolvedClassOrInterface {
   /** Is this class an annotation? */
   private boolean isAnAnnotation = false;
 
+  /** Is this an enum? */
+  private boolean isAnEnum = false;
+
+  /**
+   * The enum constants of this enum. Must be a linked set to ensure deterministic iteration order
+   * when writing out the constants for synthetic classes.
+   */
+  private final LinkedHashSet<String> enumConstants;
+
   /**
    * This class' constructor should be used for creating inner classes. Frankly, this design is a
    * mess (sorry) - controlling whether this is an inner class via inheritance is probably bad.
@@ -123,6 +133,7 @@ public UnsolvedClassOrInterface(
       this.extendsClause = " extends Exception";
     }
     this.isAnInterface = isAnInterface;
+    this.enumConstants = new LinkedHashSet<>();
   }
 
   /**
@@ -142,6 +153,41 @@ public void setIsAnInterfaceToTrue() {
     this.isAnInterface = true;
   }
 
+  /**
+   * Returns the value of isAnEnum.
+   *
+   * @return return true if the current UnsolvedClassOrInterface instance represents an enum.
+   */
+  public boolean isAnEnum() {
+    return isAnEnum;
+  }
+
+  /**
+   * Adds the given name to this enum's list of enum constants.
+   *
+   * @param enumConstantName the name of the constant
+   */
+  public void addEnumConstant(String enumConstantName) {
+    if (!isAnEnum) {
+      throw new RuntimeException(
+          "cannot add an enum constant to a synthetic class that is not an enum");
+    }
+    this.enumConstants.add(enumConstantName);
+  }
+
+  /**
+   * Sets isAnEnum to true. isAnEnum is monotonic: it can start as false and become true (because we
+   * encounter something that forces the class to be a enum, such as being used in a switch
+   * selector), but it can never go from true to false.
+   */
+  public void setIsAnEnumToTrue() {
+    this.isAnEnum = true;
+    if (extendsClause != null) {
+      throw new RuntimeException(
+          "trying to make a synthetic class that already has an extends clause into" + "an enum");
+    }
+  }
+
   /**
    * Sets isAnAnnotation to true. isAnAnnotation is monotonic: it can start as false and become true
    * (because we encounter evidence that this is an annotation), but it can never go from true to
@@ -302,6 +348,9 @@ public void implement(String interfaceName) {
    */
   public void extend(String className) {
     this.extendsClause = "extends " + className;
+    if (isAnEnum) {
+      throw new RuntimeException("enums cannot extend another class");
+    }
   }
 
   /**
@@ -505,6 +554,8 @@ public String toString() {
       sb.append("interface ");
     } else if (isAnAnnotation) {
       sb.append("@interface ");
+    } else if (isAnEnum) {
+      sb.append("enum ");
     } else {
       sb.append("class ");
     }
@@ -526,6 +577,17 @@ public String toString() {
       }
     }
     sb.append(" {\n");
+    if (isAnEnum) {
+      Iterator<String> constants = enumConstants.iterator();
+      while (constants.hasNext()) {
+        sb.append(constants.next());
+        if (constants.hasNext()) {
+          sb.append(",\n");
+        }
+      }
+      sb.append(";\n");
+    }
+
     if (innerClasses != null) {
       for (UnsolvedClassOrInterface innerClass : innerClasses) {
         sb.append(innerClass.toString());

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

@@ -43,6 +43,7 @@
 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.stmt.TryStmt;
 import com.github.javaparser.ast.stmt.WhileStmt;
 import com.github.javaparser.ast.type.ArrayType;
@@ -650,20 +651,87 @@ public Visitable visit(ForEachStmt node, Void p) {
     return result;
   }
 
+  /** The name of the enum type used as a switch selector, if one is currently in scope. */
+  private @Nullable String enumSwitchSelectorFQN = null;
+
+  /** True iff we are visiting a switch control structure (a label, guard, or selector). */
+  private boolean inSwitch = false;
+
   @Override
   public Visitable visit(SwitchExpr node, Void p) {
     HashSet<String> currentLocalVariables = new HashSet<>();
     localVariables.addFirst(currentLocalVariables);
+    // workaround JavaParser visit order bug: we should visit the
+    // selector expression first, but JavaParser for some reason
+    // visits the _entries_ (i.e., the expression in the cases) first!
+    node.getSelector().accept(this, p);
+    inSwitch = true;
+    try {
+      ResolvedType resolved = node.getSelector().calculateResolvedType();
+      enumSwitchSelectorFQN = resolved.describe();
+    } catch (UnsolvedSymbolException e) {
+      // We'll deal with this next time.
+      gotException();
+    }
     Visitable result = super.visit(node, p);
+    inSwitch = false;
     localVariables.removeFirst();
     return result;
   }
 
   @Override
-  public Visitable visit(SwitchEntry node, Void p) {
+  public Visitable visit(SwitchStmt node, Void p) {
     HashSet<String> currentLocalVariables = new HashSet<>();
     localVariables.addFirst(currentLocalVariables);
+    // workaround JavaParser visit order bug: we should visit the
+    // selector expression first, but JavaParser for some reason
+    // visits the _entries_ (i.e., the expression in the cases) first!
+    node.getSelector().accept(this, p);
+    inSwitch = true;
+    try {
+      ResolvedType resolved = node.getSelector().calculateResolvedType();
+      enumSwitchSelectorFQN = resolved.describe();
+    } catch (UnsolvedSymbolException e) {
+      // We'll deal with this next time.
+      gotException();
+    }
     Visitable result = super.visit(node, p);
+    inSwitch = false;
+    enumSwitchSelectorFQN = null;
+    localVariables.removeFirst();
+    return result;
+  }
+
+  @Override
+  public Visitable visit(SwitchEntry node, Void p) {
+    HashSet<String> currentLocalVariables = new HashSet<>();
+    localVariables.addFirst(currentLocalVariables);
+
+    // The following code is copied from super.visit(SwitchEntry, ...),
+    // because we need to differentiate between the expressions in the "labels"
+    // (which may be unqualified enum constants) and the "statements", which may not be.
+    SwitchEntry n = node;
+    Void arg = p;
+    Expression guard = n.getGuard().map(s -> (Expression) s.accept(this, arg)).orElse(null);
+    NodeList<Expression> labels = (NodeList<Expression>) n.getLabels().accept(this, arg);
+
+    // Here, we need to remove the special enum switch handling temporarily.
+    String oldEnumSwitchSelectorFQN = enumSwitchSelectorFQN;
+    enumSwitchSelectorFQN = null;
+    inSwitch = false;
+
+    NodeList<Statement> statements = (NodeList<Statement>) n.getStatements().accept(this, arg);
+    Comment comment = n.getComment().map(s -> (Comment) s.accept(this, arg)).orElse(null);
+    n.setGuard(guard);
+    n.setLabels(labels);
+    n.setStatements(statements);
+    n.setComment(comment);
+    Visitable result = n;
+
+    // and then restore it
+    enumSwitchSelectorFQN = oldEnumSwitchSelectorFQN;
+    inSwitch = true;
+
     localVariables.removeFirst();
     return result;
   }
@@ -990,7 +1058,9 @@ else if (staticImportedMembersMap.containsKey(name)) {
       if (parentNode.isEmpty()
           || !(parentNode.get() instanceof MethodCallExpr
               || parentNode.get() instanceof FieldAccessExpr)) {
-        if (!isALocalVar(name)) {
+        if (inSwitch && enumSwitchSelectorFQN != null) {
+          updateSyntheticEnumWithNewConstant(enumSwitchSelectorFQN, name);
+        } else if (!isALocalVar(name) && !inSwitch) {
           updateSyntheticClassForSuperCall(node);
         }
       }
@@ -2379,6 +2449,25 @@ public void updateSyntheticClassWithNonStaticFields(FieldAccessExpr field) {
     updateClassSetWithQualifiedFieldSignature(fieldQualifedSignature, false, false);
   }
 
+  /**
+   * Updates the synthetic enum with the given FQN by adding a new enum constant with the given
+   * name. This method is idempotent, and the enum may not yet exist (but if not, this will trigger
+   * another round of unsolved symbol visiting).
+   *
+   * @param enumFQN the fully-qualified name of a synthetic enum
+   * @param constantName the name of one of the enum constants of that enum
+   */
+  public void updateSyntheticEnumWithNewConstant(String enumFQN, String constantName) {
+    for (UnsolvedClassOrInterface synthEnum : missingClass) {
+      if (!synthEnum.getQualifiedClassName().equals(enumFQN)) {
+        continue;
+      }
+      synthEnum.setIsAnEnumToTrue();
+      synthEnum.addEnumConstant(constantName);
+      return;
+    }
+  }
+
   /**
    * For a super call, this method will update the corresponding synthetic class
    *
@@ -4032,8 +4121,8 @@ private void migrateType(String incorrectTypeName, String correctTypeName) {
   }
 
   /**
-   * Given the name of a class, this method will based on the map classAndItsParent to find the name
-   * of the super class of the input class
+   * Given the name of a class, this method look up the name in the map classAndItsParent to find
+   * the name of the super class of the input class. Otherwise, a RunTime exception is thrown.
    *
    * @param className the name of the class to be taken as the input
    * @return the name of the super class of the input class

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

@@ -0,0 +1,19 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.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.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 {
+    CONSTANT1, CONSTANT2, CONSTANT3, CONSTANT4
+}