From 2c909868d173967a789d4c838b0839857849996a Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 23 Nov 2018 16:44:27 +0000 Subject: [PATCH 1/6] Move function body generation to goto instrument directory This is because we want to use the c nondet symbol factory from the ansi-c directory, and code in goto-programs should not depend on code in ansi-c. --- src/goto-instrument/Makefile | 1 + .../generate_function_bodies.cpp | 13 ++++++++----- .../generate_function_bodies.h | 0 src/goto-instrument/goto_instrument_parse_options.h | 2 +- src/goto-programs/Makefile | 1 - 5 files changed, 10 insertions(+), 7 deletions(-) rename src/{goto-programs => goto-instrument}/generate_function_bodies.cpp (98%) rename src/{goto-programs => goto-instrument}/generate_function_bodies.h (100%) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index c2bb06a36d0..6067aa4de8a 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -35,6 +35,7 @@ SRC = accelerate/accelerate.cpp \ full_slicer.cpp \ function.cpp \ function_modifies.cpp \ + generate_function_bodies.cpp \ goto_instrument_languages.cpp \ goto_instrument_main.cpp \ goto_instrument_parse_options.cpp \ diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp similarity index 98% rename from src/goto-programs/generate_function_bodies.cpp rename to src/goto-instrument/generate_function_bodies.cpp index c7d45a3803f..6176a9cdd0c 100644 --- a/src/goto-programs/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -8,13 +8,17 @@ Author: Diffblue Ltd. #include "generate_function_bodies.h" +#include +#include + +#include +#include + #include #include #include #include -#include "remove_skip.h" - void generate_function_bodiest::generate_function_body( goto_functiont &function, symbol_tablet &symbol_table, @@ -305,9 +309,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, { auto return_instruction = add_instruction(); return_instruction->make_return(); - return_instruction->code = code_returnt( - side_effect_expr_nondett( - function.type.return_type(), function_symbol.location)); + return_instruction->code = code_returnt(side_effect_expr_nondett( + function.type.return_type(), function_symbol.location)); } auto end_function_instruction = add_instruction(); end_function_instruction->make_end_function(); diff --git a/src/goto-programs/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h similarity index 100% rename from src/goto-programs/generate_function_bodies.h rename to src/goto-instrument/generate_function_bodies.h diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index a5179302446..49a00f66a24 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -27,8 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include "aggressive_slicer.h" +#include "generate_function_bodies.h" #include "count_eloc.h" diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index fdd55802453..da48da7c821 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -6,7 +6,6 @@ SRC = adjust_float_expressions.cpp \ destructor.cpp \ elf_reader.cpp \ format_strings.cpp \ - generate_function_bodies.cpp \ goto_asm.cpp \ goto_clean_expr.cpp \ goto_convert.cpp \ From 15e34b6905bf5b2f045e0b7d58782dd13ae8b402 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 23 Nov 2018 12:58:10 +0000 Subject: [PATCH 2/6] Add regression tests for havoc-ing of function arguments --- .../main.c | 12 +++++++ .../test.desc | 7 ++++ .../main.c | 14 ++++++++ .../test.desc | 8 +++++ .../main.c | 33 +++++++++++++++++++ .../test.desc | 8 +++++ .../main.c | 19 +++++++++++ .../test.desc | 8 +++++ .../main.c | 31 +++++++++++++++++ .../test.desc | 8 +++++ .../main.c | 26 +++++++++++++++ .../test.desc | 8 +++++ 12 files changed, 182 insertions(+) create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-simple/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c create mode 100644 regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c new file mode 100644 index 00000000000..9e557e515a7 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c @@ -0,0 +1,12 @@ +#include +#include + +void func(int *p); + +void main() +{ + int *p; + p = NULL; + + func(p); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc new file mode 100644 index 00000000000..c81743d4d72 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options havoc,params:p --pointer-check +^SIGNAL=0$ +^EXIT=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c b/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c new file mode 100644 index 00000000000..7a3cc50cbe1 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-simple/main.c @@ -0,0 +1,14 @@ +#include +#include + +void func(int *p); + +void main() +{ + int i; + i = 0; + + func(&i); + + assert(i == 0); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc new file mode 100644 index 00000000000..e6f3f142cf5 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options havoc,params:p +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line \d+ assertion i == 0: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c new file mode 100644 index 00000000000..4c7270f7527 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c @@ -0,0 +1,33 @@ +#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); + +void main() +{ + st1_t st; + + func(&st); + + assert(st.to_st2 != NULL); + assert(st.to_st2->to_st1 != NULL); + assert(st.to_st2->to_st1->to_st2 == NULL); + + assert(st.to_st2 != &dummy2); + assert(st.to_st2->to_st1 != &dummy1); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc new file mode 100644 index 00000000000..d8dd403aba8 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options 'havoc,params:p' --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c new file mode 100644 index 00000000000..44848513382 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c @@ -0,0 +1,19 @@ +#include +#include + +typedef struct st +{ + int data; +} st_t; + +void func(st_t *p); + +void main() +{ + st_t st; + st.data = 0; + + func(&st); + + assert(st.data == 0); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc new file mode 100644 index 00000000000..1f964d59ba4 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options havoc,params:p +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line \d+ assertion st.data == 0: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c new file mode 100644 index 00000000000..1a2dcac6a53 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c @@ -0,0 +1,31 @@ +#include +#include + +typedef struct st +{ + struct st *next; + struct st *prev; + int data; +} st_t; + +st_t dummy; + +void func(st_t *p); + +void main() +{ + st_t st; + + func(&st); + + assert(st.prev != NULL); + assert(st.prev != &dummy); + + assert(st.next != NULL); + assert(st.next != &dummy); + + assert(st.prev->prev == NULL); + assert(st.prev->next == NULL); + assert(st.next->prev == NULL); + assert(st.next->next == NULL); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc new file mode 100644 index 00000000000..ed0a9f66c67 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c new file mode 100644 index 00000000000..4d5f4c8d16b --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c @@ -0,0 +1,26 @@ +#include +#include + +typedef struct st +{ + struct st *next; + int data; +} st_t; + +st_t dummy; + +void func(st_t *p); + +void main() +{ + st_t st; + + func(&st); + + assert(st.next != NULL); + assert(st.next->next != NULL); + assert(st.next->next->next == NULL); + + assert(st.next != &dummy); + assert(st.next->next != &dummy); +} diff --git a/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc new file mode 100644 index 00000000000..ac6ee2cc354 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 3 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring From 3401a380594b2a792003c5f55608d80fa3bd0631 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 21 Nov 2018 14:47:31 +0000 Subject: [PATCH 3/6] Move function body generation before goto_check() instrumentation This is so we can use the goto_check() features (such as --pointer-check) in the regression tests for the function body generation feature (e.g., to ensure that the generated code for a function does not dereference a null pointer passed to the function, by using --pointer-check). A potential drawback is that goto check instrumentation code is also added to the code generated by the function body generation feature, which could affect performance. --- .../goto_instrument_parse_options.cpp | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f4b29d43e02..21f1cdecae1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1185,6 +1185,19 @@ void goto_instrument_parse_optionst::instrument_goto_program() remove_skip(goto_model); } + if(cmdline.isset("generate-function-body")) + { + auto generate_implementation = generate_function_bodies_factory( + cmdline.get_value("generate-function-body-options"), + goto_model.symbol_table, + *message_handler); + generate_function_bodies( + std::regex(cmdline.get_value("generate-function-body")), + *generate_implementation, + goto_model, + *message_handler); + } + // add generic checks, if needed goto_check(options, goto_model); @@ -1487,19 +1500,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() throw 0; } - if(cmdline.isset("generate-function-body")) - { - auto generate_implementation = generate_function_bodies_factory( - cmdline.get_value("generate-function-body-options"), - goto_model.symbol_table, - *message_handler); - generate_function_bodies( - std::regex(cmdline.get_value("generate-function-body")), - *generate_implementation, - goto_model, - *message_handler); - } - // aggressive slicer if(cmdline.isset("aggressive-slice")) { From 6cf798296c033e06b41e6805eb2f720c11f6c7d5 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 21 Nov 2018 15:28:13 +0000 Subject: [PATCH 4/6] Pass c object factory parameters to function body generation Parse the c object factory command line parameters when the function body generation is enabled, and pass the resulting c_object_factory_parameterst object along to an appropriate subclass of generate_function_bodiest. --- src/goto-instrument/generate_function_bodies.cpp | 16 +++++++++++++--- src/goto-instrument/generate_function_bodies.h | 2 ++ .../goto_instrument_parse_options.cpp | 9 +++++++++ .../goto_instrument_parse_options.h | 3 +++ 4 files changed, 27 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 6176a9cdd0c..598ed439323 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -157,11 +157,13 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, havoc_generate_function_bodiest( std::vector globals_to_havoc, std::regex parameters_to_havoc, + const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler) : generate_function_bodiest(), messaget(message_handler), globals_to_havoc(std::move(globals_to_havoc)), - parameters_to_havoc(std::move(parameters_to_havoc)) + parameters_to_havoc(std::move(parameters_to_havoc)), + object_factory_parameters(object_factory_parameters) { } @@ -321,6 +323,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, private: const std::vector globals_to_havoc; std::regex parameters_to_havoc; + const c_object_factory_parameterst &object_factory_parameters; }; class generate_function_bodies_errort : public std::runtime_error @@ -336,13 +339,17 @@ class generate_function_bodies_errort : public std::runtime_error /// \see generate_function_bodies for the syntax of the options parameter std::unique_ptr generate_function_bodies_factory( const std::string &options, + const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler) { if(options.empty() || options == "nondet-return") { return util_make_unique( - std::vector{}, std::regex{}, message_handler); + std::vector{}, + std::regex{}, + object_factory_parameters, + message_handler); } if(options == "assume-false") @@ -411,7 +418,10 @@ std::unique_ptr generate_function_bodies_factory( } } return util_make_unique( - std::move(globals_to_havoc), std::move(params_regex), message_handler); + std::move(globals_to_havoc), + std::move(params_regex), + object_factory_parameters, + message_handler); } throw generate_function_bodies_errort("Can't parse \"" + options + "\""); } diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index c909bb4bdd1..88b1b1772fc 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include +#include #include #include #include @@ -59,6 +60,7 @@ class generate_function_bodiest std::unique_ptr generate_function_bodies_factory( const std::string &options, + const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 21f1cdecae1..7e191181b58 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -64,6 +64,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include @@ -1187,8 +1189,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("generate-function-body")) { + optionst c_object_factory_options; + parse_c_object_factory_options(cmdline, c_object_factory_options); + c_object_factory_parameterst object_factory_parameters( + c_object_factory_options); + auto generate_implementation = generate_function_bodies_factory( cmdline.get_value("generate-function-body-options"), + object_factory_parameters, goto_model.symbol_table, *message_handler); generate_function_bodies( @@ -1622,6 +1630,7 @@ void goto_instrument_parse_optionst::help() // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" HELP_REPLACE_FUNCTION_BODY + HELP_ANSI_C_LANGUAGE "\n" "Loop transformations:\n" " --k-induction check loops with k-induction\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 49a00f66a24..7e70a1ff1d7 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H +#include + #include #include #include @@ -104,6 +106,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_REPLACE_CALLS \ "(validate-goto-binary)" \ OPT_VALIDATE \ + OPT_ANSI_C_LANGUAGE \ // empty last line // clang-format on From 3e4701a4ad0fb55cef1b52ea32a4f360f421d883 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 21 Nov 2018 16:21:28 +0000 Subject: [PATCH 5/6] Adapt c nondet symbol factory for use in function body generation We essentially make two changes to the c nondet symbol factory: - A parameter assign_const is added to gen_nondet_init(). When false, an object of const type is not nondet assigned. This will be used in the function body generation feature to not havoc const arguments (e.g., the targets of pointers to const int) - A parameter lifetime (an enum of type lifetimet) is added to the constructor of symbol_factoryt. It indicates whether it uses lifetimet::AUTOMATIC_LOCAL, lifetimet::STATIC_GLOBAL, or lifetimet::DYNAMIC when allocating new objects with allocate_object(). Previously this was hardcoded to behave like lifetime::AUTOMATIC_LOCAL. However, in the function body generation we need to add code to a function to allocate dynamic objects. This is because the function may be called multiple times, hence using local or global variables does not work. --- src/ansi-c/ansi_c_entry_point.cpp | 3 +- src/ansi-c/c_nondet_symbol_factory.cpp | 94 ++++++++------------------ src/ansi-c/c_nondet_symbol_factory.h | 71 ++++++++++++++++++- 3 files changed, 99 insertions(+), 69 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index a6ce51d967a..ea08e404cb8 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -42,7 +42,8 @@ exprt::operandst build_function_environment( base_name, p.type(), p.source_location(), - object_factory_parameters); + object_factory_parameters, + lifetimet::AUTOMATIC_LOCAL); } return main_arguments; diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index ddb9162eb7c..f53b09b1d5a 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -25,79 +25,29 @@ Author: Diffblue Ltd. #include -class symbol_factoryt -{ - symbol_tablet &symbol_table; - const source_locationt &loc; - namespacet ns; - const c_object_factory_parameterst &object_factory_params; - - allocate_objectst allocate_objects; - - typedef std::set recursion_sett; - -public: - symbol_factoryt( - symbol_tablet &_symbol_table, - const source_locationt &loc, - const c_object_factory_parameterst &object_factory_params) - : symbol_table(_symbol_table), - loc(loc), - ns(_symbol_table), - object_factory_params(object_factory_params), - allocate_objects(ID_C, loc, loc.get_function(), symbol_table) - {} - - void gen_nondet_init( - code_blockt &assignments, - const exprt &expr, - const std::size_t depth = 0, - recursion_sett recursion_set = recursion_sett()); - - void add_created_symbol(const symbolt *symbol_ptr) - { - allocate_objects.add_created_symbol(symbol_ptr); - } - - void declare_created_symbols(code_blockt &init_code) - { - allocate_objects.declare_created_symbols(init_code); - } - - void mark_created_symbols_as_input(code_blockt &init_code) - { - allocate_objects.mark_created_symbols_as_input(init_code); - } - -private: - /// Generate initialisation code for each array element - /// \param assignments: The code block to add code to - /// \param expr: An expression of array type - /// \param depth: The struct recursion depth - /// \param recursion_set: The struct recursion set - /// \see gen_nondet_init For the meaning of the last 2 parameters - void gen_nondet_array_init( - code_blockt &assignments, - const exprt &expr, - std::size_t depth, - const recursion_sett &recursion_set); -}; - /// Creates a nondet for expr, including calling itself recursively to make /// appropriate symbols to point to if expr is a pointer. /// \param assignments: The code block to add code to /// \param expr: The expression which we are generating a non-determinate value /// for -/// \param depth: number of pointers followed so far during initialisation -/// \param recursion_set: names of structs seen so far on current pointer chain +/// \param depth number of pointers followed so far during initialisation +/// \param recursion_set names of structs seen so far on current pointer chain +/// \param assign_const Indicates whether const objects should be nondet +/// initialized void symbol_factoryt::gen_nondet_init( code_blockt &assignments, const exprt &expr, const std::size_t depth, - recursion_sett recursion_set) + recursion_sett recursion_set, + const bool assign_const) { const typet &type = expr.type(); + if(!assign_const && expr.type().get_bool(ID_C_constant)) + { + return; + } + if(type.id()==ID_pointer) { // dereferenced type @@ -120,10 +70,10 @@ void symbol_factoryt::gen_nondet_init( code_blockt non_null_inst; - exprt init_expr = allocate_objects.allocate_automatic_local_object( - non_null_inst, expr, subtype); + exprt init_expr = + allocate_objects.allocate_object(non_null_inst, expr, subtype, lifetime); - gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set); + gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true); if(depth < object_factory_params.min_null_tree_depth) { @@ -165,12 +115,18 @@ void symbol_factoryt::gen_nondet_init( for(const auto &component : struct_type.components()) { const typet &component_type = component.type(); + + if(!assign_const && component_type.get_bool(ID_C_constant)) + { + continue; + } + const irep_idt name = component.get_name(); member_exprt me(expr, name, component_type); me.add_source_location() = loc; - gen_nondet_init(assignments, me, depth, recursion_set); + gen_nondet_init(assignments, me, depth, recursion_set, assign_const); } } else if(type.id() == ID_array) @@ -221,6 +177,8 @@ void symbol_factoryt::gen_nondet_array_init( /// \param loc: The location to assign to generated code /// \param object_factory_parameters: configuration parameters for the object /// factory +/// \param lifetime: Lifetime of the allocated object (AUTOMATIC_LOCAL, +/// STATIC_GLOBAL, or DYNAMIC) /// \return Returns the symbol_exprt for the symbol created symbol_exprt c_nondet_symbol_factory( code_blockt &init_code, @@ -228,7 +186,8 @@ symbol_exprt c_nondet_symbol_factory( const irep_idt base_name, const typet &type, const source_locationt &loc, - const c_object_factory_parameterst &object_factory_parameters) + const c_object_factory_parameterst &object_factory_parameters, + const lifetimet lifetime) { irep_idt identifier=id2string(goto_functionst::entry_point())+ "::"+id2string(base_name); @@ -247,7 +206,8 @@ symbol_exprt c_nondet_symbol_factory( bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr); CHECK_RETURN(!moving_symbol_failed); - symbol_factoryt state(symbol_table, loc, object_factory_parameters); + symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime); + code_blockt assignments; state.gen_nondet_init(assignments, main_symbol_expr); diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h index c4d74f6021f..9ccda4d90f9 100644 --- a/src/ansi-c/c_nondet_symbol_factory.h +++ b/src/ansi-c/c_nondet_symbol_factory.h @@ -14,15 +14,84 @@ Author: Diffblue Ltd. #include "c_object_factory_parameters.h" +#include +#include + +#include #include #include +class symbol_factoryt +{ + symbol_tablet &symbol_table; + const source_locationt &loc; + namespacet ns; + const c_object_factory_parameterst &object_factory_params; + + allocate_objectst allocate_objects; + + const lifetimet lifetime; + +public: + typedef std::set recursion_sett; + + symbol_factoryt( + symbol_tablet &_symbol_table, + const source_locationt &loc, + const c_object_factory_parameterst &object_factory_params, + const lifetimet lifetime) + : symbol_table(_symbol_table), + loc(loc), + ns(_symbol_table), + object_factory_params(object_factory_params), + allocate_objects(ID_C, loc, loc.get_function(), symbol_table), + lifetime(lifetime) + { + } + + void gen_nondet_init( + code_blockt &assignments, + const exprt &expr, + const std::size_t depth = 0, + recursion_sett recursion_set = recursion_sett(), + const bool assign_const = true); + + void add_created_symbol(const symbolt *symbol_ptr) + { + allocate_objects.add_created_symbol(symbol_ptr); + } + + void declare_created_symbols(code_blockt &init_code) + { + allocate_objects.declare_created_symbols(init_code); + } + + void mark_created_symbols_as_input(code_blockt &init_code) + { + allocate_objects.mark_created_symbols_as_input(init_code); + } + +private: + /// Generate initialisation code for each array element + /// \param assignments: The code block to add code to + /// \param expr: An expression of array type + /// \param depth: The struct recursion depth + /// \param recursion_set: The struct recursion set + /// \see gen_nondet_init For the meaning of the last 2 parameters + void gen_nondet_array_init( + code_blockt &assignments, + const exprt &expr, + std::size_t depth, + const recursion_sett &recursion_set); +}; + symbol_exprt c_nondet_symbol_factory( code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &, - const c_object_factory_parameterst &object_factory_parameters); + const c_object_factory_parameterst &object_factory_parameters, + const lifetimet lifetime); #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H From ade4e667f7bbd3d37d242b38d82aa847e81fbbdd Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 21 Nov 2018 16:24:28 +0000 Subject: [PATCH 6/6] Use c nondet object factory in function body generation This removes the existing code in the function body generation for havoc-ing objects (in havoc_expr_rec()) and replaces it with calls to the c nondet symbol factory (gen_nondet_init()). --- .../generate_function_bodies.cpp | 167 +++++++----------- .../generate_function_bodies.h | 2 +- 2 files changed, 66 insertions(+), 103 deletions(-) diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 598ed439323..b0dea5c7f88 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -68,7 +68,7 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest protected: void generate_function_body_impl( goto_functiont &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); @@ -91,7 +91,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest protected: void generate_function_body_impl( goto_functiont &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); @@ -122,7 +122,7 @@ class assert_false_then_assume_false_generate_function_bodiest protected: void generate_function_body_impl( goto_functiont &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); @@ -150,8 +150,7 @@ class assert_false_then_assume_false_generate_function_bodiest } }; -class havoc_generate_function_bodiest : public generate_function_bodiest, - private messaget +class havoc_generate_function_bodiest : public generate_function_bodiest { public: havoc_generate_function_bodiest( @@ -160,107 +159,52 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler) : generate_function_bodiest(), - messaget(message_handler), globals_to_havoc(std::move(globals_to_havoc)), parameters_to_havoc(std::move(parameters_to_havoc)), - object_factory_parameters(object_factory_parameters) + object_factory_parameters(object_factory_parameters), + message(message_handler) { } private: void havoc_expr_rec( const exprt &lhs, - const namespacet &ns, - const std::function &add_instruction, - const irep_idt &function_name) const + const std::size_t initial_depth, + const source_locationt &source_location, + symbol_tablet &symbol_table, + goto_programt &dest) const { - // resolve type symbols - auto const lhs_type = ns.follow(lhs.type()); - // skip constants - if(!lhs_type.get_bool(ID_C_constant)) - { - // expand arrays, structs and union, everything else gets - // assigned nondet - if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union) - { - // Note: In the case of unions it's often enough to assign - // just one member; However consider a case like - // union { struct { const int x; int y; } a; - // struct { int x; const int y; } b;}; - // in this case both a.y and b.x must be assigned - // otherwise these parts stay constant even though - // they could've changed (note that type punning through - // unions is allowed in the C standard but forbidden in C++) - // so we're assigning all members even in the case of - // unions just to be safe - auto const lhs_struct_type = to_struct_union_type(lhs_type); - for(auto const &component : lhs_struct_type.components()) - { - havoc_expr_rec( - member_exprt(lhs, component.get_name(), component.type()), - ns, - add_instruction, - function_name); - } - } - else if(lhs_type.id() == ID_array) - { - auto const lhs_array_type = to_array_type(lhs_type); - if(!lhs_array_type.subtype().get_bool(ID_C_constant)) - { - bool constant_known_array_size = lhs_array_type.size().is_constant(); - if(!constant_known_array_size) - { - warning() << "Cannot havoc non-const array " << format(lhs) - << " in function " << function_name - << ": Unknown array size" << eom; - } - else - { - auto const array_size = - numeric_cast(lhs_array_type.size()); - INVARIANT( - array_size.has_value(), - "Array size should be known constant integer"); - if(array_size.value() == 0) - { - // Pretty much the same thing as a unknown size array - // Technically not allowed by the C standard, but we model - // unknown size arrays in structs this way - warning() << "Cannot havoc non-const array " << format(lhs) - << " in function " << function_name << ": Array size 0" - << eom; - } - else - { - for(mp_integer i = 0; i < array_size.value(); ++i) - { - auto const index = - from_integer(i, lhs_array_type.size().type()); - havoc_expr_rec( - index_exprt(lhs, index, lhs_array_type.subtype()), - ns, - add_instruction, - function_name); - } - } - } - } - } - else - { - auto assign_instruction = add_instruction(); - assign_instruction->make_assignment( - code_assignt( - lhs, side_effect_expr_nondett(lhs_type, lhs.source_location()))); - } - } + symbol_factoryt symbol_factory( + symbol_table, + source_location, + object_factory_parameters, + lifetimet::DYNAMIC); + + code_blockt assignments; + + symbol_factory.gen_nondet_init( + assignments, + lhs, + initial_depth, + symbol_factoryt::recursion_sett(), + false); // do not initialize const objects at the top level + + code_blockt init_code; + + symbol_factory.declare_created_symbols(init_code); + init_code.append(assignments); + + goto_programt tmp_dest; + goto_convert( + init_code, symbol_table, tmp_dest, message.get_message_handler(), ID_C); + + dest.destructive_append(tmp_dest); } protected: void generate_function_body_impl( goto_functiont &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); @@ -276,18 +220,29 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, { if( parameter.type().id() == ID_pointer && + !parameter.type().subtype().get_bool(ID_C_constant) && std::regex_match( id2string(parameter.get_base_name()), parameters_to_havoc)) { - // if (param != nullptr) { *param = nondet(); } auto goto_instruction = add_instruction(); + + const irep_idt base_name = parameter.get_base_name(); + CHECK_RETURN(!base_name.empty()); + + dereference_exprt dereference_expr( + symbol_exprt(parameter.get_identifier(), parameter.type()), + parameter.type().subtype()); + + goto_programt dest; havoc_expr_rec( - dereference_exprt( - symbol_exprt(parameter.get_identifier(), parameter.type()), - parameter.type().subtype()), - ns, - add_instruction, - function_name); + dereference_expr, + 1, // depth 1 since we pass the dereferenced pointer + function_symbol.location, + symbol_table, + dest); + + function.body.destructive_append(dest); + auto label_instruction = add_instruction(); goto_instruction->make_goto( label_instruction, @@ -301,12 +256,19 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, for(auto const &global_id : globals_to_havoc) { auto const &global_sym = symbol_table.lookup_ref(global_id); + + goto_programt dest; + havoc_expr_rec( symbol_exprt(global_sym.name, global_sym.type), - ns, - add_instruction, - function_name); + 0, + function_symbol.location, + symbol_table, + dest); + + function.body.destructive_append(dest); } + if(function.type.return_type() != void_typet()) { auto return_instruction = add_instruction(); @@ -324,6 +286,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, const std::vector globals_to_havoc; std::regex parameters_to_havoc; const c_object_factory_parameterst &object_factory_parameters; + mutable messaget message; }; class generate_function_bodies_errort : public std::runtime_error diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index 88b1b1772fc..ebbb1dda05a 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -32,7 +32,7 @@ class generate_function_bodiest /// \param function_name: Identifier of function virtual void generate_function_body_impl( goto_functiont &function, - const symbol_tablet &symbol_table, + symbol_tablet &symbol_table, const irep_idt &function_name) const = 0; public: