Change the direct super type of Enums (#6127)

checker/src/main/java/org/checkerframework/checker/tainting/TaintingAnnotatedTypeFactory.java

@@ -0,0 +1,36 @@
+package org.checkerframework.checker.tainting;
+
+import java.util.Set;
+import javax.lang.model.element.AnnotationMirror;
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
+
+/** Annotated type factory for the Tainting Checker. */
+public class TaintingAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+  /** The {@code @}{@link Untainted} annotation mirror. */
+  private final AnnotationMirror UNTAINTED;
+
+  /** A singleton set containing the {@code @}{@link Untainted} annotation mirror. */
+  private final AnnotationMirrorSet setOfUntainted;
+
+  /**
+   * Creates a {@link TaintingAnnotatedTypeFactory}.
+   *
+   * @param checker the tainting checker
+   */
+  public TaintingAnnotatedTypeFactory(BaseTypeChecker checker) {
+    super(checker);
+    this.UNTAINTED = AnnotationBuilder.fromClass(getElementUtils(), Untainted.class);
+    this.setOfUntainted = AnnotationMirrorSet.singleton(UNTAINTED);
+    postInit();
+  }
+
+  @Override
+  protected Set<AnnotationMirror> getEnumConstructorQualifiers() {
+    return setOfUntainted;
+  }
+}

checker/tests/nullness/Issue2564.java

@@ -4,9 +4,9 @@
 
 public abstract class Issue2564 {
   public enum EnumType {
-    // :: error: (assignment)
+    // :: error: (enum.declaration)
     @KeyFor("myMap") MY_KEY,
-    // :: error: (assignment)
+    // :: error: (enum.declaration)
     @KeyFor("enumMap") ENUM_KEY;
     private static final Map<String, Integer> enumMap = new HashMap<>();
 

checker/tests/nullness/Issue2587.java

@@ -2,7 +2,7 @@
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.KeyFor;
 
-@SuppressWarnings("assignment") // These warnings are not relevant
+@SuppressWarnings({"enum.declaration", "assignment"}) // These warnings are not relevant
 public abstract class Issue2587 {
   public enum EnumType {
     // :: error: (expression.unparsable)

checker/tests/tainting/Issue6110.java

@@ -0,0 +1,22 @@
+import java.util.EnumSet;
+import org.checkerframework.checker.tainting.qual.Tainted;
+import org.checkerframework.checker.tainting.qual.Untainted;
+
+class Issue6110 {
+  enum TestEnum {
+    ONE,
+    @Untainted TWO
+  }
+
+  static void test(Enum<@Untainted TestEnum> o) {
+
+    @Tainted TestEnum e = TestEnum.ONE;
+    o.compareTo(TestEnum.ONE);
+    o.compareTo(TestEnum.TWO);
+
+    EnumSet<@Tainted TestEnum> s1 = EnumSet.of(TestEnum.ONE);
+    // :: error: (assignment)
+    EnumSet<@Untainted TestEnum> s2 = EnumSet.of(TestEnum.ONE);
+    EnumSet<@Untainted TestEnum> s3 = EnumSet.of(TestEnum.TWO);
+  }
+}

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

@@ -1533,8 +1533,11 @@ && getCurrentPath().getParentPath().getLeaf().getKind() == Tree.Kind.LAMBDA_EXPR
     }
 
     atypeFactory.getDependentTypesHelper().checkTypeForErrorExpressions(variableType, tree);
-    // If there's no assignment in this variable declaration, skip it.
-    if (tree.getInitializer() != null) {
+    Element varEle = TreeUtils.elementFromDeclaration(tree);
+    if (varEle.getKind() == ElementKind.ENUM_CONSTANT) {
+      commonAssignmentCheck(tree, tree.getInitializer(), "enum.declaration");
+    } else if (tree.getInitializer() != null) {
+      // If there's no assignment in this variable declaration, skip it.
       commonAssignmentCheck(tree, tree.getInitializer(), "assignment");
     } else {
       // commonAssignmentCheck validates the type of `tree`,

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

@@ -4,6 +4,7 @@ type.anno.before.modifier=write type annotation %s immediately before type, afte
 type.anno.before.decl.anno=write type annotations %s immediately before type, after declaration annotation %s
 
 array.initializer=incompatible types in array initializer.%nfound   : %s%nrequired: %s
+enum.declaration=incompatible annotations on Enum constant declaration.%nfound   : %s%nrequired: %s
 assignment=incompatible types in assignment.%nfound   : %s%nrequired: %s
 compound.assignment=expression type incompatible with left-hand side in compound assignment.%nfound   : %s%nrequired: %s
 unary.increment=increment result incompatible with variable declared type.%nfound   : %s%nrequired: %s

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

@@ -2772,9 +2772,23 @@ public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
       // Reset the enclosing type because it can be substituted incorrectly.
       ((AnnotatedDeclaredType) con.getReturnType()).setEnclosingType(enclosingType);
     }
+    if (ctor.getEnclosingElement().getKind() == ElementKind.ENUM) {
+      Set<AnnotationMirror> enumAnnos = getEnumConstructorQualifiers();
+      con.getReturnType().replaceAnnotations(enumAnnos);
+    }
     return new ParameterizedExecutableType(con, typeargs);
   }
 
+  /**
+   * Returns the annotations that should be applied to enum constructors. This implementation
+   * returns an empty set. Subclasses can override to return a different set.
+   *
+   * @return the annotations that should be applied to enum constructors
+   */
+  protected Set<AnnotationMirror> getEnumConstructorQualifiers() {
+    return Collections.emptySet();
+  }
+
   /**
    * Creates an AnnotatedDeclaredType for a NewClassTree. Only adds explicit annotations, unless
    * newClassTree has a diamond operator. In that case, the annotations on the type arguments are

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

@@ -384,12 +384,7 @@ private AnnotatedDeclaredType createEnumSuperType(
       for (AnnotatedTypeMirror t : adt.getTypeArguments()) {
         // If the type argument of super is the same as the input type
         if (atypeFactory.types.isSameType(t.getUnderlyingType(), type.getUnderlyingType())) {
-          AnnotationMirrorSet bounds =
-              ((AnnotatedDeclaredType) atypeFactory.getAnnotatedType(dt.asElement()))
-                  .typeArgs
-                  .get(0)
-                  .getEffectiveAnnotations();
-          t.addAnnotations(bounds);
+          t.addAnnotations(type.primaryAnnotations);
         }
       }
       adt.addAnnotations(type.getPrimaryAnnotations());

framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java

@@ -129,7 +129,6 @@ public static <T extends AnnotatedTypeMirror> T asSuper(
   public static <T extends AnnotatedTypeMirror> T castedAsSuper(
       AnnotatedTypeFactory atypeFactory, AnnotatedTypeMirror subtype, T supertype) {
     Types types = atypeFactory.getProcessingEnv().getTypeUtils();
-    Elements elements = atypeFactory.getProcessingEnv().getElementUtils();
 
     if (subtype.getKind() == TypeKind.NULL) {
       // Make a copy of the supertype so that if supertype is a composite type, the
@@ -144,38 +143,6 @@ public static <T extends AnnotatedTypeMirror> T castedAsSuper(
     T asSuperType = AnnotatedTypes.asSuper(atypeFactory, subtype, supertype);
 
     fixUpRawTypes(subtype, asSuperType, supertype, types);
-
-    // if we have a type for enum MyEnum {...}
-    // When the supertype is the declaration of java.lang.Enum<E>, MyEnum values become
-    // Enum<MyEnum>.  Where really, we would like an Enum<E> with the annotations from
-    // Enum<MyEnum> are transferred to Enum<E>.  That is, if we have a type:
-    // @1 Enum<@2 MyEnum>
-    // asSuper should return:
-    // @1 Enum<E extends @2 Enum<E>>
-    if (asSuperType != null
-        && AnnotatedTypes.isEnum(asSuperType)
-        && AnnotatedTypes.isDeclarationOfJavaLangEnum(types, elements, supertype)) {
-      AnnotatedDeclaredType resultAtd = ((AnnotatedDeclaredType) supertype).deepCopy();
-      resultAtd.clearPrimaryAnnotations();
-      resultAtd.addAnnotations(asSuperType.getPrimaryAnnotations());
-
-      AnnotatedDeclaredType asSuperAdt = (AnnotatedDeclaredType) asSuperType;
-      if (!resultAtd.getTypeArguments().isEmpty() && !asSuperAdt.getTypeArguments().isEmpty()) {
-        AnnotatedTypeMirror sourceTypeArg = asSuperAdt.getTypeArguments().get(0);
-        AnnotatedTypeMirror resultTypeArg = resultAtd.getTypeArguments().get(0);
-        resultTypeArg.clearPrimaryAnnotations();
-        if (resultTypeArg.getKind() == TypeKind.TYPEVAR) {
-          // Only change the upper bound of a type variable.
-          AnnotatedTypeVariable resultTypeArgTV = (AnnotatedTypeVariable) resultTypeArg;
-          resultTypeArgTV.getUpperBound().addAnnotations(sourceTypeArg.getPrimaryAnnotations());
-        } else {
-          resultTypeArg.addAnnotations(sourceTypeArg.getEffectiveAnnotations());
-        }
-        @SuppressWarnings("unchecked")
-        T result = (T) resultAtd;
-        return result;
-      }
-    }
     return asSuperType;
   }