RLC extension for resource collection

annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Insertions.java

@@ -46,7 +46,9 @@
 import org.checkerframework.afu.scenelib.type.BoundedType;
 import org.checkerframework.afu.scenelib.type.DeclaredType;
 import org.checkerframework.afu.scenelib.type.Type;
+import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection;
 import org.checkerframework.checker.interning.qual.Interned;
+import org.checkerframework.checker.mustcall.qual.NotOwning;
 import org.objectweb.asm.TypePath;
 
 /**
@@ -177,7 +179,7 @@ public int size() {
   }
 
   @Override
-  public Iterator<Insertion> iterator() {
+  public @PolyOwningCollection Iterator<Insertion> iterator(@PolyOwningCollection Insertions this) {
     return new Iterator<Insertion>() {
       private Iterator<Map<String, Set<Insertion>>> miter = store.values().iterator();
       // These two fields are initially empty iterators, but are set the first time that hasNext is
@@ -202,7 +204,7 @@ public boolean hasNext() {
       }
 
       @Override
-      public Insertion next() {
+      public @NotOwning Insertion next() {
         if (hasNext()) {
           return iiter.next();
         }

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java

@@ -60,6 +60,8 @@
 import java.util.List;
 import java.util.NoSuchElementException;
 import java.util.Objects;
+import org.checkerframework.checker.collectionownership.qual.NotOwningCollection;
+import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection;
 import org.plumelib.util.ArraysPlume;
 
 /** A path through the AST. */
@@ -286,7 +288,7 @@ public static Comparator<ASTPath> getComparator() {
 
   // TODO: replace w/ skip list?
   @Override
-  public Iterator<ASTEntry> iterator() {
+  public @PolyOwningCollection Iterator<ASTEntry> iterator(@PolyOwningCollection ASTPath this) {
     ImmutableStack<ASTEntry> s = this;
     int n = size();
     ASTEntry[] a = new ASTEntry[n];
@@ -1357,17 +1359,16 @@ private static <T, S extends ImmutableStack<T>> S extend(T el, S s0) {
    *
    * @return true if the stack is empty
    */
-  public boolean isEmpty() {
+  public boolean isEmpty(@NotOwningCollection ImmutableStack<E> this) {
     return size == 0;
   }
 
   /**
    * Returns the top element of the stack, without modifying the stack.
    *
    * @return the top element of the stack
-   * @throws IllegalStateException if the stack is empty
    */
-  public E peek() {
+  public E peek(@NotOwningCollection ImmutableStack<E> this) {
     if (isEmpty()) {
       throw new IllegalStateException("peek() on empty stack");
     }
@@ -1378,9 +1379,8 @@ public E peek() {
    * Returns all of the stack except the top element.
    *
    * @return all of the stack except the top element
-   * @throws IllegalStateException if the stack is empty
    */
-  public ImmutableStack<E> pop() {
+  public ImmutableStack<E> pop(@NotOwningCollection ImmutableStack<E> this) {
     if (isEmpty()) {
       throw new IllegalStateException("pop() on empty stack");
     }
@@ -1396,7 +1396,7 @@ public ImmutableStack<E> push(E elem) {
    *
    * @return the size of this stack
    */
-  public int size() {
+  public int size(@NotOwningCollection ImmutableStack<E> this) {
     return size;
   }
 
@@ -1405,7 +1405,6 @@ public int size() {
    *
    * @param index which element to return
    * @return the index-th element of this stack
-   * @throws NoSuchElementException if the index is out of bounds
    */
   public E get(int index) {
     int n = size();

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/classfile/ClassAnnotationSceneWriter.java

@@ -27,6 +27,7 @@
 import org.checkerframework.afu.scenelib.field.ArrayAFT;
 import org.checkerframework.afu.scenelib.field.ClassTokenAFT;
 import org.checkerframework.afu.scenelib.field.EnumAFT;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.ClassGetName;
 import org.objectweb.asm.AnnotationVisitor;
 import org.objectweb.asm.Attribute;
@@ -430,7 +431,8 @@ public FieldAnnotationSceneWriter(int api, String name, FieldVisitor fv) {
     }
 
     @Override
-    public AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
+    @SuppressWarnings("nullness:override.return") // ASM lacks (some?) @Nullable annotations
+    public @Nullable AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
       existingFieldAnnotations.add(descriptor);
 
       // If annotation exists in scene, and in overwrite mode,
@@ -443,7 +445,8 @@ public AnnotationVisitor visitAnnotation(String descriptor, boolean visible) {
     }
 
     @Override
-    public AnnotationVisitor visitTypeAnnotation(
+    @SuppressWarnings("nullness:override.return") // ASM lacks (some?) @Nullable annotations
+    public @Nullable AnnotationVisitor visitTypeAnnotation(
         int typeRef, TypePath typePath, String descriptor, boolean visible) {
       // typeRef: FIELD
       existingFieldAnnotations.add(descriptor);

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java

@@ -4,6 +4,10 @@
 import java.util.Collection;
 import java.util.Iterator;
 import java.util.LinkedHashMap;
+import org.checkerframework.checker.collectionownership.qual.NotOwningCollection;
+import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection;
+import org.checkerframework.checker.mustcall.qual.NotOwning;
+import org.checkerframework.checker.mustcall.qual.Owning;
 
 /**
  * A simple implementation of {@link KeyedSet} backed by an insertion-order {@link
@@ -17,7 +21,7 @@ public class LinkedHashKeyedSet<K, V> extends AbstractSet<V> implements KeyedSet
   private final Keyer<? extends K, ? super V> keyer;
 
   /** The map that backs this set. */
-  // Not declared as Map because some implementations of Map prohibit null keys.
+  // Declared as LinkedHashMap because some implementations of Map prohibit null keys.
   private final LinkedHashMap<K, V> theMap = new LinkedHashMap<>();
 
   /** The values in the set. Implemented as a view into the map. */
@@ -50,7 +54,7 @@ public boolean hasNext() {
     }
 
     @Override
-    public V next() {
+    public @NotOwning V next() {
       return itr.next();
     }
 
@@ -63,7 +67,7 @@ public void remove() {
   }
 
   @Override
-  public Iterator<V> iterator() {
+  public Iterator<V> iterator(@PolyOwningCollection LinkedHashKeyedSet<K, V> this) {
     return new KeyedSetIterator();
   }
 
@@ -85,7 +89,8 @@ public <T> T[] toArray(T[] a) {
    * @param old the element to be removed, if {@code behavior} is REPLACE
    * @return true if an element was removed
    */
-  private boolean checkAdd(int behavior, V old) {
+  private boolean checkAdd(
+      @NotOwningCollection LinkedHashKeyedSet<K, V> this, int behavior, V old) {
     return switch (behavior) {
       case REPLACE -> {
         remove(old);
@@ -102,7 +107,11 @@ private static boolean eq(Object x, Object y) {
   }
 
   @Override
-  public V add(V o, int conflictBehavior, int equalBehavior) {
+  public V add(
+      @NotOwningCollection LinkedHashKeyedSet<K, V> this,
+      V o,
+      int conflictBehavior,
+      int equalBehavior) {
     K key = keyer.getKeyFor(o);
     V old = theMap.get(key);
     if (old == null
@@ -112,12 +121,12 @@ public V add(V o, int conflictBehavior, int equalBehavior) {
   }
 
   @Override
-  public boolean add(V o) {
+  public boolean add(@Owning V o) {
     return add(o, THROW_EXCEPTION, IGNORE) == null;
   }
 
   @Override
-  public boolean remove(Object o) {
+  public boolean remove(@NotOwningCollection LinkedHashKeyedSet<K, V> this, Object o) {
     return theValues.remove(o);
   }
 

annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/WrapperMap.java

@@ -3,6 +3,8 @@
 import java.util.Collection;
 import java.util.Map;
 import java.util.Set;
+import org.checkerframework.checker.mustcall.qual.NotOwning;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * A {@link WrapperMap} is a map all of whose methods delegate by default to those of a supplied
@@ -42,7 +44,7 @@ public Set<java.util.Map.Entry<K, V>> entrySet() {
   }
 
   @Override
-  public V get(Object key) {
+  public @NotOwning @Nullable V get(Object key) {
     return back.get(key);
   }
 
@@ -57,7 +59,8 @@ public Set<K> keySet() {
   }
 
   @Override
-  public V put(K key, V value) {
+  @SuppressWarnings("keyfor:contracts.postcondition") // uses a delegate map
+  public @NotOwning @Nullable V put(K key, V value) {
     return back.put(key, value);
   }
 

checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CollectionFieldDestructor.java

@@ -0,0 +1,40 @@
+package org.checkerframework.checker.collectionownership.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
+import org.checkerframework.framework.qual.PostconditionAnnotation;
+
+/**
+ * The annotated method destructs the given resource collection fields. That is, this method calls
+ * all required methods on their elements.
+ *
+ * <pre><code>
+ *  {@literal @}CollectionFieldDestructor("socketList")
+ *  void close() {
+ *    for (Socket s : this.socketList) {
+ *      try {
+ *        s.close();
+ *      } catch (Exception e) {}
+ *    }
+ *  }
+ * </code></pre>
+ *
+ * @checker_framework.manual #resource-leak-checker Resource Leak Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+@PostconditionAnnotation(qualifier = OwningCollectionWithoutObligation.class)
+@InheritedAnnotation
+public @interface CollectionFieldDestructor {
+  /**
+   * Returns the resource collection fields whose collection obligation the destructor fulfills.
+   *
+   * @return the resource collection fields whose collection obligation the destructor fulfills
+   */
+  String[] value();
+}

checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CreatesCollectionObligation.java

@@ -0,0 +1,29 @@
+package org.checkerframework.checker.collectionownership.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
+
+/**
+ * A method carrying this annotation creates a {@code CollectionObligation} for the receiver
+ * collection.
+ *
+ * <p>Consider a call to a {@code CreatesCollectionObligation}-annotated method. If the receiver is
+ * of type {@code @OwningCollectionWithoutObligation}, it is unrefined to {@code @OwningCollection},
+ * and a CollectionObligation is created for each {@code @MustCall} method of the type variable of
+ * the receiver.
+ *
+ * <p>This annotation should only be used on method declarations of collections, as defined by the
+ * CollectionOwnershipChecker, that is, {@code java.lang.Iterable} and {@code java.util.Iterator}
+ * implementations.
+ *
+ * @checker_framework.manual #resource-leak-checker Resource Leak Checker
+ */
+@Documented
+@InheritedAnnotation
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+public @interface CreatesCollectionObligation {}

checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/NotOwningCollection.java

@@ -0,0 +1,21 @@
+package org.checkerframework.checker.collectionownership.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * An expression of type {@code NotOwningCollection} is a non-owning reference to a resource
+ * collection/array. Because it does not own the underlying collection/array, it cannot add or
+ * remove elements from it.
+ *
+ * @checker_framework.manual #resource-leak-checker Resource Leak Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({})
+public @interface NotOwningCollection {}

checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollection.java

@@ -0,0 +1,24 @@
+package org.checkerframework.checker.collectionownership.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * An expression of type {@code @OwningCollection} is a resource collection/array that definitely
+ * owns the underlying collection/array. It can add or remove elements from the collection/array.
+ *
+ * <p>The annotated expression (or one of its aliases) must either call the methods in the
+ * {@code @MustCall} type of its elements on all of its elements, or pass on the obligation to
+ * another expression.
+ *
+ * @checker_framework.manual #resource-leak-checker Resource Leak Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({NotOwningCollection.class})
+public @interface OwningCollection {}

checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionBottom.java

@@ -0,0 +1,30 @@
+package org.checkerframework.checker.collectionownership.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+/**
+ * The bottom qualifier of the Collection Ownership type hierarchy. It is the default qualifier.
+ *
+ * <p>An expression of type {@code @OwningCollectionBottom} is either not a collection/array or is a
+ * collection/array whose elements have empty {@code @MustCall} type.
+ *
+ * @checker_framework.manual #resource-leak-checker Resource Leak Checker
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({OwningCollectionWithoutObligation.class})
+@DefaultQualifierInHierarchy
+@DefaultFor({
+  TypeUseLocation.EXCEPTION_PARAMETER,
+  TypeUseLocation.RESOURCE_VARIABLE,
+  TypeUseLocation.RETURN,
+  TypeUseLocation.UPPER_BOUND
+})
+public @interface OwningCollectionBottom {}