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 ac667319c2f1..9ea575ddca36 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2236,8 +2236,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { List typeargs = mType.typeArgs; List paramBounds = - CollectionsPlume.mapList( - AnnotatedTypeVariable::getBounds, invokedMethod.getTypeVariables()); + atypeFactory.methodTypeVariablesFromUse(tree); ExecutableElement method = invokedMethod.getElement(); CharSequence methodName = ElementUtils.getSimpleDescription(method); 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 7240b8be1e8b..714c59cb5a13 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -2424,6 +2424,29 @@ public List typeVariablesFromUse( return res; } + /** + * Returns the method type parameter bounds adapted to the viewpoint of a method invocation. + * + * @param tree a method invocation + * @return the adapted method type parameter bounds + */ + public List methodTypeVariablesFromUse( + MethodInvocationTree tree) { + AnnotatedExecutableType invokedMethod = + methodFromUseWithoutTypeArgInference(tree).executableType; + List typeVariables = invokedMethod.getTypeVariables(); + List bounds = new ArrayList<>(typeVariables.size()); + for (AnnotatedTypeVariable typeVariable : typeVariables) { + bounds.add(typeVariable.getBounds()); + } + + AnnotatedTypeMirror receiverType = getReceiverType(tree); + if (viewpointAdapter != null && receiverType != null) { + viewpointAdapter.viewpointAdaptTypeParameterBounds(receiverType, bounds); + } + return bounds; + } + /** * Creates and returns an AnnotatedNullType qualified with {@code annotations}. * diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index b5dfaed769af..c53c0ade02b2 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/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); - } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 928860b199dc..28f3457ce481 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -1,13 +1,30 @@ package viewpointtest; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.TreeUtils; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { + + /** Error key for {@code @Lost} in assignment targets. */ + private static final @CompilerMessageKey String LOST_LHS = "viewpointtest.lost.lhs"; + + /** Error key for {@code @Lost} in adapted parameter types. */ + private static final @CompilerMessageKey String LOST_PARAMETER = "viewpointtest.lost.parameter"; + + /** Error key for {@code @Lost} in adapted type parameter bounds. */ + private static final @CompilerMessageKey String LOST_IN_BOUNDS = "viewpointtest.lost.in.bounds"; + /** * Create a new ViewpointTestVisitor. * @@ -19,10 +36,74 @@ 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 visitMethodInvocation(MethodInvocationTree tree, Void p) { + Void result = super.visitMethodInvocation(tree, p); + checkLostMethodTypeParameterBounds(tree); + return result; + } + + @Override + protected boolean commonAssignmentCheck( + Tree varTree, + ExpressionTree valueExpTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + boolean result = super.commonAssignmentCheck(varTree, valueExpTree, errorKey, extraArgs); + AnnotatedTypeMirror varType = atypeFactory.getAnnotatedTypeLhs(varTree); + if (AnnotatedTypes.containsModifier(varType, atypeFactory.LOST)) { + checker.reportError(valueExpTree, LOST_LHS); + result = false; + } + return result; + } + + @Override + protected boolean commonAssignmentCheck( + AnnotatedTypeMirror varType, + AnnotatedTypeMirror valueType, + Tree valueExpTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + boolean result = + super.commonAssignmentCheck(varType, valueType, valueExpTree, errorKey, extraArgs); + if (AnnotatedTypes.containsModifier(varType, atypeFactory.LOST)) { + if (errorKey.equals("argument.type.incompatible") + || errorKey.equals("varargs.type.incompatible")) { + checker.reportError(valueExpTree, LOST_PARAMETER); + } else if (errorKey.equals("unary.increment.type.incompatible") + || errorKey.equals("unary.decrement.type.incompatible")) { + checker.reportError(valueExpTree, LOST_LHS); + } + result = false; + } + return result; + } + + /** + * Report an error if a method invocation viewpoint-adapts a method type parameter bound to + * {@code @Lost}. + * + * @param tree the method invocation to check + */ + private void checkLostMethodTypeParameterBounds(MethodInvocationTree tree) { + if (TreeUtils.elementFromUse(tree) == null || shouldSkipUses(tree)) { + return; + } + + for (AnnotatedTypeParameterBounds bounds : atypeFactory.methodTypeVariablesFromUse(tree)) { + if (AnnotatedTypes.containsModifier(bounds.getUpperBound(), atypeFactory.LOST) + || AnnotatedTypes.containsModifier(bounds.getLowerBound(), atypeFactory.LOST)) { + checker.reportError(tree, LOST_IN_BOUNDS); + return; + } + } + } } diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index 38e215c5293c..bf35191201f0 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -9,11 +9,11 @@ import java.lang.annotation.Target; /** - * The Lost qualifier indicates that a relationship cannot be expressed. It is the result of + * The {@code Lost} qualifier indicates that a relationship cannot be expressed. It results from * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is not reflexive in the subtyping relationship and the only subtype for Lost is {@link - * Bottom}. + *

It is a valid viewpoint-adaptation result but is invalid as an assignment target, including in + * compound assignments, increments, and decrements. */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index eacc4c9b1325..a731d6375885 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -1,7 +1,12 @@ +import java.util.List; + import viewpointtest.quals.*; public class LostNonReflexive { @ReceiverDependentQual Object f; + @ReceiverDependentQual LostNonReflexive f2; + @ReceiverDependentQual int i; + @A List<@ReceiverDependentQual Object> nested; @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {} @@ -10,11 +15,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 +34,24 @@ 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) :: error: (viewpointtest.lost.parameter) new LostNonReflexive(obj.f); - // :: error: (new.class.type.invalid) + // :: error: (new.class.type.invalid) :: error: (viewpointtest.lost.parameter) new LostNonReflexive(bottomObj); - // :: error: (argument.type.incompatible) + // :: error: (viewpointtest.lost.parameter) this.set(obj.f); + // :: error: (viewpointtest.lost.parameter) this.set(bottomObj); + + obj.f2.identity(); + + // :: error: (compound.assignment.type.incompatible) :: error: (viewpointtest.lost.lhs) + obj.i += 1; + // :: error: (unary.increment.type.incompatible) :: error: (viewpointtest.lost.lhs) + obj.i++; + + // :: error: (viewpointtest.lost.lhs) + obj.nested = null; } } diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index fc0e5a66f83a..8120cdf91748 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -21,7 +21,7 @@ public Inner() { // 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) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) super(objTop); } diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index bf2ee83a54c0..9156f4199884 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/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(); } } diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java index 8cc915c2a5e1..92d30812c642 100644 --- a/framework/tests/viewpointtest/VPAExamples.java +++ b/framework/tests/viewpointtest/VPAExamples.java @@ -29,9 +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) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) top.set(aObj); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) top.set(bObj); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index 5382f7559495..77303b0c7ea1 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -17,7 +17,8 @@ void foo() { 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) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: + // (viewpointtest.lost.parameter) @Top Object top = new @Top VarargsConstructor(topObj); // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj); @@ -42,7 +43,8 @@ void foo() { 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) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: + // (viewpointtest.lost.parameter) @Top Object top = new @Top Inner(topObj); // :: error: (argument.type.incompatible) new @A Inner(bObj); @@ -64,7 +66,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) + // (viewpointtest.lost.parameter) @Top Object top = new @Top VarargsConstructor(topObj) {}; // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj) {}; diff --git a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java new file mode 100644 index 000000000000..19ea54de62d3 --- /dev/null +++ b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java @@ -0,0 +1,73 @@ +import viewpointtest.quals.*; + +public class ViewpointAdaptationBounds { + static class Generic {} + + void compatibleBounds(@A Generic<@A Object> a, @B Generic<@B Object> b) {} + + // :: error: (type.argument.type.incompatible) + void receiverDependentArgument(@A Generic<@ReceiverDependentQual Object> rdq) {} + + // :: error: (type.argument.type.incompatible) + void topArgument(@A Generic<@Top Object> top) {} + + // :: error: (type.argument.type.incompatible) + void lostArgument(@A Generic<@Lost Object> lost) {} + + // :: error: (type.argument.type.incompatible) + void incompatibleABound(@A Generic<@B Object> b) {} + + // :: error: (type.argument.type.incompatible) + void incompatibleBBound(@B Generic<@A Object> a) {} + + void topMainBottomArgument(@Top Generic<@Bottom Object> generic) { + @Top Generic<@Bottom Object> local = generic; + } + + void topMainAArgument( + // :: error: (type.argument.type.incompatible) + @Top Generic<@A Object> a) {} + + void topMainBArgument( + // :: error: (type.argument.type.incompatible) + @Top Generic<@B Object> b) {} + + void topMainReceiverDependentArgument( + // :: error: (type.argument.type.incompatible) + @Top Generic<@ReceiverDependentQual Object> rdq) {} + + void topMainTopArgument( + // :: error: (type.argument.type.incompatible) + @Top Generic<@Top Object> top) {} + + void topMainLostArgument(@Top Generic<@Lost Object> lost) {} + + static class TopBounded {} + + void topBound( + @A TopBounded<@A Object> a, + @A TopBounded<@B Object> b, + @A TopBounded<@ReceiverDependentQual Object> rdq, + @A TopBounded<@Top Object> top, + @A TopBounded<@Lost Object> lost) {} + + static class Methods { + void method(T t) {} + + void methodWithNoArgs() {} + } + + void callMethod(@Top Methods m, @A Object a, @Bottom Object b) { + // The upper bound of T adapts to @Lost even though no argument compatibility check runs. + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + m.methodWithNoArgs(); + + // Use an explicit type argument to avoid testing type argument inference here. + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + m.<@A Object>method(a); + + // Even when using @Bottom, the adapted method type parameter bound is @Lost. + // :: error: (viewpointtest.lost.in.bounds) + m.method(b); + } +} diff --git a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java index 8dbbcae855f3..b5f70e833aee 100644 --- a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java +++ b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java @@ -17,10 +17,11 @@ void concreteReceivers(@A Sub a, @B Sub b) { } void topReceiver(@Top Sub top) { - // @Top viewpoint-adapts @ReceiverDependentQual to @Lost, but @Lost is non-reflexive in - // this test checker. - // :: error: (assignment.type.incompatible) + // @Top viewpoint-adapts @ReceiverDependentQual to @Lost in the type argument. + // :: error: (viewpointtest.lost.lhs) @Top Super<@Lost Object> lostSuper = top; + // :: error: (viewpointtest.lost.lhs) + lostSuper = top; // :: error: (assignment.type.incompatible) @Top Super<@A Object> badASuper = top; // :: error: (assignment.type.incompatible)