Merge branch 'master' into type-use-location-nested-class

.github/workflows/continuous-integration.yml

@@ -25,13 +25,13 @@ jobs:
             epVersion: 2.31.0
           - os: macos-latest
             java: 17
-            epVersion: 2.32.0
+            epVersion: 2.33.0
           - os: windows-latest
             java: 17
-            epVersion: 2.32.0
+            epVersion: 2.33.0
           - os: ubuntu-latest
             java: 17
-            epVersion: 2.32.0
+            epVersion: 2.33.0
       fail-fast: false
     runs-on: ${{ matrix.os }}
     steps:
@@ -60,7 +60,7 @@ jobs:
           ORG_GRADLE_PROJECT_epApiVersion: ${{ matrix.epVersion }}
         run: ./gradlew codeCoverageReport
         continue-on-error: true
-        if: runner.os == 'Linux' && matrix.java == '17' && matrix.epVersion == '2.32.0' && github.repository == 'uber/NullAway'
+        if: runner.os == 'Linux' && matrix.java == '17' && matrix.epVersion == '2.33.0' && github.repository == 'uber/NullAway'
       - name: Upload coverage reports to Codecov
         uses: codecov/codecov-action@v4
         with:

annotations/src/main/java/com/uber/nullaway/annotations/EnsuresNonNullIf.java

@@ -0,0 +1,54 @@
+package com.uber.nullaway.annotations;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * An annotation describing a nullability post-condition for an instance method. Each parameter to
+ * the annotation should be a field of the enclosing class. The method must ensure that the method
+ * returns true in case the fields are non-null. The method can also return false in case the fields
+ * are non-null (inverse logic), and in such case, you must set {@code result} to false. NullAway
+ * verifies that the property holds.
+ *
+ * <p>Here is an example:
+ *
+ * <pre>
+ * class Foo {
+ *     {@literal @}Nullable Object theField;
+ *
+ *     {@literal @}EnsuresNonNullIf("theField", result=true) // "this.theField" is also valid
+ *     boolean hasTheField() {
+ *         return theField != null;
+ *     }
+ *
+ *     void bar() {
+ *         if(!hasTheField()) {
+ *             return;
+ *         }
+ *
+ *         // No error, NullAway knows theField is non-null after call to hasTheField()
+ *         theField.toString();
+ *     }
+ * }
+ * </pre>
+ */
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.METHOD})
+public @interface EnsuresNonNullIf {
+  /**
+   * The list of fields that are non-null after the method returns the given result.
+   *
+   * @return The list of field names
+   */
+  String[] value();
+
+  /**
+   * The return value of the method under which the postcondition holds. The default is set to true,
+   * which means the method should return true in case fields are non-null.
+   *
+   * @return true or false
+   */
+  boolean result() default true;
+}

build.gradle

@@ -112,7 +112,7 @@ subprojects { project ->
         project.apply plugin: "com.diffplug.spotless"
         spotless {
             java {
-                googleJavaFormat()
+                googleJavaFormat(deps.versions.googlejavaformat)
             }
         }
     }
@@ -129,7 +129,7 @@ spotless {
     }
 }
 spotlessPredeclare {
-    java { googleJavaFormat('1.19.2') }
+    java { googleJavaFormat(deps.versions.googlejavaformat) }
     groovyGradle {
         greclipse()
     }

gradle/dependencies.gradle

@@ -19,7 +19,7 @@ import org.gradle.util.VersionNumber
 // The oldest version of Error Prone that we support running on
 def oldestErrorProneVersion = "2.14.0"
 // Latest released Error Prone version that we've tested with
-def latestErrorProneVersion = "2.32.0"
+def latestErrorProneVersion = "2.33.0"
 // Default to using latest tested Error Prone version
 def defaultErrorProneVersion =  latestErrorProneVersion
 def errorProneVersionToCompileAgainst = defaultErrorProneVersion
@@ -40,7 +40,7 @@ if (project.hasProperty("epApiVersion")) {
 
 def versions = [
     asm                    : "9.3",
-    checkerFramework       : "3.43.0",
+    checkerFramework       : "3.48.0",
     // for comparisons in other parts of the build
     errorProneLatest       : latestErrorProneVersion,
     // The version of Error Prone used to check NullAway's code.
@@ -53,6 +53,7 @@ def versions = [
     autoValue              : "1.10.2",
     autoService            : "1.1.1",
     javaparser             : "3.26.2",
+    googlejavaformat       : "1.24.0",
 ]
 
 def apt = [

gradle/wrapper/gradle-wrapper.properties

@@ -1,7 +1,7 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionSha256Sum=1541fa36599e12857140465f3c91a97409b4512501c26f9631fb113e392c5bd1
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.1-bin.zip
+distributionSha256Sum=31c55713e40233a8303827ceb42ca48a47267a0ad4bab9177123121e71524c26
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.2-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME

jmh/build.gradle

@@ -104,8 +104,19 @@ def nullawayReleaseClasspath = configurations.nullawayReleaseDeps.filter({f -> !
 
 def nullawayReleaseProcessorpath = configurations.nullawayReleaseProcessors.asPath
 
-// Extra JVM arguments to expose relevant paths for compiling benchmarks
 def extraJVMArgs = [
+    // needed exports for Error Prone to run
+    "--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
+    "--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
+    "--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
+    "--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED",
+    // expose relevant paths for compiling benchmarks
     "-Dnullaway.caffeine.sources=${caffeineSourceDir.get()}",
     "-Dnullaway.caffeine.classpath=$caffeineClasspath",
     "-Dnullaway.autodispose.sources=${autodisposeSourceDir.get()}",

nullaway/src/main/java/com/uber/nullaway/NullAway.java

@@ -2453,10 +2453,11 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) {
       case NEW_CLASS:
       case NEW_ARRAY:
       case ARRAY_TYPE:
+      // Lambdas may return null, but the lambda literal itself should not be null
       case LAMBDA_EXPRESSION:
-        // Lambdas may return null, but the lambda literal itself should not be null
+      // These cannot be null; the compiler would catch it
       case MEMBER_REFERENCE:
-        // These cannot be null; the compiler would catch it
+      // result of compound assignment cannot be null
       case MULTIPLY_ASSIGNMENT:
       case DIVIDE_ASSIGNMENT:
       case REMAINDER_ASSIGNMENT:
@@ -2468,9 +2469,8 @@ private boolean mayBeNullExpr(VisitorState state, ExpressionTree expr) {
       case AND_ASSIGNMENT:
       case XOR_ASSIGNMENT:
       case OR_ASSIGNMENT:
-        // result of compound assignment cannot be null
+      // rest are for auto-boxing
       case PLUS:
-        // rest are for auto-boxing
       case MINUS:
       case MULTIPLY:
       case DIVIDE:

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

@@ -231,14 +231,7 @@ public static Stream<? extends AnnotationMirror> getAllAnnotations(Symbol symbol
    */
   public static @Nullable Set<String> getAnnotationValueArray(
       Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) {
-    AnnotationMirror annot = null;
-    for (AnnotationMirror annotationMirror : methodSymbol.getAnnotationMirrors()) {
-      String name = AnnotationUtils.annotationName(annotationMirror);
-      if ((exactMatch && name.equals(annotName)) || (!exactMatch && name.endsWith(annotName))) {
-        annot = annotationMirror;
-        break;
-      }
-    }
+    AnnotationMirror annot = findAnnotation(methodSymbol, annotName, exactMatch);
     if (annot == null) {
       return null;
     }
@@ -256,6 +249,33 @@ public static Stream<? extends AnnotationMirror> getAllAnnotations(Symbol symbol
     return null;
   }
 
+  /**
+   * Retrieve the specific annotation of a method.
+   *
+   * @param methodSymbol A method to check for the annotation.
+   * @param annotName The qualified name or simple name of the annotation depending on the value of
+   *     {@code exactMatch}.
+   * @param exactMatch If true, the annotation name must match the full qualified name given in
+   *     {@code annotName}, otherwise, simple names will be checked.
+   * @return an {@code AnnotationMirror} representing that annotation, or null in case the
+   *     annotation with a given name {@code annotName} doesn't exist in {@code methodSymbol}.
+   */
+  public static @Nullable AnnotationMirror findAnnotation(
+      Symbol.MethodSymbol methodSymbol, String annotName, boolean exactMatch) {
+    AnnotationMirror annot = null;
+    for (AnnotationMirror annotationMirror : methodSymbol.getAnnotationMirrors()) {
+      String name = AnnotationUtils.annotationName(annotationMirror);
+      if ((exactMatch && name.equals(annotName)) || (!exactMatch && name.endsWith(annotName))) {
+        annot = annotationMirror;
+        break;
+      }
+    }
+    if (annot == null) {
+      return null;
+    }
+    return annot;
+  }
+
   /**
    * Works for method parameters defined either in source or in class files
    *

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java

@@ -287,7 +287,7 @@ && castToNonNull(receiver.getTree()).getKind().equals(Tree.Kind.IDENTIFIER)
             && (receiver.toString().equals("Integer") || receiver.toString().equals("Long"))) {
           return argumentToMapKeySpecifier(arguments.get(0), state, apContext);
         }
-        // Fine to fallthrough:
+      // Fine to fallthrough:
       default:
         // Every other type of expression, including variables, field accesses, new A(...), etc.
         return getAccessPathForNode(argument, state, apContext); // Every AP is a MapKey too
@@ -488,8 +488,8 @@ && isBoxingMethod(ASTHelpers.getSymbol(methodInvocationTree))) {
                   break;
                 }
               }
-              // Cascade to default, symbol is not a constant field
-              // fall through
+            // Cascade to default, symbol is not a constant field
+            // fall through
             default:
               return null; // Not an AP
           }

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java

@@ -21,8 +21,8 @@
 import static com.uber.nullaway.NullabilityUtil.castToNonNull;
 
 import com.google.common.base.Preconditions;
-import com.google.common.collect.ImmutableList;
 import com.google.errorprone.VisitorState;
+import com.google.errorprone.dataflow.nullnesspropagation.NullnessAnalysis;
 import com.sun.source.tree.Tree;
 import com.sun.source.util.TreePath;
 import com.sun.tools.javac.util.Context;
@@ -157,25 +157,7 @@ public Set<Element> getNonnullFieldsOfReceiverAtExit(TreePath path, Context cont
       // be conservative and say nothing is initialized
       return Collections.emptySet();
     }
-    return getNonnullReceiverFields(nullnessResult);
-  }
-
-  private Set<Element> getNonnullReceiverFields(NullnessStore nullnessResult) {
-    Set<AccessPath> nonnullAccessPaths = nullnessResult.getAccessPathsWithValue(Nullness.NONNULL);
-    Set<Element> result = new LinkedHashSet<>();
-    for (AccessPath ap : nonnullAccessPaths) {
-      // A null root represents the receiver
-      if (ap.getRoot() == null) {
-        ImmutableList<AccessPathElement> elements = ap.getElements();
-        if (elements.size() == 1) {
-          Element elem = elements.get(0).getJavaElement();
-          if (elem.getKind().equals(ElementKind.FIELD)) {
-            result.add(elem);
-          }
-        }
-      }
-    }
-    return result;
+    return nullnessResult.getNonNullReceiverFields();
   }
 
   /**
@@ -190,7 +172,7 @@ public Set<Element> getNonnullFieldsOfReceiverBefore(TreePath path, Context cont
     if (store == null) {
       return Collections.emptySet();
     }
-    return getNonnullReceiverFields(store);
+    return store.getNonNullReceiverFields();
   }
 
   /**

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java

@@ -852,7 +852,8 @@ public TransferResult<Nullness, NullnessStore> visitSuper(
   @Override
   public TransferResult<Nullness, NullnessStore> visitReturn(
       ReturnNode returnNode, TransferInput<Nullness, NullnessStore> input) {
-    handler.onDataflowVisitReturn(returnNode.getTree(), input.getThenStore(), input.getElseStore());
+    handler.onDataflowVisitReturn(
+        returnNode.getTree(), state, input.getThenStore(), input.getElseStore());
     return noStoreChanges(NULLABLE, input);
   }
 

nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java

@@ -19,6 +19,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 import static com.google.common.collect.Sets.intersection;
 
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.errorprone.VisitorState;
 import com.uber.nullaway.Nullness;
@@ -30,6 +31,7 @@
 import java.util.function.Predicate;
 import java.util.stream.Collectors;
 import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
 import org.checkerframework.nullaway.dataflow.analysis.Store;
 import org.checkerframework.nullaway.dataflow.cfg.node.FieldAccessNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
@@ -261,6 +263,39 @@ public NullnessStore filterAccessPaths(Predicate<AccessPath> pred) {
             .collect(Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue)));
   }
 
+  /**
+   * Return all the fields in the store that are Non-Null.
+   *
+   * @return Set of fields (represented as {@code Element}s) that are non-null
+   */
+  public Set<Element> getNonNullReceiverFields() {
+    return getReceiverFields(Nullness.NONNULL);
+  }
+
+  /**
+   * Return all the fields in the store that hold the {@code nullness} state.
+   *
+   * @param nullness The {@code Nullness} state
+   * @return Set of fields (represented as {@code Element}s) with the given {@code nullness}.
+   */
+  public Set<Element> getReceiverFields(Nullness nullness) {
+    Set<AccessPath> nonnullAccessPaths = this.getAccessPathsWithValue(nullness);
+    Set<Element> result = new LinkedHashSet<>();
+    for (AccessPath ap : nonnullAccessPaths) {
+      // A null root represents the receiver
+      if (ap.getRoot() == null) {
+        ImmutableList<AccessPathElement> elements = ap.getElements();
+        if (elements.size() == 1) {
+          Element elem = elements.get(0).getJavaElement();
+          if (elem.getKind().equals(ElementKind.FIELD)) {
+            result.add(elem);
+          }
+        }
+      }
+    }
+    return result;
+  }
+
   /** class for building up instances of the store. */
   public static final class Builder {
     private final Map<AccessPath, Nullness> contents;

nullaway/src/main/java/com/uber/nullaway/handlers/BaseNoOpHandler.java

@@ -174,7 +174,7 @@ public NullnessHint onDataflowVisitFieldAccess(
 
   @Override
   public void onDataflowVisitReturn(
-      ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) {
+      ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) {
     // NoOp
   }
 

nullaway/src/main/java/com/uber/nullaway/handlers/CompositeHandler.java

@@ -220,9 +220,9 @@ public NullnessHint onDataflowVisitFieldAccess(
 
   @Override
   public void onDataflowVisitReturn(
-      ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore) {
+      ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore) {
     for (Handler h : handlers) {
-      h.onDataflowVisitReturn(tree, thenStore, elseStore);
+      h.onDataflowVisitReturn(tree, state, thenStore, elseStore);
     }
   }
 

nullaway/src/main/java/com/uber/nullaway/handlers/Handler.java

@@ -269,12 +269,14 @@ NullnessHint onDataflowVisitFieldAccess(
    * Called when the Dataflow analysis visits a return statement.
    *
    * @param tree The AST node for the return statement being matched.
+   * @param state The current visitor state
    * @param thenStore The NullnessStore for the true case of the expression inside the return
    *     statement.
    * @param elseStore The NullnessStore for the false case of the expression inside the return
    *     statement.
    */
-  void onDataflowVisitReturn(ReturnTree tree, NullnessStore thenStore, NullnessStore elseStore);
+  void onDataflowVisitReturn(
+      ReturnTree tree, VisitorState state, NullnessStore thenStore, NullnessStore elseStore);
 
   /**
    * Called when the Dataflow analysis visits the result expression inside the body of lambda.