Skip to content

Support method-based conditional library model postconditions - #1677

Merged
msridhar merged 2 commits into
uber:masterfrom
Shankar-v27:feature/library-method-postconditions
Aug 13, 2026
Merged

Support method-based conditional library model postconditions#1677
msridhar merged 2 commits into
uber:masterfrom
Shankar-v27:feature/library-method-postconditions

Conversation

@Shankar-v27

@Shankar-v27 Shankar-v27 commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Summary

Fixes #1664.

This PR extends LibraryModels to support conditional postconditions on receiver methods, allowing library models to express relationships where the return value of one method refines the nullability of another method on the same receiver.

As an initial use case, it models the JDK relationship:

  • Class.isArray() returning true implies Class.getComponentType() is non-null.

This eliminates the false positive described in the issue while reusing NullAway's existing conditional dataflow infrastructure (AccessPath, thenUpdates, and LibraryModelsHandler).

The implementation is intentionally limited to library models and does not change the parsing or semantics of user-written @EnsuresNonNullIf annotations.

Changes

  • Added support in LibraryModels for modeling conditional receiver method postconditions.
  • Extended LibraryModelsHandler to propagate these postconditions using the existing AccessPath and conditional dataflow mechanisms.
  • Added a default library model for:
    • Class.isArray() -> Class.getComponentType()
  • Added a regression test covering the new behavior.

Testing

Added a regression test verifying that:

if (clazz.isArray()) {
    clazz.getComponentType().hashCode();
}

does not produce a nullness warning, while dereferencing getComponentType() outside the refined branch continues to report a warning.

Verified with:

./gradlew :nullaway:test

AI Usage

I used ChatGPT to better understand the existing NullAway architecture, discuss implementation approaches, and review the design. I manually implemented, reviewed, tested, and verified all code changes before submitting this PR.

Summary by CodeRabbit

  • New Features

    • Improved nullability analysis for Class.isArray() and Class.getComponentType().
    • Added support for conditional guarantees that related method calls return non-null values.
    • Added support for conditional nullability contracts across interface methods.
    • Expanded support for custom library nullability models.
  • Bug Fixes

    • More accurately identifies possible null dereferences on alternate conditional branches.
    • Improved handling of related method calls across class and interface hierarchies.

@coderabbitai

coderabbitai Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Review Change Stack

Note

Reviews paused

It looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the reviews.auto_review.auto_pause_after_reviewed_commits setting.

Use the following commands to manage reviews:

  • @coderabbitai resume to resume automatic reviews.
  • @coderabbitai review to trigger a single review.

Use the checkboxes below for quick actions:

  • ▶️ Resume reviews
  • 🔍 Trigger review

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 63979c4d-195d-4a2c-9b52-9d82e8c429f6

📥 Commits

Reviewing files that changed from the base of the PR and between df58539 and 53bb09f.

📒 Files selected for processing (3)
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java
  • nullaway/src/test/java/com/uber/nullaway/FrameworkTests.java
  • nullaway/src/test/java/com/uber/nullaway/JSpecifyJDKModelsTest.java

Walkthrough

Adds a library-model contract for conditional receiver method nullness. Aggregates and optimizes these mappings across library models. Conditional analysis resolves target methods through class hierarchies and marks receiver access paths non-null on the true branch. Default models relate Class.isArray() to Class.getComponentType(). Tests cover class and interface conditional branches.

Possibly related PRs

  • uber/NullAway#1242: Both modify DefaultLibraryModels with library-method nullability models.
  • uber/NullAway#1407: Both extend LibraryModels and LibraryModelsHandler with method-level nullability modeling.
  • uber/NullAway#1646: Both modify JSpecifyJDKModelsTest for JSpecify JDK model coverage.

Suggested labels: jspecify

Suggested reviewers: msridhar, yuxincs, lazaroclapp

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly describes the primary change: support for method-based conditional postconditions in library models.
Linked Issues check ✅ Passed The changes implement method-based conditional library models and cover the Class.isArray() and getComponentType() relationship requested in issue #1664.
Out of Scope Changes check ✅ Passed The changes are limited to library model support, related model definitions, and regression tests for the stated objectives.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
✨ Finishing Touches 💡 1
⚔️ Resolve merge conflicts 💡
  • Resolve merge conflict in branch feature/library-method-postconditions
🧪 Generate unit tests (beta)
  • Create PR with unit tests

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.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Actionable comments posted: 2

🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java`:
- Around line 350-356: Add Javadoc for the private method
setConditionalArgumentNullness in
nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java
lines 350-356, documenting its inputs, branch updates, and receiver-method
refinement. Also document the non-trivial private method at lines 390-404 in the
same file, describing its hierarchy lookup behavior and nullable return
semantics.
- Around line 390-404: Update lookupMethodSymbol to traverse classSymbol’s
directly implemented interfaces, recursively resolving targetRef before
returning null; retain superclass traversal so interfaces inherited through
superclasses are also searched. Add a regression test using a conditional model
targeting a default interface method and verify the true-branch update is
applied.
🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 457727cc-fc99-412f-8357-826c9f9fae08

📥 Commits

Reviewing files that changed from the base of the PR and between 2da3fad and f2a7cf5.

📒 Files selected for processing (3)
  • nullaway/src/main/java/com/uber/nullaway/LibraryModels.java
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java
  • nullaway/src/test/java/com/uber/nullaway/FrameworkTests.java

@Shankar-v27
Shankar-v27 force-pushed the feature/library-method-postconditions branch from f2a7cf5 to bc1795a Compare August 6, 2026 17:01
@coderabbitai

coderabbitai Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Note

GitHub couldn't provide a complete incremental comparison for this pull request, so CodeRabbit is performing a full review instead. This review may take a little longer.

@Shankar-v27
Shankar-v27 force-pushed the feature/library-method-postconditions branch from bc1795a to 71d949d Compare August 6, 2026 17:02
@coderabbitai

coderabbitai Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

Note

GitHub couldn't provide a complete incremental comparison for this pull request, so CodeRabbit is performing a full review instead. This review may take a little longer.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@nullaway/src/main/java/com/uber/nullaway/LibraryModels.java`:
- Around line 90-100: Correct the contract for nullImpliesFalseMethodCalls:
update its Javadoc to describe that a null target-method result implies the
querying method returns false, with the non-null result implying true by
contrapositive. Keep the method name and default empty ImmutableSetMultimap
implementation unchanged.
🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

  • Push a commit to this branch (recommended)
  • Create a new PR with the fixes

ℹ️ Review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 6f9ec139-b3fc-48fc-8bc7-aa9bf6de159a

📥 Commits

Reviewing files that changed from the base of the PR and between 2da3fad and 71d949d.

📒 Files selected for processing (5)
  • nullaway/src/main/java/com/uber/nullaway/LibraryModels.java
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java
  • nullaway/src/test/java/com/uber/nullaway/FrameworkTests.java
  • test-java-lib/src/main/java/com/uber/lib/unannotated/CustomInterface.java
  • test-library-models/src/main/java/com/uber/nullaway/testlibrarymodels/TestLibraryModels.java

Comment on lines +90 to +100
/**
* Get (method, target method) pairs where returning <code>false</code> implies the target method
* on the receiver is <code>null</code> (and returning <code>true</code> implies the target method
* on the receiver is non-null).
*
* @return map from querying methods to target receiver methods that are non-null when returning
* true.
*/
default ImmutableSetMultimap<MethodRef, MethodRef> nullImpliesFalseMethodCalls() {
return ImmutableSetMultimap.of();
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Correct the conditional-model contract.

The Javadoc states that a false result implies that the target method returns null. The model name and implementation encode the opposite implication: a null target result implies false. The true-branch non-null result follows by contrapositive.

Proposed fix
- * Get (method, target method) pairs where returning <code>false</code> implies the target method
- * on the receiver is <code>null</code> (and returning <code>true</code> implies the target method
- * on the receiver is non-null).
+ * Get (querying method, target receiver method) pairs where a <code>null</code> target result
+ * implies that the querying method returns <code>false</code>.
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
/**
* Get (method, target method) pairs where returning <code>false</code> implies the target method
* on the receiver is <code>null</code> (and returning <code>true</code> implies the target method
* on the receiver is non-null).
*
* @return map from querying methods to target receiver methods that are non-null when returning
* true.
*/
default ImmutableSetMultimap<MethodRef, MethodRef> nullImpliesFalseMethodCalls() {
return ImmutableSetMultimap.of();
}
/**
* Get (querying method, target receiver method) pairs where a <code>null</code> target result
* implies that the querying method returns <code>false</code>.
*
* `@return` map from querying methods to target receiver methods that are non-null when returning
* true.
*/
default ImmutableSetMultimap<MethodRef, MethodRef> nullImpliesFalseMethodCalls() {
return ImmutableSetMultimap.of();
}
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@nullaway/src/main/java/com/uber/nullaway/LibraryModels.java` around lines 90
- 100, Correct the contract for nullImpliesFalseMethodCalls: update its Javadoc
to describe that a null target-method result implies the querying method returns
false, with the non-null result implying true by contrapositive. Keep the method
name and default empty ImmutableSetMultimap implementation unchanged.

@msridhar msridhar left a comment

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.

Thanks, this looks promising! I have some review comments below

Comment thread nullaway/src/main/java/com/uber/nullaway/LibraryModels.java Outdated
Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated
Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated
Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated
Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated

@msridhar msridhar left a comment

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.

Whoops, meant to request changes before

@codecov

codecov Bot commented Aug 7, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 80.32787% with 12 lines in your changes missing coverage. Please review.
✅ Project coverage is 87.82%. Comparing base (98d7a76) to head (5bf2c7d).

Files with missing lines Patch % Lines
...m/uber/nullaway/handlers/LibraryModelsHandler.java 78.18% 4 Missing and 8 partials ⚠️
Additional details and impacted files
@@             Coverage Diff              @@
##             master    #1677      +/-   ##
============================================
- Coverage     87.88%   87.82%   -0.06%     
- Complexity     3175     3181       +6     
============================================
  Files           109      109              
  Lines         10763    10809      +46     
  Branches       2174     2185      +11     
============================================
+ Hits           9459     9493      +34     
- Misses          618      622       +4     
- Partials        686      694       +8     

☔ View full report in Codecov by Harness.
📢 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.

@Shankar-v27

Copy link
Copy Markdown
Contributor Author

@msridhar Thanks for the review! I'll address these comments and push an updated revision shortly.

@Shankar-v27
Shankar-v27 force-pushed the feature/library-method-postconditions branch from 71d949d to 8db933d Compare August 8, 2026 04:38
@Shankar-v27
Shankar-v27 requested a review from msridhar August 8, 2026 09:33

@msridhar msridhar left a comment

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.

Thanks for addressing the comments. I have another comment below.

Also, for future reference, please respond to my review comments and describe how they were addressed. This will make it easier for me to do a follow-up review. (And, I'd prefer these responses not be copy-pasted from an LLM.)

Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated
@Shankar-v27
Shankar-v27 force-pushed the feature/library-method-postconditions branch from 8db933d to df58539 Compare August 12, 2026 09:59
@Shankar-v27
Shankar-v27 requested a review from msridhar August 12, 2026 10:05

@msridhar msridhar left a comment

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.

Now mostly LGTM! Just one more change and I think we'll be good to go

Comment thread nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java Outdated
Signed-off-by: Shankar V <shankarvelmurugan2018@gmail.com>
@Shankar-v27
Shankar-v27 force-pushed the feature/library-method-postconditions branch from df58539 to 53bb09f Compare August 13, 2026 05:02
@Shankar-v27
Shankar-v27 requested a review from msridhar August 13, 2026 05:04

@msridhar msridhar left a comment

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.

Thanks for the contribution!

@msridhar
msridhar enabled auto-merge (squash) August 13, 2026 18:30
@msridhar
msridhar merged commit a46180c into uber:master Aug 13, 2026
12 of 14 checks passed
@Shankar-v27

Copy link
Copy Markdown
Contributor Author

Thank you for the review and guidance throughout the process! I really appreciate it.

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.

Support richer @EnsuresNonNullIf with methods, at least for library models

2 participants