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..cfadbde5334 --- /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-array 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..e7ea9e0461c --- /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-array 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..2bce5103c1b --- /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-array 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..b12808c84b9 --- /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-array 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..a373a72b9c0 --- /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-array 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/regression/cbmc/pointer-to-string-function-parameters/test.c b/regression/cbmc/pointer-to-string-function-parameters/test.c new file mode 100644 index 00000000000..c3a0e18f4cd --- /dev/null +++ b/regression/cbmc/pointer-to-string-function-parameters/test.c @@ -0,0 +1,14 @@ +#include +#include +#include + +int test(char *string, size_t size) +{ + for(size_t ix = 0; ix + 1 < size; ++ix) + { + char c = string[ix]; + // characters except the last should fall in printable range + assert(c == '\n' | c == '\r' | c == '\t' | (c >= 32 && c <= 126)); + } + assert(strlen(string) + 1 == size); +} diff --git a/regression/cbmc/pointer-to-string-function-parameters/test.desc b/regression/cbmc/pointer-to-string-function-parameters/test.desc new file mode 100644 index 00000000000..d041f1c399d --- /dev/null +++ b/regression/cbmc/pointer-to-string-function-parameters/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--function test --pointers-to-treat-as-string string --associated-array-sizes string:size --pointer-check --unwind 10 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index f20aa252c73..f8b260e02ab 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -67,7 +67,6 @@ rm Union_Initialization1/test.desc rm address_space_size_limit1/test.desc rm address_space_size_limit3/test.desc rm argv1/test.desc -rm argv1/test.desc rm array-function-parameters/test.desc rm array-tests/test.desc rm bounds_check1/test.desc @@ -93,6 +92,14 @@ 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 struct10/test.desc diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 49854ae2121..9c551a6b823 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 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 should be the name\n" /* NOLINT(*) */ \ + " of an array pointer \n" \ + " (see --pointers-to-treat-as-array),\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(*) */ \ + " --pointers-to-treat-as-string \n" \ + " comma separated list of identifiers that\n" \ + " should be treated like C strings\n" // clang-format on class ansi_c_languaget:public languaget diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 909fd098bf7..c96eb8550cb 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -13,16 +13,21 @@ Author: Diffblue Ltd. #include +#include #include #include #include #include #include +#include #include #include #include #include +#include +#include +#include class symbol_factoryt { @@ -31,6 +36,7 @@ class symbol_factoryt const source_locationt &loc; namespacet ns; const c_object_factory_parameterst &object_factory_params; + std::map &deferred_array_sizes; typedef std::set recursion_sett; @@ -39,12 +45,14 @@ class symbol_factoryt std::vector &_symbols_created, 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) : symbols_created(_symbols_created), symbol_table(_symbol_table), loc(loc), ns(_symbol_table), - object_factory_params(object_factory_params) + object_factory_params(object_factory_params), + deferred_array_sizes(deferred_array_sizes) {} exprt allocate_object( @@ -53,24 +61,95 @@ class symbol_factoryt const typet &allocate_type, const bool static_lifetime); + void gen_array_allocation( + code_blockt &assignments, + const exprt &array_expr, + const exprt &size); + + /// 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, const std::size_t depth = 0, recursion_sett recursion_set = recursion_sett()); + 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); + + void gen_nondet_string_member_initialization( + code_blockt &assignments, + const exprt &array, + const exprt &array_size, + std::size_t depth, + const recursion_sett &recursion_set); + private: - /// Generate initialisation code for each array element - /// \param assignments: The code block to add code to - /// \param expr: An expression of array type - /// \param depth: The struct recursion depth - /// \param recursion_set: The struct recursion set - /// \see gen_nondet_init For the meaning of the last 2 parameters + /// Add a new variable symbol to the symbol table + /// \param type: The type of the new variable + /// \param prefix: This forms the first part of the parameter, + /// for debugging purposes must be a valid identifier prefix + /// \return A reference to the newly created symbol table entry + symbolt &new_tmp_symbol(const typet &type, const std::string &prefix); void gen_nondet_array_init( code_blockt &assignments, const exprt &expr, std::size_t depth, const recursion_sett &recursion_set); + + 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 + /// (TODO: Should probably just be a plain exprt to allow + /// arbitrarily nested expressions) + /// \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); + + /// 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 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; }; /// Create a symbol for a pointer to point to @@ -133,9 +212,52 @@ 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; + if(object_factory_params.should_be_treated_as_string(symbol_name)) + { + gen_array_initialization = std::bind( + &symbol_factoryt::gen_nondet_string_member_initialization, + this, + _1, + _2, + _3, + _4, + _5); + } + else + { + 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=ns.follow(pointer_type.subtype()); + const pointer_typet &pointer_type = to_pointer_type(type); + const typet &subtype = ns.follow(pointer_type.subtype()); if(subtype.id() == ID_struct) { @@ -228,11 +350,92 @@ 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) + { + auto const &symbol_expr = to_symbol_expr(expr); + auto const associated_array_size = + get_deferred_size(get_symbol_base_name(symbol_expr)); + if(associated_array_size.has_value()) + { + assign.rhs() = typecast_exprt{ + symbol_table.lookup_ref(associated_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); + // for(size_t ix = 0; ix < size; ++ix) { + // array[ix] = nondet_init_T(); + // } + 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 = + new_tmp_symbol(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.symbol_expr(), + bool_typet{}}, + binary_exprt{size_symbol.symbol_expr(), + ID_le, + from_integer(max_array_size, size_type()), + bool_typet{}}}}; + + assignments.add(size_initialization); + gen_array_allocation(assignments, array, size_symbol.symbol_expr()); + gen_array_initialization( + assignments, array, size_symbol.symbol_expr(), 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.symbol_expr(), + 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.base_name); + } + } +} + void symbol_factoryt::gen_nondet_array_init( code_blockt &assignments, const exprt &expr, @@ -252,6 +455,270 @@ void symbol_factoryt::gen_nondet_array_init( } } +symbolt & +symbol_factoryt::new_tmp_symbol(const typet &type, const std::string &prefix) +{ + auto &symbol = get_fresh_aux_symbol( + type, + id2string(object_factory_params.function_id), + prefix, + loc, + ID_C, + symbol_table); + symbols_created.push_back(&symbol); + return symbol; +} + +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); +} + +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 = new_tmp_symbol(size_type(), "index"); + auto array_member_init = code_fort{}; + + array_member_init.init() = code_assignt{array_index_symbol.symbol_expr(), + from_integer(0, size_type())}; + + array_member_init.cond() = binary_exprt{ + array_index_symbol.symbol_expr(), 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.symbol_expr(), array.type()}}, + depth, + recursion_set); + array_member_init_body.add( + code_assignt{array_index_symbol.symbol_expr(), + plus_exprt{array_index_symbol.symbol_expr(), + from_integer(1, size_type()), + size_type()}}); + array_member_init.body() = std::move(array_member_init_body); + assignments.add(std::move(array_member_init)); +} + +void symbol_factoryt::gen_nondet_string_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 + 1 < array_size; ++ix) { + // assume(arr[ix] == '\n' + // || arr[ix] == '\t' + // || arr[ix] == '\r' + // || (32 <= arr[ix] && arr[ix] <= 126)); + // } + + auto const &array_index_symbol = + new_tmp_symbol(size_type(), CPROVER_PREFIX "array_index"); + auto array_member_init = code_fort{}; + + array_member_init.init() = code_assignt{array_index_symbol.symbol_expr(), + from_integer(0, size_type())}; + + array_member_init.cond() = binary_exprt{ + plus_exprt{array_index_symbol.symbol_expr(), from_integer(1, size_type())}, + ID_lt, + array_size, + bool_typet{}}; + + auto const array_member = dereference_exprt{ + plus_exprt{array, array_index_symbol.symbol_expr(), array.type()}}; + + auto array_member_init_body = code_blockt{}; + array_member_init_body.add(code_assumet{typecast_exprt{ + bitor_exprt{ + typecast_exprt{equal_exprt{array_member, from_integer('\n', char_type())}, + signed_int_type()}, + bitor_exprt{ + typecast_exprt{ + equal_exprt{array_member, from_integer('\t', char_type())}, + signed_int_type()}, + bitor_exprt{ + typecast_exprt{ + equal_exprt{array_member, from_integer('\r', char_type())}, + signed_int_type()}, + bitand_exprt{typecast_exprt{ + binary_relation_exprt{ + from_integer(32, char_type()), ID_le, array_member}, + signed_int_type()}, + typecast_exprt{ + binary_relation_exprt{ + array_member, ID_le, from_integer(126, char_type())}, + signed_int_type()}}, + }}}, + bool_typet{}}}); + array_member_init_body.add( + code_assignt{array_index_symbol.symbol_expr(), + plus_exprt{array_index_symbol.symbol_expr(), + from_integer(1, size_type()), + size_type()}}); + array_member_init.body() = std::move(array_member_init_body); + assignments.add(std::move(array_member_init)); + + // array[array_size - 1] = '\0'; + assignments.add( + code_assignt{dereference_exprt{plus_exprt{ + array, + minus_exprt{array_size, from_integer(1, size_type())}, + array.type()}}, + from_integer(0, char_type())}); +} + +const symbolt & +symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name) +{ + 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; + + 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(); + }; + + 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); + 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(); + + auto const malloc_res = + declare_local_variable("malloc_res", pointer_type(void_type())); + 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}); + 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()}}); + auto const record_malloc = + declare_local_variable("record_malloc", bool_typet{}); + malloc_body.add( + code_assignt{record_malloc, get_nondet_bool(bool_typet{}, loc)}); + 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}}); + 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}}); + 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()}}); + + 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)}); + 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()}}); + malloc_body.add(code_returnt{malloc_res}); + + malloc_sym.value = malloc_body; + auto inserted_sym = symbol_table.insert(malloc_sym); + 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. @@ -262,6 +729,8 @@ void symbol_factoryt::gen_nondet_array_init( /// \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, @@ -269,7 +738,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); @@ -292,7 +762,11 @@ symbol_exprt c_nondet_symbol_factory( symbols_created.push_back(main_symbol_ptr); symbol_factoryt state( - symbols_created, symbol_table, loc, object_factory_parameters); + symbols_created, + 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 diff --git a/src/ansi-c/c_object_factory_parameters.cpp b/src/ansi-c/c_object_factory_parameters.cpp index 4634dc5aeee..95ff6bf9aae 100644 --- a/src/ansi-c/c_object_factory_parameters.cpp +++ b/src/ansi-c/c_object_factory_parameters.cpp @@ -8,7 +8,141 @@ Author: Daniel Poetzl #include "c_object_factory_parameters.h" +#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-array")) + { + options.set_option( + "pointers-to-treat-as-array", + cmdline.get_comma_separated_values("pointers-to-treat-as-array")); + } + if(cmdline.isset("pointers-to-treat-as-string")) + { + options.set_option( + "pointers-to-treat-as-string", + cmdline.get_comma_separated_values("pointers-to-treat-as-string")); + } + 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")); + } +} + +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() || + should_be_treated_as_string(id); +} + +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-array"); + 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); + + auto const &pointers_to_treat_as_string = + options.get_list_option("pointers-to-treat-as-string"); + std::transform( + std::begin(pointers_to_treat_as_string), + std::end(pointers_to_treat_as_string), + std::inserter( + this->pointers_to_treat_as_string, + this->pointers_to_treat_as_string.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_string( + irep_idt id) const +{ + return pointers_to_treat_as_string.find(id) != + pointers_to_treat_as_string.end(); } diff --git a/src/ansi-c/c_object_factory_parameters.h b/src/ansi-c/c_object_factory_parameters.h index 5a2460222b1..a8bd9386b78 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,21 @@ 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 should_be_treated_as_string(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; + std::set pointers_to_treat_as_string; }; /// Parse the c object factory parameters from a given command line 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 &);