Resource Leak Checker: false positives when a resource is allocated and closed in the same expression

[Calvin-L]

The Resource Leak Checker does not accept this code:

  static void method() {
    // error: [required.method.not.called] @MustCall method close may not have been invoked on new Resource()
    close(new Resource());
  }

  @EnsuresCalledMethods(value = "#1", methods = "close")
  static void close(Resource r) {
    r.close();
  }

this very similar code works:

  static void method() {
    Resource r = new Resource();
    close(r);
  }

However, that refactoring is not possible when

• method is a constructor
• close is a call to super(...) or this(...)

For example:

class TestCase {
  @EnsuresCalledMethods(value = "#1", methods = "close")
  TestCase(Resource r) {
    r.close();
  }

  TestCase() {
    // error: [required.method.not.called] @MustCall method close may not have been invoked on new Resource()
    this(new Resource());
  }
}

Below is a more complete set of tests that exercise a few variants of that pattern. The RLC reports false positives for test cases 3-7.

import java.io.*;
import org.checkerframework.checker.calledmethods.qual.*;

class AllocResourceInExpression {

  static void testCase1() {
    new Resource().close();
  }

  static void testCase2() {
    alloc().close();
  }

  static void testCase3() {
    new Resource().free();
  }

  static void testCase4() {
    alloc().free();
  }

  static void testCase5() {
    close(new Resource());
  }

  static void testCase6() {
    close(alloc());
  }

  class TestCase7 {
    @EnsuresCalledMethods(value = "#1", methods = "close")
    TestCase7(Resource r) {
      r.close();
    }

    TestCase7() {
      this(new Resource());
    }
  }

  static class Resource implements Closeable {
    @Override
    public void close() {}

    @EnsuresCalledMethods(value = "this", methods = "close")
    public void free() {
      close();
    }
  }

  static Resource alloc() {
    return new Resource();
  }

  @EnsuresCalledMethods(value = "#1", methods = "close")
  static void close(Resource r) {
    r.close();
  }

}

[msridhar]

Did some investigation on this one, and it looks like at least one issue is we do not have handling of postconditions when they impact temporary variables. We have special handling here for when a method is directly invoked on an expression that has a temporary variable:

checker-framework/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakTransfer.java

Lines 78 to 87 in 49d97d7

	// If there is a temporary variable for the receiver, update its type.
	Node receiver = node.getTarget().getReceiver();
	MustCallAnnotatedTypeFactory mcAtf =
	rlTypeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class);
	Node accumulationTarget = mcAtf.getTempVar(receiver);
	if (accumulationTarget != null) {
	String methodName = node.getTarget().getMethod().getSimpleName().toString();
	methodName = rlTypeFactory.adjustMethodNameUsingValueChecker(methodName, node.getTree());
	accumulate(accumulationTarget, result, methodName);
	}

We need to extend this logic to handle the case where a postcondition (via @EnsuresCalledMethods) impacts a temp var. The built-in logic for handling post-conditions is around here:

checker-framework/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

Line 1111 in 49d97d7

private void processPostconditionsAndConditionalPostconditions(

@kelloggm do you think there's a way we could easily extend this logic with some method overrides? Otherwise we may need to do some copy-pasting.

[kelloggm]

If we have a ResourceLeakStore or create one, we might be able to override CFAbstractStore#insertOrRefine (which the postcondition code calls indirectly) so that it checks for temporary variables and also applies the insert/refine operation to those. As a bonus, that might also let us get rid of that special case you mentioned in ResourceLeakTransfer.

The problem is going to be finding the appropriate tempvar. insertOrRefine takes a JavaExpression, but MustCallAnnotatedTypeFactory#getTempVar operates on CFG Nodes. Going from Node -> JavaExpression is doable, but I don't think it's easy to go the other way (it may not be possible, but I'd need to do some more in-depth investigation).

Copy-pasting code from CFAbstractTransfer is ugly, but it would definitely be easier. Another option would be write a new overridable method in CFAbstractTransfer that allows subclasses to specify a set of nodes that a postcondition should also apply to (default: none).

[kelloggm]

With some more investigation, I'm not sure that our current implementation can handle this case without either a major refactoring, a new CFG API, or both. In particular, the core problem is the way that we track temporary variables.

Temporary variables are stored by the MustCallAnnotatedTypeFactory in an IdentityHashMap that is keyed on Trees. This means that to get a temporary variable, we need the associated Tree object (which is the Tree representing the expression). It is not possible (in our current implementation) to get a temporary variable for a given expression unless you can access either a Tree or Node that represents that expression: we don't keep any other kind of identifying information.

Even if we copy code from CFAbstractTransfer, under the hood it is using JavaExpression as the key into the store (i.e., the store is conceptually a map from JavaExpressions to annotations/types). Effectively, it:

1. converts and viewpoint adapts the argument to the postcondition annotation to get a JavaExpression. For example, this converts "#1" to a JavaExpression for "foo", if "foo" is the name of the parameter
2. looks up the current entry for that JavaExpression in the store
3. merges that store entry with whatever the postcondition annotation implies

As far as I know (@smillst can confirm), there is no way to retrieve a Node or Tree associated with a JavaExpression: JavaExpressions are context-free. If it was possible, we'd need some kind of lookup (maybe via the CFG?), and it would necessarily need some kind of search logic - probably something conceptually similar to what we have in StringToJavaExpression, but using the information in the target JavaExpression + some context to find a Tree or Node that matches.

In other words, we need to either:

1. build a currently non-existent API (probably in the CFG). It takes as input a JavaExpression + a context (e.g., in the form of a Node) and returns the Node from which the JavaExpression must have been constructed. This would enable us to contemplate making the necessary changes to CFAbstractTransfer to support this use case.
2. totally change the way that we store tempvars in the RLC, so that it's possible to look one up based on a JavaExpression and a context. I'm not even sure how to begin to approach that problem (need to think a little more), but I don't think the solution is that different than building an RLC-specific version of the previous approach.

[msridhar]

Thanks for digging into this @kelloggm. One question:

converts and viewpoint adapts the argument to the postcondition annotation to get a JavaExpression. For example, this converts "#1" to a JavaExpression for "foo", if "foo" is the name of the parameter

At this step the logic must have a handle on the Tree or Node for the method invocation, correct? Is there hope of doing something like making a copy of this viewpoint adaptation logic to just give back the relevant actual parameter, rather than a JavaExpression?

[kelloggm]

At this step the logic must have a handle on the Tree or Node for the method invocation, correct? Is there hope of doing something like making a copy of this viewpoint adaptation logic to just give back the relevant actual parameter, rather than a JavaExpression?

Yes, that's what the logic in StringToJavaExpression that I alluded to does: it takes as input some kind of context (the MethodInvocationNode whose postcondition is being processed) and then does something similar but not quite the same as what we need. I don't know this code very well, but I imagine we could write a similar kind of API that returns a Node: that's what I'm suggesting in my first suggestion (1) at the end of my previous comment.

[msridhar]

I guess what I don't understand from suggestion (1) is why it would take a JavaExpression as an input? Shouldn't it take the same inputs as the viewpoint adaptation code, i.e., the "context" Node and the post-condition annotation like "#1"?

[kelloggm]

Sorry to come back to this much later.

I guess what I don't understand from suggestion (1) is why it would take a JavaExpression as an input? Shouldn't it take the same inputs as the viewpoint adaptation code, i.e., the "context" Node and the post-condition annotation like "#1"?

It could, but then we'd need to viewpoint adapt the "#1" anyway to figure out what it refers to (which will give us a JavaExpression), and we know that we'll already have the relevant JavaExpression in hand. I think this is an implementation detail, though, and we'd have to implement it to see what works best.