From 9db8bd4aef5c103c755cedabff4cbf9746bac26f Mon Sep 17 00:00:00 2001 From: xbauch Date: Mon, 4 Nov 2019 11:31:23 +0000 Subject: [PATCH 1/3] Allow function pointer arguments to be equal for the function-call goto-harness. We add a new command-line option `treat-pointers-equal` that takes a list of formal parameter names and results in a harness that only generates constructor for one of the pointers. The other pointers are simply assigned with the constructed one. --- .../main.c | 16 +++++ .../test.desc | 8 +++ .../function_call_harness_generator.cpp | 64 ++++++++++++++++++- .../function_harness_generator_options.h | 6 ++ src/goto-harness/recursive_initialization.cpp | 34 ++++++++++ src/goto-harness/recursive_initialization.h | 5 ++ 6 files changed, 131 insertions(+), 2 deletions(-) create mode 100644 regression/goto-harness/pointer-function-parameters-equal-simple/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-equal-simple/test.desc 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..ece9c8f357b --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c @@ -0,0 +1,16 @@ +#include +#include + +typedef struct st +{ + struct st *next; + int data; +} st_t; + +void func(st_t *p, st_t *q) +{ + assert(p != NULL); + assert(p->next != NULL); + + assert(p == q); +} 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..3f82a6727c3 --- /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 +^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..b7118947a31 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::set function_parameters_to_treat_equal; + std::set function_arguments_to_treat_equal; + std::set function_parameters_to_treat_as_cstrings; std::set function_arguments_to_treat_as_cstrings; @@ -112,6 +115,16 @@ 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_id : split_string(value, ',')) + { + p_impl->function_parameters_to_treat_equal.insert(param_id); + } + } + } else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT) { for(auto const &array_size_pair : values) @@ -183,6 +196,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) @@ -238,7 +253,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 +273,46 @@ 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 &pointer_id : p_impl->function_parameters_to_treat_equal) + { + 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 & @@ -348,6 +403,11 @@ function_call_harness_generatort::implt::declare_arguments( function_arguments_to_treat_as_cstrings.insert(argument_name); } + if(function_parameters_to_treat_equal.count(parameter_name) != 0) + { + function_arguments_to_treat_equal.insert(argument_name); + } + auto it = function_parameter_to_associated_array_size.find(parameter_name); if(it != function_parameter_to_associated_array_size.end()) { @@ -377,7 +437,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..81158035224 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -15,6 +15,8 @@ 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 \ @@ -25,6 +27,7 @@ Author: Diffblue Ltd. "(" 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_OPTIONS @@ -43,6 +46,9 @@ 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 treat the function parameter with the name `q' equal\n" \ + " to parameter `q'\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..f9086750bbc 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -100,6 +100,19 @@ void recursive_initializationt::initialize( const exprt &depth, code_blockt &body) { + if( + lhs.id() == ID_symbol && + should_be_treated_equal(to_symbol_expr(lhs).get_identifier())) + { + if(common_arguments_origin.has_value()) + { + body.add(code_assignt{lhs, *common_arguments_origin}); + return; + } + else + common_arguments_origin = lhs; + } + const irep_idt &fun_name = build_constructor(lhs); const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name); @@ -280,6 +293,13 @@ bool recursive_initializationt::should_be_treated_as_array( initialization_config.pointers_to_treat_as_arrays.end(); } +bool recursive_initializationt::should_be_treated_equal( + const irep_idt &pointer_name) const +{ + return initialization_config.pointers_to_treat_equal.find(pointer_name) != + initialization_config.pointers_to_treat_equal.end(); +} + bool recursive_initializationt::is_array_size_parameter( const irep_idt &cmdline_arg) const { @@ -763,3 +783,17 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( return body; } + +bool recursive_initializationt::needs_freeing(const exprt &expr) const +{ + if(expr.type().id() != ID_pointer) + return false; + if(common_arguments_origin.has_value() && expr.id() == ID_symbol) + { + auto origin_name = + to_symbol_expr(*common_arguments_origin).get_identifier(); + auto expr_name = to_symbol_expr(expr).get_identifier(); + return origin_name == expr_name; + } + return true; +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 505d32d8c32..648faa4cbb4 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -37,6 +37,7 @@ struct recursive_initialization_configt std::map array_name_to_associated_array_size_variable; std::set pointers_to_treat_as_cstrings; + std::set pointers_to_treat_equal; std::string to_string() const; // for debugging purposes @@ -81,12 +82,15 @@ class recursive_initializationt !has_prefix(id2string(symbol.name), CPROVER_PREFIX)); } + bool needs_freeing(const exprt &expr) const; + 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; + optionalt common_arguments_origin; /// Get the malloc function as symbol exprt, /// and inserts it into the goto-model if it doesn't @@ -94,6 +98,7 @@ class recursive_initializationt symbol_exprt get_malloc_function(); bool should_be_treated_as_array(const irep_idt &pointer_name) const; + bool should_be_treated_equal(const irep_idt &pointer_name) const; bool is_array_size_parameter(const irep_idt &cmdline_arg) const; optionalt get_associated_size_variable(const irep_idt &array_name) const; From 0040862f8d8ca285cd5f87ba238ce8d6e10bde03 Mon Sep 17 00:00:00 2001 From: xbauch Date: Wed, 13 Nov 2019 15:32:03 +0000 Subject: [PATCH 2/3] Extend to clusters of equal parameters Specified by a semi-colon separated list of comma separated names. --- .../main.c | 17 +++- .../test.desc | 2 +- .../function_call_harness_generator.cpp | 87 +++++++++++-------- .../function_harness_generator_options.h | 4 +- src/goto-harness/recursive_initialization.cpp | 59 +++++++++---- src/goto-harness/recursive_initialization.h | 6 +- 6 files changed, 115 insertions(+), 60 deletions(-) diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/main.c b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c index ece9c8f357b..9f1b214fa77 100644 --- a/regression/goto-harness/pointer-function-parameters-equal-simple/main.c +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c @@ -1,16 +1,27 @@ #include #include -typedef struct st +typedef struct st1 { struct st *next; int data; -} st_t; +} st1_t; -void func(st_t *p, st_t *q) +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 index 3f82a6727c3..1f9be5e19f0 100644 --- a/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc +++ b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal p,q +--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 diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index b7118947a31..3544c25f64c 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -48,8 +48,8 @@ struct function_call_harness_generatort::implt std::set function_parameters_to_treat_as_arrays; std::set function_arguments_to_treat_as_arrays; - std::set function_parameters_to_treat_equal; - std::set function_arguments_to_treat_equal; + 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; @@ -119,9 +119,14 @@ void function_call_harness_generatort::handle_option( { for(auto const &value : values) { - for(auto const ¶m_id : split_string(value, ',')) + for(auto const ¶m_cluster : split_string(value, ';')) { - p_impl->function_parameters_to_treat_equal.insert(param_id); + 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); } } } @@ -276,41 +281,44 @@ void function_call_harness_generatort::validate_options( 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 &pointer_id : p_impl->function_parameters_to_treat_equal) + for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal) { - 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()) + for(auto const &pointer_id : equal_cluster) { - if(formal_param.get_identifier() == decorated_pointer_id) + 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()) { - 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(formal_param.get_identifier() == decorated_pointer_id) { - if(common_type != formal_param.type()) + is_a_param = true; + if(formal_param.type().id() != ID_pointer) { throw invalid_command_line_argument_exceptiont{ - "pointer arguments of conflicting type", + 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(); } - 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}; + if(!is_a_param) + { + throw invalid_command_line_argument_exceptiont{ + id2string(pointer_id) + " is not a parameter", + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT}; + } } } } @@ -403,11 +411,6 @@ function_call_harness_generatort::implt::declare_arguments( function_arguments_to_treat_as_cstrings.insert(argument_name); } - if(function_parameters_to_treat_equal.count(parameter_name) != 0) - { - function_arguments_to_treat_equal.insert(argument_name); - } - auto it = function_parameter_to_associated_array_size.find(parameter_name); if(it != function_parameter_to_associated_array_size.end()) { @@ -425,6 +428,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; } diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 81158035224..03f5abd2d47 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -47,8 +47,8 @@ Author: Diffblue Ltd. " p treat the function parameter with the name `p' as\n" \ " an array\n" \ "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \ - " p,q treat the function parameter with the name `q' equal\n" \ - " to parameter `q'\n" \ + " 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_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 f9086750bbc..8d3b8a598b3 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,17 +102,23 @@ void recursive_initializationt::initialize( const exprt &depth, code_blockt &body) { - if( - lhs.id() == ID_symbol && - should_be_treated_equal(to_symbol_expr(lhs).get_identifier())) + if(lhs.id() == ID_symbol) { - if(common_arguments_origin.has_value()) + const auto maybe_cluster_index = + find_equal_cluster(to_symbol_expr(lhs).get_identifier()); + if(maybe_cluster_index.has_value()) { - body.add(code_assignt{lhs, *common_arguments_origin}); - return; + if(common_arguments_origins[*maybe_cluster_index].has_value()) + { + body.add( + code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]}); + return; + } + else + { + common_arguments_origins[*maybe_cluster_index] = lhs; + } } - else - common_arguments_origin = lhs; } const irep_idt &fun_name = build_constructor(lhs); @@ -293,11 +301,17 @@ bool recursive_initializationt::should_be_treated_as_array( initialization_config.pointers_to_treat_as_arrays.end(); } -bool recursive_initializationt::should_be_treated_equal( - const irep_idt &pointer_name) const +optionalt +recursive_initializationt::find_equal_cluster(const irep_idt &name) const { - return initialization_config.pointers_to_treat_equal.find(pointer_name) != - initialization_config.pointers_to_treat_equal.end(); + for(size_t 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( @@ -786,14 +800,25 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( bool recursive_initializationt::needs_freeing(const exprt &expr) const { - if(expr.type().id() != ID_pointer) + if(expr.type().id() != ID_pointer || expr.type().id() == ID_code) return false; - if(common_arguments_origin.has_value() && expr.id() == ID_symbol) + if(expr.id() == ID_symbol) { - auto origin_name = - to_symbol_expr(*common_arguments_origin).get_identifier(); auto expr_name = to_symbol_expr(expr).get_identifier(); - return origin_name == expr_name; + if(find_equal_cluster(expr_name).has_value()) + { + for(auto const &origin_expr : common_arguments_origins) + { + if(!origin_expr.has_value()) + continue; + INVARIANT( + origin_expr->id() == ID_symbol, "common origin is not a symbol"); + auto origin_name = to_symbol_expr(*origin_expr).get_identifier(); + if(origin_name == expr_name) + return true; + } + return false; + } } return true; } diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 648faa4cbb4..62858bfc2d7 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -37,7 +37,7 @@ struct recursive_initialization_configt std::map array_name_to_associated_array_size_variable; std::set pointers_to_treat_as_cstrings; - std::set pointers_to_treat_equal; + std::vector> pointers_to_treat_equal; std::string to_string() const; // for debugging purposes @@ -90,7 +90,7 @@ class recursive_initializationt irep_idt max_depth_var_name; irep_idt min_depth_var_name; type_constructor_namest type_constructor_names; - optionalt common_arguments_origin; + std::vector> common_arguments_origins; /// Get the malloc function as symbol exprt, /// and inserts it into the goto-model if it doesn't @@ -98,7 +98,7 @@ class recursive_initializationt symbol_exprt get_malloc_function(); bool should_be_treated_as_array(const irep_idt &pointer_name) const; - bool should_be_treated_equal(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; From 49b86dcd1e5da95f238cb0913132b6bdb35d8641 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 24 Jan 2020 15:52:14 +0000 Subject: [PATCH 3/3] Extend to allow conditional equality between pointer arguments. Whether or not they will be equal is now a non-deterministic choice. Freeing pointer had to be extended. --- .../main.c | 27 ++++++ .../test.desc | 12 +++ .../function_call_harness_generator.cpp | 8 +- .../function_harness_generator_options.h | 5 ++ src/goto-harness/recursive_initialization.cpp | 87 ++++++++++++++----- src/goto-harness/recursive_initialization.h | 7 +- 6 files changed, 120 insertions(+), 26 deletions(-) create mode 100644 regression/goto-harness/pointer-function-parameters-equal-maybe/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-equal-maybe/test.desc 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/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 3544c25f64c..b7f26a1d649 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -169,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{ @@ -219,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)); } diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 03f5abd2d47..477b53a8aff 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -21,6 +21,8 @@ Author: Diffblue Ltd. "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 \ @@ -30,6 +32,7 @@ Author: Diffblue Ltd. "(" 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 @@ -49,6 +52,8 @@ Author: Diffblue Ltd. "--" 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 8d3b8a598b3..537ba8c8b4d 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -102,6 +102,9 @@ 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 = @@ -110,8 +113,25 @@ void recursive_initializationt::initialize( { if(common_arguments_origins[*maybe_cluster_index].has_value()) { - body.add( - code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]}); + 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 @@ -301,10 +321,10 @@ bool recursive_initializationt::should_be_treated_as_array( initialization_config.pointers_to_treat_as_arrays.end(); } -optionalt +optionalt recursive_initializationt::find_equal_cluster(const irep_idt &name) const { - for(size_t index = 0; + for(equal_cluster_idt index = 0; index != initialization_config.pointers_to_treat_equal.size(); ++index) { @@ -800,25 +820,46 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( bool recursive_initializationt::needs_freeing(const exprt &expr) const { - if(expr.type().id() != ID_pointer || expr.type().id() == ID_code) - return false; - if(expr.id() == ID_symbol) + 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()) { - auto expr_name = to_symbol_expr(expr).get_identifier(); - if(find_equal_cluster(expr_name).has_value()) - { - for(auto const &origin_expr : common_arguments_origins) - { - if(!origin_expr.has_value()) - continue; - INVARIANT( - origin_expr->id() == ID_symbol, "common origin is not a symbol"); - auto origin_name = to_symbol_expr(*origin_expr).get_identifier(); - if(origin_name == expr_name) - return true; - } - return false; - } + // 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}}); } - return true; } diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 62858bfc2d7..5b0dfdac37d 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -39,6 +39,8 @@ struct recursive_initialization_configt 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 /// Parse the options specific for recursive initialisation @@ -58,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, @@ -83,6 +86,8 @@ class recursive_initializationt } 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; @@ -98,7 +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; + 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;