Merge pull request #4277 from NlightNFotis/fix-goto-harness-pointer-init

Fix: Do not nondet functions and fix scoping issue

Author: NlightNFotis

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

regression/goto-harness/nondet_elements_longer_lists/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+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;
+  }
+}

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
+--

regression/goto-harness/nondet_elements_longer_lists_global/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+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;
+  }
+}

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
+--

src/goto-harness/function_call_harness_generator.cpp

@@ -182,16 +182,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<symbol_exprt>{};
     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);
+    }
   }
 }
 

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 =