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 <[email protected]>
Co-authored-by: Hannes Steffenhagen <[email protected]>

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,27 @@
+#include <assert.h>
+
+#define NULL 0
+
+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,28 @@
+#include <assert.h>
+
+#define NULL 0
+
+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

@@ -180,16 +180,29 @@ 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 global_names = std::vector<irep_idt>{};
     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());
+        global_names.push_back(symbol.name);
       }
     }
+    for(auto const &global_name : global_names)
+    {
+      generate_initialisation_code_for(
+        function_body, symbol_table->lookup_ref(global_name).symbol_expr());
+    }
   }
 }
 

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 =