Add lost qualifier to viewpointtest type checker

framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java

@@ -3,13 +3,15 @@
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.type.AbstractViewpointAdapter;
+import org.checkerframework.framework.type.QualifierHierarchy;
 
 import java.lang.annotation.Annotation;
 import java.util.Set;
 
 import viewpointtest.quals.A;
 import viewpointtest.quals.B;
 import viewpointtest.quals.Bottom;
+import viewpointtest.quals.Lost;
 import viewpointtest.quals.PolyVP;
 import viewpointtest.quals.ReceiverDependentQual;
 import viewpointtest.quals.Top;
@@ -29,11 +31,18 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
                 Bottom.class,
                 PolyVP.class,
                 ReceiverDependentQual.class,
+                Lost.class,
                 Top.class);
     }
 
     @Override
     protected AbstractViewpointAdapter createViewpointAdapter() {
         return new ViewpointTestViewpointAdapter(this);
     }
+
+    @Override
+    public QualifierHierarchy createQualifierHierarchy() {
+        return new ViewpointTestQualifierHierarchy(
+                this.getSupportedTypeQualifiers(), elements, this);
+    }
 }

framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java

@@ -0,0 +1,40 @@
+package viewpointtest;
+
+import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
+import org.checkerframework.framework.type.NoElementQualifierHierarchy;
+
+import java.lang.annotation.Annotation;
+import java.util.Collection;
+
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.util.Elements;
+
+import viewpointtest.quals.Bottom;
+import viewpointtest.quals.Lost;
+
+/** A qualifier hierarchy for the ViewpointTest checker. */
+public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy {
+    /**
+     * Creates a ViewpointTestQualifierHierarchy from the given classes.
+     *
+     * @param qualifierClasses classes of annotations that are the qualifiers
+     * @param elements element utils
+     * @param atypeFactory the associated type factory
+     */
+    public ViewpointTestQualifierHierarchy(
+            Collection<Class<? extends Annotation>> qualifierClasses,
+            Elements elements,
+            GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory) {
+        super(qualifierClasses, elements, atypeFactory);
+    }
+
+    @Override
+    public boolean isSubtypeQualifiers(AnnotationMirror subAnno, AnnotationMirror superAnno) {
+        // Lost is not reflexive and the only subtype is Bottom
+        if (atypeFactory.areSameByClass(superAnno, Lost.class)
+                && !atypeFactory.areSameByClass(subAnno, Bottom.class)) {
+            return false;
+        }
+        return super.isSubtypeQualifiers(subAnno, superAnno);
+    }
+}

framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java

@@ -8,12 +8,13 @@
 
 import javax.lang.model.element.AnnotationMirror;
 
+import viewpointtest.quals.Lost;
 import viewpointtest.quals.ReceiverDependentQual;
 import viewpointtest.quals.Top;
 
 public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter {
 
-    private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL;
+    private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, LOST;
 
     /**
      * The class constructor.
@@ -26,6 +27,7 @@ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) {
         RECEIVERDEPENDENTQUAL =
                 AnnotationBuilder.fromClass(
                         atypeFactory.getElementUtils(), ReceiverDependentQual.class);
+        LOST = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Lost.class);
     }
 
     @Override
@@ -38,7 +40,11 @@ protected AnnotationMirror combineAnnotationWithAnnotation(
             AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) {
 
         if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDENTQUAL)) {
-            return receiverAnnotation;
+            if (AnnotationUtils.areSame(receiverAnnotation, TOP)) {
+                return LOST;
+            } else {
+                return receiverAnnotation;
+            }
         }
         return declaredAnnotation;
     }

framework/src/test/java/viewpointtest/quals/Bottom.java

@@ -13,6 +13,6 @@
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
-@SubtypeOf({A.class, B.class, ReceiverDependentQual.class})
+@SubtypeOf({A.class, B.class, ReceiverDependentQual.class, Top.class, PolyVP.class, Lost.class})
 @DefaultFor(TypeUseLocation.LOWER_BOUND)
 public @interface Bottom {}

framework/src/test/java/viewpointtest/quals/Lost.java

@@ -0,0 +1,15 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({Top.class})
+public @interface Lost {}

framework/tests/viewpointtest/LostNonReflexive.java

@@ -0,0 +1,37 @@
+import viewpointtest.quals.*;
+
+public class LostNonReflexive {
+    @ReceiverDependentQual Object f;
+
+    @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
+    @ReceiverDependentQual
+    LostNonReflexive(@ReceiverDependentQual Object args) {}
+
+    @ReceiverDependentQual
+    Object get() {
+        return null;
+    }
+
+    void set(@ReceiverDependentQual Object o) {}
+
+    void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) {
+        // :: error: (assignment.type.incompatible)
+        this.f = obj.f;
+        this.f = bottomObj;
+
+        // :: error: (assignment.type.incompatible)
+        @A Object aObj = obj.get();
+        // :: error: (assignment.type.incompatible)
+        @B Object bObj = obj.get();
+        // :: error: (assignment.type.incompatible)
+        @Bottom Object botObj = obj.get();
+
+        // :: error: (argument.type.incompatible)
+        new LostNonReflexive(obj.f);
+        new LostNonReflexive(bottomObj);
+
+        // :: error: (argument.type.incompatible)
+        this.set(obj.f);
+        this.set(bottomObj);
+    }
+}

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -36,9 +36,9 @@ void topWithRefinement() {
     @SuppressWarnings({"cast.unsafe.constructor.invocation"})
     void topWithoutRefinement() {
         TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
-        // See #576.
-        // :TODO: error: (assignment.type.incompatible)
+        // :: error: (assignment.type.incompatible)
         top.f = new @B Object();
+        // :: error: (assignment.type.incompatible)
         top.f = new @A Object();
     }
 }

framework/tests/viewpointtest/VPAExamples.java

@@ -30,7 +30,9 @@ void tests(@A RDContainer a, @B RDContainer b, @Top RDContainer top) {
         // :: error: (argument.type.incompatible)
         b.set(aObj);
         b.set(bObj);
+        // :: error: (argument.type.incompatible)
         top.set(aObj);
+        // :: error: (argument.type.incompatible)
         top.set(bObj);
     }
 }

framework/tests/viewpointtest/VarargsConstructor.java

@@ -17,6 +17,7 @@ void foo() {
     void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
         @A Object a = new @A VarargsConstructor(aObj);
         @B Object b = new @B VarargsConstructor(bObj);
+        // :: error: (argument.type.incompatible)
         @Top Object top = new @Top VarargsConstructor(topObj);
         // :: error: (argument.type.incompatible)
         new @A VarargsConstructor(bObj);
@@ -31,14 +32,17 @@ class Inner {
 
         void foo() {
             Inner a = new Inner();
+            // :: error: (argument.type.incompatible)
             Inner b = new Inner(new Object());
             Inner c = VarargsConstructor.this.new Inner();
+            // :: error: (argument.type.incompatible)
             Inner d = VarargsConstructor.this.new Inner(new Object());
         }
 
         void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
             @A Object a = new @A Inner(aObj);
             @B Object b = new @B Inner(bObj);
+            // :: error: (argument.type.incompatible)
             @Top Object top = new @Top Inner(topObj);
             // :: error: (argument.type.incompatible)
             new @A Inner(bObj);
@@ -56,6 +60,7 @@ void foo() {
                 };
         @A Object a = new @A VarargsConstructor(aObj) {};
         @B Object b = new @B VarargsConstructor(bObj) {};
+        // :: error: (argument.type.incompatible)
         @Top Object top = new @Top VarargsConstructor(topObj) {};
         // :: error: (argument.type.incompatible)
         new @A VarargsConstructor(bObj) {};