Fix initial store ignoring viewpoint adaption

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java

@@ -72,8 +72,8 @@ public static class FieldInitialValue<V extends CFAbstractValue<V>> {
         /** 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<V extends CFAbstractValue<V>> {
          * 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;

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);
         }
     }
 

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;

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<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         return getBundledTypeQualifiers(
                 A.class,
                 B.class,
+                C.class,
                 Bottom.class,
                 PolyVP.class,
                 ReceiverDependentQual.class,

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;
     }
 }

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 {}

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 {}

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;
+    }
+}