Add side effect annotations#278
Conversation
|
Warning Review limit reached
More reviews will be available in 37 minutes and 15 seconds. Learn how PR review limits work. Your organization has run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans include higher PR review limits than trial, open-source, and free plans. In all cases, reviews become available again over time. During sustained high-volume PR review activity, CodeRabbit may temporarily slow when the next review becomes available. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (3)
📝 WalkthroughWalkthroughThis pull request adds Checker Framework semantic annotations to the Java base library to document operation purity, side-effects, and collection state contracts. The changes span three independent annotation strategies: adding 🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
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. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 5
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (3)
src/java.base/share/classes/java/util/TreeSet.java (1)
529-534:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winRemove
@EnsuresNonEmpty("this")from methods that always throw exceptions.Both
addFirstandaddLastunconditionally throwUnsupportedOperationExceptionand never return normally. The@EnsuresNonEmpty("this")postcondition annotation is incorrect because:
- The postcondition can never be established since the methods never complete normally
- Static analysis tools may incorrectly assume the set is non-empty after these methods are called in try-catch blocks
- The annotation misrepresents the actual behavior of these methods
Postcondition annotations should only be applied to methods that can return normally and actually establish the stated postcondition.
🔧 Proposed fix
- `@EnsuresNonEmpty`("this") // `@SideEffectsOnly`("this") `@DoesNotUnrefineReceiver`("modifiability") public void addFirst(E e) { throw new UnsupportedOperationException(); }- `@EnsuresNonEmpty`("this") // `@SideEffectsOnly`("this") `@DoesNotUnrefineReceiver`("modifiability") public void addLast(E e) { throw new UnsupportedOperationException(); }Also applies to: 544-549
🤖 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 `@src/java.base/share/classes/java/util/TreeSet.java` around lines 529 - 534, The `@EnsuresNonEmpty`("this") postcondition is incorrect on methods that always throw and never return; remove the `@EnsuresNonEmpty`("this") annotation from the addFirst(E e) and addLast(E e) methods in class TreeSet so their declarations only reflect that they throw UnsupportedOperationException (leave other annotations like `@DoesNotUnrefineReceiver` if applicable) to avoid misleading static analyzers and incorrect postcondition assumptions.src/java.base/share/classes/java/util/SortedSet.java (1)
297-302:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winMisleading
@EnsuresNonEmpty("this")on a method that always throws.The
addFirstdefault implementation unconditionally throwsUnsupportedOperationExceptionand never returns normally. While@EnsuresNonEmpty("this")is vacuously true (postcondition doesn't need to hold if method doesn't return), it misleadingly suggests the method might succeed and ensure non-emptiness. Consider removing this annotation from methods that always throw.🤖 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 `@src/java.base/share/classes/java/util/SortedSet.java` around lines 297 - 302, Remove the misleading `@EnsuresNonEmpty`("this") annotation from the default addFirst(E e) method in SortedSet (the method currently throws UnsupportedOperationException and never returns); locate the addFirst method declaration and delete the `@EnsuresNonEmpty`("this") annotation (and any similar postcondition annotations on other default methods that unconditionally throw) so annotations only appear on methods that can return normally and establish the postcondition.src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java (1)
133-136:⚠️ Potential issue | 🟠 Major | ⚖️ Poor tradeoffPre-existing bug:
add()should return the result frombase.add(e).Line 135 unconditionally returns
true, violating theSet.add()contract, which requires returningfalseif the element was already present. This causes callers to incorrectly believe the element was always added.Note: This bug exists in the base code and is not introduced by this PR's annotation changes.
🐛 Proposed fix
public boolean add(E e) { - base.add(e); - return true; + return base.add(e); }🤖 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 `@src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java` around lines 133 - 136, The add method in class ReverseOrderSortedSetView unconditionally returns true which violates Set.add() semantics; change the implementation of public boolean add(E e) in ReverseOrderSortedSetView to return the boolean result produced by base.add(e) (i.e., return base.add(e)) so callers correctly receive false when the element was already present.
♻️ Duplicate comments (1)
src/java.base/share/classes/java/util/SortedSet.java (1)
315-320:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winMisleading
@EnsuresNonEmpty("this")on a method that always throws.Same issue as
addFirst: the default implementation always throws, making the@EnsuresNonEmpty("this")annotation vacuously true but misleading.🤖 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 `@src/java.base/share/classes/java/util/SortedSet.java` around lines 315 - 320, The `@EnsuresNonEmpty`("this") on the default SortedSet.addLast(E) is misleading because the default always throws; remove the `@EnsuresNonEmpty`("this") annotation from the default addLast method in class SortedSet (and mirror the same change made for addFirst if present) so the contract does not falsely claim the receiver becomes non-empty for a method that never succeeds.
🤖 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 `@src/java.base/share/classes/java/util/ComparableTimSort.java`:
- Around line 47-48: There are two consecutive declarations of the same
top-level class (the annotated "`@UsesObjectEquals` class ComparableTimSort"
followed immediately by "class ComparableTimSort"), which breaks compilation;
remove the duplicate unannotated declaration so only the single annotated class
ComparableTimSort remains (keep the "`@UsesObjectEquals` class ComparableTimSort"
form and delete the extra "class ComparableTimSort" token), ensuring the class
body and members remain unchanged.
In `@src/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.java`:
- Around line 459-464: Remove the misleading postcondition by deleting the
`@EnsuresNonEmpty`("this") annotation from the ConcurrentSkipListSet.addFirst(E e)
declaration; leave the method body that unconditionally throws
UnsupportedOperationException and retain the other annotations (e.g.,
`@DoesNotUnrefineReceiver`("modifiability")) so the signature still indicates it
never returns normally without implying the set becomes non-empty.
- Around line 474-479: Remove the misleading postcondition by deleting the
`@EnsuresNonEmpty`("this") annotation from the addLast(E e) method; since addLast
always throws UnsupportedOperationException and never returns normally, drop the
annotation (leave `@DoesNotUnrefineReceiver` and any other valid annotations
intact) so the method’s signature no longer implies it guarantees a non-empty
set on completion.
In `@src/java.base/share/classes/java/util/DualPivotQuicksort.java`:
- Around line 185-186: The `@SideEffectsOnly` annotation on the int-array overload
incorrectly references the sorter parameter (`#1`); change it to target the
mutated array parameter (`#2`) so the signature static void sort(Sorter sorter,
int[] a, int bits, `@IndexOrHigh`({"`#1`"}) int low, `@IndexOrHigh`({"`#1`"}) int high)
uses // `@SideEffectsOnly`("`#2`") to match the long/float/double overloads and
correctly document that the array 'a' is modified.
In `@src/java.base/share/classes/java/util/ListIterator.java`:
- Around line 222-225: The `@EnsuresNonEmpty`("this") annotation on
ListIterator.add is incorrect because it claims the iterator becomes non-empty
in Checker Framework terms (which affects next()/hasNext() reasoning) even when
add(E) at the end does not make hasNext()==true; remove the
`@EnsuresNonEmpty`("this") annotation from the add(`@GuardSatisfied` ListIterator<E>
this, E e) declaration (or replace it with a safer, documented postcondition
that does not assert non-empty cursor state) and update any comment to explain
that add does not guarantee hasNext() becomes true after insertion.
---
Outside diff comments:
In `@src/java.base/share/classes/java/util/ReverseOrderSortedSetView.java`:
- Around line 133-136: The add method in class ReverseOrderSortedSetView
unconditionally returns true which violates Set.add() semantics; change the
implementation of public boolean add(E e) in ReverseOrderSortedSetView to return
the boolean result produced by base.add(e) (i.e., return base.add(e)) so callers
correctly receive false when the element was already present.
In `@src/java.base/share/classes/java/util/SortedSet.java`:
- Around line 297-302: Remove the misleading `@EnsuresNonEmpty`("this") annotation
from the default addFirst(E e) method in SortedSet (the method currently throws
UnsupportedOperationException and never returns); locate the addFirst method
declaration and delete the `@EnsuresNonEmpty`("this") annotation (and any similar
postcondition annotations on other default methods that unconditionally throw)
so annotations only appear on methods that can return normally and establish the
postcondition.
In `@src/java.base/share/classes/java/util/TreeSet.java`:
- Around line 529-534: The `@EnsuresNonEmpty`("this") postcondition is incorrect
on methods that always throw and never return; remove the
`@EnsuresNonEmpty`("this") annotation from the addFirst(E e) and addLast(E e)
methods in class TreeSet so their declarations only reflect that they throw
UnsupportedOperationException (leave other annotations like
`@DoesNotUnrefineReceiver` if applicable) to avoid misleading static analyzers and
incorrect postcondition assumptions.
---
Duplicate comments:
In `@src/java.base/share/classes/java/util/SortedSet.java`:
- Around line 315-320: The `@EnsuresNonEmpty`("this") on the default
SortedSet.addLast(E) is misleading because the default always throws; remove the
`@EnsuresNonEmpty`("this") annotation from the default addLast method in class
SortedSet (and mirror the same change made for addFirst if present) so the
contract does not falsely claim the receiver becomes non-empty for a method that
never succeeds.
🪄 Autofix (Beta)
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
Run ID: 5fd8b48c-6cae-4daa-afb6-cd14df63f33b
📒 Files selected for processing (32)
src/java.base/share/classes/java/lang/Math.javasrc/java.base/share/classes/java/lang/StrictMath.javasrc/java.base/share/classes/java/math/BigInteger.javasrc/java.base/share/classes/java/util/AbstractCollection.javasrc/java.base/share/classes/java/util/AbstractList.javasrc/java.base/share/classes/java/util/AbstractSequentialList.javasrc/java.base/share/classes/java/util/ArrayDeque.javasrc/java.base/share/classes/java/util/ArrayList.javasrc/java.base/share/classes/java/util/Arrays.javasrc/java.base/share/classes/java/util/BitSet.javasrc/java.base/share/classes/java/util/Collections.javasrc/java.base/share/classes/java/util/ComparableTimSort.javasrc/java.base/share/classes/java/util/DualPivotQuicksort.javasrc/java.base/share/classes/java/util/HashSet.javasrc/java.base/share/classes/java/util/LinkedHashSet.javasrc/java.base/share/classes/java/util/LinkedList.javasrc/java.base/share/classes/java/util/List.javasrc/java.base/share/classes/java/util/ListIterator.javasrc/java.base/share/classes/java/util/NavigableSet.javasrc/java.base/share/classes/java/util/ReverseOrderDequeView.javasrc/java.base/share/classes/java/util/ReverseOrderListView.javasrc/java.base/share/classes/java/util/ReverseOrderSortedSetView.javasrc/java.base/share/classes/java/util/SequencedCollection.javasrc/java.base/share/classes/java/util/Set.javasrc/java.base/share/classes/java/util/SortedSet.javasrc/java.base/share/classes/java/util/TreeSet.javasrc/java.base/share/classes/java/util/Vector.javasrc/java.base/share/classes/java/util/concurrent/BlockingDeque.javasrc/java.base/share/classes/java/util/concurrent/ConcurrentLinkedDeque.javasrc/java.base/share/classes/java/util/concurrent/ConcurrentSkipListSet.javasrc/java.base/share/classes/java/util/concurrent/CopyOnWriteArrayList.javasrc/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java
💤 Files with no reviewable changes (1)
- src/java.base/share/classes/java/util/HashSet.java
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
src/java.base/share/classes/java/util/ListIterator.java (1)
31-31: 🧹 Nitpick | 🔵 Trivial | 💤 Low valueConsider removing unused import.
The
EnsuresNonEmptyimport appears unused (theaddmethod uses@CFCommentto explain why it's not used, and onlyEnsuresNonEmptyIffrom this package is actually applied).♻️ Optional cleanup
-import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;🤖 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 `@src/java.base/share/classes/java/util/ListIterator.java` at line 31, The import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty is unused; remove that import line and keep the actual applied annotation EnsuresNonEmptyIf and the CFComment on the add method as-is so behavior and documentation stay unchanged—locate the unused import statement and delete it, leaving other annotations and the add method untouched.
🤖 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 `@src/java.base/share/classes/java/util/ListIterator.java`:
- Line 38: Remove the commented-out import for SideEffectsOnly (the line "//
import org.checkerframework.dataflow.qual.SideEffectsOnly;") from
ListIterator.java; if the SideEffectsOnly annotation and its commented usages
elsewhere in the file are not needed, delete this commented import (and
optionally any remaining commented annotation usages) to clean up the file and
avoid confusion.
---
Outside diff comments:
In `@src/java.base/share/classes/java/util/ListIterator.java`:
- Line 31: The import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty
is unused; remove that import line and keep the actual applied annotation
EnsuresNonEmptyIf and the CFComment on the add method as-is so behavior and
documentation stay unchanged—locate the unused import statement and delete it,
leaving other annotations and the add method untouched.
🪄 Autofix (Beta)
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
Run ID: 311d735a-635a-4053-930f-87e6e2cf2c02
📒 Files selected for processing (4)
src/java.base/share/classes/java/util/ComparableTimSort.javasrc/java.base/share/classes/java/util/DualPivotQuicksort.javasrc/java.base/share/classes/java/util/ListIterator.javasrc/java.base/share/classes/java/util/TreeMap.java
1 participant
No description provided.