Batch renaming&removal of updated API

src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java

@@ -20,15 +20,15 @@
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
-import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
 import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.TreeUtils;
-import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator;
 import pico.typecheck.PICOTypeUtil;
 
 import javax.lang.model.element.AnnotationMirror;
@@ -62,17 +62,17 @@ public PICOInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, bool
     // be inserted results anyway).
     @Override
     public TreeAnnotator createTreeAnnotator() {
-        return new ListTreeAnnotator(new ImplicitsTreeAnnotator(this),
+        return new ListTreeAnnotator(new LiteralTreeAnnotator(this),
                 new PICOInferencePropagationTreeAnnotator(this),
                 new InferenceTreeAnnotator(this, realChecker, realTypeFactory, variableAnnotator, slotManager));
     }
 
     @Override
     protected TypeAnnotator createTypeAnnotator() {
-        // Reuse PICOImplicitsTypeAnnotator even in inference mode. Because the type annotator's implementation
+        // Reuse PICODefaultForTypeAnnotator even in inference mode. Because the type annotator's implementation
         // are the same. The only drawback is that naming is not good(doesn't include "Inference"), thus may be
         // hard to debug
-        return new ListTypeAnnotator(super.createTypeAnnotator(), new PICOImplicitsTypeAnnotator(this));
+        return new ListTypeAnnotator(super.createTypeAnnotator(), new PICODefaultForTypeAnnotator(this));
     }
 
     @Override
@@ -235,7 +235,7 @@ public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
             return super.visitTypeCast(node, type);
         }
 
-        /**Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are not guaranteed
+        /**Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are not guaranteed
          to always have immutable annotation. If this happens, we manually add immutable to type. */
         private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) {
             if (PICOTypeUtil.isImplicitlyImmutableType(type)) {

src/main/java/pico/inference/PICOInferenceRealTypeFactory.java

@@ -11,16 +11,15 @@
 import java.util.List;
 import java.util.Set;
 
-import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.RelevantJavaTypes;
 import org.checkerframework.framework.type.AbstractViewpointAdapter;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
-import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
@@ -31,7 +30,8 @@
 
 import com.sun.source.tree.Tree;
 
-import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOTreeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator;
@@ -82,7 +82,7 @@ protected AbstractViewpointAdapter createViewpointAdapter() {
     protected TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(
                 new PICOPropagationTreeAnnotator(this),
-                new ImplicitsTreeAnnotator(this),
+                new LiteralTreeAnnotator(this),
                 new PICOTreeAnnotator(this));
     }
 
@@ -107,7 +107,7 @@ protected TypeAnnotator createTypeAnnotator() {
         // method, so if one annotator already applied the annotations, the others won't apply twice at the
         // same location
         typeAnnotators.add(new PICOTypeAnnotator(this));
-        typeAnnotators.add(new PICOImplicitsTypeAnnotator(this));
+        typeAnnotators.add(new PICODefaultForTypeAnnotator(this));
         return new ListTypeAnnotator(typeAnnotators);
     }
 
@@ -125,21 +125,6 @@ public boolean getShouldDefaultTypeVarLocals() {
         return false;
     }
 
-    // Copied from PICOAnnotatedTypeFactory
-    @Override
-    protected void annotateInheritedFromClass(AnnotatedTypeMirror type, Set<AnnotationMirror> fromClass) {
-        // If interitted from class element is @Mutable or @Immutable, then apply this annotation to the usage type
-        if (fromClass.contains(MUTABLE) || fromClass.contains(IMMUTABLE)) {
-            super.annotateInheritedFromClass(type, fromClass);
-            return;
-        }
-        // If interitted from class element is @ReceiverDependantMutable, then don't apply and wait for @Mutable
-        // (default qualifier in hierarchy to be applied to the usage type). This is to avoid having @ReceiverDependantMutable
-        // on type usages as a default behaviour. By default, @Mutable is better used as the type for usages that
-        // don't have explicit annotation.
-        return;// Don't add annotations from class element
-    }
-
     @Override
     public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) {
         PICOTypeUtil.addDefaultForField(this, type, elt);

src/main/java/pico/inference/PICOInferenceVisitor.java

@@ -541,7 +541,7 @@ private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, An
      * 2) In constructor
      * 3) In instance method, declared receiver is @UnderInitialized
      *
-     * @param node assignment tree that might be initializing an object
+     * @param variable assignment tree that might be initializing an object
      * @return true if the assignment tree is initializing an object
      *
      * @see #hasUnderInitializationDeclaredReceiver(MethodTree)
@@ -559,7 +559,7 @@ private boolean isInitializingObject(ExpressionTree variable) {
         }
 
         MethodTree enclosingMethod = TreeUtils.enclosingMethod(treePath);
-        // No possibility of initialiazing object if the assignment is not within constructor or method(both MethodTree)
+        // No possibility of initializing object if the assignment is not within constructor or method(both MethodTree)
         if (enclosingMethod == null) return false;
         // At this point, we already know that this assignment is field assignment within a method
         if (TreeUtils.isConstructor(enclosingMethod) || hasUnderInitializationDeclaredReceiver(enclosingMethod)) {
@@ -627,7 +627,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
         // Only check invocability if it's super call, as non-super call is already checked
         // by super implementation(of course in both cases, invocability is not checked when
         // invoking static methods)
-        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperCall(node)) {
+        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperConstructorCall(node)) {
             checkMethodInvocability(invokedMethod, node);
         }
         return null;

src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java

@@ -34,11 +34,11 @@
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.type.ViewpointAdapter;
-import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
-import org.checkerframework.framework.type.typeannotator.ImplicitsTypeAnnotator;
+import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.PropagationTypeAnnotator;
@@ -82,7 +82,7 @@ public class PICOAnnotatedTypeFactory extends InitializationAnnotatedTypeFactory
         PICOStore, PICOTransfer, PICOAnalysis> {
 
     public PICOAnnotatedTypeFactory(BaseTypeChecker checker) {
-        super(checker, true);
+        super(checker);
         postInit();
         addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY);
     }
@@ -114,7 +114,7 @@ protected ViewpointAdapter createViewpointAdapter() {
     protected TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(
                 new PICOPropagationTreeAnnotator(this),
-                new ImplicitsTreeAnnotator(this),
+                new LiteralTreeAnnotator(this),
                 new CommitmentTreeAnnotator(this),
                 new PICOTreeAnnotator(this));
     }
@@ -140,7 +140,7 @@ protected TypeAnnotator createTypeAnnotator() {
         // method, so if one annotator already applied the annotations, the others won't apply twice at the
         // same location
         typeAnnotators.add(new PICOTypeAnnotator(this));
-        typeAnnotators.add(new PICOImplicitsTypeAnnotator(this));
+        typeAnnotators.add(new PICODefaultForTypeAnnotator(this));
         typeAnnotators.add(new CommitmentTypeAnnotator(this));
         return new ListTypeAnnotator(typeAnnotators);
     }
@@ -185,20 +185,6 @@ public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) {
         super.addComputedTypeAnnotations(elt, type);
     }
 
-    @Override
-    protected void annotateInheritedFromClass(AnnotatedTypeMirror type, Set<AnnotationMirror> fromClass) {
-        // If interitted from class element is @Mutable or @Immutable, then apply this annotation to the usage type
-        if (fromClass.contains(MUTABLE) || fromClass.contains(IMMUTABLE)) {
-            super.annotateInheritedFromClass(type, fromClass);
-            return;
-        }
-        // If interitted from class element is @ReceiverDependantMutable, then don't apply and wait for @Mutable
-        // (default qualifier in hierarchy to be applied to the usage type). This is to avoid having @ReceiverDependantMutable
-        // on type usages as a default behaviour. By default, @Mutable is better used as the type for usages that
-        // don't have explicit annotation.
-        return;// Don't add annotations from class element
-    }
-
     /**This method gets lhs WITH flow sensitive refinement*/
     // TODO Should refactor super class to avoid too much duplicate code.
     // This method is pretty hacky right now.
@@ -391,7 +377,7 @@ public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
             return super.visitTypeCast(node, type);
         }
 
-        /**Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are not guaranteed
+        /**Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are not guaranteed
          to always have immutable annotation. If this happens, we manually add immutable to type. We use
          addMissingAnnotations because we want to respect existing annotation on type*/
         private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) {
@@ -488,9 +474,9 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) {
 
     }
 
-    public static class PICOImplicitsTypeAnnotator extends ImplicitsTypeAnnotator {
+    public static class PICODefaultForTypeAnnotator extends DefaultForTypeAnnotator {
 
-        public PICOImplicitsTypeAnnotator(AnnotatedTypeFactory typeFactory) {
+        public PICODefaultForTypeAnnotator(AnnotatedTypeFactory typeFactory) {
             super(typeFactory);
         }
 
@@ -520,7 +506,7 @@ protected Void scan(AnnotatedTypeMirror type, Void p) {
     // TODO Right now, instance method receiver cannot inherit bound annotation from class element, and
     // this caused the inconsistency when accessing the type of receiver while visiting the method and
     // while visiting the variable tree. Implicit annotation can be inserted to method receiver via
-    // extending ImplicitsTypeAnnotator; But InheritedFromClassAnnotator cannot be inheritted because its
+    // extending DefaultForTypeAnnotator; But InheritedFromClassAnnotator cannot be inheritted because its
     // constructor is private and I can't override it to also inherit bound annotation from class element
     // to the declared receiver type of instance methods. To view the details, look at ImmutableClass1.java
     // testcase.

src/main/java/pico/typecheck/PICOChecker.java

@@ -14,7 +14,7 @@
 public class PICOChecker extends InitializationChecker {
 
     public PICOChecker() {
-        super(true);
+        super();
     }
 
     @Override

src/main/java/pico/typecheck/PICOTypeUtil.java

@@ -14,7 +14,7 @@
 import com.sun.source.tree.UnaryTree;
 import com.sun.source.tree.VariableTree;
 import com.sun.source.util.TreePath;
-import org.checkerframework.framework.qual.ImplicitFor;
+import org.checkerframework.framework.qual.DefaultFor;
 import org.checkerframework.framework.qual.TypeKind;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -64,36 +64,36 @@ public class PICOTypeUtil {
         sideEffectingUnaryOperators.add(Tree.Kind.PREFIX_DECREMENT);
     }
 
-    private static boolean isInTypesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) {
-        ImplicitFor implicitFor = Immutable.class.getAnnotation(ImplicitFor.class);
-        assert implicitFor != null;
-        assert implicitFor.types() != null;
-        for (TypeKind typeKind : implicitFor.types()) {
+    private static boolean isInTypeKindsOfDefaultForOfImmutable(AnnotatedTypeMirror atm) {
+        DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class);
+        assert defaultFor != null;
+        for (TypeKind typeKind : defaultFor.typeKinds()) {
             if (typeKind.name() == atm.getKind().name()) return true;
         }
         return false;
     }
 
-    private static boolean isInTypeNamesOfImplicitForOfImmutable(AnnotatedTypeMirror atm) {
+    private static boolean isInTypesOfDefaultForOfImmutable(AnnotatedTypeMirror atm) {
         if (atm.getKind().name() != TypeKind.DECLARED.name()) {
             return false;
         }
-        ImplicitFor implicitFor = Immutable.class.getAnnotation(ImplicitFor.class);
-        assert implicitFor != null;
-        assert implicitFor.typeNames() != null;
-        Class<?>[] typeNames = implicitFor.typeNames();
+        DefaultFor defaultFor = Immutable.class.getAnnotation(DefaultFor.class);
+        assert defaultFor != null;
+        Class<?>[] types = defaultFor.types();
         String fqn = TypesUtils.getQualifiedName((DeclaredType) atm.getUnderlyingType()).toString();
-        for (int i = 0; i < typeNames.length; i++) {
-            if (typeNames[i].getCanonicalName().toString().contentEquals(fqn)) return true;
+        for (Class<?> type : types) {
+            if (type.getCanonicalName().contentEquals(fqn)) {
+                return true;
+            }
         }
         return false;
     }
 
     /**Method to determine if the underlying type is implicitly immutable. This method is consistent
      * with the types and typeNames that are in @ImplicitFor in the definition of @Immutable qualifier*/
     public static boolean isImplicitlyImmutableType(AnnotatedTypeMirror atm) {
-        return isInTypesOfImplicitForOfImmutable(atm)
-                || isInTypeNamesOfImplicitForOfImmutable(atm)
+        return isInTypeKindsOfDefaultForOfImmutable(atm)
+                || isInTypesOfDefaultForOfImmutable(atm)
                 || isEnumOrEnumConstant(atm);
     }
 

src/main/java/pico/typecheck/PICOVisitor.java

@@ -389,7 +389,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
         // Only check invocability if it's super call, as non-super call is already checked
         // by super implementation(of course in both cases, invocability is not checked when
         // invoking static methods)
-        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperCall(node)) {
+        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperConstructorCall(node)) {
             checkMethodInvocability(invokedMethod, node);
         }
         return null;

src/main/java/qual/Bottom.java

@@ -1,22 +1,17 @@
 package qual;
 
 import org.checkerframework.framework.qual.DefaultFor;
-import org.checkerframework.framework.qual.DefaultInUncheckedCodeFor;
-import org.checkerframework.framework.qual.ImplicitFor;
-import org.checkerframework.framework.qual.LiteralKind;
 import org.checkerframework.framework.qual.SubtypeOf;
 import org.checkerframework.framework.qual.TargetLocations;
 import org.checkerframework.framework.qual.TypeUseLocation;
 
 import java.lang.annotation.Documented;
-import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
 @SubtypeOf({Mutable.class, Immutable.class, PolyMutable.class, ReceiverDependantMutable.class})
 @DefaultFor({ TypeUseLocation.LOWER_BOUND })
-@ImplicitFor(literals = {LiteralKind.NULL})
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 // Stop allowing any explicit usage of @Bottom qualifier in source. As it causes difficulty to
@@ -26,5 +21,4 @@
 // qualifier than @Bottom explicitly on explicit lower bound to have different-than-default type.
 @Target({})
 @TargetLocations({})
-@DefaultInUncheckedCodeFor({TypeUseLocation.RETURN})
 public @interface Bottom {}

src/main/java/qual/Immutable.java

@@ -1,6 +1,7 @@
 package qual;
 
-import org.checkerframework.framework.qual.ImplicitFor;
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.QualifierForLiterals;
 import org.checkerframework.framework.qual.LiteralKind;
 import org.checkerframework.framework.qual.SubtypeOf;
 
@@ -17,10 +18,10 @@
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
-@ImplicitFor(typeNames={Enum.class, String.class, Double.class, Boolean.class, Byte.class,
+@DefaultFor(types={Enum.class, String.class, Double.class, Boolean.class, Byte.class,
         Character.class, Float.class, Integer.class, Long.class, Short.class, Number.class,
         BigDecimal.class, BigInteger.class},
-        literals = { LiteralKind.PRIMITIVE, LiteralKind.STRING},
-        types = { TypeKind.INT, TypeKind.BYTE, TypeKind.SHORT, TypeKind.BOOLEAN,
+        typeKinds = { TypeKind.INT, TypeKind.BYTE, TypeKind.SHORT, TypeKind.BOOLEAN,
                 TypeKind.LONG, TypeKind.CHAR, TypeKind.FLOAT, TypeKind.DOUBLE })
+@QualifierForLiterals({ LiteralKind.PRIMITIVE, LiteralKind.STRING})
 public @interface Immutable {}

src/main/java/qual/Readonly.java

@@ -1,7 +1,6 @@
 package qual;
 
 import org.checkerframework.framework.qual.DefaultInUncheckedCodeFor;
-import org.checkerframework.framework.qual.ImplicitFor;
 import org.checkerframework.framework.qual.SubtypeOf;
 import org.checkerframework.framework.qual.TypeUseLocation;