From 94636b4c6824313d79ee271ecd3ed992671ba4f3 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 8 Feb 2019 11:40:31 +0000 Subject: [PATCH 1/4] Refactor function call harness generator Important refactoring to make implementation of later features easier. Co-authored-by: Fotis Koutoulakis Co-authored-by: Hannes Steffenhagen --- .../function_call_harness_generator.cpp | 162 ++++++++++++------ .../function_harness_generator_options.h | 8 +- 2 files changed, 119 insertions(+), 51 deletions(-) diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index c2042da62ed..1f55eb75609 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include #include @@ -19,10 +20,31 @@ Author: Diffblue Ltd. #include "function_harness_generator_options.h" #include "goto_harness_parse_options.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; + + /// \see goto_harness_generatort::generate + void generate(goto_modelt &goto_model, const irep_idt &harness_function_name); + /// 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( @@ -53,52 +75,101 @@ 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; + 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(); + 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_initialisation_code_for( + code_blockt &block, + const exprt &lhs) +{ + block.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}}); +} - for(const auto ¶meter : parameters) +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 +177,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..ba4a79bf4a9 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -10,9 +10,12 @@ Author: Diffblue Ltd. #define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H #define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function" + +// clang-format off #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ - "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" -// FUNCTION_HARNESS_GENERATOR_OPTIONS + "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ + +// clang-format on // clang-format off #define FUNCTION_HARNESS_GENERATOR_HELP \ @@ -20,6 +23,7 @@ Author: Diffblue Ltd. "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ " the function the harness should call\n" \ // FUNCTION_HARNESS_GENERATOR_HELP + // clang-format on #endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H From d343daad7f717a6467ba31b59b521964c03b2d0d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Feb 2019 15:39:22 +0000 Subject: [PATCH 2/4] Add option to non-det globals to goto-harness Add ability to non-deterministically initialise globals in the function call harness generator. Co-authored-by: Fotis Koutoulakis Co-authored-by: Hannes Steffenhagen --- .../do_not_nondet_globals_by_default/main.c | 6 +++++ .../test.desc | 7 +++++ .../non_det_globals_option/main.c | 6 +++++ .../non_det_globals_option/test.desc | 7 +++++ .../function_call_harness_generator.cpp | 27 +++++++++++++++++++ .../function_harness_generator_options.h | 5 ++++ 6 files changed, 58 insertions(+) create mode 100644 regression/goto-harness/do_not_nondet_globals_by_default/main.c create mode 100644 regression/goto-harness/do_not_nondet_globals_by_default/test.desc create mode 100644 regression/goto-harness/non_det_globals_option/main.c create mode 100644 regression/goto-harness/non_det_globals_option/test.desc 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/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 1f55eb75609..2e7f0c7b330 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -31,9 +31,13 @@ struct function_call_harness_generatort::implt irep_idt harness_function_name; symbol_tablet *symbol_table; goto_functionst *goto_functions; + bool nondet_globals = false; /// \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); @@ -64,6 +68,10 @@ 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 { throw invalid_command_line_argument_exceptiont{ @@ -121,10 +129,29 @@ void function_call_harness_generatort::implt::generate( // create body for the function code_blockt function_body{}; + generate_nondet_globals(function_body); setup_parameters_and_call_entry_function(function_body); add_harness_function_to_goto_model(std::move(function_body)); } +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()); + } + } + } +} + void function_call_harness_generatort::implt::generate_initialisation_code_for( code_blockt &block, const exprt &lhs) diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index ba4a79bf4a9..4412daffd94 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -10,10 +10,13 @@ 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" // clang-format off #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ + "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \ +// FUNCTION_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -22,6 +25,8 @@ Author: Diffblue Ltd. "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_HELP // clang-format on From 5ce492c2fd252959dbe2c66dbf9997421075df03 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 13 Feb 2019 15:39:42 +0000 Subject: [PATCH 3/4] Add recursive initialisation of structs Recursively initialise non-deterministically struct components and pointers. Co-authored-by: Fotis Koutoulakis Co-authored-by: Hannes Steffenhagen --- .../main.c | 29 +++++ .../test.desc | 8 ++ .../main.c | 17 +++ .../test.desc | 11 ++ .../main.c | 28 +++++ .../test.desc | 8 ++ .../main.c | 22 ++++ .../test.desc | 8 ++ src/goto-harness/Makefile | 1 + .../function_call_harness_generator.cpp | 22 +++- .../function_harness_generator_options.h | 11 ++ src/goto-harness/recursive_initialization.cpp | 118 ++++++++++++++++++ src/goto-harness/recursive_initialization.h | 58 +++++++++ 13 files changed, 340 insertions(+), 1 deletion(-) create mode 100644 regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc create mode 100644 regression/goto-harness/pointer-function-parameters-struct-non-recursive/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc create mode 100644 regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc create mode 100644 regression/goto-harness/pointer-function-parameters-struct-simple-recursion/main.c create mode 100644 regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc create mode 100644 src/goto-harness/recursive_initialization.cpp create mode 100644 src/goto-harness/recursive_initialization.h 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/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 2e7f0c7b330..fb353e97b12 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -19,6 +19,7 @@ Author: Diffblue Ltd. #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 @@ -33,6 +34,9 @@ struct function_call_harness_generatort::implt 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 @@ -72,6 +76,18 @@ void function_call_harness_generatort::handle_option( { 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); + p_impl->recursive_initialization_config.min_null_tree_depth = + std::stoul(value); + } + else if(option == FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT) + { + auto const value = require_exactly_one_value(option, values); + p_impl->recursive_initialization_config.max_nondet_tree_depth = + std::stoul(value); + } else { throw invalid_command_line_argument_exceptiont{ @@ -123,6 +139,10 @@ void function_call_harness_generatort::implt::generate( { 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(); @@ -156,7 +176,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for( code_blockt &block, const exprt &lhs) { - block.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}}); + recursive_initialization->initialize(lhs, 0, block); } void function_call_harness_generatort::validate_options() diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 4412daffd94..400fd761791 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -11,11 +11,16 @@ Author: Diffblue Ltd. #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_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 @@ -27,6 +32,12 @@ Author: Diffblue Ltd. " 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 diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp new file mode 100644 index 00000000000..90435797569 --- /dev/null +++ b/src/goto-harness/recursive_initialization.cpp @@ -0,0 +1,118 @@ +/******************************************************************\ + +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, + code_blockt &body) +{ + auto const &type = lhs.type(); + if(type.id() == ID_struct_tag) + { + initialize_struct_tag(lhs, depth, body); + } + else if(type.id() == ID_pointer) + { + initialize_pointer(lhs, depth, body); + } + else + { + initialize_nondet(lhs, depth, 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, + code_blockt &body) +{ + PRECONDITION(lhs.type().id() == ID_struct_tag); + auto const &type = to_struct_tag_type(lhs.type()); + auto const &ns = namespacet{goto_model.symbol_table}; + for(auto const &component : ns.follow_tag(type).components()) + { + initialize(member_exprt{lhs, component}, depth, body); + } +} + +void recursive_initializationt::initialize_pointer( + const exprt &lhs, + std::size_t depth, + 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}}); + if(depth < initialization_config.max_nondet_tree_depth) + { + if(depth < initialization_config.min_null_tree_depth) + { + initialize(pointee, depth + 1, body); + body.add(code_assignt{lhs, address_of_exprt{pointee}}); + } + else + { + code_blockt then_case{}; + initialize(pointee, depth + 1, 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, + 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..24fa566031f --- /dev/null +++ b/src/goto-harness/recursive_initialization.h @@ -0,0 +1,58 @@ +/******************************************************************\ + +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: + 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 body: The code block to write initialisation code to. + void initialize(const exprt &lhs, std::size_t depth, 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, code_blockt &body); + void + initialize_pointer(const exprt &lhs, std::size_t depth, code_blockt &body); + void + initialize_nondet(const exprt &lhs, std::size_t depth, code_blockt &body); +}; + +#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H From 550e6abfc6fe9579f0c92ef650969c643f791bae Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 15 Feb 2019 16:01:52 +0000 Subject: [PATCH 4/4] Only apply tree limit to recursive struct Now the depth limit only applies to structs if we have seen this struct before (i.e. the initialisation chain is recursive) --- .../main.c | 36 +++++++++++++++++++ .../test.desc | 8 +++++ .../function_call_harness_generator.cpp | 31 +++++++++++++--- src/goto-harness/recursive_initialization.cpp | 27 ++++++++++---- src/goto-harness/recursive_initialization.h | 30 ++++++++++++---- 5 files changed, 113 insertions(+), 19 deletions(-) create mode 100644 regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c create mode 100644 regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc 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/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index fb353e97b12..077391b772f 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -15,6 +15,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include "function_harness_generator_options.h" @@ -79,14 +80,34 @@ void function_call_harness_generatort::handle_option( else if(option == FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT) { auto const value = require_exactly_one_value(option, values); - p_impl->recursive_initialization_config.min_null_tree_depth = - std::stoul(value); + 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); - p_impl->recursive_initialization_config.max_nondet_tree_depth = - std::stoul(value); + 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 { @@ -176,7 +197,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for( code_blockt &block, const exprt &lhs) { - recursive_initialization->initialize(lhs, 0, block); + recursive_initialization->initialize(lhs, 0, {}, block); } void function_call_harness_generatort::validate_options() diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 90435797569..4afd950ea15 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -26,20 +26,21 @@ recursive_initializationt::recursive_initializationt( 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, body); + initialize_struct_tag(lhs, depth, known_tags, body); } else if(type.id() == ID_pointer) { - initialize_pointer(lhs, depth, body); + initialize_pointer(lhs, depth, known_tags, body); } else { - initialize_nondet(lhs, depth, body); + initialize_nondet(lhs, depth, known_tags, body); } } @@ -64,20 +65,24 @@ symbol_exprt recursive_initializationt::get_malloc_function() 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, body); + 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); @@ -92,17 +97,24 @@ void recursive_initializationt::initialize_pointer( allocate_objects.allocate_automatic_local_object(type.subtype(), "pointee"); allocate_objects.declare_created_symbols(body); body.add(code_assignt{lhs, null_pointer_exprt{type}}); - if(depth < initialization_config.max_nondet_tree_depth) + 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, body); + 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, 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}); } @@ -112,6 +124,7 @@ void recursive_initializationt::initialize_pointer( 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 index 24fa566031f..fe2c5ba0f47 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -28,6 +28,8 @@ struct recursive_initialization_configt class recursive_initializationt { public: + using recursion_sett = std::set; + recursive_initializationt( recursive_initialization_configt initialization_config, goto_modelt &goto_model); @@ -35,8 +37,13 @@ class recursive_initializationt /// 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, code_blockt &body); + void initialize( + const exprt &lhs, + std::size_t depth, + const recursion_sett &known_tags, + code_blockt &body); private: const recursive_initialization_configt initialization_config; @@ -47,12 +54,21 @@ class recursive_initializationt /// exist already. symbol_exprt get_malloc_function(); - void - initialize_struct_tag(const exprt &lhs, std::size_t depth, code_blockt &body); - void - initialize_pointer(const exprt &lhs, std::size_t depth, code_blockt &body); - void - initialize_nondet(const exprt &lhs, std::size_t depth, code_blockt &body); + 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