Improve verification of !null -> !null contracts (#1441)

msridhar · web-flow · commit fc6d95655fb1 · 2026-01-23T21:01:35.000Z
Fixes #1440 Fixes #1104 It turns out we can relatively easily handle these cases by looking for `BOTTOM` in the `NullnessStore` before the return expression (which means the path is infeasible). I do wonder if there are other places in our analyses we should be checking for `BOTTOM`, but we want to be careful since some users may expect issues to be reported in unreachable code. But for contract verification, it seems essential.  ## Summary by CodeRabbit * **New Features** * Enhanced contract-driven nullness analysis to inspect all nested return expressions and detect unreachable return paths via contract dataflow. * Added an API to identify unreachable/definitively-null access paths for contract checks. * Improved construction of contract-violation messages. * **Bug Fixes** * Reduces spurious contract violation reports (including void-like returns and unreachable branches). * **Tests** * Added tests covering propagation, multi-level contracts, ternaries, void returns, and nested lambdas/anonymous classes. * **Chores** * Replaced a runtime assertion with a clearer verification error for unexpected AST kinds. <sub>✏️ Tip: You can customize this high-level summary in your review settings.</sub>
diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessAnalysis.java
@@ -144,6 +144,23 @@ public static AccessPathNullnessAnalysis instance(VisitorState state, NullAway a
         exprPath, context, castToNonNull(contractNullnessPropagation), false);
   }
 
+  /**
+   * Check if any access path in the store before an expression maps to {@link Nullness#BOTTOM} in
+   * contract dataflow.
+   *
+   * @param exprPath tree path of expression
+   * @param context Javac context
+   * @return true if any access path has {@link Nullness#BOTTOM} before the expression
+   */
+  public boolean hasBottomAccessPathForContractDataflow(TreePath exprPath, Context context) {
+    NullnessStore store =
+        dataFlow.resultBeforeExpr(exprPath, context, castToNonNull(contractNullnessPropagation));
+    if (store == null) {
+      return false;
+    }
+    return !store.getAccessPathsWithValue(Nullness.BOTTOM).isEmpty();
+  }
+
   /**
    * Get the fields that are guaranteed to be nonnull after a method or initializer block.
    *
diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/ContractCheckHandler.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/ContractCheckHandler.java
@@ -28,7 +28,12 @@
 import com.google.common.base.Preconditions;
 import com.google.errorprone.VisitorState;
 import com.google.errorprone.util.ASTHelpers;
+import com.sun.source.tree.ClassTree;
+import com.sun.source.tree.ConditionalExpressionTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.LambdaExpressionTree;
 import com.sun.source.tree.MethodTree;
+import com.sun.source.tree.ParenthesizedTree;
 import com.sun.source.tree.ReturnTree;
 import com.sun.source.util.TreePath;
 import com.sun.source.util.TreePathScanner;
@@ -37,8 +42,11 @@
 import com.uber.nullaway.ErrorMessage;
 import com.uber.nullaway.NullAway;
 import com.uber.nullaway.Nullness;
+import com.uber.nullaway.dataflow.AccessPathNullnessAnalysis;
 import com.uber.nullaway.handlers.Handler;
 import com.uber.nullaway.handlers.MethodAnalysisContext;
+import java.util.ArrayList;
+import java.util.List;
 import java.util.Set;
 import org.jspecify.annotations.Nullable;
 
@@ -136,68 +144,130 @@ public void onMatchMethod(MethodTree tree, MethodAnalysisContext methodAnalysisC
 
       // we scan the method tree for the return nodes and check the contract
       new TreePathScanner<@Nullable Void, @Nullable Void>() {
-        @Override
-        public @Nullable Void visitReturn(ReturnTree returnTree, @Nullable Void unused) {
-
-          VisitorState returnState = state.withPath(getCurrentPath());
-          Nullness nullness =
-              analysis
-                  .getNullnessAnalysis(returnState)
-                  .getNullnessForContractDataflow(
-                      new TreePath(returnState.getPath(), returnTree.getExpression()),
-                      returnState.context);
 
-          if (nullness == Nullness.NULLABLE || nullness == Nullness.NULL) {
+        @Override
+        public @Nullable Void visitLambdaExpression(
+            LambdaExpressionTree node, @Nullable Void unused) {
+          // do not scan into lambdas
+          return null;
+        }
 
-            String errorMessage;
+        @Override
+        public @Nullable Void visitClass(ClassTree node, @Nullable Void unused) {
+          // do not scan into local/anonymous classes
+          return null;
+        }
 
-            // used for error message
-            int nonNullAntecedentCount = 0;
-            int nonNullAntecedentPosition = -1;
+        @Override
+        public @Nullable Void visitReturn(ReturnTree returnTree, @Nullable Void unused) {
 
-            for (int i = 0; i < antecedent.length; ++i) {
-              String valueConstraint = antecedent[i].trim();
+          ExpressionTree returnExpression = returnTree.getExpression();
+          if (returnExpression == null) {
+            // this should only be possible with an invalid @Contract on a void-returning method
+            return null;
+          }
+          TreePath returnExpressionPath = new TreePath(getCurrentPath(), returnExpression);
+          AccessPathNullnessAnalysis nullnessAnalysis = analysis.getNullnessAnalysis(state);
+          List<TreePath> allPossiblyReturnedExpressions = new ArrayList<>();
+          collectNestedReturnedExpressions(returnExpressionPath, allPossiblyReturnedExpressions);
 
-              if (valueConstraint.equals("!null")) {
-                nonNullAntecedentCount += 1;
-                nonNullAntecedentPosition = i;
+          boolean contractViolated = false;
+          for (TreePath expressionPath : allPossiblyReturnedExpressions) {
+            Nullness nullness =
+                nullnessAnalysis.getNullnessForContractDataflow(expressionPath, state.context);
+            if (nullness == Nullness.NULLABLE || nullness == Nullness.NULL) {
+              if (nullnessAnalysis.hasBottomAccessPathForContractDataflow(
+                  expressionPath, state.context)) {
+                // if any access path is mapped to bottom, this branch is unreachable
+                continue;
               }
+              contractViolated = true;
+              break;
             }
+          }
 
-            if (nonNullAntecedentCount == 1) {
-
-              errorMessage =
-                  "Method "
-                      + callee.name
-                      + " has @Contract("
-                      + contractString
-                      + "), but this appears to be violated, as a @Nullable value may be returned when parameter "
-                      + tree.getParameters().get(nonNullAntecedentPosition).getName()
-                      + " is non-null.";
-            } else {
-              errorMessage =
-                  "Method "
-                      + callee.name
-                      + " has @Contract("
-                      + contractString
-                      + "), but this appears to be violated, as a @Nullable value may be returned "
-                      + "when the contract preconditions are true.";
-            }
+          if (contractViolated) {
+            String errorMessage =
+                getErrorMessageForViolatedContract(antecedent, callee, contractString, tree);
 
-            returnState.reportMatch(
+            state.reportMatch(
                 analysis
                     .getErrorBuilder()
                     .createErrorDescription(
                         new ErrorMessage(
                             ErrorMessage.MessageTypes.ANNOTATION_VALUE_INVALID, errorMessage),
                         returnTree,
                         analysis.buildDescription(returnTree),
-                        returnState,
+                        state,
                         null));
           }
           return super.visitReturn(returnTree, null);
         }
       }.scan(state.getPath(), null);
     }
   }
+
+  private static String getErrorMessageForViolatedContract(
+      String[] antecedent, Symbol.MethodSymbol callee, String contractString, MethodTree tree) {
+    String errorMessage;
+
+    // used for error message
+    int nonNullAntecedentCount = 0;
+    int nonNullAntecedentPosition = -1;
+
+    for (int i = 0; i < antecedent.length; ++i) {
+      String valueConstraint = antecedent[i].trim();
+
+      if (valueConstraint.equals("!null")) {
+        nonNullAntecedentCount += 1;
+        nonNullAntecedentPosition = i;
+      }
+    }
+
+    if (nonNullAntecedentCount == 1) {
+      errorMessage =
+          "Method "
+              + callee.name
+              + " has @Contract("
+              + contractString
+              + "), but this appears to be violated, as a @Nullable value may be returned when parameter "
+              + tree.getParameters().get(nonNullAntecedentPosition).getName()
+              + " is non-null.";
+    } else {
+      errorMessage =
+          "Method "
+              + callee.name
+              + " has @Contract("
+              + contractString
+              + "), but this appears to be violated, as a @Nullable value may be returned "
+              + "when the contract preconditions are true.";
+    }
+    return errorMessage;
+  }
+
+  /**
+   * Collect {@code TreePath}s to all nested expressions that may be returned, recursing through
+   * parenthesized expressions and conditional expressions.
+   *
+   * @param expressionPath the TreePath to an expression being returned
+   * @param output output parameter list to collect nested returned expression TreePaths
+   */
+  private static void collectNestedReturnedExpressions(
+      TreePath expressionPath, List<TreePath> output) {
+    ExpressionTree expression = (ExpressionTree) expressionPath.getLeaf();
+    while (expression instanceof ParenthesizedTree) {
+      ExpressionTree nestedExpression = ((ParenthesizedTree) expression).getExpression();
+      expressionPath = new TreePath(expressionPath, nestedExpression);
+      expression = nestedExpression;
+    }
+    if (expression instanceof ConditionalExpressionTree) {
+      ConditionalExpressionTree conditionalExpression = (ConditionalExpressionTree) expression;
+      TreePath truePath = new TreePath(expressionPath, conditionalExpression.getTrueExpression());
+      TreePath falsePath = new TreePath(expressionPath, conditionalExpression.getFalseExpression());
+      collectNestedReturnedExpressions(truePath, output);
+      collectNestedReturnedExpressions(falsePath, output);
+      return;
+    }
+    output.add(expressionPath);
+  }
 }
diff --git a/nullaway/src/main/java/com/uber/nullaway/handlers/contract/ContractNullnessStoreInitializer.java b/nullaway/src/main/java/com/uber/nullaway/handlers/contract/ContractNullnessStoreInitializer.java
@@ -3,6 +3,7 @@
 import static com.uber.nullaway.Nullness.NONNULL;
 import static com.uber.nullaway.Nullness.NULLABLE;
 
+import com.google.common.base.Verify;
 import com.google.errorprone.util.ASTHelpers;
 import com.sun.source.tree.ClassTree;
 import com.sun.source.tree.MethodTree;
@@ -34,7 +35,10 @@ public NullnessStore getInitialStore(
       Context context,
       Types types,
       Config config) {
-    assert underlyingAST.getKind() == UnderlyingAST.Kind.METHOD;
+    Verify.verify(
+        underlyingAST.getKind() == UnderlyingAST.Kind.METHOD,
+        "Expected AST for method but got %s",
+        underlyingAST.getKind());
 
     MethodTree methodTree = ((UnderlyingAST.CFGMethod) underlyingAST).getMethod();
     ClassTree classTree = ((UnderlyingAST.CFGMethod) underlyingAST).getClassTree();
diff --git a/nullaway/src/test/java/com/uber/nullaway/ContractsTests.java b/nullaway/src/test/java/com/uber/nullaway/ContractsTests.java
