diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index f98260e8876..23b74ab65ec 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -72,8 +72,8 @@ public static class FieldInitialValue> { /** A field access that corresponds to the declaration of a field. */ public final FieldAccess fieldDecl; - /** The value corresponding to the annotations on the declared type of the field. */ - public final V declared; + /** The declared type of the field. */ + public final AnnotatedTypeMirror declared; /** The value of the initializer of the field, or null if no initializer exists. */ public final @Nullable V initializer; @@ -82,12 +82,12 @@ public static class FieldInitialValue> { * Creates a new FieldInitialValue. * * @param fieldDecl a field access that corresponds to the declaration of a field - * @param declared value corresponding to the annotations on the declared type of {@code - * field} + * @param declared declared type of {@code field} * @param initializer value of the initializer of {@code field}, or null if no initializer * exists */ - public FieldInitialValue(FieldAccess fieldDecl, V declared, @Nullable V initializer) { + public FieldInitialValue( + FieldAccess fieldDecl, AnnotatedTypeMirror declared, @Nullable V initializer) { this.fieldDecl = fieldDecl; this.declared = declared; this.initializer = initializer; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 8130f4aff65..3f71fe1e298 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -53,6 +53,7 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.framework.util.Contract; import org.checkerframework.framework.util.Contract.ConditionalPostcondition; import org.checkerframework.framework.util.Contract.Postcondition; @@ -419,22 +420,37 @@ private void addInitialFieldValues(S store, ClassTree classTree, MethodTree meth continue; } - boolean isFieldOfCurrentClass = varEle.getEnclosingElement().equals(classEle); - // Maybe insert the declared type: - if (!isConstructor) { - // If it's not a constructor, use the declared type if the receiver of the method is - // fully initialized. - boolean isInitializedReceiver = !isNotFullyInitializedReceiver(methodTree); - if (isInitializedReceiver && isFieldOfCurrentClass) { - store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); - } - } else { - // If it is a constructor, then only use the declared type if the field has been - // initialized. - if (fieldInitialValue.initializer != null && isFieldOfCurrentClass) { - store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); + // If the field belongs to another class, don't add it to the store. + if (!varEle.getEnclosingElement().equals(classEle)) { + continue; + } + + // Maybe insert the adapted or declared field type: + V value = null; + if ((isConstructor || isStaticMethod) && fieldInitialValue.initializer != null) { + // If it is a constructor or static method, then use the declared type + // if the field has been initialized. + value = analysis.createAbstractValue(fieldInitialValue.declared); + } else if (!isStaticMethod) { + // If it's a non-constructor object method, + // use the adapted type if the receiver of the method is fully initialized. + if (!isNotFullyInitializedReceiver(methodTree)) { + AnnotatedTypeMirror receiverType = + analysis.getTypeFactory().getSelfType(methodTree.getBody()); + AnnotatedTypeMirror adaptedType = + AnnotatedTypes.asMemberOf( + analysis.getTypes(), + analysis.getTypeFactory(), + receiverType, + fieldInitialValue.fieldDecl.getField(), + fieldInitialValue.declared); + value = analysis.createAbstractValue(adaptedType); + if (value == null) { + value = analysis.createAbstractValue(fieldInitialValue.declared); + } } } + store.insertValue(fieldInitialValue.fieldDecl, value); } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 1ee058ca562..88b5fefbc92 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1459,7 +1459,6 @@ protected void performFlowAnalysis(ClassTree classTree) { VariableTree vt = (VariableTree) m; ExpressionTree initializer = vt.getInitializer(); AnnotatedTypeMirror declaredType = getAnnotatedTypeLhs(vt); - Value declaredValue = analysis.createAbstractValue(declaredType); FieldAccess fieldExpr = (FieldAccess) JavaExpression.fromVariableTree(vt); // analyze initializer if present @@ -1480,12 +1479,11 @@ protected void performFlowAnalysis(ClassTree classTree) { if (initializerValue != null) { fieldValues.add( new FieldInitialValue<>( - fieldExpr, declaredValue, initializerValue)); + fieldExpr, declaredType, initializerValue)); break; } } - fieldValues.add( - new FieldInitialValue<>(fieldExpr, declaredValue, null)); + fieldValues.add(new FieldInitialValue<>(fieldExpr, declaredType, null)); break; case BLOCK: BlockTree b = (BlockTree) m; diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index f2027bae843..548a7e3d19b 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -10,6 +10,7 @@ import viewpointtest.quals.A; import viewpointtest.quals.B; import viewpointtest.quals.Bottom; +import viewpointtest.quals.C; import viewpointtest.quals.PolyVP; import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; @@ -26,6 +27,7 @@ protected Set> createSupportedTypeQualifiers() { return getBundledTypeQualifiers( A.class, B.class, + C.class, Bottom.class, PolyVP.class, ReceiverDependentQual.class, diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 9da9504eead..ba715b46541 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -8,12 +8,14 @@ import javax.lang.model.element.AnnotationMirror; +import viewpointtest.quals.A; +import viewpointtest.quals.C; import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { - private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL; + private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, A, C; /** * The class constructor. @@ -26,6 +28,8 @@ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { RECEIVERDEPENDENTQUAL = AnnotationBuilder.fromClass( atypeFactory.getElementUtils(), ReceiverDependentQual.class); + A = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), A.class); + C = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), C.class); } @Override @@ -39,7 +43,14 @@ protected AnnotationMirror combineAnnotationWithAnnotation( if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDENTQUAL)) { return receiverAnnotation; + } else if (AnnotationUtils.areSame(declaredAnnotation, C)) { + if (AnnotationUtils.areSame(receiverAnnotation, TOP)) { + return TOP; + } else { + return C; + } + } else { + return declaredAnnotation; } - return declaredAnnotation; } } diff --git a/framework/src/test/java/viewpointtest/quals/Bottom.java b/framework/src/test/java/viewpointtest/quals/Bottom.java index 484726ae7f4..f5066cfcf59 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, C.class, ReceiverDependentQual.class}) @DefaultFor(TypeUseLocation.LOWER_BOUND) public @interface Bottom {} diff --git a/framework/src/test/java/viewpointtest/quals/C.java b/framework/src/test/java/viewpointtest/quals/C.java new file mode 100644 index 00000000000..0caeaef2a1e --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/C.java @@ -0,0 +1,19 @@ +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; + +/** + * Unlike {@link A} and {@link B}, this qualifier is adapted to {@link Top} whenever it appears on a + * field of a {@link Top} receiver. In all other cases, it stays {@code C}. + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface C {} diff --git a/framework/tests/viewpointtest/ReceiverAdaption.java b/framework/tests/viewpointtest/ReceiverAdaption.java new file mode 100644 index 00000000000..c7e40978ed5 --- /dev/null +++ b/framework/tests/viewpointtest/ReceiverAdaption.java @@ -0,0 +1,40 @@ +import viewpointtest.quals.*; + +public class ReceiverAdaption { + + @ReceiverDependentQual Object dependent; + + @C Object c; + + void testA(@A ReceiverAdaption this) { + @A Object varA = dependent; + // :: error: (assignment.type.incompatible) + @B Object varB = dependent; + @C Object varC = c; + // :: error: (assignment.type.incompatible) + @A Object varAc = c; + // :: error: (assignment.type.incompatible) + @B Object varBc = c; + } + + void testB(@B ReceiverAdaption this) { + // :: error: (assignment.type.incompatible) + @A Object varA = dependent; + @B Object varB = dependent; + @C Object varC = c; + // :: error: (assignment.type.incompatible) + @A Object varAc = c; + // :: error: (assignment.type.incompatible) + @B Object varBc = c; + } + + void testTop(@Top ReceiverAdaption this) { + // :: error: (assignment.type.incompatible) + @A Object varA = dependent; + // :: error: (assignment.type.incompatible) + @B Object varB = dependent; + // :: error: (assignment.type.incompatible) + @C Object varC = c; + @Top Object varT = c; + } +}