From cefb1ddb892af558ac5d2d1339fac22c6568cd87 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 22 Feb 2019 17:33:39 +0000 Subject: [PATCH] Fix: Do not nondet functions and fix scoping issue In goto-harness: - we used is_static && is_lvalue to determine something was global. Turns out that this also applies to extern functions for some reason, so we ended up accidentally creating nondet assignments to those. We now check type.id() != ID_code as well. - we declared pointers to local variables. In if blocks. Which went out of scope before using them. This meant we had a bunch of dangling references. We solve this by creating global variables for our pointer-pointees instead of local ones. Co-authored-by: Fotis Koutoulakis Co-authored-by: Hannes Steffenhagen --- regression/goto-harness/chain.sh | 2 +- .../nondet_elements_longer_lists/main.c | 25 ++++++++++++++++++ .../nondet_elements_longer_lists/test.desc | 10 +++++++ .../main.c | 26 +++++++++++++++++++ .../test.desc | 10 +++++++ .../function_call_harness_generator.cpp | 14 +++++++++- src/goto-harness/recursive_initialization.cpp | 13 ++++++++-- 7 files changed, 96 insertions(+), 4 deletions(-) create mode 100644 regression/goto-harness/nondet_elements_longer_lists/main.c create mode 100644 regression/goto-harness/nondet_elements_longer_lists/test.desc create mode 100644 regression/goto-harness/nondet_elements_longer_lists_global/main.c create mode 100644 regression/goto-harness/nondet_elements_longer_lists_global/test.desc diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh index ea339d8cb49..eb430bf9a17 100755 --- a/regression/goto-harness/chain.sh +++ b/regression/goto-harness/chain.sh @@ -24,4 +24,4 @@ if [ -e "${name}-mod.gb" ] ; then fi $goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} -$cbmc --function $entry_point "${name}-mod.gb" +$cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions diff --git a/regression/goto-harness/nondet_elements_longer_lists/main.c b/regression/goto-harness/nondet_elements_longer_lists/main.c new file mode 100644 index 00000000000..a3e135a442e --- /dev/null +++ b/regression/goto-harness/nondet_elements_longer_lists/main.c @@ -0,0 +1,25 @@ +#include + +typedef struct list +{ + int datum; + struct list *next; +} list_nodet; + +void test_function(list_nodet *node) +{ + int i = 0; + list_nodet *list_walker = node; + while(list_walker) + { + list_walker->datum = ++i; + list_walker = list_walker->next; + } + list_walker = node; + i = 0; + while(list_walker) + { + assert(list_walker->datum == ++i); + list_walker = list_walker->next; + } +} diff --git a/regression/goto-harness/nondet_elements_longer_lists/test.desc b/regression/goto-harness/nondet_elements_longer_lists/test.desc new file mode 100644 index 00000000000..88dc31c264c --- /dev/null +++ b/regression/goto-harness/nondet_elements_longer_lists/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function +\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS +\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS +\[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- diff --git a/regression/goto-harness/nondet_elements_longer_lists_global/main.c b/regression/goto-harness/nondet_elements_longer_lists_global/main.c new file mode 100644 index 00000000000..23e967f0d99 --- /dev/null +++ b/regression/goto-harness/nondet_elements_longer_lists_global/main.c @@ -0,0 +1,26 @@ +#include + +typedef struct list +{ + int datum; + struct list *next; +} list_nodet; + +list_nodet *global_list; +void test_function(void) +{ + int i = 0; + list_nodet *list_walker = global_list; + while(list_walker) + { + list_walker->datum = ++i; + list_walker = list_walker->next; + } + list_walker = global_list; + i = 0; + while(list_walker) + { + assert(list_walker->datum == ++i); + list_walker = list_walker->next; + } +} diff --git a/regression/goto-harness/nondet_elements_longer_lists_global/test.desc b/regression/goto-harness/nondet_elements_longer_lists_global/test.desc new file mode 100644 index 00000000000..22bfdb8bfd7 --- /dev/null +++ b/regression/goto-harness/nondet_elements_longer_lists_global/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals +\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS +\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS +\[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 077391b772f..fe25e0e9da7 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -180,16 +180,28 @@ void function_call_harness_generatort::implt::generate_nondet_globals( { if(nondet_globals) { + // generating initialisation code may introduce new globals + // i.e. modify the symbol table. + // Modifying the symbol table while iterating over it is not + // a good idea, therefore we just collect the names of globals + // we need to initialise first and then generate the + // initialisation code for all of them. + auto globals = std::vector{}; for(const auto &symbol_table_entry : *symbol_table) { const auto &symbol = symbol_table_entry.second; if( symbol.is_static_lifetime && symbol.is_lvalue && + symbol.type.id() != ID_code && !has_prefix(id2string(symbol.name), CPROVER_PREFIX)) { - generate_initialisation_code_for(function_body, symbol.symbol_expr()); + globals.push_back(symbol.symbol_expr()); } } + for(auto const &global : globals) + { + generate_initialisation_code_for(function_body, global); + } } } diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 4afd950ea15..259063f6168 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -93,8 +93,17 @@ void recursive_initializationt::initialize_pointer( 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"); + symbolt &pointee_symbol = get_fresh_aux_symbol( + type.subtype(), + "__goto_harness", + "pointee", + lhs.source_location(), + initialization_config.mode, + goto_model.symbol_table); + pointee_symbol.is_static_lifetime = true; + pointee_symbol.is_lvalue = true; + + auto pointee = pointee_symbol.symbol_expr(); allocate_objects.declare_created_symbols(body); body.add(code_assignt{lhs, null_pointer_exprt{type}}); bool is_unknown_struct_tag =