Add lost qualifier to viewpointtest type checker (#827)

Co-authored-by: Werner Dietl <[email protected]>

checker/src/main/java/org/checkerframework/checker/nullness/messages.properties

@@ -22,7 +22,6 @@ nulltest.redundant=redundant test against null; "%s" is non-null
 instanceof.nullable=instanceof is only true for a non-null expression
 instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof
 new.array.type.invalid=annotations %s may not be applied as component type for array "%s"
-new.class.type.invalid=the annotations %s do not need be applied in object creations
 nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null
 nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null
 nullness.on.exception.parameter=do not write nullness annotations on an exception parameter, which is always non-null

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

@@ -34,6 +34,7 @@ cast.unsafe.constructor.invocation=constructor invocation cast from "%s" to "%s"
 exception.parameter.invalid=invalid type in exception parameter.%nfound   : %s%nrequired: %s
 throw.type.invalid=invalid type thrown.%nfound   : %s%nrequired: %s
 expression.unparsable.type.invalid=Expression invalid in dependent type annotation: %s
+new.class.type.invalid=type annotation %s can not be applied to object creation
 explicit.annotation.ignored=The qualifier %s is ignored in favor of %s. Either delete %s or change it to %s.
 
 override.return.invalid=Incompatible return type.%nfound   : %s%nrequired: %s%nConsequence: method in %s%n  %s%ncannot override method in %s%n  %s

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

@@ -3,19 +3,36 @@
 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 org.checkerframework.javacutil.AnnotationBuilder;
 
 import java.lang.annotation.Annotation;
 import java.util.Set;
 
+import javax.lang.model.element.AnnotationMirror;
+
 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;
 
+/** The annotated type factory for the Viewpoint Test Checker. */
 public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
 
+    /** The {@link Top} annotation. */
+    public final AnnotationMirror TOP = AnnotationBuilder.fromClass(elements, Top.class);
+
+    /** The {@link Lost} annotation. */
+    public final AnnotationMirror LOST = AnnotationBuilder.fromClass(elements, Lost.class);
+
+    /**
+     * Create a new ViewpointTestAnnotatedTypeFactory.
+     *
+     * @param checker the checker to which this annotated type factory belongs
+     */
     public ViewpointTestAnnotatedTypeFactory(BaseTypeChecker checker) {
         super(checker);
         this.postInit();
@@ -29,11 +46,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,41 @@
+package viewpointtest;
+
+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. */
+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,15 @@
 
 import javax.lang.model.element.AnnotationMirror;
 
+import viewpointtest.quals.Lost;
 import viewpointtest.quals.ReceiverDependentQual;
 import viewpointtest.quals.Top;
 
+/** The viewpoint adapter for the Viewpoint Test Checker. */
 public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter {
 
-    private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL;
+    /** The {@link Top}, {@link ReceiverDependentQual} and {@link Lost} annotation. */
+    private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, LOST;
 
     /**
      * The class constructor.
@@ -22,10 +25,11 @@ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter {
      */
     public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) {
         super(atypeFactory);
-        TOP = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Top.class);
+        TOP = ((ViewpointTestAnnotatedTypeFactory) atypeFactory).TOP;
         RECEIVERDEPENDENTQUAL =
                 AnnotationBuilder.fromClass(
                         atypeFactory.getElementUtils(), ReceiverDependentQual.class);
+        LOST = ((ViewpointTestAnnotatedTypeFactory) atypeFactory).LOST;
     }
 
     @Override
@@ -38,7 +42,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/ViewpointTestVisitor.java

@@ -0,0 +1,28 @@
+package viewpointtest;
+
+import com.sun.source.tree.NewClassTree;
+
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.common.basetype.BaseTypeVisitor;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+
+/** The visitor for the Viewpoint Test Checker. */
+public class ViewpointTestVisitor extends BaseTypeVisitor<ViewpointTestAnnotatedTypeFactory> {
+    /**
+     * Create a new ViewpointTestVisitor.
+     *
+     * @param checker the checker to which this visitor belongs
+     */
+    public ViewpointTestVisitor(BaseTypeChecker checker) {
+        super(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());
+        }
+        return super.visitNewClass(tree, p);
+    }
+}

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,22 @@
+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;
+
+/**
+ * The {@link 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 {@link Lost} is
+ * {@link Bottom}.
+ */
+@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,36 @@
+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) :: 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);
+    }
+}

framework/tests/viewpointtest/PolyConstructor.java

@@ -3,10 +3,36 @@
 public class PolyConstructor {
 
     static class MyClass {
-        @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
+        // :: error: (super.invocation.invalid) :: warning: (inconsistent.constructor.type)
         @PolyVP MyClass(@PolyVP Object o) {
+            // :: error: (new.class.type.invalid)
             throw new RuntimeException(" * You are filled with DETERMINATION."); // stub
         }
+
+        void throwTopException() {
+            // :: error: (new.class.type.invalid)
+            throw new @Top RuntimeException();
+        }
+
+        void throwBottomException() {
+            // :: warning: (cast.unsafe.constructor.invocation)
+            throw new @Bottom RuntimeException();
+        }
+
+        void throwAException() {
+            // :: warning: (cast.unsafe.constructor.invocation)
+            throw new @A RuntimeException();
+        }
+
+        void throwBException() {
+            // :: warning: (cast.unsafe.constructor.invocation)
+            throw new @B RuntimeException();
+        }
+
+        void throwLostException() {
+            // :: error: (new.class.type.invalid) :: warning: (cast.unsafe.constructor.invocation)
+            throw new @Lost RuntimeException();
+        }
     }
 
     void tests(@A Object ao) {

framework/tests/viewpointtest/SuperConstructorCalls.java

@@ -17,7 +17,11 @@ public Inner() {
             super();
         }
 
+        // The constructor's return type is implicitly @Top by default.
+        // When calling the super constructor, @Top becomes @Lost in the super constructor's
+        // signature, causing a type mismatch with the expected @ReceiverDependentQual parameter.
         public Inner(@Top Object objTop) {
+            // :: error: (argument.type.incompatible)
             super(objTop);
         }
 

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -18,6 +18,7 @@
     @SuppressWarnings({"cast.unsafe.constructor.invocation"})
     void topWithRefinement() {
         TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs();
+        // :: error: (new.class.type.invalid)
         TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
         top = a;
         // When checking the below assignment, GenericAnnotatedTypeFactory#getAnnotatedTypeLhs()
@@ -33,10 +34,11 @@ void topWithRefinement() {
 
     @SuppressWarnings({"cast.unsafe.constructor.invocation"})
     void topWithoutRefinement() {
+        // :: error: (new.class.type.invalid)
         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

@@ -29,7 +29,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

@@ -10,12 +10,14 @@ public class VarargsConstructor {
     @ReceiverDependentQual VarargsConstructor(@ReceiverDependentQual Object... args) {}
 
     void foo() {
-        VarargsConstructor a = new VarargsConstructor("testStr", new Object());
+        // :: warning: (cast.unsafe.constructor.invocation)
+        VarargsConstructor a = new @A VarargsConstructor("testStr", new @A Object());
     }
 
     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) :: error: (new.class.type.invalid)
         @Top Object top = new @Top VarargsConstructor(topObj);
         // :: error: (argument.type.incompatible)
         new @A VarargsConstructor(bObj);
@@ -24,19 +26,23 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
     }
 
     class Inner {
-        @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
+        // :: warning: (inconsistent.constructor.type) :: error:(super.invocation.invalid)
         @ReceiverDependentQual Inner(@ReceiverDependentQual Object... args) {}
 
         void foo() {
+            // :: error: (new.class.type.invalid)
             Inner a = new Inner();
-            Inner b = new Inner(new Object());
-            Inner c = VarargsConstructor.this.new Inner();
-            Inner d = VarargsConstructor.this.new Inner(new Object());
+            // :: warning: (cast.unsafe.constructor.invocation)
+            Inner b = new @A Inner(new @A Object());
+            Inner c = VarargsConstructor.this.new @A Inner();
+            // :: warning: (cast.unsafe.constructor.invocation)
+            Inner d = VarargsConstructor.this.new @A Inner(new @A 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) :: error: (new.class.type.invalid)
             @Top Object top = new @Top Inner(topObj);
             // :: error: (argument.type.incompatible)
             new @A Inner(bObj);
@@ -47,13 +53,17 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
 
     void testAnonymousClass(@A Object aObj, @B Object bObj, @Top Object topObj) {
         Object o =
-                new VarargsConstructor("testStr", new Object()) {
+                // :: warning: (cast.unsafe.constructor.invocation)
+                new @A VarargsConstructor("testStr", new @A Object()) {
                     void foo() {
-                        VarargsConstructor a = new VarargsConstructor("testStr", new Object());
+                        VarargsConstructor a =
+                                // :: warning: (cast.unsafe.constructor.invocation)
+                                new @A VarargsConstructor("testStr", new @A Object());
                     }
                 };
         @A Object a = new @A VarargsConstructor(aObj) {};
         @B Object b = new @B VarargsConstructor(bObj) {};
+        // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid)
         @Top Object top = new @Top VarargsConstructor(topObj) {};
         // :: error: (argument.type.incompatible)
         new @A VarargsConstructor(bObj) {};