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 253f6d1ce7a..1660c09d668 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -106,32 +106,45 @@ public void viewpointAdaptConstructor( AnnotatedTypeMirror receiverType, ExecutableElement constructorElt, AnnotatedExecutableType constructorType) { - // constructorType's typevar are not substituted when calling viewpointAdaptConstructor + // 1. Make a copy of constructorType before type variables are substituted. AnnotatedExecutableType unsubstitutedConstructorType = constructorType.deepCopy(); - // For constructors, we adapt parameter types, return type and type parameters + // 2. Viewpoint-adapt constructor parameter types, type variable bounds, and return type. List parameterTypes = unsubstitutedConstructorType.getParameterTypes(); List typeVariables = unsubstitutedConstructorType.getTypeVariables(); AnnotatedTypeMirror constructorReturn = unsubstitutedConstructorType.getReturnType(); IdentityHashMap mappings = new IdentityHashMap<>(); + + // 2a. Adapt parameter types. for (AnnotatedTypeMirror parameterType : parameterTypes) { AnnotatedTypeMirror p = combineTypeWithType(receiverType, parameterType); mappings.put(parameterType, p); } - for (AnnotatedTypeMirror typeVariable : typeVariables) { - AnnotatedTypeMirror tv = combineTypeWithType(receiverType, typeVariable); - mappings.put(typeVariable, tv); + + // 2b. Adapt upper and lower bounds of constructor type variables. + for (AnnotatedTypeVariable typeVariable : typeVariables) { + AnnotatedTypeMirror adaptedUpper = + combineTypeWithType(receiverType, typeVariable.getUpperBound()); + mappings.put(typeVariable.getUpperBound(), adaptedUpper); + + AnnotatedTypeMirror adaptedLower = + combineTypeWithType(receiverType, typeVariable.getLowerBound()); + mappings.put(typeVariable.getLowerBound(), adaptedLower); } + + // 2c. Adapt constructor return type. AnnotatedTypeMirror cr = combineTypeWithType(receiverType, constructorReturn); mappings.put(constructorReturn, cr); + // 3. Replace components using AnnotatedTypeCopierWithReplacement. unsubstitutedConstructorType = (AnnotatedExecutableType) AnnotatedTypeCopierWithReplacement.replace( unsubstitutedConstructorType, mappings); + // 4. Update target constructor type in place with adapted components. constructorType.setParameterTypes(unsubstitutedConstructorType.getParameterTypes()); constructorType.setTypeVariables(unsubstitutedConstructorType.getTypeVariables()); constructorType.setReturnType(unsubstitutedConstructorType.getReturnType()); @@ -142,14 +155,15 @@ public void viewpointAdaptMethod( AnnotatedTypeMirror receiverType, ExecutableElement methodElt, AnnotatedExecutableType methodType) { + // 1. Check whether the method should be viewpoint-adapted (e.g. skip static methods). if (!shouldAdaptMethod(methodElt)) { return; } - // methodType's typevar are not substituted when calling viewpointAdaptMethod + // 2. Make a copy of methodType before type variables are substituted. AnnotatedExecutableType unsubstitutedMethodType = methodType.deepCopy(); - // For methods, we additionally adapt method receiver compared to constructors + // 3. Viewpoint-adapt parameter types, type variable bounds, return type, and receiver. List parameterTypes = unsubstitutedMethodType.getParameterTypes(); List typeVariables = unsubstitutedMethodType.getTypeVariables(); AnnotatedTypeMirror returnType = unsubstitutedMethodType.getReturnType(); @@ -158,33 +172,44 @@ public void viewpointAdaptMethod( IdentityHashMap mappings = new IdentityHashMap<>(); + // 3a. Adapt parameter types. for (AnnotatedTypeMirror parameterType : parameterTypes) { AnnotatedTypeMirror p = combineTypeWithType(receiverType, parameterType); mappings.put(parameterType, p); } + // 3b. Adapt upper and lower bounds of method type variables. for (AnnotatedTypeVariable typeVariable : typeVariables) { - AnnotatedTypeMirror tv = combineTypeWithType(receiverType, typeVariable); - mappings.put(typeVariable, tv); + AnnotatedTypeMirror adaptedUpper = + combineTypeWithType(receiverType, typeVariable.getUpperBound()); + mappings.put(typeVariable.getUpperBound(), adaptedUpper); + + AnnotatedTypeMirror adaptedLower = + combineTypeWithType(receiverType, typeVariable.getLowerBound()); + mappings.put(typeVariable.getLowerBound(), adaptedLower); } + // 3c. Adapt non-void return type. if (returnType.getKind() != TypeKind.VOID) { AnnotatedTypeMirror r = combineTypeWithType(receiverType, returnType); mappings.put(returnType, r); } + // 3d. Adapt method receiver type. if (methodReceiver != null) { AnnotatedTypeMirror mr = combineTypeWithType(receiverType, methodReceiver); mappings.put(methodReceiver, mr); } + // 4. Replace components using AnnotatedTypeCopierWithReplacement. unsubstitutedMethodType = (AnnotatedExecutableType) AnnotatedTypeCopierWithReplacement.replace( unsubstitutedMethodType, mappings); + // 5. Update target method type in place with adapted components. // Because we can't viewpoint adapt asMemberOf result, we adapt the declared method first, - // and sets the corresponding parts to asMemberOf result + // and set the corresponding parts on the asMemberOf result. methodType.setReturnType(unsubstitutedMethodType.getReturnType()); methodType.setReceiverType(unsubstitutedMethodType.getReceiverType()); methodType.setParameterTypes(unsubstitutedMethodType.getParameterTypes()); diff --git a/framework/tests/viewpointtest/ConstructorTypeVariableBounds.java b/framework/tests/viewpointtest/ConstructorTypeVariableBounds.java new file mode 100644 index 00000000000..7ce3c7512e6 --- /dev/null +++ b/framework/tests/viewpointtest/ConstructorTypeVariableBounds.java @@ -0,0 +1,199 @@ +import viewpointtest.quals.*; + +public class ConstructorTypeVariableBounds { + static class C { + // No-arg generic constructor: type argument is unused, so inference instantiates T to + // the adapted upper bound. + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + C() {} + + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + C(T t) {} + } + + static class LowerBoundC { + // The @ReceiverDependentQual annotation on T is its explicit lower bound. The upper bound + // is the implicit Object bound. + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + <@ReceiverDependentQual T> LowerBoundC() {} + + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + <@ReceiverDependentQual T> LowerBoundC(T t) {} + } + + static class LowerAndUpperBoundC { + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + <@ReceiverDependentQual T extends @ReceiverDependentQual Object> LowerAndUpperBoundC() {} + + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + <@ReceiverDependentQual T extends @ReceiverDependentQual Object> LowerAndUpperBoundC(T t) {} + } + + void topViewpoint(@Top Object top, @A Object a, @B Object b, @Bottom Object bottom) { + // Constructed type @Top adapts @ReceiverDependentQual to @Lost. Creating @Top is also + // forbidden by the viewpoint test checker. + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new @Top C(); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@Top Object>@Top C(top); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@A Object>@Top C(a); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@B Object>@Top C(b); + + // :: error: (new.class.type.invalid) + new <@Bottom Object>@Top C(bottom); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top C(top); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top C(a); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top C(b); + + // :: error: (new.class.type.invalid) + new @Top C(bottom); + + // The lower bound @ReceiverDependentQual viewpoint-adapts to @Lost. Explicit type + // arguments must be supertypes of that lower bound, so only @Top is valid. + // :: error: (new.class.type.invalid) + new @Top LowerBoundC(); + + // :: error: (new.class.type.invalid) + new <@Top Object>@Top LowerBoundC(top); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@A Object>@Top LowerBoundC(a); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@B Object>@Top LowerBoundC(b); + + // :: error: (new.class.type.invalid) :: error: (type.argument.type.incompatible) + new <@Bottom Object>@Top LowerBoundC(bottom); + + // Inference can choose @Top, which is above both the adapted lower bound and the argument. + // :: error: (new.class.type.invalid) + new @Top LowerBoundC(top); + + // :: error: (new.class.type.invalid) + new @Top LowerBoundC(a); + + // :: error: (new.class.type.invalid) + new @Top LowerBoundC(b); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerBoundC(bottom); + + // Both bounds viewpoint-adapt to @Lost. Because @Lost is non-reflexive, no type argument + // can be both above the lower bound and below the upper bound. + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerAndUpperBoundC(); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new <@Top Object>@Top LowerAndUpperBoundC(top); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new <@A Object>@Top LowerAndUpperBoundC(a); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new <@B Object>@Top LowerAndUpperBoundC(b); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new <@Bottom Object>@Top LowerAndUpperBoundC(bottom); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerAndUpperBoundC(top); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerAndUpperBoundC(a); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerAndUpperBoundC(b); + + // :: error: (new.class.type.invalid) :: error: (type.arguments.not.inferred) + new @Top LowerAndUpperBoundC(bottom); + } + + @SuppressWarnings("cast.unsafe.constructor.invocation") + void aViewpoint(@Top Object top, @A Object a, @B Object b, @Bottom Object bottom) { + // Constructed type @A adapts @ReceiverDependentQual to @A, so @A and @Bottom are within + // the adapted constructor type parameter bound. Inference instantiates T to @A for the + // no-arg constructor. + new @A C(); + + // :: error: (type.argument.type.incompatible) + new <@Top Object>@A C(top); + + new <@A Object>@A C(a); + + // :: error: (type.argument.type.incompatible) + new <@B Object>@A C(b); + + new <@Bottom Object>@A C(bottom); + + // :: error: (type.arguments.not.inferred) + new @A C(top); + + // Inference succeeds: argument @A is within the adapted bound @A. + new @A C(a); + + // :: error: (type.arguments.not.inferred) + new @A C(b); + + new @A C(bottom); + + // The lower bound @ReceiverDependentQual viewpoint-adapts to @A. Explicit type arguments + // must be supertypes of @A, so @Top and @A are valid. + new @A LowerBoundC(); + + new <@Top Object>@A LowerBoundC(top); + + new <@A Object>@A LowerBoundC(a); + + // :: error: (type.argument.type.incompatible) + new <@B Object>@A LowerBoundC(b); + + // :: error: (type.argument.type.incompatible) + new <@Bottom Object>@A LowerBoundC(bottom); + + // Inference chooses a type argument that is above both @A and the invocation argument. + new @A LowerBoundC(top); + + new @A LowerBoundC(a); + + new @A LowerBoundC(b); + + new @A LowerBoundC(bottom); + + // Both bounds viewpoint-adapt to @A, so an explicit type argument must be exactly @A. + new @A LowerAndUpperBoundC(); + + // :: error: (type.argument.type.incompatible) + new <@Top Object>@A LowerAndUpperBoundC(top); + + new <@A Object>@A LowerAndUpperBoundC(a); + + // :: error: (type.argument.type.incompatible) + new <@B Object>@A LowerAndUpperBoundC(b); + + // :: error: (type.argument.type.incompatible) + new <@Bottom Object>@A LowerAndUpperBoundC(bottom); + + // :: error: (type.arguments.not.inferred) + new @A LowerAndUpperBoundC(top); + + // Inference chooses T = @A. + new @A LowerAndUpperBoundC(a); + + // :: error: (type.arguments.not.inferred) + new @A LowerAndUpperBoundC(b); + + // Inference chooses T = @A, which accepts the @Bottom argument. + new @A LowerAndUpperBoundC(bottom); + } +} diff --git a/framework/tests/viewpointtest/MethodTypeVariableBounds.java b/framework/tests/viewpointtest/MethodTypeVariableBounds.java new file mode 100644 index 00000000000..4035b643983 --- /dev/null +++ b/framework/tests/viewpointtest/MethodTypeVariableBounds.java @@ -0,0 +1,179 @@ +import viewpointtest.quals.*; + +public class MethodTypeVariableBounds { + static class Methods { + void noArg() {} + + void withArg(T t) {} + + // The @ReceiverDependentQual annotation on T is its explicit lower bound. The upper bound + // is the implicit Object bound. + <@ReceiverDependentQual T> void lowerNoArg() {} + + <@ReceiverDependentQual T> void lowerWithArg(T t) {} + + <@ReceiverDependentQual T extends @ReceiverDependentQual Object> + void lowerAndUpperNoArg() {} + + <@ReceiverDependentQual T extends @ReceiverDependentQual Object> void lowerAndUpperWithArg( + T t) {} + } + + void topReceiver( + @Top Methods methods, + @Top Object top, + @A Object a, + @B Object b, + @Bottom Object bottom) { + // @Top viewpoint-adapts @ReceiverDependentQual to @Lost, so only @Bottom is within the + // adapted method type parameter bound. + // :: error: (type.argument.type.incompatible) + methods.noArg(); + + // :: error: (type.argument.type.incompatible) + methods.<@Top Object>withArg(top); + + // :: error: (type.argument.type.incompatible) + methods.<@A Object>withArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>withArg(b); + + methods.<@Bottom Object>withArg(bottom); + + // :: error: (type.arguments.not.inferred) + methods.withArg(top); + + // :: error: (type.arguments.not.inferred) + methods.withArg(a); + + // :: error: (type.arguments.not.inferred) + methods.withArg(b); + + methods.withArg(bottom); + + // The lower bound @ReceiverDependentQual viewpoint-adapts to @Lost. Explicit type + // arguments must be supertypes of that lower bound, so only @Top is valid. + methods.lowerNoArg(); + methods.<@Top Object>lowerWithArg(top); + + // :: error: (type.argument.type.incompatible) + methods.<@A Object>lowerWithArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>lowerWithArg(b); + + // :: error: (type.argument.type.incompatible) + methods.<@Bottom Object>lowerWithArg(bottom); + + // Inference can choose @Top, which is above both the adapted lower bound and the argument. + methods.lowerWithArg(top); + methods.lowerWithArg(a); + methods.lowerWithArg(b); + + // :: error: (type.arguments.not.inferred) + methods.lowerWithArg(bottom); + + // Both bounds viewpoint-adapt to @Lost. Because @Lost is non-reflexive, no type argument + // can be both above the lower bound and below the upper bound. + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperNoArg(); + + // :: error: (type.argument.type.incompatible) + methods.<@Top Object>lowerAndUpperWithArg(top); + + // :: error: (type.argument.type.incompatible) + methods.<@A Object>lowerAndUpperWithArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>lowerAndUpperWithArg(b); + + // :: error: (type.argument.type.incompatible) + methods.<@Bottom Object>lowerAndUpperWithArg(bottom); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(top); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(a); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(b); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(bottom); + } + + void aReceiver( + @A Methods methods, @Top Object top, @A Object a, @B Object b, @Bottom Object bottom) { + // @A viewpoint-adapts @ReceiverDependentQual to @A, so @A and @Bottom are within the + // adapted method type parameter bound. Inference instantiates T to the adapted upper + // bound @A, which is a valid type argument. + methods.noArg(); + + // :: error: (type.argument.type.incompatible) + methods.<@Top Object>withArg(top); + + methods.<@A Object>withArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>withArg(b); + + methods.<@Bottom Object>withArg(bottom); + + // :: error: (type.arguments.not.inferred) + methods.withArg(top); + + // Inference succeeds: argument @A is within the adapted bound @A. + methods.withArg(a); + + // :: error: (type.arguments.not.inferred) + methods.withArg(b); + + methods.withArg(bottom); + + // The lower bound @ReceiverDependentQual viewpoint-adapts to @A. Explicit type arguments + // must be supertypes of @A, so @Top and @A are valid. + methods.lowerNoArg(); + methods.<@Top Object>lowerWithArg(top); + methods.<@A Object>lowerWithArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>lowerWithArg(b); + + // :: error: (type.argument.type.incompatible) + methods.<@Bottom Object>lowerWithArg(bottom); + + // Inference chooses a type argument that is above both @A and the invocation argument. + methods.lowerWithArg(top); + methods.lowerWithArg(a); + methods.lowerWithArg(b); + methods.lowerWithArg(bottom); + + // Both bounds viewpoint-adapt to @A, so an explicit type argument must be exactly @A. + methods.lowerAndUpperNoArg(); + + // :: error: (type.argument.type.incompatible) + methods.<@Top Object>lowerAndUpperWithArg(top); + + methods.<@A Object>lowerAndUpperWithArg(a); + + // :: error: (type.argument.type.incompatible) + methods.<@B Object>lowerAndUpperWithArg(b); + + // :: error: (type.argument.type.incompatible) + methods.<@Bottom Object>lowerAndUpperWithArg(bottom); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(top); + + // Inference chooses T = @A. + methods.lowerAndUpperWithArg(a); + + // :: error: (type.arguments.not.inferred) + methods.lowerAndUpperWithArg(b); + + // Inference chooses T = @A, which accepts the @Bottom argument. + methods.lowerAndUpperWithArg(bottom); + } +}