False positive in resource leak checker when there is no catch block before finally block

[Nargeshdb]

The following example shows a false positive in resource leak checker. The code closes in1 and in2 on all paths in both tests but the checker reports a warning for test2. The only difference between this two tests is an empty catch block that shouldn't make any difference.

import java.io.*;
import java.net.*;
import org.checkerframework.checker.calledmethods.qual.*;
import org.checkerframework.checker.mustcall.qual.*;
import org.checkerframework.common.returnsreceiver.qual.*;

class FalsePositiveInRLC {

  void test1(@Owning InputStream in1, @Owning InputStream in2)
      throws IOException {
    try {
      in1.close();
    } catch (IOException e) {
    } finally {
      in2.close();
    }
  }

  // :: error: required.method.not.called
  void test2(@Owning InputStream in1, @Owning InputStream in2)
      throws IOException {
    try {
      in1.close();
    } finally {
      in2.close();
    }
  }
}

[msridhar]

@Nargeshdb I'm guessing the ReplicaInputStream stuff in your example is irrelevant to the bug, i.e., even this method won't be verified by the Resource Leak Checker:

  void test2(@Owning InputStream in1, @Owning InputStream in2)
      throws IOException {
    try {
      in1.close();
    } finally {
      in2.close();
    }
  }

Can you confirm?

I visualized the CFG for the simplified method above:
cfg.pdf

The CFG looks correct to me, but I see a potential problem. In the RLC, we do not propagate obligations along exceptional edges corresponding to NullPointerException and other ignored exception types. But, I think the Called Methods Checker does not filter these edges from consideration. Further, if you look at the CFG there are control-flow merge points at certain nodes where the predecessor edges correspond to multiple exception types, e.g.:

So, I wonder if at the entry of the in2 [ LocalVariable ] block in the above screenshot, the Called Methods Checker store does not include @CalledMethods("close") as the inferred type of in1 (since it is merging in a store from the predecessor NullPointerException edge). If this is the case, that would explain the false positive.

@Nargeshdb @kelloggm what do you think? Any ideas on a fix?

[kelloggm]

@msridhar your diagnosis looks right to me. We could add logic to the Called Methods Checker to handle this case without impacting its soundness: null already has the type @CalledMethodsBottom.

[Nargeshdb]

Can you confirm?

@msridhar you're right, ReplicaInputStream is irrelevant, I updated the example.

@Nargeshdb @kelloggm what do you think? Any ideas on a fix?

It looks right to me too.

[msridhar]

@msridhar your diagnosis looks right to me. We could add logic to the Called Methods Checker to handle this case without impacting its soundness: null already has the type @CalledMethodsBottom.

Yup this makes sense. For NullPointerExceptions I think we could change the Called Methods Checker, under the philosophy that NPEs should be prevented by the Nullness Checker. The Resource Leak Checker ignores a bunch of other exception types as well. So maybe we can implement this in an extensible way, such that the Resource Leak Checker could broaden the set of exception types to be ignored.