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 c8bd06c60c11..d53ac3d0bf47 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/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. diff --git a/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java b/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java index 518b8e6322f5..67fecba5d788 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java +++ b/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(); } diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java new file mode 100644 index 000000000000..71641a91a717 --- /dev/null +++ b/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(); + } +}