Skip to content

Support method-based conditional library model postconditions - #1677

Open
Shankar-v27 wants to merge 1 commit into
uber:masterfrom
Shankar-v27:feature/library-method-postconditions
Open

Support method-based conditional library model postconditions#1677
Shankar-v27 wants to merge 1 commit into
uber:masterfrom
Shankar-v27:feature/library-method-postconditions

Conversation

@Shankar-v27

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

Copy link
Copy Markdown

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 recognizing when one method’s result conditionally guarantees another method call is non-null.
    • Added support for conditional nullability relationships across interface method calls.
    • Expanded support for custom conditional nullability contracts.
  • Bug Fixes

    • More accurately reports potential null dereferences when array component types may be null.
    • 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

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: 6735f710-59ab-473d-8e22-58de14cae35d

📥 Commits

Reviewing files that changed from the base of the PR and between 8db933d and df58539.

📒 Files selected for processing (1)
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.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. The default models relate Class.isArray() to Class.getComponentType() and mark getComponentType() nullable. Tests cover class and interface conditional branches.

Possibly related PRs

  • uber/NullAway#1407: Both changes extend LibraryModels and LibraryModelsHandler with method-level nullability modeling APIs.

Suggested reviewers: msridhar, yuxincs

🚥 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 summarizes the main change: support for method-based conditional postconditions in library models.
Linked Issues check ✅ Passed The changes implement conditional library postconditions and model the Class.isArray()/getComponentType() relationship requested in issue #1664.
Out of Scope Changes check ✅ Passed The implementation, library models, test fixtures, and regression tests are directly related to the linked issue objectives.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
✨ Finishing Touches
🧪 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

Comment on lines 350 to 356
private void setConditionalArgumentNullness(
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
List<Node> arguments,
MethodInvocationNode node,
Symbol.MethodSymbol callee,
VisitorState state,
AccessPath.AccessPathContext apContext) {

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

Add Javadoc for the changed non-trivial private methods.

Both methods implement conditional library-model dataflow behavior without method documentation.

  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java#L350-L356: document branch updates, inputs, and receiver-method refinement.
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java#L390-L404: document hierarchy lookup behavior and nullable return semantics.

As per coding guidelines, “Add Javadoc for every non-trivial method, including private methods.”

📍 Affects 1 file
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java#L350-L356 (this comment)
  • nullaway/src/main/java/com/uber/nullaway/handlers/LibraryModelsHandler.java#L390-L404
🤖 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/handlers/LibraryModelsHandler.java`
around lines 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.

Source: Coding guidelines

@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 85.71429% with 7 lines in your changes missing coverage. Please review.
✅ Project coverage is 87.65%. Comparing base (2da3fad) to head (71d949d).
⚠️ Report is 2 commits behind head on master.

Files with missing lines Patch % Lines
...m/uber/nullaway/handlers/LibraryModelsHandler.java 83.72% 2 Missing and 5 partials ⚠️
Additional details and impacted files
@@             Coverage Diff              @@
##             master    #1677      +/-   ##
============================================
- Coverage     87.67%   87.65%   -0.02%     
- Complexity     3138     3144       +6     
============================================
  Files           109      109              
  Lines         10619    10664      +45     
  Branches       2147     2156       +9     
============================================
+ Hits           9310     9348      +38     
- Misses          628      630       +2     
- Partials        681      686       +5     

☔ 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
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
Signed-off-by: Shankar V <shankarvelmurugan2018@gmail.com>
@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
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