Description
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-failand set up the failure mode - otherwise,malloc-may-failon 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.