From d0a276c90ca911527864243a7517917f208dc075 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 4 Apr 2025 21:04:09 -0400 Subject: [PATCH 01/17] Add method invocation with lost receiver test --- framework/tests/viewpointtest/LostNonReflexive.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index eacc4c9b1325..891302548464 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -2,6 +2,7 @@ public class LostNonReflexive { @ReceiverDependentQual Object f; + @ReceiverDependentQual LostNonReflexive f2; @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {} @@ -10,6 +11,10 @@ public class LostNonReflexive { return null; } + @PolyVP LostNonReflexive identity(@PolyVP LostNonReflexive this) { + return this; + } + void set(@ReceiverDependentQual Object o) {} void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { @@ -32,5 +37,7 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { // :: error: (argument.type.incompatible) this.set(obj.f); this.set(bottomObj); + + obj.f2.identity(); } } From 0150bc256013aaffbc95761e7788e5f533835e44 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 23:39:38 -0400 Subject: [PATCH 02/17] Check lost qualifier on assignment LHS --- .../ViewpointTestQualifierHierarchy.java | 17 +---------------- .../viewpointtest/ViewpointTestVisitor.java | 17 ++++++++++++++--- .../src/test/java/viewpointtest/quals/Lost.java | 3 +-- .../tests/viewpointtest/LostNonReflexive.java | 6 +++--- .../viewpointtest/TestGetAnnotatedLhs.java | 4 ++-- .../tests/viewpointtest/VarargsConstructor.java | 3 +-- 6 files changed, 22 insertions(+), 28 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index b5dfaed769af..c53c0ade02b2 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -2,18 +2,13 @@ import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.framework.type.NoElementQualifierHierarchy; -import org.checkerframework.framework.type.QualifierHierarchy; import java.lang.annotation.Annotation; import java.util.Collection; -import javax.lang.model.element.AnnotationMirror; import javax.lang.model.util.Elements; -import viewpointtest.quals.Bottom; -import viewpointtest.quals.Lost; - -/** The {@link QualifierHierarchy} for the Viewpoint Test Checker. */ +/** The qualifier hierarchy for the Viewpoint Test Checker. */ public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy { /** * Creates a ViewpointTestQualifierHierarchy from the given classes. @@ -28,14 +23,4 @@ public ViewpointTestQualifierHierarchy( GenericAnnotatedTypeFactory atypeFactory) { super(qualifierClasses, elements, atypeFactory); } - - @Override - public boolean isSubtypeQualifiers(AnnotationMirror subAnno, AnnotationMirror superAnno) { - // Lost is not reflexive and the only subtype is Bottom. - if (atypeFactory.areSameByClass(superAnno, Lost.class) - && !atypeFactory.areSameByClass(subAnno, Bottom.class)) { - return false; - } - return super.isSubtypeQualifiers(subAnno, superAnno); - } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 928860b199dc..721c67568d87 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -1,10 +1,12 @@ package viewpointtest; +import com.sun.source.tree.AssignmentTree; import com.sun.source.tree.NewClassTree; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.util.AnnotatedTypes; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { @@ -19,10 +21,19 @@ public ViewpointTestVisitor(BaseTypeChecker checker) { @Override public Void visitNewClass(NewClassTree tree, Void p) { - AnnotatedTypeMirror Type = atypeFactory.getAnnotatedType(tree); - if (Type.hasAnnotation(atypeFactory.TOP) || Type.hasAnnotation(atypeFactory.LOST)) { - checker.reportError(tree, "new.class.type.invalid", Type.getAnnotations()); + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); + if (type.hasAnnotation(atypeFactory.TOP) || type.hasAnnotation(atypeFactory.LOST)) { + checker.reportError(tree, "new.class.type.invalid", type.getAnnotations()); } return super.visitNewClass(tree, p); } + + @Override + public Void visitAssignment(AssignmentTree tree, Void p) { + AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(tree.getVariable()); + if (AnnotatedTypes.containsModifier(variableType, atypeFactory.LOST)) { + checker.reportError(tree, "viewpointtest.lost.lhs"); + } + return super.visitAssignment(tree, p); + } } diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index 38e215c5293c..d1289367742b 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -12,8 +12,7 @@ * The Lost qualifier indicates that a relationship cannot be expressed. It is the result of * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is not reflexive in the subtyping relationship and the only subtype for Lost is {@link - * Bottom}. + *

It is valid as a viewpoint-adaptation result but not as the left-hand side of an assignment. */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index 891302548464..655dae387070 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -18,8 +18,9 @@ public class LostNonReflexive { void set(@ReceiverDependentQual Object o) {} void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { - // :: error: (assignment.type.incompatible) + // :: error: (viewpointtest.lost.lhs) this.f = obj.f; + // :: error: (viewpointtest.lost.lhs) this.f = bottomObj; // :: error: (assignment.type.incompatible) @@ -29,12 +30,11 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { // :: error: (assignment.type.incompatible) @Bottom Object botObj = obj.get(); - // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) + // :: error: (new.class.type.invalid) new LostNonReflexive(obj.f); // :: error: (new.class.type.invalid) new LostNonReflexive(bottomObj); - // :: error: (argument.type.incompatible) this.set(obj.f); this.set(bottomObj); diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index bf2ee83a54c0..9156f4199884 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -36,9 +36,9 @@ void topWithRefinement() { void topWithoutRefinement() { // :: error: (new.class.type.invalid) TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) :: error: (viewpointtest.lost.lhs) top.f = new @B Object(); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) :: error: (viewpointtest.lost.lhs) top.f = new @A Object(); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index 5382f7559495..bacd874f592b 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -63,8 +63,7 @@ void foo() { }; @A Object a = new @A VarargsConstructor(aObj) {}; @B Object b = new @B VarargsConstructor(bObj) {}; - // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: - // (varargs.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) @Top Object top = new @Top VarargsConstructor(topObj) {}; // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj) {}; From 30b6f7f39e9fed9cf2e3bdf3931eb8f4f674d57f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 23:47:06 -0400 Subject: [PATCH 03/17] Address lost LHS review feedback --- .../viewpointtest/ViewpointTestVisitor.java | 34 ++++++++++++++++--- .../tests/viewpointtest/LostNonReflexive.java | 6 ++++ 2 files changed, 35 insertions(+), 5 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 721c67568d87..0472c0a5bb6f 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -1,12 +1,14 @@ package viewpointtest; import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.CompoundAssignmentTree; import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.UnaryTree; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.util.AnnotatedTypes; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { @@ -30,10 +32,32 @@ public Void visitNewClass(NewClassTree tree, Void p) { @Override public Void visitAssignment(AssignmentTree tree, Void p) { - AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(tree.getVariable()); - if (AnnotatedTypes.containsModifier(variableType, atypeFactory.LOST)) { - checker.reportError(tree, "viewpointtest.lost.lhs"); - } + checkLostLhs(tree.getVariable(), tree); return super.visitAssignment(tree, p); } + + @Override + public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { + checkLostLhs(tree.getVariable(), tree); + return super.visitCompoundAssignment(tree, p); + } + + @Override + public Void visitUnary(UnaryTree tree, Void p) { + Tree.Kind treeKind = tree.getKind(); + if (treeKind == Tree.Kind.PREFIX_DECREMENT + || treeKind == Tree.Kind.PREFIX_INCREMENT + || treeKind == Tree.Kind.POSTFIX_DECREMENT + || treeKind == Tree.Kind.POSTFIX_INCREMENT) { + checkLostLhs(tree.getExpression(), tree); + } + return super.visitUnary(tree, p); + } + + private void checkLostLhs(Tree variableTree, Tree errorTree) { + AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedTypeLhs(variableTree); + if (variableType.hasAnnotation(atypeFactory.LOST)) { + checker.reportError(errorTree, "viewpointtest.lost.lhs"); + } + } } diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index 655dae387070..10e6d39f18bc 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -3,6 +3,7 @@ public class LostNonReflexive { @ReceiverDependentQual Object f; @ReceiverDependentQual LostNonReflexive f2; + @ReceiverDependentQual int i; @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {} @@ -39,5 +40,10 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { this.set(bottomObj); obj.f2.identity(); + + // :: error: (compound.assignment.type.incompatible) :: error: (viewpointtest.lost.lhs) + obj.i += 1; + // :: error: (unary.increment.type.incompatible) :: error: (viewpointtest.lost.lhs) + obj.i++; } } From a29edf8cc121b57e53071b863fe8e52f6bf7ef90 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 May 2026 23:48:15 -0400 Subject: [PATCH 04/17] Document lost LHS helper --- .../src/test/java/viewpointtest/ViewpointTestVisitor.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 0472c0a5bb6f..19eeb4b50fc4 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -54,6 +54,13 @@ public Void visitUnary(UnaryTree tree, Void p) { return super.visitUnary(tree, p); } + /** + * Report an error if {@code variableTree}, interpreted as an assignment left-hand side, + * contains {@code @Lost}. + * + * @param variableTree the assignment target to check + * @param errorTree the tree on which to report the error + */ private void checkLostLhs(Tree variableTree, Tree errorTree) { AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedTypeLhs(variableTree); if (variableType.hasAnnotation(atypeFactory.LOST)) { From 539258adc054a1db503a404bd3bd318f8e0a5436 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 26 May 2026 00:22:46 -0400 Subject: [PATCH 05/17] Reject nested lost qualifiers on assignment targets --- .../src/test/java/viewpointtest/ViewpointTestVisitor.java | 3 ++- framework/src/test/java/viewpointtest/quals/Lost.java | 3 ++- framework/tests/viewpointtest/LostNonReflexive.java | 6 ++++++ 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 19eeb4b50fc4..e36222d882c3 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -9,6 +9,7 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.util.AnnotatedTypes; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { @@ -63,7 +64,7 @@ public Void visitUnary(UnaryTree tree, Void p) { */ private void checkLostLhs(Tree variableTree, Tree errorTree) { AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedTypeLhs(variableTree); - if (variableType.hasAnnotation(atypeFactory.LOST)) { + if (AnnotatedTypes.containsModifier(variableType, atypeFactory.LOST)) { checker.reportError(errorTree, "viewpointtest.lost.lhs"); } } diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index d1289367742b..1e0fbb79b82c 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -12,7 +12,8 @@ * The Lost qualifier indicates that a relationship cannot be expressed. It is the result of * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is valid as a viewpoint-adaptation result but not as the left-hand side of an assignment. + *

It is valid as a viewpoint-adaptation result but not as an assignment target, including + * compound assignments and increments/decrements. */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index 10e6d39f18bc..cade8314b565 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -1,9 +1,12 @@ +import java.util.List; + import viewpointtest.quals.*; public class LostNonReflexive { @ReceiverDependentQual Object f; @ReceiverDependentQual LostNonReflexive f2; @ReceiverDependentQual int i; + @A List<@ReceiverDependentQual Object> nested; @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {} @@ -45,5 +48,8 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { obj.i += 1; // :: error: (unary.increment.type.incompatible) :: error: (viewpointtest.lost.lhs) obj.i++; + + // :: error: (viewpointtest.lost.lhs) + obj.nested = null; } } From 508ed8ee0c5c76f2fe1e20f6c3b37bdbf6edf19b Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 12:16:47 -0400 Subject: [PATCH 06/17] Handle Lost viewpoint adaptation diagnostics --- .../ViewpointTestTypeValidator.java | 66 +++++++++++++++ .../viewpointtest/ViewpointTestVisitor.java | 81 +++++++++++-------- .../tests/viewpointtest/LostInBounds.java | 14 ++++ .../tests/viewpointtest/LostNonReflexive.java | 6 +- .../viewpointtest/SuperConstructorCalls.java | 2 +- .../tests/viewpointtest/VPAExamples.java | 4 +- .../viewpointtest/VarargsConstructor.java | 9 ++- 7 files changed, 140 insertions(+), 42 deletions(-) create mode 100644 framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java create mode 100644 framework/tests/viewpointtest/LostInBounds.java diff --git a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java new file mode 100644 index 000000000000..e732ffd1fc40 --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java @@ -0,0 +1,66 @@ +package viewpointtest; + +import com.sun.source.tree.ParameterizedTypeTree; + +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeValidator; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.TreeUtils; + +import java.util.List; + +import javax.lang.model.element.TypeElement; + +/** The type validator for the Viewpoint Test Checker. */ +public class ViewpointTestTypeValidator extends BaseTypeValidator { + + private static final @CompilerMessageKey String LOST_IN_BOUNDS = + "viewpointtest.lost.in.bounds"; + + private final ViewpointTestAnnotatedTypeFactory viewpointTypeFactory; + + /** + * Create a new ViewpointTestTypeValidator. + * + * @param checker the checker to which this validator belongs + * @param visitor the visitor to which this validator belongs + * @param atypeFactory the type factory to use + */ + public ViewpointTestTypeValidator( + BaseTypeChecker checker, + BaseTypeVisitor visitor, + ViewpointTestAnnotatedTypeFactory atypeFactory) { + super(checker, visitor, atypeFactory); + viewpointTypeFactory = atypeFactory; + } + + /** Report an error if a type parameter bound contains {@code @Lost} after viewpoint adaptation. */ + @Override + protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedTypeTree tree) { + if (TreeUtils.isDiamondTree(tree)) { + return null; + } + TypeElement element = (TypeElement) type.getUnderlyingType().asElement(); + if (checker.shouldSkipUses(element)) { + return null; + } + + List typeParamBounds = + atypeFactory.typeVariablesFromUse(type, element); + for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { + if (AnnotatedTypes.containsModifier( + atpb.getUpperBound(), viewpointTypeFactory.LOST) + || AnnotatedTypes.containsModifier( + atpb.getLowerBound(), viewpointTypeFactory.LOST)) { + checker.reportError(tree, LOST_IN_BOUNDS); + } + } + + return super.visitParameterizedType(type, tree); + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index e36222d882c3..2a72b264c552 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -1,18 +1,23 @@ package viewpointtest; -import com.sun.source.tree.AssignmentTree; -import com.sun.source.tree.CompoundAssignmentTree; +import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; -import com.sun.source.tree.UnaryTree; import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.util.AnnotatedTypes; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { + + private static final @CompilerMessageKey String LOST_LHS = "viewpointtest.lost.lhs"; + + private static final @CompilerMessageKey String LOST_PARAMETER = "viewpointtest.lost.parameter"; + /** * Create a new ViewpointTestVisitor. * @@ -22,6 +27,13 @@ public ViewpointTestVisitor(BaseTypeChecker checker) { super(checker); } + /** Create the type validator for the Viewpoint Test Checker. */ + @Override + protected BaseTypeValidator createTypeValidator() { + return new ViewpointTestTypeValidator(checker, this, atypeFactory); + } + + /** Report an error if object creation has an invalid result type. */ @Override public Void visitNewClass(NewClassTree tree, Void p) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); @@ -31,41 +43,42 @@ public Void visitNewClass(NewClassTree tree, Void p) { return super.visitNewClass(tree, p); } + /** Report an error if an assignment left-hand side contains {@code @Lost}. */ @Override - public Void visitAssignment(AssignmentTree tree, Void p) { - checkLostLhs(tree.getVariable(), tree); - return super.visitAssignment(tree, p); - } - - @Override - public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { - checkLostLhs(tree.getVariable(), tree); - return super.visitCompoundAssignment(tree, p); - } - - @Override - public Void visitUnary(UnaryTree tree, Void p) { - Tree.Kind treeKind = tree.getKind(); - if (treeKind == Tree.Kind.PREFIX_DECREMENT - || treeKind == Tree.Kind.PREFIX_INCREMENT - || treeKind == Tree.Kind.POSTFIX_DECREMENT - || treeKind == Tree.Kind.POSTFIX_INCREMENT) { - checkLostLhs(tree.getExpression(), tree); + protected boolean commonAssignmentCheck( + Tree varTree, + ExpressionTree valueExpTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + boolean result = super.commonAssignmentCheck(varTree, valueExpTree, errorKey, extraArgs); + AnnotatedTypeMirror varType = atypeFactory.getAnnotatedTypeLhs(varTree); + if (AnnotatedTypes.containsModifier(varType, atypeFactory.LOST)) { + checker.reportError(valueExpTree, LOST_LHS); + result = false; } - return super.visitUnary(tree, p); + return result; } - /** - * Report an error if {@code variableTree}, interpreted as an assignment left-hand side, - * contains {@code @Lost}. - * - * @param variableTree the assignment target to check - * @param errorTree the tree on which to report the error - */ - private void checkLostLhs(Tree variableTree, Tree errorTree) { - AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedTypeLhs(variableTree); - if (AnnotatedTypes.containsModifier(variableType, atypeFactory.LOST)) { - checker.reportError(errorTree, "viewpointtest.lost.lhs"); + /** Report an error if a pseudo-assignment target contains {@code @Lost}. */ + @Override + protected boolean commonAssignmentCheck( + AnnotatedTypeMirror varType, + AnnotatedTypeMirror valueType, + Tree valueExpTree, + @CompilerMessageKey String errorKey, + Object... extraArgs) { + boolean result = + super.commonAssignmentCheck(varType, valueType, valueExpTree, errorKey, extraArgs); + if (AnnotatedTypes.containsModifier(varType, atypeFactory.LOST)) { + if (errorKey.equals("argument.type.incompatible") + || errorKey.equals("varargs.type.incompatible")) { + checker.reportError(valueExpTree, LOST_PARAMETER); + } else if (errorKey.equals("unary.increment.type.incompatible") + || errorKey.equals("unary.decrement.type.incompatible")) { + checker.reportError(valueExpTree, LOST_LHS); + } + result = false; } + return result; } } diff --git a/framework/tests/viewpointtest/LostInBounds.java b/framework/tests/viewpointtest/LostInBounds.java new file mode 100644 index 000000000000..b855a8731fd1 --- /dev/null +++ b/framework/tests/viewpointtest/LostInBounds.java @@ -0,0 +1,14 @@ +import viewpointtest.quals.*; + +public class LostInBounds { + static class Generic {} + + // Use @Bottom so the type argument is within the adapted @Lost bound. That isolates the + // diagnostic for @Lost in the adapted bound. + void testBounds( + // :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Bottom Object> generic) { + // :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Bottom Object> local = generic; + } +} diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index cade8314b565..a731d6375885 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -34,12 +34,14 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { // :: error: (assignment.type.incompatible) @Bottom Object botObj = obj.get(); - // :: error: (new.class.type.invalid) + // :: error: (new.class.type.invalid) :: error: (viewpointtest.lost.parameter) new LostNonReflexive(obj.f); - // :: error: (new.class.type.invalid) + // :: error: (new.class.type.invalid) :: error: (viewpointtest.lost.parameter) new LostNonReflexive(bottomObj); + // :: error: (viewpointtest.lost.parameter) this.set(obj.f); + // :: error: (viewpointtest.lost.parameter) this.set(bottomObj); obj.f2.identity(); diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index fc0e5a66f83a..8120cdf91748 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -21,7 +21,7 @@ public Inner() { // When calling the super constructor, @Top becomes @Lost in the super constructor's // signature, causing a type mismatch with the expected @ReceiverDependentQual parameter. public Inner(@Top Object objTop) { - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) super(objTop); } diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java index 8cc915c2a5e1..92d30812c642 100644 --- a/framework/tests/viewpointtest/VPAExamples.java +++ b/framework/tests/viewpointtest/VPAExamples.java @@ -29,9 +29,9 @@ void tests(@A RDContainer a, @B RDContainer b, @Top RDContainer top) { // :: error: (argument.type.incompatible) b.set(aObj); b.set(bObj); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) top.set(aObj); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) top.set(bObj); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index bacd874f592b..77303b0c7ea1 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -17,7 +17,8 @@ void foo() { void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A VarargsConstructor(aObj); @B Object b = new @B VarargsConstructor(bObj); - // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: + // (viewpointtest.lost.parameter) @Top Object top = new @Top VarargsConstructor(topObj); // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj); @@ -42,7 +43,8 @@ void foo() { void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A Inner(aObj); @B Object b = new @B Inner(bObj); - // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: + // (viewpointtest.lost.parameter) @Top Object top = new @Top Inner(topObj); // :: error: (argument.type.incompatible) new @A Inner(bObj); @@ -63,7 +65,8 @@ void foo() { }; @A Object a = new @A VarargsConstructor(aObj) {}; @B Object b = new @B VarargsConstructor(bObj) {}; - // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) :: error: + // (viewpointtest.lost.parameter) @Top Object top = new @Top VarargsConstructor(topObj) {}; // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj) {}; From 175580c9708018cda2d1f8c4245b99899157517e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 12:58:59 -0400 Subject: [PATCH 07/17] Remove override Javadocs from viewpoint test hooks --- .../test/java/viewpointtest/ViewpointTestTypeValidator.java | 1 - .../src/test/java/viewpointtest/ViewpointTestVisitor.java | 4 ---- 2 files changed, 5 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java index e732ffd1fc40..5a01b038675f 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java @@ -39,7 +39,6 @@ public ViewpointTestTypeValidator( viewpointTypeFactory = atypeFactory; } - /** Report an error if a type parameter bound contains {@code @Lost} after viewpoint adaptation. */ @Override protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedTypeTree tree) { if (TreeUtils.isDiamondTree(tree)) { diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 2a72b264c552..903fb8488131 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -27,13 +27,11 @@ public ViewpointTestVisitor(BaseTypeChecker checker) { super(checker); } - /** Create the type validator for the Viewpoint Test Checker. */ @Override protected BaseTypeValidator createTypeValidator() { return new ViewpointTestTypeValidator(checker, this, atypeFactory); } - /** Report an error if object creation has an invalid result type. */ @Override public Void visitNewClass(NewClassTree tree, Void p) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); @@ -43,7 +41,6 @@ public Void visitNewClass(NewClassTree tree, Void p) { return super.visitNewClass(tree, p); } - /** Report an error if an assignment left-hand side contains {@code @Lost}. */ @Override protected boolean commonAssignmentCheck( Tree varTree, @@ -59,7 +56,6 @@ protected boolean commonAssignmentCheck( return result; } - /** Report an error if a pseudo-assignment target contains {@code @Lost}. */ @Override protected boolean commonAssignmentCheck( AnnotatedTypeMirror varType, From f50096956213a5608bc78427db50a213d66bca39 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 13:17:54 -0400 Subject: [PATCH 08/17] Document viewpoint test diagnostic keys --- .../src/test/java/viewpointtest/ViewpointTestTypeValidator.java | 2 ++ framework/src/test/java/viewpointtest/ViewpointTestVisitor.java | 2 ++ 2 files changed, 4 insertions(+) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java index 5a01b038675f..779b5675d802 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java @@ -19,9 +19,11 @@ /** The type validator for the Viewpoint Test Checker. */ public class ViewpointTestTypeValidator extends BaseTypeValidator { + /** Error key for {@code @Lost} in adapted type parameter bounds. */ private static final @CompilerMessageKey String LOST_IN_BOUNDS = "viewpointtest.lost.in.bounds"; + /** The annotated type factory for the Viewpoint Test Checker. */ private final ViewpointTestAnnotatedTypeFactory viewpointTypeFactory; /** diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 903fb8488131..a61ba99a6b70 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -14,8 +14,10 @@ /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { + /** Error key for {@code @Lost} in assignment targets. */ private static final @CompilerMessageKey String LOST_LHS = "viewpointtest.lost.lhs"; + /** Error key for {@code @Lost} in adapted parameter types. */ private static final @CompilerMessageKey String LOST_PARAMETER = "viewpointtest.lost.parameter"; /** From d8d5584caa0d02048dbabaffd46cfa6f85160d46 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 13:31:20 -0400 Subject: [PATCH 09/17] Apply Spotless to viewpoint test files --- .../java/viewpointtest/ViewpointTestTypeValidator.java | 9 +++------ .../test/java/viewpointtest/ViewpointTestVisitor.java | 2 +- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java index 779b5675d802..32d261a85b6e 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java @@ -2,11 +2,10 @@ import com.sun.source.tree.ParameterizedTypeTree; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; -import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; -import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; import org.checkerframework.framework.util.AnnotatedTypes; @@ -20,8 +19,7 @@ public class ViewpointTestTypeValidator extends BaseTypeValidator { /** Error key for {@code @Lost} in adapted type parameter bounds. */ - private static final @CompilerMessageKey String LOST_IN_BOUNDS = - "viewpointtest.lost.in.bounds"; + private static final @CompilerMessageKey String LOST_IN_BOUNDS = "viewpointtest.lost.in.bounds"; /** The annotated type factory for the Viewpoint Test Checker. */ private final ViewpointTestAnnotatedTypeFactory viewpointTypeFactory; @@ -54,8 +52,7 @@ protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedT List typeParamBounds = atypeFactory.typeVariablesFromUse(type, element); for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { - if (AnnotatedTypes.containsModifier( - atpb.getUpperBound(), viewpointTypeFactory.LOST) + if (AnnotatedTypes.containsModifier(atpb.getUpperBound(), viewpointTypeFactory.LOST) || AnnotatedTypes.containsModifier( atpb.getLowerBound(), viewpointTypeFactory.LOST)) { checker.reportError(tree, LOST_IN_BOUNDS); diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index a61ba99a6b70..488a1eb04155 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -4,10 +4,10 @@ import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; +import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; -import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.util.AnnotatedTypes; From 8c4b0ecdd787611aab3c6133d5e2be8f6ffcd103 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 14:06:49 -0400 Subject: [PATCH 10/17] Retry CI From 04ddd85c5e01b18724a775f5a3394641ee35c20c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 10 Jun 2026 17:25:13 -0400 Subject: [PATCH 11/17] Trigger CI From e9004079cc9b27b8aa3400ee2a556ccc85850526 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 14 Jun 2026 14:04:05 -0400 Subject: [PATCH 12/17] Expand viewpoint adaptation bounds test --- .../tests/viewpointtest/LostInBounds.java | 14 ----- .../ViewpointAdaptationBounds.java | 60 +++++++++++++++++++ 2 files changed, 60 insertions(+), 14 deletions(-) delete mode 100644 framework/tests/viewpointtest/LostInBounds.java create mode 100644 framework/tests/viewpointtest/ViewpointAdaptationBounds.java diff --git a/framework/tests/viewpointtest/LostInBounds.java b/framework/tests/viewpointtest/LostInBounds.java deleted file mode 100644 index b855a8731fd1..000000000000 --- a/framework/tests/viewpointtest/LostInBounds.java +++ /dev/null @@ -1,14 +0,0 @@ -import viewpointtest.quals.*; - -public class LostInBounds { - static class Generic {} - - // Use @Bottom so the type argument is within the adapted @Lost bound. That isolates the - // diagnostic for @Lost in the adapted bound. - void testBounds( - // :: error: (viewpointtest.lost.in.bounds) - @Top Generic<@Bottom Object> generic) { - // :: error: (viewpointtest.lost.in.bounds) - @Top Generic<@Bottom Object> local = generic; - } -} diff --git a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java new file mode 100644 index 000000000000..3f95f87eb942 --- /dev/null +++ b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java @@ -0,0 +1,60 @@ +import viewpointtest.quals.*; + +public class ViewpointAdaptationBounds { + static class Generic {} + + void compatibleBounds(@A Generic<@A Object> a, @B Generic<@B Object> b) {} + + // :: error: (type.argument.type.incompatible) + void receiverDependentArgument(@A Generic<@ReceiverDependentQual Object> rdq) {} + + // :: error: (type.argument.type.incompatible) + void topArgument(@A Generic<@Top Object> top) {} + + // :: error: (type.argument.type.incompatible) + void lostArgument(@A Generic<@Lost Object> lost) {} + + // :: error: (type.argument.type.incompatible) + void incompatibleABound(@A Generic<@B Object> b) {} + + // :: error: (type.argument.type.incompatible) + void incompatibleBBound(@B Generic<@A Object> a) {} + + // Use @Bottom so the type argument is within the adapted @Lost bound. That isolates the + // diagnostic for @Lost in the adapted bound. + void topMainBottomArgument( + // :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Bottom Object> generic) { + // :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Bottom Object> local = generic; + } + + void topMainAArgument( + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@A Object> a) {} + + void topMainBArgument( + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@B Object> b) {} + + void topMainReceiverDependentArgument( + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@ReceiverDependentQual Object> rdq) {} + + void topMainTopArgument( + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Top Object> top) {} + + void topMainLostArgument( + // :: error: (viewpointtest.lost.in.bounds) + @Top Generic<@Lost Object> lost) {} + + static class TopBounded {} + + void topBound( + @A TopBounded<@A Object> a, + @A TopBounded<@B Object> b, + @A TopBounded<@ReceiverDependentQual Object> rdq, + @A TopBounded<@Top Object> top, + @A TopBounded<@Lost Object> lost) {} +} From ceeab99325c33af2de91f40ea6a0e4483629630b Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 15 Jun 2026 15:55:21 -0400 Subject: [PATCH 13/17] Improve English documentation in Lost qualifier --- framework/src/test/java/viewpointtest/quals/Lost.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index 1e0fbb79b82c..bf35191201f0 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -9,11 +9,11 @@ import java.lang.annotation.Target; /** - * The Lost qualifier indicates that a relationship cannot be expressed. It is the result of + * The {@code Lost} qualifier indicates that a relationship cannot be expressed. It results from * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is valid as a viewpoint-adaptation result but not as an assignment target, including - * compound assignments and increments/decrements. + *

It is a valid viewpoint-adaptation result but is invalid as an assignment target, including in + * compound assignments, increments, and decrements. */ @Documented @Retention(RetentionPolicy.RUNTIME) From 8a68568adeb68ec0a4f8c59aaa8f72587a5e01b6 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 15 Jun 2026 15:55:35 -0400 Subject: [PATCH 14/17] Add viewpoint adaptation method invocation test cases --- .../ViewpointAdaptationBounds.java | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java index 3f95f87eb942..e6791f98be91 100644 --- a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java +++ b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java @@ -57,4 +57,28 @@ void topBound( @A TopBounded<@ReceiverDependentQual Object> rdq, @A TopBounded<@Top Object> top, @A TopBounded<@Lost Object> lost) {} + + static class Methods { + void method(T t) {} + + void methodWithNoArgs() {} + } + + void callMethod(@Top Methods m, @A Object a, @Bottom Object b) { + // Here, the upper bound of T adapts to @Lost, but because we pass no arguments, + // no argument compatibility check fails. If method type parameter bounds were checked, + // this would report `viewpointtest.lost.in.bounds`. Currently, it reports 0 errors, + // clearly illustrating the missing bounds check for method invocations! + m.methodWithNoArgs(); + + // When arguments are provided, it fails subtyping because no qualifier + // is a subtype of @Lost. + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) + m.method(a); + + // Even when using @Bottom, the argument is incompatible because @Lost is intentionally + // excluded from the standard qualifier hierarchy (i.e., @Bottom <: @Lost is false). + // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) + m.method(b); + } } From 8a41e417735d9260c7a1cd0daeb33b813fba6641 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 16 Jun 2026 22:25:04 -0400 Subject: [PATCH 15/17] Check adapted Lost method bounds --- .../ViewpointTestAnnotatedTypeFactory.java | 30 +++++++++++ .../viewpointtest/ViewpointTestVisitor.java | 52 ++++++++++++++++++- .../ViewpointAdaptationBounds.java | 18 +++---- ...ointAdaptationSuperclassInstantiation.java | 8 +-- 4 files changed, 93 insertions(+), 15 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index 2f71b9d2206c..a3933f186231 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -1,12 +1,20 @@ package viewpointtest; +import com.sun.source.tree.MethodInvocationTree; + import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.AnnotationBuilder; import java.lang.annotation.Annotation; +import java.util.ArrayList; +import java.util.List; import java.util.Set; import javax.lang.model.element.AnnotationMirror; @@ -61,4 +69,26 @@ public QualifierHierarchy createQualifierHierarchy() { return new ViewpointTestQualifierHierarchy( this.getSupportedTypeQualifiers(), elements, this); } + + /** + * Returns the method type parameter bounds adapted to the viewpoint of a method invocation. + * + * @param tree a method invocation + * @return the adapted method type parameter bounds + */ + List methodTypeVariablesFromUse(MethodInvocationTree tree) { + AnnotatedExecutableType invokedMethod = + methodFromUseWithoutTypeArgInference(tree).executableType; + List typeVariables = invokedMethod.getTypeVariables(); + List bounds = new ArrayList<>(typeVariables.size()); + for (AnnotatedTypeVariable typeVariable : typeVariables) { + bounds.add(typeVariable.getBounds()); + } + + AnnotatedTypeMirror receiverType = getReceiverType(tree); + if (viewpointAdapter != null && receiverType != null) { + viewpointAdapter.viewpointAdaptTypeParameterBounds(receiverType, bounds); + } + return bounds; + } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 488a1eb04155..b8a0461c8c3c 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -1,15 +1,19 @@ package viewpointtest; import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; +import com.sun.source.tree.VariableTree; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.TreeUtils; /** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { @@ -20,6 +24,9 @@ public class ViewpointTestVisitor extends BaseTypeVisitormethod(a); - // Even when using @Bottom, the argument is incompatible because @Lost is intentionally - // excluded from the standard qualifier hierarchy (i.e., @Bottom <: @Lost is false). - // :: error: (argument.type.incompatible) :: error: (viewpointtest.lost.parameter) + // Even when using @Bottom, the adapted method type parameter bound is @Lost. + // :: error: (viewpointtest.lost.in.bounds) m.method(b); } } diff --git a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java index 8dbbcae855f3..95fddfe30536 100644 --- a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java +++ b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java @@ -17,10 +17,12 @@ void concreteReceivers(@A Sub a, @B Sub b) { } void topReceiver(@Top Sub top) { - // @Top viewpoint-adapts @ReceiverDependentQual to @Lost, but @Lost is non-reflexive in - // this test checker. - // :: error: (assignment.type.incompatible) + // Class type arguments may contain @Lost, so this declaration initialization is valid. + // @Top viewpoint-adapts @ReceiverDependentQual to @Lost in the type argument. @Top Super<@Lost Object> lostSuper = top; + // Updates are still rejected if the LHS type contains @Lost. + // :: error: (viewpointtest.lost.lhs) + lostSuper = top; // :: error: (assignment.type.incompatible) @Top Super<@A Object> badASuper = top; // :: error: (assignment.type.incompatible) From 625ab89018a1f124e50a0cf7f6c4d1e75a3e93cd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 16 Jun 2026 22:35:16 -0400 Subject: [PATCH 16/17] Reject Lost in declaration LHS --- .../viewpointtest/ViewpointTestVisitor.java | 19 +------------------ ...ointAdaptationSuperclassInstantiation.java | 3 +-- 2 files changed, 2 insertions(+), 20 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index b8a0461c8c3c..b1b32d9b1125 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -4,7 +4,6 @@ import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; -import com.sun.source.tree.VariableTree; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; @@ -65,7 +64,7 @@ protected boolean commonAssignmentCheck( Object... extraArgs) { boolean result = super.commonAssignmentCheck(varTree, valueExpTree, errorKey, extraArgs); AnnotatedTypeMirror varType = atypeFactory.getAnnotatedTypeLhs(varTree); - if (hasInvalidLostLhs(varTree, varType)) { + if (AnnotatedTypes.containsModifier(varType, atypeFactory.LOST)) { checker.reportError(valueExpTree, LOST_LHS); result = false; } @@ -94,22 +93,6 @@ protected boolean commonAssignmentCheck( return result; } - /** - * Returns true if an assignment target has an invalid {@code @Lost}. Variable declarations may - * use {@code @Lost} in class type arguments, but updates to an existing target are rejected if - * the target type contains {@code @Lost}. - * - * @param varTree the assignment target - * @param varType the target type - * @return true if the assignment target has an invalid {@code @Lost} - */ - private boolean hasInvalidLostLhs(Tree varTree, AnnotatedTypeMirror varType) { - if (varTree instanceof VariableTree) { - return varType.hasAnnotation(atypeFactory.LOST); - } - return AnnotatedTypes.containsModifier(varType, atypeFactory.LOST); - } - /** * Report an error if a method invocation viewpoint-adapts a method type parameter bound to * {@code @Lost}. diff --git a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java index 95fddfe30536..b5f70e833aee 100644 --- a/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java +++ b/framework/tests/viewpointtest/ViewpointAdaptationSuperclassInstantiation.java @@ -17,10 +17,9 @@ void concreteReceivers(@A Sub a, @B Sub b) { } void topReceiver(@Top Sub top) { - // Class type arguments may contain @Lost, so this declaration initialization is valid. // @Top viewpoint-adapts @ReceiverDependentQual to @Lost in the type argument. + // :: error: (viewpointtest.lost.lhs) @Top Super<@Lost Object> lostSuper = top; - // Updates are still rejected if the LHS type contains @Lost. // :: error: (viewpointtest.lost.lhs) lostSuper = top; // :: error: (assignment.type.incompatible) From c72da598bb0b9936291c93d6fcfd6b41bb14bfe7 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 4 Jul 2026 17:00:13 -0400 Subject: [PATCH 17/17] Adapt method type parameter bounds from use --- .../common/basetype/BaseTypeVisitor.java | 3 +- .../framework/type/AnnotatedTypeFactory.java | 23 +++++++ .../ViewpointTestAnnotatedTypeFactory.java | 30 --------- .../ViewpointTestTypeValidator.java | 64 ------------------- .../viewpointtest/ViewpointTestVisitor.java | 6 -- .../ViewpointAdaptationBounds.java | 21 ++---- 6 files changed, 31 insertions(+), 116 deletions(-) delete mode 100644 framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index ac667319c2f1..9ea575ddca36 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2236,8 +2236,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { List typeargs = mType.typeArgs; List paramBounds = - CollectionsPlume.mapList( - AnnotatedTypeVariable::getBounds, invokedMethod.getTypeVariables()); + atypeFactory.methodTypeVariablesFromUse(tree); ExecutableElement method = invokedMethod.getElement(); CharSequence methodName = ElementUtils.getSimpleDescription(method); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 0609a387345d..8ba38c6a76b3 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -2339,6 +2339,29 @@ public List typeVariablesFromUse( return res; } + /** + * Returns the method type parameter bounds adapted to the viewpoint of a method invocation. + * + * @param tree a method invocation + * @return the adapted method type parameter bounds + */ + public List methodTypeVariablesFromUse( + MethodInvocationTree tree) { + AnnotatedExecutableType invokedMethod = + methodFromUseWithoutTypeArgInference(tree).executableType; + List typeVariables = invokedMethod.getTypeVariables(); + List bounds = new ArrayList<>(typeVariables.size()); + for (AnnotatedTypeVariable typeVariable : typeVariables) { + bounds.add(typeVariable.getBounds()); + } + + AnnotatedTypeMirror receiverType = getReceiverType(tree); + if (viewpointAdapter != null && receiverType != null) { + viewpointAdapter.viewpointAdaptTypeParameterBounds(receiverType, bounds); + } + return bounds; + } + /** * Creates and returns an AnnotatedNullType qualified with {@code annotations}. * diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index a3933f186231..2f71b9d2206c 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -1,20 +1,12 @@ package viewpointtest; -import com.sun.source.tree.MethodInvocationTree; - import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.type.AbstractViewpointAdapter; -import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; -import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.AnnotationBuilder; import java.lang.annotation.Annotation; -import java.util.ArrayList; -import java.util.List; import java.util.Set; import javax.lang.model.element.AnnotationMirror; @@ -69,26 +61,4 @@ public QualifierHierarchy createQualifierHierarchy() { return new ViewpointTestQualifierHierarchy( this.getSupportedTypeQualifiers(), elements, this); } - - /** - * Returns the method type parameter bounds adapted to the viewpoint of a method invocation. - * - * @param tree a method invocation - * @return the adapted method type parameter bounds - */ - List methodTypeVariablesFromUse(MethodInvocationTree tree) { - AnnotatedExecutableType invokedMethod = - methodFromUseWithoutTypeArgInference(tree).executableType; - List typeVariables = invokedMethod.getTypeVariables(); - List bounds = new ArrayList<>(typeVariables.size()); - for (AnnotatedTypeVariable typeVariable : typeVariables) { - bounds.add(typeVariable.getBounds()); - } - - AnnotatedTypeMirror receiverType = getReceiverType(tree); - if (viewpointAdapter != null && receiverType != null) { - viewpointAdapter.viewpointAdaptTypeParameterBounds(receiverType, bounds); - } - return bounds; - } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java b/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java deleted file mode 100644 index 32d261a85b6e..000000000000 --- a/framework/src/test/java/viewpointtest/ViewpointTestTypeValidator.java +++ /dev/null @@ -1,64 +0,0 @@ -package viewpointtest; - -import com.sun.source.tree.ParameterizedTypeTree; - -import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.common.basetype.BaseTypeValidator; -import org.checkerframework.common.basetype.BaseTypeVisitor; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; -import org.checkerframework.framework.util.AnnotatedTypes; -import org.checkerframework.javacutil.TreeUtils; - -import java.util.List; - -import javax.lang.model.element.TypeElement; - -/** The type validator for the Viewpoint Test Checker. */ -public class ViewpointTestTypeValidator extends BaseTypeValidator { - - /** Error key for {@code @Lost} in adapted type parameter bounds. */ - private static final @CompilerMessageKey String LOST_IN_BOUNDS = "viewpointtest.lost.in.bounds"; - - /** The annotated type factory for the Viewpoint Test Checker. */ - private final ViewpointTestAnnotatedTypeFactory viewpointTypeFactory; - - /** - * Create a new ViewpointTestTypeValidator. - * - * @param checker the checker to which this validator belongs - * @param visitor the visitor to which this validator belongs - * @param atypeFactory the type factory to use - */ - public ViewpointTestTypeValidator( - BaseTypeChecker checker, - BaseTypeVisitor visitor, - ViewpointTestAnnotatedTypeFactory atypeFactory) { - super(checker, visitor, atypeFactory); - viewpointTypeFactory = atypeFactory; - } - - @Override - protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedTypeTree tree) { - if (TreeUtils.isDiamondTree(tree)) { - return null; - } - TypeElement element = (TypeElement) type.getUnderlyingType().asElement(); - if (checker.shouldSkipUses(element)) { - return null; - } - - List typeParamBounds = - atypeFactory.typeVariablesFromUse(type, element); - for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { - if (AnnotatedTypes.containsModifier(atpb.getUpperBound(), viewpointTypeFactory.LOST) - || AnnotatedTypes.containsModifier( - atpb.getLowerBound(), viewpointTypeFactory.LOST)) { - checker.reportError(tree, LOST_IN_BOUNDS); - } - } - - return super.visitParameterizedType(type, tree); - } -} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index b1b32d9b1125..28f3457ce481 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -7,7 +7,6 @@ import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.common.basetype.BaseTypeValidator; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; @@ -35,11 +34,6 @@ public ViewpointTestVisitor(BaseTypeChecker checker) { super(checker); } - @Override - protected BaseTypeValidator createTypeValidator() { - return new ViewpointTestTypeValidator(checker, this, atypeFactory); - } - @Override public Void visitNewClass(NewClassTree tree, Void p) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); diff --git a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java index 9ea7879bcd78..19ea54de62d3 100644 --- a/framework/tests/viewpointtest/ViewpointAdaptationBounds.java +++ b/framework/tests/viewpointtest/ViewpointAdaptationBounds.java @@ -20,34 +20,27 @@ void incompatibleABound(@A Generic<@B Object> b) {} // :: error: (type.argument.type.incompatible) void incompatibleBBound(@B Generic<@A Object> a) {} - // Use @Bottom so the type argument is within the adapted @Lost bound. That isolates the - // diagnostic for @Lost in the adapted bound. - void topMainBottomArgument( - // :: error: (viewpointtest.lost.in.bounds) - @Top Generic<@Bottom Object> generic) { - // :: error: (viewpointtest.lost.in.bounds) + void topMainBottomArgument(@Top Generic<@Bottom Object> generic) { @Top Generic<@Bottom Object> local = generic; } void topMainAArgument( - // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + // :: error: (type.argument.type.incompatible) @Top Generic<@A Object> a) {} void topMainBArgument( - // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + // :: error: (type.argument.type.incompatible) @Top Generic<@B Object> b) {} void topMainReceiverDependentArgument( - // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + // :: error: (type.argument.type.incompatible) @Top Generic<@ReceiverDependentQual Object> rdq) {} void topMainTopArgument( - // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) + // :: error: (type.argument.type.incompatible) @Top Generic<@Top Object> top) {} - void topMainLostArgument( - // :: error: (viewpointtest.lost.in.bounds) - @Top Generic<@Lost Object> lost) {} + void topMainLostArgument(@Top Generic<@Lost Object> lost) {} static class TopBounded {} @@ -66,7 +59,7 @@ static class Methods { void callMethod(@Top Methods m, @A Object a, @Bottom Object b) { // The upper bound of T adapts to @Lost even though no argument compatibility check runs. - // :: error: (viewpointtest.lost.in.bounds) + // :: error: (type.argument.type.incompatible) :: error: (viewpointtest.lost.in.bounds) m.methodWithNoArgs(); // Use an explicit type argument to avoid testing type argument inference here.