JSpecify - eisop nullness checker

checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java

@@ -0,0 +1,27 @@
+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 and this annotation is
+ * used to exclude package, class or method which already in {@code @Annotatedfor} scope. In the
+ * scope of {@code UnannotatedFor}, the source code and bytecode should use conservative default if
+ * the command-line argument {@code -AuseConservativeDefaultsForUncheckedCode=source} is supplied
+ * while other package, class or method in {@code @Annotatedfor} scope is defaulted normally
+ * (typically using the CLIMB-to-top rule).
+ *
+ * <p>For example, mark a package as @Annotatedfor("nullness") will indicate that the package has
+ * been annotated with nullness annotation but some classes or methods in the package is not
+ * annotated, then mark the class or method with @UnannotatedFor("nullness") to exclude them from
+ * the scope of @Annotatedfor("nullness").
+ */
+@Documented
+@Retention(RetentionPolicy.SOURCE)
+@Target({ElementType.TYPE, ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.PACKAGE})
+public @interface UnannotatedFor {
+    String[] value();
+}

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java

@@ -32,8 +32,10 @@
 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.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFormatter;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -393,10 +395,26 @@ public NullnessNoInitAnnotatedTypeFactory(BaseTypeChecker checker) {
                                     new TypeUseLocation[] {TypeUseLocation.UPPER_BOUND})
                             .setValue("applyToSubpackages", false)
                             .build();
+            AnnotationMirror annotatedForNullness =
+                    new AnnotationBuilder(processingEnv, AnnotatedFor.class)
+                            .setValue("value", new String[] {"nullness"})
+                            .build();
+            AnnotationMirror unannotatedForNullness =
+                    new AnnotationBuilder(processingEnv, UnannotatedFor.class)
+                            .setValue("value", new String[] {"nullness"})
+                            .build();
             addAliasedDeclAnnotation(
                     "org.jspecify.annotations.NullMarked",
                     DefaultQualifier.class.getCanonicalName(),
                     nullMarkedDefaultQual);
+            addAliasedDeclAnnotation(
+                    "org.jspecify.annotations.NullMarked",
+                    AnnotatedFor.class.getCanonicalName(),
+                    annotatedForNullness);
+            addAliasedDeclAnnotation(
+                    "org.jspecify.annotations.NullUnmarked",
+                    UnannotatedFor.class.getCanonicalName(),
+                    unannotatedForNullness);
 
             // 2022-11-17: Deprecated old package location, remove after some grace period
             addAliasedDeclAnnotation(

docs/CHANGELOG.md

@@ -3,6 +3,8 @@ Version 3.42.0-eisop5 (July ?, 2024)
 
 **User-visible changes:**
 
+The new command-line argument '-AnoBytecodeStorage' allows the option to not store defaulted annotations in bytecode.
+
 Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1.
 Use `-ApermitMissingJdk` instead.
 

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -187,6 +187,10 @@
     // org.checkerframework.framework.source.SourceChecker.useConservativeDefault
     "useConservativeDefaultsForUncheckedCode",
 
+    // Whether to store defaulted annotations in bytecode.
+    // org.checkerframework.framework.type.AnnotatedTypeFactory.postProcessClassTree
+    "noBytecodeStorage",
+
     // Whether to assume sound concurrent semantics or
     // simplified sequential semantics
     // org.checkerframework.framework.flow.CFAbstractTransfer.sequentialSemantics

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -52,6 +52,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.source.SourceChecker;
 import org.checkerframework.framework.stub.AnnotationFileElementTypes;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
@@ -203,6 +204,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;
 
@@ -708,6 +712,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 =
@@ -1528,6 +1534,10 @@ public void preProcessClassTree(ClassTree classTree) {}
      * to override this method if storing defaulted types is not desirable.
      */
     public void postProcessClassTree(ClassTree tree) {
+        if (!checker.hasOption("noBytecodeStorage")) {
+            TypesIntoElements.store(processingEnv, this, tree);
+            DeclarationsIntoElements.store(processingEnv, this, tree);
+        }
         TypesIntoElements.store(processingEnv, this, tree);
         DeclarationsIntoElements.store(processingEnv, this, tree);
 
@@ -6018,6 +6028,27 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA
         return false;
     }
 
+    /**
+     * Does {@code anno}, which is an {@link org.checkerframework.framework.qual.UnannotatedFor}
+     * annotation, apply to this checker?
+     *
+     * @param unannotatedForAnno an {@link UnannotatedFor} annotation
+     * @return whether {@code anno} applies to this checker
+     */
+    public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedForAnno) {
+        List<String> unannotatedForCheckers =
+                AnnotationUtils.getElementValueArray(
+                        unannotatedForAnno, unannotatedForValueElement, String.class);
+        for (String unannoForChecker : unannotatedForCheckers) {
+            if (checker.getUpstreamCheckerNames().contains(unannoForChecker)
+                    || CheckerMain.matchesFullyQualifiedProcessor(
+                            unannoForChecker, checker.getUpstreamCheckerNames(), true)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
     /**
      * Get the {@code expression} field/element of the given contract annotation.
      *

framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java

@@ -16,6 +16,7 @@
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.DefaultQualifier;
 import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
@@ -123,6 +124,12 @@ public class QualifierDefaults {
     /** A mapping of Element → Whether or not that element is AnnotatedFor this type system. */
     private final IdentityHashMap<Element, Boolean> elementAnnotatedFors = new IdentityHashMap<>();
 
+    /**
+     * A mapping of Element &rarr; Whether or not that element is UnannotatedFor this type system.
+     */
+    private final IdentityHashMap<Element, Boolean> elementUnannotatedFors =
+            new IdentityHashMap<>();
+
     /** CLIMB locations whose standard default is top for a given type system. */
     public static final List<TypeUseLocation> STANDARD_CLIMB_DEFAULTS_TOP =
             Collections.unmodifiableList(
@@ -660,12 +667,13 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
                     atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor);
         }
 
+        // If the element is not Annotatedfor this checker, check if the parent is.
         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.
+                // elt.getEnclosingElement() on a package is null if module does not exist;
+                // therefore, use the dedicated method.
                 parent = ElementUtils.parentPackage((PackageElement) elt, elements);
             } else {
                 parent = elt.getEnclosingElement();
@@ -681,6 +689,51 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
         return elementAnnotatedForThisChecker;
     }
 
+    /**
+     * Returns whether the element is UnannotatedFor this checker.
+     *
+     * @param elt the element
+     * @return whether the element is UnannotatedFor this checker
+     */
+    private boolean isElementUnannotatedForThisChecker(Element elt) {
+        boolean elementUnannotatedForThisChecker = false;
+
+        if (elt == null) {
+            throw new BugInCF(
+                    "Call of QualifierDefaults.isElementUnannotatedForThisChecker with null");
+        }
+
+        if (elementUnannotatedFors.containsKey(elt)) {
+            return elementUnannotatedFors.get(elt);
+        }
+
+        AnnotationMirror UnannotatedFor = atypeFactory.getDeclAnnotation(elt, UnannotatedFor.class);
+
+        if (UnannotatedFor != null) {
+            elementUnannotatedForThisChecker =
+                    atypeFactory.doesUnannotatedForApplyToThisChecker(UnannotatedFor);
+        }
+
+        if (!elementUnannotatedForThisChecker) {
+            Element parent;
+            if (elt.getKind() == ElementKind.PACKAGE) {
+                // elt.getEnclosingElement() on a package is null if module does not exist;
+                // therefore, use the dedicated method.
+                parent = ElementUtils.parentPackage((PackageElement) elt, elements);
+            } else {
+                parent = elt.getEnclosingElement();
+            }
+
+            if (parent != null && isElementUnannotatedForThisChecker(parent)) {
+                elementUnannotatedForThisChecker = true;
+            }
+        }
+
+        elementUnannotatedFors.put(elt, elementUnannotatedForThisChecker);
+
+        return elementUnannotatedForThisChecker;
+    }
+
     /**
      * Returns the defaults that apply to the given Element, considering defaults from enclosing
      * Elements.
@@ -809,7 +862,8 @@ public boolean applyConservativeDefaults(Element annotationScope) {
                         && !isFromStubFile;
         if (isBytecode) {
             return useConservativeDefaultsBytecode
-                    && !isElementAnnotatedForThisChecker(annotationScope);
+                    && (!isElementAnnotatedForThisChecker(annotationScope)
+                            || isElementUnannotatedForThisChecker(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
@@ -818,7 +872,8 @@ 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 !isElementAnnotatedForThisChecker(annotationScope)
+                    || isElementUnannotatedForThisChecker(annotationScope);
         }
         return false;
     }