diff --git a/regression/goto-harness/do_not_nondet_globals_by_default/main.c b/regression/goto-harness/do_not_nondet_globals_by_default/main.c new file mode 100644 index 00000000000..d15a72a6073 --- /dev/null +++ b/regression/goto-harness/do_not_nondet_globals_by_default/main.c @@ -0,0 +1,6 @@ +int a_global; + +void entry_function(void) +{ + assert(a_global == 0); +} diff --git a/regression/goto-harness/do_not_nondet_globals_by_default/test.desc b/regression/goto-harness/do_not_nondet_globals_by_default/test.desc new file mode 100644 index 00000000000..5666fe501fb --- /dev/null +++ b/regression/goto-harness/do_not_nondet_globals_by_default/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--harness-type call-function --function entry_function +^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/goto-harness/non_det_globals_option/main.c b/regression/goto-harness/non_det_globals_option/main.c new file mode 100644 index 00000000000..d15a72a6073 --- /dev/null +++ b/regression/goto-harness/non_det_globals_option/main.c @@ -0,0 +1,6 @@ +int a_global; + +void entry_function(void) +{ + assert(a_global == 0); +} diff --git a/regression/goto-harness/non_det_globals_option/test.desc b/regression/goto-harness/non_det_globals_option/test.desc new file mode 100644 index 00000000000..0ee7b00671a --- /dev/null +++ b/regression/goto-harness/non_det_globals_option/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--harness-type call-function --function entry_function --nondet-globals +^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/main.c b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/main.c new file mode 100644 index 00000000000..d4efed079c1 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/main.c @@ -0,0 +1,29 @@ +#include +#include + +typedef struct st1 +{ + struct st2 *to_st2; + int data; +} st1_t; + +typedef struct st2 +{ + struct st1 *to_st1; + int data; +} st2_t; + +st1_t dummy1; +st2_t dummy2; + +void func(st1_t *p) +{ + assert(p != NULL); + assert(p->to_st2 != NULL); + assert(p->to_st2->to_st1 != NULL); + assert(p->to_st2->to_st1->to_st2 == NULL); + + assert(p != &dummy1); + assert(p->to_st2 != &dummy2); + assert(p->to_st2->to_st1 != &dummy1); +} diff --git a/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc new file mode 100644 index 00000000000..9bef5d48a87 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/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 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/pointer-function-parameters-struct-non-recursive/main.c b/regression/goto-harness/pointer-function-parameters-struct-non-recursive/main.c new file mode 100644 index 00000000000..ab46298f592 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-non-recursive/main.c @@ -0,0 +1,17 @@ +#include +#include + +typedef struct st +{ + int data; +} st_t; + +st_t dummy; + +void func(st_t *p) +{ + assert(p != NULL); + assert(p != &dummy); + assert(p->data >= 4854549); + assert(p->data < 4854549); +} diff --git a/regression/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc b/regression/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc new file mode 100644 index 00000000000..5d59a83a407 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --harness-type call-function +^EXIT=10$ +^SIGNAL=0$ +\[func.assertion.1\] line [0-9]+ assertion p != .*((NULL)|0).*: SUCCESS +\[func.assertion.2\] line [0-9]+ assertion p != &dummy: SUCCESS +\[func.assertion.3\] line [0-9]+ assertion p->data >= 4854549: FAILURE +\[func.assertion.4\] line [0-9]+ assertion p->data < 4854549: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/main.c b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/main.c new file mode 100644 index 00000000000..3d25cbdb9a1 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/main.c @@ -0,0 +1,28 @@ +#include +#include + +typedef struct st +{ + struct st *next; + struct st *prev; + int data; +} st_t; + +st_t dummy; + +void func(st_t *p) +{ + assert(p != NULL); + assert(p != &dummy); + + assert(p->prev != NULL); + assert(p->prev != &dummy); + + assert(p->next != NULL); + assert(p->next != &dummy); + + assert(p->prev->prev == NULL); + assert(p->prev->next == NULL); + assert(p->next->prev == NULL); + assert(p->next->next == NULL); +} diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc new file mode 100644 index 00000000000..3ba3174202a --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --harness-type call-function +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/main.c b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/main.c new file mode 100644 index 00000000000..70abdec5c77 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/main.c @@ -0,0 +1,22 @@ +#include +#include + +typedef struct st +{ + struct st *next; + int data; +} st_t; + +st_t dummy; + +void func(st_t *p) +{ + assert(p != NULL); + assert(p->next != NULL); + assert(p->next->next != NULL); + assert(p->next->next->next == NULL); + + assert(p != &dummy); + assert(p->next != &dummy); + assert(p->next->next != &dummy); +} diff --git a/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc new file mode 100644 index 00000000000..9bef5d48a87 --- /dev/null +++ b/regression/goto-harness/pointer-function-parameters-struct-simple-recursion/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 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c b/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c new file mode 100644 index 00000000000..860a68ab18a --- /dev/null +++ b/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c @@ -0,0 +1,36 @@ +#include +#include + +typedef struct A A; +typedef struct B B; +typedef struct C C; +typedef struct D D; + +struct A +{ + B *b; +}; + +struct B +{ + C *c; +}; + +struct C +{ + D *d; +}; + +struct D +{ + A *a; +}; + +void func(A *a) +{ + assert(a != NULL); + assert(a->b != NULL); + assert(a->b->c != NULL); + assert(a->b->c->d != NULL); + assert(a->b->c->d->a == NULL); +} diff --git a/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc b/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc new file mode 100644 index 00000000000..a1a6b8ff9d9 --- /dev/null +++ b/regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 1 --harness-type call-function +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/src/goto-harness/Makefile b/src/goto-harness/Makefile index abbcd9da657..1d9edf0ecdd 100644 --- a/src/goto-harness/Makefile +++ b/src/goto-harness/Makefile @@ -4,6 +4,7 @@ SRC = \ goto_harness_generator_factory.cpp \ goto_harness_main.cpp \ goto_harness_parse_options.cpp \ + recursive_initialization.cpp \ # Empty last line OBJ += \ diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index c2042da62ed..077391b772f 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -11,18 +11,49 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include #include +#include #include #include "function_harness_generator_options.h" #include "goto_harness_parse_options.h" +#include "recursive_initialization.h" +/// This contains implementation details of +/// function call harness generator to avoid +/// leaking them out into the header. +/* NOLINTNEXTLINE(readability/identifier_spacing) */ struct function_call_harness_generatort::implt { ui_message_handlert *message_handler; irep_idt function; + irep_idt harness_function_name; + symbol_tablet *symbol_table; + goto_functionst *goto_functions; + bool nondet_globals = false; + + recursive_initialization_configt recursive_initialization_config; + std::unique_ptr recursive_initialization; + + /// \see goto_harness_generatort::generate + void generate(goto_modelt &goto_model, const irep_idt &harness_function_name); + /// Iterate over the symbol table and generate initialisation code for + /// globals into the function body. + void generate_nondet_globals(code_blockt &function_body); + /// Non-deterministically initialise the parameters of the entry function + /// and insert function call to the passed code block. + void setup_parameters_and_call_entry_function(code_blockt &function_body); + /// Return a reference to the entry function or throw if it doesn't exist. + const symbolt &lookup_function_to_call(); + /// Generate initialisation code for one lvalue inside block. + void generate_initialisation_code_for(code_blockt &block, const exprt &lhs); + /// Throw if the harness function already exists in the symbol table. + void ensure_harness_does_not_already_exist(); + /// Update the goto-model with the new harness function. + void add_harness_function_to_goto_model(code_blockt function_body); }; function_call_harness_generatort::function_call_harness_generatort( @@ -42,6 +73,42 @@ void function_call_harness_generatort::handle_option( { p_impl->function = require_exactly_one_value(option, values); } + else if(option == FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT) + { + p_impl->nondet_globals = true; + } + else if(option == FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT) + { + auto const value = require_exactly_one_value(option, values); + auto const min_null_tree_depth = string2optional(value, 10); + if(min_null_tree_depth.has_value()) + { + p_impl->recursive_initialization_config.min_null_tree_depth = + min_null_tree_depth.value(); + } + else + { + throw invalid_command_line_argument_exceptiont{ + "failed to convert `" + value + "' to integer", + "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT}; + } + } + else if(option == FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT) + { + auto const value = require_exactly_one_value(option, values); + auto const max_nondet_tree_depth = string2optional(value, 10); + if(max_nondet_tree_depth.has_value()) + { + p_impl->recursive_initialization_config.max_nondet_tree_depth = + max_nondet_tree_depth.value(); + } + else + { + throw invalid_command_line_argument_exceptiont{ + "failed to convert `" + value + "' to integer", + "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT}; + } + } else { throw invalid_command_line_argument_exceptiont{ @@ -53,52 +120,124 @@ void function_call_harness_generatort::generate( goto_modelt &goto_model, const irep_idt &harness_function_name) { - auto const &function = p_impl->function; - auto &symbol_table = goto_model.symbol_table; - auto function_found = symbol_table.lookup(function); - auto harness_function_found = symbol_table.lookup(harness_function_name); + p_impl->generate(goto_model, harness_function_name); +} - if(function_found == nullptr) +void function_call_harness_generatort::implt:: + setup_parameters_and_call_entry_function(code_blockt &function_body) +{ + const auto &function_to_call = lookup_function_to_call(); + const auto &function_type = to_code_type(function_to_call.type); + const auto ¶meters = function_type.parameters(); + + code_function_callt::operandst arguments{}; + + auto allocate_objects = allocate_objectst{function_to_call.mode, + function_to_call.location, + "__goto_harness", + *symbol_table}; + for(const auto ¶meter : parameters) { - throw invalid_command_line_argument_exceptiont{ - "function that should be harnessed is not found " + id2string(function), - "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; + auto argument = allocate_objects.allocate_automatic_local_object( + parameter.type(), parameter.get_base_name()); + arguments.push_back(argument); } - - if(harness_function_found != nullptr) + allocate_objects.declare_created_symbols(function_body); + for(auto const &argument : arguments) { - throw invalid_command_line_argument_exceptiont{ - "harness function already in the symbol table " + - id2string(harness_function_name), - "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT}; + generate_initialisation_code_for(function_body, argument); } + code_function_callt function_call{function_to_call.symbol_expr(), + std::move(arguments)}; + function_call.add_source_location() = function_to_call.location; - auto allocate_objects = allocate_objectst{function_found->mode, - function_found->location, - "__goto_harness", - symbol_table}; + function_body.add(std::move(function_call)); +} + +void function_call_harness_generatort::implt::generate( + goto_modelt &goto_model, + const irep_idt &harness_function_name) +{ + symbol_table = &goto_model.symbol_table; + goto_functions = &goto_model.goto_functions; + const auto &function_to_call = lookup_function_to_call(); + recursive_initialization_config.mode = function_to_call.mode; + recursive_initialization = util_make_unique( + recursive_initialization_config, goto_model); + this->harness_function_name = harness_function_name; + ensure_harness_does_not_already_exist(); // create body for the function code_blockt function_body{}; - const auto &function_type = to_code_type(function_found->type); - const auto ¶meters = function_type.parameters(); + generate_nondet_globals(function_body); + setup_parameters_and_call_entry_function(function_body); + add_harness_function_to_goto_model(std::move(function_body)); +} - code_function_callt::operandst arguments{}; - arguments.reserve(parameters.size()); +void function_call_harness_generatort::implt::generate_nondet_globals( + code_blockt &function_body) +{ + if(nondet_globals) + { + for(const auto &symbol_table_entry : *symbol_table) + { + const auto &symbol = symbol_table_entry.second; + if( + symbol.is_static_lifetime && symbol.is_lvalue && + !has_prefix(id2string(symbol.name), CPROVER_PREFIX)) + { + generate_initialisation_code_for(function_body, symbol.symbol_expr()); + } + } + } +} - for(const auto ¶meter : parameters) +void function_call_harness_generatort::implt::generate_initialisation_code_for( + code_blockt &block, + const exprt &lhs) +{ + recursive_initialization->initialize(lhs, 0, {}, block); +} + +void function_call_harness_generatort::validate_options() +{ + if(p_impl->function == ID_empty) + throw invalid_command_line_argument_exceptiont{ + "required parameter entry function not set", + "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; +} + +const symbolt & +function_call_harness_generatort::implt::lookup_function_to_call() +{ + auto function_found = symbol_table->lookup(function); + + if(function_found == nullptr) { - auto argument = allocate_objects.allocate_automatic_local_object( - parameter.type(), parameter.get_base_name()); - arguments.push_back(std::move(argument)); + throw invalid_command_line_argument_exceptiont{ + "function that should be harnessed is not found " + id2string(function), + "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; } - code_function_callt function_call{function_found->symbol_expr(), - std::move(arguments)}; - function_call.add_source_location() = function_found->location; + return *function_found; +} - function_body.add(std::move(function_call)); +void function_call_harness_generatort::implt:: + ensure_harness_does_not_already_exist() +{ + if(symbol_table->lookup(harness_function_name)) + { + throw invalid_command_line_argument_exceptiont{ + "harness function already exists in the symbol table", + "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT}; + } +} + +void function_call_harness_generatort::implt:: + add_harness_function_to_goto_model(code_blockt function_body) +{ + const auto &function_to_call = lookup_function_to_call(); // create the function symbol symbolt harness_function_symbol{}; @@ -106,29 +245,22 @@ void function_call_harness_generatort::generate( harness_function_symbol.pretty_name = harness_function_name; harness_function_symbol.is_lvalue = true; - harness_function_symbol.mode = function_found->mode; + harness_function_symbol.mode = function_to_call.mode; harness_function_symbol.type = code_typet{{}, empty_typet{}}; - harness_function_symbol.value = function_body; + harness_function_symbol.value = std::move(function_body); - symbol_table.insert(harness_function_symbol); + symbol_table->insert(harness_function_symbol); - goto_model.goto_functions.function_map[harness_function_name].type = - to_code_type(harness_function_symbol.type); - auto &body = - goto_model.goto_functions.function_map[harness_function_name].body; + auto const &generated_harness = + symbol_table->lookup_ref(harness_function_name); + goto_functions->function_map[harness_function_name].type = + to_code_type(generated_harness.type); + auto &body = goto_functions->function_map[harness_function_name].body; goto_convert( - static_cast(harness_function_symbol.value), - goto_model.symbol_table, + static_cast(generated_harness.value), + *symbol_table, body, - *p_impl->message_handler, - function_found->mode); + *message_handler, + function_to_call.mode); body.add(goto_programt::make_end_function()); } - -void function_call_harness_generatort::validate_options() -{ - if(p_impl->function == ID_empty) - throw invalid_command_line_argument_exceptiont{ - "required parameter entry function not set", - "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; -} diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index a9898abce3e..400fd761791 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -10,16 +10,36 @@ Author: Diffblue Ltd. #define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H #define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function" +#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals" +#define FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth" +#define FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + "max-nondet-tree-depth" + +// clang-format off #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ - "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" + "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ + "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \ + "(" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \ + "(" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ // FUNCTION_HARNESS_GENERATOR_OPTIONS +// clang-format on + // clang-format off #define FUNCTION_HARNESS_GENERATOR_HELP \ "function harness generator (--harness-type call-function)\n\n" \ "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ " the function the harness should call\n" \ + "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \ + " set global variables to non-deterministic values in harness\n" \ + "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ + " N minimum level at which a pointer can first be\n" \ + " NULL in a recursively nondet initialized struct\n" \ + "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + " N limit size of nondet (e.g. input) object tree;\n" \ + " at level N pointers are set to null\n" \ // FUNCTION_HARNESS_GENERATOR_HELP + // clang-format on #endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp new file mode 100644 index 00000000000..4afd950ea15 --- /dev/null +++ b/src/goto-harness/recursive_initialization.cpp @@ -0,0 +1,131 @@ +/******************************************************************\ + +Module: recursive_initialization + +Author: Diffblue Ltd. + +\******************************************************************/ + +#include "recursive_initialization.h" + +#include +#include +#include +#include +#include +#include + +recursive_initializationt::recursive_initializationt( + recursive_initialization_configt initialization_config, + goto_modelt &goto_model) + : initialization_config(std::move(initialization_config)), + goto_model(goto_model) +{ +} + +void recursive_initializationt::initialize( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body) +{ + auto const &type = lhs.type(); + if(type.id() == ID_struct_tag) + { + initialize_struct_tag(lhs, depth, known_tags, body); + } + else if(type.id() == ID_pointer) + { + initialize_pointer(lhs, depth, known_tags, body); + } + else + { + initialize_nondet(lhs, depth, known_tags, body); + } +} + +symbol_exprt recursive_initializationt::get_malloc_function() +{ + // unused for now, we'll need it for arrays + auto malloc_sym = goto_model.symbol_table.lookup("malloc"); + if(malloc_sym == nullptr) + { + symbolt new_malloc_sym; + new_malloc_sym.type = code_typet{code_typet{ + {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}}; + new_malloc_sym.name = new_malloc_sym.pretty_name = + new_malloc_sym.base_name = "malloc"; + new_malloc_sym.mode = initialization_config.mode; + goto_model.symbol_table.insert(new_malloc_sym); + return new_malloc_sym.symbol_expr(); + } + return malloc_sym->symbol_expr(); +} + +void recursive_initializationt::initialize_struct_tag( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body) +{ + PRECONDITION(lhs.type().id() == ID_struct_tag); + auto const &type = to_struct_tag_type(lhs.type()); + auto new_known_tags = known_tags; + new_known_tags.insert(type.get_identifier()); + auto const &ns = namespacet{goto_model.symbol_table}; + for(auto const &component : ns.follow_tag(type).components()) + { + initialize(member_exprt{lhs, component}, depth, new_known_tags, body); + } +} + +void recursive_initializationt::initialize_pointer( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body) +{ + PRECONDITION(lhs.type().id() == ID_pointer); + auto const &type = to_pointer_type(lhs.type()); + allocate_objectst allocate_objects{initialization_config.mode, + type.source_location(), + "initializer", + goto_model.symbol_table}; + exprt choice = + allocate_objects.allocate_automatic_local_object(bool_typet{}, "choice"); + auto pointee = + allocate_objects.allocate_automatic_local_object(type.subtype(), "pointee"); + allocate_objects.declare_created_symbols(body); + body.add(code_assignt{lhs, null_pointer_exprt{type}}); + bool is_unknown_struct_tag = + can_cast_type(type.subtype()) && + known_tags.find(to_tag_type(type.subtype()).get_identifier()) == + known_tags.end(); + + if( + depth < initialization_config.max_nondet_tree_depth || + is_unknown_struct_tag) + { + if(depth < initialization_config.min_null_tree_depth) + { + initialize(pointee, depth + 1, known_tags, body); + body.add(code_assignt{lhs, address_of_exprt{pointee}}); + } + else + { + code_blockt then_case{}; + initialize(pointee, depth + 1, known_tags, then_case); + then_case.add(code_assignt{lhs, address_of_exprt{pointee}}); + body.add(code_ifthenelset{choice, then_case}); + } + } +} + +void recursive_initializationt::initialize_nondet( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body) +{ + body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}}); +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h new file mode 100644 index 00000000000..fe2c5ba0f47 --- /dev/null +++ b/src/goto-harness/recursive_initialization.h @@ -0,0 +1,74 @@ +/******************************************************************\ + +Module: recursive_initialization + +Author: Diffblue Ltd. + +\******************************************************************/ + +#ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H +#define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H + +#include + +#include +#include +#include +#include + +struct recursive_initialization_configt +{ + std::size_t min_null_tree_depth = 1; + std::size_t max_nondet_tree_depth = 2; + irep_idt mode; +}; + +/// Class for generating initialisation code +/// for compound structures. +class recursive_initializationt +{ +public: + using recursion_sett = std::set; + + recursive_initializationt( + recursive_initialization_configt initialization_config, + goto_modelt &goto_model); + + /// Generate initialisation code for lhs into body. + /// \param lhs: The expression to initialise. + /// \param depth: The number of pointer follows. Starts at 0. + /// \param known_tags: The struct tags we've already seen during recursion. + /// \param body: The code block to write initialisation code to. + void initialize( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body); + +private: + const recursive_initialization_configt initialization_config; + goto_modelt &goto_model; + + /// Get the malloc function as symbol exprt, + /// and inserts it into the goto-model if it doesn't + /// exist already. + symbol_exprt get_malloc_function(); + + void initialize_struct_tag( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body); + void initialize_pointer( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body); + void initialize_nondet( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body); +}; + +#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H