diff --git a/regression/goto-harness/select-multiple-members-to-havoc/main.c b/regression/goto-harness/select-multiple-members-to-havoc/main.c new file mode 100644 index 00000000000..84e8ceb5375 --- /dev/null +++ b/regression/goto-harness/select-multiple-members-to-havoc/main.c @@ -0,0 +1,46 @@ +#include +#include + +typedef struct st1 +{ + int data11; + struct innert1 + { + int inner_data11; + int inner_data12; + } inner1; + int data12; +} st1_t; + +typedef struct st2 +{ + int data21; + struct innert2 + { + int inner_data21; + int inner_data22; + } inner2; + int data22; +} st2_t; + +st1_t dummy1 = {.data11 = 0, + .inner1.inner_data11 = 0, + .inner1.inner_data12 = 0, + .data12 = 0}; + +st2_t dummy2 = {.data21 = 0, + .inner2.inner_data21 = 0, + .inner2.inner_data22 = 0, + .data22 = 0}; + +void func(st1_t *p) +{ + assert(dummy1.data11 == 0); //should succeed + assert(dummy1.inner1.inner_data11 == 0); + assert(dummy1.inner1.inner_data12 == 0); //should fail + assert(dummy1.data12 == 0); + assert(dummy2.data21 == 0); //should succeed + assert(dummy2.inner2.inner_data21 == 0); //should fail + assert(dummy2.inner2.inner_data22 == 0); + assert(dummy2.data22 == 0); +} diff --git a/regression/goto-harness/select-multiple-members-to-havoc/test.desc b/regression/goto-harness/select-multiple-members-to-havoc/test.desc new file mode 100644 index 00000000000..87e6a111b98 --- /dev/null +++ b/regression/goto-harness/select-multiple-members-to-havoc/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --havoc-member 'dummy1.inner1.inner_data12,dummy2.inner2.inner_data21' --nondet-globals +^\[func.assertion.\d+\] line \d+ assertion dummy1.data11 == 0: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion dummy1.inner1.inner_data11 == 0: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion dummy1.inner1.inner_data12 == 0: FAILURE$ +^\[func.assertion.\d+\] line \d+ assertion dummy1.data12 == 0: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion dummy2.inner2.inner_data21 == 0: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/goto-harness/select-struct-member-to-havoc/main.c b/regression/goto-harness/select-struct-member-to-havoc/main.c new file mode 100644 index 00000000000..84621165154 --- /dev/null +++ b/regression/goto-harness/select-struct-member-to-havoc/main.c @@ -0,0 +1,26 @@ +#include +#include + +typedef struct st +{ + int data1; + struct innert + { + int inner_data1; + int inner_data2; + } inner; + int data2; +} st_t; + +st_t dummy = {.data1 = 0, + .inner.inner_data1 = 0, + .inner.inner_data2 = 0, + .data2 = 0}; + +void func(st_t *p) +{ + assert(dummy.data1 == 0); //should succeed + assert(dummy.inner.inner_data1 == 0); + assert(dummy.inner.inner_data2 == 0); //should fail + assert(dummy.data2 == 0); +} diff --git a/regression/goto-harness/select-struct-member-to-havoc/test.desc b/regression/goto-harness/select-struct-member-to-havoc/test.desc new file mode 100644 index 00000000000..c9642660ae2 --- /dev/null +++ b/regression/goto-harness/select-struct-member-to-havoc/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 --havoc-member 'dummy.inner.inner_data2' --nondet-globals +^\[func.assertion.\d+\] line \d+ assertion dummy.data1 == 0: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion dummy.inner.inner_data1 == 0: SUCCESS$ +^\[func.assertion.\d+\] line \d+ assertion dummy.inner.inner_data2 == 0: FAILURE$ +^\[func.assertion.\d+\] line \d+ assertion dummy.data2 == 0: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +-- +^warning: ignoring diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h index 9a4c396133d..b661661bae3 100644 --- a/src/goto-harness/common_harness_generator_options.h +++ b/src/goto-harness/common_harness_generator_options.h @@ -16,6 +16,7 @@ Author: Diffblue Ltd. #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size" #define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ "function-pointer-can-be-null" +#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "havoc-member" // clang-format off #define COMMON_HARNESS_GENERATOR_OPTIONS \ @@ -24,6 +25,7 @@ Author: Diffblue Ltd. "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "):" \ // COMMON_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -44,7 +46,9 @@ Author: Diffblue Ltd. " (default: 2)\n" \ "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ " , name of the function(s) pointer parameters\n" \ - " that can be NULL pointing." + " that can be NULL pointing." \ + "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT \ + " path to the member to be havoced\n" \ // COMMON_HARNESS_GENERATOR_HELP // clang-format on diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 2ba446def5b..669a7664270 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -19,6 +19,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include @@ -86,6 +87,28 @@ bool recursive_initialization_configt::handle_option( [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); return true; } + else if(option == COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT) + { + const auto list_of_members_string = + harness_options_parser::require_exactly_one_value( + COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT, values); + const auto list_of_members = split_string(list_of_members_string, ','); + for(const auto &member : list_of_members) + { + const auto selection_spec_strings = split_string(member, '.'); + + selection_specs.push_back({}); + auto &selection_spec = selection_specs.back(); + std::transform( + selection_spec_strings.begin(), + selection_spec_strings.end(), + std::back_inserter(selection_spec), + [](const std::string &member_name_string) { + return irep_idt{member_name_string}; + }); + } + return true; + } return false; } @@ -114,6 +137,18 @@ void recursive_initializationt::initialize( const exprt &depth, code_blockt &body) { + if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty()) + { + auto lhs_id = to_symbol_expr(lhs).get_identifier(); + for(const auto &selection_spec : initialization_config.selection_specs) + { + if(selection_spec.front() == lhs_id) + { + initialize_selected_member(lhs, depth, body, selection_spec); + return; + } + } + } // 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 @@ -956,3 +991,51 @@ code_blockt recursive_initializationt::build_function_pointer_constructor( return body; } + +void recursive_initializationt::initialize_selected_member( + const exprt &lhs, + const exprt &depth, + code_blockt &body, + const std::vector &selection_spec) +{ + PRECONDITION(lhs.id() == ID_symbol); + PRECONDITION(lhs.type().id() == ID_struct_tag); + PRECONDITION(!selection_spec.empty()); + + auto component_member = lhs; + const namespacet ns{goto_model.symbol_table}; + + for(auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++) + { + if(component_member.type().id() != ID_struct_tag) + { + throw invalid_command_line_argument_exceptiont{ + "'" + id2string(*it) + "' is not a component name", + "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT}; + } + const auto &struct_tag_type = to_struct_tag_type(component_member.type()); + const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type)); + + bool found = false; + for(auto const &component : struct_type.components()) + { + const auto &component_type = component.type(); + const auto component_name = component.get_name(); + + if(*it == component_name) + { + component_member = + member_exprt{component_member, component_name, component_type}; + found = true; + break; + } + } + if(!found) + { + throw invalid_command_line_argument_exceptiont{ + "'" + id2string(*it) + "' is not a component name", + "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT}; + } + } + initialize(component_member, depth, body); +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 725fec9efdf..a790ad0eb07 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -42,6 +42,8 @@ struct recursive_initialization_configt bool arguments_may_be_equal = false; + std::vector> selection_specs; + std::string to_string() const; // for debugging purposes /// Parse the options specific for recursive initialisation @@ -263,6 +265,19 @@ class recursive_initializationt /// \param result: symbol of the result parameter /// \return the body of the constructor code_blockt build_array_string_constructor(const symbol_exprt &result) const; + + /// Select the specified struct-member to be non-deterministically + /// initialized. + /// \param lhs: symbol expression of the top structure + /// \param depth: only to be passed + /// \param body: code block for the initializing assignment + /// \param selection_spec: the user specification of the particular member to + /// havoc + void initialize_selected_member( + const exprt &lhs, + const exprt &depth, + code_blockt &body, + const std::vector &selection_spec); }; #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H