diff --git a/regression/goto-harness/pointer-function-parameters-equal-maybe/main.c b/regression/goto-harness/pointer-function-parameters-equal-maybe/main.c new file mode 100644 index 00000000000..9f1b214fa77 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-equal-maybe/main.c @@ -0,0 +1,27 @@ +#include +#include + +typedef struct st1 +{ + struct st *next; + int data; +} st1_t; + +typedef struct st2 +{ + struct st *next; + int data; +} st2_t; + +void func(st1_t *p, st1_t *q, st2_t *r, st2_t *s, st2_t *t) +{ + assert(p != NULL); + assert(p->next != NULL); + + assert(p == q); + + assert((void *)p != (void *)r); + + assert(r == s); + assert(r == t); +} diff --git a/regression/goto-harness/pointer-function-parameters-equal-maybe/test.desc b/regression/goto-harness/pointer-function-parameters-equal-maybe/test.desc new file mode 100644 index 00000000000..84a96e3e99d --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-equal-maybe/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' --treat-pointers-equal-maybe +^EXIT=10$ +^SIGNAL=0$ +^\[func.assertion.\d+\] line \d+ assertion p == q: FAILURE$ +^\[func.assertion.\d+\] line \d+ assertion \(void \*\)p != \(void \*\)r: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion r == s: FAILURE$ +^\[func.assertion.\d+\] line \d+ assertion r == t: FAILURE$ +VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/main.c b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c new file mode 100644 index 00000000000..9f1b214fa77 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c @@ -0,0 +1,27 @@ +#include +#include + +typedef struct st1 +{ + struct st *next; + int data; +} st1_t; + +typedef struct st2 +{ + struct st *next; + int data; +} st2_t; + +void func(st1_t *p, st1_t *q, st2_t *r, st2_t *s, st2_t *t) +{ + assert(p != NULL); + assert(p->next != NULL); + + assert(p == q); + + assert((void *)p != (void *)r); + + assert(r == s); + assert(r == t); +} diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc new file mode 100644 index 00000000000..1f9be5e19f0 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index a470e21f6f3..b7f26a1d649 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt std::set function_parameters_to_treat_as_arrays; std::set function_arguments_to_treat_as_arrays; + std::vector> function_parameters_to_treat_equal; + std::vector> function_arguments_to_treat_equal; + std::set function_parameters_to_treat_as_cstrings; std::set function_arguments_to_treat_as_cstrings; @@ -112,6 +115,21 @@ void function_call_harness_generatort::handle_option( p_impl->function_parameters_to_treat_as_arrays.insert( values.begin(), values.end()); } + else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT) + { + for(auto const &value : values) + { + for(auto const ¶m_cluster : split_string(value, ';')) + { + std::set equal_param_set; + for(auto const ¶m_id : split_string(param_cluster, ',')) + { + equal_param_set.insert(param_id); + } + p_impl->function_parameters_to_treat_equal.push_back(equal_param_set); + } + } + } else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT) { for(auto const &array_size_pair : values) @@ -151,6 +169,10 @@ void function_call_harness_generatort::handle_option( p_impl->function_parameters_to_treat_as_cstrings.insert( values.begin(), values.end()); } + else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT) + { + p_impl->recursive_initialization_config.arguments_may_be_equal = true; + } else { throw invalid_command_line_argument_exceptiont{ @@ -183,6 +205,8 @@ void function_call_harness_generatort::implt::generate( recursive_initialization_config.mode = function_to_call.mode; recursive_initialization_config.pointers_to_treat_as_arrays = function_arguments_to_treat_as_arrays; + recursive_initialization_config.pointers_to_treat_equal = + function_arguments_to_treat_equal; recursive_initialization_config.array_name_to_associated_array_size_variable = function_argument_to_associated_array_size; for(const auto &pair : function_argument_to_associated_array_size) @@ -199,9 +223,9 @@ void function_call_harness_generatort::implt::generate( call_function(arguments, function_body); for(const auto &global_pointer : global_pointers) { - function_body.add(code_function_callt{ - recursive_initialization->get_free_function(), {global_pointer}}); + recursive_initialization->free_if_possible(global_pointer, function_body); } + recursive_initialization->free_cluster_origins(function_body); add_harness_function_to_goto_model(std::move(function_body)); } @@ -238,7 +262,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for( { recursive_initialization->initialize( lhs, from_integer(0, signed_int_type()), block); - if(lhs.type().id() == ID_pointer) + if(recursive_initialization->needs_freeing(lhs)) global_pointers.insert(to_symbol_expr(lhs)); } @@ -258,6 +282,49 @@ void function_call_harness_generatort::validate_options( "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT}; } + + auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function); + auto ftype = to_code_type(function_to_call.type); + for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal) + { + for(auto const &pointer_id : equal_cluster) + { + std::string decorated_pointer_id = + id2string(p_impl->function) + "::" + id2string(pointer_id); + bool is_a_param = false; + typet common_type = empty_typet{}; + for(auto const &formal_param : ftype.parameters()) + { + if(formal_param.get_identifier() == decorated_pointer_id) + { + is_a_param = true; + if(formal_param.type().id() != ID_pointer) + { + throw invalid_command_line_argument_exceptiont{ + id2string(pointer_id) + " is not a pointer parameter", + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT}; + } + if(common_type.id() != ID_empty) + { + if(common_type != formal_param.type()) + { + throw invalid_command_line_argument_exceptiont{ + "pointer arguments of conflicting type", + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT}; + } + } + else + common_type = formal_param.type(); + } + } + if(!is_a_param) + { + throw invalid_command_line_argument_exceptiont{ + id2string(pointer_id) + " is not a parameter", + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT}; + } + } + } } const symbolt & @@ -365,6 +432,22 @@ function_call_harness_generatort::implt::declare_arguments( {argument_name, associated_array_size_argument->second}); } } + + // translate the parameter to argument also in the equality clusters + for(auto const &equal_cluster : function_parameters_to_treat_equal) + { + std::set cluster_argument_names; + for(auto const ¶meter_name : equal_cluster) + { + INVARIANT( + parameter_name_to_argument_name.count(parameter_name) != 0, + id2string(parameter_name) + " is not a parameter"); + cluster_argument_names.insert( + parameter_name_to_argument_name[parameter_name]); + } + function_arguments_to_treat_equal.push_back(cluster_argument_names); + } + allocate_objects.declare_created_symbols(function_body); return arguments; } @@ -377,7 +460,7 @@ void function_call_harness_generatort::implt::call_function( for(auto const &argument : arguments) { generate_initialisation_code_for(function_body, argument); - if(argument.type().id() == ID_pointer) + if(recursive_initialization->needs_freeing(argument)) global_pointers.insert(to_symbol_expr(argument)); } code_function_callt function_call{function_to_call.symbol_expr(), diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 83cf1bcabac..477b53a8aff 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -15,18 +15,24 @@ Author: Diffblue Ltd. #define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals" #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ "treat-pointer-as-array" +#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ + "treat-pointers-equal" #define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ "associated-array-size" #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \ "treat-pointer-as-cstring" +#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \ + "treat-pointers-equal-maybe" // clang-format off #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \ "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):" \ + "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT ")" \ // FUNCTION_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -43,6 +49,11 @@ Author: Diffblue Ltd. "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ " p treat the function parameter with the name `p' as\n" \ " an array\n" \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ + " p,q,r[;s,t] treat the function parameters `q,r' equal\n" \ + " to parameter `p'; `s` to `t` and so on\n" \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \ + " function parameters equality is non-deterministic\n" \ "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ " array_name:size_name\n" \ " set the parameter to the size" \ diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 6193b91fbc6..537ba8c8b4d 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -93,6 +93,8 @@ recursive_initializationt::recursive_initializationt( initialization_config.min_null_tree_depth, signed_int_type()))) { + common_arguments_origins.resize( + this->initialization_config.pointers_to_treat_equal.size()); } void recursive_initializationt::initialize( @@ -100,6 +102,45 @@ void recursive_initializationt::initialize( const exprt &depth, code_blockt &body) { + // special handling for the case that pointer arguments should be treated + // equal: if the equality is enforced (rather than the pointers may be equal), + // then we don't even build the constructor functions + if(lhs.id() == ID_symbol) + { + const auto maybe_cluster_index = + find_equal_cluster(to_symbol_expr(lhs).get_identifier()); + if(maybe_cluster_index.has_value()) + { + if(common_arguments_origins[*maybe_cluster_index].has_value()) + { + const auto set_equal_case = + code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]}; + if(initialization_config.arguments_may_be_equal) + { + const irep_idt &fun_name = build_constructor(lhs); + const symbolt &fun_symbol = + goto_model.symbol_table.lookup_ref(fun_name); + const auto proper_init_case = code_function_callt{ + fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}}; + + body.add(code_ifthenelset{ + side_effect_expr_nondett{bool_typet{}, source_locationt{}}, + set_equal_case, + proper_init_case}); + } + else + { + body.add(set_equal_case); + } + return; + } + else + { + common_arguments_origins[*maybe_cluster_index] = lhs; + } + } + } + const irep_idt &fun_name = build_constructor(lhs); const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name); @@ -280,6 +321,19 @@ bool recursive_initializationt::should_be_treated_as_array( initialization_config.pointers_to_treat_as_arrays.end(); } +optionalt +recursive_initializationt::find_equal_cluster(const irep_idt &name) const +{ + for(equal_cluster_idt index = 0; + index != initialization_config.pointers_to_treat_equal.size(); + ++index) + { + if(initialization_config.pointers_to_treat_equal[index].count(name) != 0) + return index; + } + return {}; +} + bool recursive_initializationt::is_array_size_parameter( const irep_idt &cmdline_arg) const { @@ -763,3 +817,49 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( return body; } + +bool recursive_initializationt::needs_freeing(const exprt &expr) const +{ + return expr.type().id() == ID_pointer && expr.type().id() != ID_code; +} + +void recursive_initializationt::free_if_possible( + const exprt &expr, + code_blockt &body) +{ + PRECONDITION(expr.id() == ID_symbol); + const auto expr_id = to_symbol_expr(expr).get_identifier(); + const auto maybe_cluster_index = find_equal_cluster(expr_id); + const auto call_free = code_function_callt{get_free_function(), {expr}}; + if(!maybe_cluster_index.has_value()) + { + // not in any equality cluster -> just free + body.add(call_free); + return; + } + + if( + to_symbol_expr(*common_arguments_origins[*maybe_cluster_index]) + .get_identifier() != expr_id && + initialization_config.arguments_may_be_equal) + { + // in equality cluster but not common origin -> free if not equal to origin + const auto condition = + notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]}; + body.add(code_ifthenelset{condition, call_free}); + } + else + { + // expr is common origin, leave freeing until the rest of the cluster is + // freed + return; + } +} + +void recursive_initializationt::free_cluster_origins(code_blockt &body) +{ + for(auto const &origin : common_arguments_origins) + { + body.add(code_function_callt{get_free_function(), {*origin}}); + } +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 505d32d8c32..5b0dfdac37d 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -37,6 +37,9 @@ struct recursive_initialization_configt std::map array_name_to_associated_array_size_variable; std::set pointers_to_treat_as_cstrings; + std::vector> pointers_to_treat_equal; + + bool arguments_may_be_equal = false; std::string to_string() const; // for debugging purposes @@ -57,6 +60,7 @@ class recursive_initializationt public: using recursion_sett = std::set; using type_constructor_namest = std::map; + using equal_cluster_idt = std::size_t; recursive_initializationt( recursive_initialization_configt initialization_config, @@ -81,12 +85,17 @@ class recursive_initializationt !has_prefix(id2string(symbol.name), CPROVER_PREFIX)); } + bool needs_freeing(const exprt &expr) const; + void free_if_possible(const exprt &expr, code_blockt &body); + void free_cluster_origins(code_blockt &body); + private: const recursive_initialization_configt initialization_config; goto_modelt &goto_model; irep_idt max_depth_var_name; irep_idt min_depth_var_name; type_constructor_namest type_constructor_names; + std::vector> common_arguments_origins; /// Get the malloc function as symbol exprt, /// and inserts it into the goto-model if it doesn't @@ -94,6 +103,7 @@ class recursive_initializationt symbol_exprt get_malloc_function(); bool should_be_treated_as_array(const irep_idt &pointer_name) const; + optionalt find_equal_cluster(const irep_idt &name) const; bool is_array_size_parameter(const irep_idt &cmdline_arg) const; optionalt get_associated_size_variable(const irep_idt &array_name) const;