Invariant with diagnostics #2906
Conversation
hannes-steffenhagen-diffblue
requested review from
peterschrammel and
danpoe
hannes-steffenhagen-diffblue
requested review from
kroening,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 702ab09).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
|
@peterschrammel and @danpoe, please could you take a quick look at this and see if it does what you want? |
src/util/invariant.h
Outdated
| #define CBMC_NORETURN [[noreturn]] | ||
| #else | ||
| #define CBMC_NORETURN | ||
| #endif | ||
| // The macros MACRO<n> (e.g., INVARIANT2) are for internal use in this file | ||
| // only. The corresponding macros that take a variable number of arguments (see | ||
| // further below) should be used instead, which in turn call those with a fixed |
There was a problem hiding this comment.
These comments can be removed, and the lines following right after that still contain the macros INVARIANT3, etc. should be adapted to the new macros.
src/util/invariant.h
Outdated
| std::ostringstream out; | ||
| out << "[ " << diagnostic_as_string(std::forward<T>(first)); | ||
| write_rest_diagnostics(out, std::forward<Ts>(rest)...); | ||
| out << " ]"; |
There was a problem hiding this comment.
Can we separate the diagnostics by newlines? Some of them are expected to go over several lines (like expr.pretty()).
There was a problem hiding this comment.
Good point, I'd still want to bracket them somehow - how about
<< EXTRA DIAGNOSTICS >>
D1
D2
...
DN
<< END EXTRA DIAGNOSTICS>>
?
src/util/source_location.h
Outdated
| static std::string | ||
| diagnostics_as_string(const source_locationt &source_location) | ||
| { | ||
| return source_location.as_string(); |
There was a problem hiding this comment.
Maybe we can add a heading too, like "source location:\n" + source_location.as_string().
| template <> | ||
| struct diagnostics_helpert<dstringt> | ||
| { | ||
| static std::string diagnostics_as_string(const dstringt &dstring) |
There was a problem hiding this comment.
I'm considering making this a function that takes a std::ostream& and writes some string representation of its argument there rather than returning string. Thoughts?
There was a problem hiding this comment.
We can leave this for future work I'd say :)
hannes-steffenhagen-diffblue
force-pushed
the
invariant-with-diagnostics
branch
from
0557549 to
a1595ac
Compare
src/util/invariant.h
Outdated
| // only. The corresponding macros that take a variable number of arguments (see | ||
| // further below) should be used instead, which in turn call those with a fixed | ||
| // number of arguments. For example, if INVARIANT(...) is called with two | ||
| // arguments, it calls INVARIANT2(). | ||
|
|
||
| #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) |
There was a problem hiding this comment.
In the following we should also add the new macro INVARIANT_WITH_DIAGNOSTICS, etc. and remove the macros INVARIANT3, etc.
There was a problem hiding this comment.
Done, thanks!
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 0557549).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84023225
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 0557549).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84023225
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a1595ac).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84026701
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 4082396).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84033439
hannes-steffenhagen-diffblue
changed the title
Framework for putting arbitrary diagnostics on invariants.
Ideally, we should never need this because of course saying something is
INVARIANTmeans we're pretty sure it's always true, but we get the situation that we do unexpected violate an invariant sometimes and in that case we want to give at least a hint of where we went wrong to make it easier for people to create small reproducers.This is similar to a previous PR which added some ways to add things like source locations onto invariants, this is meant to be more general in case we need to add new kinds of diagnostics or new ways to output them (e.g. as XML or JSON instead of plain text). It doesn't do that right now though.