[RFC] New default flags enabled for more language-feature complete analysis

[NlightNFotis]

This is an RFC for some new default values for flags on an invocation of the cbmc, goto-analyser and jbmc binaries in version 6.0+ (#7743).

---

The reason this change is being put forward is so that a "plain" invocation of a tool (e.g. cbmc) is better aligned with the expectations of a non-expert user. That is, there's a need to get the tool closer to giving useful feedback on an invocation of cbmc file.c rather than the current situation, which would need several flags/(__CPROVER_assert || assert) statements in order to provide analysis results that are meaningful and not trivially concluded.

To that end, we have come up with a recommended set of program instrumentation options to be turned on by default in version 6.0 and beyond, for cbmc and goto-analyser (given the symmetry in their UI). We arrived at these through investigating the tool's internals, user reports and cross referencing with the C language standard. Some of these flags are guarding against catastrophic errors at runtime (program crashes) and others are guarding against program state compromises (through undefined behaviour, etc). The flags are:

• --bounds-check
• --pointer-check
• --pointer-primitive-check
• --malloc-may-fail
  • --malloc-fail-null
  • --malloc-fail-assert
  • (One of the above options is needed to be on by default as they accompany malloc-may-fail and set up the failure mode - otherwise, malloc-may-fail on by itself doesn't accomplish anything).
  • (There's an idea to collapse these flags into options passed into malloc-may-fail
• --div-by-zero-check
• --signed-overflow-check
• --undefined-shift-check
• --unwinding-assertions

The above checks would also be bundled into a new flag called --standard-checks, which would be on by default, which would transitively enable all of the checks above.

We understand that this new change would bundle up a number of checks to be performed on a per-invocation basis, and that a user might not want all of them, or want a refined set of checks performed. For this case, we are also proposing the addition of a --no-****-check flag for each of the checks above, which would deactivate the check for that run. For example, even though --bounds-check would be on by default for every run, one could deactivate it by passing --no-bounds-check to a particular invocation of CBMC.

Combining the information from the last two paragraphs above, we are also going to provide a --no-standard-checks flag, whose behaviour would be functionally the opposite of the --standard-checks one, i.e. deactivating all of the checks that are now on by default. This would allow a user to either check only their assertions, or provide a more refined list of property checking flags on their own accord.

---

Aside from the above flags, there's a couple more that we would want to have enabled by default for cbmc and JBMC, and these are:

• --validate-ssa-equation, and
• --validate-goto-model

These shouldn't affect a user's analysis results, but they perform some needed integrity checks for the internals of our tools, validating the data model against expectations for every run. These would enable us to identify inconsistencies between the data model and the expectations across various tools, while minimising the impact on users, enabling us to identify and fix issues earlier in our development cycle.

[NlightNFotis]

Hello,

We're keen to proceed with implementation on this one, so I'm pinging here a few people who might be interested in this one:

@feliperodri @martin-cs @tautschnig @kroening @remi-delmas-3000 @peterschrammel

If we don't see any major disagreement here, we're going to proceed with implementation and raise a draft PR (to be linked here) as soon as we can so that people can look at a more concrete instance of the proposal.

[NlightNFotis]

Okay, we raised a PR to make the proposal a bit more concrete.

We imagine something like #8006 (with tests fixed, of course and then with the same change applied to goto-analyser).

[thomasspriggs]

I am going to close this out as it has been resolved via #8093 and other related PRs which are now merged.