Add recursive initialisation of structs

Recursively initialise non-deterministically
struct components and pointers.

Co-authored-by: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Co-authored-by: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>

Author: NlightNFotis

regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/main.c

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

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

regression/goto-harness/pointer-function-parameters-struct-non-recursive/main.c

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

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

regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/main.c

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

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

regression/goto-harness/pointer-function-parameters-struct-simple-recursion/main.c

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

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

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

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_initializationt> 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_initializationt>(
+    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()