Skip to content

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

Merged
msridhar merged 12 commits intomasterfrom
contracts-issue
Jan 23, 2026
Merged

Improve verification of !null -> !null contracts#1441
msridhar merged 12 commits intomasterfrom
contracts-issue

Conversation

@msridhar
Copy link
Copy Markdown
Collaborator

@msridhar msridhar commented Jan 21, 2026

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 definitively-null/unreachable access paths used by contract checks.
    • Improved construction of contract-violation messages and skipping void-returning contracts.
  • Bug Fixes

    • Reduces spurious contract violation reports and avoids descending into lambdas/local/anonymous classes.
  • Tests

    • Added tests for 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.

✏️ Tip: You can customize this high-level summary in your review settings.

@coderabbitai
Copy link
Copy Markdown
Contributor

coderabbitai Bot commented Jan 21, 2026

Walkthrough

Adds AccessPathNullnessAnalysis.hasBottomAccessPathForContractDataflow(TreePath, Context) to query the contract dataflow store for access paths mapped to Nullness.BOTTOM. Refactors ContractCheckHandler to collect nested return expressions (ParenthesizedTree and ConditionalExpressionTree), avoid entering lambdas and local/anonymous classes during contract scanning, and use access-path analysis to skip contract-violation reports when infeasible branches are indicated by bottom mappings. Adds six unit tests in ContractsTests covering !null->!null contracts, multi-level cases, ternaries, void-return handling, and nested lambda/anonymous-class returns. Replaces an assertion with a Guava Verify check in ContractNullnessStoreInitializer.

Possibly related PRs

Suggested reviewers

  • yuxincs
  • lazaroclapp
🚥 Pre-merge checks | ✅ 4 | ❌ 1
❌ Failed checks (1 warning)
Check name Status Explanation Resolution
Docstring Coverage ⚠️ Warning Docstring coverage is 31.25% which is insufficient. The required threshold is 80.00%. Write docstrings for the functions missing them to satisfy the coverage threshold.
✅ Passed checks (4 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title 'Improve verification of !null -> !null contracts' directly describes the main objective of improving contract verification to handle infeasible paths.
Linked Issues check ✅ Passed The pull request implements changes to detect BOTTOM in NullnessStore to identify infeasible paths, preventing false-positive contract violations. Test coverage validates the fixes for issues #1440 and #1104.
Out of Scope Changes check ✅ Passed All changes are scoped to contract verification improvements: new bottom-detection method in AccessPathNullnessAnalysis, updated contract-checking logic to collect and analyze return paths, verification refactoring, and comprehensive test coverage.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing touches
  • 📝 Generate docstrings

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Fix all issues with AI agents
In
`@nullaway/src/main/java/com/uber/nullaway/handlers/contract/ContractCheckHandler.java`:
- Around line 145-158: The code assumes returnTree.getExpression() is non-null
which crashes for bare "return;" in void methods; add a defensive null check
after computing ExpressionTree returnExpression (from
returnTree.getExpression()) and skip the nullness checks (e.g., return null or
continue the handler) when returnExpression == null to avoid constructing a
TreePath for a null expression; update use-sites including returnExpressionPath,
getNullnessForContractDataflow(..., returnState.context) and
hasBottomAccessPathForContractDataflow(..., returnState.context) to only run
when returnExpression is non-null.

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 1

🤖 Fix all issues with AI agents
In `@nullaway/src/test/java/com/uber/nullaway/ContractsTests.java`:
- Around line 752-767: In testPositive1 replace the null-branch call that uses
the possibly-null parameter with a non-null constant to avoid unrelated nullness
diagnostics: update the branch in the method testPositive1 (which is annotated
`@Contract`("!null -> !null")) so it does not call Integer.parseInt(text) when
text == null but instead returns a non-null constant (e.g., use
Integer.parseInt("1") or return Integer.valueOf(1)) so the test focuses only on
the contract violation.

Comment thread nullaway/src/test/java/com/uber/nullaway/ContractsTests.java
@codecov
Copy link
Copy Markdown

codecov Bot commented Jan 21, 2026

Codecov Report

❌ Patch coverage is 94.82759% with 3 lines in your changes missing coverage. Please review.
✅ Project coverage is 88.40%. Comparing base (7f8bbca) to head (d286650).
⚠️ Report is 1 commits behind head on master.

Files with missing lines Patch % Lines
.../nullaway/dataflow/AccessPathNullnessAnalysis.java 60.00% 1 Missing and 1 partial ⚠️
...ers/contract/ContractNullnessStoreInitializer.java 66.66% 0 Missing and 1 partial ⚠️
Additional details and impacted files
@@             Coverage Diff              @@
##             master    #1441      +/-   ##
============================================
+ Coverage     88.37%   88.40%   +0.02%     
- Complexity     2702     2711       +9     
============================================
  Files            99       99              
  Lines          8965     9004      +39     
  Branches       1790     1799       +9     
============================================
+ Hits           7923     7960      +37     
- Misses          516      517       +1     
- Partials        526      527       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

}
}

private static String getErrorMessageForViolatedContract(
Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is drive-by refactoring to extract this method from the one above which was getting huge. Sorry for the unrelated change.

@msridhar msridhar requested a review from yuxincs January 23, 2026 06:29
Comment on lines +166 to +167
// this should only be possible with an invalid @Contract on a void-returning method;
// report an error on that in the future?
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if this is a responsibility of another EP checker that checks such contract validity?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, fair enough, I agree this should probably be out of bounds for NullAway. Will update the comment

@msridhar msridhar enabled auto-merge (squash) January 23, 2026 20:51
@msridhar msridhar merged commit fc6d956 into master Jan 23, 2026
11 checks passed
@msridhar msridhar deleted the contracts-issue branch January 23, 2026 21:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unexpected errors from contract checking for !null -> !null contracts NullAway dataflow analysis does not prune out infeasible paths

2 participants