Spurious resource leak report when returning before a variable's definition

[Calvin-L]

Given this code:

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

abstract class TestCase {

  abstract @Nullable Closeable alloc();
  abstract boolean arbitraryChoice();

  void method() throws IOException {

    if (arbitraryChoice()) {
      return;
    }

    Closeable r1 = alloc();
    if (r1 == null) {
      return;
    }
    r1.close();

  }

}

The RLC reports

error: [required.method.not.called] @MustCall method close may not have been invoked on r1 or any of its aliases.
      Closeable r1 = alloc();
                ^
  The type of object is: java.io.Closeable.
  Reason for going out of scope: regular method exit

The error looks spurious. Indeed, removing the early return block

      if (arbitraryChoice()) {
        return;
      }

silences the warning! It appears that the RLC wants us to close r1 at the premature return site, before it has been defined.

[msridhar]

Did some quick investigation here. Something seems to be going on where when we remove the first early return block, the resource leak store (i.e., the called methods store) holds the fact that close() is always called on r1 at the normal exit of the method. My guess is the first early return block leads to a control-flow merge just before the normal exit, such that the r1.close() fact no longer remains in the store at the normal exit, hence the false positive warning.

Where I am lost is that I don't understand why we don't report a warning even without the first early return block. For this version of the code:

  void method() throws IOException {
    Closeable r1 = alloc();
    if (r1 == null) {
      return;
    }
    r1.close();
  }

Reasoning that this code is safe requires knowing that at the explicit return statement, r1 is null and hence should have type @CalledMethodsBottom (or something like that). I don't see any code in our checkers that performs this kind of reasoning, though. @kelloggm @Nargeshdb am I missing something, and did we write code somewhere to reason about this kind of null check?

[msridhar]

Ok, upon further investigation I found the code that refines the type of r1 under the conditional to @CalledMethodsBottom due to the null comparison (very cool!):

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

Line 766 in 49d97d7

protected TransferResult<V, S> strengthenAnnotationOfEqualTo(

So now I think the issue is in how we handle the control-flow merge resulting from the first explicit return statement. Here is the relevant comment:

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

Lines 1173 to 1174 in 49d97d7

	// local variables that are only part of one store, but not the other are discarded, as
	// one of store implicitly contains 'top' for that variable.

In this case, I don't think this comment captures what we want to do. The first early return appears even before r1 is declared. So really, we'd like the absence of r1 in that store to be interpreted as r1 having the type @CalledMethodsBottom.

@smillst @mernst have you seen this issue come up before? Is there a way we can tweak the Called Methods Checker to get this desired behavior?

[Calvin-L]

@msridhar I also did a little investigating. I'm not sure if this will be useful, but here are some disorganized thoughts.

---

My original diagnosis might not have been right. The test case is very brittle. You can also, surprisingly, silence the error by removing the second if-check:

    if (r1 == null) {
      return;
    }

So I might have been wrong when I wrote "the RLC wants us to close r1 at the premature return site, before it has been defined". Instead, I now believe that there's some other explanation, and that you figured it out:

So now I think the issue is in how we handle the control-flow merge resulting from the first explicit return statement.

But, I have a different idea about the fix.

Here's the relevant part of the CFG:

The conditional block at the top of the picture corresponds to the second if-check in the original code. The error is reported when MustCallConsistencyAnalyzer.propagateObligationsToSuccessorBlock visits the starred edge.

There's a piece of true information that is not shown the CFG:

• Along the starred edge, the information r1 > @CalledMethodsBottom flows to the <exit> block.

But that information is lost. As you noted, r1 is not present in the <exit> block's before-store because it is not present in every incoming store. Instead, we only have access to the merged result of all those incoming stores. Some incoming stores have r1 in scope and some don't.

Instead of making a sweeping change like

the absence of r1 in that store to be interpreted as r1 having the type @CalledMethodsBottom

maybe a simpler fix is to write a method that can tell us what information flows along a certain edge. Such a method might obviate a lot of complex and subtle logic in MustCallConsistencyAnalyzer:

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

Lines 2098 to 2099 in 43db447

	// Which stores from the called-methods and must-call checkers are used in
	// the consistency check varies depending on the context. The rules are:

Ideally, I think all that complex logic could be replaced with something extremely simple:

  var mcStore = mcAtf.getAnalysisResult().getStoreAlongEdge(currentBlock, successor);
  var cmStore = analysis.getResult().getStoreAlongEdge(currentBlock, successor);

[msridhar]

Very interesting @Calvin-L. I'll have to digest more but your proposed solution sounds a lot simpler and cleaner than what I was thinking.

[msridhar]

maybe a simpler fix is to write a method that can tell us what information flows along a certain edge. Such a method might obviate a lot of complex and subtle logic in MustCallConsistencyAnalyzer

Looking more I think this is the right idea here. The problem in this case is that when doing a consistency check for the CFG edge from a conditional block to the exit block, we use analysis.getInput(currentBlock).getRegularStore() to do the consistency check. We should instead choose either the then store or the else store, depending on which successor edge we are looking at. I think this is only an issue for conditional blocks. For any other block with multiple CFG successors (just exceptional blocks?), the block should contain at least one node, and then we choose the store immediately after that node, which is indeed the information that would flow along any successor edge.

As to adding a getStoreAlongEdge() method, it's a nice abstraction that could make the code easier to read, but I think we'd have to implement it using logic similar to what we have now. Unfortunately I don't think that information is cached anywhere in the AnalysisResult. There is also some hacky logic around @CreatesMustCallFor here:

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

Lines 2145 to 2148 in 43db447

	// If this is an exceptional block, check the MC store beforehand to avoid
	// issuing an error about a call to a CreatesMustCallFor method that might
	// throw an exception. Otherwise, use the store after.
	if (exceptionType != null && isInvocationOfCreatesMustCallForMethod(last)) {

But I think that will go away as part of #6221.

[msridhar]

FYI I have a WIP branch investigating a fix to this issue here:

https://github.com/msridhar/checker-framework/tree/issue-6317

Still too hacky and not everything is working as I expect, but I think (hope?) it's on the right track.