Resource Leak Checker: Verify @EnsuresCalledMethods calling @Owning even on exceptional paths

[msridhar]

After #5733, I would expect this code to pass the Resource Leak Checker:

@InheritableMustCall("dispose")
public class OwningEnsuresCalledMethods {

  @Owning Socket con;

  @EnsuresCalledMethods(value = "this.con", methods = "close")
  void dispose() throws IOException {
    closeCon(con);
  }

  static void closeCon(@Owning Socket con) throws IOException {
      con.close();
  }
}

The reason is that @Owning guarantees the @MustCall method is invoked on all paths, including exceptional paths, and the Called Methods Checker code should be propagating called methods along both normal and exceptional paths. But, we still get a destructor.exceptional.postcondition for the dispose() method above. We should investigate.

[msridhar]

@Calvin-L am I right that in light of the changes in #6241, the checker is behaving correctly for the example above in reporting a warning? I think to get the test case to pass, we need to write:

@InheritableMustCall("dispose")
public class OwningEnsuresCalledMethods {

  @Owning Socket con;

  @EnsuresCalledMethods(value = "this.con", methods = "close")
  void dispose() throws IOException {
    closeCon(con);
  }

  @EnsuresCalledMethods(value = "#1", methods = "close")
  static void closeCon(Socket con) throws IOException {
      con.close();
  }
}

UPDATE: actually, no, the above test case should not pass the type checker either, since typically @EnsuresCalledMethods only makes guarantees for the normal exit. Is there any way now to get this test case to pass without catching the IOException in dispose() and calling this.con.close()?

[Calvin-L]

There are two ways to get that test case to pass:

• The way you suggested (catch the exception in dispose())
• Change closeCon so it does not throw IOException --- the RLC assumes that Throwble/Error/RuntimeException cannot happen, so the @EnsuresCalledMethods annotation is now sufficient.

Although, I have a secret plan for this use case (and by extension, surprisingly, #6204):

Add a new annotation (or an option to @EnsuresCalledMethods) indicating that the method calls some methods even on exception.

See tentative commits:

• Calvin-L@6a42b77
• Calvin-L@020aded

[msridhar]

@Calvin-L looks very promising. It would be a breaking change, and we'd have to discuss naming, but I am in favor of the approach suggested by your tentative commits.

[kelloggm]

I agree with @msridhar that this is a good idea, and I'm in favor of a change along these lines.

[msridhar]

The checker now behaves as expected for this example, in light of #6241 and #6271, so closing