Add method call for testing RD class substitution

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -75,6 +75,7 @@
 import org.checkerframework.framework.qual.Unused;
 import org.checkerframework.framework.source.DiagMessage;
 import org.checkerframework.framework.source.SourceVisitor;
+import org.checkerframework.framework.type.AbstractViewpointAdapter;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -5073,9 +5074,18 @@ public boolean isValidUse(
         AnnotationMirrorSet tops = qualHierarchy.getTopAnnotations();
         TypeMirror declarationTM = declarationType.getUnderlyingType();
         AnnotationMirrorSet upperBounds = atypeFactory.getTypeDeclarationBounds(declarationTM);
+        AbstractViewpointAdapter vpa =
+                (AbstractViewpointAdapter) atypeFactory.getViewpointAdapter();
+
         for (AnnotationMirror top : tops) {
             AnnotationMirror upperBound = qualHierarchy.findAnnotationInHierarchy(upperBounds, top);
-            if (!typeHierarchy.isSubtypeShallowEffective(useType, upperBound)) {
+            if (vpa != null) {
+                AnnotatedDeclaredType adaptedBound =
+                        (AnnotatedDeclaredType) vpa.combineAnnotationWithType(upperBound, useType);
+                if (!typeHierarchy.isSubtypeShallowEffective(useType, adaptedBound)) {
+                    return false;
+                }
+            } else if (!typeHierarchy.isSubtypeShallowEffective(useType, upperBound)) {
                 return false;
             }
         }

framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java

@@ -259,7 +259,7 @@ protected AnnotatedTypeMirror combineTypeWithType(
      * @param declared declared type
      * @return {@link AnnotatedTypeMirror} after viewpoint adaptation
      */
-    protected AnnotatedTypeMirror combineAnnotationWithType(
+    public AnnotatedTypeMirror combineAnnotationWithType(
             AnnotationMirror receiverAnnotation, AnnotatedTypeMirror declared) {
         if (declared.getKind().isPrimitive()) {
             AnnotatedPrimitiveType apt = (AnnotatedPrimitiveType) declared.shallowCopy();

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -5689,6 +5689,15 @@ public Trees getTreeUtils() {
         return this.trees;
     }
 
+    /**
+     * Accessor for the viewpoint adapter.
+     *
+     * @return the viewpoint adapter
+     */
+    public ViewpointAdapter getViewpointAdapter() {
+        return this.viewpointAdapter;
+    }
+
     /**
      * Accessor for the processing environment.
      *

framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java

@@ -12,7 +12,11 @@ public class ViewpointTestCheckerTest extends CheckerFrameworkPerDirectoryTest {
      * @param testFiles the files containing test code, which will be type-checked
      */
     public ViewpointTestCheckerTest(List<File> testFiles) {
-        super(testFiles, viewpointtest.ViewpointTestChecker.class, "viewpointtest");
+        super(
+                testFiles,
+                viewpointtest.ViewpointTestChecker.class,
+                "viewpointtest",
+                "-Astubs=src/test/java/viewpointtest/jdk.astub");
     }
 
     @Parameterized.Parameters

framework/src/test/java/viewpointtest/jdk.astub

@@ -0,0 +1,7 @@
+import viewpointtest.quals.ReceiverDependentQual;
+
+package java.lang;
+
+@ReceiverDependentQual class Object {
+    @ReceiverDependentQual Object() {}
+}

framework/tests/viewpointtest/LostNonReflexive.java

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

framework/tests/viewpointtest/PolyConstructor.java

@@ -3,7 +3,7 @@
 public class PolyConstructor {
 
     static class MyClass {
-        // :: error: (super.invocation.invalid) :: warning: (inconsistent.constructor.type)
+        // :: warning: (inconsistent.constructor.type)
         @PolyVP MyClass(@PolyVP Object o) {
             // :: error: (new.class.type.invalid)
             throw new RuntimeException(" * You are filled with DETERMINATION."); // stub

framework/tests/viewpointtest/SuperConstructorCalls.java

@@ -2,24 +2,27 @@
 // https://github.com/eisop/checker-framework/issues/782
 import viewpointtest.quals.*;
 
-public class SuperConstructorCalls {
-
+@ReceiverDependentQual public class SuperConstructorCalls {
+    @SuppressWarnings("inconsistent.constructor.type")
     public SuperConstructorCalls() {}
 
+    @SuppressWarnings("inconsistent.constructor.type")
     public SuperConstructorCalls(@ReceiverDependentQual Object obj) {}
 
     @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
     public @ReceiverDependentQual SuperConstructorCalls(
             @ReceiverDependentQual Object obj, int dummy) {}
 
-    class Inner extends SuperConstructorCalls {
+    @ReceiverDependentQual class Inner extends SuperConstructorCalls {
+        @SuppressWarnings("inconsistent.constructor.type")
         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.
+        @SuppressWarnings("inconsistent.constructor.type")
         public Inner(@Top Object objTop) {
             // :: error: (argument.type.incompatible)
             super(objTop);
@@ -32,7 +35,6 @@ public Inner(@Top Object objTop) {
 
         @SuppressWarnings("inconsistent.constructor.type")
         public @A Inner(@A Object objA, @B Object objB) {
-            // :: error: (super.invocation.invalid)
             super(objA);
         }
 

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -15,9 +15,27 @@
         this.f = new @ReceiverDependentQual Object();
     }
 
+    // This method could be called by both @A and @B instances.
+    void recieverDependentMethod(@ReceiverDependentQual TestGetAnnotatedLhs this) {}
+
+    // This method could only be called by @A instances.
+    void aMethod(@A TestGetAnnotatedLhs this) {}
+
+    // This method could only be called by @B instances.
+    void bMethod(@B TestGetAnnotatedLhs this) {}
+
     @SuppressWarnings({"cast.unsafe.constructor.invocation"})
     void topWithRefinement() {
         TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs();
+        TestGetAnnotatedLhs b = new @B TestGetAnnotatedLhs();
+        a.recieverDependentMethod();
+        b.recieverDependentMethod();
+        a.aMethod();
+        // :: error: (method.invocation.invalid)
+        a.bMethod();
+        // :: error: (method.invocation.invalid)
+        b.aMethod();
+        b.bMethod();
         // :: error: (new.class.type.invalid)
         TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
         top = a;

framework/tests/viewpointtest/ThisConstructorCalls.java

@@ -2,9 +2,11 @@
 
 // Test case for EISOP issue #782:
 // https://github.com/eisop/checker-framework/issues/782
-public class ThisConstructorCalls {
+@ReceiverDependentQual public class ThisConstructorCalls {
+    @SuppressWarnings("inconsistent.constructor.type")
     public ThisConstructorCalls() {}
 
+    @SuppressWarnings("inconsistent.constructor.type")
     public ThisConstructorCalls(@ReceiverDependentQual Object obj) {}
 
     @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
@@ -24,7 +26,6 @@ public ThisConstructorCalls(@ReceiverDependentQual Object obj) {}
 
     @SuppressWarnings("inconsistent.constructor.type")
     public @A ThisConstructorCalls(@A Object objA, @B Object objB) {
-        // :: error: (this.invocation.invalid)
         this(objA);
     }
 }

framework/tests/viewpointtest/VPAExamples.java

@@ -1,6 +1,7 @@
 import viewpointtest.quals.*;
 
-public class VPAExamples {
+@SuppressWarnings("inconsistent.constructor.type")
+@ReceiverDependentQual public class VPAExamples {
 
     static class RDContainer {
         @ReceiverDependentQual Object get() {

framework/tests/viewpointtest/VarargsConstructor.java

@@ -2,15 +2,14 @@
 // https://github.com/eisop/checker-framework/issues/777
 import viewpointtest.quals.*;
 
-public class VarargsConstructor {
-
+@ReceiverDependentQual public class VarargsConstructor {
+    @SuppressWarnings("inconsistent.constructor.type")
     VarargsConstructor(String str, Object... args) {}
 
-    @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"})
+    @SuppressWarnings("inconsistent.constructor.type")
     @ReceiverDependentQual VarargsConstructor(@ReceiverDependentQual Object... args) {}
 
     void foo() {
-        // :: warning: (cast.unsafe.constructor.invocation)
         VarargsConstructor a = new @A VarargsConstructor("testStr", new @A Object());
     }
 
@@ -25,17 +24,14 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
         new @B VarargsConstructor(aObj);
     }
 
-    class Inner {
-        // :: warning: (inconsistent.constructor.type) :: error:(super.invocation.invalid)
+    @ReceiverDependentQual class Inner {
+        @SuppressWarnings("inconsistent.constructor.type")
         @ReceiverDependentQual Inner(@ReceiverDependentQual Object... args) {}
 
         void foo() {
-            // :: error: (new.class.type.invalid)
             Inner a = new Inner();
-            // :: 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());
         }
 
@@ -53,11 +49,9 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) {
 
     void testAnonymousClass(@A Object aObj, @B Object bObj, @Top Object topObj) {
         Object o =
-                // :: warning: (cast.unsafe.constructor.invocation)
                 new @A VarargsConstructor("testStr", new @A Object()) {
                     void foo() {
                         VarargsConstructor a =
-                                // :: warning: (cast.unsafe.constructor.invocation)
                                 new @A VarargsConstructor("testStr", new @A Object());
                     }
                 };