Remove implicit bottom checks

src/main/java/universe/UniverseAnnotatedTypeFactory.java

@@ -2,22 +2,18 @@
 
 import checkers.inference.BaseInferenceRealTypeFactory;
 
-import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.IdentifierTree;
 import com.sun.source.tree.MethodTree;
 import com.sun.source.tree.Tree;
-import com.sun.source.tree.TypeCastTree;
 
 import org.checkerframework.common.basetype.BaseTypeChecker;
-import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
 import org.checkerframework.framework.type.ViewpointAdapter;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
-import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator;
 import org.checkerframework.javacutil.TreeUtils;
 
 import universe.qual.Any;
@@ -71,7 +67,7 @@ protected ViewpointAdapter createViewpointAdapter() {
     @Override
     protected TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(
-                new UniversePropagationTreeAnnotator(this),
+                new PropagationTreeAnnotator(this),
                 new LiteralTreeAnnotator(this),
                 new UniverseTreeAnnotator());
     }
@@ -137,50 +133,4 @@ public Void visitMethod(MethodTree node, AnnotatedTypeMirror p) {
             return super.visitMethod(node, p);
         }
     }
-
-    private static class UniversePropagationTreeAnnotator extends PropagationTreeAnnotator {
-        /**
-         * Creates a {@link DefaultForTypeAnnotator} from the given checker, using that checker's
-         * type hierarchy.
-         *
-         * @param atypeFactory type factory to use
-         */
-        public UniversePropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) {
-            super(atypeFactory);
-        }
-
-        /**
-         * Add immutable to the result type of a binary operation if the result type is implicitly
-         * immutable
-         */
-        @Override
-        public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
-            applyImmutableIfImplicitlyBottom(
-                    type); // Usually there isn't existing annotation on binary trees, but to be
-            // safe, run it first
-            super.visitBinary(node, type);
-            return null;
-        }
-
-        /** Add immutable to the result type of a cast if the result type is implicitly immutable */
-        @Override
-        public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
-            applyImmutableIfImplicitlyBottom(
-                    type); // Must run before calling super method to respect existing annotation
-            return super.visitTypeCast(node, type);
-        }
-
-        /**
-         * 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 applyImmutableIfImplicitlyBottom(AnnotatedTypeMirror type) {
-            if (UniverseTypeUtil.isImplicitlyBottomType(type)) {
-                type.addMissingAnnotations(
-                        new HashSet<>(Arrays.asList(UniverseAnnotationMirrorHolder.BOTTOM)));
-            }
-        }
-    }
 }

src/main/java/universe/UniverseInferenceAnnotatedTypeFactory.java

@@ -1,7 +1,6 @@
 package universe;
 
 import static universe.UniverseAnnotationMirrorHolder.ANY;
-import static universe.UniverseAnnotationMirrorHolder.BOTTOM;
 import static universe.UniverseAnnotationMirrorHolder.PEER;
 import static universe.UniverseAnnotationMirrorHolder.REP;
 import static universe.UniverseAnnotationMirrorHolder.SELF;
@@ -18,7 +17,6 @@
 
 import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.Tree;
-import com.sun.source.tree.TypeCastTree;
 
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
@@ -58,7 +56,7 @@ public UniverseInferenceAnnotatedTypeFactory(
     public TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(
                 new LiteralTreeAnnotator(this),
-                new UniverseInferencePropagationTreeAnnotater(this),
+                new PropagationTreeAnnotator(this),
                 new InferenceTreeAnnotator(
                         this, realChecker, realTypeFactory, variableAnnotator, slotManager));
     }
@@ -117,45 +115,6 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) {
         }
     }
 
-    private static class UniverseInferencePropagationTreeAnnotater
-            extends PropagationTreeAnnotator {
-        public UniverseInferencePropagationTreeAnnotater(AnnotatedTypeFactory atypeFactory) {
-            super(atypeFactory);
-        }
-
-        @Override
-        public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
-            applyBottomIfImplicitlyBottom(
-                    type); // Usually there isn't existing annotation on binary trees, but to be
-            // safe, run it first
-            return super.visitBinary(node, type);
-        }
-
-        @Override
-        public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
-            applyBottomIfImplicitlyBottom(
-                    type); // Must run before calling super method to respect existing annotation
-            if (type.isAnnotatedInHierarchy(ANY)) {
-                // VarAnnot is guarenteed to not exist on type, because PropagationTreeAnnotator has
-                // the highest previledge
-                // So VarAnnot hasn't been inserted to cast type yet.
-                UniverseTypeUtil.applyConstant(type, type.getAnnotationInHierarchy(ANY));
-            }
-            return super.visitTypeCast(node, type);
-        }
-
-        /**
-         * Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are
-         * not guaranteed to always have immutable annotation. If this happens, we manually add
-         * immutable to type.
-         */
-        private void applyBottomIfImplicitlyBottom(AnnotatedTypeMirror type) {
-            if (UniverseTypeUtil.isImplicitlyBottomType(type)) {
-                UniverseTypeUtil.applyConstant(type, BOTTOM);
-            }
-        }
-    }
-
     public static class UniverseInferenceViewpointAdapter extends InferenceViewpointAdapter {
 
         public UniverseInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) {

src/main/java/universe/UniverseInferenceValidator.java

@@ -1,6 +1,5 @@
 package universe;
 
-import static universe.UniverseAnnotationMirrorHolder.BOTTOM;
 import static universe.UniverseAnnotationMirrorHolder.LOST;
 import static universe.UniverseAnnotationMirrorHolder.REP;
 
@@ -39,9 +38,6 @@ public UniverseInferenceValidator(
      */
     @Override
     public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) {
-        if (checkTopLevelDeclaredOrPrimitiveType) {
-            checkImplicitlyBottomTypeError(type, p);
-        }
         checkStaticRepError(type, p);
         // @Peer is allowed in static context
 
@@ -79,25 +75,10 @@ public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) {
         return super.visitArray(type, tree);
     }
 
-    @Override
-    public Void visitPrimitive(AnnotatedTypeMirror.AnnotatedPrimitiveType type, Tree tree) {
-        if (checkTopLevelDeclaredOrPrimitiveType) {
-            checkImplicitlyBottomTypeError(type, tree);
-        }
-        return super.visitPrimitive(type, tree);
-    }
-
     private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) {
         if (UniverseTypeUtil.inStaticScope(visitor.getCurrentPath())) {
             ((UniverseInferenceVisitor) visitor)
                     .doesNotContain(type, REP, "uts.static.rep.forbidden", tree);
         }
     }
-
-    private void checkImplicitlyBottomTypeError(AnnotatedTypeMirror type, Tree tree) {
-        if (UniverseTypeUtil.isImplicitlyBottomType(type)) {
-            ((UniverseInferenceVisitor) visitor)
-                    .effectiveIs(type, BOTTOM, "type.invalid.annotations.on.use", tree);
-        }
-    }
 }

src/main/java/universe/UniverseInferenceVisitor.java

@@ -66,12 +66,6 @@ protected UniverseInferenceValidator createTypeValidator() {
         return new UniverseInferenceValidator(checker, this, atypeFactory);
     }
 
-    @Override
-    public boolean isValidUse(
-            AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) {
-        return true;
-    }
-
     /**
      * Ignore constructor receiver annotations as result type of the constructor is always SELF for
      * universe.

src/main/java/universe/UniverseTypeValidator.java

@@ -1,6 +1,5 @@
 package universe;
 
-import static universe.UniverseAnnotationMirrorHolder.BOTTOM;
 import static universe.UniverseAnnotationMirrorHolder.LOST;
 import static universe.UniverseAnnotationMirrorHolder.REP;
 
@@ -36,9 +35,6 @@ public UniverseTypeValidator(
      */
     @Override
     public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) {
-        if (checkTopLevelDeclaredOrPrimitiveType) {
-            checkImplicitlyBottomTypeError(type, p);
-        }
         checkStaticRepError(type, p);
         // @Peer is allowed in static context
 
@@ -77,14 +73,6 @@ public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) {
         return super.visitArray(type, tree);
     }
 
-    @Override
-    public Void visitPrimitive(AnnotatedTypeMirror.AnnotatedPrimitiveType type, Tree tree) {
-        if (checkTopLevelDeclaredOrPrimitiveType) {
-            checkImplicitlyBottomTypeError(type, tree);
-        }
-        return super.visitPrimitive(type, tree);
-    }
-
     private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) {
         if (UniverseTypeUtil.inStaticScope(visitor.getCurrentPath())) {
             if (AnnotatedTypes.containsModifier(type, REP)) {
@@ -93,12 +81,4 @@ private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) {
             }
         }
     }
-
-    private void checkImplicitlyBottomTypeError(AnnotatedTypeMirror type, Tree tree) {
-        if (UniverseTypeUtil.isImplicitlyBottomType(type)) {
-            if (!type.hasAnnotation(BOTTOM)) {
-                reportInvalidAnnotationsOnUse(type, tree);
-            }
-        }
-    }
 }

src/main/java/universe/UniverseVisitor.java

@@ -53,12 +53,6 @@ protected UniverseTypeValidator createTypeValidator() {
         return new UniverseTypeValidator(checker, this, atypeFactory);
     }
 
-    @Override
-    public boolean isValidUse(
-            AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) {
-        return true;
-    }
-
     /** Ignore method receiver annotations. */
     @Override
     protected void checkMethodInvocability(

src/main/java/universe/qual/Bottom.java

@@ -7,6 +7,7 @@
 import org.checkerframework.framework.qual.TargetLocations;
 import org.checkerframework.framework.qual.TypeKind;
 import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UpperBoundFor;
 
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
@@ -25,6 +26,28 @@
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND})
 @SubtypeOf({Self.class, Rep.class})
 @QualifierForLiterals({LiteralKind.ALL})
+@UpperBoundFor(
+        typeKinds = {
+            TypeKind.INT,
+            TypeKind.BYTE,
+            TypeKind.SHORT,
+            TypeKind.BOOLEAN,
+            TypeKind.LONG,
+            TypeKind.CHAR,
+            TypeKind.FLOAT,
+            TypeKind.DOUBLE
+        },
+        types = {
+            String.class,
+            Double.class,
+            Boolean.class,
+            Byte.class,
+            Character.class,
+            Float.class,
+            Integer.class,
+            Long.class,
+            Short.class
+        })
 @DefaultFor(
         value = {TypeUseLocation.LOWER_BOUND},
         typeKinds = {

tests/inference/InvalidString.java

@@ -2,7 +2,8 @@
 
 public class InvalidString {
     void foo() {
-        throwException("" + Arrays.asList("", ""));
+        throwException("" + Arrays.asList("", "") + "");
+        throwException(3 + "");
     }
 
     void throwException(String s) {}