From 5059a207bc5d1209ace597a3650ea002e944fb8b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 23:43:44 +0000 Subject: [PATCH 1/8] Add `--no-malloc-fail` parameter So that the malloc failure configuration can be returned to non failure, without using the full `--no-standard-checks` option. --- src/util/config.cpp | 5 +++++ src/util/config.h | 3 ++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/util/config.cpp b/src/util/config.cpp index a390435b264..9b46f89df19 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1127,6 +1127,11 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail"); + if(cmdline.isset("no-malloc-fail")) + { + ansi_c.malloc_may_fail = false; + ansi_c.malloc_failure_mode = ansi_ct::malloc_failure_mode_none; + } if(cmdline.isset("c89")) ansi_c.set_c89(); diff --git a/src/util/config.h b/src/util/config.h index 0bfedadc627..50038cd8e13 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -70,7 +70,7 @@ class symbol_table_baset; " {y--no-library} \t disable built-in abstract C library\n" #define OPT_CONFIG_LIBRARY \ - "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \ + "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)(no-malloc-fail)" \ "(string-abstraction)" #define HELP_CONFIG_LIBRARY \ @@ -78,6 +78,7 @@ class symbol_table_baset; " {y--malloc-fail-assert} \t " \ "set malloc failure mode to assert-then-assume\n" \ " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \ + " {y--no-malloc-fail} \t Disable potential malloc failure.\n" \ " {y--string-abstraction} \t track C string lengths and zero-termination\n" #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)" From 36960204cdec4e3b29b6c89e03084b7aef89f0db Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Dec 2023 23:48:43 +0000 Subject: [PATCH 2/8] Use `malloc-fail-null` as the default model configuration --- src/util/config.cpp | 5 ++++- src/util/config.h | 4 ++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/util/config.cpp b/src/util/config.cpp index 9b46f89df19..2787eafa16b 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1126,7 +1126,10 @@ bool configt::set(const cmdlinet &cmdline) if(cmdline.isset("malloc-fail-assert")) ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; - ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail"); + if(cmdline.isset("malloc-may-fail")) + { + ansi_c.malloc_may_fail = true; + } if(cmdline.isset("no-malloc-fail")) { ansi_c.malloc_may_fail = false; diff --git a/src/util/config.h b/src/util/config.h index 50038cd8e13..f0c9de8f692 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -272,7 +272,7 @@ class configt libt lib; bool string_abstraction; - bool malloc_may_fail = false; + bool malloc_may_fail = true; enum malloc_failure_modet { @@ -281,7 +281,7 @@ class configt malloc_failure_mode_assert_then_assume = 2 }; - malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none; + malloc_failure_modet malloc_failure_mode = malloc_failure_mode_return_null; static const std::size_t default_object_bits = 8; From 06a48de7293292dc3f7b3862db739db5efbf3b07 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 14 Dec 2023 13:20:26 +0000 Subject: [PATCH 3/8] Make `--no-standard-checks` reinstate old malloc behaviour The calls to the `set_default_analysis_flags` functions need to be before the call to `config.set(cmdline)` so that the malloc defaults can be set before being overridden by any command line specified malloc behaviour. --- src/cbmc/cbmc_parse_options.cpp | 23 +++++++++++++++---- .../goto_analyzer_parse_options.cpp | 19 ++++++++++++--- 2 files changed, 34 insertions(+), 8 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d0bef5fa8a1..19f450e13c9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -126,10 +126,28 @@ void cbmc_parse_optionst::set_default_analysis_flags( { options.set_option("unwinding-assertions", enabled); } + + if(enabled) + { + config.ansi_c.malloc_may_fail = true; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; + } + else + { + config.ansi_c.malloc_may_fail = false; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none; + } } 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(config.set(cmdline)) { usage_error(); @@ -366,11 +384,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) "self-loops-to-assumptions", !cmdline.isset("no-self-loops-to-assumptions")); - // 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")); - // 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 868d23e71f0..5fe19e6bd55 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -68,6 +68,19 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags( options.set_option("signed-overflow-check", enabled); options.set_option("undefined-shift-check", enabled); + if(enabled) + { + config.ansi_c.malloc_may_fail = true; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null; + } + else + { + config.ansi_c.malloc_may_fail = false; + config.ansi_c.malloc_failure_mode = + configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none; + } + // 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. @@ -75,6 +88,9 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags( 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")); + if(config.set(cmdline)) { usage_error(); @@ -84,9 +100,6 @@ 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")); - // all (other) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); From f69be775fc167f885ddf1ecddc228a30ad2cc09d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 14 Dec 2023 11:29:35 +0000 Subject: [PATCH 4/8] Add `--no-malloc-fail` to test runners In order to keep existing tests passing. --- regression/contracts-dfcc/chain.sh | 4 ++++ regression/goto-instrument/chain.sh | 4 ++-- regression/goto-synthesizer/chain.sh | 6 +++--- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh index 97f9afb5ab1..0d61c8b1f38 100755 --- a/regression/contracts-dfcc/chain.sh +++ b/regression/contracts-dfcc/chain.sh @@ -43,6 +43,10 @@ else $goto_cc -o "${name}${dfcc_suffix}.gb" "${name}.c" fi +if [[ "${args_inst}" != *"malloc"* ]]; then + args_inst="--no-malloc-fail $args_inst" +fi + rm -f "${name}${dfcc_suffix}-mod.gb" $goto_instrument ${args_inst} "${name}${dfcc_suffix}.gb" "${name}${dfcc_suffix}-mod.gb" if [ ! -e "${name}${dfcc_suffix}-mod.gb" ] ; then diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh index ed4fdbedc9d..7f596e9f0fb 100755 --- a/regression/goto-instrument/chain.sh +++ b/regression/goto-instrument/chain.sh @@ -21,7 +21,7 @@ else fi rm -f "${target}-mod.gb" -$goto_instrument ${args} "${target}.gb" "${target}-mod.gb" +$goto_instrument --no-malloc-fail ${args} "${target}.gb" "${target}-mod.gb" if [ ! -e "${target}-mod.gb" ] ; then cp "${target}.gb" "${target}-mod.gb" elif echo $args | grep -q -- "--dump-c-type-header" ; then @@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then rm "${target}-mod.c" fi -$goto_instrument --show-goto-functions "${target}-mod.gb" +$goto_instrument --no-malloc-fail --show-goto-functions "${target}-mod.gb" $cbmc --no-standard-checks "${target}-mod.gb" diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh index ed7c7fa498d..50e1b6240ff 100755 --- a/regression/goto-synthesizer/chain.sh +++ b/regression/goto-synthesizer/chain.sh @@ -37,7 +37,7 @@ fi rm -f "${name}-mod.gb" rm -f "${name}-mod-2.gb" echo "Running goto-instrument: " -$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb" +$goto_instrument --no-malloc-fail ${args_inst} "${name}.gb" "${name}-mod.gb" if [ ! -e "${name}-mod.gb" ] ; then cp "$name.gb" "${name}-mod.gb" elif echo $args_inst | grep -q -- "--dump-c" ; then @@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then fi echo "Running goto-synthesizer: " if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then - $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" else - $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" "${name}-mod-2.gb" echo "Running CBMC: " $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb" fi From c3635b1bda1a6050c8e62930cf132d6507bb3ac2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 15 Dec 2023 14:23:34 +0000 Subject: [PATCH 5/8] Upate man files to match `--no-malloc-fail` option implemented --- doc/man/cbmc.1 | 7 ++----- doc/man/goto-analyzer.1 | 7 ++----- doc/man/goto-instrument.1 | 3 +++ 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index d356eabf5ba..65a4dfdfae4 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -102,11 +102,8 @@ do not check that all pointers in pointer primitives are valid or null \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 +\fB\-\-no\-malloc\-fail\fR +Do not allow malloc calls to fail by default. .TP \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) do not generate unwinding assertions (cannot be diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index ea41841da47..ef7365a78a5 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -634,11 +634,8 @@ do not check that all pointers in pointer primitives are valid or null \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 +\fB\-\-no\-malloc\-fail\fR +Do not allow malloc calls to fail by default. .TP \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) do not generate unwinding assertions (cannot be diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 6ecdb5efc37..e5ac005aef5 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -697,6 +697,9 @@ set malloc failure mode to assert\-then\-assume \fB\-\-malloc\-fail\-null\fR set malloc failure mode to return null .TP +\fB\-\-no\-malloc\-fail\fR +Do not allow malloc calls to fail by default. +.TP \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination .TP From 77befb999be8033fba8fe9b683266b6285423203 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 18 Dec 2023 17:38:20 +0000 Subject: [PATCH 6/8] Renamed no-malloc-fail to no-malloc-may-fail to mirror malloc-may-fail --- doc/man/cbmc.1 | 4 ++-- doc/man/goto-analyzer.1 | 4 ++-- doc/man/goto-instrument.1 | 4 ++-- src/util/config.cpp | 2 +- src/util/config.h | 5 +++-- 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 65a4dfdfae4..15fffbcf2c3 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -102,8 +102,8 @@ do not check that all pointers in pointer primitives are valid or null \fB\-\-no\-signed\-overflow\-check\fR disable signed arithmetic over\- and underflow checks .TP -\fB\-\-no\-malloc\-fail\fR -Do not allow malloc calls to fail by default. +\fB\-\-no\-malloc\-may\-fail\fR +do not allow malloc calls to fail by default .TP \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) do not generate unwinding assertions (cannot be diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index ef7365a78a5..a42eb3cc461 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -634,8 +634,8 @@ do not check that all pointers in pointer primitives are valid or null \fB\-\-no\-signed\-overflow\-check\fR disable signed arithmetic over\- and underflow checks .TP -\fB\-\-no\-malloc\-fail\fR -Do not allow malloc calls to fail by default. +\fB\-\-no\-malloc\-may\-fail\fR +do not allow malloc calls to fail by default .TP \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only) do not generate unwinding assertions (cannot be diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index e5ac005aef5..88428b58c7c 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -697,8 +697,8 @@ set malloc failure mode to assert\-then\-assume \fB\-\-malloc\-fail\-null\fR set malloc failure mode to return null .TP -\fB\-\-no\-malloc\-fail\fR -Do not allow malloc calls to fail by default. +\fB\-\-no\-malloc\-may\-fail\fR +do not allow malloc calls to fail by default .TP \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination diff --git a/src/util/config.cpp b/src/util/config.cpp index 2787eafa16b..892ae6995a0 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1130,7 +1130,7 @@ bool configt::set(const cmdlinet &cmdline) { ansi_c.malloc_may_fail = true; } - if(cmdline.isset("no-malloc-fail")) + if(cmdline.isset("no-malloc-may-fail")) { ansi_c.malloc_may_fail = false; ansi_c.malloc_failure_mode = ansi_ct::malloc_failure_mode_none; diff --git a/src/util/config.h b/src/util/config.h index f0c9de8f692..253eedeeadb 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -70,15 +70,16 @@ class symbol_table_baset; " {y--no-library} \t disable built-in abstract C library\n" #define OPT_CONFIG_LIBRARY \ - "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)(no-malloc-fail)" \ + "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \ + "(no-malloc-may-fail)" \ "(string-abstraction)" #define HELP_CONFIG_LIBRARY \ " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \ + " {y--no-malloc-may-fail} \t disable potential malloc failure\n" \ " {y--malloc-fail-assert} \t " \ "set malloc failure mode to assert-then-assume\n" \ " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \ - " {y--no-malloc-fail} \t Disable potential malloc failure.\n" \ " {y--string-abstraction} \t track C string lengths and zero-termination\n" #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)" From c63610bdc667abc6e3bc5a42460ce84cf4f4c440 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 19 Dec 2023 11:28:55 +0000 Subject: [PATCH 7/8] Added malloc failure model to goto-analyzer --- src/goto-analyzer/goto_analyzer_parse_options.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 0e55007c81c..a78643b12d7 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -89,6 +89,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H +#include #include #include #include @@ -152,6 +153,7 @@ class optionst; OPT_SHOW_GOTO_FUNCTIONS \ OPT_SHOW_PROPERTIES \ OPT_GOTO_CHECK \ + OPT_CONFIG_LIBRARY \ "(show-symbol-table)(show-parse-tree)" \ "(property):" \ "(verbosity):(version)" \ From c3c7bc01cc5892c9809252c20a9454deca185343 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 19 Dec 2023 11:31:47 +0000 Subject: [PATCH 8/8] Renamed no-malloc-fail to no-malloc-may-fail to mirror malloc-may-fail on tests runners --- regression/contracts-dfcc/chain.sh | 2 +- regression/goto-instrument/chain.sh | 4 ++-- regression/goto-synthesizer/chain.sh | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh index 0d61c8b1f38..8b931718943 100755 --- a/regression/contracts-dfcc/chain.sh +++ b/regression/contracts-dfcc/chain.sh @@ -44,7 +44,7 @@ else fi if [[ "${args_inst}" != *"malloc"* ]]; then - args_inst="--no-malloc-fail $args_inst" + args_inst="--no-malloc-may-fail $args_inst" fi rm -f "${name}${dfcc_suffix}-mod.gb" diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh index 7f596e9f0fb..96ebce32760 100755 --- a/regression/goto-instrument/chain.sh +++ b/regression/goto-instrument/chain.sh @@ -21,7 +21,7 @@ else fi rm -f "${target}-mod.gb" -$goto_instrument --no-malloc-fail ${args} "${target}.gb" "${target}-mod.gb" +$goto_instrument --no-malloc-may-fail ${args} "${target}.gb" "${target}-mod.gb" if [ ! -e "${target}-mod.gb" ] ; then cp "${target}.gb" "${target}-mod.gb" elif echo $args | grep -q -- "--dump-c-type-header" ; then @@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then rm "${target}-mod.c" fi -$goto_instrument --no-malloc-fail --show-goto-functions "${target}-mod.gb" +$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb" $cbmc --no-standard-checks "${target}-mod.gb" diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh index 50e1b6240ff..d6379cac470 100755 --- a/regression/goto-synthesizer/chain.sh +++ b/regression/goto-synthesizer/chain.sh @@ -37,7 +37,7 @@ fi rm -f "${name}-mod.gb" rm -f "${name}-mod-2.gb" echo "Running goto-instrument: " -$goto_instrument --no-malloc-fail ${args_inst} "${name}.gb" "${name}-mod.gb" +$goto_instrument --no-malloc-may-fail ${args_inst} "${name}.gb" "${name}-mod.gb" if [ ! -e "${name}-mod.gb" ] ; then cp "$name.gb" "${name}-mod.gb" elif echo $args_inst | grep -q -- "--dump-c" ; then @@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then fi echo "Running goto-synthesizer: " if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then - $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" else - $goto_synthesizer ${args_synthesizer} --no-malloc-fail "${name}-mod.gb" "${name}-mod-2.gb" + $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" "${name}-mod-2.gb" echo "Running CBMC: " $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb" fi