Catch and log invariant errors when cbmc_invariants_should_throwt is enabled

[jeannielynnmoulton]

If cbmc_invariants_should_throwt is enabled, then invariants become
exceptions, and we should log them instead of putting them into the catch
all with no information.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[martin-cs]

This patch is an improvement but I think this shows a weakness of cbmc_invariants_should_throwt. There are two reasons the original invariant design did not throw exceptions:

1. The design of CPROVER and the intended use of invariants mean that invariant failures are non-recoverable. You should stop immediately and print out an error -- which is exactly what the default implementation does.

2. If it throws an exception people think they can be clever and catch it and then they wind up hiding errors. There have been a number of incidence of this. This patch removes a place it can happen and that is good. The way to remove all places it can happen is to not throw an exception on invariant failure.

[hannes-steffenhagen-diffblue]

@martin-cs Invariant failures are usually unrecoverable, but most of them aren’t fatal. Having invariants throw is useful for unit testing (where you can mark a test as failing instead of having to comment it out entirely, because otherwise abort aborts the entire test suite) and for providing additional diagnostic information on invariant failure (which may not be local to the point where the invariant failure actually occurs). I agree that during normal operation abort is a sensible default, but there are genuine reasons why you might not want that to happen.

Code that blanket catches exceptions (other than to log information and rethrow or abort) ideally shouldn’t pass code review.

[martin-cs]

On Mon, 2020-02-10 at 06:15 -0800, hannes-steffenhagen-diffblue wrote: @martin-cs Invariant failures are usually unrecoverable, but most of them aren’t fatal. Having invariants throw is useful for unit testing (where you can mark a test as failing instead of having to comment it out entirely, because otherwise `abort` aborts the entire test suite) and for providing additional diagnostic information on invariant failure (which may not be local to the point where the invariant failure actually occurs). I agree that during normal operation `abort` is a sensible default, but there are genuine reasons why you might not want that to happen.

I strongly disagree. An invariant failure means that something beyond the anticipation of the programmers is wrong and you should hard abort. It is evidence against any of the results being trustworthy and I would not make any use of them. I think having invariant failure handled with throw is unsafe because it encourages people to think it is safe to continue. But ... it's your application, it's your use case and it's your life. Do what works for you. Thanks to @jeannielynnmoulton for making things a bit safer.