Resource Leak Checker: inconsistent behavior for ownership transfer in constructor

[Calvin-L]

Consider:

import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
import org.checkerframework.checker.mustcall.qual.Owning;
import org.checkerframework.checker.nullness.qual.NonNull;

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

public class ConstructorOwnership implements Closeable {

    private final @Owning @NonNull Closeable resource;

    public ConstructorOwnership(@Owning @NonNull Closeable resource, int value) {
        if (value == 0) {
            throw new IllegalArgumentException();
        }
        this.resource = resource;
    }

    public ConstructorOwnership(@Owning @NonNull Closeable resource, boolean value) {
        this.resource = resource;
        if (value) {
            throw new IllegalArgumentException();
        }
    }

    @Override
    @EnsuresCalledMethods(value = "resource", methods = {"close"})
    public void close() throws IOException {
        resource.close();
    }

}

The resource leak checker reports an error for the first constructor, but not the second:

ConstructorOwnership.java:[14,59] error: [required.method.not.called] @MustCall method close may not have been invoked on resource or any of its aliases.

I think it should report an error for both constructors or neither. I am not sure which it should be.

[msridhar]

Thanks for the report @Calvin-L. I think an error should be reported for the second constructor as well, since if it terminates exceptionally, there will be no reference to a ConstructorOwnership object that can be used to invoke close() (so ownership was not successfully transferred). I'm pretty sure this is a soundness bug.

[msridhar]

After further discussion with @kelloggm and @Nargeshdb I think the above comment is wrong. We now think that @Owning on a parameter p of method m (constructor or not) should mean that an ownership transfer takes place only when m returns normally. If m throws an exception, then no ownership transfer occurs, and the caller is still responsible for satisfying the @MustCall obligation of whatever value was passed in. The issue is that even for a non-constructor method, the caller may be left with no reference to the relevant object in the exceptional case (e.g., for code like x = makeContainer(s)), and in such cases the caller will still only have the option of satisfying the @MustCall obligation of the parameter. It's best to be consistent here.

We need to test how we handle calls to methods with @Owning parameters to make sure the ownership only occurs on the normal successor of the call. If those are handled correctly, then this is not a soundness issue. And, I now think the right fix here is to not report an issue for the first constructor.

We also need to update our documentation on @Owning parameters to capture this subtlety, both in the manual and in the Javadoc.

[Calvin-L]

I think I agree.

Here's a related thought:

The "transfer ownership only on normal return" rule would also address a secret fear of mine: when you call a method or constructor, the JVM can throw certain exceptions (e.g. OutOfMemoryError or StackOverflowError) before the called code has a chance to run even a single instruction. In those cases, ownership has to remain with the caller.

FWIW I am firmly in the camp that there are no safe ways to handle those Errors, and that nobody should try... but the reality is that lots of programs catch Throwable and think they can keep running, and I think the RLC should be able to say something true about those programs.

[Calvin-L]

@msridhar @kelloggm I've made some hacky local patches that fix this issue. If nobody else is working on it, I'd be happy to clean them up and open a PR.

[msridhar]

@Calvin-L unfortunately none of us has had time to work on this one yet. If you're able to contribute a PR that would be much appreciated.