Possible unsoundness in the resource leak checker due to ownership + generics

[Calvin-L]

I am applying the resource leak checker to a large program. I encountered some interesting patterns.

Perhaps the most interesting: my program has a number of methods that take ownership of an object but are generic. In some sense these methods "forget" the type of the owned argument, including any must-call requirements. (In practice the owned objects are eventually passed back to a non-generic callback that closes the argument. The flow is not obviously correct and difficult to simplify, and therefore it is important to verify.)

I'm worried that the resource leak checker might be missing some bugs in my program. Consider this simplified example:

package calvin.example;

import org.checkerframework.checker.mustcall.qual.*;

class Resource implements java.io.Closeable {
    @Override
    public void close() {
    }
}

public class Driver {

    public static <T> void sneakyDrop(@Owning T value) {
    }

    public static void main(String[] args) throws Exception {
        Resource x = new Resource();
        sneakyDrop(x);
    }

}

To my surprise, the call to sneakyDrop(x) seems to satisfy the resource leak checker even though the resource x is obviously not being closed.

[kelloggm]

Thanks for reporting this, and sorry you've encountered a problem.

To my surprise, the call to sneakyDrop(x) seems to satisfy the resource leak checker even though the resource x is obviously not being closed.

I am also surprised by this - I would expect that the Must Call Checker would issue an error when you attempt to substitute an @MustCall("close") Resource for a T.

Here is a theory about why: CLIMB-to-top inference treats T and T extends Object differently: the former is usually default to the top type, while the latter uses the regular rules for Object. In the Must Call Checker, the top type is an artificial, invisible type (@MustCallUnknown, meaning any must call obligations are permitted); the default for object by contrast is bottom (@MustCall({})). The Resource Leak Checker might be incorrectly assuming that T means T extends @MustCallUnknown Object, but if it is doing so I'd expect us to get a warning in sneakyThrows, instead.

Regardless, I'll investigate this issue and let you know when we've figured it out (probably tomorrow, though, since it's late on the east coast already).

[kelloggm]

There was in fact a soundness bug related to @MustCallUnknown, which should be fixed by #5912. My hypothesis in my previous comment about the cause appears to have been correct: T means T extends @MustCallUnknown Object, and the checker's logic for handling obligations incorrectly treated @MustCallUnknown as @MustCall({}) when converting between two internal subcheckers (the Must Call Checker and the consistency analyzer).

[Calvin-L]

Thanks a ton for the quick followup. :)