Enable default analysis flags for CBMC version 6.0+ #8093

NlightNFotis · 2023-12-05T10:33:58Z

This is a cleaned up version of #8006.

There are two difference over the previous PR:

Primary difference is setting up the --no-standard-checks flag in all of the regression test runners, instead of adjusting flags on each failing test. The reason we need to adjust flags to begin with is that a lot of tests are checking for number of properties or specific labels in the output, which, now that we enable a lot more properties by default, have been invalidated.
Presents a cleaner change into cbmc_parse_options and goto_check_c. Previous version rejected a flag that was on by default, such as --pointer-check, this version silently ignores it.

Still to-do:

Add new flag to goto-analyzer as well.
Add documentation for new flags and behaviour.

TGWDB · 2023-12-05T11:08:37Z

src/ansi-c/goto_check_c.h

-  "(assert-to-assume)"
+  "(assert-to-assume)"                                                         \
+  "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
+  "(no-pointer-primitive-check)(no-undefined-shift-check)"


Missing "no-div-by-zero-check?

Yeah, this was missed. I've added it now.

TGWDB · 2023-12-05T11:12:11Z

src/cbmc/cbmc_parse_options.cpp

+  options.set_option("bounds-check", true);
+  options.set_option("pointer-check", true);
+  options.set_option("pointer-primitive-check", true);
+  options.set_option("div-by-zero-check", true);
+  options.set_option("signed-overflow-check", true);
+  options.set_option("undefined-shift-check", true);


Aren't all of these then re-set later depending on the [no-]standard-checks option?

This code is called depending on whether the no-standard-checks is set.

Aren't they called on both line 140 and line 337?

Ah, I see what you mean now. Yeah, that has been eliminated now :) Good catch, it was an artefact of a previous design that set the default options unconditionally, and then if the --no-standard-checks flag was present it was just overriding it.

Now we've moved to a design that sets or doesn't set based on the flag being present.

TGWDB · 2023-12-05T11:12:42Z

src/cbmc/cbmc_parse_options.cpp

+
+  // Unwinding assertions required in certain cases for sound verification
+  // results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
+  options.set_option("unwinding-assertions", true);


Line 144 below now needs to handle this being set on be default. Maybe also line 287?

thomasspriggs

The handling of the malloc checks looks wrong. This is the main blocking comment which needs to be addressed.

My overarching remaining nitpick is that perhaps everything carried out by your duplicated set_default_analysis_flags functions should actually be done elsewhere. If you move all the functionality out of the functions, they will be unneeded and then duplication can be resolved by removing them.

thomasspriggs · 2023-12-06T16:35:50Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -56,6 +56,25 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
 {
 }

+void goto_analyzer_parse_optionst::set_default_analysis_flags(optionst &options)
+{
+  // Checks enabled by default in v6.0+.


The code in goto_analyzer_parse_optionst::set_default_analysis_flags and cbmc_parse_optionst::set_default_analysis_flags is duplicated. This is is a potential maintenance issue, to keep them synchronised.

This should stay as it is, because these two functions may be equivalent in form, but they represent different knowledge - the default configuration of two tools that are functionally different (one is a model checker and the other is an abstract interpreter), which only incidentally happens to be similar now, and could very well develop independently in the future.

thomasspriggs · 2023-12-06T16:38:23Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

+  options.set_option("pointer-primitive-check", true);
+  options.set_option("div-by-zero-check", true);
+  options.set_option("signed-overflow-check", true);
+  options.set_option("undefined-shift-check", true);


As per @TGWDB comment, the options in the PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS macro don't need to be in this function. This is because the macro sets the options after this function is called and it will set the value of the option regardless of whether it needs to be true or false.

The PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS's main functional aim is to be there to overwrite the flags in case they happen to be different (say, if a user is using default checks, but also --no-div-by-zero-check).

I agree that the end result is setting the flags to true twice, but I like that they are present in set_default_analysis_flags as documentation of the tool's default behaviour at the very least, and also without having to depend on flags being implicitly set to the default values by inverted logic in a different place in the code (goto_check_c.h).

thomasspriggs · 2023-12-06T17:17:02Z

src/cbmc/cbmc_parse_options.cpp

+
+  // Default malloc failure profile chosen to be returning null.
+  options.set_option("malloc-may-fail", true);
+  options.set_option("malloc-fail-null", true);


🚫 This doesn't look right. In develop the malloc-may-fail argument and the malloc-fail-null argument are never added to (or read from) the options. Therefore it appears to me that adding them to the options will have no effect. The command line arguments are read from cmdline and immediately used to setup configt::ansi_ct. See

cbmc/src/util/config.cpp

Line 1124 in 64fe4d0

if(cmdline.isset("malloc-fail-null"))

It might be worth considering implementing the default in the above location, in order to keep all the logic for the malloc checks in the same place.

Thank you for the catch!

I have attempted a fix in 71cda7c that I think should achieve the same end-goal but keep the code a bit cleaner. It achieves that by restricting the knowledge about the standard checks inside the cbmc_parse_optionst and goto_analyzer_parse_optionst. I think that changing the config.set function would distribute the knowledge about default flags (which for now is strictly a CBMC/goto-analyzer thing) into multiple places, making it harder to follow, and making the configuration (for other tools, as config.set is invoked in 30+ places) more convoluted without any direct correspondence to actual flags.

thomasspriggs · 2023-12-06T17:21:31Z

src/cbmc/cbmc_parse_options.cpp

+
+  // Unwinding assertions required in certain cases for sound verification
+  // results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
+  options.set_option("unwinding-assertions", true);


As goto_instrument can be used to perform unwinding, shouldn't this new default be applied in that entry point in that case?

Hm, I think in that case it probably wouldn't matter, because the analysis tools (the two main ones - cbmc and goto-analyzer) would add these, if I understand this correctly.

I need to play with this a bit and get back to you.

As unwinding is a transformation, rather than an analysis on its own right, I think this option needs to be set correctly for which ever entry point is performing the the transformation. My current assumption is that the unwinding assertions are added during the unwinding process. So the usual process flow is that the unwinding and the assertions would be done as part of the cbmc entry point. But if unwinding is performed on the goto-program before cbmc then the analysis won't go back and add the assertions which should have been added prior.

codecov · 2023-12-08T12:33:13Z

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (97ab133) 79.08% compared to head (9747f61) 79.09%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8093   +/-   ##
========================================
  Coverage    79.08%   79.09%           
========================================
  Files         1698     1698           
  Lines       196457   196485   +28     
========================================
+ Hits        155370   155401   +31     
+ Misses       41087    41084    -3

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

kroening · 2023-12-08T13:18:55Z

regression/contracts-dfcc/chain.sh

@@ -59,4 +59,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
  rm "${name}${dfcc_suffix}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
-$cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
+$cbmc --no-standard-checks "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}


Please don't do this. It will be very though for anyone to work out what the tests actually do execute when one fails.

Hi @kroening, just for clarification:

We were hoping to use this approach as a stop-gap to allow us to get the regression test suite in a way that is all-green again, so that we could merge this in time, seeing as this is the main ticket that's blocking a v6 release.

But the aim was to get this in temporarily, and as soon our v6 release is unblocked, reopen #8006, rebase it and then move to a model where the extra flag is being passed on an individual basis to tests (to localise the information about the test on the individual .desc file).

The original approach (of getting all the .desc readjusted) was found to be time consuming, and we wanted to at least unblock the release before we embark on that.

Is that something that works for you? If not, is there a particular proposal you had mind?

It's ok to use --no-standard-checks on most of the tests; my suggestion is to add it to the .desc file, where everyone will see it, instead of burying it inside a script.

I agree that the place for the --no-standard-checks flag is the .desc file of each failing test.
Unfortunately there are about 300 failing tests, so the idea was to avoid having a PR with code changes in the middle of 300 repetitive test fixes, but instead to temporarily add --no-standard-checks to the scripts to pass CI and them fix all the failing test on a subsequent PR aimed solely at fixing the regression tests.

@kroening I hope that this clarifies why the --no-standard-checks flag has been added on the runner script at the moment.

peterschrammel · 2023-12-11T10:24:40Z

💡 Since we have now combinations of flags that turn on and off checks, it would be great to output the list of actually active checks to the console.

…cript

…runner script

…on runner script

So that the defaults can be selectively overridden, whether they are initially on or off.

This allows for parsing the whole set of options regardless of whether the default is true or false. This then simplifies the usage of the macro as the separate option parsing no longer depends on if "no-standard-checks" is specified.

The `optionst` class essentially uses tri-state logic for booleans, where an option may be true, false or unset. `is_set` will return `true` for both the true and false options. Therefore we need `get_bool_option` to get the state of whether the option is set to true or false.

As the default is now to switch on the unwinding-assertions, we don't want a user to have to specify `--no-unwinding-assertions` in order to use `--cover`.

It will be handled in next PR.

thomasspriggs

I am approving as the malloc changes have been removed, for handling this separately.

peterschrammel

Approving to unblock the pre-release, given the promise that open requests come in a separate PR.

With additional checks turned on as of diffblue#8093, we failed CSmith tests with (legitimate) pointer property failures in `strcmp`. These are caused by trying to compare `argv[1]` to a string. As we do not model `argv` in these tests, `argv[1]` was not a valid pointer. This fix just removes the string comparison, which is only used for turning on/off debug output in test execution.

NlightNFotis added the Version 6 Pull requests and issues requiring a major version bump label Dec 5, 2023

NlightNFotis requested review from kroening, tautschnig, peterschrammel, thomasspriggs and remi-delmas-3000 as code owners December 5, 2023 10:33

NlightNFotis mentioned this pull request Dec 5, 2023

Enable default flags on for checks #8006

Closed

TGWDB reviewed Dec 5, 2023

View reviewed changes

NlightNFotis requested a review from martin-cs as a code owner December 6, 2023 12:04

NlightNFotis force-pushed the new_flags_on_clean branch from 43ebc37 to 2d7a5ee Compare December 6, 2023 12:18

thomasspriggs suggested changes Dec 6, 2023

View reviewed changes

kroening reviewed Dec 8, 2023

View reviewed changes

NlightNFotis force-pushed the new_flags_on_clean branch from 5992227 to cac6ead Compare December 12, 2023 16:14

NlightNFotis requested a review from jimgrundy as a code owner December 12, 2023 16:14

NlightNFotis force-pushed the new_flags_on_clean branch from cac6ead to 4fdab91 Compare December 12, 2023 16:32

thomasspriggs mentioned this pull request Dec 13, 2023

Use malloc fail null by default #8101

Merged

7 tasks

NlightNFotis force-pushed the new_flags_on_clean branch from 5ff9d49 to ea83bc9 Compare December 13, 2023 14:53

NlightNFotis added 11 commits December 13, 2023 15:54

Enable standard checks in CBMC

3cea665

Add --no-standard-checks to regression/cbmc runner scripts

457b953

Add --no-standard-checks to regression/cbmc-incr-smt2 runner scripts

4435c12

Add --no-standard-checks to regression/cbmc-shadow-memory runner scripts

8b54e10

Add --no-standard-checks to regression/cbmc-with-incr runner scripts

1d791d2

Add --no-standard-checks to regression/cbmc-primitives runner scripts

f277a9f

Add --no-standard-checks to regression/cbmc-library runner scripts

161321f

Add --no-standard-checks to regression/book-examples runner scripts

aaf2b8d

Add --no-standard-checks to regression/cbmc-concurrency runner scripts

d1cc469

Add --no-standard-checks to regression/cbmc-cover runner scripts

cf4269d

Add --no-standard-checks to regression/cbmc-cpp runner scripts

622440c

NlightNFotis and others added 17 commits December 13, 2023 15:54

Add --no-standard-checks to regression/acceleration test runner script

81c73d0

Add --no-standard-checks to regresion/contracts-dfcc test runner script

bc9ae9b

Add --no-standard-checks to regression/contracts test runner script

b90ea03

Add --no-standard-checks to regression/goto-synthesiser test runner s…

7d65934

…cript

Add --no-standard-checks to regression/goto-harness test runner script

0d19437

Add --no-standard-checks to ../regression/linking-goto-binaries test …

1f81854

…runner script

Add --no-standard-checks to regression/validate-trace-xml-schema pyth…

bda5ed3

…on runner script

Add documentation for new options in goto_check_c.h

13a6e0b

Add new flags to CBMC man page

a485f70

Set the default checks status for both defaults on and off

9b52a38

So that the defaults can be selectively overridden, whether they are initially on or off.

Combine NEGATIVE and POSITIVE check macros

1575958

This allows for parsing the whole set of options regardless of whether the default is true or false. This then simplifies the usage of the macro as the separate option parsing no longer depends on if "no-standard-checks" is specified.

When --cover is used switch off unwinding-assertions

64a7e54

As the default is now to switch on the unwinding-assertions, we don't want a user to have to specify `--no-unwinding-assertions` in order to use `--cover`.

Add standard checks to goto-analyzer's man page

07ab70e

Remove handling of malloc-may-fail.

7838ad8

It will be handled in next PR.

Don't expect goto-check negative checks for goto-diff manpage.

3ec5bfd

Add negative default checks to ignore list of goto-instrument as well

9747f61

NlightNFotis force-pushed the new_flags_on_clean branch from ea83bc9 to 9747f61 Compare December 13, 2023 15:54

NlightNFotis requested a review from a team as a code owner December 13, 2023 15:54

thomasspriggs approved these changes Dec 13, 2023

View reviewed changes

peterschrammel approved these changes Dec 13, 2023

View reviewed changes

NlightNFotis merged commit 41af31c into diffblue:develop Dec 13, 2023

NlightNFotis deleted the new_flags_on_clean branch December 13, 2023 23:36

tautschnig mentioned this pull request Dec 14, 2023

Permit re-setting --object-bits #7858

Merged

4 tasks

tautschnig mentioned this pull request Dec 14, 2023

CSmith test script: avoid a need for argv modelling #8105

Merged

3 tasks

This was referenced Dec 14, 2023

Add support for a --no-unwinding-assertions flag #8109

Merged

Enable logging of default flags on tool invocation #8110

Closed

Run again tests with new default checks #8106

Merged

thomasspriggs mentioned this pull request Jan 5, 2024

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

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enable default analysis flags for CBMC version 6.0+ #8093

Enable default analysis flags for CBMC version 6.0+ #8093

NlightNFotis commented Dec 5, 2023 •

edited

Loading

TGWDB Dec 5, 2023

NlightNFotis Dec 5, 2023

TGWDB Dec 5, 2023

NlightNFotis Dec 5, 2023

TGWDB Dec 5, 2023

NlightNFotis Dec 6, 2023

TGWDB Dec 5, 2023

thomasspriggs left a comment

thomasspriggs Dec 6, 2023

NlightNFotis Dec 7, 2023

thomasspriggs Dec 6, 2023

NlightNFotis Dec 7, 2023 •

edited

Loading

thomasspriggs Dec 6, 2023

NlightNFotis Dec 7, 2023

thomasspriggs Dec 6, 2023

NlightNFotis Dec 7, 2023

thomasspriggs Dec 7, 2023

codecov bot commented Dec 8, 2023 •

edited

Loading

kroening Dec 8, 2023

NlightNFotis Dec 8, 2023

kroening Dec 8, 2023

esteffin Dec 8, 2023

peterschrammel commented Dec 11, 2023

thomasspriggs left a comment

peterschrammel left a comment

Enable default analysis flags for CBMC version 6.0+ #8093

Enable default analysis flags for CBMC version 6.0+ #8093

Conversation

NlightNFotis commented Dec 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomasspriggs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis Dec 7, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov bot commented Dec 8, 2023 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Dec 11, 2023

thomasspriggs left a comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

NlightNFotis commented Dec 5, 2023 •

edited

Loading

NlightNFotis Dec 7, 2023 •

edited

Loading

codecov bot commented Dec 8, 2023 •

edited

Loading