Viewpoint test checker: lost receiver invoke poly receiver method

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

@@ -2,18 +2,13 @@
 
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
 import org.checkerframework.framework.type.NoElementQualifierHierarchy;
-import org.checkerframework.framework.type.QualifierHierarchy;
 
 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;
-
-/** The {@link QualifierHierarchy} for the Viewpoint Test Checker. */
+/** The qualifier hierarchy for the Viewpoint Test Checker. */
 public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy {
     /**
      * Creates a ViewpointTestQualifierHierarchy from the given classes.
@@ -28,14 +23,4 @@ public ViewpointTestQualifierHierarchy(
             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/ViewpointTestVisitor.java

@@ -1,10 +1,12 @@
 package viewpointtest;
 
+import com.sun.source.tree.AssignmentTree;
 import com.sun.source.tree.NewClassTree;
 
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.common.basetype.BaseTypeVisitor;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.util.AnnotatedTypes;
 
 /** The visitor for the Viewpoint Test Checker. */
 public class ViewpointTestVisitor extends BaseTypeVisitor<ViewpointTestAnnotatedTypeFactory> {
@@ -19,10 +21,19 @@ public ViewpointTestVisitor(BaseTypeChecker checker) {
 
     @Override
     public Void visitNewClass(NewClassTree tree, Void p) {
-        AnnotatedTypeMirror Type = atypeFactory.getAnnotatedType(tree);
-        if (Type.hasAnnotation(atypeFactory.TOP) || Type.hasAnnotation(atypeFactory.LOST)) {
-            checker.reportError(tree, "new.class.type.invalid", Type.getAnnotations());
+        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree);
+        if (type.hasAnnotation(atypeFactory.TOP) || type.hasAnnotation(atypeFactory.LOST)) {
+            checker.reportError(tree, "new.class.type.invalid", type.getAnnotations());
         }
         return super.visitNewClass(tree, p);
     }
+
+    @Override
+    public Void visitAssignment(AssignmentTree tree, Void p) {
+        AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(tree.getVariable());
+        if (AnnotatedTypes.containsModifier(variableType, atypeFactory.LOST)) {
+            checker.reportError(tree, "viewpointtest.lost.lhs");
+        }
+        return super.visitAssignment(tree, p);
+    }
 }

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

@@ -12,8 +12,7 @@
  * The Lost qualifier indicates that a relationship cannot be expressed. It is the result of
  * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}.
  *
- * <p>It is not reflexive in the subtyping relationship and the only subtype for Lost is {@link
- * Bottom}.
+ * <p>It is valid as a viewpoint-adaptation result but not as the left-hand side of an assignment.
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)

framework/tests/viewpointtest/LostNonReflexive.java

@@ -2,6 +2,7 @@
 
 public class LostNonReflexive {
     @ReceiverDependentQual Object f;
+    @ReceiverDependentQual LostNonReflexive f2;
 
     @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
     @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {}
@@ -10,11 +11,16 @@ public class LostNonReflexive {
         return null;
     }
 
+    @PolyVP LostNonReflexive identity(@PolyVP LostNonReflexive this) {
+        return this;
+    }
+
     void set(@ReceiverDependentQual Object o) {}
 
     void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) {
-        // :: error: (assignment.type.incompatible)
+        // :: error: (viewpointtest.lost.lhs)
         this.f = obj.f;
+        // :: error: (viewpointtest.lost.lhs)
         this.f = bottomObj;
 
         // :: error: (assignment.type.incompatible)
@@ -24,13 +30,14 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) {
         // :: error: (assignment.type.incompatible)
         @Bottom Object botObj = obj.get();
 
-        // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid)
+        // :: error: (new.class.type.invalid)
         new LostNonReflexive(obj.f);
         // :: error: (new.class.type.invalid)
         new LostNonReflexive(bottomObj);
 
-        // :: error: (argument.type.incompatible)
         this.set(obj.f);
         this.set(bottomObj);
+
+        obj.f2.identity();
     }
 }

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -36,9 +36,9 @@ void topWithRefinement() {
     void topWithoutRefinement() {
         // :: error: (new.class.type.invalid)
         TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
-        // :: error: (assignment.type.incompatible)
+        // :: error: (assignment.type.incompatible) :: error: (viewpointtest.lost.lhs)
         top.f = new @B Object();
-        // :: error: (assignment.type.incompatible)
+        // :: error: (assignment.type.incompatible) :: error: (viewpointtest.lost.lhs)
         top.f = new @A Object();
     }
 }

framework/tests/viewpointtest/VarargsConstructor.java

@@ -63,8 +63,7 @@ void foo() {
                 };
         @A Object a = new @A VarargsConstructor(aObj) {};
         @B Object b = new @B VarargsConstructor(bObj) {};
-        // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error:
-        // (varargs.type.incompatible)
+        // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid)
         @Top Object top = new @Top VarargsConstructor(topObj) {};
         // :: error: (argument.type.incompatible)
         new @A VarargsConstructor(bObj) {};