Apply flow-refinement for receivers even when using getAnnotatedTypeLhs

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

@@ -1781,6 +1781,24 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
         return res;
     }
 
+    /**
+     * As long as everUseFlow is true, always enable flow refinement for the receiver. This method
+     * is an implementation detail and visible inside the package only. See the comment in this
+     * testcase for more details framework/tests/viewpointtest/TestGetAnnotatedLhs.java.
+     *
+     * @see #getAnnotatedType(Tree)
+     * @see #getAnnotatedTypeLhs(Tree)
+     * @param tree an expression tree
+     * @return the refined type of the expression tree
+     */
+    /*package-private*/ AnnotatedTypeMirror getAnnotatedTypeWithReceiverRefinement(Tree tree) {
+        boolean oldUseFlow = useFlow;
+        useFlow = everUseFlow;
+        AnnotatedTypeMirror result = getAnnotatedType(tree);
+        useFlow = oldUseFlow;
+        return result;
+    }
+
     /**
      * Returns the type of a varargs array of a method invocation or a constructor invocation.
      * Returns null only if private field {@code useFlow} is false.

framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java

@@ -270,7 +270,22 @@ public AnnotatedTypeMirror visitMemberSelect(MemberSelectTree tree, AnnotatedTyp
         } else {
             // tree must be a field access, so get the type of the expression, and then call
             // asMemberOf.
-            AnnotatedTypeMirror t = f.getAnnotatedType(tree.getExpression());
+            AnnotatedTypeMirror t;
+            if (f instanceof GenericAnnotatedTypeFactory) {
+                // If calling GenericAnnotatedTypeFactory#getAnnotatedTypeLhs(Tree lhsTree) to
+                // get the type of this MemberSelectTree, flow refinement is disabled. However,
+                // we want the receiver to have the refined type because type
+                // systems can use receiver-dependent qualifiers for viewpoint adaptation.
+                // Thus, we re-enable the flow refinement for a while just for the receiver
+                // expression.
+                // See framework/tests/viewpointtest/TestGetAnnotatedLhs.java for a concrete
+                // example.
+                t =
+                        ((GenericAnnotatedTypeFactory<?, ?, ?, ?>) f)
+                                .getAnnotatedTypeWithReceiverRefinement(tree.getExpression());
+            } else {
+                t = f.getAnnotatedType(tree.getExpression());
+            }
             t = f.applyCaptureConversion(t);
             return AnnotatedTypes.asMemberOf(f.types, f, t, elt).asUse();
         }

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -0,0 +1,44 @@
+import viewpointtest.quals.A;
+import viewpointtest.quals.B;
+import viewpointtest.quals.ReceiverDependentQual;
+import viewpointtest.quals.Top;
+
+@ReceiverDependentQual
+class TestGetAnnotatedLhs {
+    @ReceiverDependentQual Object f;
+
+    @SuppressWarnings({
+        "inconsistent.constructor.type",
+        "super.invocation.invalid",
+        "cast.unsafe.constructor.invocation"
+    })
+    @ReceiverDependentQual
+    TestGetAnnotatedLhs() {
+        this.f = new @ReceiverDependentQual Object();
+    }
+
+    @SuppressWarnings({"cast.unsafe.constructor.invocation"})
+    void topWithRefinement() {
+        TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs();
+        TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
+        top = a;
+        // When checking the below assignment, GenericAnnotatedTypeFactory#getAnnotatedTypeLhs()
+        // will be called to get the type of the lhs tree (top.f).
+        // Previously this method will completely disable flow refinment, and top.f will have type
+        // @Top and thus accept the below assingment. But we should reject it, as top
+        // is refined to be @A before. As long as top is still pointing to the @A object, top.f
+        // will have type @A, which is not the supertype of @B.
+        // :: error: (assignment.type.incompatible)
+        top.f = new @B Object();
+        top.f = new @A Object(); // no error here
+    }
+
+    @SuppressWarnings({"cast.unsafe.constructor.invocation"})
+    void topWithoutRefinement() {
+        TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
+        // See #576.
+        // :TODO: error: (assignment.type.incompatible)
+        top.f = new @B Object();
+        top.f = new @A Object();
+    }
+}