Fix unsoundess in Resource Leak Checker related to owning fields and EnsuresCalledMethods

[kelloggm]

fixes #4838

The general approach here is the one described in my comment on #4838: to treat owning fields in destructors as effectively owning formal parameters. As I suspected, the necessary modifications weren't too invasive.

I also enhanced the error message for requird.method.not.called to also name the reference which might not have its must-call obligations fulfilled, because otherwise this PR could cause two identical errors to be issued at the same point. Now, those errors will be different (since they would have to have been about different fields).

[msridhar]

I think I see why this code works, but conceptually it seems a bit hackish, since we don't really treat field access references in a sound way as a resource alias. Consider (assume dispose() is a destructor):

@EnsuresCalledMethods("this.f", "close")
void dispose() {
  this.f = new Socket();
  ...
}

At the program point after the assignment, this.f is no longer an alias for the resource that it named at the beginning of the method, but it will still get propagated as such to the method exit. Like I said, I can see why this works for now, but I worry that by allowing arbitrary JavaExpressions here we might be setting ourselves up for confusion later.

As an alternative, we could leave this type as LocalVariable and then add extra logic to create a temp variable for the field at the beginning of the method and to handle it specially in other places. But that's more code and possibly more clutter in the implementation.

I'll keep thinking about an alternative here; I'd like to mull it over more and see if we can come up with something a bit cleaner.

[kelloggm]

At the program point after the assignment, this.f is no longer an alias for the resource that it named at the beginning of the method, but it will still get propagated as such to the method exit

No, but it is an alias for some resource that this method is responsible for closing. And, our logic for overwriting fields should take care of ensuring that this.f was closed before the re-assignment (in particular, this example cannot ever work, because we wouldn't be able to prove that this.f was closed on the first line of a method).

I worry that by allowing arbitrary JavaExpressions here we might be setting ourselves up for confusion later

The more I've thought about this, the more I've felt that this is what we should've done all along. The restriction that resource aliases must be local variables seems arbitrary; it's a bit of a hack to begin with that formal parameters are represented as locals, for example, but without that we would've already needed to switch to JavaExpression.

As an alternative, we could leave this type as LocalVariable and then add extra logic to create a temp variable for the field at the beginning of the method and to handle it specially in other places. But that's more code and possibly more clutter in the implementation.

I considered this approach and discarded it in favor of the one you see in this PR because I worried that this would lead to more clutter.

One thing that your comment about soundness made me realize is that I think there might still be a soundness hole in this approach: we treat fields that a destructor must close just like any other resource, which means that their obligations can be fulfilled by assigning them to owning fields. That would be circular, and we should forbid it.

[msridhar]

At the program point after the assignment, this.f is no longer an alias for the resource that it named at the beginning of the method, but it will still get propagated as such to the method exit

No, but it is an alias for some resource that this method is responsible for closing.

But won't the tree in the ResourceAlias be incorrect? I don't think it will get updated.

And, our logic for overwriting fields should take care of ensuring that this.f was closed before the re-assignment (in particular, this example cannot ever work, because we wouldn't be able to prove that this.f was closed on the first line of a method).

Yes, that is true.

I worry that by allowing arbitrary JavaExpressions here we might be setting ourselves up for confusion later

The more I've thought about this, the more I've felt that this is what we should've done all along. The restriction that resource aliases must be local variables seems arbitrary; it's a bit of a hack to begin with that formal parameters are represented as locals, for example, but without that we would've already needed to switch to JavaExpression.

I think it depends on what we want our invariants to be. If we want an invariant that if an Obligation gets propagated to a particular program point, then all contained resource aliases must reference the same resource at that program point, it is much easier to maintain the invariant if we only track locals. Once you start tracking fields, you have to worry about updates through an alias. E.g., here is a (contrived) variant of my previous example:

class Foo {
  ...
  @EnsuresCalledMethods("this.f", "close")
  void dispose(Foo x) {
    x.f = new Socket();
    ...
  }
}

Now, whether this.f still references the same Socket after the assignment depends on whether x is aliased with this or not.

As an alternative, we could leave this type as LocalVariable and then add extra logic to create a temp variable for the field at the beginning of the method and to handle it specially in other places. But that's more code and possibly more clutter in the implementation.

I considered this approach and discarded it in favor of the one you see in this PR because I worried that this would lead to more clutter.

Yes, I agree this may be more cluttered. I am wondering if we can just document very carefully what the current code is doing and just get away with that.

One thing that your comment about soundness made me realize is that I think there might still be a soundness hole in this approach: we treat fields that a destructor must close just like any other resource, which means that their obligations can be fulfilled by assigning them to owning fields. That would be circular, and we should forbid it.

Yes, that's interesting. I am honestly not sure what our code would do in that situation; definitely something to be tested.

[kelloggm]

At the program point after the assignment, this.f is no longer an alias for the resource that it named at the beginning of the method, but it will still get propagated as such to the method exit

No, but it is an alias for some resource that this method is responsible for closing.

But won't the tree in the ResourceAlias be incorrect? I don't think it will get updated.

I think you're right, and that probably means this approach is flawed. I don't think this breaks soundness (only error reporting), but it probably means we should go another way.

I worry that by allowing arbitrary JavaExpressions here we might be setting ourselves up for confusion later

The more I've thought about this, the more I've felt that this is what we should've done all along. The restriction that resource aliases must be local variables seems arbitrary; it's a bit of a hack to begin with that formal parameters are represented as locals, for example, but without that we would've already needed to switch to JavaExpression.

I think it depends on what we want our invariants to be. If we want an invariant that if an Obligation gets propagated to a particular program point, then all contained resource aliases must reference the same resource at that program point, it is much easier to maintain the invariant if we only track locals. Once you start tracking fields, you have to worry about updates through an alias. E.g., here is a (contrived) variant of my previous example:

I think I understand your point about local variables and aliasing, and I hadn't considered anything like the example you gave. That's a further reason to take a different approach.

As an alternative, we could leave this type as LocalVariable and then add extra logic to create a temp variable for the field at the beginning of the method and to handle it specially in other places. But that's more code and possibly more clutter in the implementation.

I considered this approach and discarded it in favor of the one you see in this PR because I worried that this would lead to more clutter.

Yes, I agree this may be more cluttered. I am wondering if we can just document very carefully what the current code is doing and just get away with that.

Given the two problems above, this approach might be worth taking. Other than what's needed to create the temporaries, what else will end up cluttered? We'll need logic to avoid discharging this kind of obligation by assigning to owning fields, certainly (but we would've needed that anyway). Anything else?

Another alternative (that you suggested earlier) would be to try to do this check elsewhere, such as in ResourceLeakVisitor. It might be worth exploring that alternative in more detail, too, because it might be simpler: when verifying the @EnsuresCalledMethods annotation on a destructor, use the stronger semantics.

One thing that your comment about soundness made me realize is that I think there might still be a soundness hole in this approach: we treat fields that a destructor must close just like any other resource, which means that their obligations can be fulfilled by assigning them to owning fields. That would be circular, and we should forbid it.

Yes, that's interesting. I am honestly not sure what our code would do in that situation; definitely something to be tested.

I wrote a test case and pushed it here.

[msridhar]

Another alternative (that you suggested earlier) would be to try to do this check elsewhere, such as in ResourceLeakVisitor. It might be worth exploring that alternative in more detail, too, because it might be simpler: when verifying the @EnsuresCalledMethods annotation on a destructor, use the stronger semantics.

My feeling is this is the right thing to explore next. If there is an API to get the exceptional exit store from the Called Methods Checker, we could just use the inferred @CalledMethods types in that store to do our additional consistency checking. If we expose the method performing the actual consistency check from the consistency analyzer, this might be only a small amount of code.

[kelloggm]

I tried this, and unfortunately at least my first draft isn't working. There is a method to get the exceptional exit store of a method in GenericAnnotatedTypeFactory, but it doesn't appear to work - the store it produces for the Called Methods Checker always has top for every value. It has no (other) clients - i.e., it's currently not used by any other checkers - so I suspect it is buggy. I'll try to dig a little further, but I'm not optimistic.

[msridhar]

Hrm, ok, I would expect it to be not that hard to fix? Also, if you can get ahold of the ControlFlowGraph for the method, it has a getExceptionalExitBlock() method, so we could combine that with getStoreBefore() hopefully to get what we want? I'm surprised the GenericAnnotatedTypeFactory method doesn't work, the code looks pretty simple.

[kelloggm]

Yeah, I'm stumped on what's wrong with the GenericAnnotatedTypeFactory method. It returns a store, but the store just isn't what I expected. There are a few examples in our test suite where the produced store doesn't have top for every value, but for almost every one of our tests that has a destructor, the relevant information isn't in the exceptional exit store.

If you want to take a look, I've pushed what I wrote onto the rlc-twoclose-soundness-2 branch in my fork: https://github.com/kelloggm/checker-framework/tree/rlc-twoclose-soundness-2 (sorry that there are a couple of unrelated changes in that branch; it came off of this one). If you run ./gradlew ResourceLeakTest you can see that the new destructor.exceptional.postcondition errors:

    CheckFields.java:68: error: (destructor.exceptional.postcondition)
    CheckFields.java:162: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:38: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:56: error: (destructor.exceptional.postcondition)
    CreatesMustCallForTargets.java:67: error: (destructor.exceptional.postcondition)
    MCAOwningField.java:21: error: (destructor.exceptional.postcondition)
    ManualMustCallEmptyOnConstructor.java:20: error: (destructor.exceptional.postcondition)
    MultipleMethodParamsMustCallAliasTest.java:84: error: (destructor.exceptional.postcondition)
    MustCallAliasImpl.java:20: error: (destructor.exceptional.postcondition)
    MustCallAliasImplWrong1.java:22: error: (destructor.exceptional.postcondition)
    MustCallAliasOwningField.java:20: error: (destructor.exceptional.postcondition)
    NonFinalFieldOnlyOverwrittenIfNull.java:75: error: (destructor.exceptional.postcondition)
    NonFinalFieldOnlyOverwrittenIfNull2.java:52: error: (destructor.exceptional.postcondition)
    ReplicaInputStreams.java:24: error: (destructor.exceptional.postcondition)
    :-1: other: error: unexpected receiver of field assignment: (this).other of type class org.checkerframework.dataflow.cfg.node.FieldAccessNode
    RequiresCalledMethodsTest.java:45: error: (destructor.exceptional.postcondition)
    SocketContainer.java:24: error: (destructor.exceptional.postcondition)
    SocketContainer2.java:20: error: (destructor.exceptional.postcondition)
    SocketContainer3.java:17: error: (destructor.exceptional.postcondition)
    SocketField.java:62: error: (destructor.exceptional.postcondition)
    TwoResourcesECM.java:23: error: (destructor.exceptional.postcondition)
    3 expected diagnostics were not found:
    ReplicaInputStreams.java:24: error: required.method.not.called
    ReplicaInputStreamsCircularReasoning.java:32: error: required.method.not.called
    TwoResourcesECM.java:23: error: required.method.not.called

(Though not all of those errors are wrong per se - e.g. the one in TwoResourcesECM is fine, the expected error just needs to be changed. But the point here is that lots of code that should be verifiable isn't.)

[kelloggm]

#4867 removes almost all of the errors I reported above, resulting in this output:

    4 unexpected diagnostics were found
    CheckFields.java:68: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:38: error: (destructor.exceptional.postcondition)
    CreatesMustCallForOverride2.java:56: error: (destructor.exceptional.postcondition)
    MultipleMethodParamsMustCallAliasTest.java:82: error: (destructor.exceptional.postcondition)

Looking at the error messages for these, they look as if they were caused by a bug in my new code; e.g. consider this one from CheckFields.java:

checker/tests/resourceleak/CheckFields.java:68: error: [destructor.exceptional.postcondition] Method b must resolve the must-call obligations of the owning field this.owningFoo along all paths, including exceptional paths. On an exceptional path, the @EnsuresCalledMethods annotation was not satisfied.
    void b() {
         ^
  Found:    null
  Required: @CalledMethods("a")

The "found: null" suggests to me that there's still a bug in my implementation.

In any event, I'm going to close this PR in favor of eventually opening one based on that branch.