diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Insertions.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Insertions.java index 2f30758984f..33249d23a94 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/find/Insertions.java +++ b/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; /** @@ -185,7 +187,7 @@ public int size() { } @Override - public Iterator iterator() { + public @PolyOwningCollection Iterator iterator(@PolyOwningCollection Insertions this) { return new Iterator() { private Iterator>> miter = store.values().iterator(); // These two fields are initially empty iterators, but are set the first time that hasNext is @@ -210,7 +212,7 @@ public boolean hasNext() { } @Override - public Insertion next() { + public @NotOwning Insertion next() { if (hasNext()) { return iiter.next(); } diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java index 723b027086a..1a19a3e1ae0 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java @@ -61,6 +61,8 @@ import java.util.NoSuchElementException; import java.util.Objects; import org.checkerframework.afu.annotator.find.CaseUtils; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; +import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection; import org.plumelib.util.ArraysPlume; /** A path through the AST. */ @@ -295,7 +297,7 @@ public static Comparator getComparator() { // TODO: replace w/ skip list? @Override - public Iterator iterator() { + public @PolyOwningCollection Iterator iterator(@PolyOwningCollection ASTPath this) { ImmutableStack s = this; int n = size(); ASTEntry[] a = new ASTEntry[n]; @@ -1465,7 +1467,7 @@ private static > S extend(T el, S s0) { * * @return true if the stack is empty */ - public boolean isEmpty() { + public boolean isEmpty(@NotOwningCollection ImmutableStack this) { return size == 0; } @@ -1473,9 +1475,8 @@ public boolean isEmpty() { * 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 this) { if (isEmpty()) { throw new IllegalStateException("peek() on empty stack"); } @@ -1486,9 +1487,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 pop() { + public ImmutableStack pop(@NotOwningCollection ImmutableStack this) { if (isEmpty()) { throw new IllegalStateException("pop() on empty stack"); } @@ -1504,7 +1504,7 @@ public ImmutableStack push(E elem) { * * @return the size of this stack */ - public int size() { + public int size(@NotOwningCollection ImmutableStack this) { return size; } @@ -1513,7 +1513,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(); diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/classfile/ClassAnnotationSceneWriter.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/classfile/ClassAnnotationSceneWriter.java index 48d25fca072..b3c2ba9f7bf 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/classfile/ClassAnnotationSceneWriter.java +++ b/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); diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java index 4d1497ba5fb..18ea4b261f7 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java +++ b/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.OwningCollection; +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 extends AbstractSet implements KeyedSet private final Keyer 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 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 iterator() { + public Iterator iterator(@PolyOwningCollection LinkedHashKeyedSet this) { return new KeyedSetIterator(); } @@ -85,7 +89,7 @@ public 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(@OwningCollection LinkedHashKeyedSet this, int behavior, V old) { switch (behavior) { case REPLACE: remove(old); @@ -104,7 +108,11 @@ private static boolean eq(Object x, Object y) { } @Override - public V add(V o, int conflictBehavior, int equalBehavior) { + public V add( + @OwningCollection LinkedHashKeyedSet this, + V o, + int conflictBehavior, + int equalBehavior) { K key = keyer.getKeyFor(o); V old = theMap.get(key); if (old == null @@ -114,12 +122,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(@OwningCollection LinkedHashKeyedSet this, Object o) { return theValues.remove(o); } diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/WrapperMap.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/WrapperMap.java index 3d88f84d172..b826e9861bc 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/WrapperMap.java +++ b/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 @@ -39,7 +41,7 @@ public Set> entrySet() { } @Override - public V get(Object key) { + public @NotOwning @Nullable V get(Object key) { return back.get(key); } @@ -54,7 +56,8 @@ public Set 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); } diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CollectionFieldDestructor.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CollectionFieldDestructor.java new file mode 100644 index 00000000000..0453b4ff3b3 --- /dev/null +++ b/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. + * + * 

+ *  {@literal @}CollectionFieldDestructor("socketList")
+ *  void close() {
+ *    for (Socket s : this.socketList) {
+ *      try {
+ *        s.close();
+ *      } catch (Exception e) {}
+ *    }
+ *  }
+ *
+ * + * @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(); +} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CreatesCollectionObligation.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/CreatesCollectionObligation.java new file mode 100644 index 00000000000..ad68ff3246c --- /dev/null +++ b/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. + * + *

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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/NotOwningCollection.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/NotOwningCollection.java new file mode 100644 index 00000000000..3ac85e3d0a8 --- /dev/null +++ b/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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollection.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollection.java new file mode 100644 index 00000000000..721ebdeef6c --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionBottom.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionBottom.java new file mode 100644 index 00000000000..dcfe1b75c4d --- /dev/null +++ b/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. + * + *

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 {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionWithoutObligation.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionWithoutObligation.java new file mode 100644 index 00000000000..13c0f8b4d46 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/OwningCollectionWithoutObligation.java @@ -0,0 +1,26 @@ +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 @OwningCollectionWithoutObligation} is a resource collection/array, + * which definitely owns the underlying collection/array. Furthermore, every element has already + * called all of the methods in its {@code @MustCall} type. + * + *

Consider a destructor method {@code d} of a class {@code C} with an {@code @OwningCollection} + * field {@code f}. The post-condition of the destructor method is + * {@code @EnsuresQualifier(expression = "this.f", qualifier = + * OwningCollectionWithoutObligation.class)}. + * + * @checker_framework.manual #resource-leak-checker Resource Leak Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({OwningCollection.class}) +public @interface OwningCollectionWithoutObligation {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/PolyOwningCollection.java b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/PolyOwningCollection.java new file mode 100644 index 00000000000..a0d64255ebf --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/collectionownership/qual/PolyOwningCollection.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.PolymorphicQualifier; + +/** + * A polymorphic qualifier for the Collection-Ownership type system. + * + * @checker_framework.manual #resource-leak-checker Resource Leak Checker + * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism + * @see NotOwningCollection + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@PolymorphicQualifier(NotOwningCollection.class) +public @interface PolyOwningCollection {} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnalysis.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnalysis.java new file mode 100644 index 00000000000..14a4fe97b6b --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnalysis.java @@ -0,0 +1,49 @@ +package org.checkerframework.checker.collectionownership; + +import javax.lang.model.type.TypeMirror; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.javacutil.AnnotationMirrorSet; + +/** + * The analysis class for the collection ownership type system. + * + *

This class extends {@link CFAbstractAnalysis} so that {@link CollectionOwnershipStore} is used + * rather than {@link CFStore}. + */ +public class CollectionOwnershipAnalysis + extends CFAbstractAnalysis { + + /** + * Creates a new {@link CollectionOwnershipAnalysis}. + * + * @param checker the checker + * @param factory the factory + */ + public CollectionOwnershipAnalysis( + BaseTypeChecker checker, CollectionOwnershipAnnotatedTypeFactory factory) { + super(checker, factory); + } + + @Override + public CollectionOwnershipTransfer createTransferFunction() { + return new CollectionOwnershipTransfer(this, (CollectionOwnershipChecker) checker); + } + + @Override + public CollectionOwnershipStore createEmptyStore(boolean sequentialSemantics) { + return new CollectionOwnershipStore(this, sequentialSemantics); + } + + @Override + public CollectionOwnershipStore createCopiedStore(CollectionOwnershipStore s) { + return new CollectionOwnershipStore(this, s); + } + + @Override + public CFValue createAbstractValue(AnnotationMirrorSet annotations, TypeMirror underlyingType) { + return getCfValue(this, annotations, underlyingType); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java new file mode 100644 index 00000000000..80992324146 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java @@ -0,0 +1,745 @@ +package org.checkerframework.checker.collectionownership; + +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; +import java.lang.annotation.Annotation; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.DeclaredType; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; +import org.checkerframework.checker.collectionownership.qual.CollectionFieldDestructor; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; +import org.checkerframework.checker.collectionownership.qual.OwningCollection; +import org.checkerframework.checker.collectionownership.qual.OwningCollectionBottom; +import org.checkerframework.checker.collectionownership.qual.OwningCollectionWithoutObligation; +import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection; +import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer; +import org.checkerframework.checker.resourceleak.MustCallInference; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; +import org.checkerframework.checker.resourceleak.ResourceLeakUtils; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory.PotentiallyFulfillingLoop; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.dataflow.cfg.ControlFlowGraph; +import org.checkerframework.dataflow.cfg.UnderlyingAST; +import org.checkerframework.dataflow.cfg.block.Block; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.expression.JavaExpressionParseException; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.TypeAnnotator; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.framework.util.StringToJavaExpression; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; + +/** The annotated type factory for the Collection Ownership Checker. */ +public class CollectionOwnershipAnnotatedTypeFactory + extends GenericAnnotatedTypeFactory< + CFValue, + CollectionOwnershipStore, + CollectionOwnershipTransfer, + CollectionOwnershipAnalysis> { + + /** + * The {@code @} {@link MustCallAnnotatedTypeFactory} instance in the checker hierarchy. Used for + * getting the {@code @MustCall} type of expressions. + */ + private final MustCallAnnotatedTypeFactory mcAtf; + + /** The {@code @}{@link NotOwningCollection} annotation. */ + public final AnnotationMirror TOP; + + /** The {@code @}{@link NotOwningCollection} annotation. Equals TOP. */ + public final AnnotationMirror NOTOWNINGCOLLECTION; + + /** The {@code @}{@link OwningCollection} annotation. */ + public final AnnotationMirror OWNINGCOLLECTION; + + /** The {@code @}{@link OwningCollectionWithoutObligation} annotation. */ + public final AnnotationMirror OWNINGCOLLECTIONWITHOUTOBLIGATION; + + /** + * The {@code @}{@link OwningCollectionBottom}{@code ()} annotation. It is the default in + * unannotated code. + */ + public final AnnotationMirror BOTTOM; + + /** The {@code @}{@link PolyOwningCollection}{@code ()} polymorphic annotation. */ + public final AnnotationMirror POLY; + + /** The value element of the {@code @}{@link CollectionFieldDestructor} annotation. */ + private final ExecutableElement collectionFieldDestructorValueElement = + TreeUtils.getMethod(CollectionFieldDestructor.class, "value", 0, processingEnv); + + /** + * Enum for the types in the hierarchy. Combined with a few utility methods to get the right enum + * value from various sources, this is a convenient interface to deal with annotations in this + * hierarchy. + */ + public enum CollectionOwnershipType { + /** The @NotOwningCollection type. */ + NotOwningCollection, + /** The @OwningCollection type. */ + OwningCollection, + /** The @OwningCollectionWithoutObligation type. */ + OwningCollectionWithoutObligation, + /** The @OwningCollectionBottom type. */ + OwningCollectionBottom + }; + + /** + * The method name used for CollectionObligations that represent an obligation of MustCallUnkown. + * The digit in the first character ensures this cannot coincide with an actual method name. + */ + public static final String UNKNOWN_METHOD_NAME = "1UNKNOWN"; + + /** + * Maps the AST-tree corresponding to the loop condition of a collection-obligation-fulfilling + * loop to the loop wrapper. + */ + private static Map conditionToFulfillingLoopMap = + new HashMap<>(); + + /** + * Maps the cfg-block corresponding to the loop conditional block of a + * collection-obligation-fulfilling loop to the loop wrapper. + */ + private static Map conditionalBlockToFulfillingLoopMap = + new HashMap<>(); + + /** + * Marks the specified loop as fulfilling a collection obligation. + * + * @param loop the loop wrapper + */ + public static void markFulfillingLoop(PotentiallyFulfillingLoop loop) { + conditionToFulfillingLoopMap.put(loop.condition, loop); + conditionalBlockToFulfillingLoopMap.put(loop.loopConditionalBlock, loop); + } + + /** + * Returns the collection-obligation-fulfilling loop for which the given tree is the condition. + * + * @param tree a tree that is potentially the condition for a fulfilling loop + * @return the collection-obligation-fulfilling loop for which the given tree is the condition + */ + public static PotentiallyFulfillingLoop getFulfillingLoopForCondition(Tree tree) { + return conditionToFulfillingLoopMap.get(tree); + } + + /** + * Returns the collection-obligation-fulfilling loop for which the given block is the CFG + * conditional block. + * + * @param block the block that is potentially the conditional block for a fulfilling loop + * @return the collection-obligation-fulfilling loop for which the given block is the CFG + * conditional block + */ + public static PotentiallyFulfillingLoop getFulfillingLoopForConditionalBlock(Block block) { + return conditionalBlockToFulfillingLoopMap.get(block); + } + + /** + * Creates a CollectionOwnershipAnnotatedTypeFactory. + * + * @param checker the checker associated with this type factory + */ + @SuppressWarnings("this-escape") + public CollectionOwnershipAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + NOTOWNINGCOLLECTION = AnnotationBuilder.fromClass(elements, NotOwningCollection.class); + TOP = NOTOWNINGCOLLECTION; + OWNINGCOLLECTION = AnnotationBuilder.fromClass(elements, OwningCollection.class); + OWNINGCOLLECTIONWITHOUTOBLIGATION = + AnnotationBuilder.fromClass(elements, OwningCollectionWithoutObligation.class); + BOTTOM = AnnotationBuilder.fromClass(elements, OwningCollectionBottom.class); + POLY = AnnotationBuilder.fromClass(elements, PolyOwningCollection.class); + mcAtf = ResourceLeakUtils.getMustCallAnnotatedTypeFactory(checker); + this.postInit(); + } + + @Override + protected Set> createSupportedTypeQualifiers() { + return new LinkedHashSet<>( + Arrays.asList( + PolyOwningCollection.class, + NotOwningCollection.class, + OwningCollection.class, + OwningCollectionWithoutObligation.class, + OwningCollectionBottom.class)); + } + + /** + * Fetches the store from the results of dataflow for {@code firstBlock}. If {@code + * afterFirstStore} is true, then the store after {@code firstBlock} is returned; if {@code + * afterFirstStore} is false, the store before {@code succBlock} is returned. + * + * @param afterFirstStore if true, use the store after the first block or the store before its + * successor, succBlock + * @param firstBlock a block + * @param succBlock {@code firstBlock}'s successor + * @return the appropriate CollectionOwnershipStore, populated with MustCall annotations, from the + * results of running dataflow + */ + public CollectionOwnershipStore getStoreForBlock( + boolean afterFirstStore, Block firstBlock, Block succBlock) { + return afterFirstStore + ? flowResult.getStoreAfter(firstBlock) + : flowResult.getStoreBefore(succBlock); + } + + // Note that this method is overridden here because the collections ownership + // typechecker runs last in the RLC, not because this has anything to do with + // collections. Whatever checker runs last in the RLC must do this. TODO: make this + // run last in a more sensible way. + @Override + public void postAnalyze(ControlFlowGraph cfg) { + ResourceLeakChecker rlc = ResourceLeakUtils.getResourceLeakChecker(this); + rlc.setRoot(root); + MustCallConsistencyAnalyzer mustCallConsistencyAnalyzer = + new MustCallConsistencyAnalyzer(rlc, false); + mustCallConsistencyAnalyzer.analyze(cfg); + RLCCalledMethodsAnnotatedTypeFactory cmAtf = + (RLCCalledMethodsAnnotatedTypeFactory) + ResourceLeakUtils.getRLCCalledMethodsChecker(this).getTypeFactory(); + // Inferring owning annotations for @Owning fields/parameters, @EnsuresCalledMethods for + // finalizer methods, and @InheritableMustCall annotations for the class declarations. + if (cmAtf.getWholeProgramInference() != null) { + if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { + MustCallInference.runMustCallInference(cmAtf, cfg, mustCallConsistencyAnalyzer); + } + } + + super.postAnalyze(cfg); + } + + /** + * Returns true if the given type is a resource collection: a type assignable from {@code + * Collection} whose single type var has non-empty MustCall type. + * + *

This overload should be used only before computation of AnnotatedTypeMirrors is completed, + * in particular in addComputedTypeAnnotations(AnnotatedTypeMirror). + * + * @param t the AnnotatedTypeMirror + * @return true if t is a resource collection + */ + public boolean isResourceCollection(TypeMirror t) { + List mcValues = getMustCallValuesOfResourceCollectionComponent(t); + return mcValues != null && mcValues.size() > 0; + } + + /** + * Returns true if the given element is a resource collection field that is declared as + * {@code @OwningCollection}. Since that is the default, this method also returns true if the + * field has no collection ownership annotation. + * + * @param elt a field that might be a resource collection + * @return true if the element is a resource collection field that is {@code @OwningCollection} by + * declaration + */ + public boolean isOwningCollectionField(Element elt) { + if (elt == null) { + return false; + } + if (elt.getKind().isField()) { + if (isResourceCollection(elt.asType())) { + AnnotatedTypeMirror atm = getAnnotatedType(elt); + CollectionOwnershipType fieldType = + getCoType(Collections.singletonList(atm.getPrimaryAnnotationInHierarchy(TOP))); + if (fieldType == null) { + return false; + } + switch (fieldType) { + case OwningCollection: + case OwningCollectionWithoutObligation: + return true; + default: + return false; + } + } + } + return false; + } + + /** + * Returns true if the given element is a resource collection field. + * + * @param elt an element + * @return true if the element is a resource collection field + */ + public boolean isResourceCollectionField(Element elt) { + if (elt.getKind().isField()) { + if (isResourceCollection(elt.asType())) { + return true; + } + } + return false; + } + + /** + * Returns true if the given element is a resource collection parameter that is declared as + * {@code @OwningCollection}. Since that is the default, this method also returns true if the + * parameter has no collection ownership annotation. + * + * @param elt an element + * @return true if the element is a resource collection parameter that is + * {@code @OwningCollection} by declaration + */ + public boolean isOwningCollectionParameter(Element elt) { + if (isResourceCollection(elt.asType())) { + if (elt.getKind() == ElementKind.PARAMETER) { + AnnotatedTypeMirror atm = getAnnotatedType(elt); + CollectionOwnershipType paramType = + getCoType(Collections.singletonList(atm.getPrimaryAnnotationInHierarchy(TOP))); + if (paramType == null) { + return false; + } + switch (paramType) { + case OwningCollection: + return true; + default: + return false; + } + } + } + return false; + } + + /** + * Returns true if the given AST tree is a resource collection. + * + *

That is, whether the given tree is of a type assignable from java.util.Collection, whose + * only type var has non-empty MustCall type. + * + * @param tree the tree + * @return true if the tree is a resource collection + */ + public boolean isResourceCollection(Tree tree) { + if (tree == null) { + return false; + } + AnnotatedTypeMirror treeMcType; + try { + treeMcType = mcAtf.getAnnotatedType(tree); + } catch (BugInCF e) { + // this happens if the tree is not of a supported format, thrown by + // AnnotatedTypeFactory#getAnnotatedType + treeMcType = null; + } + List mcValues = getMustCallValuesOfResourceCollectionComponent(treeMcType); + return mcValues != null && mcValues.size() > 0; + } + + /** + * If the given type is a collection, this method returns the MustCall values of its elements or + * null if there are none or if the given type is not a collection. + * + *

That is, if the given type is a Java.util.Collection implementation, this method returns the + * MustCall values of its type variable upper bound if there are any or else null. + * + * @param atm the AnnotatedTypeMirror + * @return if the given type is a collection, returns the MustCall values of its elements or null + * if there are none or if the given type is not a collection + */ + public List getMustCallValuesOfResourceCollectionComponent(AnnotatedTypeMirror atm) { + if (atm == null) { + return null; + } + boolean isCollectionType = ResourceLeakUtils.isCollection(atm.getUnderlyingType()); + + AnnotatedTypeMirror componentType = null; + if (isCollectionType) { + List typeArgs = + ((AnnotatedDeclaredType) atm).getTypeArguments(); + if (typeArgs.size() == 1) { + componentType = typeArgs.get(0); + } + } + + if (componentType != null) { + List list = ResourceLeakUtils.getMcValues(componentType, mcAtf); + return list; + } else { + return null; + } + } + + /** + * If the given tree represents a collection, this method returns the MustCall values of its + * elements. It returns null if there are none or if the given type is not a collection. + * + *

That is, if the given tree is of a Java.util.Collection implementation, this method returns + * the MustCall values of its type variable upper bound if there are any or else null. + * + * @param tree the AST tree + * @return if the given tree represents a collection, returns the MustCall values of its elements + * or null if there are none or if the given type is not a collection + */ + public List getMustCallValuesOfResourceCollectionComponent(Tree tree) { + return getMustCallValuesOfResourceCollectionComponent(mcAtf.getAnnotatedType(tree)); + } + + /** + * If the given type is a collection, this method returns the MustCall values of its elements. It + * returns null if there are none or if the given type is not a collection. + * + *

That is, if the given type is a Java.util.Collection implementation, this method returns the + * MustCall values of its type variable upper bound if there are any or else null. + * + * @param t the TypeMirror + * @return if the given type is a collection, returns the MustCall values of its elements or null + * if there are none or if the given type is not a collection + */ + public List getMustCallValuesOfResourceCollectionComponent(TypeMirror t) { + boolean isCollectionType = ResourceLeakUtils.isCollection(t); + + TypeMirror componentType = null; + if (isCollectionType) { + List typeArgs = ((DeclaredType) t).getTypeArguments(); + if (typeArgs.size() == 1) { + componentType = typeArgs.get(0); + } + } + + if (componentType != null) { + List list = ResourceLeakUtils.getMcValues(componentType, mcAtf); + return list; + } else { + return null; + } + } + + /** + * Returns the flow-sensitive {@code CollectionOwnershipType} that the given node has in the given + * store. + * + * @param node the node + * @param coStore the store + * @return the {@code CollectionOwnershipType} that the given node has in the given store + */ + public CollectionOwnershipType getCoType(Node node, CollectionOwnershipStore coStore) { + JavaExpression jx = JavaExpression.fromNode(node); + CFValue storeVal; + try { + storeVal = coStore.getValue(jx); + } catch (BugInCF e) { + storeVal = null; + } + if (storeVal == null) { + return null; + } + return getCoType(storeVal.getAnnotations()); + } + + /** + * Returns the flow-sensitive {@code CollectionOwnershipType} of the given tree. + * + * @param tree the tree + * @return the {@code CollectionOwnershipType} that the given tree has + */ + public CollectionOwnershipType getCoType(Tree tree) { + JavaExpression jx = null; + if (tree instanceof ExpressionTree) { + jx = JavaExpression.fromTree((ExpressionTree) tree); + } else if (tree instanceof VariableTree) { + jx = JavaExpression.fromVariableTree((VariableTree) tree); + } + try { + CollectionOwnershipStore coStore = getStoreBefore(tree); + CFValue storeVal = coStore.getValue(jx); + return getCoType(storeVal.getAnnotations()); + } catch (Exception e) { + return null; + } + } + + /** + * Utility method to extract the {@code CollectionOwnershipType} from a collection of {@code + * AnnotationMirror}s. + * + * @param annos the {@code AnnotationMirror} collection + * @return the extracted {@code CollectionOwnershipType} from annos + */ + public CollectionOwnershipType getCoType(Collection annos) { + for (AnnotationMirror anm : annos) { + if (anm == null) { + continue; + } + if (AnnotationUtils.areSame(anm, NOTOWNINGCOLLECTION)) { + return CollectionOwnershipType.NotOwningCollection; + } else if (AnnotationUtils.areSame(anm, OWNINGCOLLECTION)) { + return CollectionOwnershipType.OwningCollection; + } else if (AnnotationUtils.areSame(anm, OWNINGCOLLECTIONWITHOUTOBLIGATION)) { + return CollectionOwnershipType.OwningCollectionWithoutObligation; + } else if (AnnotationUtils.areSame(anm, BOTTOM)) { + return CollectionOwnershipType.OwningCollectionBottom; + } + } + return null; + } + + /** + * Returns the field names in the {@code @CollectionFieldDestructor} annotation that the given + * method has or an empty list if there is no such annotation. + * + * @param method the method + * @return the field names in the method's {@code @CollectionFieldDestructor} annotation, or an + * empty list if there is no such annotation + */ + public List getCollectionFieldDestructorAnnoFields(ExecutableElement method) { + AnnotationMirror collectionFieldDestructorAnno = + getDeclAnnotation(method, CollectionFieldDestructor.class); + if (collectionFieldDestructorAnno == null) { + return new ArrayList(); + } + return AnnotationUtils.getElementValueArray( + collectionFieldDestructorAnno, collectionFieldDestructorValueElement, String.class); + } + + /** + * Returnst true if the given expression {@code e} refers to {@code this.field}. + * + * @param e the expression + * @param field the field + * @return true if {@code e} refers to {@code this.field} + */ + public boolean expressionIsFieldAccess(String e, VariableElement field) { + try { + JavaExpression je = StringToJavaExpression.atFieldDecl(e, field, this.checker); + return je instanceof FieldAccess && ((FieldAccess) je).getField().equals(field); + } catch (JavaExpressionParseException ex) { + // The parsing error will be reported elsewhere, assuming e was derived from an + // annotation. + return false; + } + } + + /** + * Returns a JavaExpression for the given String. Returns null if string is not parsable as a Java + * expression. + * + * @param s the string + * @param method the method with the annotation + * @return a JavaExpression for the given String, or null if the string is not parsable as a Java + * expression + */ + public JavaExpression stringToJavaExpression(String s, ExecutableElement method) { + Tree methodTree = declarationFromElement(method); + if (methodTree instanceof MethodTree) { + try { + return StringToJavaExpression.atMethodBody(s, (MethodTree) methodTree, checker); + } catch (JavaExpressionParseException ex) { + return null; + } + } + return null; + } + + @Override + protected TypeAnnotator createTypeAnnotator() { + return new ListTypeAnnotator( + super.createTypeAnnotator(), new CollectionOwnershipTypeAnnotator(this)); + } + + /** + * The TypeAnnotator for the Collection Ownership type system. + * + *

This TypeAnnotator defaults resource collection return types to OwningCollection, and + * resource collection parameters to NotOwningCollection. + */ + private class CollectionOwnershipTypeAnnotator extends TypeAnnotator { + + /** + * Creates a CollectionOwnershipTypeAnnotator. + * + * @param atypeFactory the type factory + */ + public CollectionOwnershipTypeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + @Override + public Void visitExecutable(AnnotatedExecutableType t, Void p) { + + AnnotatedDeclaredType receiverType = t.getReceiverType(); + AnnotationMirror receiverAnno = + receiverType == null ? null : receiverType.getEffectiveAnnotationInHierarchy(TOP); + boolean receiverHasExplicitAnno = + receiverAnno != null && !AnnotationUtils.areSameByName(BOTTOM, receiverAnno); + + AnnotatedTypeMirror returnType = t.getReturnType(); + AnnotationMirror returnAnno = returnType.getEffectiveAnnotationInHierarchy(TOP); + boolean returnHasExplicitAnno = + returnAnno != null && !AnnotationUtils.areSameByName(BOTTOM, returnAnno); + + // inherit supertype annotations + + Map overriddenMethods = + AnnotatedTypes.overriddenMethods( + elements, CollectionOwnershipAnnotatedTypeFactory.this, t.getElement()); + + if (overriddenMethods != null) { + for (ExecutableElement superElt : overriddenMethods.values()) { + AnnotatedExecutableType annotatedSuperMethod = + CollectionOwnershipAnnotatedTypeFactory.this.getAnnotatedType(superElt); + + if (!receiverHasExplicitAnno) { + AnnotatedDeclaredType superReceiver = annotatedSuperMethod.getReceiverType(); + AnnotationMirror superReceiverAnno = superReceiver.getPrimaryAnnotationInHierarchy(TOP); + boolean superReceiverHasExplicitAnno = + superReceiverAnno != null + && !AnnotationUtils.areSameByName(BOTTOM, superReceiverAnno) + && !AnnotationUtils.areSameByName(POLY, superReceiverAnno); + if (superReceiverHasExplicitAnno) { + receiverType.replaceAnnotation(superReceiverAnno); + } + } + + if (!returnHasExplicitAnno) { + AnnotatedTypeMirror superReturnType = annotatedSuperMethod.getReturnType(); + AnnotationMirror superReturnAnno = superReturnType.getPrimaryAnnotationInHierarchy(TOP); + boolean superReturnHasExplicitAnno = + superReturnAnno != null + && !AnnotationUtils.areSameByName(BOTTOM, superReturnAnno) + && !AnnotationUtils.areSameByName(POLY, superReturnAnno); + if (superReturnHasExplicitAnno) { + returnType.replaceAnnotation(superReturnAnno); + } + } + + List paramTypes = t.getParameterTypes(); + List superParamTypes = + annotatedSuperMethod.getParameterTypes(); + for (int i = 0; i < superParamTypes.size(); i++) { + AnnotationMirror paramAnno = paramTypes.get(i).getEffectiveAnnotationInHierarchy(TOP); + boolean paramHasExplicitAnno = + paramAnno != null && !AnnotationUtils.areSameByName(BOTTOM, paramAnno); + if (!paramHasExplicitAnno) { + AnnotationMirror superParamAnno = + superParamTypes.get(i).getPrimaryAnnotationInHierarchy(TOP); + boolean superParamHasExplicitAnno = + superParamAnno != null + && !AnnotationUtils.areSameByName(BOTTOM, superParamAnno) + && !AnnotationUtils.areSameByName(POLY, superParamAnno); + if (superParamHasExplicitAnno) { + paramTypes.get(i).replaceAnnotation(superParamAnno); + } + } + } + } + } // end "if (overriddenMethods != null)" + + if (isResourceCollection(returnType.getUnderlyingType())) { + AnnotationMirror manualAnno = returnType.getEffectiveAnnotationInHierarchy(TOP); + if (manualAnno == null || AnnotationUtils.areSameByName(BOTTOM, manualAnno)) { + boolean isConstructor = t.getElement().getKind() == ElementKind.CONSTRUCTOR; + if (isConstructor) { + returnType.replaceAnnotation(OWNINGCOLLECTIONWITHOUTOBLIGATION); + } else { + returnType.replaceAnnotation(OWNINGCOLLECTION); + } + } + } + + for (AnnotatedTypeMirror paramType : t.getParameterTypes()) { + if (isResourceCollection(paramType.getUnderlyingType())) { + AnnotationMirror manualAnno = paramType.getEffectiveAnnotationInHierarchy(TOP); + if (manualAnno == null || AnnotationUtils.areSameByName(BOTTOM, manualAnno)) { + paramType.replaceAnnotation(NOTOWNINGCOLLECTION); + } + } + } + + return super.visitExecutable(t, p); + } + } + + /* + * Defaults resource collection field uses within member methods to @OwningCollection. + */ + @Override + protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) { + super.addComputedTypeAnnotations(tree, type, iUseFlow); + + if (type.getKind() == TypeKind.DECLARED) { + Element elt = TreeUtils.elementFromTree(tree); + if (elt != null) { + boolean isField = elt.getKind() == ElementKind.FIELD; + if (isField && isResourceCollection(type.getUnderlyingType())) { + AnnotationMirror fieldAnno = type.getEffectiveAnnotationInHierarchy(TOP); + if (fieldAnno == null || AnnotationUtils.areSameByName(BOTTOM, fieldAnno)) { + TreePath currentPath = getPath(tree); + MethodTree enclosingMethodTree = TreePathUtil.enclosingMethod(currentPath); + if (enclosingMethodTree != null && TreeUtils.isConstructor(enclosingMethodTree)) { + type.replaceAnnotation(OWNINGCOLLECTIONWITHOUTOBLIGATION); + } else { + type.replaceAnnotation(OWNINGCOLLECTION); + } + } + } + } + } + } + + // Default resource collection fields to @OwningCollection and resource collection parameters + // to @NotOwningCollection (inside the method). + // + // A resource collection is a `Iterable` or `Iterator`, whose component has non-empty + // @MustCall type, as defined by the predicate isResourceCollection(AnnotatedTypeMirror). + @Override + public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { + super.addComputedTypeAnnotations(elt, type); + + if (elt instanceof VariableElement) { + if (isResourceCollection(type.getUnderlyingType())) { + if (elt.getKind() == ElementKind.FIELD) { + AnnotationMirror fieldAnno = type.getEffectiveAnnotationInHierarchy(TOP); + if (fieldAnno == null || AnnotationUtils.areSameByName(BOTTOM, fieldAnno)) { + type.replaceAnnotation(OWNINGCOLLECTION); + } + } else if (elt.getKind() == ElementKind.PARAMETER) { + // Propagate the parameter annotation to the use site. + ExecutableElement method = (ExecutableElement) elt.getEnclosingElement(); + AnnotatedExecutableType annotatedMethod = + CollectionOwnershipAnnotatedTypeFactory.this.getAnnotatedType(method); + List params = method.getParameters(); + List paramTypes = annotatedMethod.getParameterTypes(); + for (int i = 0; i < params.size(); i++) { + if (params.get(i).getSimpleName() == elt.getSimpleName()) { + type.replaceAnnotation(paramTypes.get(i).getEffectiveAnnotationInHierarchy(TOP)); + break; + } + } + } + } + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipChecker.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipChecker.java new file mode 100644 index 00000000000..99480c80457 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipChecker.java @@ -0,0 +1,26 @@ +package org.checkerframework.checker.collectionownership; + +import java.util.LinkedHashSet; +import java.util.Set; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsChecker; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.source.SourceChecker; + +/** + * This typechecker tracks at most one owning variable per resource collection using an ownership + * type system. The Resource Leak Checker verifies that (at least) the determined owner fulfills the + * calling obligations of its elements. + */ +public class CollectionOwnershipChecker extends BaseTypeChecker { + + /** Creates a CollectionOwnershipChecker. */ + public CollectionOwnershipChecker() {} + + @Override + protected Set> getImmediateSubcheckerClasses() { + Set> checkers = + new LinkedHashSet<>(super.getImmediateSubcheckerClasses()); + checkers.add(RLCCalledMethodsChecker.class); + return checkers; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipStore.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipStore.java new file mode 100644 index 00000000000..80a495a93fb --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipStore.java @@ -0,0 +1,62 @@ +package org.checkerframework.checker.collectionownership; + +import org.checkerframework.checker.collectionownership.qual.CollectionFieldDestructor; +import org.checkerframework.checker.collectionownership.qual.OwningCollection; +import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.framework.flow.CFAbstractStore; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; + +/** + * The CollectionOwnership Store behaves like CFAbstractStore but keeps {@code @}{@link + * OwningCollection} fields in the store. This is justified by the strict access rules of such + * fields. Keeping the field in the store is required for verifying the postcondition annotation + * {@code @}{@link CollectionFieldDestructor}. + */ +public class CollectionOwnershipStore extends CFAbstractStore { + + /** The annotated type factory. */ + private final CollectionOwnershipAnnotatedTypeFactory atypeFactory; + + /** + * Constructs a collection ownership store. + * + * @param analysis the collection ownership analysis + * @param sequentialSemantics if true, use sequential semantics + */ + public CollectionOwnershipStore( + CollectionOwnershipAnalysis analysis, boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + this.atypeFactory = (CollectionOwnershipAnnotatedTypeFactory) analysis.getTypeFactory(); + } + + /** + * Copy constructor. + * + * @param analysis the collection ownership analysis + * @param other the store to construct from + */ + public CollectionOwnershipStore( + CollectionOwnershipAnalysis analysis, + CFAbstractStore other) { + super(other); + this.atypeFactory = ((CollectionOwnershipStore) other).atypeFactory; + } + + /* + * Keep OwningCollection fields in the store. + */ + @Override + protected CFValue newFieldValueAfterMethodCall( + FieldAccess fieldAccess, + GenericAnnotatedTypeFactory atf, + CFValue value) { + CFValue superResult = super.newFieldValueAfterMethodCall(fieldAccess, atf, value); + if (superResult == null) { + if (atypeFactory.isResourceCollectionField(fieldAccess.getField())) { + return value; + } + } + return superResult; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java new file mode 100644 index 00000000000..cff2f91a6e3 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipTransfer.java @@ -0,0 +1,343 @@ +package org.checkerframework.checker.collectionownership; + +import com.sun.source.tree.Tree; +import java.util.List; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import org.checkerframework.checker.collectionownership.CollectionOwnershipAnnotatedTypeFactory.CollectionOwnershipType; +import org.checkerframework.checker.collectionownership.qual.CollectionFieldDestructor; +import org.checkerframework.checker.collectionownership.qual.CreatesCollectionObligation; +import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory; +import org.checkerframework.checker.resourceleak.ResourceLeakUtils; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory.PotentiallyFulfillingLoop; +import org.checkerframework.dataflow.analysis.ConditionalTransferResult; +import org.checkerframework.dataflow.analysis.RegularTransferResult; +import org.checkerframework.dataflow.analysis.TransferInput; +import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.LessThanNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.util.NodeUtils; +import org.checkerframework.framework.flow.CFAbstractTransfer; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; + +/** + * Transfer function for the collection ownership type system. Its primary purpose is to create + * temporary variables for expressions (which allow those expressions to have refined information in + * the store, which the consistency checker can use). + */ +public class CollectionOwnershipTransfer + extends CFAbstractTransfer { + + /** The type factory. */ + private final CollectionOwnershipAnnotatedTypeFactory atypeFactory; + + /** The checker. */ + private final CollectionOwnershipChecker checker; + + /** The MustCall type factory to manage temporary variables. */ + private final MustCallAnnotatedTypeFactory mcAtf; + + /** + * Create a CollectionOwnershipTransfer. + * + * @param analysis the analysis + * @param checker the checker + */ + public CollectionOwnershipTransfer( + CollectionOwnershipAnalysis analysis, CollectionOwnershipChecker checker) { + super(analysis); + this.atypeFactory = (CollectionOwnershipAnnotatedTypeFactory) analysis.getTypeFactory(); + this.mcAtf = ResourceLeakUtils.getMustCallAnnotatedTypeFactory(checker); + this.checker = checker; + } + + @Override + public TransferResult visitAssignment( + AssignmentNode node, TransferInput in) { + TransferResult res = super.visitAssignment(node, in); + + Node lhs = getNodeOrTempVar(node.getTarget()); + JavaExpression lhsJE = JavaExpression.fromNode(lhs); + + Node rhs = getNodeOrTempVar(node.getExpression()); + CollectionOwnershipType rhsType = + atypeFactory.getCoType(rhs, atypeFactory.getStoreBefore(node)); + + // Ownership transfer from rhs into lhs usually. + // Special case: desugared assignments of a temporary array variable + // and rhs being owning resource collection field. + if (rhsType != null) { + switch (rhsType) { + case OwningCollection: + case OwningCollectionWithoutObligation: + JavaExpression rhsJE = JavaExpression.fromNode(rhs); + if (node.isDesugaredFromEnhancedArrayForLoop() + || atypeFactory.isOwningCollectionField( + TreeUtils.elementFromTree(node.getExpression().getTree()))) { + replaceInStores(res, lhsJE, atypeFactory.NOTOWNINGCOLLECTION); + } else { + replaceInStores(res, rhsJE, atypeFactory.NOTOWNINGCOLLECTION); + } + break; + default: + } + } + return res; + } + + /** + * May refine the type of the collection to @OwningCollectionWithoutObligation in the else store + * of the incoming transfer result. Does so if the given AST tree is the condition for a + * collection-obligation-fulfilling loop that calls all methods in the MustCall type of the + * elements of some collection. + * + * @param res the incoming transfer result + * @param tree the AST tree that is possibly the loop condition for a + * collection-obligation-fulfilling loop + * @return the resulting transfer result + */ + private TransferResult updateStoreForPotentiallyFulfillingLoop( + TransferResult res, Tree tree) { + PotentiallyFulfillingLoop loop = + CollectionOwnershipAnnotatedTypeFactory.getFulfillingLoopForCondition(tree); + if (loop != null) { + CollectionOwnershipStore elseStore = res.getElseStore(); + JavaExpression collectionJE = JavaExpression.fromTree(loop.collectionTree); + + CollectionOwnershipType collectionCoType = atypeFactory.getCoType(loop.collectionTree); + if (collectionCoType == CollectionOwnershipType.OwningCollection) { + List mustCallValuesOfElements = + atypeFactory.getMustCallValuesOfResourceCollectionComponent(loop.collectionTree); + if (loop.getCalledMethods().containsAll(mustCallValuesOfElements)) { + elseStore.clearValue(collectionJE); + elseStore.insertValue(collectionJE, atypeFactory.OWNINGCOLLECTIONWITHOUTOBLIGATION); + return new ConditionalTransferResult<>( + res.getResultValue(), res.getThenStore(), elseStore); + } + } + } + return res; + } + + @Override + public TransferResult visitLessThan( + LessThanNode node, TransferInput in) { + TransferResult res = super.visitLessThan(node, in); + return updateStoreForPotentiallyFulfillingLoop(res, node.getTree()); + } + + @Override + public TransferResult visitMethodInvocation( + MethodInvocationNode node, TransferInput in) { + TransferResult res = super.visitMethodInvocation(node, in); + + updateStoreWithTempVar(res, node); + + ExecutableElement method = node.getTarget().getMethod(); + List args = node.getArguments(); + res = transferOwnershipForMethodInvocation(method, node, args, res); + res = updateStoreForPotentiallyFulfillingLoop(res, node.getTree()); + + // Check whether the method is annotated @CreatesCollectionObligation. + ExecutableElement methodElement = TreeUtils.elementFromUse(node.getTree()); + boolean hasCreatesCollectionObligation = + atypeFactory.getDeclAnnotation(methodElement, CreatesCollectionObligation.class) != null; + boolean hasCollectionFieldDestructor = + atypeFactory.getDeclAnnotation(methodElement, CollectionFieldDestructor.class) != null; + if (hasCreatesCollectionObligation) { + Node receiverNode = node.getTarget().getReceiver(); + JavaExpression receiverJE = JavaExpression.fromNode(receiverNode); + if (atypeFactory.getCoType(receiverNode, atypeFactory.getStoreBefore(node)) + == CollectionOwnershipType.OwningCollectionWithoutObligation) { + replaceInStores(res, receiverJE, atypeFactory.OWNINGCOLLECTION); + } + } + if (hasCollectionFieldDestructor) { + List destructedFields = + atypeFactory.getCollectionFieldDestructorAnnoFields(methodElement); + for (String destructedFieldName : destructedFields) { + JavaExpression fieldExpr = + atypeFactory.stringToJavaExpression(destructedFieldName, methodElement); + if (fieldExpr != null) { + replaceInStores(res, fieldExpr, atypeFactory.OWNINGCOLLECTIONWITHOUTOBLIGATION); + } + } + } + return res; + } + + /** + * Executes collection ownership transfer in method invocations. Owning arguments to an owning + * parameter lose ownership. + * + * @param method the method whose parameters are checked + * @param node the node of the invocation + * @param args the list of method arguments + * @param res the transfer result so far + * @return the updated transfer result + */ + private TransferResult transferOwnershipForMethodInvocation( + ExecutableElement method, + Node node, + List args, + TransferResult res) { + List params = method.getParameters(); + + for (int i = 0; i < Math.min(args.size(), params.size()); i++) { + VariableElement param = params.get(i); + Node arg = getNodeOrTempVar(args.get(i)); + JavaExpression argJE = JavaExpression.fromNode(arg); + CollectionOwnershipType argType = + atypeFactory.getCoType(arg, atypeFactory.getStoreBefore(node)); + CollectionOwnershipType paramType = + atypeFactory.getCoType(param.asType().getAnnotationMirrors()); + if (paramType == null) { + continue; + } + + Element argElem = TreeUtils.elementFromTree(arg.getTree()); + boolean transferOwnership = false; + switch (paramType) { + case OwningCollection: + switch (argType) { + case OwningCollection: + case OwningCollectionWithoutObligation: + transferOwnership = true; + break; + default: + } + break; + case OwningCollectionWithoutObligation: + switch (argType) { + case OwningCollectionWithoutObligation: + transferOwnership = true; + break; + default: + } + break; + default: + } + if (transferOwnership) { + if (argElem.getKind().isField()) { + checker.reportError( + arg.getTree(), "transfer.owningcollection.field.ownership", arg.getTree().toString()); + } else { + replaceInStores(res, argJE, atypeFactory.NOTOWNINGCOLLECTION); + } + } + } + return res; + } + + @Override + public TransferResult visitObjectCreation( + ObjectCreationNode node, TransferInput input) { + TransferResult result = + super.visitObjectCreation(node, input); + updateStoreWithTempVar(result, node); + + ExecutableElement constructor = TreeUtils.elementFromUse(node.getTree()); + List args = node.getArguments(); + result = transferOwnershipForMethodInvocation(constructor, node, args, result); + + // The return value defaulting logic cannot recognize that a diamond-constructed collection + // is a resource collection, as it runs before the type variable is inferred: + // List = new ArrayList<>(); + // Thus, the following checks object creation expressions again on whether they are + // resource collections with no type variables, and if they are @Bottom, they are + // unrefined to @OwningCollection. Change the type of both the type var and the computed + // expression itself. + CollectionOwnershipStore store = result.getRegularStore(); + CFValue resultValue = result.getResultValue(); + Node tempVarNode = getNodeOrTempVar(node); + JavaExpression tempVarJE = JavaExpression.fromNode(tempVarNode); + + CollectionOwnershipType resolvedType = + atypeFactory.getCoType(tempVarNode, atypeFactory.getStoreBefore(node)); + if (atypeFactory.isResourceCollection(node.getTree())) { + boolean isDiamond = node.getTree().getTypeArguments().size() == 0; + if (isDiamond && resolvedType == CollectionOwnershipType.OwningCollectionBottom) { + store.clearValue(tempVarJE); + store.insertValue(tempVarJE, atypeFactory.OWNINGCOLLECTIONWITHOUTOBLIGATION); + resultValue = + analysis.createSingleAnnotationValue( + atypeFactory.OWNINGCOLLECTIONWITHOUTOBLIGATION, node.getType()); + } + } + + return new RegularTransferResult(resultValue, store); + } + + /** + * Updates the store to give the temp var for {@code node} the same type as {@code node}. + * + * @param node the node to be assigned to a temporary variable + * @param result the transfer result containing the store to be modified + */ + public void updateStoreWithTempVar( + TransferResult result, Node node) { + // Must-call obligations on primitives are not supported. + if (!TypesUtils.isPrimitiveOrBoxed(node.getType())) { + LocalVariableNode temp = mcAtf.getTempVar(node); + if (temp != null) { + JavaExpression localExp = JavaExpression.fromNode(temp); + AnnotationMirror anm = + atypeFactory + .getAnnotatedType(node.getTree()) + .getPrimaryAnnotationInHierarchy(atypeFactory.TOP); + insertIntoStores(result, localExp, anm == null ? atypeFactory.TOP : anm); + } + } + } + + /** + * Inserts {@code newAnno} as the value into all stores (conditional or not) in the result for + * node, clearing the previous value first. + * + * @param result the TransferResult holding the stores to modify + * @param target the receiver whose value should be modified + * @param newAnno the new value + */ + protected static void replaceInStores( + TransferResult result, + JavaExpression target, + AnnotationMirror newAnno) { + if (result.containsTwoStores()) { + result.getThenStore().clearValue(target); + result.getElseStore().clearValue(target); + result.getThenStore().insertValue(target, newAnno); + result.getElseStore().insertValue(target, newAnno); + } else { + result.getRegularStore().clearValue(target); + result.getRegularStore().insertValue(target, newAnno); + } + } + + /** + * Returns the temp-var corresponding to {@code node} if it exists, or else returns {@code node} + * with casts removed. + * + * @param node the node + * @return the temp-var corresponding to {@code node} with casts removed if it exists or else + * {@code node} with casts removed + */ + protected Node getNodeOrTempVar(Node node) { + node = NodeUtils.removeCasts(node); + Node tempVarForNode = + ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(atypeFactory) + .getTempVarForNode(node); + if (tempVarForNode != null) { + return tempVarForNode; + } + return node; + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipVisitor.java b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipVisitor.java new file mode 100644 index 00000000000..c872f51b652 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipVisitor.java @@ -0,0 +1,167 @@ +package org.checkerframework.checker.collectionownership; + +import com.sun.source.tree.AnnotationTree; +import com.sun.source.tree.VariableTree; +import java.util.List; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.VariableElement; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer; +import org.checkerframework.checker.resourceleak.ResourceLeakUtils; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreeUtils; + +/** + * The visitor for the Collection Ownership Checker. This visitor is similar to BaseTypeVisitor, but + * overrides methods that don't work well with the ownership type hierarchy because it doesn't use + * the top type as the default type. + */ +public class CollectionOwnershipVisitor + extends BaseTypeVisitor { + + /** + * Creates a new CollectionOwnershipVisitor. + * + * @param checker the type-checker associated with this visitor + */ + public CollectionOwnershipVisitor(BaseTypeChecker checker) { + super(checker); + } + + @Override + public Void visitAnnotation(AnnotationTree tree, Void p) { + AnnotationMirror am = TreeUtils.annotationFromAnnotationTree(tree); + if (AnnotationUtils.areSame(am, atypeFactory.BOTTOM) + || AnnotationUtils.areSame(am, atypeFactory.OWNINGCOLLECTIONWITHOUTOBLIGATION)) { + checker.reportError(tree, "illegal.type.annotation", tree); + } + return super.visitAnnotation(tree, p); + } + + /** + * This method checks that the result type of a constructor is a supertype of the declared type on + * the class, if one exists. + * + *

This method typically issues a warning if the result type of the constructor is not top, + * because in top-default type systems that indicates a potential problem. For the Collection + * Ownership Checker, this does not apply, since the default return type is bottom. This is + * justified by examining all return types and setting them to a safe default in {@code + * CollectionOwnershipTypeAnnotator#visitExecutable}. + * + * @param constructorType an AnnotatedExecutableType for the constructor + * @param constructorElement element that declares the constructor + */ + @Override + protected void checkConstructorResult( + AnnotatedExecutableType constructorType, ExecutableElement constructorElement) { + AnnotatedTypeMirror defaultType = + atypeFactory.getAnnotatedType(ElementUtils.enclosingTypeElement(constructorElement)); + AnnotationMirror defaultAnno = defaultType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP); + AnnotatedTypeMirror resultType = constructorType.getReturnType(); + AnnotationMirror resultAnno = resultType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP); + if (!qualHierarchy.isSubtypeShallow( + defaultAnno, defaultType.getUnderlyingType(), resultAnno, resultType.getUnderlyingType())) { + checker.reportError( + constructorElement, "inconsistent.constructor.type", resultAnno, defaultAnno); + } + } + + /** + * Change the default for exception parameter lower bounds to bottom, to prevent false positives. + * + * @return a set containing only the Bottom annotation + */ + @Override + protected AnnotationMirrorSet getExceptionParameterLowerBoundAnnotations() { + return new AnnotationMirrorSet(atypeFactory.BOTTOM); + } + + @Override + public Void visitVariable(VariableTree tree, Void p) { + Element elt = TreeUtils.elementFromDeclaration(tree); + if (elt != null && atypeFactory.isResourceCollectionField(elt)) { + if (elt.getModifiers().contains(Modifier.STATIC)) { + // error: static resource collection fields not supported + checker.reportError(tree, "static.resource.collection.field", tree); + } + if (atypeFactory.isOwningCollectionField(elt)) { + checkOwningCollectionField(tree); + } + } + return super.visitVariable(tree, p); + } + + /** + * Checks validity of an {@code OwningCollection} field {@code field}. Say the element type {@code + * field} is {@code @MustCall("m"}}. This method checks that the enclosing class of {@code field} + * has a type {@code @MustCall("m2")} for some method {@code m2}, and that {@code m2} has an + * annotation {@code @CollectionFieldDestructor("field")}, guaranteeing that the {@code @MustCall} + * obligation of the field will be satisfied. + * + * @param fieldTree the declaration of the field to check + */ + private void checkOwningCollectionField(VariableTree fieldTree) { + VariableElement fieldElement = TreeUtils.elementFromDeclaration(fieldTree); + List mustCallValues = + atypeFactory.getMustCallValuesOfResourceCollectionComponent(fieldTree); + + if (mustCallValues == null || mustCallValues.isEmpty()) { + return; + } + + RLCCalledMethodsAnnotatedTypeFactory rlAtf = + ResourceLeakUtils.getRLCCalledMethodsAnnotatedTypeFactory(atypeFactory); + Element enclosingElement = fieldElement.getEnclosingElement(); + List enclosingMustCallValues = rlAtf.getMustCallValues(enclosingElement); + + String error; + if (enclosingMustCallValues == null) { + error = + " The enclosing element " + + ElementUtils.getQualifiedName(enclosingElement) + + " has no @MustCall annotation"; + } else if (enclosingMustCallValues.isEmpty()) { + error = + " The enclosing element " + + ElementUtils.getQualifiedName(enclosingElement) + + " has an empty @MustCall annotation"; + } else { + List siblingsOfOwningField = enclosingElement.getEnclosedElements(); + for (Element siblingElement : siblingsOfOwningField) { + if (siblingElement.getKind() == ElementKind.METHOD + && enclosingMustCallValues.contains(siblingElement.getSimpleName().toString())) { + + ExecutableElement siblingMethod = (ExecutableElement) siblingElement; + + List destructedFields = + atypeFactory.getCollectionFieldDestructorAnnoFields(siblingMethod); + for (String destructedFieldName : destructedFields) { + if (atypeFactory.expressionIsFieldAccess(destructedFieldName, fieldElement)) { + return; + } + } + } + } + error = + " No Destructor Method annotated @CollectionFieldDestructor(" + + fieldTree.getName().toString() + + ") found."; + } + checker.reportError( + fieldTree, + "unfulfilled.field.obligations", + fieldTree.getName().toString(), + MustCallConsistencyAnalyzer.formatMissingMustCallMethods(mustCallValues), + error); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/collectionownership/messages.properties b/checker/src/main/java/org/checkerframework/checker/collectionownership/messages.properties new file mode 100644 index 00000000000..f5ed712d084 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/collectionownership/messages.properties @@ -0,0 +1,5 @@ +unfulfilled.collection.obligations=@MustCall method %s may not have been invoked on the elements of %s.%nReason for going out of scope: %s +unfulfilled.field.obligations=The field %s may not have all of its @MustCall %s called on its elements.%nReason for failure of proving fulfillment: %s +transfer.owningcollection.field.ownership=Method invocation unsafely transfers the ownership away from field %s. An @OwningCollection field can never lose ownership. +illegal.type.annotation=Users may not write %s. +static.resource.collection.field=The static field %s is unsoundly treated as non-static. diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java index e53a5583aa5..b5be59815b4 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -23,7 +23,9 @@ import javax.lang.model.element.ElementKind; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.TypeElement; +import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; +import javax.lang.model.type.WildcardType; import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor; import org.checkerframework.checker.mustcall.qual.InheritableMustCall; import org.checkerframework.checker.mustcall.qual.MustCall; @@ -33,6 +35,7 @@ import org.checkerframework.checker.mustcall.qual.PolyMustCall; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.resourceleak.ResourceLeakChecker; +import org.checkerframework.checker.resourceleak.ResourceLeakUtils; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.cfg.block.Block; @@ -42,7 +45,9 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.framework.type.QualifierUpperBounds; @@ -158,6 +163,131 @@ public void setRoot(@Nullable CompilationUnitTree newRoot) { tempVars.clear(); } + /** + * Replace all the type variables of the given AnnotatedDeclaredType that refer to Collections or + * Iterators with Bottom if they are Top. This is because having a Top type parameter is unsafe + * and occurs when the type variable is a generic or wildcard without upper bound. We want to + * prevent such a Collection/Iterator from holding elements with MustCall obligations. + * + * @param tree the tree + * @param adt the annotated declared type for which all Collection type variables with Top type + * are to be replaced with Bottom + */ + private void replaceCollectionTypeVarsWithBottomIfTop(Tree tree, AnnotatedDeclaredType adt) { + if (ResourceLeakUtils.isCollection(adt.getUnderlyingType())) { + for (AnnotatedTypeMirror typeArg : adt.getTypeArguments()) { + if (typeArg == null) { + continue; + } + if (typeArg.getKind() == TypeKind.WILDCARD || typeArg.getKind() == TypeKind.TYPEVAR) { + if (tree != null && tree instanceof NewClassTree) { + if (((NewClassTree) tree).getTypeArguments().isEmpty()) { + // Diamond [new Class()<>]. Not explicit generic type param. + // This will be inferred later. Don't put it to bottom here. + continue; + } + } + AnnotationMirror mcAnno = typeArg.getEffectiveAnnotationInHierarchy(TOP); + boolean typeArgIsMcUnknown = + mcAnno != null + && processingEnv + .getTypeUtils() + .isSameType(mcAnno.getAnnotationType(), TOP.getAnnotationType()); + if (typeArgIsMcUnknown) { + // check whether the upper bounds have manual MustCallUnknown annotations, in which case + // they should + // not be reset to bottom. For example like this: + // void m(List) {} + + if (typeArg.getUnderlyingType() instanceof WildcardType) { + TypeMirror extendsBound = + ((WildcardType) typeArg.getUnderlyingType()).getExtendsBound(); + if (!ResourceLeakUtils.hasManualMustCallUnknownAnno(extendsBound)) { + typeArg.replaceAnnotation(BOTTOM); + } + } else if (typeArg instanceof AnnotatedTypeVariable) { + AnnotatedTypeMirror upperBound = ((AnnotatedTypeVariable) typeArg).getUpperBound(); + // set back to bottom if the type var is a captured wildcard + // or if it doesn't have a manual MustCallUnknown anno + if (typeArg.containsCapturedTypes() + || !ResourceLeakUtils.hasManualMustCallUnknownAnno(upperBound, this)) { + typeArg.replaceAnnotation(BOTTOM); + } + } else { + typeArg.replaceAnnotation(BOTTOM); + } + } + } else if (typeArg.getKind() == TypeKind.DECLARED) { + replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) typeArg); + } + } + } + } + + /** + * Changes the type parameter annotations of resource collections and iterators to + * {@code @MustCall({})} if they are currently {@code @MustCallUnknown}. + * + *

This is necessary, as the type variable upper bounds for collections is + * {@code @MustCallUnknown}. When the type variable is a generic or wildcard with no upper bound, + * the type parameter defaults to {@code @MustCallUnknown}, which is both unsound and imprecise. + * + *

This method changes the type parameter annotations for declared types directly. The other + * overload {@link #addComputedTypeAnnotations(Element, AnnotatedTypeMirror)} handles type + * parameter annotations for method return types and parameters, such that the changes are + * 'visible' at call- site as well as within the method. Changing this on the {@code Tree} is not + * sufficient. The reason that declared types are handled here is that for object initializations + * where the type parameter is left for inference (e.g., {@code new Object<>()}), we don't want to + * change the type parameter annotation here, but wait for the inference instead, which + * instantiates it with the inferred type and corresponding annotation. Access to the {@code Tree} + * allows us to detect whether we have a new class tree without type parameters. + */ + @Override + public void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean useFlow) { + super.addComputedTypeAnnotations(tree, type, useFlow); + + if (tree.getKind() != Tree.Kind.CLASS && tree.getKind() != Tree.Kind.INTERFACE) { + if (type.getKind() == TypeKind.DECLARED) { + replaceCollectionTypeVarsWithBottomIfTop(tree, (AnnotatedDeclaredType) type); + } + } + } + + /** + * Changes the type parameter annotations of collections and iterators to {@code @MustCall} if + * they are currently {@code @MustCallUnknown}. + * + *

This is necessary, as the type variable upper bounds for collections is + * {@code @MustCallUnknown}. When the type variable is a generic or wildcard with no upper bound, + * the type parameter does default to {@code @MustCallUnknown}, which is both unsound and + * imprecise. + * + *

This method changes the type parameter annotations of {@code Element}s, which is the + * preferred way for method return types and parameters, such that the changes are 'visible' at + * call-site as well as within the method. The type parameter annotations at other places is + * handled by {@link #addComputedTypeAnnotations(Tree, AnnotatedTypeMirror, boolean)}, because it + * has access to the {@code Tree}. + */ + @Override + public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { + super.addComputedTypeAnnotations(elt, type); + + if (type.getKind() == TypeKind.EXECUTABLE) { + AnnotatedExecutableType methodType = (AnnotatedExecutableType) type; + AnnotatedTypeMirror returnType = methodType.getReturnType(); + + if (returnType.getKind() == TypeKind.DECLARED) { + replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) returnType); + } + + for (AnnotatedTypeMirror paramType : methodType.getParameterTypes()) { + if (paramType.getKind() == TypeKind.DECLARED) { + replaceCollectionTypeVarsWithBottomIfTop(null, (AnnotatedDeclaredType) paramType); + } + } + } + } + @Override protected Set> createSupportedTypeQualifiers() { // Explicitly name the qualifiers, in order to exclude @MustCallAlias. diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java index e3ce2bd774a..b7bac877000 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -2,20 +2,35 @@ import com.sun.source.tree.AnnotationTree; import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.BlockTree; +import com.sun.source.tree.BreakTree; import com.sun.source.tree.ClassTree; +import com.sun.source.tree.CompoundAssignmentTree; +import com.sun.source.tree.ExpressionStatementTree; import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.ForLoopTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.LiteralTree; import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.ReturnTree; +import com.sun.source.tree.StatementTree; import com.sun.source.tree.Tree; +import com.sun.source.tree.UnaryTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreeScanner; import java.util.ArrayList; import java.util.Collections; import java.util.List; +import java.util.Set; +import java.util.concurrent.atomic.AtomicBoolean; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Name; import javax.lang.model.element.TypeElement; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.mustcall.qual.InheritableMustCall; @@ -24,8 +39,15 @@ import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.mustcall.qual.PolyMustCall; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakUtils; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.dataflow.cfg.block.Block; +import org.checkerframework.dataflow.cfg.block.ConditionalBlock; +import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; +import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; @@ -329,4 +351,355 @@ protected AnnotationMirrorSet getExceptionParameterLowerBoundAnnotations() { public Void visitAnnotation(AnnotationTree tree, Void p) { return null; } + + // /////////////////////////////////////////////////////////////////////////// + // Syntactically match for-loops that iterate over all elements of a collection on the AST. + // This happens here in the MustCallVisitor instead of the CollectionOwnershipVisitor, which + // would be the natural place to put this logic, because the matching must be completed + // before the CollectionOwnershipTransfer logic runs, and the CollectionOwnershipVisitor runs + // after the CollectionOwnershipTransfer. + + /** + * Records, in the {@code @CollectionOwnershipAnnotatedTypeFactory}, loops that call a method on + * entries of an {@code @OwningCollection}. + */ + @Override + public Void visitForLoop(ForLoopTree tree, Void p) { + boolean singleLoopVariable = tree.getUpdate().size() == 1 && tree.getInitializer().size() == 1; + if (singleLoopVariable) { + detectCollectionObligationFulfillingLoop(tree); + } + return super.visitForLoop(tree, p); + } + + /** + * Marks the for-loop if it potentially fulfills collection obligations of a collection. + * + * @param tree a `for` loop with exactly one loop variable + */ + private void detectCollectionObligationFulfillingLoop(ForLoopTree tree) { + List loopBodyStatementList; + if (tree.getStatement() instanceof BlockTree) { + BlockTree blockT = (BlockTree) tree.getStatement(); + loopBodyStatementList = blockT.getStatements(); + } else { + loopBodyStatementList = Collections.singletonList(tree.getStatement()); + } + StatementTree init = tree.getInitializer().get(0); + ExpressionTree condition = TreeUtils.withoutParens(tree.getCondition()); + ExpressionStatementTree update = tree.getUpdate().get(0); + if (!(condition instanceof BinaryTree)) { + return; + } + Name identifierInHeader = + nameOfCollectionThatAllElementsAreCalledOn(init, (BinaryTree) condition, update); + Name iterator = getNameFromStatementTree(init); + if (identifierInHeader == null || iterator == null) { + return; + } + ExpressionTree collectionElementTree = + getLastElementAccessIfLoopValid(loopBodyStatementList, identifierInHeader, iterator); + if (collectionElementTree != null) { + // Pattern match succeeded, now mark the loop in the respective datastructures. + + Block loopConditionBlock = null; + for (Node node : atypeFactory.getNodesForTree(condition)) { + Block blockOfNode = node.getBlock(); + if (blockOfNode != null) { + loopConditionBlock = blockOfNode; + break; + } + } + + Block loopUpdateBlock = null; + for (Node node : atypeFactory.getNodesForTree(update.getExpression())) { + Block blockOfNode = node.getBlock(); + if (blockOfNode != null) { + loopUpdateBlock = blockOfNode; + break; + } + } + + Set collectionEltNodes = atypeFactory.getNodesForTree(collectionElementTree); + Node nodeForCollectionElt = null; + if (collectionEltNodes != null) { + nodeForCollectionElt = collectionEltNodes.iterator().next(); + } + if (loopUpdateBlock == null || loopConditionBlock == null) { + return; + } + // Add the blocks into a static datastructure in the calledmethodsatf, such that it can + // analyze them (call MustCallConsistencyAnalyzer.analyzeFulfillingLoops, which in turn adds + // the trees to the static datastructure in McoeAtf). + Block conditionalBlock = ((SingleSuccessorBlock) loopConditionBlock).getSuccessor(); + Block loopBodyEntryBlock = ((ConditionalBlock) conditionalBlock).getThenSuccessor(); + RLCCalledMethodsAnnotatedTypeFactory.addPotentiallyFulfillingLoop( + collectionTreeFromExpression(collectionElementTree), + collectionElementTree, + tree.getCondition(), + loopBodyEntryBlock, + loopUpdateBlock, + (ConditionalBlock) conditionalBlock, + nodeForCollectionElt); + } + } + + /** + * Conservatively decides whether a loop iterates over all elements of some collection, using the + * following rules: + * + *

    + *
  • only one loop variable + *
  • initialization must be of the form i = 0 + *
  • condition must be of the form (i < col.size()) + *
  • update must be prefix or postfix {@code ++} + *
+ * + * Returns: + * + *
    + *
  • null, if any of the above rules is violated + *
  • the name of the collection if the loop condition is of the form (i < col.size()) + *
+ * + * @param init the initializer of the loop + * @param condition the loop condition + * @param update the loop update + * @return the name of the collection that the loop iterates over all elements of, or null + */ + protected Name nameOfCollectionThatAllElementsAreCalledOn( + StatementTree init, BinaryTree condition, ExpressionStatementTree update) { + Tree.Kind updateKind = update.getExpression().getKind(); + if (updateKind == Tree.Kind.PREFIX_INCREMENT || updateKind == Tree.Kind.POSTFIX_INCREMENT) { + UnaryTree inc = (UnaryTree) update.getExpression(); + + // Verify update is of form i++ or ++i and init is variable initializer. + if (!(init instanceof VariableTree) || !(inc.getExpression() instanceof IdentifierTree)) + return null; + VariableTree initVar = (VariableTree) init; + + // Verify that intializer is i=0. + if (!(initVar.getInitializer() instanceof LiteralTree) + || !((LiteralTree) initVar.getInitializer()).getValue().equals(0)) { + return null; + } + + // Verify that condition is of the form: i < something. + if (!(condition.getLeftOperand() instanceof IdentifierTree)) { + return null; + } + + // Verify that i=0, i statements, Name identifierInHeader, Name iterator) { + AtomicBoolean blockIsIllegal = new AtomicBoolean(false); + final ExpressionTree[] collectionElementTree = {null}; + + TreeScanner scanner = + new TreeScanner() { + @Override + public Void visitUnary(UnaryTree tree, Void p) { + switch (tree.getKind()) { + case PREFIX_DECREMENT: + case POSTFIX_DECREMENT: + case PREFIX_INCREMENT: + case POSTFIX_INCREMENT: + if (getNameFromExpressionTree(tree.getExpression()) == iterator) { + blockIsIllegal.set(true); + } + break; + default: + break; + } + return super.visitUnary(tree, p); + } + + @Override + public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { + if (getNameFromExpressionTree(tree.getVariable()) == iterator) { + blockIsIllegal.set(true); + } + return super.visitCompoundAssignment(tree, p); + } + + @Override + public Void visitAssignment(AssignmentTree tree, Void p) { + Name assignedVariable = getNameFromExpressionTree(tree.getVariable()); + if (assignedVariable == iterator || assignedVariable == identifierInHeader) { + blockIsIllegal.set(true); + } + + return super.visitAssignment(tree, p); + } + + @Override + public Void visitBreak(BreakTree bt, Void p) { + blockIsIllegal.set(true); + return super.visitBreak(bt, p); + } + + @Override + public Void visitReturn(ReturnTree rt, Void p) { + blockIsIllegal.set(true); + return super.visitReturn(rt, p); + } + + // check whether corresponds to collection.get(i) + @Override + public Void visitMethodInvocation(MethodInvocationTree mit, Void p) { + if (isIthCollectionElement(mit, iterator) + && identifierInHeader == getNameFromExpressionTree(mit) + && identifierInHeader != null) { + collectionElementTree[0] = mit; + } + return super.visitMethodInvocation(mit, p); + } + }; + + for (StatementTree stmt : statements) { + scanner.scan(stmt, null); + } + if (!blockIsIllegal.get() && collectionElementTree[0] != null) { + return collectionElementTree[0]; + } + return null; + } + + /** + * Returns the simple name of the identifier referenced by the given expression, or {@code null} + * if the expression does not reference an identifier. + * + * @param expr an expression + * @return the name of the referenced identifier, or {@code null} if none + */ + protected Name getNameFromExpressionTree(ExpressionTree expr) { + if (expr == null) { + return null; + } + switch (expr.getKind()) { + case IDENTIFIER: + return ((IdentifierTree) expr).getName(); + case MEMBER_SELECT: + Element elt = TreeUtils.elementFromUse((MemberSelectTree) expr); + if (elt.getKind() == ElementKind.METHOD || elt.getKind() == ElementKind.FIELD) { + return getNameFromExpressionTree(((MemberSelectTree) expr).getExpression()); + } else { + return null; + } + case METHOD_INVOCATION: + return getNameFromExpressionTree(((MethodInvocationTree) expr).getMethodSelect()); + default: + return null; + } + } + + /** + * Returns the simple name of the identifier declared or referenced by the given statement, or + * {@code null} if the statement does not declare or reference an identifier. + * + * @param expr the {@code StatementTree} + * @return the name of the identifier declared or referenced by the statement, or {@code null} if + * none + */ + protected Name getNameFromStatementTree(StatementTree expr) { + if (expr == null) { + return null; + } + switch (expr.getKind()) { + case VARIABLE: + return ((VariableTree) expr).getName(); + case EXPRESSION_STATEMENT: + return getNameFromExpressionTree(((ExpressionStatementTree) expr).getExpression()); + default: + return null; + } + } + + /** + * Returns the ExpressionTree of the collection in the given expression. + * + * @param expr ExpressionTree + * @return the expression evaluates to or null if it doesn't + */ + protected ExpressionTree collectionTreeFromExpression(ExpressionTree expr) { + switch (expr.getKind()) { + case IDENTIFIER: + return expr; + case MEMBER_SELECT: + Element elt = TreeUtils.elementFromUse((MemberSelectTree) expr); + if (elt.getKind() == ElementKind.METHOD) { + return ((MemberSelectTree) expr).getExpression(); + } else { + return null; + } + case METHOD_INVOCATION: + return collectionTreeFromExpression(((MethodInvocationTree) expr).getMethodSelect()); + default: + return null; + } + } + + /** + * Returns true if the given tree is of the form collection.get(i), where i is the given index + * name. + * + * @param tree the tree to check + * @param index the index variable name + * @return true if the given tree is of the form collection.get(index) + */ + private boolean isIthCollectionElement(Tree tree, Name index) { + if (tree == null || index == null) { + return false; + } + if (tree instanceof MethodInvocationTree + && index == getNameFromExpressionTree(TreeUtils.getIdxForGetCall(tree))) { + MethodInvocationTree mit = (MethodInvocationTree) tree; + ExpressionTree methodSelect = mit.getMethodSelect(); + if (methodSelect instanceof MemberSelectTree) { + MemberSelectTree mst = (MemberSelectTree) methodSelect; + Element receiverElt = TreeUtils.elementFromTree(mst.getExpression()); + return ResourceLeakUtils.isCollection(receiverElt, atypeFactory); + } + } + return false; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java index 66758b166ed..29313294417 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -4,6 +4,8 @@ import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; +import com.sun.source.tree.EnhancedForLoopTree; +import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.NewClassTree; @@ -27,16 +29,22 @@ import java.util.Objects; import java.util.Set; import java.util.StringJoiner; +import java.util.stream.Collectors; import javax.lang.model.SourceVersion; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.qual.CalledMethods; +import org.checkerframework.checker.collectionownership.CollectionOwnershipAnnotatedTypeFactory; +import org.checkerframework.checker.collectionownership.CollectionOwnershipAnnotatedTypeFactory.CollectionOwnershipType; +import org.checkerframework.checker.collectionownership.CollectionOwnershipStore; +import org.checkerframework.checker.collectionownership.qual.CreatesCollectionObligation; import org.checkerframework.checker.mustcall.CreatesMustCallForToJavaExpression; import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory; import org.checkerframework.checker.mustcall.MustCallChecker; @@ -47,9 +55,11 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnalysis; import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory.PotentiallyFulfillingLoop; import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsVisitor; import org.checkerframework.common.accumulation.AccumulationStore; import org.checkerframework.common.accumulation.AccumulationValue; +import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.cfg.ControlFlowGraph; import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.UnderlyingAST.Kind; @@ -57,6 +67,7 @@ import org.checkerframework.dataflow.cfg.block.Block.BlockType; import org.checkerframework.dataflow.cfg.block.ConditionalBlock; import org.checkerframework.dataflow.cfg.block.ExceptionBlock; +import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; import org.checkerframework.dataflow.cfg.node.AssignmentNode; import org.checkerframework.dataflow.cfg.node.ClassNameNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; @@ -69,6 +80,7 @@ import org.checkerframework.dataflow.cfg.node.SuperNode; import org.checkerframework.dataflow.cfg.node.ThisNode; import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.JavaExpressionParseException; import org.checkerframework.dataflow.expression.LocalVariable; @@ -162,6 +174,15 @@ public class MustCallConsistencyAnalyzer { */ private final RLCCalledMethodsAnnotatedTypeFactory cmAtf; + /** The type factory for the Collection Ownership Checker. */ + private final CollectionOwnershipAnnotatedTypeFactory coAtf; + + /** + * True if currently executing a loop body analysis and false if executing a normal consistency + * analysis. + */ + private boolean isLoopBodyAnalysis; + /** * A cache for the result of calling {@code RLCCalledMethodsAnnotatedTypeFactory.getStoreAfter()} * on a node. The cache prevents repeatedly computing least upper bounds on stores. @@ -256,6 +277,48 @@ public Obligation(Set resourceAliases, Set whenTo this.whenToEnforce = ImmutableSet.copyOf(whenToEnforce); } + /** + * Returns a new Obligation. + * + *

We need this method since we frequently need to replace obligations. If the old obligation + * was of a certain subclass, we want the replacement to be as well. Dynamic dispatch then + * allows us to simply call getReplacement() on an obligation and get the replacement of the + * correct (sub)class. + * + * @param resourceAliases set of resource aliases for the new obligation + * @param whenToEnforce when this Obligation should be enforced + * @return a new Obligation with the passed traits + */ + public Obligation getReplacement( + Set resourceAliases, Set whenToEnforce) { + return new Obligation(resourceAliases, whenToEnforce); + } + + /** + * Creates and returns an obligation derived from the given expression. + * + * @param tree the tree from which the Obligation is to be created. Must be {@code + * ExpressionTree} or {@code VariableTree}. + * @return an obligation derived from the given tree + */ + public static Obligation fromTree(Tree tree) { + JavaExpression jx; + Element elem; + if (tree instanceof ExpressionTree) { + jx = JavaExpression.fromTree((ExpressionTree) tree); + elem = TreeUtils.elementFromTree((ExpressionTree) tree); + } else if (tree instanceof VariableTree) { + jx = JavaExpression.fromVariableTree((VariableTree) tree); + elem = TreeUtils.elementFromDeclaration((VariableTree) tree); + } else { + throw new IllegalArgumentException( + "Tree must be ExpressionTree or VariableTree but is " + tree.getClass()); + } + return new Obligation( + ImmutableSet.of(new ResourceAlias(jx, elem, tree)), + Collections.singleton(MethodExitKind.NORMAL_RETURN)); + } + /** * Returns the resource alias in this Obligation's resource alias set corresponding to {@code * localVariableNode} if one is present. Otherwise, returns null. @@ -303,6 +366,26 @@ private boolean canBeSatisfiedThrough(LocalVariableNode localVariableNode) { return getResourceAlias(localVariableNode) != null; } + /** + * Returns true if this contains a resource alias corresponding to {@code localVariableNode}, + * meaning that calling the required methods on {@code localVariableNode} is sufficient to + * satisfy the must-call obligation this object represents. + * + * @param tree a local variable tree + * @return true if a resource alias corresponding to {@code tree} is present + */ + private boolean canBeSatisfiedThrough(Tree tree) { + for (ResourceAlias alias : resourceAliases) { + if (alias.tree.equals(tree) + || ((tree instanceof ExpressionTree) + && JavaExpression.fromTree((ExpressionTree) tree) != null + && alias.reference.equals(JavaExpression.fromTree((ExpressionTree) tree)))) { + return true; + } + } + return false; + } + /** * Does this Obligation contain any resource aliases that were derived from {@link * MustCallAlias} parameters? @@ -425,6 +508,80 @@ public int hashCode() { } } + /** Obligation to call a certain method on all elements of a collection. */ + static class CollectionObligation extends Obligation { + + /** The method that must be called on all elements of the collection. */ + public String mustCallMethod; + + /** + * Create a CollectionObligation from a set of resource aliases. + * + * @param mustCallMethod the method to be called on all elements of the collection + * @param resourceAliases a set of resource aliases + * @param whenToEnforce when this Obligation should be enforced + */ + public CollectionObligation( + String mustCallMethod, + Set resourceAliases, + Set whenToEnforce) { + super(resourceAliases, whenToEnforce); + this.mustCallMethod = mustCallMethod; + } + + /** + * Create a CollectionObligation from an Obligation. + * + * @param obligation the obligation to create a CollectionObligation from + * @param mustCallMethod the method that must be called on the elements of the collection + */ + private CollectionObligation(Obligation obligation, String mustCallMethod) { + super(obligation.resourceAliases, obligation.whenToEnforce); + this.mustCallMethod = mustCallMethod; + } + + /** + * Creates and returns a CollectionObligation derived from the given expression. + * + * @param tree the tree from which to create the CollectionObligation. Must be {@code + * ExpressionTree} or {@code VariableTree}. + * @param mustCallMethod the method that must be called on the elements of the collection + * @return a CollectionObligation derived from the given tree + */ + public static CollectionObligation fromTree(Tree tree, String mustCallMethod) { + return new CollectionObligation(Obligation.fromTree(tree), mustCallMethod); + } + + /** + * Returns a new CollectionObligation. + * + *

We need this method since we frequently need to replace obligations. If the old obligation + * was a CollectionObligation, we want the replacement to be as well. Dynamic dispatch then + * allows us to simply call getReplacement() on an obligation and get the replacement of the + * right class. + * + * @param resourceAliases set of resource aliases for the new obligation + * @return a new CollectionObligation with the passed traits + */ + @Override + public CollectionObligation getReplacement( + Set resourceAliases, Set whenToEnforce) { + return new CollectionObligation(this.mustCallMethod, resourceAliases, whenToEnforce); + } + + @Override + public boolean equals(@Nullable Object obj) { + if (obj == this) { + return true; + } + if (!(obj instanceof CollectionObligation)) { + return false; + } + return super.equals(obj) + && ((CollectionObligation) obj).mustCallMethod.equals(this.mustCallMethod); + } + } + // Is there a different Obligation on every line of the program, or is Obligation mutable? // (Or maybe Obligation is abstractly mutable when you consider the @MustCall types that are not // recorded in Obligation's representation.) Could you clarify? I found the first paragraph @@ -555,11 +712,14 @@ public String stringForErrorMessage() { * #analyze(ControlFlowGraph)}. * * @param rlc the resource leak checker + * @param isLoopBodyAnalysis true if this is a loop body analysis */ - public MustCallConsistencyAnalyzer(ResourceLeakChecker rlc) { + public MustCallConsistencyAnalyzer(ResourceLeakChecker rlc, boolean isLoopBodyAnalysis) { this.cmAtf = (RLCCalledMethodsAnnotatedTypeFactory) ResourceLeakUtils.getRLCCalledMethodsChecker(rlc).getTypeFactory(); + this.coAtf = ResourceLeakUtils.getCollectionOwnershipAnnotatedTypeFactory(cmAtf); + this.isLoopBodyAnalysis = isLoopBodyAnalysis; this.checker = rlc; this.permitStaticOwning = checker.hasOption("permitStaticOwning"); this.permitInitializationLeak = checker.hasOption("permitInitializationLeak"); @@ -604,6 +764,112 @@ public void analyze(ControlFlowGraph cfg) { } } + /** + * Adds {@code CollectionObligation}s if the type of {@code node} is {@code @OwningCollection}. + * + * @param obligations the set of tracked obligations + * @param node the node of a return expression + */ + private void addObligationsForOwningCollectionReturn(Set obligations, Node node) { + LocalVariableNode tmpVar = cmAtf.getTempVarForNode(node); + if (tmpVar != null) { + CollectionOwnershipStore coStore = coAtf.getStoreAfter(node); + CollectionOwnershipType cotype = coAtf.getCoType(tmpVar, coStore); + if (cotype == CollectionOwnershipType.OwningCollection) { + ResourceAlias tmpVarAsResourceAlias = + new ResourceAlias(new LocalVariable(tmpVar), node.getTree()); + List mustCallValues = + coAtf.getMustCallValuesOfResourceCollectionComponent(node.getTree()); + if (mustCallValues == null) { + throw new BugInCF( + "List of MustCall values of component type is null for OwningCollection return value:" + + " " + + node); + } + if (!ResourceLeakUtils.isIterator(node.getType())) { + for (String mustCallMethod : mustCallValues) { + obligations.add( + new CollectionObligation( + mustCallMethod, ImmutableSet.of(tmpVarAsResourceAlias), MethodExitKind.ALL)); + } + } + } + } + } + + /** + * Adds {@code CollectionObligation}s if the method is annotated + * {@code @CreatesCollectionObligation} and the receiver is currently + * {@code @OwningCollectionWithoutObligation}. + * + * @param obligations the set of tracked obligations + * @param node the method invocation node + */ + private void addObligationsForCreatesCollectionObligationAnno( + Set obligations, MethodInvocationNode node) { + ExecutableElement methodElement = TreeUtils.elementFromUse(node.getTree()); + boolean hasCreatesCollectionObligation = + coAtf.getDeclAnnotation(methodElement, CreatesCollectionObligation.class) != null; + if (hasCreatesCollectionObligation) { + Node receiverNode = node.getTarget().getReceiver(); + receiverNode = removeCastsAndGetTmpVarIfPresent(receiverNode); + boolean receiverIsResourceCollection = coAtf.isResourceCollection(receiverNode.getTree()); + if (!receiverIsResourceCollection) { + return; + } + boolean receiverIsOwningField = + coAtf.isOwningCollectionField(TreeUtils.elementFromTree(receiverNode.getTree())); + + CollectionOwnershipStore coStore = coAtf.getStoreBefore(node); + CollectionOwnershipType receiverType = coAtf.getCoType(receiverNode, coStore); + if (receiverType == null) { + throw new BugInCF("Method receiver not in collection ownership store: " + receiverNode); + } + switch (receiverType) { + case OwningCollectionWithoutObligation: + // fall through + case OwningCollection: + if (!receiverIsOwningField) { + List mustCallValues = + coAtf.getMustCallValuesOfResourceCollectionComponent(receiverNode.getTree()); + for (String mustCallMethod : mustCallValues) { + obligations.add( + CollectionObligation.fromTree(receiverNode.getTree(), mustCallMethod)); + } + } + if (receiverIsOwningField) { + TreePath currentPath = cmAtf.getPath(node.getTree()); + MethodTree enclosingMethodTree = TreePathUtil.enclosingMethod(currentPath); + if (enclosingMethodTree != null) { + checkEnclosingMethodIsCreatesMustCallFor(receiverNode, enclosingMethodTree); + } + } + break; + default: + } + } + } + + /** + * Prevents leaking of resource collection fields owned by the enclosing class by simply + * forbidding any access to it from anyone outside the immediate class. + * + * @param node the field access to check + */ + private void checkOwningResourceCollectionFieldAccess(FieldAccessNode node) { + if (coAtf.isOwningCollectionField(node.getElement())) { + String receiverString = receiverAsString(node); + boolean isSelfAccess = "this".equals(receiverString); + boolean isSuperAccess = "super".equals(receiverString); + if (!isSelfAccess && !isSuperAccess) { + checker.reportError( + node.getTree(), + "foreign.owningcollection.field.access", + node.getFieldName().toString()); + } + } + } + /** * Update a set of Obligations to account for a method or constructor invocation. * @@ -626,6 +892,12 @@ private void updateObligationsForInvocation( incrementNumMustCall(node); } + addObligationsForOwningCollectionReturn(obligations, node); + + if (node instanceof MethodInvocationNode) { + addObligationsForCreatesCollectionObligationAnno(obligations, (MethodInvocationNode) node); + } + if (!shouldTrackInvocationResult(obligations, node, false)) { return; } @@ -752,7 +1024,7 @@ private boolean isValidCreatesMustCallForExpression( "tried to remove multiple sets containing a reset expression at once"); } toRemove = obligation; - toAdd = new Obligation(ImmutableSet.of(alias), obligation.whenToEnforce); + toAdd = obligation.getReplacement(ImmutableSet.of(alias), obligation.whenToEnforce); } } @@ -881,7 +1153,7 @@ private boolean areSame(JavaExpression target, @Nullable JavaExpression enclosin .toSet(); obligations.remove(obligationContainingMustCallAlias); obligations.add( - new Obligation( + obligationContainingMustCallAlias.getReplacement( newResourceAliasSet, obligationContainingMustCallAlias.whenToEnforce)); // It is not an error if there is no Obligation containing the must-call // alias. In that case, what has usually happened is that no Obligation was @@ -1041,6 +1313,13 @@ private void removeObligationsAtOwnershipTransferToParameters( obligations.remove(localObligation); } } + + if (coAtf.isOwningCollectionParameter(parameter)) { + Set obligationsForVar = getObligationsForVar(obligations, local); + for (Obligation obligation : obligationsForVar) { + obligations.remove(obligation); + } + } } } } @@ -1058,7 +1337,7 @@ private void removeObligationsAtOwnershipTransferToParameters( */ private void updateObligationsForOwningReturn( Set obligations, ControlFlowGraph cfg, ReturnNode node) { - if (isTransferOwnershipAtReturn(cfg)) { + if (isTransferOwnershipAtReturn(cfg, node)) { Node returnExpr = node.getResult(); returnExpr = getTempVarOrNode(returnExpr); if (returnExpr instanceof LocalVariableNode) { @@ -1091,10 +1370,11 @@ private void updateObligationsForOwningReturn( * Returns true when there is no {@link NotOwning} annotation on the return type. * * @param cfg the CFG of the method + * @param node the return node * @return true iff ownership should be transferred to the return type of the method corresponding * to a CFG */ - private boolean isTransferOwnershipAtReturn(ControlFlowGraph cfg) { + private boolean isTransferOwnershipAtReturn(ControlFlowGraph cfg, ReturnNode node) { if (noLightweightOwnership) { // If not using LO, default to always transfer at return, just like Eclipse does. return true; @@ -1106,6 +1386,22 @@ private boolean isTransferOwnershipAtReturn(ControlFlowGraph cfg) { // not be transferred. MethodTree method = ((UnderlyingAST.CFGMethod) underlyingAST).getMethod(); ExecutableElement executableElement = TreeUtils.elementFromDeclaration(method); + boolean returnTypeHasManualNocAnno = + coAtf.getCoType(executableElement.getReturnType().getAnnotationMirrors()) + == CollectionOwnershipType.NotOwningCollection; + if (returnTypeHasManualNocAnno) { + // return is @NotOwningCollection. No ownership transfer to call-site. + return false; + } else { + // return is @OwningCollection. Report error if @OwningCollection field. + if (coAtf.isOwningCollectionField(TreeUtils.elementFromTree(node.getResult().getTree()))) { + checker.reportError( + node.getTree(), + "transfer.owningcollection.field.ownership", + node.getTree().toString(), + node.getResult().getTree().toString()); + } + } return !cmAtf.hasNotOwning(executableElement); } return false; @@ -1134,6 +1430,7 @@ private void updateObligationsForAssignment( // Ownership transfer to @Owning field. if (lhsElement.getKind() == ElementKind.FIELD) { + checkReassignmentToOwningCollectionField(obligations, assignmentNode); boolean isOwningField = !noLightweightOwnership && cmAtf.hasOwning(lhsElement); // Check that the must-call obligations of the lhs have been satisfied, if the field is // non-final and owning. @@ -1200,6 +1497,68 @@ private void updateObligationsForAssignment( } else if (lhs instanceof LocalVariableNode) { LocalVariableNode lhsVar = (LocalVariableNode) lhs; updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs); + if (isLoopBodyAnalysis) { + handleAssignmentToCollectionElementVariable(obligations, assignmentNode, lhsVar, rhsExpr); + } + } + } + + /** + * In the case of a loop body analysis, this method checks whether the rhs of the assignment + * corresponds to the collection element iterated over, by comparing the AST-trees of the + * collection element and the rhs for structural equality (as defined by + * TreeUtils#sameTree(ExpressionTree, ExpressionTree)). + * + *

If they are determined equal, the lhs variable is added as a resource alias to the + * obligation of the collection element. + * + * @param obligations the set of tracked obligations + * @param node the assignment node to handle + * @param lhsVar the left-hand side for the pseudo-assignment + * @param rhsExpr the right-hand side for the pseudo-assignment, without conversion to a + * temp-variable + */ + private void handleAssignmentToCollectionElementVariable( + Set obligations, AssignmentNode node, LocalVariableNode lhsVar, Node rhsExpr) { + if (!isLoopBodyAnalysis) { + return; + } + Obligation oldObligation = null, newObligation = null; + for (Obligation o : obligations) { + if (oldObligation != null && newObligation != null) { + break; + } + for (ResourceAlias alias : o.resourceAliases) { + if ((alias.tree instanceof ExpressionTree) + && (rhsExpr.getTree() instanceof ExpressionTree) + && TreeUtils.sameTree( + (ExpressionTree) alias.tree, (ExpressionTree) rhsExpr.getTree())) { + Set newResourceAliasesForObligation = + new LinkedHashSet<>(o.resourceAliases); + // It is possible to observe assignments to temporary variables, e.g., + // synthetic assignments to ternary expression variables in the CFG. For such + // cases, use the tree associated with the temp var for the resource alias, + // as that is the tree where errors should be reported. + Tree treeForAlias = + // I don't think we need a tempVar here, since the only case where we're interested + // in such an assignment in the loopBodyAnalysis is if the lhs is an actual variable + // to be used as an alias, so we don't care about the case where lhs is a temp-var. + // typeFactory.isTempVar(lhsVar) + // ? typeFactory.getTreeForTempVar(lhsVar) + // : node.getTree(); + node.getTree(); + ResourceAlias aliasForAssignment = + new ResourceAlias(new LocalVariable(lhsVar), treeForAlias); + newResourceAliasesForObligation.add(aliasForAssignment); + oldObligation = o; + newObligation = new Obligation(newResourceAliasesForObligation, o.whenToEnforce); + break; + } + } + } + if (oldObligation != null && newObligation != null) { + obligations.remove(oldObligation); + obligations.add(newObligation); } } @@ -1248,7 +1607,7 @@ private void addAliasToObligationsContainingVar( Set newAliases = new LinkedHashSet<>(obligation.resourceAliases); newAliases.add(newAlias); - newObligations.add(new Obligation(newAliases, obligation.whenToEnforce)); + newObligations.add(obligation.getReplacement(newAliases, obligation.whenToEnforce)); } } @@ -1319,7 +1678,7 @@ private void removeObligationsContainingVar( whenToEnforce.removeAll(whatToClear); if (!whenToEnforce.isEmpty()) { - newObligations.add(new Obligation(obligation.resourceAliases, whenToEnforce)); + newObligations.add(obligation.getReplacement(obligation.resourceAliases, whenToEnforce)); } } } @@ -1414,7 +1773,8 @@ private void removeObligationsContainingVar( replacements.put(obligation, null); } else { replacements.put( - obligation, new Obligation(newResourceAliasesForObligation, obligation.whenToEnforce)); + obligation, + obligation.getReplacement(newResourceAliasesForObligation, obligation.whenToEnforce)); } } @@ -1427,6 +1787,162 @@ private void removeObligationsContainingVar( } } + /** + * Issues an error if the given (re-)assignment to a resource collection field is not valid. A + * (re-)assignment is valid if the field previously is null, declared final, or of type + * {@code @OwningCollectionWithoutObligation}. + * + * @param obligations current tracked Obligations + * @param node an assignment to a non-final, owning field + */ + private void checkReassignmentToOwningCollectionField( + Set obligations, AssignmentNode node) { + Node lhs = node.getTarget(); + Node rhs = node.getExpression(); + + if (!coAtf.isResourceCollection(lhs.getType()) && !coAtf.isResourceCollection(rhs.getType())) { + return; + } + + boolean isOwningCollectionField = + coAtf.isOwningCollectionField(TreeUtils.elementFromTree(lhs.getTree())); + boolean isFinalField = false; + + if (lhs != null && lhs.getTree() != null) { + Element lhsElt = TreeUtils.elementFromTree(lhs.getTree()); + if (lhsElt != null) { + if (lhsElt.getModifiers().contains(Modifier.FINAL)) { + isFinalField = true; + } + } + } + + TreePath currentPath = cmAtf.getPath(node.getTree()); + MethodTree enclosingMethodTree = TreePathUtil.enclosingMethod(currentPath); + + if (enclosingMethodTree == null) { + // The assignment is taking place in a variable declaration's + // initializer or in an initializer block. + if (node.getTree() instanceof VariableTree) { + // assignment is a field initializer. Permitted only if RHS is + // @OwningCollectionWithoutObligation + // or null. + CollectionOwnershipStore coStore = coAtf.getStoreBefore(node); + CollectionOwnershipType rhsCoType = + coAtf.getCoType(removeCastsAndGetTmpVarIfPresent(rhs), coStore); + if (rhsCoType == null) { + if (TreeUtils.isNullExpression(rhs.getTree())) { + // assignment to null allowed + return; + } else { + rhsCoType = CollectionOwnershipType.NotOwningCollection; + } + } + switch (rhsCoType) { + case OwningCollectionWithoutObligation: + return; + case OwningCollection: + // remove obligations of rhs if lhs is @OC field. + // Although only safe if lhs is also final, remove + // obligations to prevent a second error. The illegal + // assignment error below is issued if lhs not final. + if (isOwningCollectionField) { + Set obligationsForVar = getObligationsForVar(obligations, rhs.getTree()); + for (Obligation obligation : obligationsForVar) { + obligations.remove(obligation); + } + if (isFinalField) { + return; + } + } + // fall through + case NotOwningCollection: + checker.reportError( + node.getTree(), "illegal.owningcollection.field.assignment", rhsCoType.toString()); + return; + case OwningCollectionBottom: + return; + } + } else { + // is an initialization block. Not supported. + checker.reportError( + node, + "unfulfilled.collection.obligations", + coAtf.getMustCallValuesOfResourceCollectionComponent(lhs.getTree()).get(0), + lhs.getTree(), + "Field assignment outside method or declaration might overwrite field's current value"); + } + } else { + // The assignment is taking place in a (possibly constructor) method. + CollectionOwnershipStore coStore = coAtf.getStoreBefore(node); + CollectionOwnershipType rhsCoType = + coAtf.getCoType(removeCastsAndGetTmpVarIfPresent(rhs), coStore); + if (rhsCoType == null) { + if (TreeUtils.isNullExpression(rhs.getTree())) { + rhsCoType = CollectionOwnershipType.OwningCollectionBottom; + } else { + rhsCoType = CollectionOwnershipType.NotOwningCollection; + } + } + + if (isFinalField) { + // special case because final field is not in store before initial assignment. + // final assignment is always allowed. Remove obligations of RHS if field is owning. + if (isOwningCollectionField) { + Set obligationsForVar = getObligationsForVar(obligations, rhs.getTree()); + for (Obligation obligation : obligationsForVar) { + obligations.remove(obligation); + } + } + return; + } + + CollectionOwnershipType lhsCoType = + coAtf.getCoType(removeCastsAndGetTmpVarIfPresent(lhs), coStore); + if (lhsCoType == null) { + throw new BugInCF( + "Expression " + lhs + " cannot be found in CollectionOwnership store " + coStore); + } else if (lhsCoType == CollectionOwnershipType.OwningCollectionBottom + || rhsCoType == CollectionOwnershipType.OwningCollectionBottom) { + throw new BugInCF( + "Expression " + + node + + " has resource collection operand, but @OwningCollectionBottom type."); + } + + switch (lhsCoType) { + case NotOwningCollection: + // doesn't own elements. safe to overwrite. + return; + case OwningCollectionWithoutObligation: + // no obligation. assignment allowed. + // but if rhs is owning, demand CreatesMustCallFor("this") + if (rhsCoType == CollectionOwnershipType.OwningCollection + || rhsCoType == CollectionOwnershipType.NotOwningCollection) { + checkEnclosingMethodIsCreatesMustCallFor(lhs, enclosingMethodTree); + if (isOwningCollectionField) { + Set obligationsForVar = getObligationsForVar(obligations, rhs.getTree()); + for (Obligation obligation : obligationsForVar) { + obligations.remove(obligation); + } + } + } + return; + case OwningCollection: + // assignment not allowed + checker.reportError( + node.getTree(), + "unfulfilled.collection.obligations", + coAtf.getMustCallValuesOfResourceCollectionComponent(lhs.getTree()).get(0), + lhs.getTree(), + "Field assignment might overwrite field's current value"); + return; + default: + return; + } + } + } + /** * Issues an error if the given re-assignment to a non-final, owning field is not valid. A * re-assignment is valid if the called methods type of the lhs before the assignment satisfies @@ -1521,7 +2037,7 @@ private void checkReassignmentToOwningField(Set obligations, Assignm if (!(receiver instanceof LocalVariableNode && varTrackedInObligations(obligations, (LocalVariableNode) receiver)) && !(node.getExpression() instanceof NullLiteralNode)) { - checkEnclosingMethodIsCreatesMustCallFor(node, enclosingMethodTree); + checkEnclosingMethodIsCreatesMustCallFor(node.getTarget(), enclosingMethodTree); } // The following code handles a special case where the field being assigned is itself @@ -1631,27 +2147,29 @@ && varTrackedInObligations(obligations, (LocalVariableNode) receiver)) } /** - * Checks that the method that encloses an assignment is marked with @CreatesMustCallFor - * annotation whose target is the object whose field is being re-assigned. + * Checks that the method that encloses an obligation creation for an owning field (e.g. a + * reassignment to an {@code @Owning} field or an invocation of a method annotated + * {@code @CreatesCollectionObligation} on an {@code @OwningCollection} field) is marked + * with @CreatesMustCallFor annotation whose target is the object for whose field an obligation is + * created. * - * @param node an assignment node whose lhs is a non-final, owning field - * @param enclosingMethod the MethodTree in which the re-assignment takes place + * @param node the owning field node + * @param enclosingMethod the MethodTree in which the obligation creation takes place + * @return true if the check was successful and false if an error had to be reported */ - private void checkEnclosingMethodIsCreatesMustCallFor( - AssignmentNode node, MethodTree enclosingMethod) { - Node lhs = node.getTarget(); - if (!(lhs instanceof FieldAccessNode)) { - return; + private boolean checkEnclosingMethodIsCreatesMustCallFor(Node node, MethodTree enclosingMethod) { + if (!(node instanceof FieldAccessNode)) { + return true; } - if (permitStaticOwning && ((FieldAccessNode) lhs).getReceiver() instanceof ClassNameNode) { - return; + if (permitStaticOwning && ((FieldAccessNode) node).getReceiver() instanceof ClassNameNode) { + return true; } - String receiverString = receiverAsString((FieldAccessNode) lhs); + String receiverString = receiverAsString((FieldAccessNode) node); if ("this".equals(receiverString) && TreeUtils.isConstructor(enclosingMethod)) { // Constructors always create must-call obligations, so there is no need for them to // be annotated. - return; + return true; } ExecutableElement enclosingMethodElt = TreeUtils.elementFromDeclaration(enclosingMethod); MustCallAnnotatedTypeFactory mcAtf = cmAtf.getTypeFactoryOfSubchecker(MustCallChecker.class); @@ -1665,8 +2183,8 @@ private void checkEnclosingMethodIsCreatesMustCallFor( "missing.creates.mustcall.for", enclosingMethodElt.getSimpleName().toString(), receiverString, - ((FieldAccessNode) lhs).getFieldName()); - return; + ((FieldAccessNode) node).getFieldName()); + return false; } List checked = new ArrayList<>(); @@ -1682,7 +2200,7 @@ private void checkEnclosingMethodIsCreatesMustCallFor( } if (targetStr.equals(receiverString)) { // This @CreatesMustCallFor annotation matches. - return; + return true; } checked.add(targetStr); } @@ -1691,8 +2209,9 @@ private void checkEnclosingMethodIsCreatesMustCallFor( "incompatible.creates.mustcall.for", enclosingMethodElt.getSimpleName().toString(), receiverString, - ((FieldAccessNode) lhs).getFieldName(), + ((FieldAccessNode) node).getFieldName(), String.join(", ", checked)); + return false; } /** @@ -1715,6 +2234,11 @@ private String receiverAsString(FieldAccessNode fieldAccessNode) { if (receiver instanceof SuperNode) { return "super"; } + if (receiver instanceof FieldAccessNode) { + return receiverAsString((FieldAccessNode) receiver) + + "." + + ((FieldAccessNode) receiver).getFieldName(); + } throw new TypeSystemError( "unexpected receiver of field assignment: " + receiver + " of type " + receiver.getClass()); } @@ -1945,19 +2469,25 @@ private void propagateObligationsToSuccessorBlocks( updateObligationsForOwningReturn(obligations, cfg, (ReturnNode) node); } else if (node instanceof MethodInvocationNode || node instanceof ObjectCreationNode) { updateObligationsForInvocation(obligations, node, successorAndExceptionType.second); + } else if (node instanceof FieldAccessNode) { + checkOwningResourceCollectionFieldAccess((FieldAccessNode) node); } // All other types of nodes are ignored. This is safe, because other kinds of // nodes cannot create or modify the resource-alias sets that the algorithm is // tracking. } - propagateObligationsToSuccessorBlock( - obligations, - currentBlock, - successorAndExceptionType.first, - successorAndExceptionType.second, - visited, - worklist); + try { + propagateObligationsToSuccessorBlock( + obligations, + currentBlock, + successorAndExceptionType.first, + successorAndExceptionType.second, + visited, + worklist); + } catch (InvalidLoopBodyAnalysisException e) { + // this exception is only thrown from the loop body analysis, which has another entry point. + } } } @@ -1972,6 +2502,8 @@ private void propagateObligationsToSuccessorBlocks( * null} for normal control flow, or a throwable type for exceptional control flow * @param visited block-Obligations pairs already analyzed or already on the worklist * @param worklist current worklist + * @throws InvalidLoopBodyAnalysisException if the propagation is called as part of a loop body + * analysis and a state without input (unreachable in conventional analysis) is reached */ private void propagateObligationsToSuccessorBlock( Set obligations, @@ -1979,7 +2511,8 @@ private void propagateObligationsToSuccessorBlock( Block successor, @Nullable TypeMirror exceptionType, Set visited, - Deque worklist) { + Deque worklist) + throws InvalidLoopBodyAnalysisException { List currentBlockNodes = currentBlock.getNodes(); // successorObligations eventually contains the Obligations to propagate to successor. // The loop below mutates it. @@ -1999,9 +2532,58 @@ private void propagateObligationsToSuccessorBlock( + ((ExceptionBlock) currentBlock).getNode().getTree() + " with exception type " + exceptionType; + TransferInput input = cmAtf.getInput(successor); + if (input == null) { + if (isLoopBodyAnalysis) { + // there are CFG nodes that have no incoming store. In the consistency analysis, + // these are not explored. However, in the loop body analysis, such a node may be explicitly + // explored + // (if a potentially fulfilling loop is in an unreachable block). Hence it is safe to return + // here and + // not propagate obligations, since the state is not reached by the analysis anyways. + // Not just that, but note that if this state is reached, the entire loop is in an state + // unreachable + // by the analysis. If the beginning of the loop was reachable, the analysis wouldn't have + // taken a path that is + // unreachable for it. Hence, the entire loop body analysis can be aborted here. + // The thrown exception is caught in the caller and the loop body analysis aborts, i.e. + // returns + // immediately. + throw new InvalidLoopBodyAnalysisException("Block with no incoming store."); + } else { + throw new BugInCF("block with no outgoing incoming store: " + successor); + } + } + + // check whether this corresponds to the else-cfg-edge of a conditional block + // corresponding to the loop condition of a collection-obligation-fulfilling + // loop. If yes, don't propagate the collection obligations that are fulfilled + // inside the loop. + boolean isElseEdgeOfFulfillingLoop = false; + PotentiallyFulfillingLoop loop = + CollectionOwnershipAnnotatedTypeFactory.getFulfillingLoopForConditionalBlock(currentBlock); + if ((currentBlock instanceof ConditionalBlock) && loop != null) { + ConditionalBlock conditionalBlock = (ConditionalBlock) currentBlock; + if (conditionalBlock.getElseSuccessor().equals(successor)) { + isElseEdgeOfFulfillingLoop = true; + } + } + // Computed outside the Obligation loop for efficiency. - AccumulationStore regularStoreOfSuccessor = cmAtf.getInput(successor).getRegularStore(); + AccumulationStore regularStoreOfSuccessor = input.getRegularStore(); + for (Obligation obligation : obligations) { + + if (isElseEdgeOfFulfillingLoop) { + if (obligation instanceof CollectionObligation) { + String mustCallMethodOfCo = ((CollectionObligation) obligation).mustCallMethod; + if (loop.getCalledMethods().contains(mustCallMethodOfCo)) { + // don't propagate this obligation along this edge, as it was fulfilled + // in the loop that the currentBlock is the conditional block of + continue; + } + } + } // This boolean is true if there is no evidence that the Obligation does not go out // of scope - that is, if there is definitely a resource alias that is in scope in // the successor. @@ -2016,8 +2598,9 @@ private void propagateObligationsToSuccessorBlock( // going out of scope: if this is an exit block or there is no information about any // of them in the successor store, all aliases must be going out of scope and a // consistency check should occur. - if (successor.getType() == BlockType.SPECIAL_BLOCK /* special blocks are exit blocks */ - || obligationGoesOutOfScopeBeforeSuccessor) { + if (!isLoopBodyAnalysis + && (successor.getType() == BlockType.SPECIAL_BLOCK /* special blocks are exit blocks */ + || obligationGoesOutOfScopeBeforeSuccessor)) { MustCallAnnotatedTypeFactory mcAtf = cmAtf.getTypeFactoryOfSubchecker(MustCallChecker.class); @@ -2145,8 +2728,10 @@ private void propagateObligationsToSuccessorBlock( // scope. Set copyOfResourceAliases = new LinkedHashSet<>(obligation.resourceAliases); copyOfResourceAliases.removeIf( - alias -> !aliasInScopeInSuccessor(regularStoreOfSuccessor, alias)); - successorObligations.add(new Obligation(copyOfResourceAliases, obligation.whenToEnforce)); + alias -> + !isLoopBodyAnalysis && !aliasInScopeInSuccessor(regularStoreOfSuccessor, alias)); + successorObligations.add( + obligation.getReplacement(copyOfResourceAliases, obligation.whenToEnforce)); } } @@ -2182,7 +2767,7 @@ private AccumulationStore getStoreForEdgeFromEmptyBlock(Block currentBlock, Bloc /** * Returns true if {@code alias.reference} is definitely in-scope in the successor store: that is, - * there is a value for it in {@code successorStore}. + * there is a value for it in {@code successorStore} or {@code coStore}. * * @param successorStore the regular CalledMethods store of the successor block * @param alias the resource alias to check @@ -2220,6 +2805,11 @@ private Set computeOwningParameters(ControlFlowGraph cfg) { if (cfg.getUnderlyingAST().getKind() == Kind.METHOD) { MethodTree method = ((UnderlyingAST.CFGMethod) cfg.getUnderlyingAST()).getMethod(); Set result = new LinkedHashSet<>(1); + CollectionOwnershipStore coStore = coAtf.getRegularStore(cfg.getEntryBlock()); + if (coStore == null) { + throw new BugInCF("Cannot get initial store for " + cfg); + } + for (VariableTree param : method.getParameters()) { VariableElement paramElement = TreeUtils.elementFromDeclaration(param); boolean hasMustCallAlias = cmAtf.hasMustCallAlias(paramElement); @@ -2237,6 +2827,25 @@ private Set computeOwningParameters(ControlFlowGraph cfg) { // method. incrementNumMustCall(paramElement); } + if (coAtf.isOwningCollectionParameter(paramElement)) { + List mustCallValues = coAtf.getMustCallValuesOfResourceCollectionComponent(param); + if (mustCallValues != null) { + if (!ResourceLeakUtils.isIterator(paramElement.asType())) { + for (String mustCallMethod : mustCallValues) { + result.add( + new CollectionObligation( + mustCallMethod, + ImmutableSet.of( + new ResourceAlias( + new LocalVariable(paramElement), + paramElement, + param, + hasMustCallAlias)), + MethodExitKind.ALL)); + } + } + } + } } return result; } @@ -2280,6 +2889,65 @@ private static boolean varTrackedInObligations( return null; } + /** + * Gets the Obligation whose resource alias set contains the given tree, if one exists in {@code + * obligations}. + * + * @param obligations a set of Obligations + * @param tree variable tree of interest + * @return the Obligation in {@code obligations} whose resource alias set contains {@code tree}, + * or {@code null} if there is no such Obligation + */ + /*package-private*/ static @Nullable Obligation getObligationForVar( + Set obligations, Tree tree) { + for (Obligation obligation : obligations) { + if (obligation.canBeSatisfiedThrough(tree)) { + return obligation; + } + } + return null; + } + + /** + * Gets the set of Obligations whose resource alias set contains the given tree in {@code + * obligations}. + * + * @param obligations a set of Obligations + * @param tree variable tree of interest + * @return the set of Obligations in {@code obligations} whose resource alias set contains {@code + * tree} + */ + /*package-private*/ static Set getObligationsForVar( + Set obligations, Tree tree) { + Set res = new HashSet<>(); + for (Obligation obligation : obligations) { + if (obligation.canBeSatisfiedThrough(tree)) { + res.add(obligation); + } + } + return res; + } + + /** + * Gets the set of Obligations whose resource alias set contain the given local variable, or an + * empty set if none exist. in {@code obligations}. + * + * @param obligations a set of Obligations + * @param node variable of interest + * @return the set of Obligations in {@code obligations} whose resource alias set contains {@code + * node}, or an empty set if there is no such Obligation + */ + /*package-private*/ static Set getObligationsForVar( + Set obligations, LocalVariableNode node) { + Set obligationsForVar = new HashSet<>(); + for (Obligation obligation : obligations) { + if (obligation.canBeSatisfiedThrough(node)) { + obligationsForVar.add(obligation); + } + } + return obligationsForVar; + } + /** * For the given Obligation, checks that at least one of its variables has its {@code @MustCall} * obligation satisfied, based on {@code @CalledMethods} and {@code @MustCall} types in the given @@ -2294,6 +2962,29 @@ private static boolean varTrackedInObligations( private void checkMustCall( Obligation obligation, AccumulationStore cmStore, CFStore mcStore, String outOfScopeReason) { + if (isLoopBodyAnalysis) { + // don't report warnings in loop body analysis + return; + } + + if (obligation instanceof CollectionObligation) { + ResourceAlias firstAlias = obligation.resourceAliases.iterator().next(); + if (!reportedErrorAliases.contains(firstAlias)) { + if (!checker.shouldSkipUses(TreeUtils.elementFromTree(firstAlias.tree))) { + reportedErrorAliases.add(firstAlias); + String methodName = ((CollectionObligation) obligation).mustCallMethod; + checker.reportError( + firstAlias.tree, + "unfulfilled.collection.obligations", + methodName.equals(CollectionOwnershipAnnotatedTypeFactory.UNKNOWN_METHOD_NAME) + ? "Unknown" + : methodName, + firstAlias.stringForErrorMessage(), + outOfScopeReason); + } + } + } + Map> mustCallValues = obligation.getMustCallMethods(cmAtf, mcStore); // Optimization: if mustCallValues is null, always issue a warning (there is no way to @@ -2475,12 +3166,30 @@ public static String formatMissingMustCallMethods(List mustCallVal) { if (size == 0) { throw new TypeSystemError("empty mustCallVal " + mustCallVal); } else if (size == 1) { - return "method " + mustCallVal.get(0); + return "method " + formatMustCallMethod(mustCallVal.get(0)); } else { - return "methods " + String.join(", ", mustCallVal); + return "methods " + + String.join( + ", ", + mustCallVal.stream().map(s -> formatMustCallMethod(s)).collect(Collectors.toList())); } } + /** + * Returns a human-readable representation of a must-call method name. If the given method name + * equals {@link CollectionOwnershipAnnotatedTypeFactory#UNKNOWN_METHOD_NAME}, the literal string + * {@code "Unknown"} is returned. Otherwise, the original name is returned unchanged. + * + * @param method the must-call method name + * @return {@code "Unknown"} if {@code method} equals {@code UNKNOWN_METHOD_NAME}, otherwise + * {@code method} itself + */ + private static String formatMustCallMethod(String method) { + return method.equals(CollectionOwnershipAnnotatedTypeFactory.UNKNOWN_METHOD_NAME) + ? "Unknown" + : method; + } + /** * A pair of a {@link Block} and a set of dataflow facts on entry to the block. Each dataflow fact * represents a set of resource aliases for some tracked resource. The analyzer's worklist @@ -2563,4 +3272,409 @@ public static String collectionToString(Collection bwos) { return result.toString(); } } + + /* + * SECTION: Loop Body Analysis. This section finds loops and analyzes them to determine whether they + * call methods on each element of a collection, which allows for fulfilling collection obligations. + * It reuses much of the cfg traversal logic of the consistency analysis, but is it's own separate + * thing. + */ + + /** + * Traverses the cfg of a method to find and mark enhanced-for-loops that potentially fulfill + * {@code CollectionObligation}s. + * + * @param cfg the cfg of the method to analyze + */ + public void findFulfillingForEachLoops(ControlFlowGraph cfg) { + // The `visited` set contains everything that has been added to the worklist, even if it has + // not yet been removed and analyzed. + Set visited = new HashSet<>(); + Deque worklist = new ArrayDeque<>(); + + // Add any owning parameters to the initial set of variables to track. + BlockWithObligations entry = + new BlockWithObligations(cfg.getEntryBlock(), new HashSet()); + worklist.add(entry); + visited.add(entry); + + while (!worklist.isEmpty()) { + BlockWithObligations current = worklist.remove(); + Block currentBlock = current.block; + + for (IPair successorAndExceptionType : + getSuccessorsExceptIgnoredExceptions(currentBlock)) { + for (Node node : currentBlock.getNodes()) { + if (node instanceof MethodInvocationNode) { + patternMatchEnhancedCollectionForLoop((MethodInvocationNode) node, cfg); + } + } + propagate( + new BlockWithObligations(successorAndExceptionType.first, new HashSet()), + visited, + worklist); + } + } + } + + /** + * Calls a loop-body-analysis on the loop if it is desugared from an enhanced for loop. + * + *

If a {@code MethodInvocationNode} is desugared from an enhanced for loop over a collection + * it corresponds to the node in the synthetic {@code Iterator.next()} method call, which is the + * loop update instruction. The AST node corresponding to the loop itself is in this case + * contained as a field in the {@code MethodInvocationNode}, which is set in the CFG translation + * phase one. + * + *

This method now traverses the CFG upwards to find the loop condition and downwards to find + * the first block of the loop body. With these two blocks, it can then call a loop-body-analysis + * to find the methods the loop calls on the elements of the iterated collection, as part of the + * MustCallOnElements checker. + * + * @param methodInvocationNode the {@code MethodInvocationNode}, for which it is checked, whether + * it is desugared from an enhanced for loop + * @param cfg the enclosing cfg of the {@code MethodInvocationNode} + */ + private void patternMatchEnhancedCollectionForLoop( + MethodInvocationNode methodInvocationNode, ControlFlowGraph cfg) { + boolean nodeIsDesugaredFromEnhancedForLoop = + methodInvocationNode.getIterableExpression() != null; + if (nodeIsDesugaredFromEnhancedForLoop) { + // this is the Iterator.next() call desugared from an enhanced-for-loop + EnhancedForLoopTree loop = methodInvocationNode.getEnhancedForLoop(); + if (loop == null) { + throw new BugInCF( + "MethodInvocationNode.iterableExpression should be non-null iff" + + " MethodInvocationNode.enhancedForLoop is non-null"); + } + + // Find the first block of the loop body. + // Start from the synthetic (desugared) iterator.next() node and traverse the cfg + // until the assignment of the loop iterator variable is found, which is the last + // desugared instruction. The next block is then the start of the loop body. + VariableTree loopVariable = loop.getVariable(); + SingleSuccessorBlock ssblock = (SingleSuccessorBlock) methodInvocationNode.getBlock(); + Iterator nodeIterator = ssblock.getNodes().iterator(); + Node loopVarNode = null; + Node node; + boolean isAssignmentOfIterVar; + do { + while (!nodeIterator.hasNext()) { + ssblock = (SingleSuccessorBlock) ssblock.getSuccessor(); + nodeIterator = ssblock.getNodes().iterator(); + } + node = nodeIterator.next(); + isAssignmentOfIterVar = false; + if ((node instanceof AssignmentNode) && (node.getTree() instanceof VariableTree)) { + loopVarNode = ((AssignmentNode) node).getTarget(); + VariableTree iterVarDecl = (VariableTree) node.getTree(); + isAssignmentOfIterVar = iterVarDecl.getName() == loopVariable.getName(); + } + } while (!isAssignmentOfIterVar); + Block loopBodyEntryBlock = ssblock.getSuccessor(); + + // Find the loop-body-condition + // Start from the synthetic (desugared) iterator.next() node and traverse the cfg + // backwards until the conditional block is found. The previous block is then the block + // containing the desugared loop condition iterator.hasNext(). + Block block = methodInvocationNode.getBlock(); + nodeIterator = block.getNodes().iterator(); + boolean isLoopCondition; + do { + while (!nodeIterator.hasNext()) { + Set predBlocks = block.getPredecessors(); + if (predBlocks.size() == 1) { + block = predBlocks.iterator().next(); + nodeIterator = block.getNodes().iterator(); + } else { + // there is no trivial resolution here. Best we can do is just skip this loop, + // which is of course sound. + return; + // throw new BugInCF( + // "Encountered more than one CFG Block predecessor trying to find the" + // + " enhanced-for-loop update block. Block: "); + } + } + node = nodeIterator.next(); + isLoopCondition = false; + if (node instanceof MethodInvocationNode) { + MethodInvocationTree mit = ((MethodInvocationNode) node).getTree(); + isLoopCondition = TreeUtils.isHasNextCall(mit); + } + } while (!isLoopCondition); + + Block blockContainingLoopCondition = node.getBlock(); + if (blockContainingLoopCondition.getSuccessors().size() != 1) { + throw new BugInCF( + "loop condition has: " + + blockContainingLoopCondition.getSuccessors().size() + + " successors instead of 1."); + } + Block conditionalBlock = blockContainingLoopCondition.getSuccessors().iterator().next(); + if (!(conditionalBlock instanceof ConditionalBlock)) { + throw new BugInCF( + "loop condition successor is not ConditionalBlock, but: " + + conditionalBlock.getClass()); + } + + // add the blocks into a static datastructure in the calledmethodsatf, such that it can + // analyze + // them (call MustCallConsistencyAnalyzer.analyzeFulfillingLoops, which in turn adds the trees + // to the static datastructure in McoeAtf) + PotentiallyFulfillingLoop pfLoop = + new PotentiallyFulfillingLoop( + loop.getExpression(), + loopVarNode.getTree(), + node.getTree(), + loopBodyEntryBlock, + block, + (ConditionalBlock) conditionalBlock, + loopVarNode); + this.analyzeObligationFulfillingLoop(cfg, pfLoop); + } + } + + /** + * Analyze the loop body of a 'potentially-mcoe-obligation-fulfilling-loop', as determined by a + * pre-pattern-match in the MustCallVisitor (in the case of a normal for-loop) or determined by a + * pre-pattern-match in {@code this.patternMatchEnhancedForLoop(MethodInvocationNode)} (in the + * case of an enhanced-for-loop). + * + *

The analysis uses the CalledMethods type of the collection element iterated over to + * determine the methods the loop calls on the collection elements. + * + *

This method should be called after the called-method-analysis is finished (in the {@code + * postAnalyze(cfg)} method of the {@code RLCCalledMethodsAnnotatedTypeFactory}). + * + * @param cfg the cfg of the enclosing method + * @param potentiallyFulfillingLoop the loop to check + */ + public void analyzeObligationFulfillingLoop( + ControlFlowGraph cfg, PotentiallyFulfillingLoop potentiallyFulfillingLoop) { + + // ensure checked loop is initialized in a valid way + Objects.requireNonNull( + potentiallyFulfillingLoop.collectionElementTree, + "CollectionElementAccess tree provided to analyze loop body of an" + + " mcoe-obligation-fulfilling loop is null."); + Objects.requireNonNull( + potentiallyFulfillingLoop.loopBodyEntryBlock, + "Block provided to analyze loop body of an mcoe-obligation-fulfilling loop is null."); + Objects.requireNonNull( + potentiallyFulfillingLoop.loopUpdateBlock, + "Block provided to analyze loop body of an mcoe-obligation-fulfilling loop is null."); + + Block loopBodyEntryBlock = potentiallyFulfillingLoop.loopBodyEntryBlock; + Block loopUpdateBlock = potentiallyFulfillingLoop.loopUpdateBlock; + Tree collectionElement = potentiallyFulfillingLoop.collectionElementTree; + + boolean emptyLoopBody = loopBodyEntryBlock.equals(loopUpdateBlock); + if (emptyLoopBody) { + return; + } + + // The `visited` set contains everything that has been added to the worklist, even if it has + // not yet been removed and analyzed. + Set visited = new HashSet<>(); + Deque worklist = new ArrayDeque<>(); + + // Add an obligation for the element of the collection iterated over + + Obligation collectionElementObligation = Obligation.fromTree(collectionElement); + if (collectionElement instanceof VariableTree) { + VariableElement varElt = TreeUtils.elementFromDeclaration((VariableTree) collectionElement); + boolean hasMustCallAlias = cmAtf.hasMustCallAlias(varElt); + collectionElementObligation = + new Obligation( + ImmutableSet.of( + new ResourceAlias( + new LocalVariable(varElt), varElt, collectionElement, hasMustCallAlias)), + Collections.singleton(MethodExitKind.NORMAL_RETURN)); + } + + BlockWithObligations loopBodyEntry = + new BlockWithObligations( + loopBodyEntryBlock, Collections.singleton(collectionElementObligation)); + + worklist.add(loopBodyEntry); + visited.add(loopBodyEntry); + Set calledMethodsInLoop = null; + + // main loop: propagate obligations block-by-block + while (!worklist.isEmpty()) { + BlockWithObligations current = worklist.remove(); + Block currentBlock = current.block; + + for (IPair successorAndExceptionType : + getSuccessorsExceptIgnoredExceptions(currentBlock)) { + Set obligations = new LinkedHashSet<>(current.obligations); + for (Node node : currentBlock.getNodes()) { + if (node instanceof AssignmentNode) { + updateObligationsForAssignment(obligations, cfg, (AssignmentNode) node); + } + } + + @SuppressWarnings("interning:not.interned") + boolean isLastBlockOfBody = successorAndExceptionType.first == loopUpdateBlock; + if (isLastBlockOfBody) { + Set calledMethodsAfterBlock = + analyzeTypeOfCollectionElement( + currentBlock, potentiallyFulfillingLoop, obligations, loopUpdateBlock); + // intersect the called methods after this block with the accumulated ones so far. + // This is required because there may be multiple "back edges" of the loop, in which + // case we must intersect the called methods between those. + if (calledMethodsAfterBlock != null) { + if (calledMethodsInLoop == null) { + calledMethodsInLoop = calledMethodsAfterBlock; + } else { + calledMethodsInLoop.retainAll(calledMethodsAfterBlock); + } + } + } else { + try { + propagateObligationsToSuccessorBlock( + obligations, + currentBlock, + successorAndExceptionType.first, + successorAndExceptionType.second, + visited, + worklist); + } catch (InvalidLoopBodyAnalysisException e) { + // Expected when analyzing unreachable loop bodies. Safely abort the analysis. + return; + } + } + } + } + + // now put the loop into the static datastructure if it calls any methods on the element + if (calledMethodsInLoop != null && calledMethodsInLoop.size() > 0) { + potentiallyFulfillingLoop.addCalledMethods(calledMethodsInLoop); + CollectionOwnershipAnnotatedTypeFactory.markFulfillingLoop(potentiallyFulfillingLoop); + } + } + + /** + * Checks the CalledMethods store after the given block and determines the CalledMethods type of + * the given tree (which corresponds to the collection element iterated over) and returns the + * union of methods in the CalledMethods type of the collection element and all its resource + * aliases. + * + * @param lastLoopBodyBlock last block of loop body + * @param potentiallyFulfillingLoop loop wrapper of the loop to analyze + * @param obligations the set of tracked obligations + * @param loopUpdateBlock block that updates the loop + * @return the union of methods in the CalledMethods type of the collection element and all its + * resource aliases or {@code null} if the called methods is bottom + */ + private Set analyzeTypeOfCollectionElement( + Block lastLoopBodyBlock, + PotentiallyFulfillingLoop potentiallyFulfillingLoop, + Set obligations, + Block loopUpdateBlock) { + AccumulationStore store = null; + if (lastLoopBodyBlock.getType() == BlockType.CONDITIONAL_BLOCK) { + ConditionalBlock conditionalBlock = (ConditionalBlock) lastLoopBodyBlock; + @SuppressWarnings("interning:not.interned") + boolean thenSuccessor = conditionalBlock.getThenSuccessor() == loopUpdateBlock; + store = cmAtf.getStoreAfterConditionalBlock(conditionalBlock, thenSuccessor); + } else if (lastLoopBodyBlock.getLastNode() == null) { + throw new BugInCF("Loop Body Analysis -- Block " + lastLoopBodyBlock + " has no nodes"); + // store = cmAtf.getStoreAfterBlock(lastLoopBodyBlock); + } else { + store = cmAtf.getStoreAfter(lastLoopBodyBlock.getLastNode()); + } + Obligation collectionElementObligation = + getObligationForVar(obligations, potentiallyFulfillingLoop.collectionElementTree); + if (collectionElementObligation == null) { + // the loop did something weird. Might have reassigned the collection element. + // The sound thing to do is return an empty list. + // TODO SCK look at this. Why is the collection element obligaiton gone? + return new HashSet<>(); + // throw new BugInCF( + // "No obligation for collection element " + // + potentiallyFulfillingLoop.collectionElementTree); + } + + Set calledMethodsAfterThisBlock = null; + + // add the called methods of the ICE + IteratedCollectionElement ice = + store.getIteratedCollectionElement( + potentiallyFulfillingLoop.collectionElementNode, + potentiallyFulfillingLoop.collectionElementTree); + if (ice != null) { + AccumulationValue cmValOfIce = store.getValue(ice); + List calledMethods = getCalledMethods(cmValOfIce); + if (calledMethods != null) { + calledMethodsAfterThisBlock = new HashSet<>(calledMethods); + } + } + + // add the called methods of possible aliases of the collection element + for (ResourceAlias alias : collectionElementObligation.resourceAliases) { + AccumulationValue cmValOfAlias = store.getValue(alias.reference); + if (cmValOfAlias == null) { + continue; + } + List calledMethods = getCalledMethods(cmValOfAlias); + if (calledMethods != null) { + if (calledMethodsAfterThisBlock == null) { + calledMethodsAfterThisBlock = new HashSet<>(calledMethods); + } else { + calledMethodsAfterThisBlock.addAll(calledMethods); + } + } + } + + return calledMethodsAfterThisBlock; + } + + /** + * Returns the set of called methods values given an AccumulationValue or null if the accumulation + * value is bottom. + * + * @param cmVal the accumulation value + * @return the set of called methods of the given value or null if the accumulation value is + * bottom + */ + private List getCalledMethods(AccumulationValue cmVal) { + Set calledMethods = cmVal.getAccumulatedValues(); + if (calledMethods != null) { + return new ArrayList<>(calledMethods); + } else { + for (AnnotationMirror anno : cmVal.getAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + return cmAtf.getCalledMethods(anno); + } else if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethodsBottom")) { + return null; + } + } + } + return new ArrayList<>(); + } + + /** + * If this exception is thrown, it indicates to the caller of the method that the loop body + * analysis should be aborted and immediately return. This happens if a {@code Block} is + * encountered, which does not have an incoming store, meaning the analysis is not supposed to + * reach it. However, in the loop body analysis, such a store may be explicitly explored (if a + * potentially fulfilling loop is in an unreachable {@code Block}). It is then impossible to + * proceed with the analysis, since stores for these {@code Block}s don't exist. Hence, the + * analysis should abort. + */ + @SuppressWarnings("serial") + private static class InvalidLoopBodyAnalysisException extends Exception { + + /** + * Construct an InvalidLoopBodyAnalysisException. + * + * @param message the error message + */ + public InvalidLoopBodyAnalysisException(String message) { + super(message); + } + } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java index bab9b67ba88..2812f090e76 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java @@ -24,6 +24,7 @@ import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.collectionownership.CollectionOwnershipAnnotatedTypeFactory; import org.checkerframework.checker.mustcall.qual.InheritableMustCall; import org.checkerframework.checker.mustcall.qual.MustCallAlias; import org.checkerframework.checker.mustcall.qual.NotOwning; @@ -311,7 +312,9 @@ private void analyzeReturnNode(Set obligations, ReturnNode node) { * {@literal @InheritableMustCall} annotations to the enclosing class. */ private void addMemberAndClassAnnotations() { - WholeProgramInference wpi = resourceLeakAtf.getWholeProgramInference(); + CollectionOwnershipAnnotatedTypeFactory coAtf = + ResourceLeakUtils.getCollectionOwnershipAnnotatedTypeFactory(resourceLeakAtf); + WholeProgramInference wpi = coAtf.getWholeProgramInference(); assert wpi != null : "MustCallInference is running without WPI."; for (VariableElement fieldElt : getOwningFields()) { wpi.addFieldDeclarationAnnotation(fieldElt, OWNING); diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java index 5471c00dbd5..b474510fcb2 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -12,6 +12,7 @@ import javax.lang.model.element.TypeElement; import javax.lang.model.type.TypeMirror; import javax.tools.Diagnostic; +import org.checkerframework.checker.collectionownership.CollectionOwnershipChecker; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.checker.mustcall.MustCallChecker; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; @@ -24,16 +25,17 @@ /** * The entry point for the Resource Leak Checker. This checker only counts the number of {@link * org.checkerframework.checker.mustcall.qual.MustCall} annotations and defines a set of ignored - * exceptions. This checker calls the {@link RLCCalledMethodsChecker} as a direct subchecker, which - * then in turn calls the {@link MustCallChecker} as a subchecker, and afterwards this checker - * traverses the CFG to check whether all MustCall obligations are fulfilled. + * exceptions. This checker calls the {@link CollectionOwnershipChecker} as a direct subchecker, + * which then in turn calls the {@link RLCCalledMethodsChecker} as a subchecker, which calls the + * {@link MustCallChecker} as a subchecker. Afterwards, the consistency analyzer traverses the cfg + * to check whether all MustCall obligations are fulfilled. * - *

The checker hierarchy is: this "empty" RLC → RLCCalledMethodsChecker → - * MustCallChecker + *

The checker hierarchy is: this "empty" RLC → CollectionOwnershipChecker → + * RLCCalledMethodsChecker → MustCallChecker * - *

The MustCallChecker is a subchecker of the RLCCm checker (instead of a sibling), since we want - * them to operate on the same CFG (so we can get both a CM and MC store for a given CFG block), - * which only works if one of them is a subchecker of the other. + *

The subchecker hierarchy is a line graph (instead of siblings), since we want them to operate + * on the same CFG (so we can get a CalledMethods, MustCall, and CollectionOwnership store for a + * given CFG block), which only works if they are in a linear subchecker hierarchy. */ @SupportedOptions({ "permitStaticOwning", @@ -154,7 +156,7 @@ public ResourceLeakChecker() {} @Override protected Set> getSupportedCheckers() { Set> checkers = new LinkedHashSet<>(1); - checkers.add(RLCCalledMethodsChecker.class); + checkers.add(CollectionOwnershipChecker.class); return checkers; } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java index b9d50178758..34b5c434d5e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakUtils.java @@ -2,13 +2,36 @@ import java.util.ArrayList; import java.util.Arrays; +import java.util.Collections; +import java.util.Iterator; import java.util.List; +import java.util.Map; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.AnnotationValue; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.TypeElement; +import javax.lang.model.type.TypeMirror; +import javax.lang.model.type.TypeVariable; +import javax.lang.model.type.WildcardType; +import org.checkerframework.checker.collectionownership.CollectionOwnershipAnnotatedTypeFactory; +import org.checkerframework.checker.collectionownership.CollectionOwnershipChecker; +import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory; import org.checkerframework.checker.mustcall.MustCallChecker; import org.checkerframework.checker.mustcall.MustCallNoCreatesMustCallForChecker; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; +import org.checkerframework.checker.mustcall.qual.MustCall; +import org.checkerframework.checker.mustcall.qual.MustCallUnknown; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsAnnotatedTypeFactory; import org.checkerframework.checker.rlccalledmethods.RLCCalledMethodsChecker; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.TypeSystemError; +import org.checkerframework.javacutil.TypesUtils; /** * Collection of static utility functions related to the various (sub-) checkers within the @@ -26,6 +49,7 @@ private ResourceLeakUtils() { new ArrayList<>( Arrays.asList( ResourceLeakChecker.class.getCanonicalName(), + CollectionOwnershipChecker.class.getCanonicalName(), RLCCalledMethodsChecker.class.getCanonicalName(), MustCallChecker.class.getCanonicalName(), MustCallNoCreatesMustCallForChecker.class.getCanonicalName())); @@ -54,6 +78,7 @@ public static ResourceLeakChecker getResourceLeakChecker(SourceChecker reference if (referenceChecker instanceof ResourceLeakChecker) { return (ResourceLeakChecker) referenceChecker; } else if (referenceChecker instanceof RLCCalledMethodsChecker + || referenceChecker instanceof CollectionOwnershipChecker || referenceChecker instanceof MustCallChecker) { return getResourceLeakChecker(referenceChecker.getParentChecker()); } else { @@ -63,6 +88,60 @@ public static ResourceLeakChecker getResourceLeakChecker(SourceChecker reference } } + /** + * Given a type factory part of the resource leak ecosystem, returns the {@link + * MustCallAnnotatedTypeFactory} in the checker hierarchy. + * + * @param referenceAtf the type factory to retrieve the {@link MustCallAnnotatedTypeFactory} from + * @return the {@link MustCallAnnotatedTypeFactory} in the checker hierarchy + */ + public static MustCallAnnotatedTypeFactory getMustCallAnnotatedTypeFactory( + AnnotatedTypeFactory referenceAtf) { + if (referenceAtf == null) { + throw new IllegalArgumentException("Argument referenceAtf cannot be null"); + } else { + return getMustCallAnnotatedTypeFactory(referenceAtf.getChecker()); + } + } + + /** + * Given a checker part of the resource leak ecosystem, returns the {@link + * MustCallAnnotatedTypeFactory} in the checker hierarchy. + * + * @param referenceChecker the checker to retrieve the {@link MustCallAnnotatedTypeFactory} from + * @return the {@link MustCallAnnotatedTypeFactory} in the checker hierarchy + */ + public static MustCallAnnotatedTypeFactory getMustCallAnnotatedTypeFactory( + SourceChecker referenceChecker) { + if (referenceChecker == null) { + throw new IllegalArgumentException("Argument referenceChecker cannot be null"); + } + + String className = referenceChecker.getClass().getSimpleName(); + if ("MustCallChecker".equals(className) + || "MustCallNoCreatesMustCallForChecker".equals(className)) { + return (MustCallAnnotatedTypeFactory) ((MustCallChecker) referenceChecker).getTypeFactory(); + } else if ("CollectionOwnershipChecker".equals(className)) { + return getMustCallAnnotatedTypeFactory( + referenceChecker.getSubchecker(RLCCalledMethodsChecker.class)); + } else if ("RLCCalledMethodsChecker".equals(className)) { + MustCallChecker mcc = referenceChecker.getSubchecker(MustCallChecker.class); + return getMustCallAnnotatedTypeFactory( + mcc != null + ? mcc + : referenceChecker.getSubchecker(MustCallNoCreatesMustCallForChecker.class)); + } else if ("ResourceLeakChecker".equals(className)) { + return getMustCallAnnotatedTypeFactory( + referenceChecker.getSubchecker(CollectionOwnershipChecker.class)); + } else { + throw new IllegalArgumentException( + "Argument referenceChecker to" + + " ResourceLeakUtils#getMustCallAnnotatedTypeFactory(referenceChecker) expected to" + + " be an RLC checker but is " + + className); + } + } + /** * Given a type factory that is part of the resource leak checker hierarchy, returns the {@link * RLCCalledMethodsChecker} in the checker hierarchy. @@ -88,6 +167,9 @@ public static RLCCalledMethodsChecker getRLCCalledMethodsChecker(SourceChecker r if (referenceChecker instanceof RLCCalledMethodsChecker) { return (RLCCalledMethodsChecker) referenceChecker; } else if (referenceChecker instanceof ResourceLeakChecker) { + return getRLCCalledMethodsChecker( + referenceChecker.getSubchecker(CollectionOwnershipChecker.class)); + } else if (referenceChecker instanceof CollectionOwnershipChecker) { return getRLCCalledMethodsChecker( referenceChecker.getSubchecker(RLCCalledMethodsChecker.class)); } else if (referenceChecker instanceof MustCallChecker) { @@ -99,4 +181,288 @@ public static RLCCalledMethodsChecker getRLCCalledMethodsChecker(SourceChecker r + (referenceChecker == null ? "null" : referenceChecker.getClass().getSimpleName())); } } + + /** + * Given a type factory that is part of the resource leak checker hierarchy, returns the {@link + * RLCCalledMethodsAnnotatedTypeFactory} in the checker hierarchy. + * + * @param referenceAtf the type factory to retrieve the {@link + * RLCCalledMethodsAnnotatedTypeFactory} from; must be part of the Resource Leak hierarchy + * @return the {@link RLCCalledMethodsAnnotatedTypeFactory} in the checker hierarchy + */ + public static RLCCalledMethodsAnnotatedTypeFactory getRLCCalledMethodsAnnotatedTypeFactory( + AnnotatedTypeFactory referenceAtf) { + return getRLCCalledMethodsAnnotatedTypeFactory(referenceAtf.getChecker()); + } + + /** + * Given a checker that is part of the resource leak checker hierarchy, returns the {@link + * RLCCalledMethodsAnnotatedTypeFactory} in the hierarchy. + * + * @param referenceChecker the checker to retrieve the {@link + * RLCCalledMethodsAnnotatedTypeFactory} from; must be part of the Resource Leak hierarchy + * @return the {@link RLCCalledMethodsAnnotatedTypeFactory} in the hierarchy + */ + public static RLCCalledMethodsAnnotatedTypeFactory getRLCCalledMethodsAnnotatedTypeFactory( + SourceChecker referenceChecker) { + return (RLCCalledMethodsAnnotatedTypeFactory) + getRLCCalledMethodsChecker(referenceChecker).getTypeFactory(); + } + + /** + * Given a checker part of the resource leak ecosystem, returns the {@link + * CollectionOwnershipAnnotatedTypeFactory} in the checker hierarchy. + * + * @param referenceChecker the checker to retrieve the {@link + * CollectionOwnershipAnnotatedTypeFactory} from + * @return the {@link CollectionOwnershipAnnotatedTypeFactory} in the checker hierarchy + */ + public static CollectionOwnershipAnnotatedTypeFactory getCollectionOwnershipAnnotatedTypeFactory( + SourceChecker referenceChecker) { + if (referenceChecker == null) { + throw new IllegalArgumentException("Argument referenceChecker cannot be null"); + } + + String className = referenceChecker.getClass().getSimpleName(); + if ("CollectionOwnershipChecker".equals(className) + || "MustCallNoCreatesMustCallForChecker".equals(className)) { + return (CollectionOwnershipAnnotatedTypeFactory) + ((CollectionOwnershipChecker) referenceChecker).getTypeFactory(); + } else if ("RLCCalledMethodsChecker".equals(className)) { + return getCollectionOwnershipAnnotatedTypeFactory(referenceChecker.getParentChecker()); + } else if ("MustCallChecker".equals(className)) { + return getCollectionOwnershipAnnotatedTypeFactory(referenceChecker.getParentChecker()); + } else if ("ResourceLeakChecker".equals(className)) { + return getCollectionOwnershipAnnotatedTypeFactory( + referenceChecker.getSubchecker(CollectionOwnershipChecker.class)); + } else { + throw new IllegalArgumentException( + "Argument referenceChecker to" + + " ResourceLeakUtils#getCollectionOwnershipAnnotatedTypeFactory(referenceChecker)" + + " expected to be an RLC checker but is " + + className); + } + } + + /** + * Given a type factory part of the resource leak ecosystem, returns the {@link + * CollectionOwnershipAnnotatedTypeFactory} in the checker hierarchy. + * + * @param referenceAtf the type factory to retrieve the {@link + * CollectionOwnershipAnnotatedTypeFactory} from + * @return the {@link CollectionOwnershipAnnotatedTypeFactory} in the checker hierarchy + */ + public static CollectionOwnershipAnnotatedTypeFactory getCollectionOwnershipAnnotatedTypeFactory( + AnnotatedTypeFactory referenceAtf) { + if (referenceAtf == null) { + throw new IllegalArgumentException("Argument referenceAtf cannot be null"); + } else { + return getCollectionOwnershipAnnotatedTypeFactory(referenceAtf.getChecker()); + } + } + + /** + * Returns true if the given Element is a java.lang.Iterable or java.util.Iterator type by + * checking whether the raw type of the element is assignable from either. Returns false if + * element is null, or has no valid type. + * + * @param element the element + * @param atf an AnnotatedTypeFactory to get the annotated type of the element + * @return true if the given element is a Java.lang.Iterable or Java.util.Iterator type + */ + public static boolean isCollection(Element element, AnnotatedTypeFactory atf) { + if (element == null) { + return false; + } + AnnotatedTypeMirror elementTypeMirror = atf.getAnnotatedType(element).getErased(); + if (elementTypeMirror == null || elementTypeMirror.getUnderlyingType() == null) { + return false; + } + return isCollection(elementTypeMirror.getUnderlyingType()); + } + + /** + * Returns true if the given {@link TypeMirror} is a java.lang.Iterable or java.util.Iterator + * subclass. This is determined by getting the class of the TypeMirror and checking whether it is + * assignable from either. + * + * @param type the TypeMirror + * @return true if type is a java.lang.Iterable or java.util.Iterator + */ + public static boolean isCollection(TypeMirror type) { + if (type == null) { + return false; + } + Class elementRawType = TypesUtils.getClassFromType(type); + if (elementRawType == null) { + return false; + } + return Iterable.class.isAssignableFrom(elementRawType) + || Iterator.class.isAssignableFrom(elementRawType) + || Map.class.isAssignableFrom(elementRawType); + } + + /** + * Returns true if the given {@link TypeMirror} is a java.util.Iterator subclass. This is + * determined by getting the class of the TypeMirror and checking whether it is assignable from + * java.util.Iterator. + * + * @param type the TypeMirror + * @return true if type is a java.util.Iterator + */ + public static boolean isIterator(TypeMirror type) { + if (type == null) { + return false; + } + Class elementRawType = TypesUtils.getClassFromType(type); + if (elementRawType == null) { + return false; + } + return Iterator.class.isAssignableFrom(elementRawType); + } + + /** + * Safely extract the values of a given element in an {@link AnnotationMirror}. Returns the list + * of such values and the empty list if the element is not present. + * + * @param anno the annotation to extract values from + * @param element the element to access from the annotation + * @return the list of values of the given element in the given annotation and the empty list if + * it is not present + */ + public static List getValuesInAnno(AnnotationMirror anno, ExecutableElement element) { + if (anno == null) { + throw new BugInCF("Annotation " + anno + " must not be null."); + } else { + AnnotationValue av = anno.getElementValues().get(element); + if (av == null) { + return new ArrayList(); + } else { + return AnnotationUtils.annotationValueToList(av, String.class); + } + } + } + + /** + * Returns the list of mustcall obligations for the given {@code TypeMirror} upper bound (either + * the type variable itself if it is concrete or the upper bound if its a wildcard or generic). + * + *

If the type variable has no upper bound, for instance if it is a wildcard with no extends + * clause the method returns null. + * + * @param type the {@code TypeMirror} + * @param mcAtf the {@code MustCallAnnotatedTypeFactory} to get the {@code MustCall} type + * @return the list of mustcall obligations for the upper bound of {@code type} or null if the + * upper bound is null + */ + public static @Nullable List getMcValues( + TypeMirror type, MustCallAnnotatedTypeFactory mcAtf) { + if (type instanceof TypeVariable) { + // a generic - replace with upper bound and return null if it has no upper bound + type = ((TypeVariable) type).getUpperBound(); + if (type == null) { + return null; + } + } else if (type instanceof WildcardType) { + // a wildcard - replace with upper bound and return null if it has no upper bound + type = ((WildcardType) type).getExtendsBound(); + if (type == null) { + return null; + } + } + + AnnotationMirror manualAnno = + AnnotationUtils.getAnnotationByClass(type.getAnnotationMirrors(), MustCall.class); + AnnotationMirror manualMcUnkownAnno = + AnnotationUtils.getAnnotationByClass(type.getAnnotationMirrors(), MustCallUnknown.class); + if (manualAnno != null) { + return getValuesInAnno(manualAnno, mcAtf.getMustCallValueElement()); + } + if (manualMcUnkownAnno != null) { + return Collections.singletonList(CollectionOwnershipAnnotatedTypeFactory.UNKNOWN_METHOD_NAME); + } + + TypeElement typeElement = TypesUtils.getTypeElement(type); + if (typeElement == null) { + return new ArrayList<>(); + } + AnnotationMirror imcAnnotation = + mcAtf.getDeclAnnotation(typeElement, InheritableMustCall.class); + AnnotationMirror mcAnnotation = mcAtf.getDeclAnnotation(typeElement, MustCall.class); + AnnotationMirror mcUnknownAnnotation = + mcAtf.getDeclAnnotation(typeElement, MustCallUnknown.class); + if (mcAnnotation != null) { + return getValuesInAnno(mcAnnotation, mcAtf.getMustCallValueElement()); + } + if (imcAnnotation != null) { + return getValuesInAnno(imcAnnotation, mcAtf.getInheritableMustCallValueElement()); + } + if (mcUnknownAnnotation != null) { + return Collections.singletonList(CollectionOwnershipAnnotatedTypeFactory.UNKNOWN_METHOD_NAME); + } + return new ArrayList<>(); + } + + /** + * Returns the list of mustcall obligations for the given {@code AnnotatedTypeMirror} upper bound + * (either the type variable itself if it is concrete or the upper bound if its a wildcard or + * generic). + * + * @param type the {@code AnnotatedTypeMirror} + * @param mcAtf the {@code MustCallAnnotatedTypeFactory} to get the {@code MustCall} type + * @return the list of mustcall obligations for the upper bound of {@code type} + */ + public static List getMcValues( + AnnotatedTypeMirror type, MustCallAnnotatedTypeFactory mcAtf) { + AnnotationMirror anno = type.getEffectiveAnnotationInHierarchy(mcAtf.TOP); + if (anno == null) { + return Collections.emptyList(); + } + if (AnnotationUtils.areSameByName(anno, mcAtf.TOP)) { + return Collections.singletonList(CollectionOwnershipAnnotatedTypeFactory.UNKNOWN_METHOD_NAME); + } + return getValuesInAnno(anno, mcAtf.getMustCallValueElement()); + } + + /** + * Returns true if the passed {@code TypeMirror} has a manual {@code MustCallUnknown} annotation. + * + * @param typeMirror the {@code TypeMirror} + * @return true if the passed {@code TypeMirror} has a manual {@code MustCallUnknown} annotation + */ + public static boolean hasManualMustCallUnknownAnno(TypeMirror typeMirror) { + if (typeMirror == null) { + return false; + } + for (AnnotationMirror paramAnno : typeMirror.getAnnotationMirrors()) { + if (AnnotationUtils.areSameByName(paramAnno, MustCallUnknown.class.getCanonicalName())) { + return true; + } + } + return false; + } + + /** + * Returns true if the passed {@code AnnotatedTypeMirror} has a manual {@code MustCallUnknown} + * annotation. + * + * @param annotatedTypeMirror the {@code AnnotatedTypeMirror} + * @param mcAtf the annotated type factory of the MustCall type system + * @return true if the passed {@code AnnotatedTypeMirror} has a manual {@code MustCallUnknown} + * annotation + */ + public static boolean hasManualMustCallUnknownAnno( + AnnotatedTypeMirror annotatedTypeMirror, MustCallAnnotatedTypeFactory mcAtf) { + if (annotatedTypeMirror == null) { + return false; + } + AnnotationMirror manualMcAnno = annotatedTypeMirror.getPrimaryAnnotationInHierarchy(mcAtf.TOP); + if (manualMcAnno == null) { + return false; + } + if (AnnotationUtils.areSameByName(manualMcAnno, MustCallUnknown.class.getCanonicalName())) { + return true; + } + return false; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties index a9df3c24711..2e3209b40c6 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties @@ -1,5 +1,5 @@ required.method.not.called=@MustCall %s may not have been invoked on %s or any of its aliases.%nThe type of object is: %s.%nReason for going out of scope: %s -missing.creates.mustcall.for=Method %s re-assigns the non-final, owning field %s.%s, but does not have a corresponding @CreatesMustCallFor annotation. +missing.creates.mustcall.for=Method %s possibly creates a new obligation for the owning field %s.%s, but does not have a corresponding @CreatesMustCallFor annotation. incompatible.creates.mustcall.for=Method %s re-assigns the non-final, owning field %s.%s, but its @CreatesMustCallFor annotation targets %s. reset.not.owning=Calling method %s resets the must-call obligations of the expression %s, which is non-owning. Either annotate its declaration with an @Owning annotation, extract it into a local variable, or write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement. creates.mustcall.for.override.invalid=Method %s cannot override method %s, which defines fewer @CreatesMustCallFor targets.%nfound: %s%nrequired: %s @@ -7,6 +7,8 @@ creates.mustcall.for.invalid.target=Cannot create a must-call obligation for "%s destructor.exceptional.postcondition=Method %s must resolve the must-call obligations of the owning field %s along all paths, including exceptional paths. On an exceptional path, the @EnsuresCalledMethods annotation was not satisfied.%nFound: %s%nRequired: %s mustcallalias.out.of.scope=This @MustCallAlias parameter might go out of scope without being assigned into an owning field of this object (if this is a constructor) or returned.%nReason for going out of scope: %s mustcallalias.method.return.and.param=@MustCallAlias annotations must appear in pairs (one on a return type and one on a parameter type).%nBut %s -owning.override.param=Incompatible ownership for parameter %s.%nfound : no ownership annotation or @NotOwning%nrequired: @Owning%nConsequence: method %s in %s cannot override method %s in %s -owning.override.return=Incompatible ownership for return.%nfound : no ownership annotation or @Owning%nrequired: @NotOwning%nConsequence: method %s in %s cannot override method %s in %s required.method.not.known=The checker cannot determine the must call methods of %s or any of its aliases, so it could not determine if they were called. Typically, this error indicates that you need to write an @MustCall annotation (often on an unconstrained generic type).%nThe type of object is: %s.%nReason for going out of scope: %s +unfulfilled.collection.obligations=@MustCall method %s may not have been invoked on the elements of %s.%nReason for going out of scope: %s +transfer.owningcollection.field.ownership=%s unsafely transfers the ownership away from field %s. Consider annotating the return type @NotOwningCollection. +foreign.owningcollection.field.access=Illegal access of field %s. Cannot access a resource collection field not owned by this class instance. +illegal.owningcollection.field.assignment=Owning resource-collection field initializer assigned to type %s. Expected @OwningCollectionWithoutObligation. Consider moving the assignment into the constructor. diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java index 5884b938e47..a676502fd30 100644 --- a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsAnnotatedTypeFactory.java @@ -3,6 +3,7 @@ import com.google.common.collect.BiMap; import com.google.common.collect.HashBiMap; import com.sun.source.tree.ClassTree; +import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.LambdaExpressionTree; import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; @@ -12,6 +13,7 @@ import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.Collections; +import java.util.HashSet; import java.util.List; import java.util.Queue; import java.util.Set; @@ -47,6 +49,7 @@ import org.checkerframework.dataflow.cfg.ControlFlowGraph; import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.block.Block; +import org.checkerframework.dataflow.cfg.block.ConditionalBlock; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; @@ -116,6 +119,52 @@ public class RLCCalledMethodsAnnotatedTypeFactory extends CalledMethodsAnnotated */ private final BiMap tempVarToTree = HashBiMap.create(); + /** + * Set of potentially collection-obligation-fulfilling loops. Found in the MustCallVisitor, which + * checks the header and (parts of the) body. + */ + private static final Set potentiallyFulfillingLoops = new HashSet<>(); + + /** + * Construct a {@code PotentiallyFulfillingLoop} and add it to the static set of such loops to + * have their loop body analyzed for possibly fulfilling collection obligations. + * + * @param collectionTree AST {@code Tree} for collection iterated over + * @param collectionElementTree AST {@code Tree} for collection element iterated over + * @param condition AST {@code Tree} for loop condition + * @param loopBodyEntryBlock cfg {@code Block} for loop body entry + * @param loopUpdateBlock {@code Block} containing loop update + * @param loopConditionalBlock {@code Block} containing loop condition + * @param collectionEltNode cfg {@code Node} for collection element iterated over + */ + public static void addPotentiallyFulfillingLoop( + ExpressionTree collectionTree, + Tree collectionElementTree, + Tree condition, + Block loopBodyEntryBlock, + Block loopUpdateBlock, + ConditionalBlock loopConditionalBlock, + Node collectionEltNode) { + potentiallyFulfillingLoops.add( + new PotentiallyFulfillingLoop( + collectionTree, + collectionElementTree, + condition, + loopBodyEntryBlock, + loopUpdateBlock, + loopConditionalBlock, + collectionEltNode)); + } + + /** + * Returns the static set of {@code PotentiallyFulfillingLoop}s scheduled for analysis. + * + * @return the static set of {@code PotentiallyFulfillingLoop}s scheduled for analysis + */ + public static Set getPotentiallyFulfillingLoops() { + return potentiallyFulfillingLoops; + } + /** * Creates a new RLCCalledMethodsAnnotatedTypeFactory. * @@ -182,7 +231,8 @@ protected ControlFlowGraph analyze( capturedStore); assert root != null : "@AssumeAssertion(nullness): at this point root is always nonnull"; rlc.setRoot(root); - MustCallConsistencyAnalyzer mustCallConsistencyAnalyzer = new MustCallConsistencyAnalyzer(rlc); + MustCallConsistencyAnalyzer mustCallConsistencyAnalyzer = + new MustCallConsistencyAnalyzer(rlc, false); mustCallConsistencyAnalyzer.analyze(cfg); // Inferring owning annotations for @Owning fields/parameters, @EnsuresCalledMethods for @@ -433,6 +483,36 @@ public boolean canCreateObligations() { return !rlc.hasOption(MustCallChecker.NO_CREATES_MUSTCALLFOR); } + /** + * Fetches the store from the results of dataflow for {@code block}. The store after {@code block} + * is returned. + * + * @param block a block + * @return the appropriate CFStore, populated with CalledMethods annotations, from the results of + * running dataflow + */ + public AccumulationStore getStoreAfterBlock(Block block) { + return flowResult.getStoreAfter(block); + } + + /** + * Returns the then or else store after {@code block} depending on the value of {@code then} is + * returned. + * + * @param block a conditional block + * @param then wether the then store should be returned + * @return the then or else store after {@code block} depending on the value of {@code then} is + * returned + */ + public AccumulationStore getStoreAfterConditionalBlock(ConditionalBlock block, boolean then) { + TransferInput transferInput = flowResult.getInput(block); + assert transferInput != null : "@AssumeAssertion(nullness): transferInput should be non-null"; + if (then) { + return transferInput.getThenStore(); + } + return transferInput.getElseStore(); + } + @Override @SuppressWarnings("TypeParameterUnusedInFormals") // Intentional abuse public > @@ -603,4 +683,125 @@ public TransferInput getInput(Block block) return analysis.getInput(block); } } + + /** Wrapper for a loop that potentially calls methods on all elements of a collection/array. */ + public static class PotentiallyFulfillingLoop { + + /** AST {@code Tree} for collection iterated over. */ + public final ExpressionTree collectionTree; + + /** AST {@code Tree} for collection element iterated over. */ + public final Tree collectionElementTree; + + /** AST {@code Tree} for loop condition. */ + public final Tree condition; + + /** + * The methods that the loop definitely calls on all elements of the collection it iterates + * over. + */ + protected final Set calledMethods; + + /** cfg {@code Block} containing the loop body entry. */ + public final Block loopBodyEntryBlock; + + /** cfg {@code Block} containing the loop update. */ + public final Block loopUpdateBlock; + + /** cfg conditional {@link Block} following loop condition. */ + public final ConditionalBlock loopConditionalBlock; + + /** cfg {@code Node} for the collection element iterated over. */ + public final Node collectionElementNode; + + /** + * Constructs a new {@code PotentiallyFulfillingLoop} + * + * @param collectionTree AST {@link Tree} for collection iterated over + * @param collectionElementTree AST {@link Tree} for collection element iterated over + * @param condition AST {@link Tree} for loop condition + * @param loopBodyEntryBlock cfg {@link Block} for the loop body entry + * @param loopUpdateBlock cfg {@link Block} for the loop update + * @param loopConditionalBlock cfg conditional {@link Block} following loop condition + * @param collectionEltNode cfg {@link Node} for the collection element iterated over + */ + public PotentiallyFulfillingLoop( + ExpressionTree collectionTree, + Tree collectionElementTree, + Tree condition, + Block loopBodyEntryBlock, + Block loopUpdateBlock, + ConditionalBlock loopConditionalBlock, + Node collectionEltNode) { + this.collectionTree = collectionTree; + this.collectionElementTree = collectionElementTree; + this.condition = condition; + this.calledMethods = new HashSet<>(); + this.loopBodyEntryBlock = loopBodyEntryBlock; + this.loopUpdateBlock = loopUpdateBlock; + this.loopConditionalBlock = loopConditionalBlock; + this.collectionElementNode = collectionEltNode; + } + + /** + * Add methods that are guaranteed to be invoked on every element of the collection the loop + * iterates over. + * + * @param methods the set of methods to add + */ + public void addCalledMethods(Set methods) { + calledMethods.addAll(methods); + } + + /** + * Returns methods that are guaranteed to be invoked on every element of the collection the loop + * iterates over. + * + * @return the set of methods the loop calls on all elements of the iterated collection + */ + public Set getCalledMethods() { + return calledMethods; + } + } + + /** + * After running the called-methods analysis, call the consistency analyzer to analyze the loop + * bodys of 'potentially-collection-obligation-fulfilling-loops', as determined by a + * pre-pattern-match in the MustCallVisitor. + * + *

The analysis uses the CalledMethods type of the collection element iterated over to + * determine the methods the loop calls on the collection elements. + * + * @param cfg the cfg of the enclosing method + */ + @Override + public void postAnalyze(ControlFlowGraph cfg) { + MustCallConsistencyAnalyzer mustCallConsistencyAnalyzer = + new MustCallConsistencyAnalyzer(ResourceLeakUtils.getResourceLeakChecker(this), true); + + // traverse the cfg to find enhanced-for-loops over collections and perform a + // loop-body-analysis. + // since this runs before the consistency analysis, we unfortunately have to traverse the cfg + // twice. The first time to find these for-each loop, and the second time much later to do the + // final consistency analysis. + mustCallConsistencyAnalyzer.findFulfillingForEachLoops(cfg); + + // perform loop-body-analysis on normal for-loops that were pattern matched on the AST + if (potentiallyFulfillingLoops.size() > 0) { + Set analyzed = new HashSet<>(); + for (PotentiallyFulfillingLoop potentiallyFulfillingLoop : potentiallyFulfillingLoops) { + Tree collectionElementTree = potentiallyFulfillingLoop.collectionElementTree; + boolean loopContainedInThisMethod = + cfg.getNodesCorrespondingToTree(collectionElementTree) != null; + if (loopContainedInThisMethod) { + mustCallConsistencyAnalyzer.analyzeObligationFulfillingLoop( + cfg, potentiallyFulfillingLoop); + analyzed.add(potentiallyFulfillingLoop); + } + } + potentiallyFulfillingLoops.removeAll(analyzed); + } + + super.postAnalyze(cfg); + } } diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsTransfer.java index 28bd017fafe..eb6f6cc3250 100644 --- a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsTransfer.java @@ -1,10 +1,13 @@ package org.checkerframework.checker.rlccalledmethods; import com.sun.source.tree.MethodInvocationTree; +import java.util.Arrays; import java.util.List; +import java.util.Map; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.CalledMethodsTransfer; import org.checkerframework.checker.mustcall.CreatesMustCallForToJavaExpression; import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory; @@ -14,13 +17,17 @@ import org.checkerframework.common.accumulation.AccumulationValue; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; import org.checkerframework.dataflow.cfg.node.SwitchExpressionNode; import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.javacutil.AnnotationMirrorSet; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypesUtils; @@ -45,6 +52,80 @@ public RLCCalledMethodsTransfer(RLCCalledMethodsAnalysis analysis) { this.rlTypeFactory = (RLCCalledMethodsAnnotatedTypeFactory) analysis.getTypeFactory(); } + @Override + public void accumulate( + Node node, TransferResult result, String... values) { + super.accumulate(node, result, values); + updateStoreForIteratedCollectionElement(Arrays.asList(values), result, node); + } + + /** + * Add the collection elements iterated over in potentially Mcoe-obligation-fulfilling loops to + * the store. + */ + @Override + public AccumulationStore initialStore( + UnderlyingAST underlyingAST, List parameters) { + AccumulationStore store = super.initialStore(underlyingAST, parameters); + RLCCalledMethodsAnnotatedTypeFactory cmAtf = + (RLCCalledMethodsAnnotatedTypeFactory) this.analysis.getTypeFactory(); + for (RLCCalledMethodsAnnotatedTypeFactory.PotentiallyFulfillingLoop loop : + RLCCalledMethodsAnnotatedTypeFactory.getPotentiallyFulfillingLoops()) { + IteratedCollectionElement collectionElementJE = + new IteratedCollectionElement(loop.collectionElementNode, loop.collectionElementTree); + store.insertValue(collectionElementJE, cmAtf.top); + } + return store; + } + + /** + * Accumulates the called methods to this collection element if the given node is the element of a + * collection iterated over in a potentially-Mcoe-obligation-fulfilling loop. + * + * @param valuesAsList the list of called methods + * @param result the transfer result + * @param node a cfg node + */ + private void updateStoreForIteratedCollectionElement( + List valuesAsList, + TransferResult result, + Node node) { + IteratedCollectionElement collectionElement = + result.getRegularStore().getIteratedCollectionElement(node, node.getTree()); + if (collectionElement != null) { + AccumulationValue flowValue = result.getRegularStore().getValue(collectionElement); + if (flowValue != null) { + // Dataflow has already recorded information about the target. Integrate it into + // the list of values in the new annotation. + AnnotationMirrorSet flowAnnos = flowValue.getAnnotations(); + assert flowAnnos.size() <= 1; + for (AnnotationMirror anno : flowAnnos) { + if (atypeFactory.isAccumulatorAnnotation(anno)) { + List oldFlowValues = + AnnotationUtils.getElementValueArray(anno, calledMethodsValueElement, String.class); + // valuesAsList cannot have its length changed -- it is backed by an + // array. getElementValueArray returns a new, modifiable list. + oldFlowValues.addAll(valuesAsList); + valuesAsList = oldFlowValues; + } + } + } + AnnotationMirror newAnno = atypeFactory.createAccumulatorAnnotation(valuesAsList); + if (result.containsTwoStores()) { + updateValueAndInsertIntoStore(result.getThenStore(), collectionElement, valuesAsList); + updateValueAndInsertIntoStore(result.getElseStore(), collectionElement, valuesAsList); + } else { + updateValueAndInsertIntoStore(result.getRegularStore(), collectionElement, valuesAsList); + } + Map exceptionalStores = result.getExceptionalStores(); + exceptionalStores.forEach( + (tm, s) -> + s.replaceValue( + collectionElement, + analysis.createSingleAnnotationValue(newAnno, collectionElement.getType()))); + } + } + @Override public TransferResult visitTernaryExpression( TernaryExpressionNode node, TransferInput input) { @@ -167,12 +248,7 @@ public void updateStoreWithTempVar( if (anm == null) { anm = rlTypeFactory.top; } - if (result.containsTwoStores()) { - result.getThenStore().insertValue(localExp, anm); - result.getElseStore().insertValue(localExp, anm); - } else { - result.getRegularStore().insertValue(localExp, anm); - } + insertIntoStores(result, localExp, anm); } } } diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties new file mode 100644 index 00000000000..1935440e2db --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties @@ -0,0 +1,2 @@ +owning.override.return=Incompatible ownership for return.%nfound : no ownership annotation or @Owning%nrequired: @NotOwning%nConsequence: method %s in %s cannot override method %s in %s +owning.override.param=Incompatible ownership for parameter %s.%nfound : no ownership annotation or @NotOwning%nrequired: @Owning%nConsequence: method %s in %s cannot override method %s in %s diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/ResourceLeakCollections.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ResourceLeakCollections.java new file mode 100644 index 00000000000..6642b6eb3d8 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/ResourceLeakCollections.java @@ -0,0 +1,25 @@ +package org.checkerframework.checker.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +/** Tests for the Resource Leak Checker for Collections. */ +public class ResourceLeakCollections extends CheckerFrameworkPerDirectoryTest { + public ResourceLeakCollections(List testFiles) { + super( + testFiles, + ResourceLeakChecker.class, + "resourceleak", + "-AwarnUnneededSuppressions", + "-encoding", + "UTF-8"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"resourceleak-collections"}; + } +} diff --git a/checker/tests/mustcall/ListOfMustCall.java b/checker/tests/mustcall/ListOfMustCall.java index 3d6648ee20c..21c0d5d2ca8 100644 --- a/checker/tests/mustcall/ListOfMustCall.java +++ b/checker/tests/mustcall/ListOfMustCall.java @@ -12,8 +12,6 @@ @InheritableMustCall("a") class ListOfMustCall { static void test(ListOfMustCall lm) { - // :: error: type.argument - // :: error: type.arguments.not.inferred List l = new ArrayList<>(); // add(E e) takes an object of the type argument's type l.add(lm); @@ -22,8 +20,6 @@ static void test(ListOfMustCall lm) { } static void test2(ListOfMustCall lm) { - // :: error: type.argument - // :: error: type.arguments.not.inferred List<@MustCall("a") ListOfMustCall> l = new ArrayList<>(); l.add(lm); l.remove(lm); diff --git a/checker/tests/resourceleak-collections/CollectionOwnershipBasicTyping.java b/checker/tests/resourceleak-collections/CollectionOwnershipBasicTyping.java new file mode 100644 index 00000000000..35aa0679afd --- /dev/null +++ b/checker/tests/resourceleak-collections/CollectionOwnershipBasicTyping.java @@ -0,0 +1,146 @@ +import java.net.Socket; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.collectionownership.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +/* + * Test whether the defaults of resource collection fields, parameters, return types and new +allocations + * are as expected. + */ +class CollectionOwnershipBasicTyping { + + int n = 10; + + /* + * Check that this return is allowed. The local list defaults to @OwningCollection, which + * the return type does too. Thus, return value is consistent with the return type. + */ + Collection checkReturn() { + List list = new ArrayList<>(); + return list; + } + + /* + * Check that this return is disallowed. The parameter list defaults to @NotOwningCollection, + * which is a supertype of the @OwningCollection return type. + * Thus, return value is inconsistent with the return type. + */ + Collection checkReturn(List list) { + // :: error: return + return list; + } + + // this return looks harmless. However, it returns a collection, but not its ownership. + // Since no obligation will be created at call-site (it expects a non-owning collection), + // this method must ensure the returned collection has no obligations, which it fails to + // do in this case. + @NotOwningCollection + Collection checkIllegalNotOwningReturn() { + List l = new ArrayList<>(); + // :: error: unfulfilled.collection.obligations + l.add(new Socket()); + return l; + } + + // this is the correct version of above. It passes ownership to another method first, + // and then returns the non-owning reference. + @NotOwningCollection + Collection checkLegalNotOwningReturn1() { + List list = new ArrayList<>(); + try { + list.add(new Socket("", 42)); + } catch (Exception e) { + } + closeElements(list); + return list; + } + + @NotOwningCollection + Collection checkLegalNotOwningReturn2() { + List list = new ArrayList<>(); + return list; + } + + // check that unrefinement in assignments is allowed. + void checkUnrefinement() { + List list = new ArrayList<>(); + List newOwner = list; + // newOwner : @OwningCollection, list: @NotOwningCollection + list = newOwner; + // newOwner = @NotOwningCollection, list: @OwningCollection + closeElements(list); + } + + void testAssignmentTransfersOwnership() { + // col is overwritten and its obligation never fulfilled or passed on + Collection col = new ArrayList<>(); + // :: error: unfulfilled.collection.obligations + col.add(new Socket()); + Collection col2 = new ArrayList<>(); + // col : @OwningCollection, col2 : @OwningCollection + col = col2; + // col : @OwningCollection, col2 : @NotOwningCollection + + // col2 is NotOwningCollection, so the second call should fail + checkArgIsOwning(col); + // :: error: argument + checkArgIsOwning(col2); + } + + /* + * Check that a resource collection constructed without explicit type argument is of type @OwningCollection + * as well. + */ + void testDiamond() { + Collection col = new ArrayList<>(); + col.add(new Socket()); + // :: error: argument + checkArgIsOCwoO(col); + closeElements(col); + } + + void checkAdvancedDiamond() { + // check that this doesn't create an obligation and defaults to @OwningCollectionBottom + Collection<@MustCall({}) Socket> c = new ArrayList<>(); + checkArgIsBottom(c); + + // these all create obligations + + Collection c1 = new ArrayList<>(); + Collection<@MustCall("close") Object> c2 = new ArrayList<>(); + Collection<@MustCallUnknown Object> c3 = new ArrayList<>(); + c.add(new Socket()); + // :: error: unfulfilled.collection.obligations + c1.add(new Socket()); + // :: error: unfulfilled.collection.obligations + c2.add(new Socket()); + // :: error: unfulfilled.collection.obligations + c3.add(new Socket()); + } + + void closeElements(@OwningCollection Collection socketCollection) { + for (Socket s : socketCollection) { + try { + s.close(); + } catch (Exception e) { + } + } + } + + void checkArgIsBottom(Collection collection) {} + + // these two methods take on unfulfillable obligations and thus throw an error + + void checkArgIsOwning( + // :: error: unfulfilled.collection.obligations + @OwningCollection Collection collection) {} + + void checkArgIsOCwoO( + // :: error: illegal.type.annotation + @OwningCollectionWithoutObligation + Collection collection) {} +} diff --git a/checker/tests/resourceleak-collections/CollectionOwnershipDefaults.java b/checker/tests/resourceleak-collections/CollectionOwnershipDefaults.java new file mode 100644 index 00000000000..7c5892fe7a0 --- /dev/null +++ b/checker/tests/resourceleak-collections/CollectionOwnershipDefaults.java @@ -0,0 +1,127 @@ +import java.net.Socket; +import java.util.ArrayList; +import java.util.Collection; +import java.util.LinkedList; +import java.util.List; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.collectionownership.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +/* + * Test whether the defaults of resource collection fields, parameters, return types and new allocations + * are as expected. + */ +class CollectionOwnershipDefaults { + + int n = 10; + + /* + * Check that manual MustCall annotations are correctly considered when deciding whether + * something is a resource collection. + */ + public void detectResourceCollection( + List<@MustCall({}) Socket> l1, + Collection<@MustCall({"close"}) Socket> l2, + LinkedList l3, + ArrayList l4, + ArrayList<@MustCall({"a"}) String> l5) { + // not a resource collection, this call succeeds. + checkArgIsOwning(l1); + // a resource collection, this call fails. + // :: error: argument + checkArgIsOwning(l2); + // a resource collection, this call fails. + // :: error: argument + checkArgIsOwning(l3); + // not a resource collection, this call succeeds. + checkArgIsOwning(l4); + // a resource collection, this call fails. + // :: error: argument + checkArgIsOwning(l5); + } + + /* + * This method checks that its parameter defaults to @NotOwningCollection. + */ + void checkParamIsNotOwningCollection(List list) { + // list : @NotOwningCollection. Thus, next line should throw an error. + + // :: error: argument + checkArgIsOwning(list); + } + + /* + * Return type should default to @OwningCollection. Thus this is perfectly okay. + */ + List identity(@OwningCollection List list) { + return list; + } + + /* + * Check whether manual annotations on the return type correctly override the default. + */ + @NotOwningCollection + List overrideReturnType(List list) { + return list; + } + + void overrideReturnTypeClient() { + // the arraylist passed to the method is never closed. The ownership is not passed + // to overrideReturnType(), since parameters are @NotOwningCollection by default + List notOwninglist = overrideReturnType(new ArrayList()); + List owninglist = identity(new ArrayList()); + + checkArgIsOwning(owninglist); + // :: error: argument + checkArgIsOwning(notOwninglist); + } + + /* + * Checks that an @OwningCollection can be passed to a resource collection parameter (because it should default + * to @OwningCollection). I.e. check that the resource collection parameter default is visible at call-site as well. + */ + void checkResourceCollectionParameterDefault() { + List list = new ArrayList(); + closeElements(identity(list)); + } + + /* + * Checks that return value of a resource collection correctly defaults to @OwningCollection + */ + void checkResourceCollectionReturnValueDefault() { + List returnVal = identity(new ArrayList()); + // returnVal supposed to be @OwningCollection. Thus, first call should succeed, second fail. + + checkArgIsOwning(returnVal); + // :: error: argument + checkArgIsOCwoO(returnVal); + } + + /* + * Checks that a newly allocated resource collection has type @OwningCollection. + */ + void checkNewResourceCollectionDefault() { + List newResourceCollection = new ArrayList(); + checkArgIsOwning(newResourceCollection); + // :: error: argument + checkArgIsOCwoO(newResourceCollection); + } + + void closeElements(@OwningCollection Collection socketCollection) { + for (Socket s : socketCollection) { + try { + s.close(); + } catch (Exception e) { + } + } + } + + void checkArgIsOwning( + // :: error: unfulfilled.collection.obligations + @OwningCollection Collection collection) {} + + void checkArgIsOCwoO( + // :: error: illegal.type.annotation + @OwningCollectionWithoutObligation + Collection collection) {} +} diff --git a/checker/tests/resourceleak-collections/LoopBodyAnalysisTest.java b/checker/tests/resourceleak-collections/LoopBodyAnalysisTest.java new file mode 100644 index 00000000000..077ce0d18fe --- /dev/null +++ b/checker/tests/resourceleak-collections/LoopBodyAnalysisTest.java @@ -0,0 +1,143 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.collectionownership.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class LoopBodyAnalysisTests { + + void fullSatisfyCollection(@OwningCollection Collection resources) { + for (Resource r : resources) { + r.close(); + r.flush(); + } + checkArgIsOCWO(resources); + } + + // here, the argument defaults to @NotOwningCollection. + // the loop should not change that type + void fullSatisfyCollectionNotOwning(Collection resources) { + for (Resource r : resources) { + r.close(); + r.flush(); + } + // :: error: argument + checkArgIsOCWO(resources); + } + + // :: error: unfulfilled.collection.obligations + void partialSatisfyCollectionShouldError(@OwningCollection Collection resources) { + for (Resource r : resources) { + r.close(); + } + // :: error: argument + checkArgIsOCWO(resources); + } + + void multipleMustCallPartial() { + List l = new ArrayList<>(); + // :: error: unfulfilled.collection.obligations + l.add(new Resource()); + for (Resource r : l) { + r.close(); + } + // :: error: argument + checkArgIsOCWO(l); + } + + void multipleMustCallFull() { + List l = new ArrayList<>(); + l.add(new Resource()); + for (Resource r : l) { + r.close(); + r.flush(); + } + checkArgIsOCWO(l); + } + + void tryCatchShouldWork(@OwningCollection List resources) { + for (Resource r : resources) { + try { + r.close(); + r.flush(); + } catch (Exception e) { + } + } + } + + void methodCallInsideLoop(@OwningCollection List resources) { + for (Resource r : resources) { + doCloseFlush(r); + } + } + + // :: error: unfulfilled.collection.obligations + void earlyBreak(@OwningCollection List resources) { + for (Resource r : resources) { + r.close(); + r.flush(); + break; // not all elements visited + } + } + + // TODO SCK: uncomment these tests + // void tryWithResources(@OwningCollection List resources) { + // for (Resource r : resources) { + // try (Resource auto = r) { + // auto.flush(); + // } + // } + // } + + void nullableElementWithCheck(@OwningCollection List resources) { + for (Resource r : resources) { + if (r != null) { + r.close(); + r.flush(); + } + } + } + + void nullableElementHelper(@OwningCollection List resources) { + for (Resource r : resources) { + if (r != null) { + doCloseFlush(r); + } + } + } + + @EnsuresCalledMethods( + value = "#1", + methods = {"close", "flush"}) + void doCloseFlush(Resource r) { + r.close(); + r.flush(); + } + + void indexForLoop(@OwningCollection List resources) { + for (int i = 0; i < resources.size(); i++) { + resources.get(i).close(); + resources.get(i).flush(); + } + } + + // :: error: unfulfilled.collection.obligations + void indexForLoopPartial(@OwningCollection List resources) { + for (int i = 0; i < resources.size(); i++) { + resources.get(i).close(); + // missing flush + } + } + + void indexForLoopList(@OwningCollection List resources) { + for (int i = 0; i < resources.size(); i++) { + Resource r = resources.get(i); + r.close(); + r.flush(); + } + } + + // :: error: illegal.type.annotation + void checkArgIsOCWO(@OwningCollectionWithoutObligation Iterable arg) {} +} diff --git a/checker/tests/resourceleak-collections/OwningCollectionFieldTest.java b/checker/tests/resourceleak-collections/OwningCollectionFieldTest.java new file mode 100644 index 00000000000..a18fb2084b8 --- /dev/null +++ b/checker/tests/resourceleak-collections/OwningCollectionFieldTest.java @@ -0,0 +1,142 @@ +import java.io.Closeable; +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.collectionownership.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +@InheritableMustCall({"flush", "close"}) +class Resource implements AutoCloseable { + @Override + public void close() {} + + void flush() {} +} + +// 2. check that Aggregator has MustCall method +class Aggregator implements Closeable { + // 1. infer this field as @OwningCollection + List resList = new ArrayList<>(); + + public Aggregator() {} + + public Aggregator(@OwningCollection List list) { + resList = list; + } + + // 5. demand methods adding elements to have @CreatesMustCallFor("this") + @CreatesMustCallFor("this") + void add(@Owning Resource r) { + resList.add(r); + } + + // 3. check that mustcall method has a @CollectionFieldDestructor annotation + // 4. check that field has @OCwO as postcondition + @Override + @CollectionFieldDestructor("resList") + public void close() { + for (Resource r : resList) { + r.close(); + r.flush(); + } + } + + // :: error: missing.creates.mustcall.for + void addIllegal(Resource r) { + resList.add(r); + } + + @CollectionFieldDestructor("resList") + // :: error: contracts.postcondition + public void partialClose() { + for (Resource r : resList) { + r.flush(); + } + } +} + +// has no @MustCall method +class IllegalAggregator { + // :: error: unfulfilled.field.obligations + List resList = new ArrayList<>(); + + @CollectionFieldDestructor("resList") + public void close() { + for (Resource r : resList) { + r.close(); + r.flush(); + } + } +} + +public class OwningCollectionFieldTest { + void addToAggregator(Resource @OwningCollection [] resources) { + Aggregator agg = new Aggregator(); + for (Resource r : resources) { + agg.add(r); + } + agg.close(); + + // this is not necessary, but the checker would issue a false positive + // without this closing loop. + for (Resource r : resources) { + r.close(); + r.flush(); + } + } + + // Mainly test that accessing the owning resource collection field of another class is + // forbidden. + // since an obligaton for the field agg.resList is created, a @CreatesMustCallFor("agg") + // annotation is expected, which is nonsensical (why the assignment of this field itself + // is forbidden). + // :: error: missing.creates.mustcall.for + void accessOwningFieldAfterClosing(Resource @OwningCollection [] resources) { + Aggregator agg = new Aggregator(); + for (Resource r : resources) { + agg.add(r); + } + agg.close(); + // :: error: foreign.owningcollection.field.access + agg.resList.add(new Resource()); + + // this is not necessary, but the checker would issue a false positive + // without this closing loop. + for (Resource r : resources) { + r.close(); + r.flush(); + } + } + + void failToDestructAggregator(Resource @OwningCollection [] resources) { + // :: error: required.method.not.called + Aggregator agg = new Aggregator(); + for (Resource r : resources) { + agg.add(r); + } + + // this is not necessary, but the checker would issue a false positive + // without this closing loop. + for (Resource r : resources) { + r.close(); + r.flush(); + } + } + + void addAfterDestructing(Resource @OwningCollection [] resources) { + // :: error: required.method.not.called + Aggregator agg = new Aggregator(); + for (Resource r : resources) { + agg.add(r); + } + agg.close(); + agg.add(new Resource()); + + // this is not necessary, but the checker would issue a false positive + // without this closing loop. + for (Resource r : resources) { + r.close(); + r.flush(); + } + } +} diff --git a/checker/tests/resourceleak-collections/OwningCollectionFieldTyping.java b/checker/tests/resourceleak-collections/OwningCollectionFieldTyping.java new file mode 100644 index 00000000000..6629b0f1809 --- /dev/null +++ b/checker/tests/resourceleak-collections/OwningCollectionFieldTyping.java @@ -0,0 +1,201 @@ +import java.io.Closeable; +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.collectionownership.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class ConstructorTakesOwnership implements Closeable { + List resList = new ArrayList<>(); + @NotOwningCollection List notOwningField = new ArrayList<>(); + + public ConstructorTakesOwnership(@OwningCollection List list) { + resList = list; + } + + // :: error: unfulfilled.collection.obligations + public ConstructorTakesOwnership(@OwningCollection List list, int a) { + if (a > 5) { + // this doesn't remove the obligation of list + notOwningField = list; + } + } + + public ConstructorTakesOwnership(@OwningCollection List list, float a) { + resList = list; + if (a > 5) { + // illegal reassignment + // :: error: unfulfilled.collection.obligations + resList = new ArrayList<>(); + } + } + + // assignment to @NotOwningCollection field is legal, but + // here the obligation is not fulfilled after reassigning. + public void reassignNotOwningCollectionFieldLegal() { + // :: error: unfulfilled.collection.obligations + notOwningField = getList(); + } + + List getList() { + return new ArrayList(); + } + + // no justification for reassignment. Not allowed. + public void reassignCollectionFieldIllegal() { + // :: error: unfulfilled.collection.obligations + resList = new ArrayList<>(); + } + + // allowed since resList has @OwningCollectionWithoutObligation at reassignment time. + // No CreatesMustCallFor("this") required, since the rhs is @OwningCollectionWithoutObligation. + public void reassignCollectionFieldLegal() { + for (Resource r : resList) { + r.close(); + r.flush(); + } + resList = new ArrayList<>(); + } + + // assignment allowed since resList has @OwningCollectionWithoutObligation at reassignment time, + // but method + // is missing an @CreatesMustCallFor("this") + // :: error: missing.creates.mustcall.for + public void reassignCollectionFieldMissingCMCF() { + for (Resource r : resList) { + r.close(); + r.flush(); + } + List newList = new ArrayList<>(); + newList.add(new Resource()); + resList = newList; + } + + // allowed since resList has @OwningCollectionWithoutObligation at reassignment time + public void reassignCollectionFieldAfterDestructor() { + close(); + resList = new ArrayList<>(); + } + + // TODO SCK: uncomment this test + // // allowed since assignment cannot overwrite anything + // public void reassignCollectionFieldIfNull() { + // if (resList != null) { + // resList = new ArrayList<>(); + // } + // } + + // assignment allowed since field not owned by class. + // treated as normal variable. + public void reassignCollectionNotOwningField() { + notOwningField = new ArrayList<>(); + // :: error: unfulfilled.collection.obligations + notOwningField.add(new Resource()); + } + + @CollectionFieldDestructor("resList") + @Override + public void close() { + for (Resource r : resList) { + r.close(); + r.flush(); + } + } +} + +class OwningCollectionFieldTyping { + // :: error: unfulfilled.field.obligations + List ocField = new ArrayList<>(); + + void tryTransferringFieldOwnershipAssignment() { + // try to steal ownership + List ownershipStealer = ocField; + // :: error: method.invocation + ownershipStealer.add(new Resource()); + } + + void tryTransferringFieldOwnershipArgumentPassing() { + // try to give away ownership of field to parameter + // :: error: transfer.owningcollection.field.ownership + takeArgumentOwnership(ocField); + } + + void takeArgumentOwnership(@OwningCollection List param) { + // do scary things like adding new elements with calling obligations, or pass + // it on into a class that stores it as an owning field. + param.add(new Resource()); + Aggregator agg = new Aggregator(param); + agg.close(); + } + + List tryTransferringFieldOwnershipReturn() { + // :: error: transfer.owningcollection.field.ownership + return ocField; + } +} + +class OwningFieldWithIllegalInitializer implements Closeable { + // :: error: illegal.owningcollection.field.assignment + List fieldList = getList(); + + List getList() { + return new ArrayList(); + } + + @CollectionFieldDestructor("fieldList") + @Override + public void close() { + for (Resource r : fieldList) { + r.close(); + r.flush(); + } + } +} + +// here, the assignment to an @OwningCollection rhs is allowed +class OwningFinalFieldWithOwningRHSInitializer implements Closeable { + final List fieldList = getList(); + + List getList() { + return new ArrayList(); + } + + @CollectionFieldDestructor("fieldList") + @Override + public void close() { + for (Resource r : fieldList) { + r.close(); + r.flush(); + } + } +} + +class OwningFieldWithNullInitializer implements Closeable { + List fieldList = null; + + @CollectionFieldDestructor("fieldList") + @Override + public void close() { + for (Resource r : fieldList) { + r.close(); + r.flush(); + } + } +} + +class OwningFinalField implements Closeable { + final List fieldList; + + public OwningFinalField(@OwningCollection List list) { + this.fieldList = list; + } + + @CollectionFieldDestructor("fieldList") + @Override + public void close() { + for (Resource r : fieldList) { + r.close(); + r.flush(); + } + } +} diff --git a/checker/tests/resourceleak/EnhancedFor.java b/checker/tests/resourceleak/EnhancedFor.java index 2f2afcac14b..a244a926207 100644 --- a/checker/tests/resourceleak/EnhancedFor.java +++ b/checker/tests/resourceleak/EnhancedFor.java @@ -25,15 +25,9 @@ void test2(List<@MustCall Socket> list) { } } - // :: error: type.argument void test3(List list) { - // This error is issued because `s` is a local variable, and - // the foreach loop under the hood assigns the result of a call - // to Iterator#next into it (which is owning by default, because it's - // a method return type). Both this error and the type.argument error - // above can be suppressed by writing @MustCall on the Socket type, as in - // test4 below (but note that this will make call sites difficult to verify). - // :: error: (required.method.not.called) + // Iterator#next returns @NotOwning: iterators do not own their elements; ownership + // stays with the host collection associated with the iterator. for (Socket s : list) {} } diff --git a/checker/tests/resourceleak/IndexMode.java b/checker/tests/resourceleak/IndexMode.java index b41a251310d..abd9f093721 100644 --- a/checker/tests/resourceleak/IndexMode.java +++ b/checker/tests/resourceleak/IndexMode.java @@ -38,9 +38,9 @@ public static Object getMode2(Map indexOpt // This copy of getMode() adds an explicit `@MustCall` annotation to the String and to // the local variable. This version currently works as expected, unlike getMode2(). + // Since Map#get returns @NotOwning, this reports no error. public static Object getMode2a(Map indexOptions) { try { - // :: error: required.method.not.called @MustCall("hashCode") String literalOption = indexOptions.get("is_literal"); } catch (Exception e) { } @@ -51,7 +51,7 @@ public static Object getMode2a(Map indexOp // This copy of getMode() adds an explicit `@MustCall` annotation to the String and removes // the try-catch. public static Object getMode3(Map indexOptions) { - // :: error: required.method.not.called + // Since Map#get returns @NotOwning, this reports no error. String literalOption = indexOptions.get("is_literal"); return null; } @@ -59,7 +59,7 @@ public static Object getMode3(Map indexOpt // This copy of getMode() adds an explicit `@MustCall` annotation to the String, removes // the try-catch, and makes the return type void. public static void getMode4(Map indexOptions) { - // :: error: required.method.not.called + // Since Map#get returns @NotOwning, this reports no error. String literalOption = indexOptions.get("is_literal"); } @@ -69,11 +69,10 @@ public static void getMode5(Map indexOptions) { } // This variant uses an InputStream (which has a MustCall type by default) as the - // value type in the map. - // :: error: type.argument + // value type in the map. The values are permitted to have any @MustCall type. public static Object getModeIS(Map indexOptions) { try { - // :: error: required.method.not.called + // Since Map#get returns @NotOwning, this reports no error. InputStream literalOption = indexOptions.get("is_literal"); } catch (Exception e) { } diff --git a/checker/tests/resourceleak/Issue4815.java b/checker/tests/resourceleak/Issue4815.java index ec9178ad1e5..7032dbc2bcd 100644 --- a/checker/tests/resourceleak/Issue4815.java +++ b/checker/tests/resourceleak/Issue4815.java @@ -8,6 +8,12 @@ public class Issue4815 { public void initialize( List list, @Owning @MustCall("initialize") T object) { object.initialize(); + // `list` resolves to List<@MustCall Component> and thus cannot accept + // an element of non-empty @MustCall type enforced by the Java + // type checker. This is an unfortunate consequence of the otherwise + // elegant extension of the RLC to collections, which doesn't detect + // that object already fulfilled its obligation here. + // :: error: argument list.add(object); } diff --git a/checker/tests/resourceleak/Issue6030.java b/checker/tests/resourceleak/Issue6030.java index abb621a5cfd..f300b03b8af 100644 --- a/checker/tests/resourceleak/Issue6030.java +++ b/checker/tests/resourceleak/Issue6030.java @@ -1,6 +1,8 @@ // Test case for https://github.com/typetools/checker-framework/issues/6030 import java.util.*; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; +import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; public class Issue6030 { @@ -11,16 +13,19 @@ static class MyScanner> implements CloseableIterato @Owning I iterator; // :: error: missing.creates.mustcall.for - public boolean hasNext() { + public boolean hasNext(@NotOwningCollection MyScanner this) { if (iterator == null) iterator = createIterator(); return iterator.hasNext(); } - public T next() { + // The @NotOwning annotation is required to be consistent with the superclass implementation. + // The return type of Iterator#next is @NotOwning. Soundness is ensured by the RLC for + // collections. + public @NotOwning T next(@NotOwningCollection MyScanner this) { return null; } - private I createIterator() { + private I createIterator(@NotOwningCollection MyScanner this) { return null; } diff --git a/checker/tests/resourceleak/SocketIntoList.java b/checker/tests/resourceleak/SocketIntoList.java index d95c7a33c63..971f98cb7d2 100644 --- a/checker/tests/resourceleak/SocketIntoList.java +++ b/checker/tests/resourceleak/SocketIntoList.java @@ -4,6 +4,7 @@ import java.net.*; import java.util.List; +import org.checkerframework.checker.collectionownership.qual.OwningCollection; import org.checkerframework.checker.mustcall.qual.*; public class SocketIntoList { @@ -13,26 +14,31 @@ public void test1(List<@MustCall({}) Socket> l) { l.add(s); } - // :: error: type.argument - public void test2(List l) { + public List test2(@OwningCollection List l) { // s is unconnected, so no error is expected when it's stored into the list. - // But, if the list is unannotated, we do get an error at its declaration site - // (as expected, due to #5912). + // However, l would be allowed to store even connected sockets. Socket s = new Socket(); l.add(s); + return l; } public void test3(List<@MustCall({}) Socket> l) throws Exception { - // :: error: required.method.not.called + // Although s is illegally added to l, a required.method.not.called error + // is not additionally reported at this declaration site. List#add(@Owning E) takes on + // the obligation of its argument. Socket s = new Socket(); s.bind(new InetSocketAddress("192.168.0.1", 0)); + // l cannot hold elements with non-empty @MustCall values + // :: error: argument l.add(s); } // This input list might have been produced by e.g., test1() public void test4(List<@MustCall({}) Socket> l) throws Exception { - // :: error: required.method.not.called + // l.get(0) is not an error as List#get returns @NotOwning. However, s.bind tries + // to reset the MustCall obligations of s, which is only permitted if s is owning. Socket s = l.get(0); + // :: error: reset.not.owning s.bind(new InetSocketAddress("192.168.0.1", 0)); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index cd6b23943ea..9c06c6289cc 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -911,7 +911,7 @@ protected void addLabelForNextNode(Label l) { /* --------------------------------------------------------- */ /** The UID for the next unique name. */ - protected long uid = 0; + protected static long uid = 0; /** * Returns a unique name starting with {@code prefix}. diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/TryFinallyScopeMap.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/TryFinallyScopeMap.java index d640a9d6b6a..af7f930b824 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/TryFinallyScopeMap.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/TryFinallyScopeMap.java @@ -3,6 +3,7 @@ import java.util.HashMap; import java.util.Map; import javax.lang.model.element.Name; +import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.nullness.qual.Nullable; import org.plumelib.util.ArrayMap; @@ -22,7 +23,7 @@ protected TryFinallyScopeMap() { } @Override - public Label get(@Nullable Object key) { + public @NotOwning Label get(@Nullable Object key) { if (key == null) { throw new IllegalArgumentException(); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizer.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizer.java index 116fa08f39b..4130e06170b 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizer.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizer.java @@ -14,6 +14,7 @@ import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.expression.MethodCall; @@ -102,6 +103,16 @@ public interface CFGVisualizer< */ String visualizeStoreLocalVar(LocalVariable localVar, V value); + /** + * Called by {@code CFAbstractStore#internalVisualize()} to visualize an iterated collection + * element. + * + * @param ice the iterated collection element + * @param value the value associated with {@code ice} + * @return the String representation of this entry + */ + String visualizeStoreIteratedCollectionElt(IteratedCollectionElement ice, V value); + /** * Called by {@code CFAbstractStore#internalVisualize()} to visualize the value of the current * object {@code this} in this Store. diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/DOTCFGVisualizer.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/DOTCFGVisualizer.java index ff526cb125c..7c7ad55c7e8 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/DOTCFGVisualizer.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/DOTCFGVisualizer.java @@ -37,6 +37,7 @@ import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.expression.MethodCall; import org.checkerframework.javacutil.BugInCF; @@ -297,6 +298,11 @@ public String visualizeStoreLocalVar(LocalVariable localVar, V value) { return storeEntryIndent + localVar + " > " + escapeString(value); } + @Override + public String visualizeStoreIteratedCollectionElt(IteratedCollectionElement ice, V value) { + return storeEntryIndent + ice + " > " + escapeString(value); + } + @Override public String visualizeStoreFieldVal(FieldAccess fieldAccess, V value) { return storeEntryIndent + fieldAccess + " > " + escapeString(value); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/StringCFGVisualizer.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/StringCFGVisualizer.java index 4cef0a8e26a..c9ea4a5d05a 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/StringCFGVisualizer.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/StringCFGVisualizer.java @@ -21,6 +21,7 @@ import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.expression.MethodCall; @@ -135,6 +136,11 @@ public String visualizeStoreLocalVar(LocalVariable localVar, V value) { return storeEntryIndent + localVar + " > " + value; } + @Override + public String visualizeStoreIteratedCollectionElt(IteratedCollectionElement ice, V value) { + return storeEntryIndent + ice + " > " + value; + } + @Override public String visualizeStoreFieldVal(FieldAccess fieldAccess, V value) { return storeEntryIndent + fieldAccess + " > " + value; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/IteratedCollectionElement.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/IteratedCollectionElement.java new file mode 100644 index 00000000000..7e88b6139cf --- /dev/null +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/IteratedCollectionElement.java @@ -0,0 +1,88 @@ +package org.checkerframework.dataflow.expression; + +import com.sun.source.tree.Tree; +import java.util.Objects; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.javacutil.AnnotationProvider; + +/** + * Represents a collection element that is iterated over in a potentially + * collection-obligation-fulfilling loop, for example {@code o} in {@code for (Object o: list) { }}. + */ +public class IteratedCollectionElement extends JavaExpression { + /** The CFG node for this collection element. */ + public final Node node; + + /** The AST node for this collection element. */ + public final Tree tree; + + /** + * Creates a new IteratedCollectionElement. + * + * @param node CFG node + * @param tree an AST tree + */ + public IteratedCollectionElement(Node node, Tree tree) { + super(node.getType()); + this.node = node; + this.tree = tree; + } + + @Override + public boolean equals(@Nullable Object obj) { + if (this == obj) { + return true; + } + if (!(obj instanceof IteratedCollectionElement)) { + return false; + } + IteratedCollectionElement other = (IteratedCollectionElement) obj; + return this.tree.equals(other.tree) && this.node.equals(other.node); + } + + @Override + public int hashCode() { + return Objects.hash(tree, node); + } + + @SuppressWarnings("unchecked") // generic cast + @Override + public @Nullable T containedOfClass(Class clazz) { + return getClass() == clazz ? (T) this : null; + } + + @Override + public boolean isDeterministic(AnnotationProvider provider) { + return true; + } + + @Override + public boolean syntacticEquals(JavaExpression je) { + if (!(je instanceof IteratedCollectionElement)) { + return false; + } + IteratedCollectionElement other = (IteratedCollectionElement) je; + return this.equals(other); + } + + @Override + public boolean containsSyntacticEqualJavaExpression(JavaExpression other) { + return syntacticEquals(other); + } + + @Override + public boolean isAssignableByOtherCode() { + return false; + } + + @Override + public boolean isModifiableByOtherCode() { + return false; + } + + @Override + public R accept(JavaExpressionVisitor visitor, P p) { + return visitor.visitIteratedCollectionElement(this, p); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java index 78066c11225..e6a010c0e6f 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java @@ -89,6 +89,12 @@ protected JavaExpression visitLocalVariable(LocalVariable localVarExpr, Void unu return localVarExpr; } + @Override + protected JavaExpression visitIteratedCollectionElement( + IteratedCollectionElement iteratedCollectionElt, Void unused) { + return iteratedCollectionElt; + } + @Override protected JavaExpression visitMethodCall(MethodCall methodCallExpr, Void unused) { JavaExpression receiver = convert(methodCallExpr.getReceiver()); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java index 79c9eb0f158..1b9fb9abe6c 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java @@ -76,6 +76,12 @@ protected Void visitLocalVariable(LocalVariable localVarExpr, P p) { return null; } + @Override + protected Void visitIteratedCollectionElement( + IteratedCollectionElement iteratedCollectionElement, P p) { + return null; + } + @Override protected Void visitMethodCall(MethodCall methodCallExpr, P p) { visit(methodCallExpr.getReceiver(), p); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java index 2fa169f8bc8..b798371aeb1 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java @@ -82,6 +82,16 @@ public R visit(JavaExpression javaExpr, P p) { */ protected abstract R visitLocalVariable(LocalVariable localVarExpr, P p); + /** + * Visit a {@link IteratedCollectionElement}. + * + * @param iteratedCollectionElt the JavaExpression to visit + * @param p the parameter to pass to the visit method + * @return the result of visiting the {@code localVarExpr} + */ + protected abstract R visitIteratedCollectionElement( + IteratedCollectionElement iteratedCollectionElt, P p); + /** * Visit a {@link MethodCall}. * diff --git a/docs/manual/resource-leak-checker.tex b/docs/manual/resource-leak-checker.tex index b6cc177b9ef..dbcdaf09998 100644 --- a/docs/manual/resource-leak-checker.tex +++ b/docs/manual/resource-leak-checker.tex @@ -135,6 +135,28 @@ \end{description} +\subsectionAndLabel{Resource Leak Checker annotations for collections}{resource-leak-annotations-collections} + +The Resource Leak Checker also supports collections of resources. The following annotations express ownership over resource collections. + +\begin{description} +\item[\refqualclass{checker/collectionownership/qual}{OwningCollection}] +\item[\refqualclass{checker/collectionownership/qual}{NotOwningCollection}] + expresses ownership over resource collections. Resource collection formal parameters default to \texttt{@NotOwningCollection}, while resource collection fields and return types default to \texttt{@OwningCollection}. + For more details, see Section~\ref{resource-leak-collections}. + +\end{description} + +This annotation is for dedicated destructor methods of resource collection fields. + +\begin{description} +\item[\refqualclasswithparams{checker/collectionownership/qual}{CollectionFieldDestructor}{String[] value}] + expresses that the annotated method fulfills the obligations of the given resource collection fields. + For more details, see Section~\ref{resource-leak-collections-fields}. + +\end{description} + + \sectionAndLabel{Example of how safe resource usage is verified}{resource-leak-example} Consider the following example of safe use of a \, in which the comments indicate the @@ -620,46 +642,362 @@ \sectionAndLabel{Collections of resources}{resource-leak-collections} -The Resource Leak Checker cannot verify code that stores a collection of -resources in a generic collection (e.g., \) and then -resolves the obligations of each element of the collection at once (e.g., -by iterating over the \). In the future, the checker will support -this. The remainder of this section explains the implementation issues; -most users can skip it. - -The first implementation issue is that \<@Owning> and \<@NotOwning> are -declaration annotations rather than type qualifiers, so they cannot be -written on type arguments. It is possible under the current design to have -an \code{@Owning List}, but not a \code{List<@Owning Socket>}. -It would be better to make \<@Owning> a type annotation, but this is a -challenging design problem. - -The second implementation issue is the defaulting rule for \<@MustCall> on -type variable upper bounds. Currently, this default is \<@MustCall(\{\})>, -which prevents many false positives in code with type variables that makes -no use of resources --- an important design principle. -However, this defaulting rule does have an unfortunate consequence: it is -an error to write \code{List} or any other type with a concrete -type argument where the type argument itself isn't \<@MustCall(\{\})>. A programmer who -needs to write such a type while using the Resource Leak Checker has a few -choices, all of which have some downsides: +The Resource Leak Checker handles homogeneous collections of resources. In a homogeneous collection, every element +has exactly the same must-call and called-methods properties. Instances of \texttt{java.util.Iterable} are supported; +this section calls those ``collections''. +% Usage of \texttt{java.util.Iterator}s over \texttt{java.util.Iterable}s are also supported, but they are not considered collections. + +What the checker effectively verifies is that any resource collection is properly disposed of. That is, there is some loop that definitely calls the required methods on all elements of the collection. + +Towards that end, the Resource Leak Checker tracks every allocated resource collection in two ways: + +\begin{itemize} + \item at most one owning reference for each underlying resource collection is tracked via an ownership type system. This owning reference may arbitrarily mutate the collection. All other references are considered not owning and are restricted - for example, they can't be used to add or remove elements to and from the collection, respectively. + \item a complementary dataflow analysis tracks an obligation for each allocated resource collection. The obligation can be passed on to method parameters, fields, or return values for example, just like the ownership. The difference is that while the type system tracks at most one owner per resource collection allowed to mutate it without restriction, the dataflow analysis tracks at least one obligation per resource collection to ensure it is definitely fulfilled. +\end{itemize} + +For the purposes of this checker, \textit{resource collections} are precisely defined, as the objects of interest for both the type system and obligation tracking. A Java expression is a \textit{resource collection} if it is: + +\begin{enumerate} + \item A \texttt{java.util.Iterable} or implementation thereof (which includes the entire Java Collections framework), and:%, or a \texttt{java.util.Iterator} + \item Its type parameter upper bound has non-empty \texttt{MustCall} type. +\end{enumerate} + +For example, expressions of type \texttt{List} or \texttt{Iterable} are both resource collections, but one of type \texttt{Set} is not. + +\subsectionAndLabel{Ownership type system for resource collections}{resource-leak-collections-ownership-types} +Of the two tracking mechanisms described above, the ownership type system is more visible from the user perspective. The type hierarchy is the following: + +\begin{verbatim} + @NotOwningCollection + | + @OwningCollection + | + @OwningCollectionWithoutObligation + | + @OwningCollectionBottom +\end{verbatim} + +\begin{itemize} + \item \textbf{@NotOwningCollection} is the type of resource collection references that might not own the underlying resource collection. + \item \textbf{@OwningCollection} is the type of resource collection references that definitely own the underlying collection, but might have open calling obligations for their elements. + \item \textbf{@OwningCollectionWithoutObligation} is the type of \textit{resource collection} references that definitely own the underlying collection, but also definitely don't have any open calling obligations on their elements. For example, a freshly allocated resource collection that doesn't yet contain any resources is of this type. + \item \textbf{@OwningCollectionBottom} is the type of non-\textit{resource collections}. It is thus the type the vast majority of expressions have, because most expressions are not collections of resources. +\end{itemize} + +Only \texttt{@OwningCollection} and \texttt{@NotOwningCollection} are permitted as user-written annotations. The other types are only used internally. + +\subsectionAndLabel{Ownership types in action: defaults and ownership transfer}{resource-leak-collections-types-in-action} + +A freshly allocated resource collection always defaults to \texttt{@OwningCollectionWithoutObligation}. + +\begin{Verbatim} +List sockets = new ArrayList<>(); +// `sockets` is now @OwningCollectionWithoutObligation +\end{Verbatim} + +When you now add elements into this collection, its type unrefines to \texttt{@OwningCollection}. + +\begin{Verbatim} +List sockets = new ArrayList<>(); +// `sockets` is @OwningCollectionWithoutObligation +for (int i = 0; i < n; i++) { + sockets.add(new Socket(myHost, myPort + i)); + // `sockets` is @OwningCollection +} +// `sockets` is @OwningCollection +\end{Verbatim} + +All methods called on a resource collection that potentially move an element with a calling obligation into the collection change the type of the receiving collection to \texttt{@OwningCollection} and create a tracked obligation for the collection in the dataflow analysis. + +For method parameters, the default type of resource collection references is \texttt{@NotOwningCollection}. + +\begin{Verbatim} +void m(Iterable sockets) { + // `sockets` is @NotOwningCollection + ... +} +\end{Verbatim} + +This means that by default, a resource collection parameter can only do certain 'safe' operations on the collection that do not add, remove, or overwrite existing elements. But it also means that the parameter does not have any calling obligation for the elements of the collection, and it can accept both owning and not owning collection references due to normal subtyping rules. If an \texttt{OwningCollection} reference is passed to an unannotated parameter, the obligation stays at the call-site. + +Annotating the parameter with \texttt{@OwningCollection} overrides this behavior. In this case, the ownership is transferred from the call-site argument to the method parameter. Concretely, this means that the call-site obligation is removed and the parameter takes on the responsibility of disposing of the collection. The type of the argument at the call-site is changed to \texttt{@NotOwningCollection} to maintain the invariant that there's at most one owning reference for each resource collection. + +\begin{Verbatim} +void m(@OwningCollection Iterable sockets) { + // `sockets` is @OwningCollection + ... + // this loop disposes of the collection and fulfills the obligation + for (Socket s : sockets) { + try { + s.close(); + } catch (Exception e) { + System.out.println(e.stackTrace()); + } + } + // `sockets` is @OwningCollectionWithoutObligation again +} +\end{Verbatim} + +Resource collection return types default to \texttt{@OwningCollection}. Returning a resource collection from a method with that return type fulfills the collection's obligation. The obligation and ownership are both transferred to the method invocation expression at the call-site. + +\begin{verbatim} +List returnSocketList() { + List socketList = new ArrayList<>(); + // `socketList` is @OwningCollectionWithoutObligation + socketList.add(new Socket(myHost, myPort)); + // `socketList` is @OwningCollection + return socketList; + // the return transfers obligation and ownership to the call-site +} +\end{verbatim} + +Writing \texttt{@NotOwningCollection} on the return type overrides this default. In this case, ownership and obligation are not transferred to the call-site and the obligation must be fulfilled or passed on prior to the return. + +Ownership is also transferred through assignments. If the right-hand side of an assignment is of type \texttt{@OwningCollection} or \texttt{@OwningCollectionWithoutObligation}, the ownership is transferred to the left-hand side expression, and thus the right-hand side is unrefined to \texttt{@NotOwningCollection} to maintain the invariant of having at most one owning reference per resource collection. + +\begin{verbatim} +// `r` is @OwningCollection +l = r; +// `l` is now @OwningCollection, `r` is @NotOwningCollection +\end{verbatim} + +Just like the ownership, the obligation is also transferred to the left-hand side. + +\subsectionAndLabel{Fulfilling collection obligations}{resource-leak-collections-fulfillment} + +To fulfill the obligation of a resource collection, the obligation can be passed on, but at some point it has to be fulfilled by calling the required methods on its elements. Recommended are enhanced \texttt{for} loops, but indexed \texttt{for} loops are also supported with some syntactic restrictions. + +Here is an example of such a loop: + +\begin{verbatim} +// `socketList` is @OwningCollection and has an obligation for calling `close` on its elements +for (Socket s : socketList) { + try { + s.close(); + } catch (Exception e) { + e.printStackTrace(); + } +} +// `socketList` is @OwningCollectionWithoutObligation and has no obligation +\end{verbatim} + +The main effect such a loop has is that the obligations corresponding to the methods it calls on all elements are removed. If the loop calls all required methods - which is almost always the case, since classes usually have at most one \texttt{MustCall} method - the type of the collection is additionally refined to \texttt{@OwningCollectionWithoutObligation}. + +To determine the methods such a loop calls, the checker does the following things: + +\begin{itemize} + \item It checks that the loop does not terminate early. + \item It leverages the \texttt{CalledMethods} analysis to determine the methods definitely called on the loop iterator variable. This means that anything that changes the \texttt{CalledMethods} type of the iterator variable is supported, for example passing it as an argument to a method annotated \texttt{@EnsuresCalledMethods(``m'')}, or using try-with constructs. Nullness checks are also supported: that is, it is sufficient to fulfill the obligation for every non-null element of the collection; note that this is a simple, syntactic check, not a full-fledged nullness analysis, and so it might fail to certify loops that use an unorthodox method for nullness checking. +\end{itemize} + +If an indexed \texttt{for} loop is used, the checker must additionally check that the loop does in fact iterate over all elements of the collection, and that the loop doesn't write to the loop variable for example. The checks are the following: + +\begin{itemize} + \item Loop iteration bounds: + \begin{itemize} + \item The lower bound of iteration is 0, and + \item The upper bound of iteration is \texttt{c.size()} + \item The loop's increment expression is a pre- or post-increment of the loop variable. + \item The collection element is accessed using \texttt{collection.get(i)}, where \texttt{i} is the loop variable. + \end{itemize} + \item The loop does not assign to the collection variable. + \item The loop does not assign to collection elements. +\end{itemize} + +Here is an example using an indexed \texttt{for} loop. + +\begin{verbatim} +for (int i = 0; i < socketList.size(); i++) { + try { + socketList.get(i).close(); + } catch (Exception e) {} +} +\end{verbatim} + +\subsectionAndLabel{Resource collection fields}{resource-leak-collections-fields} +By default, resource collection fields are owned by the enclosing class. Static fields are not supported and an error is reported for a declaration of a static resource collection field. +Consider the following example: + +\begin{verbatim} +class Aggregator implements Closeable { + List socketList = new ArrayList<>(); + + public Aggregator() {} + + public Aggregator(@OwningCollection List l) { + // `this.socketList` is @OwningCollectionWithoutObligation + this.socketList = l; + // `this.socketList` is @OwningCollection + // the obligation of `l` has been resolved + } + + @CreatesMustCallFor("this") + public void add(@Owning Socket s) { + // this call creates an obligation for the field. + // thus, the enclosing method must have a @CreatesMustCallFor("this") annotation. + socketList.add(s); + } + + @Override + @CollectionFieldDestructor("socketList") + public void close() { + for (Socket s : socketList) { + try { + s.close(); + } catch (Exception e) { + e.printStackTrace(); + } + } + } +} +\end{verbatim} + +To verify a resource collection field \textit{field}, the checker looks for the following: +\begin{enumerate} + \item A \texttt{@MustCall} annotation on the enclosing class. In this case, the class is of type \texttt{@MustCall(``close'')} by subclassing Closeable. + \item Among the methods in the \texttt{@MustCall} type of the enclosing class (usually there's just one), the checker now looks for the post-condition annotation \texttt{@CollectionFieldDestructor(``field'')}. + \item The annotation \texttt{@CollectionFieldDestructor(``field'')} asserts that at the method exit, \textit{field} has type \texttt{@OwningCollectionWithoutObligation}, which the checker verifies. + \item Methods that call 'unsafe' methods creating obligations for the resource collection field, such as \texttt{socketList.add(Socket)} in this case, must have a \texttt{@CreatesMustCallFor(``this'')} annotation. +\end{enumerate} + +This now shifts the burden to the client of the \texttt{Aggregator} class to call \texttt{close()} on instances before they leave scope. + +If a resource collection field is final, the checker doesn't have to verify assignments to it. If it is not final, the check verifies assignments in the following way: +\begin{itemize} + \item Assignments in initializer blocks are not permitted. + \item Assignments in a declaration initializer are permitted if the right-hand side is at most \texttt{@OwningCollectionWithoutObligation}. + \item Thanks to the above two restrictions, it can be assumed that an owned resource collection field is \texttt{@OwningCollectionWithoutObligation} at the beginning of a constructor. An assignment to the field is now allowed if the field is \texttt{@OwningCollectionWithoutObligation} just before the assignment. This condition holds in any other (non-constructor) method too, but the field is \texttt{@OwningCollection} at the method entrance, unlike for a constructor. A legal assignment to an owning resource collection field resolves the obligation of the right-hand side. +\end{itemize} + +Resource collection fields owned by the enclosing class are special cases for ownership transfer, as the checker doesn't allow transferring the ownership away from such a field. If for example a member method were able to transfer the ownership of the field to an external method parameter, the checker would have to track that the field is no longer the owner and set its type to \texttt{@NotOwningCollection} for future method invocations on the class instance. For the sake of simplicity, the checker doesn't track this and thus doesn't allow ownership transfers for fields. In particular: + +\begin{itemize} + \item The field cannot be passed as an argument to an \texttt{@OwningCollection} parameter. + \item The field cannot be returned to an \texttt{@OwningCollection} return type. + \item If the field is on the right-hand side of an assignment, the left-hand side has type \texttt{@NotOwningCollection} after the assignment, so as to keep the at-most-one-owner invariant. + \item Any access to the field from outside of the class (or a subclass) is not permitted. +\end{itemize} + +If the enclosing class is not intended to take responsibility for the resource collection field, annotate it with @NotOwningCollection. It now behaves just like any other resource collection reference. In particular: \begin{itemize} -\item Write \code{List}. This rejects calls to \ -or other methods that require an instance of the type variable, but it -preserves some of the behavior (e.g., calls to \ are permitted). -This is the best choice most of the time if the \ is not intended to -be owning. -\item Write \code{List<@MustCall Socket>}. This makes it an error to -add a Socket to the list, since the type of the Socket is -\<@MustCall("close")> but the list requires \<@MustCall()>. -\item Suppress one or more warnings. + \item Assigning to such a field does not resolve the obligation of the right-hand side. + \item The enclosing class does not have to fulfill any obligations on the field. \end{itemize} -The recommended way to use the Resource Leak Checker in this situation is -to rewrite the code to avoid a \ of owning resources. If rewriting is -not possible, the programmer will probably need to suppress a warning and -then verify the code using a method other than the Resource Leak Checker. +% \subsectionAndLabel{Iterators over resource collections}{resource-leak-collections-iterators} +% Iterators are frequently used to traverse collections. It is always safe to create an iterator for any non-resource collection. Since an iterator takes a snapshot of the collection at the time it is created, it does not matter what happens with the collection after the iterator is created (else, a \ is thrown for the next usage of the iterator). +% An iterator created for a resource collection has the same collection ownership type as the resource collection. + +% \begin{verbatim} +% // `socketList` is @OwningCollectionWithoutObligation +% Iterator socketIterator = socketList.iterator(); +% // `socketIterator` is @OwningCollectionWithoutObligation +% \end{verbatim} + +% The only concering operation an iterator can do is \texttt{remove()}, as the removed element might have open calling obligations. + +% Just like a \texttt{java.util.Collection} of type \texttt{@NotOwningCollection}, an iterator of this type is not allowed to call \texttt{remove()} at all. Iterators of type \texttt{@OwningCollectionBottom} and \texttt{@OwningCollectionWithoutObligation} can always call \texttt{remove()}. The interesting remaining case is that of an \texttt{@OwningCollection} iterator. +% Such an iterator and the values its calls to \texttt{next()} return are tracked with special obligations. This is to ensure that whenever an \texttt{@OwningCollection} iterator calls \texttt{close()}, the value returned by the previous call to \texttt{Iterator.next()} has its \texttt{MustCall} obligations fulfilled. + +% Here is an example of unsafe iterator usage: + +% \begin{verbatim} +% List foo(@OwningCollection List list) { +% Iterator iter = list.iterator(); +% // `iter` is @OwningCollection and must be tracked +% iter.next(); +% iter.remove(); // unsafe! +% return list; +% } +% \end{verbatim} + +% \begin{verbatim} +% error: [required.method.not.called] @MustCall method close may not have been invoked on iter.next() or any of its aliases. +% iter.next(); +% ^ +% \end{verbatim} + +% The removed element must have its must-call obligations fulfilled. Here is an example of safe usage: + +% \begin{verbatim} +% List foo(@OwningCollection List list) { +% Iterator iter = list.iterator(); +% // `iter` is @OwningCollection and must be tracked +% try { +% iter.next().close(); +% } catch (Exception e) { +% } +% iter.remove(); +% return list; +% } +% \end{verbatim} + +% The returned element may also be stored in a variable first and the fulfillment of the obligation of the returned element may also occur after the call to \texttt{remove()}: + +% \begin{verbatim} +% List foo(@OwningCollection List list) { +% Iterator iter = list.iterator(); +% // `iter` is @OwningCollection and must be tracked +% Socket s = iter.next(); +% iter.remove(); +% try { +% s.close(); +% } catch (Exception e) { +% } +% return list; +% } +% \end{verbatim} + +% The returned element by \texttt{iter.next()} may have its must-call obligation fulfilled in any way described by the resource leak checker, even by transferring its ownership (for example by storing it in a field or passing it as an \texttt{@OwningCollection} method argument). + +% Iterators over collections with obligations may also be returned, passed as method or constructor arguments and even be stored in fields. + +\subsectionAndLabel{JDK Method Signatures}{resource-leak-collections-jdk-methods} +[[TODO: Add a table with a number of collection/iterable methods and their collection ownership annotations]] + + +% The Resource Leak Checker cannot verify code that stores a collection of +% resources in a generic collection (e.g., \) and then +% resolves the obligations of each element of the collection at once (e.g., +% by iterating over the \). In the future, the checker will support +% this. The remainder of this section explains the implementation issues; +% most users can skip it. + +% The first implementation issue is that \<@Owning> and \<@NotOwning> are +% declaration annotations rather than type qualifiers, so they cannot be +% written on type arguments. It is possible under the current design to have +% an \code{@Owning List}, but not a \code{List<@Owning Socket>}. +% It would be better to make \<@Owning> a type annotation, but this is a +% challenging design problem. + +% The second implementation issue is the defaulting rule for \<@MustCall> on +% type variable upper bounds. Currently, this default is \<@MustCall(\{\})>, +% which prevents many false positives in code with type variables that makes +% no use of resources --- an important design principle. +% However, this defaulting rule does have an unfortunate consequence: it is +% an error to write \code{List} or any other type with a concrete +% type argument where the type argument itself isn't \<@MustCall(\{\})>. A programmer who +% needs to write such a type while using the Resource Leak Checker has a few +% choices, all of which have some downsides: + +% \begin{itemize} +% \item Write \code{List}. This rejects calls to \ +% or other methods that require an instance of the type variable, but it +% preserves some of the behavior (e.g., calls to \ are permitted). +% This is the best choice most of the time if the \ is not intended to +% be owning. +% \item Write \code{List<@MustCall Socket>}. This makes it an error to +% add a Socket to the list, since the type of the Socket is +% \<@MustCall("close")> but the list requires \<@MustCall()>. +% \item Suppress one or more warnings. +% \end{itemize} + +% The recommended way to use the Resource Leak Checker in this situation is +% to rewrite the code to avoid a \ of owning resources. If rewriting is +% not possible, the programmer will probably need to suppress a warning and +% then verify the code using a method other than the Resource Leak Checker. \sectionAndLabel{Further reading}{resource-leak-checker-references} diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java index cbf79c8d6f2..ef72856bedb 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java @@ -12,8 +12,10 @@ import java.util.NoSuchElementException; import javax.tools.JavaFileObject; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; import org.checkerframework.checker.index.qual.GTENegativeOne; import org.checkerframework.checker.initialization.qual.UnknownInitialization; +import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.nullness.qual.RequiresNonNull; @@ -233,7 +235,7 @@ public void remove() { } @Override - public TestDiagnosticLine next() { + public @NotOwning TestDiagnosticLine next() { if (nextLine == null) { throw new NoSuchElementException(); } @@ -260,8 +262,15 @@ public TestDiagnosticLine next() { return codec.createTestDiagnosticLine(filename, currentLine, currentLineNumber); } + /** + * Advances the reader by reading a single line, updating the {@code nextLine} and {@code + * NextLineNumber} fields. If there is no remaining line, the reader is {@code close}d. + * + * @throws IOException propagated reader exception + */ @RequiresNonNull("reader") - protected void advance(@UnknownInitialization JavaDiagnosticReader this) throws IOException { + protected void advance(@NotOwningCollection @UnknownInitialization JavaDiagnosticReader this) + throws IOException { nextLine = reader.readLine(); nextLineNumber = reader.getLineNumber(); if (nextLine == null) { diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java index 2612f19669f..f5940c3612a 100644 --- a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java @@ -102,7 +102,7 @@ public void accumulate( * returned true) * @param values a list of newly-accumulated values */ - private void updateValueAndInsertIntoStore( + protected void updateValueAndInsertIntoStore( AccumulationStore store, JavaExpression target, List values) { // Make a modifiable copy of the list. List valuesAsList = new ArrayList<>(values); diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueCheckerUtils.java b/framework/src/main/java/org/checkerframework/common/value/ValueCheckerUtils.java index bb7ccafde77..37471931dbb 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueCheckerUtils.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueCheckerUtils.java @@ -174,6 +174,7 @@ private static T convertLongToType(long value, Class expectedType) { * @param origValues the objects to format * @return a list of the formatted objects */ + @SuppressWarnings("collectionownership:argument") // defaulting/ownership CollectionsPlume.mapList private static @Nullable List convertToStringVal( List origValues) { if (origValues == null) { diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index f991098874d..6a8395ccd1f 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -1,5 +1,6 @@ package org.checkerframework.framework.flow; +import com.sun.source.tree.Tree; import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; @@ -30,6 +31,7 @@ import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; +import org.checkerframework.dataflow.expression.IteratedCollectionElement; import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.expression.MethodCall; @@ -73,6 +75,9 @@ public abstract class CFAbstractStore, S extends CF /** Information collected about local variables (including method parameters). */ protected final Map localVariableValues; + /** Information collected about iterated collection elements. */ + protected final Map iteratedCollectionElements; + /** Information collected about the current object. */ protected V thisValue; @@ -143,6 +148,7 @@ public long getUid() { protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { this.analysis = analysis; this.localVariableValues = new HashMap<>(); + this.iteratedCollectionElements = new HashMap<>(); this.thisValue = null; this.fieldValues = new HashMap<>(); this.methodCallExpressions = new HashMap<>(); @@ -163,6 +169,7 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti protected CFAbstractStore(CFAbstractStore other) { this.analysis = other.analysis; this.localVariableValues = new HashMap<>(other.localVariableValues); + this.iteratedCollectionElements = new HashMap<>(other.iteratedCollectionElements); this.thisValue = other.thisValue; this.fieldValues = new HashMap<>(other.fieldValues); this.methodCallExpressions = new HashMap<>(other.methodCallExpressions); @@ -503,6 +510,7 @@ public static boolean canInsertJavaExpression(JavaExpression expr) { || expr instanceof ThisReference || expr instanceof SuperReference || expr instanceof LocalVariable + || expr instanceof IteratedCollectionElement || expr instanceof MethodCall || expr instanceof ArrayAccess || expr instanceof ClassName) { @@ -637,6 +645,13 @@ protected void computeNewValueAndInsert( if (newValue != null) { localVariableValues.put(localVar, newValue); } + } else if (expr instanceof IteratedCollectionElement) { + IteratedCollectionElement collectionElt = (IteratedCollectionElement) expr; + V oldValue = iteratedCollectionElements.get(collectionElt); + V newValue = merger.apply(oldValue, value); + if (newValue != null) { + iteratedCollectionElements.put(collectionElt, newValue); + } } else if (expr instanceof FieldAccess) { FieldAccess fieldAcc = (FieldAccess) expr; // Only store information about final fields (where the receiver is @@ -767,6 +782,9 @@ public void clearValue(JavaExpression expr) { if (expr instanceof LocalVariable) { LocalVariable localVar = (LocalVariable) expr; localVariableValues.remove(localVar); + } else if (expr instanceof IteratedCollectionElement) { + IteratedCollectionElement collectionElt = (IteratedCollectionElement) expr; + iteratedCollectionElements.remove(collectionElt); } else if (expr instanceof FieldAccess) { FieldAccess fieldAcc = (FieldAccess) expr; fieldValues.remove(fieldAcc); @@ -786,6 +804,23 @@ public void clearValue(JavaExpression expr) { } } + /** + * Returns the {@link IteratedCollectionElement} associated with the given node or tree. + * + * @param node CFG node for which the associated {@link IteratedCollectionElement} is sought + * @param tree AST tree for which the associated {@link IteratedCollectionElement} is sought + * @return the {@link IteratedCollectionElement} associated with the given node or tree + */ + @SuppressWarnings("interning:not.interned") // we want to check reference equality + public @Nullable IteratedCollectionElement getIteratedCollectionElement(Node node, Tree tree) { + for (IteratedCollectionElement ice : iteratedCollectionElements.keySet()) { + if (ice.tree == tree || ice.node == node || ice.tree.equals(tree) || ice.node.equals(node)) { + return ice; + } + } + return null; + } + /** * Returns the current abstract value of a Java expression, or {@code null} if no information is * available. @@ -797,6 +832,9 @@ public void clearValue(JavaExpression expr) { if (expr instanceof LocalVariable) { LocalVariable localVar = (LocalVariable) expr; return localVariableValues.get(localVar); + } else if (expr instanceof IteratedCollectionElement) { + IteratedCollectionElement collectionElt = (IteratedCollectionElement) expr; + return iteratedCollectionElements.get(collectionElt); } else if (expr instanceof ThisReference || expr instanceof SuperReference) { return thisValue; } else if (expr instanceof FieldAccess) { @@ -1195,6 +1233,18 @@ private S upperBound(S other, boolean shouldWiden) { } } + for (Map.Entry e : other.iteratedCollectionElements.entrySet()) { + IteratedCollectionElement ice = e.getKey(); + V thisVal = iteratedCollectionElements.get(ice); + if (thisVal != null) { + V otherVal = e.getValue(); + V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden); + if (mergedVal != null) { + newStore.iteratedCollectionElements.put(ice, mergedVal); + } + } + } + // information about the current object { V otherVal = other.thisValue; @@ -1277,6 +1327,13 @@ protected boolean supersetOf(CFAbstractStore other) { return false; } } + for (Map.Entry e : other.iteratedCollectionElements.entrySet()) { + IteratedCollectionElement key = e.getKey(); + V value = iteratedCollectionElements.get(key); + if (value == null || !value.equals(e.getValue())) { + return false; + } + } if (!Objects.equals(thisValue, other.thisValue)) { return false; } @@ -1360,6 +1417,10 @@ protected String internalVisualize(CFGVisualizer viz) { for (LocalVariable lv : ToStringComparator.sorted(localVariableValues.keySet())) { res.add(viz.visualizeStoreLocalVar(lv, localVariableValues.get(lv))); } + for (IteratedCollectionElement ice : + ToStringComparator.sorted(iteratedCollectionElements.keySet())) { + res.add(viz.visualizeStoreIteratedCollectionElt(ice, iteratedCollectionElements.get(ice))); + } if (thisValue != null) { res.add(viz.visualizeStoreThisVal(thisValue)); } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 535b4fa1a24..496e5a174df 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1506,8 +1506,8 @@ public TransferResult visitExpressionStatement( * @param target the receiver whose value should be modified * @param newAnno the new value */ - protected static void insertIntoStores( - TransferResult result, JavaExpression target, AnnotationMirror newAnno) { + protected void insertIntoStores( + TransferResult result, JavaExpression target, AnnotationMirror newAnno) { if (result.containsTwoStores()) { result.getThenStore().insertValue(target, newAnno); result.getElseStore().insertValue(target, newAnno); diff --git a/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java b/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java index 6fe7ca077d0..098c311717e 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java @@ -391,6 +391,7 @@ private void indent() { * @param lst a list to format * @return a string representation of the list, without surrounding square brackets */ + @SuppressWarnings("collectionownership:argument") // defaulting/inference for StringsPlume.join private String formatList(@MustCallUnknown List lst) { return StringsPlume.join(", ", lst); } diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 8b38a8f7b30..b42848afa25 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -61,6 +61,7 @@ import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGStatement; +import org.checkerframework.dataflow.cfg.block.Block; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; @@ -1214,6 +1215,23 @@ public Store getStoreBefore(Set nodes) { return merge; } + /** + * Returns the regular store for a given block. + * + * @param block a block whose regular store to return + * @return the regular store of {@code block} + */ + public Store getRegularStore(Block block) { + TransferInput input; + if (!analysis.isRunning()) { + input = flowResult.getInput(block); + } else { + input = analysis.getInput(block); + } + + return input.getRegularStore(); + } + /** * Returns the store immediately before a given node. * diff --git a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java index 3dd6f7f744c..6a67d9629af 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java @@ -779,6 +779,7 @@ public static void assertSameSize(Collection c1, Collection c2) { * @param c2 the second collection * @param result the result collection */ + @SuppressWarnings("collectionownership:argument") // defaulting/inference for StringsPlume.join public static void assertSameSize( @MustCallUnknown Collection c1, @MustCallUnknown Collection c2, diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/util/Theta.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/util/Theta.java index 3ae9182408b..9eb08fb820a 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/util/Theta.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/util/Theta.java @@ -5,6 +5,8 @@ import java.util.LinkedHashMap; import java.util.List; import javax.lang.model.type.TypeVariable; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; +import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.framework.util.typeinference8.types.Variable; import org.checkerframework.javacutil.TypesUtils; @@ -25,7 +27,7 @@ public Theta() {} * @return the type variable in the key set that is {@link TypesUtils#areSame(TypeVariable, * TypeVariable)} as {@code typeVariable} */ - private TypeVariable getTypeVariable(TypeVariable typeVariable) { + private TypeVariable getTypeVariable(@NotOwningCollection Theta this, TypeVariable typeVariable) { for (TypeVariable key : keySet()) { if (TypesUtils.areSame(key, typeVariable)) { return key; @@ -43,7 +45,7 @@ public boolean containsKey(Object key) { } @Override - public Variable get(Object key) { + public @NotOwning Variable get(Object key) { if (key instanceof TypeVariable) { return super.get(getTypeVariable((TypeVariable) key)); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java index 33a44906898..88f58879729 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java @@ -7,6 +7,7 @@ import java.util.Set; import java.util.TreeMap; import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.nullness.qual.KeyFor; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.returnsreceiver.qual.This; @@ -112,7 +113,7 @@ public boolean containsValue(Object value) { @Override @Pure - public @Nullable V get(Object key) { + public @NotOwning @Nullable V get(Object key) { if (key instanceof AnnotationMirror) { AnnotationMirror keyAnno = AnnotationUtils.getSame(shadowMap.keySet(), (AnnotationMirror) key); @@ -129,7 +130,7 @@ public boolean containsValue(Object value) { "keyfor:argument" }) // delegation @Override - public @Nullable V put(AnnotationMirror key, V value) { + public @NotOwning @Nullable V put(AnnotationMirror key, V value) { V pre = get(key); remove(key); shadowMap.put(key, value); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java index cbe810a39e7..a334530895e 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java @@ -7,7 +7,10 @@ import java.util.NavigableSet; import java.util.TreeSet; import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.checker.collectionownership.qual.NotOwningCollection; +import org.checkerframework.checker.collectionownership.qual.PolyOwningCollection; import org.checkerframework.checker.initialization.qual.UnknownInitialization; +import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.nullness.qual.KeyFor; import org.checkerframework.checker.nullness.qual.KeyForBottom; import org.checkerframework.checker.nullness.qual.Nullable; @@ -142,7 +145,8 @@ public boolean contains( } @Override - public Iterator<@KeyFor("this") AnnotationMirror> iterator() { + public Iterator<@KeyFor("this") AnnotationMirror> iterator( + @PolyOwningCollection AnnotationMirrorSet this) { return shadowSet.iterator(); } @@ -157,11 +161,13 @@ public Object[] toArray() { return shadowSet.toArray(a); } - @SuppressWarnings("keyfor:argument") // delegation + @SuppressWarnings({ + "keyfor:argument" // delegation + }) @Override public boolean add( @UnknownInitialization(AnnotationMirrorSet.class) AnnotationMirrorSet this, - AnnotationMirror annotationMirror) { + @Owning AnnotationMirror annotationMirror) { if (contains(annotationMirror)) { return false; } @@ -179,7 +185,7 @@ public boolean remove(@Nullable Object o) { } @Override - public boolean containsAll(Collection c) { + public boolean containsAll(@NotOwningCollection AnnotationMirrorSet this, Collection c) { for (Object o : c) { if (!contains(o)) { return false; diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 5bd8445c9f0..1aff290ff6f 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -169,6 +169,16 @@ public static boolean isConstructor(MethodTree tree) { return tree.getName().contentEquals(""); } + /** + * Checks if the method invocation is a call to hasNext. + * + * @param tree a tree defining a method invocation + * @return true iff tree describes a call to hasNext + */ + public static boolean isHasNextCall(MethodInvocationTree tree) { + return isNamedMethodCall("hasNext", tree) && tree.getArguments().isEmpty(); + } + /** * Checks if the method invocation is a call to super. * @@ -1711,6 +1721,36 @@ && getFieldName(tree).equals("length")) { return false; } + /** + * If the given tree is a call to "get", this method returns the expression tree of the first + * argument and null else. + * + *

Assuming it's a call to List.get(), this will be the iterator variable. For example, if the + * tree is {@code Collection.get(i)}, the method returns {@code i}. + * + * @param tree the tree to check + * @return ExpressionTree of {@code idx} if tree is {@code Collection.get(idx)} and null else + */ + public static @Nullable ExpressionTree getIdxForGetCall(Tree tree) { + if ((tree instanceof MethodInvocationTree) + && isNamedMethodCall("get", (MethodInvocationTree) tree)) { + return ((MethodInvocationTree) tree).getArguments().get(0); + } + return null; + } + + /** + * Returns true if the given tree is of the form object.size(). + * + * @param tree the tree to check + * @return true if the given tree is of the form object.size() + */ + public static boolean isSizeAccess(Tree tree) { + return (tree instanceof MethodInvocationTree) + && isNamedMethodCall("size", (MethodInvocationTree) tree) + && ((MethodInvocationTree) tree).getArguments().isEmpty(); + } + /** * Returns true if the given {@link MethodTree} is an anonymous constructor (the constructor for * an anonymous class).