From bff5630097e73ada442ffc299b0899308ec51e48 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 9 Jan 2019 11:43:38 +0000 Subject: [PATCH 1/4] Add a helper function that behaves like malloc in GOTO This adds a function that generates a malloc function that replicates the behaviour of malloc from CBMCs stdlib implementation. This is useful in situations in which we can't rely on malloc being present. --- src/ansi-c/c_nondet_symbol_factory.cpp | 143 +++++++++++++++++++++++++ 1 file changed, 143 insertions(+) diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index ddb9162eb7c..0460356d459 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -48,6 +48,11 @@ class symbol_factoryt allocate_objects(ID_C, loc, loc.get_function(), symbol_table) {} + /// Generate a function that behaves like malloc from our stdlib + /// implementation + /// \param malloc_symbol_name The name of the malloc function + const symbolt &gen_malloc_function(const irep_idt &malloc_symbol_name); + void gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -211,6 +216,144 @@ void symbol_factoryt::gen_nondet_array_init( } } +const symbolt & +symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name) +{ + // the name passed in as parameter should not exist in the symbol + // table already + PRECONDITION(symbol_table.lookup(malloc_symbol_name) == nullptr); + + auto source_location = source_locationt{}; + source_location.set_file( + ""); + symbolt malloc_sym; + malloc_sym.base_name = malloc_sym.name = malloc_sym.pretty_name = + malloc_symbol_name; + malloc_sym.mode = "C"; + + auto malloc_body = code_blockt{}; + malloc_body.add_source_location() = source_location; + + // create a new local variable with this name and type, and return + // a symbol_expr that represents this variable + auto declare_local_variable = [&]( + const std::string &name, const typet &type) { + auto const local_id = irep_idt{id2string(malloc_symbol_name) + "::" + name}; + auto local_sym = symbolt{}; + local_sym.type = type; + local_sym.pretty_name = name; + local_sym.name = id2string(local_id); + local_sym.base_name = name; + local_sym.is_lvalue = false; + local_sym.is_static_lifetime = false; + local_sym.is_type = false; + local_sym.mode = "C"; + symbol_table.insert(local_sym); + malloc_body.add(code_declt{local_sym.symbol_expr()}); + return local_sym.symbol_expr(); + }; + + // declare the parameter `size_t malloc_size` for malloc + auto malloc_size_param_symbol = symbolt{}; + malloc_size_param_symbol.type = size_type(); + malloc_size_param_symbol.name = + id2string(malloc_symbol_name) + "::malloc_size"; + malloc_size_param_symbol.pretty_name = "malloc_size"; + malloc_size_param_symbol.base_name = "malloc_size"; + malloc_size_param_symbol.is_static_lifetime = false; + malloc_size_param_symbol.is_parameter = true; + symbol_table.insert(malloc_size_param_symbol); + auto malloc_size_param = code_typet::parametert{size_type()}; + malloc_size_param.set_base_name("malloc_size"); + malloc_size_param.set_identifier(malloc_size_param_symbol.name); + + // the signature for our malloc is + // void *__CPROVER_malloc(size_t malloc_size); + malloc_sym.type = code_typet{code_typet::parameterst{malloc_size_param}, + pointer_type(void_type())}; + + auto const &local_size_variable = malloc_size_param_symbol.symbol_expr(); + + // the variable that holds the allocation result, i.e. a valid void* + // that points to a memory region of malloc_size bytes + // void *malloc_res = __CPROVER_allocate(malloc_size, 0); + auto const malloc_res = + declare_local_variable("malloc_res", pointer_type(void_type())); + + // the actual allocation + auto malloc_allocate = side_effect_exprt{ID_allocate}; + malloc_allocate.copy_to_operands(local_size_variable); + malloc_allocate.copy_to_operands(false_exprt{}); + malloc_body.add(code_assignt{malloc_res, malloc_allocate}); + + // the following are all setting various CBMC book-keeping variables + + // __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated; + auto const &cprover_deallocated = + symbol_table.lookup_ref(CPROVER_PREFIX "deallocated"); + malloc_body.add(code_assignt{ + cprover_deallocated.symbol_expr(), + if_exprt{equal_exprt{malloc_res, cprover_deallocated.symbol_expr()}, + from_integer(0, cprover_deallocated.type), + cprover_deallocated.symbol_expr()}}); + + // __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); + auto const record_malloc = + declare_local_variable("record_malloc", bool_typet{}); + malloc_body.add( + code_assignt{record_malloc, get_nondet_bool(bool_typet{}, loc)}); + + // __CPROVER_malloc_object=record_malloc?malloc_res:__CPROVER_malloc_object; + auto const &malloc_object = + symbol_table.lookup_ref(CPROVER_PREFIX "malloc_object"); + malloc_body.add(code_assignt{malloc_object.symbol_expr(), + if_exprt{record_malloc, + malloc_res, + malloc_object.symbol_expr(), + malloc_object.type}}); + + // __CPROVER_malloc_size=record_malloc?malloc_size:__CPROVER_malloc_size; + auto const &malloc_size = + symbol_table.lookup_ref(CPROVER_PREFIX "malloc_size"); + malloc_body.add(code_assignt{malloc_size.symbol_expr(), + if_exprt{record_malloc, + local_size_variable, + malloc_size.symbol_expr(), + malloc_size.type}}); + + // __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array; + auto const &malloc_is_new_array = + symbol_table.lookup_ref(CPROVER_PREFIX "malloc_is_new_array"); + malloc_body.add(code_assignt{ + malloc_is_new_array.symbol_expr(), + if_exprt{record_malloc, false_exprt{}, malloc_is_new_array.symbol_expr()}}); + + // __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool(); + auto const record_may_leak = + declare_local_variable("record_may_leak", bool_typet{}); + malloc_body.add(code_declt{record_may_leak}); + malloc_body.add( + code_assignt{record_may_leak, get_nondet_bool(bool_typet{}, loc)}); + + // __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak; + auto const &memory_leak = + symbol_table.lookup_ref(CPROVER_PREFIX "memory_leak"); + malloc_body.add(code_assignt{ + memory_leak.symbol_expr(), + if_exprt{record_may_leak, malloc_res, memory_leak.symbol_expr()}}); + + // return malloc_res; + malloc_body.add(code_returnt{malloc_res}); + + malloc_sym.value = malloc_body; + auto inserted_sym = symbol_table.insert(malloc_sym); + + // since the function is only called when there's no symbol with + // malloc_sym.name already in the symbol table, inserting it does succeed + CHECK_RETURN(inserted_sym.second); + return inserted_sym.first; +} + /// Creates a symbol and generates code so that it can vary over all possible /// values for its type. For pointers this involves allocating symbols which it /// can point to. From 6a700f6239e69bd0597e893eefef3f634a75c295 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 10 Jan 2019 13:27:52 +0000 Subject: [PATCH 2/4] Make object_factory_parameters::set virtual This enables derived classes to implement their own language specific options --- src/util/object_factory_parameters.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/object_factory_parameters.h b/src/util/object_factory_parameters.h index 1904205ff30..8f52e42e9e6 100644 --- a/src/util/object_factory_parameters.h +++ b/src/util/object_factory_parameters.h @@ -77,7 +77,7 @@ struct object_factory_parameterst irep_idt function_id; /// Assigns the parameters from given options - void set(const optionst &); + virtual void set(const optionst &); }; void parse_object_factory_options(const cmdlinet &, optionst &); From 849aca883fe92302151ceb7a049bae2ef5c4eb41 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 10 Jan 2019 13:27:16 +0000 Subject: [PATCH 3/4] Add option handling for dynamic array initialisation Adds the --pointers-to-treat-as-arrays --associated-array-sizes --max-dynamic-array-size options. The intended behaviour is that the former should indicate which of the function parameters to an entry function that are pointers should be backed by an array, the parameter that should hold the size of that array (if any) and the maximum size of such an array (minimum 1) respectively. These options currently have no effect and will be implemented in a later commit --- src/ansi-c/ansi_c_language.h | 17 +++- src/ansi-c/c_object_factory_parameters.cpp | 111 +++++++++++++++++++++ src/ansi-c/c_object_factory_parameters.h | 17 ++++ 3 files changed, 143 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index d554dbb9d0c..724aa76071b 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -22,13 +22,26 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #define OPT_ANSI_C_LANGUAGE \ "(max-nondet-tree-depth):" \ - "(min-null-tree-depth):" + "(min-null-tree-depth):" \ + "(pointers-to-treat-as-arrays):" \ + "(associated-array-sizes):" \ + "(max-dynamic-array-size):" \ #define HELP_ANSI_C_LANGUAGE \ " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\ " at level N pointers are set to null\n" \ " --min-null-tree-depth N minimum level at which a pointer can first be\n" /* NOLINT(*) */\ - " NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */ + " NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */\ + " --pointers-to-treat-as-arrays comma separated list of\n" \ + " identifiers that should be initialized as arrays\n" /* NOLINT(*) */ \ + " --associated-array-sizes \n" \ + " comma separated list of colon separated pairs\n" /* NOLINT(*) */ \ + " of identifiers; The first element of the pair \n" /* NOLINT(*) */ \ + " should be the name of an array pointer \n" \ + " (see --pointers-to-treat-as-arrays),\n" \ + " the second an integer parameter that\n" \ + " should hold its size\n" \ + " --max-dynamic-array-size max size for dynamically allocated arrays\n" /* NOLINT(*) */ // clang-format on class ansi_c_languaget:public languaget diff --git a/src/ansi-c/c_object_factory_parameters.cpp b/src/ansi-c/c_object_factory_parameters.cpp index 4634dc5aeee..0f06d70aa4a 100644 --- a/src/ansi-c/c_object_factory_parameters.cpp +++ b/src/ansi-c/c_object_factory_parameters.cpp @@ -8,7 +8,118 @@ Author: Daniel Poetzl #include "c_object_factory_parameters.h" +#include +#include +#include +#include + +#include +#include +#include + void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options) { parse_object_factory_options(cmdline, options); + if(cmdline.isset("pointers-to-treat-as-arrays")) + { + options.set_option( + "pointers-to-treat-as-arrays", + cmdline.get_comma_separated_values("pointers-to-treat-as-arrays")); + } + if(cmdline.isset("associated-array-sizes")) + { + options.set_option( + "associated-array-sizes", + cmdline.get_comma_separated_values("associated-array-sizes")); + } + if(cmdline.isset("max-dynamic-array-size")) + { + options.set_option( + "max-dynamic-array-size", cmdline.get_value("max-dynamic-array-size")); + } +} + +void c_object_factory_parameterst::set(const optionst &options) +{ + object_factory_parameterst::set(options); + auto const &pointers_to_treat_as_array = + options.get_list_option("pointers-to-treat-as-arrays"); + std::transform( + std::begin(pointers_to_treat_as_array), + std::end(pointers_to_treat_as_array), + std::inserter( + this->pointers_to_treat_as_array, this->pointers_to_treat_as_array.end()), + id2string); + + if(options.is_set("max-dynamic-array-size")) + { + max_dynamic_array_size = + options.get_unsigned_int_option("max-dynamic-array-size"); + if(max_dynamic_array_size == 0) + { + throw invalid_command_line_argument_exceptiont( + "Max dynamic array size must be >= 1", "--max-dynamic-array-size"); + } + } + if(options.is_set("associated-array-sizes")) + { + array_name_to_associated_array_size_variable.clear(); + variables_that_hold_array_sizes.clear(); + auto const &array_size_pairs = + options.get_list_option("associated-array-sizes"); + for(auto const &array_size_pair : array_size_pairs) + { + std::string array_name; + std::string size_name; + try + { + split_string(array_size_pair, ':', array_name, size_name); + } + catch(const deserialization_exceptiont &e) + { + throw invalid_command_line_argument_exceptiont{ + "can't parse parameter value", + "--associated-array-sizes", + "pairs of array/size parameter names, separated by a ':' colon"}; + } + auto const mapping_insert_result = + array_name_to_associated_array_size_variable.insert( + {irep_idt{array_name}, irep_idt{size_name}}); + if(!mapping_insert_result.second) + { + throw invalid_command_line_argument_exceptiont{ + "duplicate associated size entries for array `" + array_name + + "', existing: `" + id2string(mapping_insert_result.first->second) + + "', tried to insert: `" + size_name + "'", + "--associated-array-sizes"}; + } + auto const size_name_insert_result = + variables_that_hold_array_sizes.insert(irep_idt{size_name}); + if(!size_name_insert_result.second) + { + throw invalid_command_line_argument_exceptiont{ + "using size parameter `" + size_name + "' more than once", + "--associated-array-sizes"}; + } + } + } +} + +bool c_object_factory_parameterst::is_array_size_parameter(irep_idt id) const +{ + return variables_that_hold_array_sizes.find(id) != + end(variables_that_hold_array_sizes); +} + +optionalt c_object_factory_parameterst::get_associated_size_variable( + irep_idt array_id) const +{ + return optional_lookup( + array_name_to_associated_array_size_variable, array_id); +} + +bool c_object_factory_parameterst::should_be_treated_as_array(irep_idt id) const +{ + return pointers_to_treat_as_array.find(id) != + pointers_to_treat_as_array.end(); } diff --git a/src/ansi-c/c_object_factory_parameters.h b/src/ansi-c/c_object_factory_parameters.h index 1da85f407ec..cc338bd830c 100644 --- a/src/ansi-c/c_object_factory_parameters.h +++ b/src/ansi-c/c_object_factory_parameters.h @@ -9,7 +9,11 @@ Author: Daniel Poetzl #ifndef CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H #define CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H +#include +#include #include +#include +#include struct c_object_factory_parameterst final : public object_factory_parameterst { @@ -21,6 +25,19 @@ struct c_object_factory_parameterst final : public object_factory_parameterst : object_factory_parameterst(options) { } + + bool should_be_treated_as_array(irep_idt id) const; + bool is_array_size_parameter(irep_idt id) const; + optionalt get_associated_size_variable(irep_idt array_id) const; + + void set(const optionst &options) override; + + std::size_t max_dynamic_array_size = 2; + +private: + std::set pointers_to_treat_as_array; + std::set variables_that_hold_array_sizes; + std::map array_name_to_associated_array_size_variable; }; /// Parse the c object factory parameters from a given command line From 14e883344037b9f9bfa6dd0395b1348e98dad721 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 10 Jan 2019 13:35:36 +0000 Subject: [PATCH 4/4] Implement initialization of dynamic array parameters This implements the behaviour of the --pointers-to-treat-as-arrays --associated-array-sizes --max-dynamic-array-size options. --- .../test.c | 9 + .../test.desc | 12 + .../test.c | 22 ++ .../test.desc | 6 + .../test.c | 24 ++ .../test.desc | 7 + .../test.c | 7 + .../test.desc | 11 + .../test.c | 10 + .../test.desc | 6 + scripts/delete_failing_smt2_solver_tests | 11 + src/ansi-c/ansi_c_entry_point.cpp | 5 +- src/ansi-c/c_nondet_symbol_factory.cpp | 275 +++++++++++++++++- src/ansi-c/c_nondet_symbol_factory.h | 5 +- 14 files changed, 400 insertions(+), 10 deletions(-) create mode 100644 regression/cbmc/pointer-to-array-function-parameters-max-size/test.c create mode 100644 regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc create mode 100644 regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c create mode 100644 regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc create mode 100644 regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c create mode 100644 regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc create mode 100644 regression/cbmc/pointer-to-array-function-parameters-with-size/test.c create mode 100644 regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc create mode 100644 regression/cbmc/pointer-to-array-function-parameters/test.c create mode 100644 regression/cbmc/pointer-to-array-function-parameters/test.desc diff --git a/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c new file mode 100644 index 00000000000..ae83a9f6c48 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.c @@ -0,0 +1,9 @@ +#include +void test(int *arr, int sz) +{ + assert(sz <= 10); + for(int i = 0; i < sz; ++i) + { + arr[i] = 0; + } +} diff --git a/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc new file mode 100644 index 00000000000..eaddb5de044 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-max-size/test.desc @@ -0,0 +1,12 @@ +CORE +test.c +--function test --pointers-to-treat-as-arrays arr --max-dynamic-array-size 20 --pointer-check --unwind 20 --associated-array-sizes arr:sz +\[test.assertion.1\] line \d+ assertion sz <= 10: FAILURE +\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS +EXIT=10 +SIGNAL=0 diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c new file mode 100644 index 00000000000..3afac1ef068 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.c @@ -0,0 +1,22 @@ +#include + +int is_prefix_of( + const char *string, + int string_size, + const char *prefix, + int prefix_size) +{ + if(string_size < prefix_size) + { + return 0; + } + + for(int ix = 0; ix < prefix_size; ++ix) + { + if(string[ix] != prefix[ix]) + { + return 0; + } + } + return 1; +} diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc new file mode 100644 index 00000000000..29a23f608ca --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 20 +SIGNAL=0 +EXIT=0 +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c new file mode 100644 index 00000000000..6500af4f123 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.c @@ -0,0 +1,24 @@ +#include +#include + +int is_prefix_of( + const char *string, + size_t string_size, + const char *prefix, + size_t prefix_size) +{ + if(string_size < prefix_size) + { + return 0; + } + assert(prefix_size <= string_size); + // oh no! we should have used prefix_size here + for(int ix = 0; ix < string_size; ++ix) + { + if(string[ix] != prefix[ix]) + { + return 0; + } + } + return 1; +} diff --git a/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc new file mode 100644 index 00000000000..280b5c4c832 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 10 +EXIT=10 +SIGNAL=0 +\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE +VERIFICATION FAILED diff --git a/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c new file mode 100644 index 00000000000..436baadd23d --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.c @@ -0,0 +1,7 @@ +void test(int *arr, int sz) +{ + for(int i = 0; i < sz; ++i) + { + arr[i] = 0; + } +} diff --git a/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc new file mode 100644 index 00000000000..18faa5c7c81 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters-with-size/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 10 --associated-array-sizes arr:sz +EXIT=0 +SIGNAL=0 +\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS diff --git a/regression/cbmc/pointer-to-array-function-parameters/test.c b/regression/cbmc/pointer-to-array-function-parameters/test.c new file mode 100644 index 00000000000..f70cbfbae28 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters/test.c @@ -0,0 +1,10 @@ +#include + +void test(int *arr) +{ + // works because the arrays we generate have at least one element + arr[0] = 5; + + // doesn't work because our arrays have at most ten elements + arr[10] = 10; +} diff --git a/regression/cbmc/pointer-to-array-function-parameters/test.desc b/regression/cbmc/pointer-to-array-function-parameters/test.desc new file mode 100644 index 00000000000..079e897d7b4 --- /dev/null +++ b/regression/cbmc/pointer-to-array-function-parameters/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 20 +\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS +\[test.pointer_dereference.12\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE +-- diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index 9453c077af4..eec59ce3ef5 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -49,6 +49,8 @@ rm Quantifiers-invalid-var-range/test.desc rm Quantifiers-type/test.desc rm Union_Initialization1/test.desc rm address_space_size_limit1/test.desc +rm address_space_size_limit3/test.desc +rm argv1/test.desc rm array-function-parameters/test.desc rm array-tests/test.desc rm bounds_check1/test.desc @@ -68,6 +70,15 @@ rm memory_allocation1/test.desc rm pointer-function-parameters-struct-mutual-recursion/test.desc rm pointer-function-parameters-struct-simple-recursion/test.desc rm pointer-function-parameters-struct-simple-recursion-2/test.desc +rm pointer-function-parameters-struct-simple-recursion-3/test.desc +rm pointer-to-array-function-parameters-max-size/test.desc +rm pointer-to-array-function-parameters-multi-arg-right/test.desc +rm pointer-to-array-function-parameters-multi-arg-wrong/test.desc +rm pointer-to-array-function-parameters-with-size/test.desc +rm pointer-to-array-function-parameters/test.desc +rm read1/test.desc +rm realloc1/test.desc +rm realloc2/test.desc rm scanf1/test.desc rm stack-trace/test.desc rm struct6/test.desc diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index a6ce51d967a..03df46ccf11 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -27,7 +27,7 @@ exprt::operandst build_function_environment( { exprt::operandst main_arguments; main_arguments.resize(parameters.size()); - + std::map deferred_array_sizes; for(std::size_t param_number=0; param_number #include +#include #include #include #include #include +#include +#include +#include #include #include #include #include +#include + class symbol_factoryt { symbol_tablet &symbol_table; const source_locationt &loc; namespacet ns; const c_object_factory_parameterst &object_factory_params; - allocate_objectst allocate_objects; + std::map &deferred_array_sizes; typedef std::set recursion_sett; @@ -40,12 +46,14 @@ class symbol_factoryt symbol_factoryt( symbol_tablet &_symbol_table, const source_locationt &loc, - const c_object_factory_parameterst &object_factory_params) + const c_object_factory_parameterst &object_factory_params, + std::map &deferred_array_sizes) : symbol_table(_symbol_table), loc(loc), ns(_symbol_table), object_factory_params(object_factory_params), - allocate_objects(ID_C, loc, loc.get_function(), symbol_table) + allocate_objects(ID_C, loc, loc.get_function(), symbol_table), + deferred_array_sizes(deferred_array_sizes) {} /// Generate a function that behaves like malloc from our stdlib @@ -53,6 +61,11 @@ class symbol_factoryt /// \param malloc_symbol_name The name of the malloc function const symbolt &gen_malloc_function(const irep_idt &malloc_symbol_name); + void gen_array_allocation( + code_blockt &assignments, + const exprt &array_expr, + const exprt &size); + void gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -86,6 +99,62 @@ class symbol_factoryt const exprt &expr, std::size_t depth, const recursion_sett &recursion_set); + + /// Type for functions that initialise array elements + /// \see gen_nondet_size_array_init + using gen_array_initialization_t = std::function; + + /// Generate code to nondet-initialize each element of an array + /// \param assignments: The code block the initialization statements + /// are written to + /// \param array: The expression representing the array type + /// \param depth: Struct initialisation recursion depth, \see gen_nondet_init + /// \param recursion_set: Struct initialisation recursion set + /// \param gen_array_initialization: A function that generates + /// initialisation code for array members + void gen_nondet_size_array_init( + code_blockt &assignments, + const symbol_exprt &array, + const size_t depth, + const symbol_factoryt::recursion_sett &recursion_set, + const gen_array_initialization_t &gen_array_initialization); + + /// Initialize each element of an array to nondet + /// \see gen_array_initialization_t + void gen_nondet_array_member_initialization( + code_blockt &assignments, + const exprt &array, + const exprt &array_size, + std::size_t depth, + const recursion_sett &recursion_set); + + /// Remember to initialise a variable representing array size to the given + /// concrete size. + /// When generating array initialisation code we often have the case where we + /// have a pointer that should be initialised to be pointing to some array, + /// and some integer type variable that should hold its size. Sometimes when + /// generating the array initialisation code we haven't "seen" the size + /// variable yet (i.e. it is not yet in the symbol table and doesn't have + /// initialisation code generated for it yet). If that's the case we remember + /// that we have to set it to the right size later with this method. + /// \param associated_size_name: The name of variable that should be set to + /// the right size + /// \param array_size_name: The name of the variable that holds the size + void defer_size_initialization( + irep_idt associated_size_name, + irep_idt array_size_name); + + /// Return the name of a variable holding an array size if one is associated + /// with the given symbol name + optionalt get_deferred_size(irep_idt symbol_name) const; + + /// Lookup symbol expression in symbol table and get its base name + const irep_idt &get_symbol_base_name(const symbol_exprt &symbol_expr) const; }; /// Creates a nondet for expr, including calling itself recursively to make @@ -105,6 +174,34 @@ void symbol_factoryt::gen_nondet_init( if(type.id()==ID_pointer) { + if(expr.id() == ID_symbol) + { + auto const &symbol_expr = to_symbol_expr(expr); + const auto &symbol_name = get_symbol_base_name(symbol_expr); + using std::placeholders::_1; + using std::placeholders::_2; + using std::placeholders::_3; + using std::placeholders::_4; + using std::placeholders::_5; + if(object_factory_params.should_be_treated_as_array(symbol_name)) + { + gen_array_initialization_t gen_array_initialization = std::bind( + &symbol_factoryt::gen_nondet_array_member_initialization, + this, + _1, + _2, + _3, + _4, + _5); + gen_nondet_size_array_init( + assignments, + symbol_expr, + depth, + recursion_set, + gen_array_initialization); + return; + } + } // dereferenced type const pointer_typet &pointer_type=to_pointer_type(type); const typet &subtype = pointer_type.subtype(); @@ -192,11 +289,93 @@ void symbol_factoryt::gen_nondet_init( : side_effect_expr_nondett(type, loc); code_assignt assign(expr, rhs); assign.add_source_location()=loc; - + if(expr.id() == ID_symbol) + { + // check if this variable is meant to hold the size of a + // dynamically allocated array; If it is, set the value to the length + // of that array instead of leaving it nondet + auto const &symbol_expr = to_symbol_expr(expr); + auto const deferred_array_size = + get_deferred_size(get_symbol_base_name(symbol_expr)); + if(deferred_array_size.has_value()) + { + assign.rhs() = typecast_exprt{ + symbol_table.lookup_ref(deferred_array_size.value()).symbol_expr(), + symbol_expr.type()}; + } + } assignments.add(std::move(assign)); } } +const irep_idt & +symbol_factoryt::get_symbol_base_name(const symbol_exprt &symbol_expr) const +{ + return symbol_table.lookup_ref(symbol_expr.get_identifier()).base_name; +} + +void symbol_factoryt::gen_nondet_size_array_init( + code_blockt &assignments, + const symbol_exprt &array, + const size_t depth, + const symbol_factoryt::recursion_sett &recursion_set, + const gen_array_initialization_t &gen_array_initialization) +{ + // This works on dynamic arrays, so the thing we assign to is a pointer + // rather than an array with a fixed size + PRECONDITION(array.type().id() == ID_pointer); + + // Overall, create code that roughly does this: + // size_t size; + // T *array; + // size = choose_in_range(1, max_array_size); + // array = malloc(sizeof(T) * size); + // nondet_fill_T(array, size); + // where nondet_fill_T is responsible for setting up the values of the array, + // for example nondet-initialiasing them + auto const max_array_size = object_factory_params.max_dynamic_array_size; + auto const &array_name = get_symbol_base_name(array); + auto const &size_symbol = allocate_objects.allocate_automatic_local_object( + size_type(), CPROVER_PREFIX "nondet_array_size"); + + // assume (1 <= size && size <= max_array_size) + auto size_initialization = code_assumet{ + and_exprt{binary_exprt{ + from_integer(1, size_type()), ID_le, size_symbol, bool_typet{}}, + binary_exprt{size_symbol, + ID_le, + from_integer(max_array_size, size_type()), + bool_typet{}}}}; + + assignments.add(size_initialization); + gen_array_allocation(assignments, array, size_symbol); + gen_array_initialization( + assignments, array, size_symbol, depth, recursion_set); + // if we've already initialised the associated array size, + // then set the associated array size to the size of the generated array + // otherwise, defer the initialisation of the associated array size + auto const associated_size = + object_factory_params.get_associated_size_variable(array_name); + if(associated_size.has_value()) + { + auto const associated_size_symbol = + symbol_table.lookup(associated_size.value()); + if(associated_size_symbol != nullptr) + { + assignments.add(code_assignt{ + associated_size_symbol->symbol_expr(), + typecast_exprt{size_symbol, associated_size_symbol->type}}); + } + else + { + // we've not seen the associated size symbol yet, so we have + // to defer setting it to when we do get there... + defer_size_initialization( + associated_size.value(), size_symbol.get_identifier()); + } + } +} + void symbol_factoryt::gen_nondet_array_init( code_blockt &assignments, const exprt &expr, @@ -354,6 +533,86 @@ symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name) return inserted_sym.first; } +void symbol_factoryt::defer_size_initialization( + irep_idt associated_size_name, + irep_idt array_size_name) +{ + auto succeeded = + deferred_array_sizes.insert({associated_size_name, array_size_name}); + INVARIANT( + succeeded.second, + "each size parameter should have a unique associated array"); +} + +optionalt +symbol_factoryt::get_deferred_size(irep_idt symbol_name) const +{ + return optional_lookup(deferred_array_sizes, symbol_name); +} + +/// Generates a statement that allocates an array with a certain number of +/// elements +/// \param assignments: Where the statement is being written to +/// \param array_expr: An expression representing a pointer to an array +/// \param size: The number of elements to allocate for the array +void symbol_factoryt::gen_array_allocation( + code_blockt &assignments, + const exprt &array_expr, + const exprt &size) +{ + PRECONDITION(array_expr.type().id() == ID_pointer); + irep_idt malloc_symbol_name = CPROVER_PREFIX "malloc"; + auto const *malloc_symbol = symbol_table.lookup(malloc_symbol_name); + if(!malloc_symbol) + { + malloc_symbol = &gen_malloc_function(malloc_symbol_name); + } + auto const &element_type = array_expr.type().subtype(); + const exprt &array_size = size_of_expr(array_typet{element_type, size}, ns); + + // array = malloc(sizeof(array[size])) + auto allocate_array = + side_effect_expr_function_callt{malloc_symbol->symbol_expr(), + exprt::operandst{array_size}, + array_expr.type(), + loc}; + assignments.add(code_assignt{array_expr, allocate_array}); +} + +void symbol_factoryt::gen_nondet_array_member_initialization( + code_blockt &assignments, + const exprt &array, + const exprt &array_size, + std::size_t depth, + const symbol_factoryt::recursion_sett &recursion_set) +{ + // for(size_t ix = 0; ix < size; ++ix) { + // arr[ix] = nondet_init_T(); + // } + + auto const &array_index_symbol = + allocate_objects.allocate_automatic_local_object(size_type(), "index"); + auto array_member_init = code_fort{}; + + array_member_init.init() = + code_assignt{array_index_symbol, from_integer(0, size_type())}; + + array_member_init.cond() = + binary_exprt{array_index_symbol, ID_lt, array_size, bool_typet{}}; + + auto array_member_init_body = code_blockt{}; + gen_nondet_init( + array_member_init_body, + dereference_exprt{plus_exprt{array, array_index_symbol, array.type()}}, + depth + 1, + recursion_set); + array_member_init_body.add(code_assignt{ + array_index_symbol, + plus_exprt{array_index_symbol, from_integer(1, size_type()), size_type()}}); + array_member_init.body() = std::move(array_member_init_body); + assignments.add(std::move(array_member_init)); +} + /// Creates a symbol and generates code so that it can vary over all possible /// values for its type. For pointers this involves allocating symbols which it /// can point to. @@ -364,6 +623,8 @@ symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name) /// \param loc: The location to assign to generated code /// \param object_factory_parameters: configuration parameters for the object /// factory +/// \param deferred_array_sizes: A map of size parameter name -> symbol +/// that holds the value the parameter should be assigned to /// \return Returns the symbol_exprt for the symbol created symbol_exprt c_nondet_symbol_factory( code_blockt &init_code, @@ -371,7 +632,8 @@ symbol_exprt c_nondet_symbol_factory( const irep_idt base_name, const typet &type, const source_locationt &loc, - const c_object_factory_parameterst &object_factory_parameters) + const c_object_factory_parameterst &object_factory_parameters, + std::map &deferred_array_sizes) { irep_idt identifier=id2string(goto_functionst::entry_point())+ "::"+id2string(base_name); @@ -390,7 +652,8 @@ symbol_exprt c_nondet_symbol_factory( bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr); CHECK_RETURN(!moving_symbol_failed); - symbol_factoryt state(symbol_table, loc, object_factory_parameters); + symbol_factoryt state( + symbol_table, loc, object_factory_parameters, deferred_array_sizes); code_blockt assignments; state.gen_nondet_init(assignments, main_symbol_expr); diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h index c4d74f6021f..2dd2b75dd39 100644 --- a/src/ansi-c/c_nondet_symbol_factory.h +++ b/src/ansi-c/c_nondet_symbol_factory.h @@ -22,7 +22,8 @@ symbol_exprt c_nondet_symbol_factory( symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, - const source_locationt &, - const c_object_factory_parameterst &object_factory_parameters); + const source_locationt &loc, + const c_object_factory_parameterst &object_factory_parameters, + std::map &deferred_array_sizes); #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H