@Shrinkable annotations

Author: mernst

README.md

@@ -133,8 +133,8 @@ jar tf checker-qual.jar | grep '\.java$' | sed 's/\/[^/]*\.java/;/' | sed 's/\//
 The result of the command will be a list of export lines.
 Replace the existing export lines present in
 `src/java.base/share/classes/module-info.java` with the newly-generated list of
-exports. If no new packages were added, then there are likely going to be no
-changes to the `module-info.java` file.
+exports. If no new packages were added, then likely no changes are needed
+in the `module-info.java` file.
 
 Commit the changes, including the new `checker.jar` file and any new `.java`
 files in a `qual/` directory.  (Both are used, by different parts of the build.)

checker-qual.jar

@@ -24,6 +24,7 @@
  */
 package java.lang;
 
+import org.checkerframework.checker.index.qual.PolyGrowShrink;
 import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
 import org.checkerframework.common.aliasing.qual.NonLeaked;
 import org.checkerframework.framework.qual.AnnotatedFor;
@@ -50,7 +51,7 @@ public interface Iterable<T> {
      *
      * @return an Iterator.
      */
-    @PolyNonEmpty Iterator<T> iterator(@PolyNonEmpty Iterable<T> this);
+    @PolyGrowShrink @PolyNonEmpty Iterator<T> iterator(@PolyGrowShrink @PolyNonEmpty Iterable<T> this);
 
     /**
      * Performs the given action for each element of the {@code Iterable}

src/java.base/share/classes/java/lang/Iterable.java

@@ -26,6 +26,8 @@
 package java.util;
 
 import org.checkerframework.checker.index.qual.NonNegative;
+import org.checkerframework.checker.index.qual.PolyGrowShrink;
+import org.checkerframework.checker.index.qual.Shrinkable;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;
 import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
@@ -92,7 +94,7 @@ protected AbstractCollection() {
      * @return an iterator over the elements contained in this collection
      */
     @SideEffectFree
-    public abstract @PolyNonEmpty Iterator<E> iterator(@PolyNonEmpty AbstractCollection<E> this);
+    public abstract @PolyGrowShrink @PolyNonEmpty Iterator<E> iterator(@PolyGrowShrink @PolyNonEmpty AbstractCollection<E> this);
 
     @Pure
     public abstract @NonNegative int size(@GuardSatisfied AbstractCollection<E> this);
@@ -292,7 +294,7 @@ public boolean add(@GuardSatisfied AbstractCollection<E> this, E e) {
      * @throws ClassCastException            {@inheritDoc}
      * @throws NullPointerException          {@inheritDoc}
      */
-    public boolean remove(@GuardSatisfied AbstractCollection<E> this, @GuardSatisfied @UnknownSignedness Object o) {
+    public boolean remove(@GuardSatisfied @Shrinkable AbstractCollection<E> this, @GuardSatisfied @UnknownSignedness Object o) {
         Iterator<E> it = iterator();
         if (o==null) {
             while (it.hasNext()) {
@@ -385,7 +387,7 @@ public boolean addAll(@GuardSatisfied AbstractCollection<E> this, Collection<? e
      * @see #remove(Object)
      * @see #contains(Object)
      */
-    public boolean removeAll(@GuardSatisfied AbstractCollection<E> this, Collection<? extends @UnknownSignedness Object> c) {
+    public boolean removeAll(@GuardSatisfied @Shrinkable AbstractCollection<E> this, Collection<? extends @UnknownSignedness Object> c) {
         Objects.requireNonNull(c);
         boolean modified = false;
         Iterator<?> it = iterator();
@@ -420,7 +422,7 @@ public boolean removeAll(@GuardSatisfied AbstractCollection<E> this, Collection<
      * @see #remove(Object)
      * @see #contains(Object)
      */
-    public boolean retainAll(@GuardSatisfied AbstractCollection<E> this, Collection<? extends @UnknownSignedness Object> c) {
+    public boolean retainAll(@GuardSatisfied @Shrinkable AbstractCollection<E> this, Collection<? extends @UnknownSignedness Object> c) {
         Objects.requireNonNull(c);
         boolean modified = false;
         Iterator<E> it = iterator();
@@ -449,7 +451,7 @@ public boolean retainAll(@GuardSatisfied AbstractCollection<E> this, Collection<
      *
      * @throws UnsupportedOperationException {@inheritDoc}
      */
-    public void clear(@GuardSatisfied AbstractCollection<E> this) {
+    public void clear(@GuardSatisfied @Shrinkable AbstractCollection<E> this) {
         Iterator<E> it = iterator();
         while (it.hasNext()) {
             it.next();

src/java.base/share/classes/java/util/AbstractCollection.java

@@ -28,10 +28,13 @@
 import org.checkerframework.checker.index.qual.GTENegativeOne;
 import org.checkerframework.checker.index.qual.IndexFor;
 import org.checkerframework.checker.index.qual.IndexOrHigh;
+import org.checkerframework.checker.index.qual.PolyGrowShrink;
+import org.checkerframework.checker.index.qual.Shrinkable;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;
 import org.checkerframework.checker.nonempty.qual.NonEmpty;
+import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signedness.qual.UnknownSignedness;
 import org.checkerframework.dataflow.qual.Pure;
@@ -183,7 +186,7 @@ public void add(@GuardSatisfied AbstractList<E> this, @IndexOrHigh({"this"}) int
      * @throws UnsupportedOperationException {@inheritDoc}
      * @throws IndexOutOfBoundsException     {@inheritDoc}
      */
-    public E remove(@GuardSatisfied AbstractList<E> this, @IndexFor({"this"}) int index) {
+    public E remove(@GuardSatisfied @Shrinkable AbstractList<E> this, @IndexFor({"this"}) int index) {
         throw new UnsupportedOperationException();
     }
 
@@ -261,7 +264,7 @@ public E remove(@GuardSatisfied AbstractList<E> this, @IndexFor({"this"}) int in
      * @throws UnsupportedOperationException if the {@code clear} operation
      *         is not supported by this list
      */
-    public void clear(@GuardSatisfied AbstractList<E> this) {
+    public void clear(@GuardSatisfied @Shrinkable AbstractList<E> this) {
         removeRange(0, size());
     }
 
@@ -318,7 +321,7 @@ public boolean addAll(@GuardSatisfied AbstractList<E> this, @IndexOrHigh({"this"
      * @return an iterator over the elements in this list in proper sequence
      */
     @SideEffectFree
-    public Iterator<E> iterator() {
+    public @PolyGrowShrink @PolyNonEmpty Iterator<E> iterator(@PolyGrowShrink @PolyNonEmpty AbstractList<E> this) {
         return new Itr();
     }
 
@@ -330,7 +333,7 @@ public Iterator<E> iterator() {
      *
      * @see #listIterator(int)
      */
-    public ListIterator<E> listIterator() {
+    public @PolyGrowShrink @PolyNonEmpty ListIterator<E> listIterator(@PolyGrowShrink @PolyNonEmpty AbstractList<E> this) {
         return listIterator(0);
     }
 
@@ -357,7 +360,7 @@ public ListIterator<E> listIterator() {
      *
      * @throws IndexOutOfBoundsException {@inheritDoc}
      */
-    public ListIterator<E> listIterator(final @IndexOrHigh({"this"}) int index) {
+    public @PolyGrowShrink ListIterator<E> listIterator(@PolyGrowShrink AbstractList<E> this, final @IndexOrHigh({"this"}) int index) {
         rangeCheckForAdd(index);
 
         return new ListItr(index);
@@ -520,7 +523,7 @@ public void add(E e) {
      *         {@code (fromIndex > toIndex)}
      */
     @SideEffectFree
-    public List<E> subList(@GuardSatisfied AbstractList<E> this, @IndexOrHigh({"this"}) int fromIndex, @IndexOrHigh({"this"}) int toIndex) {
+    public @PolyGrowShrink List<E> subList(@GuardSatisfied @PolyGrowShrink AbstractList<E> this, @IndexOrHigh({"this"}) int fromIndex, @IndexOrHigh({"this"}) int toIndex) {
         subListRangeCheck(fromIndex, toIndex, size());
         return (this instanceof RandomAccess ?
                 new RandomAccessSubList<>(this, fromIndex, toIndex) :
@@ -620,7 +623,7 @@ public int hashCode(@GuardSatisfied AbstractList<E> this) {
      * @param fromIndex index of first element to be removed
      * @param toIndex index after last element to be removed
      */
-    protected void removeRange(@IndexOrHigh({"this"}) int fromIndex, @IndexOrHigh({"this"}) int toIndex) {
+    protected void removeRange(@GuardSatisfied @Shrinkable AbstractList<E> this, @IndexOrHigh({"this"}) int fromIndex, @IndexOrHigh({"this"}) int toIndex) {
         ListIterator<E> it = listIterator(fromIndex);
         for (int i=0, n=toIndex-fromIndex; i<n; i++) {
             it.next();

src/java.base/share/classes/java/util/AbstractList.java

@@ -35,6 +35,7 @@
 
 package java.util;
 
+import org.checkerframework.checker.index.qual.Shrinkable;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty;
 import org.checkerframework.checker.nonempty.qual.NonEmpty;
@@ -116,7 +117,7 @@ public boolean add(@GuardSatisfied AbstractQueue<E> this, E e) {
      * @return the head of this queue
      * @throws NoSuchElementException if this queue is empty
      */
-    public E remove(@GuardSatisfied @NonEmpty AbstractQueue<E> this) {
+    public E remove(@GuardSatisfied @NonEmpty @Shrinkable AbstractQueue<E> this) {
         E x = poll();
         if (x != null)
             return x;
@@ -150,7 +151,7 @@ public E element(@GuardSatisfied @NonEmpty AbstractQueue<E> this) {
      * <p>This implementation repeatedly invokes {@link #poll poll} until it
      * returns {@code null}.
      */
-    public void clear(@GuardSatisfied AbstractQueue<E> this) {
+    public void clear(@GuardSatisfied @Shrinkable AbstractQueue<E> this) {
         while (poll() != null)
             ;
     }

src/java.base/share/classes/java/util/AbstractQueue.java

@@ -25,7 +25,10 @@
 
 package java.util;
 
+import org.checkerframework.checker.index.qual.PolyGrowShrink;
+import org.checkerframework.checker.index.qual.Shrinkable;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
+import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
@@ -175,7 +178,7 @@ public void add(@GuardSatisfied AbstractSequentialList<E> this, int index, E ele
      * @throws UnsupportedOperationException {@inheritDoc}
      * @throws IndexOutOfBoundsException     {@inheritDoc}
      */
-    public E remove(@GuardSatisfied AbstractSequentialList<E> this, int index) {
+    public E remove(@GuardSatisfied @Shrinkable AbstractSequentialList<E> this, int index) {
         try {
             ListIterator<E> e = listIterator(index);
             E outCast = e.next();
@@ -244,7 +247,7 @@ public boolean addAll(@GuardSatisfied AbstractSequentialList<E> this, int index,
      * @return an iterator over the elements in this list (in proper sequence)
      */
     @SideEffectFree
-    public Iterator<E> iterator() {
+    public @PolyGrowShrink @PolyNonEmpty Iterator<E> iterator(@PolyGrowShrink @PolyNonEmpty AbstractSequentialList<E> this) {
         return listIterator();
     }
 
@@ -258,5 +261,5 @@ public Iterator<E> iterator() {
      *         sequence)
      * @throws IndexOutOfBoundsException {@inheritDoc}
      */
-    public abstract ListIterator<E> listIterator(int index);
+    public abstract @PolyGrowShrink ListIterator<E> listIterator(@PolyGrowShrink AbstractSequentialList<E> this, int index);
 }

src/java.base/share/classes/java/util/AbstractSequentialList.java

@@ -35,6 +35,8 @@
 package java.util;
 
 import org.checkerframework.checker.index.qual.NonNegative;
+import org.checkerframework.checker.index.qual.PolyGrowShrink;
+import org.checkerframework.checker.index.qual.Shrinkable;
 import org.checkerframework.checker.lock.qual.GuardSatisfied;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty;
 import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf;
@@ -375,7 +377,7 @@ public boolean offerLast(E e) {
     /**
      * @throws NoSuchElementException {@inheritDoc}
      */
-    public E removeFirst(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
+    public E removeFirst(@GuardSatisfied @NonEmpty @Shrinkable ArrayDeque<E> this) {
         E e = pollFirst();
         if (e == null)
             throw new NoSuchElementException();
@@ -385,14 +387,14 @@ public E removeFirst(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
     /**
      * @throws NoSuchElementException {@inheritDoc}
      */
-    public E removeLast(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
+    public E removeLast(@GuardSatisfied @NonEmpty @Shrinkable ArrayDeque<E> this) {
         E e = pollLast();
         if (e == null)
             throw new NoSuchElementException();
         return e;
     }
 
-    public @Nullable E pollFirst(@GuardSatisfied ArrayDeque<E> this) {
+    public @Nullable E pollFirst(@GuardSatisfied @Shrinkable ArrayDeque<E> this) {
         final Object[] es;
         final int h;
         E e = elementAt(es = elements, h = head);
@@ -403,7 +405,7 @@ public E removeLast(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
         return e;
     }
 
-    public @Nullable E pollLast(@GuardSatisfied ArrayDeque<E> this) {
+    public @Nullable E pollLast(@GuardSatisfied @Shrinkable ArrayDeque<E> this) {
         final Object[] es;
         final int t;
         E e = elementAt(es = elements, t = dec(tail, es.length));
@@ -456,7 +458,7 @@ public E getLast(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
      * @param o element to be removed from this deque, if present
      * @return {@code true} if the deque contained the specified element
      */
-    public boolean removeFirstOccurrence(@GuardSatisfied ArrayDeque<E> this, @Nullable Object o) {
+    public boolean removeFirstOccurrence(@GuardSatisfied @Shrinkable ArrayDeque<E> this, @GuardSatisfied @Nullable @UnknownSignedness Object o) {
         if (o != null) {
             final Object[] es = elements;
             for (int i = head, end = tail, to = (i <= end) ? end : es.length;
@@ -484,7 +486,7 @@ public boolean removeFirstOccurrence(@GuardSatisfied ArrayDeque<E> this, @Nullab
      * @param o element to be removed from this deque, if present
      * @return {@code true} if the deque contained the specified element
      */
-    public boolean removeLastOccurrence(@GuardSatisfied ArrayDeque<E> this, @Nullable Object o) {
+    public boolean removeLastOccurrence(@GuardSatisfied @Shrinkable ArrayDeque<E> this, @GuardSatisfied @Nullable @UnknownSignedness Object o) {
         if (o != null) {
             final Object[] es = elements;
             for (int i = tail, end = head, to = (i >= end) ? end : 0;
@@ -541,7 +543,7 @@ public boolean offer(@GuardSatisfied ArrayDeque<E> this, E e) {
      * @return the head of the queue represented by this deque
      * @throws NoSuchElementException {@inheritDoc}
      */
-    public E remove(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
+    public E remove(@GuardSatisfied @NonEmpty @Shrinkable ArrayDeque<E> this) {
         return removeFirst();
     }
 
@@ -555,7 +557,7 @@ public E remove(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
      * @return the head of the queue represented by this deque, or
      *         {@code null} if this deque is empty
      */
-    public @Nullable E poll(@GuardSatisfied ArrayDeque<E> this) {
+    public @Nullable E poll(@GuardSatisfied @Shrinkable ArrayDeque<E> this) {
         return pollFirst();
     }
 
@@ -612,7 +614,7 @@ public void push(@GuardSatisfied ArrayDeque<E> this, E e) {
      *         of the stack represented by this deque)
      * @throws NoSuchElementException {@inheritDoc}
      */
-    public E pop(@GuardSatisfied @NonEmpty ArrayDeque<E> this) {
+    public E pop(@GuardSatisfied @NonEmpty @Shrinkable ArrayDeque<E> this) {
         return removeFirst();
     }
 
@@ -694,11 +696,11 @@ public boolean isEmpty(@GuardSatisfied ArrayDeque<E> this) {
      * @return an iterator over the elements in this deque
      */
     @SideEffectFree
-    public @PolyNonEmpty Iterator<E> iterator(@PolyNonEmpty ArrayDeque<E> this) {
+    public @PolyGrowShrink @PolyNonEmpty Iterator<E> iterator(@PolyGrowShrink @PolyNonEmpty ArrayDeque<E> this) {
         return new DeqIterator();
     }
 
-    public @PolyNonEmpty Iterator<E> descendingIterator(@PolyNonEmpty ArrayDeque<E> this) {
+    public @PolyGrowShrink @PolyNonEmpty Iterator<E> descendingIterator(@PolyGrowShrink @PolyNonEmpty ArrayDeque<E> this) {
         return new DescendingIterator();
     }
 
@@ -927,23 +929,23 @@ public void forEach(Consumer<? super E> action) {
     /**
      * @throws NullPointerException {@inheritDoc}
      */
-    public boolean removeIf(Predicate<? super E> filter) {
+    public boolean removeIf(@Shrinkable ArrayDeque<E> this, Predicate<? super E> filter) {
         Objects.requireNonNull(filter);
         return bulkRemove(filter);
     }
 
     /**
      * @throws NullPointerException {@inheritDoc}
      */
-    public boolean removeAll(Collection<? extends @UnknownSignedness Object> c) {
+    public boolean removeAll(@Shrinkable ArrayDeque<E> this, Collection<? extends @UnknownSignedness Object> c) {
         Objects.requireNonNull(c);
         return bulkRemove(e -> c.contains(e));
     }
 
     /**
      * @throws NullPointerException {@inheritDoc}
      */
-    public boolean retainAll(Collection<? extends @UnknownSignedness Object> c) {
+    public boolean retainAll(@GuardSatisfied @Shrinkable ArrayDeque<E> this, Collection<? extends @UnknownSignedness Object> c) {
         Objects.requireNonNull(c);
         return bulkRemove(e -> !c.contains(e));
     }
@@ -1059,15 +1061,15 @@ public boolean contains(@GuardSatisfied ArrayDeque<E> this, @GuardSatisfied @Nul
      * @param o element to be removed from this deque, if present
      * @return {@code true} if this deque contained the specified element
      */
-    public boolean remove(@GuardSatisfied ArrayDeque<E> this, @GuardSatisfied @Nullable @UnknownSignedness Object o) {
+    public boolean remove(@GuardSatisfied @Shrinkable ArrayDeque<E> this, @GuardSatisfied @Nullable @UnknownSignedness Object o) {
         return removeFirstOccurrence(o);
     }
 
     /**
      * Removes all of the elements from this deque.
      * The deque will be empty after this call returns.
      */
-    public void clear(@GuardSatisfied ArrayDeque<E> this) {
+    public void clear(@GuardSatisfied @Shrinkable ArrayDeque<E> this) {
         circularClear(elements, head, tail);
         head = tail = 0;
     }