diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index f1ccf838bf4..e3aaa1a85d3 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/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 diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 1644fa2acdb..87fcc85c9ac 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/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 diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index f2027bae843..a17426e754a 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/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,6 +46,7 @@ protected Set> createSupportedTypeQualifiers() { Bottom.class, PolyVP.class, ReceiverDependentQual.class, + Lost.class, Top.class); } @@ -36,4 +54,10 @@ protected Set> createSupportedTypeQualifiers() { protected AbstractViewpointAdapter createViewpointAdapter() { return new ViewpointTestViewpointAdapter(this); } + + @Override + public QualifierHierarchy createQualifierHierarchy() { + return new ViewpointTestQualifierHierarchy( + this.getSupportedTypeQualifiers(), elements, this); + } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java new file mode 100644 index 00000000000..b5dfaed769a --- /dev/null +++ b/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> 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); + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index bf4f491edba..aae61833e10 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/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; } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java new file mode 100644 index 00000000000..928860b199d --- /dev/null +++ b/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 { + /** + * 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); + } +} diff --git a/framework/src/test/java/viewpointtest/quals/Bottom.java b/framework/src/test/java/viewpointtest/quals/Bottom.java index 484726ae7f4..753d57fad71 100644 --- a/framework/src/test/java/viewpointtest/quals/Bottom.java +++ b/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 {} diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java new file mode 100644 index 00000000000..ade8ff1d01b --- /dev/null +++ b/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}. + * + *

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 {} diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java new file mode 100644 index 00000000000..eacc4c9b132 --- /dev/null +++ b/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); + } +} diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index 66ab42c48d9..eec0533b8ae 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/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) { diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index cf7213d6e9f..fc0e5a66f83 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/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); } diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index 12e3d79d862..bf2ee83a54c 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/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(); } } diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java index fbaa2b62b08..8cc915c2a5e 100644 --- a/framework/tests/viewpointtest/VPAExamples.java +++ b/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); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index 962fdc1bfc9..bacd874f592 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/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) {};