Add @EnsuresCalledMethodsOnException

[Calvin-L]

Fixes #6204 and adds a useful feature to the Called Methods Checker.

See also this comment.

Motivation

It is very common for resource-handling code to close owned resources even on exceptional return. The existing annotations like @EnsuresCalledMethods and @Owning only describe what happens on normal return, and there is no way to write a stronger contract that says a method always closes a resource. (As far as I know, this limitation is common to all post-condition annotations in the Checker Framework.)

This PR adds @EnsuresCalledMethodsOnException, a new post-condition annotation that says what the method guarantees when it throws (subclasses of) java.lang.Exception.

Why a new annotation instead of strengthening @EnsuresCalledMethods?

I added an example in the manual for when you might want @EnsuresCalledMethodsOnException without promising @EnsuresCalledMethods. In short, the new annotation interacts well with @Owning, enabling users to write a contract that says "this method either takes ownership of the resource or closes it immediately and throws an exception".

Why only for Exception and not all Throwables?

I believe it is essentially impossible to guarantee no resource leaks in the presence of runtime errors: if socket.close() throws StackOverflowError, what can you possibly do?

We should discuss whether limiting @EnsuresCalledMethodsOnException to only Exception is right or not. There might be a good reason to generalize to all Throwables, or to have some complex set of exceptions like "all subclasses of Throwable except these specific subclases of Error".

Modified handling for destructors

The Resource Leak Checker requires a stronger contract for "destructor-like" methods. They must close their resources even when they throw an exception. Previously, that was accomplished with a special-case check. Now it can be accomplished in terms of the new annotation.

To avoid a breaking change, I have made @EnsuresCalledMethods imply an identical @EnsuresCalledMethodsOnException when it appears on a destructor. In my opinion this is just as hacky as the previous approach, but it ensures backwards compatibility while unifying some related code. This is the change that fixes #6204, since callers of destructors now benefit from the implied exceptional post-condition.

Misc notes

We should discuss if the name @EnsuresCalledMethodsOnException is good or not. I don't know if there is a precedent for this kind of annotation.

In the future, we might want to add framework support for this kind of post-condition annotation, like how @EnsuresCalledMethods is mostly handled by existing machinery.

Originally I had hoped to have this done by the November release, but it took a while to put together. We should take the time to review it carefully, and I'll look forward to using it in December. :)

[kelloggm]

Overall this looks like a great change! There are definitely some things I'm concerned about, but most of those are #6276, which this PR didn't introduce (just brought to my attention).

I'd like to have a syntactic sugar for the common case on destructors where both @EnsuresCalledMethods and @EnsuresCalledMethodsOnException are desirable. I'm not sure that needs to block landing this PR, though - we can add it in a follow-up change.

Other than that, my comments are mostly minor. @msridhar should probably take a look next.

[kelloggm]

If a user wants to write a method that guarantees that some methods are called on both the normal and exceptional exit paths, they'd need to write both @EnsuresCalledMethods and @EnsuresCalledMethodsOnException annotations. I don't think this is a good user experience: it would be better to have a single annotation for "ensures some methods are called on all exit paths" that logically means both normal and exceptional exits. I'd call such an annotation @EnsuresCalledMethodsOnAllPaths or something similar, I think.

This PR doesn't need to implement it, but it's probably something that we should consider. This is also the semantics of destructors exactly, so we know that there is a use case for it.

[msridhar]

Agreed that we need such an annotation and that we can do it in a follow-up to this PR. I would strongly prefer to have at least an alias for the annotation that has fewer characters to type than @EnsuresCalledMethodsOnAllPaths; maybe @AlwaysCalls? But we can discuss that as part of the follow-up.

[kelloggm]

LGTM, other than #6276. This PR doesn't make that worse, so I think it can be landed as-is. @msridhar needs to review this first, though.

[msridhar]

Overall, looks great! Just a few minor comments

[msridhar]

Agreed that we need such an annotation and that we can do it in a follow-up to this PR. I would strongly prefer to have at least an alias for the annotation that has fewer characters to type than @EnsuresCalledMethodsOnAllPaths; maybe @AlwaysCalls? But we can discuss that as part of the follow-up.

[msridhar]

Thanks for all the fixes, looks great!