Resource Leak Checker's rules for owning fields rely on a stronger contract for @EnsuresCalledMethods than the actual contract

[kelloggm]

The contract of the @EnsuresCalledMethods annotation is that it guarantees that the given method(s) are called on the given expression(s) if the method exits normally. The rules used by the Resource Leak Checker, however, assume that the given methods are called on all paths. This was first noticed by @msridhar in https://github.com/typetools/checker-framework/pull/4808/files#r673287910.

As a concrete example, consider the following program:

import java.io.IOException;
import java.io.InputStream;
import java.io.Closeable;
import org.checkerframework.checker.mustcall.qual.Owning;
import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;

class ReplicaInputStreams implements Closeable {

  private final @Owning InputStream in1;
  private final @Owning InputStream in2;

  public ReplicaInputStreams(
      @Owning InputStream i1, @Owning InputStream i2) {
    this.in1 = i1;
    this.in2 = i2;
  }

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

Currently, the Resource Leak Checker incorrectly verifies this program (i.e. running javac -processor resourceleak ReplicaInputStreams.java does not issue any errors). I would expect some kind of error to be issued about this implementation of close(), because it does not guarantee that in2.close() is called on all paths - there is an exceptional exit path from in1.close().

Confusingly, a similar example I wrote up does issue an error:

import java.net.Socket;
import java.io.IOException;
import org.checkerframework.checker.mustcall.qual.*;
import org.checkerframework.checker.calledmethods.qual.*;

@MustCall("dispose")
class TwoResourcesECM {
  @Owning Socket s1, s2;

  @EnsuresCalledMethods(value = {"this.s1", "this.s2"}, methods={"close"})
  public void dispose() throws IOException {
    s1.close();
    s2.close();
  }
}

In this nearly identical example, the Called Methods Checker rejects dispose(), issuing the following error:

!?rlc-twoclose-soundness ~/jsr308/checker-framework> checker/bin/javac -processor resourceleak checker/tests/resourceleak/TwoResourcesECM.java    
checker/tests/resourceleak/TwoResourcesECM.java:14: error: [contracts.postcondition] postcondition of dispose is not satisfied.
  public void dispose() throws IOException {
              ^
  found   : no information about this.s1
  required: this.s1 is @CalledMethods("close")
1 error
exit 1

[kelloggm]

I see two possible paths forward on this issue:

• assume the false negative is in the Called Methods Checker, and that the first example (ReplicaInputStreams) should also issue a contracts.postcondition error. This would also involve changing the documentation of EnsuresCalledMethods (and maybe other postcondition annotations, too) so that they're guaranteed to be rejected if the method may not guarantee them on non-exceptional exits.
• assume the false negative is in the Resource Leak Checker, and that the contracts.postcondition error in the second example is a false positive. This would require us to change how the Resource Leak Checker handles owning fields: it should check that the destructor-like method does actually close the owned field on all paths rather than just relying on an @EnsuresCalledMethods annotation. More detail on this below.

I think the second option is the better one. The fix will likely be smaller, though there is still the unexplained contracts.postcondition false positive in the second example. Taking the first path would likely result in changes to other postcondition annotations, which is undesirable (unless they're buggy).

More detail on my proposal to fix the Resource Leak Checker: in a class C with owning fields f_1...f_n and must-call obligations to call destructors m_1...m_k, I propose that rather than relying on the Called Methods Checker to verify the @EnsuresCalledMethods annotation on each destructor, the Resource Leak Checker should apply its own analysis (i.e. the Must Call Consistency Analyzer) to each such method, with the fields that that destructor supposedly guarantees will be closed treated as in-scope local variables whose obligations need to be fulfilled before the method exits. That is, for each m_i in m_1...m_k, the Consistency Checker will look at the existing @EnsuresCalledMethods annotation and see that it guarantees the requirements will be fulfilled on the happy path for some f_x in f_1...f_n. (The checker already does this.) I propose that in addition, each such f_x will be added to the set of resource aliases for a new Obligation, which will be tracked in the same manner as an owning formal parameter or newly-created local variable. Because the existing Consistency Checker already tracks that the required methods are called on all paths, this should do what we want and prevent the false negative above.

Because there isn't an assignment tree, we won't be able to use the existing required.method.not.called error. I suggest adding a new required.method.not.called.owning.field error instead, which will be issued on the method declaration and give the name of the field, the missing method calls, and the path, similar to the existing error message for other kinds of aliases.

[kelloggm]

A third possible option: insert a new kind of postcondition annotation, such as @EnsuresCalledMethodsOnAllPaths, that has the semantics described above. Then, require it for destructors and use the same verification procedure described above. This seems to have all the same downsides as the proposal above, with the added one of introducing a new annotation, to me.

[kelloggm]

@msridhar @mernst @Nargeshdb what do you think of these proposed fixes?

[msridhar]

I like the second option. One comment.

each such f_x will be added to the set of resource aliases for a new Obligation

I wonder instead of tracking new Obligations in the consistency analyzer, we could instead just piggy-back on the existing type inference for the Called Methods Checker, by just checking if the relevant fields have the right CalledMethods type in the store corresponding to the exceptional exit. I don't think we really need any of the consistency analyzer's logic for variables going out of scope early, tracking resource aliases, etc. for this case. @kelloggm am I missing something? This alternate scheme might be even simpler. If we can get access to the relevant stores in the ResourceLeakVisitor we could potentially even do the check right there.

[kelloggm]

I don't think we really need any of the consistency analyzer's logic for variables going out of scope early, tracking resource aliases, etc. for this case

That's fair, but I was planning to do it this way for implementation reasons - I think this approach is actually simpler rather than adding another check that requires digging into the Called Methods store. We already have to machinery to do so, so we may as well use it.

If we can get access to the relevant stores in the ResourceLeakVisitor we could potentially even do the check right there

We still need a dataflow analysis to compute the "going-out-of-scope" point; I don't think there's a hook in the visitor to run a check at the end of a method. I think it could be done, if somewhat awkwardly, but I'd rather use the existing machinery that we have that will find the right "going-out-of-scope" points automatically (I think).

[msridhar]

That's fair, but I was planning to do it this way for implementation reasons - I think this approach is actually simpler rather than adding another check that requires digging into the Called Methods store. We already have to machinery to do so, so we may as well use it.

Thinking more, my hesitation is that the consistency analyzer knows nothing about tracking a field as a resource alias right now; it only knows about locals. Probably you could just create a temporary local yourself associated with the field, but I still think you'd need special logic in the actual consistency check at the exit stores to look up the info for the field in place of the local. It might work out, just may end up being rather hackish.

If we can get access to the relevant stores in the ResourceLeakVisitor we could potentially even do the check right there

We still need a dataflow analysis to compute the "going-out-of-scope" point; I don't think there's a hook in the visitor to run a check at the end of a method. I think it could be done, if somewhat awkwardly, but I'd rather use the existing machinery that we have that will find the right "going-out-of-scope" points automatically (I think).

My assumption was that the Resource Leak Checker's visitor runs after type inference has completed. So, if you can get access to the exceptional exit store somehow, you could just implement the check in visitMethod() by looking up the right store. I could have missed something though.