Resource Leak Checker: multiple false positives trying to build a collection of owned resources

[Calvin-L]

I am working on a program that passes around "bundles" of resources. When a client is done with a bundle, all of the underlying resources have to be closed.

Today my program represents bundles as List<Resource>. I more or less understand why List<@Owned Resource> is disallowed, so I set out to write a small class that can own more than one resource. I was not able to make headway using arrays, but I almost succeeded using a linked data structure.

However, the Resource Leak Checker still issues a number of errors that I am unable to fix. In particular, I would like it to be powerful enough to verify the loop in disconnectAll():

import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor;
import org.checkerframework.checker.mustcall.qual.MustCall;
import org.checkerframework.checker.mustcall.qual.Owning;
import org.checkerframework.checker.nullness.qual.Nullable;

import java.io.Closeable;
import java.io.IOException;

@MustCall("disconnectAll")
public class ResourceBundle {

    private @Owning @Nullable Node head = null;

    @CreatesMustCallFor("this")
    public boolean add(@Owning Closeable resource) {
        head = new Node(resource, head);
        return true;
    }

    @EnsuresCalledMethods(value="this.head", methods="disconnect")
    public void disconnectAll() {
        Node ptr = head;
        while (ptr != null) {
            ptr = ptr.disconnect();
        }
    }

    @MustCall("disconnect")
    private static class Node {
        @Owning private final Closeable resource;
        @Owning private final @Nullable Node next;

        public Node(@Owning Closeable resource, @Owning @Nullable Node next) {
            this.resource = resource;
            this.next = next;
        }

        @EnsuresCalledMethods(value="this.resource", methods="quietDisconnect")
        @EnsuresCalledMethods(value="this.next", methods="disconnect")
        public @Owning @Nullable Node disconnect() {
            try {
                resource.close();
            } catch (IOException e) {
                e.printStackTrace();
            }
            return next;
        }
    }

}

Checker Framework version 3.34.0 issues four spurious-looking errors.

1. At head = new Node(resource, head);: "error: [required.method.not.called] @MustCall method disconnect may not have been invoked on field head or any of its aliases [...] Non-final owning field might be overwritten". I believe the error is incorrect; the Node constructor takes ownership of the old value of head.
2. At public void disconnectAll(): "error: [contracts.postcondition] postcondition of disconnectAll is not satisfied. [...] found : no information about this.head [...] required : this.head is @CalledMethods("disconnect")". This message is extremely confusing. There must be a way to write this loop that satisfies the RLC, but I can't figure it out.
3. At @Owning private final Closeable resource;: "@EnsuresCalledMethods written on MustCall methods doesn't contain method close". Likely due to False positive in the resource leak checker when the finalizer method has multiple @EnsuresCalledMethods annotation #5911.
4. At @Owning private final @Nullable Node next;: "@EnsuresCalledMethods written on MustCall methods doesn't contain method disconnect". Likely due to False positive in the resource leak checker when the finalizer method has multiple @EnsuresCalledMethods annotation #5911.

I was able to make a little progress using a silly-looking helper definition vaguely inspired by C++ std::move:

    @Pure
    private static @Owning @Nullable Node move(@Owning @Nullable Node x) {
        return x;
    }

With that definition, error (1) can be silenced using this code instead:

        Node oldHead = move(head);
        head = new Node(resource, oldHead);

However, I still have no way to silence error (2). I had thought that changing the first line of disconnectAll to Node ptr = move(head); might do the trick, but that seems to have no effect.

[kelloggm]

Today my program represents bundles as List. I more or less understand why List<@Owned Resource> is disallowed, so I set out to write a small class that can own more than one resource. I was not able to make headway using arrays, but I almost succeeded using a linked data structure.

I'm impressed by how close you've come! Currently, the RLC is not designed to permit you to verify that arbitrarily-sized collections of resources can be closed without warning suppressions, unfortunately.

I've opened a new issue to track problem 1 (#5971). I suspect that there is an easy fix to that one.

As for issue 2, I don't know of a way to write the loop in a way that the RLC will verify. @Nargeshdb @msridhar do you have any ideas? As I mentioned before, the RLC isn't really designed to handle this case.

An alternative would be to make each ResourceBundle responsible for a fixed set of resources (e.g., by making fields for each resource in the bundle). I don't know if this is possible in your use case, because it requires you to know the number of resources that each bundle will handle at compile time. If you do know that e.g., each bundle will always hold 3 resources, you could make each of those resources a field in the bundle; the RLC should be able to verify such a class.

[msridhar]

I am also amazed how far you got @Calvin-L! Unfortunately I don't really see a way to get around 2 with the current RLC either. What we really need is some way to support @Owning type variables and to reason about when the corresponding obligations are satisfied. A hacky initial approach to this would be to bake in some understand of Java's for-each loop. The hope would be that we could verify code like this:

@MustCall("release")
class Foo {
  List<@Owning InputStream> streams;
  ...
  void addStream(@Owning InputStream s) {
    // support ownership transfer here somehow
    streams.add(s);
  }
  // syntax??
  @EnsuresCalledMethods("streams.__contents__","close")
  void release() {
    for (InputStream s: streams) {
      try {
        s.close();
      } catch (Exception e) { /* log it? */ }
    }
  }
}

But there are probably gotchas I didn't think of. And adding this support will take some work. This is a relatively high-priority feature for us to work on, but for now, I'm not sure what you can do with the RLC other than suppress the warnings.

[jacek-lewandowski]

I've also tried to implement a collection of resources. Additionally, to the problems mentioned above, I found no way to return a collection of those resources to iterate over by the callers so that the resources are must-call-aliases. The callers were always blamed for not calling the required method.