From 8ebb81918463cb279f0a550a559a0e97db60357b Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 1 Jul 2025 10:22:24 -0400 Subject: [PATCH 01/12] Introduce `@NullMarked` aliasing --- .../NullnessNoInitAnnotatedTypeFactory.java | 10 ++++ .../common/basetype/BaseTypeChecker.java | 47 +++++++++++++++++++ .../framework/source/SourceChecker.java | 25 +--------- 3 files changed, 58 insertions(+), 24 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java index 5da576329b08..8a13d8f73907 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java @@ -32,6 +32,7 @@ import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.DefaultQualifier; import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AnnotatedTypeFactory; @@ -416,6 +417,15 @@ public NullnessNoInitAnnotatedTypeFactory(BaseTypeChecker checker) { "org.jspecify.nullness.NullMarked", DefaultQualifier.class.getCanonicalName(), nullMarkedDefaultQual); + + AnnotationMirror annotatedForNullness = + new AnnotationBuilder(processingEnv, AnnotatedFor.class) + .setValue("value", new String[] {"nullness"}) + .build(); + addAliasedDeclAnnotation( + "org.jspecify.annotations.NullMarked", + AnnotatedFor.class.getCanonicalName(), + annotatedForNullness); } boolean permitClearProperty = diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 0bb07e6db3f8..cfec240642af 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -4,6 +4,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.signature.qual.ClassGetName; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; +import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; @@ -13,6 +14,7 @@ import org.checkerframework.javacutil.AbstractTypeProcessor; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TypeSystemError; import org.checkerframework.javacutil.UserError; import org.plumelib.util.CollectionsPlume; @@ -25,6 +27,9 @@ import java.util.Set; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.PackageElement; /** * An abstract {@link SourceChecker} that provides a simple {@link @@ -313,4 +318,46 @@ public BaseTypeChecker getUltimateParentChecker() { causeMessage); } } + + /** + * This method is almost identical to {@link + * org.checkerframework.framework.util.defaults.QualifierDefaults#isElementAnnotatedForThisChecker(Element)}. + * except for early return if element is null and the conservative default for "source" is not + * used. + * + * @param elt the source code element to check, or null + * @return true if the element is annotated for this checker or an upstream checker + */ + @Override + protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + if (elt == null || !useConservativeDefault("source")) { + return false; + } + + boolean elementAnnotatedForThisChecker = false; + AnnotationMirror annotatedFor = getTypeFactory().getDeclAnnotation(elt, AnnotatedFor.class); + + if (annotatedFor != null) { + elementAnnotatedForThisChecker = + getTypeFactory().doesAnnotatedForApplyToThisChecker(annotatedFor); + } + + if (!elementAnnotatedForThisChecker) { + Element parent; + if (elt.getKind() == ElementKind.PACKAGE) { + // TODO: should AnnotatedFor apply to subpackages?? + // elt.getEnclosingElement() on a package is null; therefore, + // use the dedicated method. + parent = ElementUtils.parentPackage((PackageElement) elt, elements); + } else { + parent = elt.getEnclosingElement(); + } + + if (parent != null && isAnnotatedForThisCheckerOrUpstreamChecker(parent)) { + elementAnnotatedForThisChecker = true; + } + } + + return elementAnnotatedForThisChecker; + } } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 11709a6877b8..ffe791c8b654 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -32,9 +32,7 @@ import org.checkerframework.checker.signature.qual.FullyQualifiedName; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.reflection.MethodValChecker; -import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.util.CheckerMain; import org.checkerframework.framework.util.OptionConfiguration; import org.checkerframework.framework.util.TreePathCacher; import org.checkerframework.javacutil.AbstractTypeProcessor; @@ -2984,28 +2982,7 @@ protected boolean messageKeyMatches( * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker */ - private boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { - if (elt == null || !useConservativeDefault("source")) { - return false; - } - - AnnotatedFor anno = elt.getAnnotation(AnnotatedFor.class); - - String[] userAnnotatedFors = (anno == null ? null : anno.value()); - - if (userAnnotatedFors != null) { - List<@FullyQualifiedName String> upstreamCheckerNames = getUpstreamCheckerNames(); - - for (String userAnnotatedFor : userAnnotatedFors) { - if (CheckerMain.matchesCheckerOrSubcheckerFromList( - userAnnotatedFor, upstreamCheckerNames)) { - return true; - } - } - } - - return false; - } + protected abstract boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt); /** * Returns a modifiable set of lower-case strings that are prefixes for SuppressWarnings From 1366194ae7373e32c9dd7d31d74201fd45a42eb5 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 1 Jul 2025 10:39:46 -0400 Subject: [PATCH 02/12] Keep the source checker version implementation --- .../common/basetype/BaseTypeChecker.java | 26 +++---------------- .../framework/source/SourceChecker.java | 25 +++++++++++++++++- 2 files changed, 28 insertions(+), 23 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index cfec240642af..129c45ee5716 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -14,7 +14,6 @@ import org.checkerframework.javacutil.AbstractTypeProcessor; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.BugInCF; -import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TypeSystemError; import org.checkerframework.javacutil.UserError; import org.plumelib.util.CollectionsPlume; @@ -28,8 +27,6 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; -import javax.lang.model.element.ElementKind; -import javax.lang.model.element.PackageElement; /** * An abstract {@link SourceChecker} that provides a simple {@link @@ -320,10 +317,11 @@ public BaseTypeChecker getUltimateParentChecker() { } /** - * This method is almost identical to {@link + * This method is almost similar to {@link * org.checkerframework.framework.util.defaults.QualifierDefaults#isElementAnnotatedForThisChecker(Element)}. - * except for early return if element is null and the conservative default for "source" is not - * used. + * except for early return if element is null, the conservative default for "source" is not used + * and do not recursively check enclosing elements because the logic is implemented at call + * sites. * * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker @@ -342,22 +340,6 @@ protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element e getTypeFactory().doesAnnotatedForApplyToThisChecker(annotatedFor); } - if (!elementAnnotatedForThisChecker) { - Element parent; - if (elt.getKind() == ElementKind.PACKAGE) { - // TODO: should AnnotatedFor apply to subpackages?? - // elt.getEnclosingElement() on a package is null; therefore, - // use the dedicated method. - parent = ElementUtils.parentPackage((PackageElement) elt, elements); - } else { - parent = elt.getEnclosingElement(); - } - - if (parent != null && isAnnotatedForThisCheckerOrUpstreamChecker(parent)) { - elementAnnotatedForThisChecker = true; - } - } - return elementAnnotatedForThisChecker; } } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index ffe791c8b654..0f0c65e7169b 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -32,7 +32,9 @@ import org.checkerframework.checker.signature.qual.FullyQualifiedName; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.reflection.MethodValChecker; +import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.util.CheckerMain; import org.checkerframework.framework.util.OptionConfiguration; import org.checkerframework.framework.util.TreePathCacher; import org.checkerframework.javacutil.AbstractTypeProcessor; @@ -2982,7 +2984,28 @@ protected boolean messageKeyMatches( * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker */ - protected abstract boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt); + protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + if (elt == null || !useConservativeDefault("source")) { + return false; + } + + AnnotatedFor anno = elt.getAnnotation(AnnotatedFor.class); + + String[] userAnnotatedFors = (anno == null ? null : anno.value()); + + if (userAnnotatedFors != null) { + List<@FullyQualifiedName String> upstreamCheckerNames = getUpstreamCheckerNames(); + + for (String userAnnotatedFor : userAnnotatedFors) { + if (CheckerMain.matchesCheckerOrSubcheckerFromList( + userAnnotatedFor, upstreamCheckerNames)) { + return true; + } + } + } + + return false; + } /** * Returns a modifiable set of lower-case strings that are prefixes for SuppressWarnings From fce8b4385b408f99563a656ea23f7095c8a49eff Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 1 Jul 2025 13:08:05 -0400 Subject: [PATCH 03/12] Add test case and flag --- .../checker/test/junit/NullnessNullMarkedTest.java | 7 ++++++- .../nullness-nullmarked/NullMarkedSuppressError.java | 11 +++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 checker/tests/nullness-nullmarked/NullMarkedSuppressError.java diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java index df697164a87c..74c790c9b427 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java @@ -17,7 +17,12 @@ public class NullnessNullMarkedTest extends CheckerFrameworkPerDirectoryTest { * @param testFiles the files containing test code, which will be type-checked */ public NullnessNullMarkedTest(List testFiles) { - super(testFiles, org.checkerframework.checker.nullness.NullnessChecker.class, "nullness"); + super( + testFiles, + org.checkerframework.checker.nullness.NullnessChecker.class, + "nullness", + // TODO: Replace this `-AonlyAnnotatedFor` flag after EISOP#1290 is merged. + "-AuseConservativeDefaultsForUncheckedCode=source"); } @Parameters diff --git a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java new file mode 100644 index 000000000000..7ffb8bcb6e94 --- /dev/null +++ b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java @@ -0,0 +1,11 @@ +public class NullMarkedSuppressError { + @org.jspecify.annotations.NullMarked + class A { + // :: error: (assignment.type.incompatible) + Object o = null; + } + + class B { + Object o = null; + } +} From 8131a526c462065aef78d59bf5f34f73af7314be Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 9 Jul 2025 20:40:28 -0400 Subject: [PATCH 04/12] Refactor cache to determine if an element is annotatedfor --- .../common/basetype/BaseTypeChecker.java | 6 +++ .../framework/source/SourceChecker.java | 2 +- .../framework/stub/AnnotationFileParser.java | 2 +- .../framework/type/AnnotatedTypeFactory.java | 52 ++++++++++++++++++- .../util/defaults/QualifierDefaults.java | 49 ++--------------- 5 files changed, 62 insertions(+), 49 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 0bb07e6db3f8..9d88fac577d6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -25,6 +25,7 @@ import java.util.Set; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; /** * An abstract {@link SourceChecker} that provides a simple {@link @@ -313,4 +314,9 @@ public BaseTypeChecker getUltimateParentChecker() { causeMessage); } } + + @Override + protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + return getTypeFactory().isElementAnnotatedForThisCheckerOrUpstreamChecker(elt); + } } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 8f169f8454d2..8ea9376284ef 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -2995,7 +2995,7 @@ protected boolean messageKeyMatches( * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker */ - private boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { if (elt == null || !useConservativeDefaultsSource) { return false; } diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java index 480b17c47d83..efc7a4b5375f 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java @@ -2615,7 +2615,7 @@ private boolean isAnnotatedForThisChecker(List annotations) { .equals("org.checkerframework.framework.qual.AnnotatedFor")) { AnnotationMirror af = getAnnotation(ae, allAnnotations); if (atypeFactory.areSameByClass(af, AnnotatedFor.class)) { - return atypeFactory.doesAnnotatedForApplyToThisChecker(af); + return atypeFactory.isAnnotatedForThisCheckerOrUpstreamChecker(af); } } } 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 cb28a2142a5e..2518e0df7c2b 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -534,6 +534,9 @@ void checkRep(String aliasName) { /** Mapping from an Element to the source Tree of the declaration. */ private final Map elementToTreeCache; + /** A mapping of Element → Whether or not that element is AnnotatedFor this type system. */ + private final IdentityHashMap elementAnnotatedFors = new IdentityHashMap<>(); + /** Mapping from a Tree to its TreePath. Shared between all instances. */ private final TreePathCacher treePathCache; @@ -6020,7 +6023,7 @@ protected void makeConditionConsistentWithOtherMethod( * @param annotatedForAnno an {@link AnnotatedFor} annotation * @return whether {@code annotatedForAnno} applies to this checker */ - public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForAnno) { + public boolean isAnnotatedForThisCheckerOrUpstreamChecker(AnnotationMirror annotatedForAnno) { List annotatedForCheckers = AnnotationUtils.getElementValueArray( annotatedForAnno, annotatedForValueElement, String.class); @@ -6035,6 +6038,53 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA return false; } + /** + * Return true if the element has an {@code @AnnotatedFor} annotation, for this checker or an + * upstream checker that called this one. + * + * @param elt the source code element to check, or null + * @return true if the element is annotated for this checker or an upstream checker + */ + public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(Element elt) { + boolean elementAnnotatedForThisChecker = false; + + if (elt == null) { + throw new BugInCF( + "Call of QualifierDefaults.isElementAnnotatedForThisChecker with null"); + } + + if (elementAnnotatedFors.containsKey(elt)) { + return elementAnnotatedFors.get(elt); + } + + AnnotationMirror annotatedFor = getDeclAnnotation(elt, AnnotatedFor.class); + + if (annotatedFor != null) { + elementAnnotatedForThisChecker = + isAnnotatedForThisCheckerOrUpstreamChecker(annotatedFor); + } + + if (!elementAnnotatedForThisChecker) { + Element parent; + if (elt.getKind() == ElementKind.PACKAGE) { + // TODO: should AnnotatedFor apply to subpackages?? + // elt.getEnclosingElement() on a package is null; therefore, + // use the dedicated method. + parent = ElementUtils.parentPackage((PackageElement) elt, elements); + } else { + parent = elt.getEnclosingElement(); + } + + if (parent != null && isElementAnnotatedForThisCheckerOrUpstreamChecker(parent)) { + elementAnnotatedForThisChecker = true; + } + } + + elementAnnotatedFors.put(elt, elementAnnotatedForThisChecker); + + return elementAnnotatedForThisChecker; + } + /** * Get the {@code expression} field/element of the given contract annotation. * diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java index 080d1cec1429..1439dd96eb16 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java +++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java @@ -14,7 +14,6 @@ import org.checkerframework.checker.interning.qual.FindDistinct; import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.DefaultQualifier; import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AnnotatedTypeFactory; @@ -121,9 +120,6 @@ public class QualifierDefaults { */ private final IdentityHashMap elementDefaults = new IdentityHashMap<>(); - /** A mapping of Element → Whether or not that element is AnnotatedFor this type system. */ - private final IdentityHashMap elementAnnotatedFors = new IdentityHashMap<>(); - /** CLIMB locations whose standard default is top for a given type system. */ public static final List STANDARD_CLIMB_DEFAULTS_TOP = Collections.unmodifiableList( @@ -642,46 +638,6 @@ private void applyDefaults(Tree tree, AnnotatedTypeMirror type) { } } - private boolean isElementAnnotatedForThisChecker(Element elt) { - boolean elementAnnotatedForThisChecker = false; - - if (elt == null) { - throw new BugInCF( - "Call of QualifierDefaults.isElementAnnotatedForThisChecker with null"); - } - - if (elementAnnotatedFors.containsKey(elt)) { - return elementAnnotatedFors.get(elt); - } - - AnnotationMirror annotatedFor = atypeFactory.getDeclAnnotation(elt, AnnotatedFor.class); - - if (annotatedFor != null) { - elementAnnotatedForThisChecker = - atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor); - } - - if (!elementAnnotatedForThisChecker) { - Element parent; - if (elt.getKind() == ElementKind.PACKAGE) { - // TODO: should AnnotatedFor apply to subpackages?? - // elt.getEnclosingElement() on a package is null; therefore, - // use the dedicated method. - parent = ElementUtils.parentPackage((PackageElement) elt, elements); - } else { - parent = elt.getEnclosingElement(); - } - - if (parent != null && isElementAnnotatedForThisChecker(parent)) { - elementAnnotatedForThisChecker = true; - } - } - - elementAnnotatedFors.put(elt, elementAnnotatedForThisChecker); - - return elementAnnotatedForThisChecker; - } - /** * Returns the defaults that apply to the given Element, considering defaults from enclosing * Elements. @@ -810,7 +766,8 @@ public boolean applyConservativeDefaults(Element annotationScope) { && !isFromStubFile; if (isBytecode) { return useConservativeDefaultsBytecode - && !isElementAnnotatedForThisChecker(annotationScope); + && !atypeFactory.isElementAnnotatedForThisCheckerOrUpstreamChecker( + annotationScope); } else if (isFromStubFile) { // TODO: Types in stub files not annotated for a particular checker should be // treated as unchecked bytecode. For now, all types in stub files are treated as @@ -819,7 +776,7 @@ public boolean applyConservativeDefaults(Element annotationScope) { // be treated like unchecked code except for methods in the scope of an @AnnotatedFor. return false; } else if (useConservativeDefaultsSource) { - return !isElementAnnotatedForThisChecker(annotationScope); + return !atypeFactory.isElementAnnotatedForThisCheckerOrUpstreamChecker(annotationScope); } return false; } From f71b68a3d53e974f89b953a1db224292cb09c001 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 09:21:13 -0700 Subject: [PATCH 05/12] Apply suggestions from code review Co-authored-by: Werner Dietl --- checker/tests/nullness-nullmarked/NullMarkedSuppressError.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java index 7ffb8bcb6e94..965eeeb60ce2 100644 --- a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java +++ b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java @@ -6,6 +6,7 @@ class A { } class B { + // No expected error, because code is not annotated for nullness. Object o = null; } } From d8f2cb22dbe925a4d29c8a53ae74eaf0a7fc4912 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 09:21:50 -0700 Subject: [PATCH 06/12] Fix TODO --- .../checker/test/junit/NullnessNullMarkedTest.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java index 74c790c9b427..d39785790cee 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessNullMarkedTest.java @@ -21,8 +21,7 @@ public NullnessNullMarkedTest(List testFiles) { testFiles, org.checkerframework.checker.nullness.NullnessChecker.class, "nullness", - // TODO: Replace this `-AonlyAnnotatedFor` flag after EISOP#1290 is merged. - "-AuseConservativeDefaultsForUncheckedCode=source"); + "-AonlyAnnotatedFor"); } @Parameters From 8b7e190f5bb9f62f050c693e47b21a4feb861d8b Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 09:37:38 -0700 Subject: [PATCH 07/12] Apply suggestions in the comment --- .../tests/nullness-nullmarked/NullMarkedSuppressError.java | 4 +++- .../org/checkerframework/common/basetype/BaseTypeChecker.java | 2 +- .../org/checkerframework/framework/source/SourceChecker.java | 4 ++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java index 965eeeb60ce2..70a80f5e3f64 100644 --- a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java +++ b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java @@ -1,5 +1,7 @@ +import org.jspecify.annotations.NullMarked; + public class NullMarkedSuppressError { - @org.jspecify.annotations.NullMarked + @NullMarked class A { // :: error: (assignment.type.incompatible) Object o = null; diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 129c45ee5716..fa0619621f29 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -328,7 +328,7 @@ public BaseTypeChecker getUltimateParentChecker() { */ @Override protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { - if (elt == null || !useConservativeDefault("source")) { + if (elt == null || (!useConservativeDefaultsSource && !onlyAnnotatedFor)) { return false; } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 06d51c49d06f..e5e97889c967 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -694,13 +694,13 @@ public abstract class SourceChecker extends AbstractTypeProcessor implements Opt private boolean warnUnneededSuppressions; /** True if the -AonlyAnnotatedFor command-line argument was passed. */ - private boolean onlyAnnotatedFor; + protected boolean onlyAnnotatedFor; /** * True if the -AuseConservativeDefaultsForUncheckedCode=source command-line argument was * passed. */ - private boolean useConservativeDefaultsSource; + protected boolean useConservativeDefaultsSource; /** * The full list of subcheckers that need to be run prior to this one, in the order they need to From a3bbf87fb225ecdcbc83685213e9de33de8c9bcb Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 19:50:27 -0700 Subject: [PATCH 08/12] Refactor --- .../framework/source/SourceChecker.java | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 06d51c49d06f..f2c1a4d82bae 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -2880,11 +2880,6 @@ public boolean shouldSuppressWarnings(@Nullable Element elt, String errKey) { return true; } } - if (isAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - // Return false immediately. Do NOT check for AnnotatedFor in the - // enclosing elements, because they may not have an @AnnotatedFor. - return false; - } } return false; } @@ -3017,15 +3012,6 @@ protected boolean messageKeyMatches( * @return true if the element is annotated for this checker or an upstream checker */ protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { - // Return false if elt is null, or if neither useConservativeDefaultsSource nor - // issueErrorsForOnlyAnnotatedForScope is set, since the @AnnotatedFor status is irrelevant - // in that case. - // TODO: Refactor SourceChecker and QualifierDefaults to use a cache for determining if an - // element is annotated for. - if (elt == null || (!useConservativeDefaultsSource && !onlyAnnotatedFor)) { - return false; - } - AnnotatedFor anno = elt.getAnnotation(AnnotatedFor.class); String[] userAnnotatedFors = (anno == null ? null : anno.value()); From 967b18d072c3a0b5e9ecc0ea6e227a78903a5cfd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 20:36:13 -0700 Subject: [PATCH 09/12] Refactor for better code --- .../common/basetype/BaseTypeChecker.java | 2 +- .../util/count/AnnotationStatistics.java | 7 +++++ .../common/util/count/JavaCodeStatistics.java | 7 +++++ .../common/util/debug/SignaturePrinter.java | 6 ++++ .../framework/source/AggregateChecker.java | 8 +++++ .../framework/source/SourceChecker.java | 30 ++++--------------- .../framework/type/AnnotatedTypeFactory.java | 2 +- 7 files changed, 36 insertions(+), 26 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 9d88fac577d6..cfe2f29adff2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -316,7 +316,7 @@ public BaseTypeChecker getUltimateParentChecker() { } @Override - protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { return getTypeFactory().isElementAnnotatedForThisCheckerOrUpstreamChecker(elt); } } diff --git a/framework/src/main/java/org/checkerframework/common/util/count/AnnotationStatistics.java b/framework/src/main/java/org/checkerframework/common/util/count/AnnotationStatistics.java index 5415660c9874..bead1be69157 100644 --- a/framework/src/main/java/org/checkerframework/common/util/count/AnnotationStatistics.java +++ b/framework/src/main/java/org/checkerframework/common/util/count/AnnotationStatistics.java @@ -19,6 +19,7 @@ import com.sun.tools.javac.tree.JCTree.JCAnnotation; import com.sun.tools.javac.util.Log; +import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.source.SourceVisitor; import org.checkerframework.framework.source.SupportedOptions; @@ -31,6 +32,7 @@ import javax.annotation.processing.SupportedSourceVersion; import javax.lang.model.SourceVersion; +import javax.lang.model.element.Element; import javax.lang.model.element.Name; import javax.tools.Diagnostic; @@ -326,4 +328,9 @@ public AnnotationProvider getAnnotationProvider() { throw new UnsupportedOperationException( "getAnnotationProvider is not implemented for this class."); } + + @Override + protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + return false; + } } diff --git a/framework/src/main/java/org/checkerframework/common/util/count/JavaCodeStatistics.java b/framework/src/main/java/org/checkerframework/common/util/count/JavaCodeStatistics.java index 5eed8083588b..c2b240a1640b 100644 --- a/framework/src/main/java/org/checkerframework/common/util/count/JavaCodeStatistics.java +++ b/framework/src/main/java/org/checkerframework/common/util/count/JavaCodeStatistics.java @@ -13,6 +13,7 @@ import com.sun.source.tree.TypeCastTree; import com.sun.tools.javac.util.Log; +import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.source.SourceVisitor; import org.checkerframework.javacutil.AnnotationProvider; @@ -24,6 +25,7 @@ import javax.annotation.processing.SupportedSourceVersion; import javax.lang.model.SourceVersion; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; /** @@ -203,4 +205,9 @@ public AnnotationProvider getAnnotationProvider() { throw new UnsupportedOperationException( "getAnnotationProvider is not implemented for this class."); } + + @Override + protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + return false; + } } diff --git a/framework/src/main/java/org/checkerframework/common/util/debug/SignaturePrinter.java b/framework/src/main/java/org/checkerframework/common/util/debug/SignaturePrinter.java index e27de1e8b599..fe7e3b7c8608 100644 --- a/framework/src/main/java/org/checkerframework/common/util/debug/SignaturePrinter.java +++ b/framework/src/main/java/org/checkerframework/common/util/debug/SignaturePrinter.java @@ -100,6 +100,12 @@ private void init(ProcessingEnvironment env, @Nullable @BinaryName String checke checker = new SourceChecker() { + @Override + protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker( + @Nullable Element elt) { + return false; + } + @Override protected SourceVisitor createSourceVisitor() { return null; diff --git a/framework/src/main/java/org/checkerframework/framework/source/AggregateChecker.java b/framework/src/main/java/org/checkerframework/framework/source/AggregateChecker.java index 727e2b8f6d6c..f6cee1ad5f77 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/AggregateChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/AggregateChecker.java @@ -3,10 +3,13 @@ import com.sun.source.tree.CompilationUnitTree; import com.sun.source.tree.Tree; +import org.checkerframework.checker.nullness.qual.Nullable; + import java.util.Collection; import java.util.LinkedHashSet; import java.util.Set; +import javax.lang.model.element.Element; import javax.tools.Diagnostic; /** @@ -52,4 +55,9 @@ protected final Set> getImmediateSubcheckerClasse // the checkers in the aggregate checker do. }; } + + @Override + protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { + return false; + } } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index f2c1a4d82bae..9871d2089220 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -32,9 +32,7 @@ import org.checkerframework.checker.signature.qual.FullyQualifiedName; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.reflection.MethodValChecker; -import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.util.CheckerMain; import org.checkerframework.framework.util.OptionConfiguration; import org.checkerframework.framework.util.TreePathCacher; import org.checkerframework.javacutil.AbstractTypeProcessor; @@ -153,7 +151,7 @@ // only issue errors for code inside the scope of `@NullMarked` annotations. // See // https://github.com/uber/NullAway/wiki/Configuration#only-nullmarked-version-0123-and-after. - // org.checkerframework.framework.source.SourceChecker.isAnnotatedForThisCheckerOrUpstreamChecker + // org.checkerframework.framework.source.SourceChecker.isElementAnnotatedForThisCheckerOrUpstreamChecker "onlyAnnotatedFor", // Unsoundly assume all methods have no side effects, are deterministic, or both. @@ -2778,7 +2776,7 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(elt)) { + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { // Return false immediately. Do NOT check for AnnotatedFor in the enclosing // elements as the closest AnnotatedFor is already found. return false; @@ -2790,7 +2788,7 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(elt)) { + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { // Return false immediately. Do NOT check for AnnotatedFor in the enclosing // elements as the closest AnnotatedFor is already found. return false; @@ -2800,7 +2798,7 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { if (shouldSuppressWarnings(packageElement, errKey)) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { // Return false immediately. Do NOT check for AnnotatedFor in the enclosing // elements as the closest AnnotatedFor is already found. return false; @@ -3011,24 +3009,8 @@ protected boolean messageKeyMatches( * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker */ - protected boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { - AnnotatedFor anno = elt.getAnnotation(AnnotatedFor.class); - - String[] userAnnotatedFors = (anno == null ? null : anno.value()); - - if (userAnnotatedFors != null) { - List<@FullyQualifiedName String> upstreamCheckerNames = getUpstreamCheckerNames(); - - for (String userAnnotatedFor : userAnnotatedFors) { - if (CheckerMain.matchesCheckerOrSubcheckerFromList( - userAnnotatedFor, upstreamCheckerNames)) { - return true; - } - } - } - - return false; - } + protected abstract boolean isElementAnnotatedForThisCheckerOrUpstreamChecker( + @Nullable Element elt); /** * Returns a modifiable set of lower-case strings that are prefixes for SuppressWarnings 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 2518e0df7c2b..260f12da02e5 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -6045,7 +6045,7 @@ public boolean isAnnotatedForThisCheckerOrUpstreamChecker(AnnotationMirror annot * @param elt the source code element to check, or null * @return true if the element is annotated for this checker or an upstream checker */ - public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(Element elt) { + public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { boolean elementAnnotatedForThisChecker = false; if (elt == null) { From 487025f14992c15b522c7000642a55be3095e441 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 25 Aug 2025 21:56:22 -0700 Subject: [PATCH 10/12] Remove comments that are no longer true --- .../checkerframework/framework/source/SourceChecker.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 9871d2089220..7c735eff4469 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -2777,8 +2777,6 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { } if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. return false; } } else if (TreeUtils.classTreeKinds().contains(decl.getKind())) { @@ -2789,8 +2787,6 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { } if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. return false; } Element packageElement = elt.getEnclosingElement(); @@ -2798,9 +2794,8 @@ public boolean shouldSuppressWarnings(@Nullable TreePath path, String errKey) { if (shouldSuppressWarnings(packageElement, errKey)) { return true; } + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. return false; } } From c9cd722ceca6fa02e8e9c6bf6f2d794a64e998e0 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 27 Aug 2025 22:49:04 -0700 Subject: [PATCH 11/12] Revert --- .../org/checkerframework/common/basetype/BaseTypeChecker.java | 2 -- .../org/checkerframework/framework/source/SourceChecker.java | 4 ++-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 613da30be042..cfe2f29adff2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -4,7 +4,6 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.signature.qual.ClassGetName; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; -import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; @@ -316,7 +315,6 @@ public BaseTypeChecker getUltimateParentChecker() { } } - @Override protected boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt) { return getTypeFactory().isElementAnnotatedForThisCheckerOrUpstreamChecker(elt); diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 408bb21faac5..7c735eff4469 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -692,13 +692,13 @@ public abstract class SourceChecker extends AbstractTypeProcessor implements Opt private boolean warnUnneededSuppressions; /** True if the -AonlyAnnotatedFor command-line argument was passed. */ - protected boolean onlyAnnotatedFor; + private boolean onlyAnnotatedFor; /** * True if the -AuseConservativeDefaultsForUncheckedCode=source command-line argument was * passed. */ - protected boolean useConservativeDefaultsSource; + private boolean useConservativeDefaultsSource; /** * The full list of subcheckers that need to be run prior to this one, in the order they need to From dd1976dc5583409ff17881d9749ad569e386c695 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 3 Sep 2025 22:18:26 -0700 Subject: [PATCH 12/12] Changelog --- docs/CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index afad2ac0f46b..9c9f29934eb5 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,8 @@ Version 3.49.5-eisop1 (July ??, 2025) **User-visible changes:** +Support the JSpecify `@NullMarked` annotation as an alias to `@AnnotatedFor("nullness")`. + The new command-line option `-AonlyAnnotatedFor` suppresses all type-checking errors and warnings outside the scope of a corresponding `@AnnotatedFor` annotation. Note that the `@AnnotatedFor` annotation must include the checker's name to enable warnings from that checker.