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 b9eac4414083..a970adcf6a1b 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; @@ -417,6 +418,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/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..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 @@ -17,7 +17,11 @@ 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", + "-AonlyAnnotatedFor"); } @Parameters diff --git a/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java new file mode 100644 index 000000000000..70a80f5e3f64 --- /dev/null +++ b/checker/tests/nullness-nullmarked/NullMarkedSuppressError.java @@ -0,0 +1,14 @@ +import org.jspecify.annotations.NullMarked; + +public class NullMarkedSuppressError { + @NullMarked + class A { + // :: error: (assignment.type.incompatible) + Object o = null; + } + + class B { + // No expected error, because code is not annotated for nullness. + Object o = null; + } +} diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index d5f4d358af06..762283a8484e 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,8 @@ Version 3.49.5-eisop2 (May ?, 2026) **User-visible changes:** +Support the JSpecify `@NullMarked` annotation as an alias to `@AnnotatedFor("nullness")`. + **Implementation details:** Fixed a bug that caused an IndexOutOfBoundsException for lambdas in varargs, 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..cfe2f29adff2 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 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 427737914e76..462df32a3645 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 076ccaaed36b..43bb4d74460a 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -31,9 +31,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; @@ -152,7 +150,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. @@ -2790,9 +2788,7 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { return false; } } else if (TreeUtils.classTreeKinds().contains(decl.getKind())) { @@ -2802,9 +2798,7 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { return false; } Element packageElement = elt.getEnclosingElement(); @@ -2812,9 +2806,8 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) { if (shouldSuppressWarnings(packageElement, errKey)) { return true; } - if (isAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { - // Return false immediately. Do NOT check for AnnotatedFor in the enclosing - // elements as the closest AnnotatedFor is already found. + + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { return false; } } @@ -2892,11 +2885,6 @@ public boolean shouldSuppressWarnings(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; } @@ -3028,33 +3016,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 */ - private 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()); - - 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/stub/AnnotationFileParser.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java index 8d267fbe95cf..d5cf4c5e3bc5 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java @@ -2634,7 +2634,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 b3d529c0d499..e0235c8dacb5 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -533,6 +533,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; @@ -6055,7 +6058,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); @@ -6070,6 +6073,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(@Nullable 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 603ca75118fd..2454c675f212 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; @@ -116,9 +115,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( @@ -812,7 +808,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 @@ -821,7 +818,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; }