From 3cea665679d195505830231729d5249fc87a38f2 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:04:36 +0000 Subject: [PATCH 01/39] Enable standard checks in CBMC --- src/ansi-c/goto_check_c.h | 33 ++++++++++++++++----- src/cbmc/cbmc_parse_options.cpp | 51 +++++++++++++++++++++++++++++---- src/cbmc/cbmc_parse_options.h | 6 ++++ 3 files changed, 78 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 451bfa15c3c..c76eadff688 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -47,7 +47,10 @@ void goto_check_c( "(retain-trivial-checks)" \ "(error-label):" \ "(no-assertions)(no-assumptions)" \ - "(assert-to-assume)" + "(assert-to-assume)" \ + "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)" \ + "(no-pointer-primitive-check)(no-undefined-shift-check)" \ + "(no-div-by-zero-check)" #define HELP_GOTO_CHECK \ " {y--bounds-check} \t enable array bounds checks\n" \ @@ -77,23 +80,39 @@ void goto_check_c( " {y--no-assumptions} \t ignore user assumptions\n" \ " {y--assert-to-assume} \t convert user assertions to assumptions\n" +// clang-format off + #define PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options) \ + options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \ + options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \ + options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \ + options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + (void) 0; +// clang-format on + +// clang-format off + #define PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options) \ + options.set_option("bounds-check", cmdline.isset("bounds-check")); \ + options.set_option("pointer-check", cmdline.isset("pointer-check")); \ + options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ + options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + (void) 0; +// clang-format on + // clang-format off #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ - options.set_option("bounds-check", cmdline.isset("bounds-check")); \ - options.set_option("pointer-check", cmdline.isset("pointer-check")); \ options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \ options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \ - options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("conversion-check", cmdline.isset("conversion-check")); \ - options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("nan-check", cmdline.isset("nan-check")); \ options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial-checks", \ cmdline.isset("retain-trivial-checks")); \ options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e8579a519eb..2c4150a58fb 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -106,6 +106,25 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("depth", UINT32_MAX); } +void cbmc_parse_optionst::set_default_analysis_flags(optionst &options) +{ + // Checks enabled by default in v6.0+. + 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); + + // Default malloc failure profile chosen to be returning null. + options.set_option("malloc-may-fail", true); + options.set_option("malloc-fail-null", true); + + // 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); +} + void cbmc_parse_optionst::get_command_line_options(optionst &options) { if(config.set(cmdline)) @@ -120,7 +139,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); - if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions")) + if( + cmdline.isset("cover") && + // The option is set by default, or passed in the by the user. + (options.is_set("unwinding-assertions") || + cmdline.isset("unwinding-assertions"))) { log.error() << "--cover and --unwinding-assertions must not be given together" @@ -261,7 +284,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("unwind")) { options.set_option("unwind", cmdline.get_value("unwind")); - if(!cmdline.isset("unwinding-assertions")) + if( + !options.is_set("unwinding-assertions") && + !cmdline.isset("unwinding-assertions")) { log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " "sound verification results" @@ -288,7 +313,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) { options.set_option( "unwindset", cmdline.get_comma_separated_values("unwindset")); - if(!cmdline.isset("unwinding-assertions")) + if( + !options.is_set("unwinding-assertions") && + !cmdline.isset("unwinding-assertions")) { log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " "sound verification results" @@ -305,11 +332,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) "self-loops-to-assumptions", !cmdline.isset("no-self-loops-to-assumptions")); - // all checks supported by goto_check + // Enable flags that in combination provide analysis with no surprises + // (expected checks and no unsoundness by missing checks). + if(!cmdline.isset("no-standard-checks")) + { + cbmc_parse_optionst::set_default_analysis_flags(options); + PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); + } + else if(cmdline.isset("no-standard-checks")) + { + PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); + } + + // all (other) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // generate unwinding assertions - if(cmdline.isset("unwinding-assertions")) + if( + options.is_set("unwinding-assertions") || + cmdline.isset("unwinding-assertions")) { options.set_option("unwinding-assertions", true); options.set_option("paths-symex-explore-all", true); diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 8ec5b04ffaa..22ad39a663e 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -34,6 +34,7 @@ class optionst; // clang-format off #define CBMC_OPTIONS \ OPT_BMC \ + "(no-standard-checks)" \ "(preprocess)(slice-by-trace):" \ OPT_FUNCTIONS \ "(no-simplify)(full-slice)" \ @@ -91,6 +92,11 @@ class cbmc_parse_optionst : public parse_options_baset /// default behaviour, for example unit tests. static void set_default_options(optionst &); + /// \brief Setup default analysis flags. + /// + /// This function sets up the default analysis checks as discussed + /// in RFC https://github.com/diffblue/cbmc/issues/7975. + static void set_default_analysis_flags(optionst &); static bool process_goto_program(goto_modelt &, const optionst &, messaget &); static int get_goto_program( From 457b953e6b469040b8b9dd0bf29f9e024911d9d6 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:11:22 +0000 Subject: [PATCH 02/39] Add --no-standard-checks to regression/cbmc runner scripts --- regression/cbmc/CMakeLists.txt | 8 ++++---- regression/cbmc/Makefile | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index b0de5320280..96aca8cf05c 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -13,19 +13,19 @@ else() endif() add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} ) add_test_pl_profile( "cbmc-paths-lifo" - "$ --paths lifo" + "$ --no-standard-checks --paths lifo" "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}" "CORE" ) add_test_pl_profile( "cbmc-cprover-smt2" - "$ --cprover-smt2" + "$ --no-standard-checks --cprover-smt2" "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}" "CORE" ) @@ -33,7 +33,7 @@ add_test_pl_profile( # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it. add_test_pl_profile( "cbmc-new-smt-backend" - "$ --incremental-smt2-solver 'z3 --smt2 -in'" + "$ --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend" "CORE" ) diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile index e5777ce8774..969a26ca813 100644 --- a/regression/cbmc/Makefile +++ b/regression/cbmc/Makefile @@ -10,27 +10,27 @@ GCC_ONLY = endif test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY) test-cprover-smt2: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \ -X broken-smt-backend -X thorough-smt-backend \ -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \ -s cprover-smt2 $(GCC_ONLY) test-z3: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \ -X broken-smt-backend -X thorough-smt-backend \ -X broken-z3-smt-backend -X thorough-z3-smt-backend \ -s z3 $(GCC_ONLY) test-paths-lifo: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \ -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \ -s paths-lifo $(GCC_ONLY) test-new-smt-backend: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \ -X no-new-smt \ -s new-smt-backend $(GCC_ONLY) From 4435c12a6e4748b8fa085304982add0f9e817b0f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:12:31 +0000 Subject: [PATCH 03/39] Add --no-standard-checks to regression/cbmc-incr-smt2 runner scripts --- regression/cbmc-incr-smt2/CMakeLists.txt | 4 ++-- regression/cbmc-incr-smt2/Makefile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt index 2e8e54e434c..ddce0eab71b 100644 --- a/regression/cbmc-incr-smt2/CMakeLists.txt +++ b/regression/cbmc-incr-smt2/CMakeLists.txt @@ -1,13 +1,13 @@ add_test_pl_profile( "cbmc-incr-smt2-z3" - "$ --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" "-C;-s;new-smt-z3" "CORE" ) add_test_pl_profile( "cbmc-incr-smt2-cvc5" - "$ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" "-C;-s;new-smt-cvc5" "CORE" ) diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile index 9a5b8bf4195..f766292bc22 100644 --- a/regression/cbmc-incr-smt2/Makefile +++ b/regression/cbmc-incr-smt2/Makefile @@ -6,10 +6,10 @@ include ../../src/common test: test.z3 test.cvc5 test.z3: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" test.cvc5: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" tests.log: ../test.pl test From 8b54e1009f3dc35b5a4f7c6b48f88ee69d839fc5 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:14:25 +0000 Subject: [PATCH 04/39] Add --no-standard-checks to regression/cbmc-shadow-memory runner scripts --- regression/cbmc-shadow-memory/CMakeLists.txt | 2 +- regression/cbmc-shadow-memory/Makefile | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-shadow-memory/CMakeLists.txt b/regression/cbmc-shadow-memory/CMakeLists.txt index 93d5ee716c2..5e2a1847360 100644 --- a/regression/cbmc-shadow-memory/CMakeLists.txt +++ b/regression/cbmc-shadow-memory/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --no-standard-checks" ) diff --git a/regression/cbmc-shadow-memory/Makefile b/regression/cbmc-shadow-memory/Makefile index d86a43477e6..63237f82e69 100644 --- a/regression/cbmc-shadow-memory/Makefile +++ b/regression/cbmc-shadow-memory/Makefile @@ -1,13 +1,13 @@ default: tests.log test: - @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend + @../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks" -X smt-backend test-cprover-smt2: - @../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" + @../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" tests.log: ../test.pl - @../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend + @../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks" -X smt-backend show: @for dir in *; do \ From 1d791d29a71361a97143000b01b3de05472cfc83 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:15:29 +0000 Subject: [PATCH 05/39] Add --no-standard-checks to regression/cbmc-with-incr runner scripts --- regression/cbmc-with-incr/CMakeLists.txt | 2 +- regression/cbmc-with-incr/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-with-incr/CMakeLists.txt b/regression/cbmc-with-incr/CMakeLists.txt index da7f7e70da7..bf03c7249a2 100644 --- a/regression/cbmc-with-incr/CMakeLists.txt +++ b/regression/cbmc-with-incr/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$ --incremental" + "$ --no-standard-checks --incremental" ) diff --git a/regression/cbmc-with-incr/Makefile b/regression/cbmc-with-incr/Makefile index 1b69101ed35..ffb4f3b84d2 100644 --- a/regression/cbmc-with-incr/Makefile +++ b/regression/cbmc-with-incr/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -c "../../../src/cbmc/cbmc --incremental" + @../test.pl -c "../../../src/cbmc/cbmc --no-standard-checks --incremental" tests.log: ../test.pl - @../test.pl -c "../../../src/cbmc/cbmc --incremental" + @../test.pl -c "../../../src/cbmc/cbmc --no-standard-checks --incremental" clean: @$(RM) *.log From f277a9f98621efdec3978c10b76375c977e14656 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:17:17 +0000 Subject: [PATCH 06/39] Add --no-standard-checks to regression/cbmc-primitives runner scripts --- regression/cbmc-primitives/CMakeLists.txt | 6 +++--- regression/cbmc-primitives/Makefile | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/cbmc-primitives/CMakeLists.txt b/regression/cbmc-primitives/CMakeLists.txt index 331c1cd1fe2..f8cd4322355 100644 --- a/regression/cbmc-primitives/CMakeLists.txt +++ b/regression/cbmc-primitives/CMakeLists.txt @@ -2,18 +2,18 @@ find_program(Z3_EXISTS "z3") message(${Z3_EXISTS}) if(Z3_EXISTS) add_test_pl_tests( - "$" + "$ --no-standard-checks" ) # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it. add_test_pl_profile( "cbmc-primitives-new-smt-backend" - "$ --incremental-smt2-solver 'z3 --smt2 -in'" + "$ --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" "-X;no-new-smt;-s;new-smt-backend" "CORE" ) else() add_test_pl_tests( - "$" -X smt-backend + "$ --no-standard-checks" -X smt-backend ) endif() diff --git a/regression/cbmc-primitives/Makefile b/regression/cbmc-primitives/Makefile index e60c0d87ca5..2c9885222db 100644 --- a/regression/cbmc-primitives/Makefile +++ b/regression/cbmc-primitives/Makefile @@ -1,13 +1,13 @@ default: tests.log test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" test.smt2_incr: - @../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" + @../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" clean: find . -name '*.out' -execdir $(RM) '{}' \; From 161321fddd0d7e11427df86d9640a3d85ef58893 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:18:38 +0000 Subject: [PATCH 07/39] Add --no-standard-checks to regression/cbmc-library runner scripts --- regression/cbmc-library/CMakeLists.txt | 4 ++-- regression/cbmc-library/Makefile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-library/CMakeLists.txt b/regression/cbmc-library/CMakeLists.txt index f523261d1aa..9e76346fe05 100644 --- a/regression/cbmc-library/CMakeLists.txt +++ b/regression/cbmc-library/CMakeLists.txt @@ -1,11 +1,11 @@ if(NOT WIN32) add_test_pl_tests( - "$" + "$ --no-standard-checks" ) else() add_test_pl_profile( "cbmc-library" - "$" + "$ --no-standard-checks" "-C;-X;unix;-X;gcc-only" "CORE" ) diff --git a/regression/cbmc-library/Makefile b/regression/cbmc-library/Makefile index e82cb289424..3389cea12c8 100644 --- a/regression/cbmc-library/Makefile +++ b/regression/cbmc-library/Makefile @@ -9,10 +9,10 @@ ifeq ($(BUILD_ENV_),MSVC) endif test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" $(unix_only) $(gcc_only) tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" $(unix_only) $(gcc_only) clean: find . -name '*.out' -execdir $(RM) '{}' \; From aaf2b8d8837f674bd510fbe0d0b566b71b6bc2dc Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:20:30 +0000 Subject: [PATCH 08/39] Add --no-standard-checks to regression/book-examples runner scripts --- regression/book-examples/CMakeLists.txt | 8 ++++---- regression/book-examples/Makefile | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/regression/book-examples/CMakeLists.txt b/regression/book-examples/CMakeLists.txt index d61cfb85b92..88cf52769ec 100644 --- a/regression/book-examples/CMakeLists.txt +++ b/regression/book-examples/CMakeLists.txt @@ -13,19 +13,19 @@ else() endif() add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} ) add_test_pl_profile( "book-examples-paths-lifo" - "$ --paths lifo" + "$ --no-standard-checks --paths lifo" "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}" "CORE" ) add_test_pl_profile( "book-examples-cprover-smt2" - "$ --cprover-smt2" + "$ --no-standard-checks --cprover-smt2" "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}" "CORE" ) @@ -33,7 +33,7 @@ add_test_pl_profile( # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it. add_test_pl_profile( "book-examples-new-smt-backend" - "$ --incremental-smt2-solver 'z3 --smt2 -in'" + "$ --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend" "CORE" ) diff --git a/regression/book-examples/Makefile b/regression/book-examples/Makefile index e5777ce8774..969a26ca813 100644 --- a/regression/book-examples/Makefile +++ b/regression/book-examples/Makefile @@ -10,27 +10,27 @@ GCC_ONLY = endif test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY) test-cprover-smt2: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \ -X broken-smt-backend -X thorough-smt-backend \ -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \ -s cprover-smt2 $(GCC_ONLY) test-z3: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \ -X broken-smt-backend -X thorough-smt-backend \ -X broken-z3-smt-backend -X thorough-z3-smt-backend \ -s z3 $(GCC_ONLY) test-paths-lifo: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \ -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \ -s paths-lifo $(GCC_ONLY) test-new-smt-backend: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \ + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \ -X no-new-smt \ -s new-smt-backend $(GCC_ONLY) From d1cc4694ffe918c1c2df82f8174c3f94f33bab12 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:22:33 +0000 Subject: [PATCH 09/39] Add --no-standard-checks to regression/cbmc-concurrency runner scripts --- regression/cbmc-concurrency/CMakeLists.txt | 4 ++-- regression/cbmc-concurrency/Makefile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt index 2071288ffd8..f4a9787031e 100644 --- a/regression/cbmc-concurrency/CMakeLists.txt +++ b/regression/cbmc-concurrency/CMakeLists.txt @@ -1,11 +1,11 @@ if((NOT WIN32) AND (NOT APPLE)) add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" ) else() add_test_pl_profile( "cbmc-concurrency" - "$ --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" "-C;-X;pthread" "CORE" ) diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile index bd3ca1bdf60..2f8153fc7c3 100644 --- a/regression/cbmc-concurrency/Makefile +++ b/regression/cbmc-concurrency/Makefile @@ -10,10 +10,10 @@ ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),) endif test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread) tests.log: ../test.pl - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread) clean: find . -name '*.out' -execdir $(RM) '{}' \; From cf4269dafec31e3e30f12f857f755252f0e66c6b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:23:30 +0000 Subject: [PATCH 10/39] Add --no-standard-checks to regression/cbmc-cover runner scripts --- regression/cbmc-cover/CMakeLists.txt | 2 +- regression/cbmc-cover/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-cover/CMakeLists.txt b/regression/cbmc-cover/CMakeLists.txt index 93d5ee716c2..5e2a1847360 100644 --- a/regression/cbmc-cover/CMakeLists.txt +++ b/regression/cbmc-cover/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --no-standard-checks" ) diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile index 1a63894412b..82aa192b5ad 100644 --- a/regression/cbmc-cover/Makefile +++ b/regression/cbmc-cover/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" clean: find . -name '*.out' -execdir $(RM) '{}' \; From 622440ca21e7862b55535144f7c9b424314ba2d6 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:24:28 +0000 Subject: [PATCH 11/39] Add --no-standard-checks to regression/cbmc-cpp runner scripts --- regression/cbmc-cpp/CMakeLists.txt | 2 +- regression/cbmc-cpp/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt index 4d141f395e6..72ba751bca3 100644 --- a/regression/cbmc-cpp/CMakeLists.txt +++ b/regression/cbmc-cpp/CMakeLists.txt @@ -5,5 +5,5 @@ else() endif() add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" ${gcc_only} + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" ${gcc_only} ) diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile index b08769d4551..2ad6fbdcac6 100644 --- a/regression/cbmc-cpp/Makefile +++ b/regression/cbmc-cpp/Makefile @@ -8,10 +8,10 @@ ifeq ($(BUILD_ENV_),MSVC) endif test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests) tests.log: ../test.pl - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests) clean: find . -name '*.out' -execdir $(RM) '{}' \; From 014a33c54c6edea26ea298e615f1b0f519c41e44 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:25:24 +0000 Subject: [PATCH 12/39] Add --no-standard-checks to regression/cbmc-incr runner scripts --- regression/cbmc-incr/CMakeLists.txt | 2 +- regression/cbmc-incr/Makefile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-incr/CMakeLists.txt b/regression/cbmc-incr/CMakeLists.txt index aad62741a82..636afd1a7b6 100644 --- a/regression/cbmc-incr/CMakeLists.txt +++ b/regression/cbmc-incr/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "perl ../timeout.pl 30 $ --incremental --magic-numbers" + "perl ../timeout.pl 30 $ --no-standard-checks --incremental --magic-numbers" ) diff --git a/regression/cbmc-incr/Makefile b/regression/cbmc-incr/Makefile index 1de65b50102..5113fb4050b 100644 --- a/regression/cbmc-incr/Makefile +++ b/regression/cbmc-incr/Makefile @@ -1,6 +1,6 @@ default: tests.log -PARAM = --incremental --magic-numbers +PARAM = --incremental --magic-numbers --no-standard-checks # --refine --slice-formula test: From 2b6446e2994cf277e681f0e0ce870ace2ad7e87c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:26:40 +0000 Subject: [PATCH 13/39] Add --no-standard-checks to regression/cbmc-incr-oneloop test runner scripts --- regression/cbmc-incr-oneloop/CMakeLists.txt | 2 +- regression/cbmc-incr-oneloop/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-incr-oneloop/CMakeLists.txt b/regression/cbmc-incr-oneloop/CMakeLists.txt index 33d24bd6b3b..476a5d9f5d8 100644 --- a/regression/cbmc-incr-oneloop/CMakeLists.txt +++ b/regression/cbmc-incr-oneloop/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "perl ../timeout.pl 8 $ --slice-formula" + "perl ../timeout.pl 8 $ --no-standard-checks --slice-formula" ) diff --git a/regression/cbmc-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile index 35d25c57e2c..750ca5aca2a 100644 --- a/regression/cbmc-incr-oneloop/Makefile +++ b/regression/cbmc-incr-oneloop/Makefile @@ -2,10 +2,10 @@ default: tests.log # Note the `perl -e` serves the purpose of providing timeout test: - @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula" + @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula" tests.log: ../test.pl - @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula" + @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula" clean: @$(RM) *.log From f79b5bc9841f796bccb642df4107aef42e39524e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 5 Dec 2023 10:27:35 +0000 Subject: [PATCH 14/39] Add --no-standard-checks to regression/cbmc-sequentialization test runner scripts --- regression/cbmc-sequentialization/CMakeLists.txt | 4 ++-- regression/cbmc-sequentialization/Makefile | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-sequentialization/CMakeLists.txt b/regression/cbmc-sequentialization/CMakeLists.txt index 761fc6bca19..4d532a9d46e 100644 --- a/regression/cbmc-sequentialization/CMakeLists.txt +++ b/regression/cbmc-sequentialization/CMakeLists.txt @@ -1,10 +1,10 @@ if(NOT WIN32) add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" ) else() add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" + "$ --no-standard-checks --validate-goto-model --validate-ssa-equation" -X requires_posix_only_headers ) endif() diff --git a/regression/cbmc-sequentialization/Makefile b/regression/cbmc-sequentialization/Makefile index 672dac210bb..fa2c53859e2 100644 --- a/regression/cbmc-sequentialization/Makefile +++ b/regression/cbmc-sequentialization/Makefile @@ -10,7 +10,7 @@ POSIX_ONLY = endif test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY) tests.log: ../test.pl test From 5f43f5315a6042f66edcc529f13cf27232e8d78a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Dec 2023 11:12:02 +0000 Subject: [PATCH 15/39] Fix issue with non-null-terminated string in shadow-memory regression tests --- regression/cbmc-shadow-memory/strdup1/main.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/regression/cbmc-shadow-memory/strdup1/main.c b/regression/cbmc-shadow-memory/strdup1/main.c index b937b83bc97..fd23e37436c 100644 --- a/regression/cbmc-shadow-memory/strdup1/main.c +++ b/regression/cbmc-shadow-memory/strdup1/main.c @@ -8,6 +8,9 @@ int main() __CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0); char *s = (char *)malloc(3 * sizeof(char)); + // Terminate string so that `strdup` will not call `strlen` + // on a string without a null-terminator. + s[2] = '\0'; assert(__CPROVER_get_field(&s[0], "field1") == 0); assert(__CPROVER_get_field(&s[1], "field1") == 0); From 1f577e703e374a859d1f69ba8f2023fb039f5ccf Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Dec 2023 12:03:54 +0000 Subject: [PATCH 16/39] Add default options to goto-analyzer --- .../goto_analyzer_parse_options.cpp | 33 ++++++++++++++++++- .../goto_analyzer_parse_options.h | 6 +++- 2 files changed, 37 insertions(+), 2 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index b64119b6b9e..f35dc427446 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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+. + 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); + + // Default malloc failure profile chosen to be returning null. + options.set_option("malloc-may-fail", true); + options.set_option("malloc-fail-null", true); + + // This is in-line with the options we set for CBMC in cbmc_parse_optionst + // with the exception of unwinding-assertions, which don't make sense in + // the context of abstract interpretation. +} + void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) { if(config.set(cmdline)) @@ -67,7 +86,19 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); - // all checks supported by goto_check + // Enable flags that in combination provide analysis with no surprises + // (expected checks and no unsoundness by missing checks). + if(!cmdline.isset("no-standard-checks")) + { + goto_analyzer_parse_optionst::set_default_analysis_flags(options); + PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); + } + else if(cmdline.isset("no-standard-checks")) + { + PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); + } + + // all (other) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // The user should either select: diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index beda0d3a2d3..52c967a9135 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -109,7 +109,8 @@ class optionst; "(show)(verify)(simplify):" \ "(show-on-source)" \ "(unreachable-instructions)(unreachable-functions)" \ - "(reachable-functions)" + "(reachable-functions)" \ + "(no-standard-checks)" #define GOTO_ANALYSER_OPTIONS_AI \ "(recursive-interprocedural)" \ @@ -188,6 +189,9 @@ class goto_analyzer_parse_optionst: public parse_options_baset virtual bool process_goto_program(const optionst &options); virtual int perform_analysis(const optionst &options); + + // TODO: Add documentation + static void set_default_analysis_flags(optionst &options); }; #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H From ce65686d1c18b5bd2acc4504cd7f903b9d5568bd Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Dec 2023 12:08:09 +0000 Subject: [PATCH 17/39] Add --no-standard-checks to regression/goto-analyzer test runner scripts --- regression/goto-analyzer/CMakeLists.txt | 2 +- regression/goto-analyzer/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/goto-analyzer/CMakeLists.txt b/regression/goto-analyzer/CMakeLists.txt index 73af8689568..16978abe8a8 100644 --- a/regression/goto-analyzer/CMakeLists.txt +++ b/regression/goto-analyzer/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --no-standard-checks" ) diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile index 22e68590597..66fd99853f9 100644 --- a/regression/goto-analyzer/Makefile +++ b/regression/goto-analyzer/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer + @../test.pl -e -p -c "../../../src/goto-analyzer/goto-analyzer --no-standard-checks" tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer + @../test.pl -e -p -c "../../../src/goto-analyzer/goto-analyzer --no-standard-checks" clean: find . -name '*.out' -execdir $(RM) '{}' \; From 5f172967986ba5c289eeb53285ed2b5143ddc018 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Dec 2023 12:12:47 +0000 Subject: [PATCH 18/39] Add --no-standard-checks to goto-analyzer-simplify runner scripts --- regression/goto-analyzer-simplify/CMakeLists.txt | 2 +- regression/goto-analyzer-simplify/Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/goto-analyzer-simplify/CMakeLists.txt b/regression/goto-analyzer-simplify/CMakeLists.txt index d0e80bbd2bf..c77b87019d7 100644 --- a/regression/goto-analyzer-simplify/CMakeLists.txt +++ b/regression/goto-analyzer-simplify/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $" + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ --no-standard-checks" ) diff --git a/regression/goto-analyzer-simplify/Makefile b/regression/goto-analyzer-simplify/Makefile index 4f66d4159ea..7852dc3448c 100644 --- a/regression/goto-analyzer-simplify/Makefile +++ b/regression/goto-analyzer-simplify/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer" + @../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer --no-standard-checks" tests.log: ../test.pl - @../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer" + @../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer --no-standard-checks" clean: find . -name '*.out' -execdir $(RM) '{}' \; From 56e978352cf3921a519cf8c2ee7a92438a97f761 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Dec 2023 17:03:08 +0000 Subject: [PATCH 19/39] Add --no-standard-checks to regression/goto-instrument test runner --- regression/goto-instrument/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh index 2b4381ae918..ed4fdbedc9d 100755 --- a/regression/goto-instrument/chain.sh +++ b/regression/goto-instrument/chain.sh @@ -40,4 +40,4 @@ elif echo $args | grep -q -- "--dump-c" ; then rm "${target}-mod.c" fi $goto_instrument --show-goto-functions "${target}-mod.gb" -$cbmc "${target}-mod.gb" +$cbmc --no-standard-checks "${target}-mod.gb" From 8d70395e6387a3673cf6c1ac54617b9c627007bf Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 7 Dec 2023 14:49:05 +0000 Subject: [PATCH 20/39] Rework handling of `malloc-may-fail`. This was being handled in `config.set`, which correspondingly used the command line flags to check if the option should be set, skipping the `options` data structure alltogether, causing our `options.set_option` call for the `malloc-may-fail` and the `malloc-fail-null` to have no observable outcome. --- src/cbmc/cbmc_parse_options.cpp | 17 ++++++++++++++++- .../goto_analyzer_parse_options.cpp | 17 ++++++++++++++++- 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2c4150a58fb..838b02e76a2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -116,7 +116,9 @@ void cbmc_parse_optionst::set_default_analysis_flags(optionst &options) options.set_option("signed-overflow-check", true); options.set_option("undefined-shift-check", true); - // Default malloc failure profile chosen to be returning null. + // Default malloc failure profile chosen to be returning null. These options + // are not strictly needed, but they are staying here as part of documentation + // of the default option set for the tool. options.set_option("malloc-may-fail", true); options.set_option("malloc-fail-null", true); @@ -337,11 +339,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(!cmdline.isset("no-standard-checks")) { cbmc_parse_optionst::set_default_analysis_flags(options); + // The malloc failure mode is by default handled by the `config.set` call + // which only looks at the `cmdline` flags. In the case of default checks, + // these haven't been set - we need to overwrite the config object to manually + // bootstrap the malloc-may-fail behaviour + if(!config.ansi_c.malloc_may_fail && options.is_set("malloc-may-fail")) + { + config.ansi_c.malloc_may_fail = true; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; + } PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); } else if(cmdline.isset("no-standard-checks")) { PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); + // If the user opts for no standard checks, it's safe to assume he also + // wants to control the malloc failure behaviour, in which case we can + // also assume that it's going to be setup in the `config.set` call above. } // all (other) checks supported by goto_check diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f35dc427446..a5bb39aa5f3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -66,7 +66,9 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(optionst &options) options.set_option("signed-overflow-check", true); options.set_option("undefined-shift-check", true); - // Default malloc failure profile chosen to be returning null. + // Default malloc failure profile chosen to be returning null. These options + // are not strictly *needed*, but they are staying here as part of documentation + // of the default option set for the tool. options.set_option("malloc-may-fail", true); options.set_option("malloc-fail-null", true); @@ -91,11 +93,24 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(!cmdline.isset("no-standard-checks")) { goto_analyzer_parse_optionst::set_default_analysis_flags(options); + // The malloc failure mode is by default handled by the `config.set` call + // which only looks at the `cmdline` flags. In the case of default checks, + // these haven't been set - we need to overwrite the config object to manually + // bootstrap the malloc-may-fail behaviour + if(!config.ansi_c.malloc_may_fail && options.is_set("malloc-may-fail")) + { + config.ansi_c.malloc_may_fail = true; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; + } PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); } else if(cmdline.isset("no-standard-checks")) { PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); + // If the user opts for no standard checks, it's safe to assume he also + // wants to control the malloc failure behaviour, in which case we can + // also assume that it's going to be setup in the `config.set` call above. } // all (other) checks supported by goto_check From 1d7d4cfb1f89fe5036580e343316e7ede4d48e04 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 10:38:06 +0000 Subject: [PATCH 21/39] Add missing positive checks back into goto-instrument --- src/goto-instrument/goto_instrument_parse_options.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 55721374ce6..e2e8fd5f355 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1026,6 +1026,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() options.set_option("simplify", true); // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // initialize argv with valid pointers From 7e385187b40b673574406ceac37aa310e18922f7 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 10:56:22 +0000 Subject: [PATCH 22/39] Add --no-standard-checks to regression/goto-cc-cbmc test runner script --- regression/goto-cc-cbmc/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-cc-cbmc/chain.sh b/regression/goto-cc-cbmc/chain.sh index 61ec544401e..68e5f19b600 100755 --- a/regression/goto-cc-cbmc/chain.sh +++ b/regression/goto-cc-cbmc/chain.sh @@ -17,4 +17,4 @@ else "${goto_cc}" "${name}" -o "${base_name}.gb" fi -"${cbmc}" "${base_name}.gb" ${options} +"${cbmc}" --no-standard-checks "${base_name}.gb" ${options} From 81c73d01d2b3d6a5c33a1583a968f18e1fc6ca14 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:04:50 +0000 Subject: [PATCH 23/39] Add --no-standard-checks to regression/acceleration test runner script --- regression/acceleration/accelerate.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/acceleration/accelerate.sh b/regression/acceleration/accelerate.sh index c8598419ef0..7b1f17cf908 100755 --- a/regression/acceleration/accelerate.sh +++ b/regression/acceleration/accelerate.sh @@ -16,7 +16,7 @@ is_windows=$4 shift 4 cfile="" -cbmcargs="" +cbmcargs="--no-standard-checks" # create the temporary directory relative to the current directory, thus # avoiding file names that start with a "/", which confuses goto-cl (Windows) From bc9ae9b99c225db42be7d05722ea3f4d8077e9fa Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:15:57 +0000 Subject: [PATCH 24/39] Add --no-standard-checks to regresion/contracts-dfcc test runner script --- regression/contracts-dfcc/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh index 0bd901feaaf..97f9afb5ab1 100755 --- a/regression/contracts-dfcc/chain.sh +++ b/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} From b90ea03e19718bcf8319f2f036e7e6adddb3c891 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:54:28 +0000 Subject: [PATCH 25/39] Add --no-standard-checks to regression/contracts test runner script --- regression/contracts/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh index 615fd4568d6..527167d5984 100755 --- a/regression/contracts/chain.sh +++ b/regression/contracts/chain.sh @@ -42,4 +42,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then rm "${name}-mod.c" fi $goto_instrument --show-goto-functions "${name}-mod.gb" -$cbmc "${name}-mod.gb" ${args_cbmc} +$cbmc --no-standard-checks "${name}-mod.gb" ${args_cbmc} From 7d659349477cd0165f0b90c7a69e941cfb859aeb Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:55:38 +0000 Subject: [PATCH 26/39] Add --no-standard-checks to regression/goto-synthesiser test runner script --- regression/goto-synthesizer/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh index 52b4b683dbc..ed7c7fa498d 100755 --- a/regression/goto-synthesizer/chain.sh +++ b/regression/goto-synthesizer/chain.sh @@ -57,5 +57,5 @@ if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then else $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb" echo "Running CBMC: " - $cbmc ${args_cbmc} "${name}-mod-2.gb" + $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb" fi From 0d19437e911d5b42e2cb4199c82595e27e04c23a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:57:41 +0000 Subject: [PATCH 27/39] Add --no-standard-checks to regression/goto-harness test runner script --- regression/goto-harness/chain.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh index c9f796abfc2..050de057785 100755 --- a/regression/goto-harness/chain.sh +++ b/regression/goto-harness/chain.sh @@ -58,12 +58,14 @@ $goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entr $cbmc --show-goto-functions "$harness_file" if [[ "${harness_file}" == "harness.gb" ]];then $cbmc --function $entry_point "$harness_file" \ + --no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \ --pointer-check `# because we want to see out of bounds errors` \ --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \ --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ # cbmc args end else $cbmc --function $entry_point "$input_c_file" "$harness_file" \ + --no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \ --pointer-check `# because we want to see out of bounds errors` \ --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \ --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ From 1f81854e6da02d3cd27fcc60194896ee68cd1ac8 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 11:58:58 +0000 Subject: [PATCH 28/39] Add --no-standard-checks to ../regression/linking-goto-binaries test runner script --- regression/linking-goto-binaries/chain.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/linking-goto-binaries/chain.sh b/regression/linking-goto-binaries/chain.sh index d74593341a0..d391318efbd 100755 --- a/regression/linking-goto-binaries/chain.sh +++ b/regression/linking-goto-binaries/chain.sh @@ -21,4 +21,4 @@ else $goto_cc "${main}.gb" "${next}.gb" -o "final.gb" fi -$cbmc --validate-goto-model "final.gb" +$cbmc --no-standard-checks --validate-goto-model "final.gb" From bda5ed3c221604a124e53bf3890e0f4029245815 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 12:01:21 +0000 Subject: [PATCH 29/39] Add --no-standard-checks to regression/validate-trace-xml-schema python runner script --- regression/validate-trace-xml-schema/check.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 1ee1c781abd..fe9601d04d2 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -133,7 +133,7 @@ def check_test_desc(self, test_desc_path): self.check_trace(test_desc_path, trace_file) def read_trace_into(self, trace_file, args): - subprocess.run([CbmcPath, '--trace', '--xml-ui'] + args, + subprocess.run([CbmcPath, '--no-standard-checks', '--trace', '--xml-ui'] + args, stdout=trace_file) def check_trace(self, test_desc_path, trace_file): From 13a6e0b61d3cadd0972e54ef91eabd7e5f3daea7 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Dec 2023 17:28:08 +0000 Subject: [PATCH 30/39] Add documentation for new options in goto_check_c.h --- src/ansi-c/goto_check_c.h | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index c76eadff688..588e63aba7a 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -52,33 +52,47 @@ void goto_check_c( "(no-pointer-primitive-check)(no-undefined-shift-check)" \ "(no-div-by-zero-check)" -#define HELP_GOTO_CHECK \ - " {y--bounds-check} \t enable array bounds checks\n" \ - " {y--pointer-check} \t enable pointer checks\n" \ +// clang-format off +#define HELP_GOTO_CHECK \ + " {y--no-standard-checks} \t disable default checks (more information in manpage)" /* NOLINT(whitespace/line_length) */ \ + " {y--bounds-check} \t enable array bounds checks (default on)\n" \ + " {y--no-bounds-check} \t disable array bounds checks\n" \ + " {y--pointer-check} \t enable pointer checks (default on)\n" \ + " {y--no-pointer-check} \t disable pointer checks\n" \ " {y--memory-leak-check} \t enable memory leak checks\n" \ " {y--memory-cleanup-check} \t enable memory cleanup checks\n" \ - " {y--div-by-zero-check} \t enable division by zero checks\n" \ + " {y--div-by-zero-check} \t enable division by zero checks (default on)\n" \ + " {y--no-div-by-zero-check} \t disable division by zero checks\n" \ " {y--signed-overflow-check} \t " \ - "enable signed arithmetic over- and underflow checks\n" \ + "enable signed arithmetic over- and underflow checks (default on)\n" \ + " {y--no-signed-overflow-check} \t " \ + "disable signed arithmetic over- and underflow checks\n" \ " {y--unsigned-overflow-check} \t " \ "enable arithmetic over- and underflow checks\n" \ " {y--pointer-overflow-check} \t " \ "enable pointer arithmetic over- and underflow checks\n" \ " {y--conversion-check} \t " \ "check whether values can be represented after type cast\n" \ - " {y--undefined-shift-check} \t check shift greater than bit-width\n" \ + " {y--undefined-shift-check} \t check shift greater than bit-width " \ + "(default on)\n" \ + " {y--no-undefined-shift-check} \t disable check for shift greater than " \ + "bit-width\n" \ " {y--float-overflow-check} \t check floating-point for +/-Inf\n" \ " {y--nan-check} \t check floating-point for NaN\n" \ " {y--enum-range-check} \t " \ "checks that all enum type expressions have values in the enum range\n" \ " {y--pointer-primitive-check} \t " \ - "checks that all pointers in pointer primitives are valid or null\n" \ + "checks that all pointers in pointer primitives are valid or null (default " \ + "on)\n" \ + " {y--no-pointer-primitive-check} \t " \ + "disable checks that all pointers in pointer primitives are valid or null\n" \ " {y--retain-trivial-checks} \t include checks that are trivially true\n" \ " {y--error-label} {ulabel} \t check that label {ulabel} is unreachable\n" \ " {y--no-built-in-assertions} \t ignore assertions in built-in library\n" \ " {y--no-assertions} \t ignore user assertions\n" \ " {y--no-assumptions} \t ignore user assumptions\n" \ " {y--assert-to-assume} \t convert user assertions to assumptions\n" +// clang-format on // clang-format off #define PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options) \ From a485f7098a34ead0d1bdd7a48b803b22be9e4c63 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 12 Dec 2023 16:14:06 +0000 Subject: [PATCH 31/39] Add new flags to CBMC man page --- doc/man/cbmc.1 | 77 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 8722b40ada9..d356eabf5ba 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -8,6 +8,12 @@ cbmc \- Bounded Model Checker for C/C++ and Java programs .B cbmc [--all-properties] \fIfile.c\fB ... +.B cbmc [--no-standard-checks] \fIfile.c\fB ... + +.B cbmc [--no-standard-checks] [--pointer-check] \fIfile.c\fB ... + +.B cbmc [--no-bounds-check] \fIfile.c\fB ... + .B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB] .B goto-instrument \fIinfile\fB \fIoutfile\fR @@ -41,8 +47,79 @@ The usual flow is to (1) translate source into a GOTO binary using goto-cc, then (2) perform instrumentation with goto-instrument, and finally (3) perform the analysis with cbmc. .SH OPTIONS +.SS "Standard Checks" +From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools +apply some checks to the program by default (called the "standard checks"), with the +aim to provide a better user experience for a non-expert user of the tool. These checks are: +.TP +\fB\-\-pointer\-check\fR +enable pointer checks +.TP +\fB\-\-bounds\-check\fR +enable array bounds checks +.TP +\fB\-\-undefined\-shift\-check\fR +check shift greater than bit\-width +.TP +\fB\-\-div\-by\-zero\-check\fR +enable division by zero checks +.TP +\fB\-\-pointer\-primitive\-check\fR +checks that all pointers in pointer primitives are valid or null +.TP +\fB\-\-signed\-overflow\-check\fR +enable signed arithmetic over\- and underflow checks +.TP +\fB\-\-malloc\-may\-fail\fR +allow malloc calls to return a null pointer +.TP +\fB\-\-malloc\-fail\-null\fR +set malloc failure mode to return null +.TP +\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only) +generate unwinding assertions (cannot be +used with \fB\-\-cover\fR) +.PP +These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag +like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like +so: +.TP +\fB\-\-no\-pointer\-check\fR +disable pointer checks +.TP +\fB\-\-no\-bounds\-check\fR +disable array bounds checks +.TP +\fB\-\-no\-undefined\-shift\-check\fR +do not perform check for shift greater than bit\-width +.TP +\fB\-\-no\-div\-by\-zero\-check\fR +disable division by zero checks +.TP +\fB\-\-no\-pointer\-primitive\-check\fR +do not check that all pointers in pointer primitives are valid or null +.TP +\fB\-\-no\-signed\-overflow\-check\fR +disable signed arithmetic over\- and underflow checks +.TP +\fB\-\-no\-malloc\-may\-fail\fR +do not allow malloc calls to fail by default +.TP +\fB\-\-no\-malloc\-fail\-null\fR +do not set malloc failure mode to return null pointer +.TP +\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) +do not generate unwinding assertions (cannot be +used with \fB\-\-cover\fR) +.PP +If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR +when default checks are already on, the flag is simply ignored. .SS "Analysis options:" .TP +\fB\-\-no\-standard\-checks\fR +disable the standard (default) checks applied to a C/GOTO program +(see above for more information) +.TP \fB\-\-show\-properties\fR show the properties, but don't run analysis .TP From 9b52a385210142b667e37092ba709d528e64012e Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 12:43:45 +0000 Subject: [PATCH 32/39] Set the default checks status for both defaults on and off So that the defaults can be selectively overridden, whether they are initially on or off. --- src/cbmc/cbmc_parse_options.cpp | 26 +++++++++++-------- src/cbmc/cbmc_parse_options.h | 2 +- .../goto_analyzer_parse_options.cpp | 24 ++++++++++------- .../goto_analyzer_parse_options.h | 2 +- 4 files changed, 31 insertions(+), 23 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 838b02e76a2..caff61d7318 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -106,25 +106,27 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("depth", UINT32_MAX); } -void cbmc_parse_optionst::set_default_analysis_flags(optionst &options) +void cbmc_parse_optionst::set_default_analysis_flags( + optionst &options, + const bool enabled) { // Checks enabled by default in v6.0+. - 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); + options.set_option("bounds-check", enabled); + options.set_option("pointer-check", enabled); + options.set_option("pointer-primitive-check", enabled); + options.set_option("div-by-zero-check", enabled); + options.set_option("signed-overflow-check", enabled); + options.set_option("undefined-shift-check", enabled); // Default malloc failure profile chosen to be returning null. These options // are not strictly needed, but they are staying here as part of documentation // of the default option set for the tool. - options.set_option("malloc-may-fail", true); - options.set_option("malloc-fail-null", true); + options.set_option("malloc-may-fail", enabled); + options.set_option("malloc-fail-null", enabled); // 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); + options.set_option("unwinding-assertions", enabled); } void cbmc_parse_optionst::get_command_line_options(optionst &options) @@ -336,9 +338,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // Enable flags that in combination provide analysis with no surprises // (expected checks and no unsoundness by missing checks). + cbmc_parse_optionst::set_default_analysis_flags( + options, !cmdline.isset("no-standard-checks")); + if(!cmdline.isset("no-standard-checks")) { - cbmc_parse_optionst::set_default_analysis_flags(options); // The malloc failure mode is by default handled by the `config.set` call // which only looks at the `cmdline` flags. In the case of default checks, // these haven't been set - we need to overwrite the config object to manually diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 22ad39a663e..303c6feddac 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -96,7 +96,7 @@ class cbmc_parse_optionst : public parse_options_baset /// /// This function sets up the default analysis checks as discussed /// in RFC https://github.com/diffblue/cbmc/issues/7975. - static void set_default_analysis_flags(optionst &); + static void set_default_analysis_flags(optionst &, const bool enabled); static bool process_goto_program(goto_modelt &, const optionst &, messaget &); static int get_goto_program( diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index a5bb39aa5f3..611cb26cdb2 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -56,21 +56,23 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( { } -void goto_analyzer_parse_optionst::set_default_analysis_flags(optionst &options) +void goto_analyzer_parse_optionst::set_default_analysis_flags( + optionst &options, + const bool enabled) { // Checks enabled by default in v6.0+. - 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); + options.set_option("bounds-check", enabled); + options.set_option("pointer-check", enabled); + options.set_option("pointer-primitive-check", enabled); + options.set_option("div-by-zero-check", enabled); + options.set_option("signed-overflow-check", enabled); + options.set_option("undefined-shift-check", enabled); // Default malloc failure profile chosen to be returning null. These options // are not strictly *needed*, but they are staying here as part of documentation // of the default option set for the tool. - options.set_option("malloc-may-fail", true); - options.set_option("malloc-fail-null", true); + options.set_option("malloc-may-fail", enabled); + options.set_option("malloc-fail-null", enabled); // This is in-line with the options we set for CBMC in cbmc_parse_optionst // with the exception of unwinding-assertions, which don't make sense in @@ -88,11 +90,13 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); + goto_analyzer_parse_optionst::set_default_analysis_flags( + options, !cmdline.isset("no-standard-checks")); + // Enable flags that in combination provide analysis with no surprises // (expected checks and no unsoundness by missing checks). if(!cmdline.isset("no-standard-checks")) { - goto_analyzer_parse_optionst::set_default_analysis_flags(options); // The malloc failure mode is by default handled by the `config.set` call // which only looks at the `cmdline` flags. In the case of default checks, // these haven't been set - we need to overwrite the config object to manually diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 52c967a9135..0e55007c81c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -191,7 +191,7 @@ class goto_analyzer_parse_optionst: public parse_options_baset virtual int perform_analysis(const optionst &options); // TODO: Add documentation - static void set_default_analysis_flags(optionst &options); + static void set_default_analysis_flags(optionst &options, const bool enabled); }; #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H From 1575958ceb0788b70c17fbfd51d49aeaebca57a6 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 13:17:37 +0000 Subject: [PATCH 33/39] Combine `NEGATIVE` and `POSITIVE` check macros 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. --- src/ansi-c/goto_check_c.h | 35 +++++++------------ src/cbmc/cbmc_parse_options.cpp | 8 ----- .../goto_analyzer_parse_options.cpp | 8 ----- .../goto_instrument_parse_options.cpp | 1 - 4 files changed, 13 insertions(+), 39 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 588e63aba7a..9fcf818241b 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -94,27 +94,12 @@ void goto_check_c( " {y--assert-to-assume} \t convert user assertions to assumptions\n" // clang-format on -// clang-format off - #define PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options) \ - options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \ - options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \ - options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \ - options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ - (void) 0; -// clang-format on - -// clang-format off - #define PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options) \ - options.set_option("bounds-check", cmdline.isset("bounds-check")); \ - options.set_option("pointer-check", cmdline.isset("pointer-check")); \ - options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ - options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ - (void) 0; -// clang-format on +#define PARSE_OPTION_OVERRIDE(cmdline, options, option) \ + if(cmdline.isset(option)) \ + options.set_option(option, true); \ + if(cmdline.isset("no-" option)) \ + options.set_option(option, false); \ + (void)0 // clang-format off #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ @@ -134,7 +119,13 @@ void goto_check_c( options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \ if(cmdline.isset("error-label")) \ - options.set_option("error-label", cmdline.get_values("error-label")); \ + options.set_option("error-label", cmdline.get_values("error-label")); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \ + PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \ (void)0 // clang-format on diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index caff61d7318..5068a25e4d8 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -353,14 +353,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) config.ansi_c.malloc_failure_mode = configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; } - PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); - } - else if(cmdline.isset("no-standard-checks")) - { - PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); - // If the user opts for no standard checks, it's safe to assume he also - // wants to control the malloc failure behaviour, in which case we can - // also assume that it's going to be setup in the `config.set` call above. } // all (other) checks supported by goto_check diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 611cb26cdb2..a1744b9d719 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -107,14 +107,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) config.ansi_c.malloc_failure_mode = configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; } - PARSE_OPTIONS_GOTO_CHECK_NEGATIVE_DEFAULT_CHECKS(cmdline, options); - } - else if(cmdline.isset("no-standard-checks")) - { - PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); - // If the user opts for no standard checks, it's safe to assume he also - // wants to control the malloc failure behaviour, in which case we can - // also assume that it's going to be setup in the `config.set` call above. } // all (other) checks supported by goto_check diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index e2e8fd5f355..55721374ce6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1026,7 +1026,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() options.set_option("simplify", true); // all checks supported by goto_check - PARSE_OPTIONS_GOTO_CHECK_POSITIVE_DEFAULT_CHECKS(cmdline, options); PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // initialize argv with valid pointers From a5a29ad8ea14dc6e59c2d7ad6c8c24ccfa26d82a Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 16:05:36 +0000 Subject: [PATCH 34/39] Use `get_bool_option` to get `unwinding-assertions` option 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. --- src/cbmc/cbmc_parse_options.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5068a25e4d8..6aec304ee05 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -146,7 +146,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if( cmdline.isset("cover") && // The option is set by default, or passed in the by the user. - (options.is_set("unwinding-assertions") || + (options.get_bool_option("unwinding-assertions") || cmdline.isset("unwinding-assertions"))) { log.error() @@ -289,7 +289,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) { options.set_option("unwind", cmdline.get_value("unwind")); if( - !options.is_set("unwinding-assertions") && + !options.get_bool_option("unwinding-assertions") && !cmdline.isset("unwinding-assertions")) { log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " @@ -318,7 +318,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option( "unwindset", cmdline.get_comma_separated_values("unwindset")); if( - !options.is_set("unwinding-assertions") && + !options.get_bool_option("unwinding-assertions") && !cmdline.isset("unwinding-assertions")) { log.warning() << "**** WARNING: Use --unwinding-assertions to obtain " @@ -360,7 +360,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // generate unwinding assertions if( - options.is_set("unwinding-assertions") || + options.get_bool_option("unwinding-assertions") || cmdline.isset("unwinding-assertions")) { options.set_option("unwinding-assertions", true); From 64a7e54d4f7e11eae40d819e1573a20a93d1c2f9 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 16:12:38 +0000 Subject: [PATCH 35/39] When `--cover` is used switch off unwinding-assertions 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`. --- src/cbmc/cbmc_parse_options.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6aec304ee05..7011c9ac769 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -143,11 +143,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); - if( - cmdline.isset("cover") && - // The option is set by default, or passed in the by the user. - (options.get_bool_option("unwinding-assertions") || - cmdline.isset("unwinding-assertions"))) + if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions")) { log.error() << "--cover and --unwinding-assertions must not be given together" @@ -204,7 +200,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-vcc", true); if(cmdline.isset("cover")) + { parse_cover_options(cmdline, options); + // The default unwinding assertions option needs to be switched off when + // performing coverage checks because we intend to solve for coverage rather + // than assertions. + options.set_option("unwinding-assertions", false); + } if(cmdline.isset("mm")) options.set_option("mm", cmdline.get_value("mm")); From 07ab70ef48db774ad1627a70facf1014b3e20823 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Dec 2023 11:04:55 +0000 Subject: [PATCH 36/39] Add standard checks to goto-analyzer's man page --- doc/man/goto-analyzer.1 | 77 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index bfa40f426f7..ea41841da47 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -8,6 +8,12 @@ goto-analyzer \- Data-flow analysis for C programs and goto binaries .B goto\-analyzer [options] file.c|file.gb +.B goto\-analyzer [--no-standard-checks] \fIfile.c\fB ... + +.B goto\-analyzer [--no-standard-checks] [--pointer-check] \fIfile.c\fB ... + +.B goto\-analyzer [--no-bounds-check] \fIfile.c\fB ... + .SH DESCRIPTION .B goto-analyzer is an abstract interpreter which uses the same @@ -494,6 +500,10 @@ list loaded goto functions show the properties, but don't run analysis .SS "Program instrumentation options:" .TP +\fB\-\-no\-standard\-checks\fR +disable the standard (default) checks applied to a C/GOTO program +(see below for more information) +.TP \fB\-\-property\fR id enable selected properties only .TP @@ -569,6 +579,73 @@ set malloc failure mode to return null .TP \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination +.SS "Standard Checks" +From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools +apply some checks to the program by default (called the "standard checks"), with the +aim to provide a better user experience for a non-expert user of the tool. These checks are: +.TP +\fB\-\-pointer\-check\fR +enable pointer checks +.TP +\fB\-\-bounds\-check\fR +enable array bounds checks +.TP +\fB\-\-undefined\-shift\-check\fR +check shift greater than bit\-width +.TP +\fB\-\-div\-by\-zero\-check\fR +enable division by zero checks +.TP +\fB\-\-pointer\-primitive\-check\fR +checks that all pointers in pointer primitives are valid or null +.TP +\fB\-\-signed\-overflow\-check\fR +enable signed arithmetic over\- and underflow checks +.TP +\fB\-\-malloc\-may\-fail\fR +allow malloc calls to return a null pointer +.TP +\fB\-\-malloc\-fail\-null\fR +set malloc failure mode to return null +.TP +\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only) +generate unwinding assertions (cannot be +used with \fB\-\-cover\fR) +.PP +These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag +like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like +so: +.TP +\fB\-\-no\-pointer\-check\fR +disable pointer checks +.TP +\fB\-\-no\-bounds\-check\fR +disable array bounds checks +.TP +\fB\-\-no\-undefined\-shift\-check\fR +do not perform check for shift greater than bit\-width +.TP +\fB\-\-no\-div\-by\-zero\-check\fR +disable division by zero checks +.TP +\fB\-\-no\-pointer\-primitive\-check\fR +do not check that all pointers in pointer primitives are valid or null +.TP +\fB\-\-no\-signed\-overflow\-check\fR +disable signed arithmetic over\- and underflow checks +.TP +\fB\-\-no\-malloc\-may\-fail\fR +do not allow malloc calls to fail by default +.TP +\fB\-\-no\-malloc\-fail\-null\fR +do not set malloc failure mode to return null pointer +.TP +\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) +do not generate unwinding assertions (cannot be +used with \fB\-\-cover\fR) +.PP +If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR +when default checks are already on, the flag is simply ignored. .SS "Other options:" .TP \fB\-\-validate\-goto\-model\fR From 7838ad85924ad3c4262b2da13c3c47e75d241f22 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Dec 2023 14:53:29 +0000 Subject: [PATCH 37/39] Remove handling of `malloc-may-fail`. It will be handled in next PR. --- src/cbmc/cbmc_parse_options.cpp | 20 ----------------- .../goto_analyzer_parse_options.cpp | 22 ------------------- 2 files changed, 42 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7011c9ac769..a26448a9f54 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -118,12 +118,6 @@ void cbmc_parse_optionst::set_default_analysis_flags( options.set_option("signed-overflow-check", enabled); options.set_option("undefined-shift-check", enabled); - // Default malloc failure profile chosen to be returning null. These options - // are not strictly needed, but they are staying here as part of documentation - // of the default option set for the tool. - options.set_option("malloc-may-fail", enabled); - options.set_option("malloc-fail-null", enabled); - // 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", enabled); @@ -343,20 +337,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_analysis_flags( options, !cmdline.isset("no-standard-checks")); - if(!cmdline.isset("no-standard-checks")) - { - // The malloc failure mode is by default handled by the `config.set` call - // which only looks at the `cmdline` flags. In the case of default checks, - // these haven't been set - we need to overwrite the config object to manually - // bootstrap the malloc-may-fail behaviour - if(!config.ansi_c.malloc_may_fail && options.is_set("malloc-may-fail")) - { - config.ansi_c.malloc_may_fail = true; - config.ansi_c.malloc_failure_mode = - configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; - } - } - // all (other) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index a1744b9d719..868d23e71f0 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -68,12 +68,6 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags( options.set_option("signed-overflow-check", enabled); options.set_option("undefined-shift-check", enabled); - // Default malloc failure profile chosen to be returning null. These options - // are not strictly *needed*, but they are staying here as part of documentation - // of the default option set for the tool. - options.set_option("malloc-may-fail", enabled); - options.set_option("malloc-fail-null", enabled); - // This is in-line with the options we set for CBMC in cbmc_parse_optionst // with the exception of unwinding-assertions, which don't make sense in // the context of abstract interpretation. @@ -93,22 +87,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) goto_analyzer_parse_optionst::set_default_analysis_flags( options, !cmdline.isset("no-standard-checks")); - // Enable flags that in combination provide analysis with no surprises - // (expected checks and no unsoundness by missing checks). - if(!cmdline.isset("no-standard-checks")) - { - // The malloc failure mode is by default handled by the `config.set` call - // which only looks at the `cmdline` flags. In the case of default checks, - // these haven't been set - we need to overwrite the config object to manually - // bootstrap the malloc-may-fail behaviour - if(!config.ansi_c.malloc_may_fail && options.is_set("malloc-may-fail")) - { - config.ansi_c.malloc_may_fail = true; - config.ansi_c.malloc_failure_mode = - configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; - } - } - // all (other) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); From 3ec5bfdfc21f971109410284c9ecacbcbbe6e825 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Dec 2023 15:45:11 +0000 Subject: [PATCH 38/39] Don't expect goto-check negative checks for goto-diff manpage. --- scripts/check_help.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/scripts/check_help.sh b/scripts/check_help.sh index f524c0fb5d7..103ace59165 100755 --- a/scripts/check_help.sh +++ b/scripts/check_help.sh @@ -91,6 +91,21 @@ for t in \ echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts done ;; + # goto-diff is a bit of a peculiar situation in that it initialises some + # of its options using the PARSE_OPTIONS_GOTO_CHECK macro which initialises + # the negative checks (being the mirror image of the default checks), which + # this tool doesn't make use of - but there's also no good way to remove + # given our current architecture. Thus, we just don't document them (and + # ignore them if someone falls on them by accident). + goto-diff) + for undoc in \ + -no-pointer-check -no-bounds-check -no-undefined-shift-check \ + -no-pointer-primitive-check -no-div-by-zero-check \ + -no-signed-overflow-check ; do + echo "$undoc" >> help_string + echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts + done + ;; janalyzer) # -jar, -gb are documented, but in a different format for undoc in -show-intervals -show-non-null -jar -gb ; do From 9747f611973effabb1dcfd0d0baa3e8c4a61a01f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Dec 2023 15:49:16 +0000 Subject: [PATCH 39/39] Add negative default checks to ignore list of goto-instrument as well --- scripts/check_help.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/check_help.sh b/scripts/check_help.sh index 103ace59165..6dad8f8e5ef 100755 --- a/scripts/check_help.sh +++ b/scripts/check_help.sh @@ -83,10 +83,15 @@ for t in \ echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts done ;; + # We also need ignore the negative default checks for goto-instrument given + # that it's not processing them (but still ends up importing them by using + # the macro PARSE_OPTIONS_GOTO_CHECK). The rationale for ignoring them is + # similar to the goto-diff entry below. goto-instrument) for undoc in \ -document-claims-html -document-claims-latex -show-claims \ - -no-simplify ; do + -no-simplify -no-pointer-check -no-bounds-check -no-undefined-shift-check \ + -no-pointer-primitive-check -no-div-by-zero-check -no-signed-overflow-check ; do echo "$undoc" >> help_string echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts done