Incorrect RLC inference of EnsuresCalledMethods for outer-class fields released by inner-class methods

[iamsanjaymalakar]

The inference for Resource Leak Checker's (RLC) annotations incorrectly infers the EnsuresCalledMethods annotation on outer-class resources that are closed by methods within an inner class.

For example:

class Foo {
    @Owning private final FileWriter fileWriter; 

    public Foo(File file) throws IOException {
        this.fileWriter = new FileWriter(file);
    }

    private class InnerFoo {
        // The inference incorrectly produces:
        // @EnsuresCalledMethods(value = { "this.fileWriter" }, methods = { "close" })
        public void close() throws IOException {
            fileWriter.close();
        }
    }
}

Here, the field fileWriter is declared and owned by the outer class Foo. However, since it is closed inside the inner class InnerFoo, the inference incorrectly annotates it as:

@EnsuresCalledMethods(value = { "this.fileWriter" }, methods = { "close" })

The reference this.fileWriter is incorrect because fileWriter is not a field of the inner class (InnerFoo), but a field of the outer class (Foo). If the annotation should be allowed at all, it needs to properly reference the field as belonging to the outer class.

Additionally, this situation raises some questions about intended behavior:

• Should inference allow inner-class methods to ensure called methods on outer-class fields?
• If yes, what should the correct syntax for referencing the outer-class field be? (e.g., Foo.this.fileWriter)
• Given that the method performing the close operation belongs to the inner class, what should the inferred method name for InheritableMustCall annotation on the outer class be? In this scenario, it clearly cannot use the inner-class method directly as that method isn't accessible in the outer-class context.

I need some clarifications on the intended semantics and proper annotation references.

[msridhar]

I think that if Checker Framework supports it, inferring @EnsuresCalledMethods on the inner class method using syntax like Foo.this.fileWriter is fine. But I don't see how we can infer an @InheritableMustCall method for the outer class; that would need to be a method on Foo itself I think. @iamsanjaymalakar do you have a real code example showing how the inner class method is correctly used to ensure there is no leak? That might help us understand if/how we can handle this.

[iamsanjaymalakar]

@msridhar this is the abstracted example from real code keeping the same structure on how the real code closed the resource:

class Foo {
    @Owning private final FileWriter fileWriter; 
    private InnerFoo innerFoo;

    public Foo(File file, InnerFoo innerFoo) throws IOException {
        this.fileWriter = new FileWriter(file);
        this.innerFoo = innerFoo;
    }

    public void handle() {
         innerFoo.close();
    }

    private class InnerFoo {
        // The inference incorrectly produces:
        // @EnsuresCalledMethods(value = { "this.fileWriter" }, methods = { "close" })
        public void close() throws IOException {
            fileWriter.close();
        }
    }
}

This is the full source code of the file containinng this example: https://gist.github.com/iamsanjaymalakar/45cffb7d4312d58d9c3d02ee6ea0f5f3 (The owning field is private final SessionImpl m_session).

[msridhar]

Ok. It seems we could handle this via inference, but it might be tricky. I'm not sure it's a common enough case to be worth prioritizing.