diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6cb489b93f6..ed9fc7e6a40 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/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; } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index a2121ad4bf0..62539f3a879 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/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(); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 4bfa54ee549..85342a310b9 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/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. * diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java index 81479836a19..59f00ae29a7 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java +++ b/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 testFiles) { - super(testFiles, viewpointtest.ViewpointTestChecker.class, "viewpointtest"); + super( + testFiles, + viewpointtest.ViewpointTestChecker.class, + "viewpointtest", + "-Astubs=src/test/java/viewpointtest/jdk.astub"); } @Parameterized.Parameters diff --git a/framework/src/test/java/viewpointtest/jdk.astub b/framework/src/test/java/viewpointtest/jdk.astub new file mode 100644 index 00000000000..046d2ea51c8 --- /dev/null +++ b/framework/src/test/java/viewpointtest/jdk.astub @@ -0,0 +1,7 @@ +import viewpointtest.quals.ReceiverDependentQual; + +package java.lang; + +@ReceiverDependentQual class Object { + @ReceiverDependentQual Object() {} +} diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index eacc4c9b132..36d7ba029d8 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/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) diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index eec0533b8ae..7a7cb0d3b0e 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/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 diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index fc0e5a66f83..a22bcf17803 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -2,17 +2,19 @@ // 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(); } @@ -20,6 +22,7 @@ public Inner() { // 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); } diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index bf2ee83a54c..988d6a25cd6 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/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; diff --git a/framework/tests/viewpointtest/ThisConstructorCalls.java b/framework/tests/viewpointtest/ThisConstructorCalls.java index 0c7567059e7..4d7fe9a6db5 100644 --- a/framework/tests/viewpointtest/ThisConstructorCalls.java +++ b/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); } } diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java index 8cc915c2a5e..4b1a20c726f 100644 --- a/framework/tests/viewpointtest/VPAExamples.java +++ b/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() { diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index bacd874f592..8e72e468818 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/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()); } };