replace assert()

[kroening]

The assert() macro has various issues, e.g., discussed here:

https://www.softwariness.com/articles/assertions-in-cpp/

We should follow the recommendation there and replace them with exceptions thrown.

[tautschnig]

The code base is surely not perfect in this regard, but isn't the current rule that assert() is used whenever there is an internal error, whereas exceptions are thrown when user-provided input is inconsistent?

For example, I don't see why exceptions would be appropriate in all the checks of std_expr.h.

[martin-cs]

Perhaps we could have a range of macros; UNREACHABLE, INTERNALINVARIANT, USERERROR, UNFINISHED, UNHANDLEDCASE, etc. with a string giving the explanation and then have the definitions expand to assert or throw. I tried to do this in the SMT-LIB2 back-end and I've seen it used to great effect in CVC4. I realise this is dangerously close to documentation but...

[peterschrammel]

I see the advantage of exceptions when the code is used as a library and I can't modify the source. In that case, I would like to catch internal errors of the library. But I would not like to see an InternalException inside CBMC caught without exiting.

I like Martin's proposal. It seems lightweight and well maintainable.

[tautschnig]

I have previously used the diagnostics library; fully using it would provide a lot of additional features, but I don't think taking this kind of (not particularly necessary) dependency is desirable. Its annotations could be used standalone - FShell has this: https://github.com/tautschnig/fshell/blob/master/fshell2/config/annotations.hpp

[NathanJPhillips]

After a code review I have just had to implement code with the following structure because of the aversion to throwing exceptions:

assert(ptr!=nullptr);
ptr->method();

When a user of my generic library class wrongly calls the function in release versions of the software (for efficient operation NDEBUG should be set in release versions to eliminate debug-only code) this will cause undefined behaviour (a segmentation fault if we're lucky). std::logic_error is specifically designed for situations like this. Please listen to Daniel's concerns and allow us to throw logic_error in situations like this.

[smowton]

How about introducing cbmc_assert whose behaviour is configurable at compile time-- for a standalone executable, it dies (and isn't disabled by NDEBUG); for a shared library build it throws?

[marek-trtik]

For consideration, here is C++ code I use in my project (it could be taken/adopted freely into our code base):

https://github.com/trtikm/E2/blob/master/code/utility/include/utility/invariants.hpp
https://github.com/trtikm/E2/blob/master/code/utility/include/utility/assumptions.hpp
https://github.com/trtikm/E2/blob/master/code/utility/include/utility/fail_message.hpp
https://github.com/trtikm/E2/blob/master/code/utility/src/fail_message.cpp

[NathanJPhillips]

Just seen more code where assert(false); is used followed by code that carries on as though it was now impossible to have taken the path that caused the assert.
This was in the code to parse Java. Better use of structured exceptions really is the correct way to handle this. If parsing a Java class causes a problem then that should be propagated up and reported at a level where the offending Java class name/file name can be reported. It may even be that in the future we try to continue with the remaining classes that can be loaded. Exiting forcefully in the guts of type parsing will never help us find and fix these issues once our software is being run outside our development environment.
This issue really needs progressing and instructions to use a better solution need to be disseminated to the team quickly to avoid more code like this being created.

[reuk]

I agree with Nathan. assert should only ever be used to document provable truths about the state of the code, and we should never fail an assert for any input, even ill-formed inputs. That is, we should use asserts in the same way that inputs to CBMC use asserts. Currently, there are a great number of inputs that @mgudemann found via fuzzing that would cause memory errors if we were to disable assertions (which should be done on release builds). It is not inconceivable that a user might enter ill-formed input, and in these cases, CBMC should always (in release and debug) have well-defined behaviour that doesn't involve dumping core.

Importantly, assert should never be used to validate preconditions on methods, because in these cases it is impossible to prove, within the scope of the method, that the assertion always holds true. Failing the assertion gives the caller no opportunity to recover, even though this behaviour is often desirable. However, assert is suitable for validating postconditions.

I think that UNREACHABLE, INTERNALINVARIANT, USERERROR, UNFINISHED, UNHANDLEDCASE macros will just make the code more unreadable, as assert(false) already means 'unreachable' and assert(condition) already means that 'condition' is an internal invariant. In the other cases (user error, unfinished, unhandled case) we probably do want to throw one of a family of exceptions so that we can return a unique error code, print formatted diagnostics and so on. In these cases, the type of the exception can encode whether the error was thrown because of bad input, unfinished code, or for some other reason.

On a related note, if we make any changes, the existing places where we throw things other than std::exceptions (like strings and ints) should be updated to throw types derived from std::exception too.

[martin-cs]

On Thu, 2017-04-20 at 03:13 -0700, Reuben Thomas wrote: I agree with Nathan. `assert` should only ever be used to document provable truths about the state of the code,

Although this might be pedantic, I'm not sure I would say "provable truths" but "things the programmer believes are provable truths".

and we should *never* fail an assert for any input, even ill-formed inputs.

Yes.

That is, we should use asserts in the same way that inputs to CBMC use asserts.

Yes. Once the C++ front-end is in better shape we should literally use them as they are used in CBMC.

Currently, there are a great number of inputs that @mgudemann found via fuzzing that would cause memory errors if we were to disable assertions (which should be done on release builds). It is not inconceivable that a user might enter ill-formed input, and in these cases, CBMC should always (in release and debug) have well-defined behaviour that doesn't involve dumping core.

It should definitely have a well-defined behaviour. Given an issue that has arisen recently, I don't think core dumps should be ruled out -- they can be very useful. Stack traces as well!

Importantly, `assert` should never be used to validate preconditions on methods, because in these cases it is impossible to prove, within the scope of the method, that the assertion always holds true.

They should not be used for validating inputs but they are valid for checking / documenting beliefs about how the code should be used. Restricting them to things that can be checked purely locally is too limiting.

Failing the assertion gives the caller no opportunity to recover, even though this behaviour is often desirable. However, `assert` *is* suitable for validating postconditions. I personally don't like the idea of `UNREACHABLE, INTERNALINVARIANT, USERERROR, UNFINISHED, UNHANDLEDCASE` macros, as `assert(false)` already means 'unreachable' and `assert(condition)` means that 'condition' is an internal invariant.

It's not a question of what they do but giving a way of documenting /why/ the condition is believed to hold. PRECONDITION and POSTCONDITION are other possible ideas.

In the other cases (user error, unfinished, unhandled case) we probably *do* want to throw one of a family of exceptions so that we can return a unique error code, print formatted diagnostics and so on.

I think we need to separate out how the conditions are written in the code and how they are handled. Handling depends very much on the context in which the program is being run / built.

On a related note, if we make any changes, the existing places where we throw things other than `std::exception`s (like strings and ints) should be updated to throw types derived from `std::exception` too.

Yes.

[martin-cs]

This has now become a customer facing issue ( @jgwilson42 can give more details but preferably not on a public bug tracker ) so we need to come to some kind of conclusion. My attempt at summarising the discussion so far (and requirements for the customer issue) :

A. We need a way of documenting things the programmer believes to be true about the code. Ideally this would include some record of /why/ they believe this. These should be true for all inputs and failure denotes an exceptional state.

B. What is done with these conditions should be in some way build time configurable. Options that are needed are:

B.1. Check the condition, if it fails, print a full stack trace and then dump the core.
B.2. Ignore the conditions completely.
B.3. Have them become / call assert() or __CPROVER_assert() so that we can use CPROVER tools to check them.

C. It is not yet clear which of the proposed solutions is the most appropriate.

Maybe @kroening @tautschnig or @peterschrammel can add a definitive statement here.