diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java new file mode 100644 index 000000000000..0a87d8937406 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java @@ -0,0 +1,39 @@ +package org.checkerframework.framework.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Indicates that this class has not been annotated for the given type system, even though an + * enclosing element is annotated for it. For example, if a package is + * {@code @AnnotatedFor("nullness")} but one of its classes has not been annotated with + * {@code @Nullable} and friends, mark that class {@code @UnannotatedFor("nullness")}. The argument + * to {@code UnannotatedFor} is not an annotation name, but a checker name. + * + *

This annotation has no effect unless the {@code + * -AuseConservativeDefaultsForUncheckedCode=source} command-line argument is supplied. It only + * subtracts from the scope of an enclosing {@link AnnotatedFor}: an element in its scope is + * defaulted using conservative defaults and its warnings are suppressed, as if no enclosing + * {@code @AnnotatedFor} were present. An {@code @AnnotatedFor} on a nested element takes effect + * again for that element. + * + * @checker_framework.manual #compiling-libraries Compiling partially-annotated libraries + */ +@Documented +@Retention(RetentionPolicy.SOURCE) +@Target({ElementType.TYPE, ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.PACKAGE}) +public @interface UnannotatedFor { + /** + * Returns the type systems for which the class has not been annotated. Legal arguments are any + * string that may be passed to the {@code -processor} command-line argument: the + * fully-qualified class name for the checker, or a shorthand for built-in checkers. Using the + * annotation with no arguments, as in {@code @UnannotatedFor({})}, has no effect. + * + * @return the type systems for which the class has not been annotated + * @checker_framework.manual #shorthand-for-checkers Short names for built-in checkers + */ + String[] value(); +} diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java new file mode 100644 index 000000000000..349d36de2a2f --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java @@ -0,0 +1,34 @@ +package org.checkerframework.checker.test.junit; + +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +import java.io.File; +import java.util.List; + +/** JUnit tests for the Nullness checker. */ +public class NullnessUnannotatedForTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create a NullnessNullMarkedTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public NullnessUnannotatedForTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.nullness.NullnessChecker.class, + "nullness", + "-AuseConservativeDefaultsForUncheckedCode=source"); + } + + /** + * This method returns the directory containing test code. + * + * @return the directories containing test code + */ + @Parameters + public static String[] getTestDirs() { + return new String[] {"nullness-unannotatedfor"}; + } +} diff --git a/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java new file mode 100644 index 000000000000..9bdac0219f37 --- /dev/null +++ b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java @@ -0,0 +1,57 @@ +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.framework.qual.AnnotatedFor; +import org.checkerframework.framework.qual.UnannotatedFor; + +public class NullnessUnannotatedForTest { + @AnnotatedFor("nullness") + class A { + // :: error: (assignment.type.incompatible) + Object o = null; + } + + @AnnotatedFor("nullness") + class B { + @UnannotatedFor("nullness") + void method(@Nullable Object o) { + o.toString(); + } + } + + @AnnotatedFor("nullness") + class Lambdas { + // A lambda body is in the scope of the @UnannotatedFor method that contains it, even + // though a lambda is not itself a declaration. + @UnannotatedFor("nullness") + Runnable excluded(@Nullable Object o) { + return () -> o.toString(); + } + + Runnable included(@Nullable Object o) { + // :: error: (dereference.of.nullable) + return () -> o.toString(); + } + } + + @AnnotatedFor("nullness") + class C { + // @UnannotatedFor only subtracts from the enclosing scope, so a nested @AnnotatedFor takes + // effect again. + @UnannotatedFor("nullness") + class Excluded { + Object unannotated = null; + + @AnnotatedFor("nullness") + void reannotated(@Nullable Object o) { + // :: error: (dereference.of.nullable) + o.toString(); + } + } + + // An @UnannotatedFor for a different checker does not exclude this class. + @UnannotatedFor("regex") + class UnannotatedForOtherChecker { + // :: error: (assignment.type.incompatible) + Object o = null; + } + } +} diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java new file mode 100644 index 000000000000..210fbb470aca --- /dev/null +++ b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java @@ -0,0 +1,12 @@ +package packageunannotatedfornullness; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.framework.qual.UnannotatedFor; + +@UnannotatedFor("nullness") +public class Excluded { + void foo(@Nullable Object o) { + // No error: @UnannotatedFor excludes this class from the package's @AnnotatedFor scope. + o.toString(); + } +} diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java new file mode 100644 index 000000000000..7d80b73b621c --- /dev/null +++ b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java @@ -0,0 +1,10 @@ +package packageunannotatedfornullness; + +import org.checkerframework.checker.nullness.qual.Nullable; + +public class Included { + void foo(@Nullable Object o) { + // :: error: (dereference.of.nullable) + o.toString(); + } +} diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java new file mode 100644 index 000000000000..3ea907dc08b6 --- /dev/null +++ b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java @@ -0,0 +1,4 @@ +@AnnotatedFor("nullness") +package packageunannotatedfornullness; + +import org.checkerframework.framework.qual.AnnotatedFor; diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 63142b582161..7de904121552 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,13 @@ Version 3.49.5-eisop2 (June ?, 2026) **User-visible changes:** +New declaration annotation `@UnannotatedFor`, which excludes a package, class, method, or +constructor from the scope of an enclosing `@AnnotatedFor` for the given checkers. Its scope is +defaulted using conservative defaults and its warnings are suppressed, as if no enclosing +`@AnnotatedFor` were present; a nested `@AnnotatedFor` takes effect again. Like `@AnnotatedFor`, +it has no effect unless `-AuseConservativeDefaultsForUncheckedCode=source` or `-AonlyAnnotatedFor` +is supplied. + The Checker Framework now issues an `annotation.on.supertype` error when an annotation supported by the checker is written as a main annotation on the superclass or interface in an `extends` or `implements` clause. Annotations on the supertype's type arguments remain permitted. A checker diff --git a/docs/manual/annotating-libraries.tex b/docs/manual/annotating-libraries.tex index b6ce89dc8fd8..acce944cf7d6 100644 --- a/docs/manual/annotating-libraries.tex +++ b/docs/manual/annotating-libraries.tex @@ -436,6 +436,16 @@ any annotations, but that you examined the source code and verified that all appropriate annotations are present. +The \refqualclass{framework/qual}{UnannotatedFor} annotation is the inverse: +it excludes a package, class, method, or constructor from the scope of an +enclosing \<@AnnotatedFor>. For example, if a package is +\<@AnnotatedFor("nullness")> but one class in it has not been annotated, write +\<@UnannotatedFor("nullness")> on that class; it is then treated as unchecked +code, exactly as if the package had no \<@AnnotatedFor>. An \<@AnnotatedFor> +on a nested element takes effect again for that element. +\refqualclass{framework/qual}{UnannotatedFor}'s arguments are checker names, +in the same format as \refqualclass{framework/qual}{AnnotatedFor}'s. + \begin{sloppypar} Whenever you compile a class using the Checker Framework, including when using the \<-AuseConservativeDefaultsForUncheckedCode=source,bytecode> command-line 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 ae058151e952..79d94c089ebd 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -6,6 +6,7 @@ import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.SubtypeOf; +import org.checkerframework.framework.qual.UnannotatedFor; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; @@ -76,7 +77,8 @@ public abstract class BaseTypeChecker extends SourceChecker { /** * A mapping from an element to whether it is in an {@code @AnnotatedFor} scope for this checker - * or an upstream checker. + * or an upstream checker. The value is the fully-resolved answer for the element: it accounts + * for enclosing elements and for {@code @UnannotatedFor} exclusions. */ private final IdentityHashMap elementAnnotatedForThisCheckerOrUpstreamCache = new IdentityHashMap<>(); @@ -344,7 +346,10 @@ public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Eleme annotatedFor != null && atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor); - if (!elementAnnotatedForThisChecker) { + // @UnannotatedFor only subtracts from an enclosing @AnnotatedFor scope, so consult it only + // when this element is not itself annotated for this checker, and let it stop the walk to + // the enclosing element. + if (!elementAnnotatedForThisChecker && !isElementUnannotatedForThisChecker(elt)) { Element parent; if (elt.getKind() == ElementKind.PACKAGE) { parent = @@ -362,4 +367,19 @@ public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Eleme elementAnnotatedForThisCheckerOrUpstreamCache.put(elt, elementAnnotatedForThisChecker); return elementAnnotatedForThisChecker; } + + /** + * Is {@code elt} annotated with an {@code @UnannotatedFor} that applies to this checker or an + * upstream checker? Unlike {@link #isElementAnnotatedForThisCheckerOrUpstreamChecker}, this + * does not consider enclosing elements. + * + * @param elt the element to check + * @return true if {@code elt} is excluded from an enclosing {@code @AnnotatedFor} scope + */ + private boolean isElementUnannotatedForThisChecker(Element elt) { + AnnotatedTypeFactory atypeFactory = getTypeFactory(); + AnnotationMirror unannotatedFor = atypeFactory.getDeclAnnotation(elt, UnannotatedFor.class); + return unannotatedFor != null + && atypeFactory.doesUnannotatedForApplyToThisChecker(unannotatedFor); + } } 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 b28eae57f77a..d8163658f40b 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -2841,7 +2841,9 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) { return true; } - boolean foundAnnotatedFor = false; + // The innermost declaration enclosing path. The @AnnotatedFor scope question is asked + // about it once, after the loop. + Element innermostDecl = null; // iterate through the path; continue until path contains no declarations for (TreePath declPath = TreePathUtil.enclosingDeclarationPath(path); @@ -2849,46 +2851,37 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) { declPath = TreePathUtil.enclosingDeclarationPath(declPath.getParentPath())) { Tree decl = declPath.getLeaf(); + Element elt; if (decl instanceof VariableTree) { - Element elt = TreeUtils.elementFromDeclaration((VariableTree) decl); - if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) { - return true; - } + elt = TreeUtils.elementFromDeclaration((VariableTree) decl); } else if (decl instanceof MethodTree) { - Element elt = TreeUtils.elementFromDeclaration((MethodTree) decl); - if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) { - return true; - } - - if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - foundAnnotatedFor = true; - } + elt = TreeUtils.elementFromDeclaration((MethodTree) decl); } else if (TreeUtils.classTreeKinds().contains(decl.getKind())) { - // A class tree - Element elt = TreeUtils.elementFromDeclaration((ClassTree) decl); - if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) { - return true; - } - - if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { - foundAnnotatedFor = true; - } - Element packageElement = elt.getEnclosingElement(); - if (packageElement != null && packageElement.getKind() == ElementKind.PACKAGE) { - if (hasSuppressWarningsAnnotationForErrorKey(packageElement, errKey)) { - return true; - } - if (!foundAnnotatedFor - && isElementAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) { - foundAnnotatedFor = true; - } - } + elt = TreeUtils.elementFromDeclaration((ClassTree) decl); } else { throw new BugInCF("Unexpected declaration kind: " + decl.getKind() + " " + decl); } + + if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) { + return true; + } + if (innermostDecl == null) { + innermostDecl = elt; + } + + Element packageElement = elt.getEnclosingElement(); + if (packageElement != null + && packageElement.getKind() == ElementKind.PACKAGE + && hasSuppressWarningsAnnotationForErrorKey(packageElement, errKey)) { + return true; + } } - if (foundAnnotatedFor) { + // Ask only about the innermost declaration: + // isElementAnnotatedForThisCheckerOrUpstreamChecker already resolves the enclosing scope, + // and asking about an enclosing element separately would ignore an @UnannotatedFor that + // excludes the innermost declaration from that scope. + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(innermostDecl)) { return false; } else if (useConservativeDefaultsSource || onlyAnnotatedFor) { // If we got this far without hitting an @AnnotatedFor and returning @@ -2955,17 +2948,16 @@ public boolean shouldSuppressWarnings(Element elt, String errKey) { return true; } - boolean foundAnnotatedFor = false; for (Element currElt = elt; currElt != null; currElt = currElt.getEnclosingElement()) { if (hasSuppressWarningsAnnotationForErrorKey(currElt, errKey)) { return true; } - if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(currElt)) { - foundAnnotatedFor = true; - } } - if (foundAnnotatedFor) { + // Ask only about elt: isElementAnnotatedForThisCheckerOrUpstreamChecker already resolves + // the enclosing scope, and asking about an enclosing element separately would ignore an + // @UnannotatedFor that excludes elt from that scope. + if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) { return false; } else if (useConservativeDefaultsSource || onlyAnnotatedFor) { // If we got this far without hitting an @AnnotatedFor and returning 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 92992a67cd0d..ed0e5bc2c653 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -55,6 +55,7 @@ import org.checkerframework.framework.qual.InheritedAnnotation; import org.checkerframework.framework.qual.NoQualifierParameter; import org.checkerframework.framework.qual.RequiresQualifier; +import org.checkerframework.framework.qual.UnannotatedFor; import org.checkerframework.framework.stub.AnnotationFileElementTypes; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -206,6 +207,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider { /** The AnnotatedFor.value argument/element. */ protected final ExecutableElement annotatedForValueElement; + /** The UnannotatedFor.value argument/element. */ + protected final ExecutableElement unannotatedForValueElement; + /** The EnsuresQualifier.expression field/element. */ protected final ExecutableElement ensuresQualifierExpressionElement; @@ -800,6 +804,8 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { annotatedForValueElement = TreeUtils.getMethod(AnnotatedFor.class, "value", 0, processingEnv); + unannotatedForValueElement = + TreeUtils.getMethod(UnannotatedFor.class, "value", 0, processingEnv); ensuresQualifierExpressionElement = TreeUtils.getMethod(EnsuresQualifier.class, "expression", 0, processingEnv); ensuresQualifierListValueElement = @@ -6874,6 +6880,28 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA return false; } + /** + * Does {@code unannotatedForAnno}, which is an {@link UnannotatedFor} annotation, apply to this + * checker? + * + * @param unannotatedForAnno an {@link UnannotatedFor} annotation + * @return whether {@code unannotatedForAnno} applies to this checker + */ + public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedForAnno) { + List unannotatedForCheckers = + AnnotationUtils.getElementValueArray( + unannotatedForAnno, unannotatedForValueElement, String.class); + List<@FullyQualifiedName String> upstreamCheckerNames = checker.getUpstreamCheckerNames(); + for (String unannoForChecker : unannotatedForCheckers) { + if (upstreamCheckerNames.contains(unannoForChecker) + || CheckerMain.matchesFullyQualifiedProcessor( + unannoForChecker, upstreamCheckerNames, true)) { + return true; + } + } + return false; + } + /** * Get the {@code expression} field/element of the given contract annotation. *