From b9d06c8ded32fd0b5ee0535fe8c6eec548ed5f90 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 21 Sep 2020 10:16:48 +0100 Subject: [PATCH 1/3] Fix bug that prevented --malloc-may-fail from working We have code in our stdlib models that depends on two global variables, __CPROVER_malloc_may_fail and __CPROVER_malloc_failure_mode. Previously these were set based on the ansi-c config in builtin_additions by generating C code containing definitions for these variables. The problem with that is that if you compile an executable using goto-cc we also load the builtin_additions, so this executable already contains definitions for these variables which can't be overridden. This works around this issue by instead declaring these variables as extern in builtin_additions, and setting their values dynamically as last-minute instrumentation at the end of __CPROVER_initialize. Giving these no/nondet initial values is important because otherwise preprocessing like constant folding on goto-binaries before cbmc actually runs could remove branches we can, in fact, take with different values set by --malloc-fail-* flags. An alternative would be to instead dynamically change the code for the models functions as instrumentation, but this has a couple of problems; For instance this means we might change the behaviour of custom stdlib models (which we allow via --no-library) or custom goto instrumentation in unexpected ways. I believe this way is the least likely to cause any friction like that. --- .../test.c | 10 +++ .../test.desc | 11 ++++ src/ansi-c/ansi_c_internal_additions.cpp | 6 +- src/cbmc/cbmc_parse_options.cpp | 3 + src/goto-programs/Makefile | 3 +- ...lloc_may_fail_variable_initializations.cpp | 62 +++++++++++++++++++ ...malloc_may_fail_variable_initializations.h | 20 ++++++ 7 files changed, 110 insertions(+), 5 deletions(-) create mode 100644 regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c create mode 100644 regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc create mode 100644 src/goto-programs/add_malloc_may_fail_variable_initializations.cpp create mode 100644 src/goto-programs/add_malloc_may_fail_variable_initializations.h diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c new file mode 100644 index 00000000000..9995977ec2d --- /dev/null +++ b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.c @@ -0,0 +1,10 @@ +#include +#include + +int main(void) +{ + int *array = calloc(10, sizeof(int)); + assert(array != NULL); + free(array); + return 0; +} diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc new file mode 100644 index 00000000000..77516db1ccb --- /dev/null +++ b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--malloc-may-fail --malloc-fail-null +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line 7 assertion array != .*: FAILURE +-- +-- +Compiling a file with goto-cc should not affect how --malloc-may-fail behaves +Regex in the assertion because on travis for some reason the preprocessor seems to run +before cbmc. diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index cc6e04020ec..965dfb36d22 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -186,8 +186,7 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" "const void *" CPROVER_PREFIX "alloca_object = 0;\n" - "int " CPROVER_PREFIX "malloc_failure_mode="+ - std::to_string(config.ansi_c.malloc_failure_mode)+";\n" + "extern int " CPROVER_PREFIX "malloc_failure_mode;\n" "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+ std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n" "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+ @@ -195,8 +194,7 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ integer2string(max_malloc_size(config.ansi_c.pointer_width, config .bv_encoding.object_bits))+";\n" - CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " + - std::to_string(config.ansi_c.malloc_may_fail) + ";\n" + "extern " CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail;\n" // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5c77b4e1942..b00f85f891a 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -48,6 +48,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -879,6 +880,8 @@ bool cbmc_parse_optionst::process_goto_program( link_to_library( goto_model, log.get_message_handler(), cprover_c_library_factory); + add_malloc_may_fail_variable_initializations(goto_model); + if(options.get_bool_option("string-abstraction")) string_instrumentation(goto_model, log.get_message_handler()); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index ac22aa41a86..18a9129e7be 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,4 +1,5 @@ -SRC = adjust_float_expressions.cpp \ +SRC = add_malloc_may_fail_variable_initializations.cpp \ + adjust_float_expressions.cpp \ builtin_functions.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ diff --git a/src/goto-programs/add_malloc_may_fail_variable_initializations.cpp b/src/goto-programs/add_malloc_may_fail_variable_initializations.cpp new file mode 100644 index 00000000000..c426a42bb76 --- /dev/null +++ b/src/goto-programs/add_malloc_may_fail_variable_initializations.cpp @@ -0,0 +1,62 @@ +/// \file +/// \author Diffblue Ltd. + +#include "add_malloc_may_fail_variable_initializations.h" + +#include "goto_model.h" + +#include +#include +#include + +template +code_assignt make_integer_assignment( + const symbol_table_baset &symbol_table, + const irep_idt &symbol_name, + T &&value) +{ + const auto &symbol = symbol_table.lookup_ref(symbol_name).symbol_expr(); + return code_assignt{symbol, from_integer(value, symbol.type())}; +} + +void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model) +{ + const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"}; + const auto malloc_failure_mode_id = + irep_idt{CPROVER_PREFIX "malloc_failure_mode"}; + if(!goto_model.symbol_table.has_symbol(malloc_may_fail_id)) + { + // if malloc_may_fail isn't in the symbol table (i.e. builtin library not + // loaded) then we don't generate initialisation code for it. + return; + } + + INVARIANT( + goto_model.symbol_table.has_symbol(malloc_failure_mode_id), + "if malloc_may_fail is in the symbol table then so should " + "malloc_failure_mode"); + + auto const initialize_function_name = CPROVER_PREFIX "initialize"; + PRECONDITION( + goto_model.get_goto_functions().function_map.count( + initialize_function_name) == 1); + auto &initialize_function = + goto_model.goto_functions.function_map.find(initialize_function_name) + ->second; + const auto initialize_function_end = + --initialize_function.body.instructions.end(); + + initialize_function.body.insert_before( + initialize_function_end, + goto_programt::make_assignment(make_integer_assignment( + goto_model.symbol_table, + malloc_may_fail_id, + config.ansi_c.malloc_may_fail))); + + initialize_function.body.insert_before( + initialize_function_end, + goto_programt::make_assignment(make_integer_assignment( + goto_model.symbol_table, + malloc_failure_mode_id, + config.ansi_c.malloc_failure_mode))); +} diff --git a/src/goto-programs/add_malloc_may_fail_variable_initializations.h b/src/goto-programs/add_malloc_may_fail_variable_initializations.h new file mode 100644 index 00000000000..074cb522966 --- /dev/null +++ b/src/goto-programs/add_malloc_may_fail_variable_initializations.h @@ -0,0 +1,20 @@ +/// \file +/// \author Diffblue Ltd. +/// Adds an instrumentation to add initialisations for variables +/// used by the --malloc-may-fail and related flags in cbmc + +// NOLINT(whitespace/line_length) +#ifndef CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H +// NOLINT(whitespace/line_length) +#define CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H + +class goto_modelt; + +/// Some variables have different initial values based on what flags are being +/// passed to cbmc; since the _start function might've been generated by goto-cc +/// before getting passed over here we need to add the initialisation of these +/// variables here as a post-processing step +void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model); + +// NOLINT(whitespace/line_length) +#endif // CPROVER_GOTO_PROGRAMS_ADD_MALLOC_MAY_FAIL_VARIABLE_INITIALIZATIONS_H From e0eee9df4709fd41969b826ed93bd04e33a98705 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 21 Sep 2020 16:06:05 +0100 Subject: [PATCH 2/3] Fix constant_propagation tests These constant_propagation tests expect specific numbers of assignments. Since we changed around how we initialize the variables for the --malloc-may-fail feature these numbers have changed. --- regression/goto-analyzer/constant_propagation_01/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_02/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_03/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_04/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_07/test.desc | 4 ++-- regression/goto-analyzer/constant_propagation_12/test.desc | 4 ++-- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 04d1b4716c0..ff04300c5c0 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index e315b641f52..1aed1891945 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index e315b641f52..1aed1891945 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index e315b641f52..1aed1891945 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 9d08d672a02..71416697fd4 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 14, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index ae3f57fbdf2..50879584471 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ -- ^warning: ignoring From aea6b8ed14979e12c2c7a28b9eeded6fc8697e3a Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 22 Sep 2020 17:02:55 +0100 Subject: [PATCH 3/3] Add commented out code relating to --malloc-may-fail MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also add some explanation for why it’s commented out --- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 ++++ src/goto-analyzer/goto_analyzer_parse_options.cpp | 8 +++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 3677bf0084f..ac670796907 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -726,6 +726,10 @@ int jbmc_parse_optionst::get_goto_program( goto_modelt &goto_model = dynamic_cast(*goto_model_ptr); + // if we added the ansi-c library models here this should also call + // add_malloc_may_fail_variable_initializations(goto_model); + // here + if(cmdline.isset("validate-goto-model")) { goto_model.validate(); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 46797cb55f9..57236b4a6dd 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -814,7 +815,12 @@ bool goto_analyzer_parse_optionst::process_goto_program( link_to_library( goto_model, ui_message_handler, cprover_cpp_library_factory); link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); - #endif + + // these are commented out as well because without the library + // this initialization code doesn’t make any sense + add_malloc_may_fail_variable_initializations(goto_model); + +#endif // remove function pointers log.status() << "Removing function pointers and virtual functions"