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/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 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-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" 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