Verifast & Java's "finally" clause

[Bob Rubbens]

Hey everyone,

Verifast's support for Java exceptions seems very solid. However it does not seem to support the "finally" clause. Am I using an outdated version of Verifast or is there a technical reason for this? I could not get it to work on the nightly release from the Github repo.

Kind regards,
Bob Rubbens

[Bart Jacobs]

Hi Bob,

Indeed, VeriFast does not yet support the "finally" clause. It is not clear to me what would be a good separation logic proof rule for it. In fact, I don't think it's easy to use "finally" clauses in a provably safe way. I would go so far as to claim that most code out there that uses finally clauses is probably not provably correct :-)

The problem is that the code in a finally clause is executed even if a really nasty exception occurred, such as OutOfMemoryError or StackOverflowError, or (even nastier) InternalError, which could occur at literally any point in the try block (and at any point during methods called directly or indirectly from the try block). So there is very little that it can assume about the program state on entry to the finally block.

(See also my work on Failboxes, a proposal for extending Java-like languages to support safe exception handling.)

Actually, a simple proof rule that would be sound (which is exactly what I am using for catch blocks) is to verify the finally block under an empty symbolic heap. That is, any resources owned by the stack frames that have been unwound by the exception are lost. This is not as bad as it sounds, since resources owned by the caller of the method containing the try-finally block would still be available.

(One could refine this proof rule by allowing the user to associate a "try invariant" with a try-catch/finally block. The resources described by the try invariant would be consumed on entry to the try block, and would be produced on entry to the catch or finally block.)

Usually, a finally block "cleans up" some resource used by the try block. To verify such a code pattern (without additional VeriFast extensions), the resource would have to be put in a "shared region" and accessed through atomic machine instructions. This would allow the try block and the try invariant to "share" the resource, as if they were concurrent threads.

Of course, using atomic machine instructions to access resources "shared" between a try block and a catch/finally block is overkill; the accesses need not be concurrency-atomic, they need only be exception-atomic. You'd need to come up with some proof rules for reasoning about exception-atomicity.

BTW: Come to think of it, one could work around the lack of "finally" support in the current version of VeriFast by encoding try-finally using try-catch. (This is always possible; in fact, Java compilers compile try-finally into try-catch.)

Best regards,
Bart

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/0f19b626-316a-43ad-b444-54ed0c2a3b76%40googlegroups.com.

[Bob Rubbens]

Thank you Bart for your detailed answer, this clears it up for me. From this point of view it indeed seems that Java cannot handle this besides a "best effort" attempt.

To unsubscribe from this group and stop receiving emails from it, send an email to veri...@googlegroups.com.