Add recursive initialisation of structs

Recursively initialise non-deterministically
struct components and pointers.

Co-authored-by: Fotis Koutoulakis <[email protected]>
Co-authored-by: Hannes Steffenhagen <[email protected]>

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

src/goto-harness/function_harness_generator_options.h

@@ -11,11 +11,16 @@ Author: Diffblue Ltd.
 
 #define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
 #define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals"
+#define FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth"
+#define FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT                   \
+  "max-nondet-tree-depth"
 
 // clang-format off
 #define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
   "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"                             \
   "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")"                        \
+  "(" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):"                  \
+  "(" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):"                \
 // FUNCTION_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -27,6 +32,12 @@ Author: Diffblue Ltd.
   "      the function the harness should call\n"                               \
   "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT                           \
   "      set global variables to non-deterministic values in harness\n"        \
+  "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT                      \
+  " N      minimum level at which a pointer can first be\n"                    \
+  "        NULL in a recursively nondet initialized struct\n"                  \
+  "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT                    \
+  " N    limit size of nondet (e.g. input) object tree;\n"                     \
+  "      at level N pointers are set to null\n"                                \
   // FUNCTION_HARNESS_GENERATOR_HELP
 
 // clang-format on

src/goto-harness/recursive_initialization.cpp

@@ -0,0 +1,118 @@
+/******************************************************************\
+
+Module: recursive_initialization
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include "recursive_initialization.h"
+
+#include <util/allocate_objects.h>
+#include <util/c_types.h>
+#include <util/fresh_symbol.h>
+#include <util/irep.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+
+recursive_initializationt::recursive_initializationt(
+  recursive_initialization_configt initialization_config,
+  goto_modelt &goto_model)
+  : initialization_config(std::move(initialization_config)),
+    goto_model(goto_model)
+{
+}
+
+void recursive_initializationt::initialize(
+  const exprt &lhs,
+  std::size_t depth,
+  code_blockt &body)
+{
+  auto const &type = lhs.type();
+  if(type.id() == ID_struct_tag)
+  {
+    initialize_struct_tag(lhs, depth, body);
+  }
+  else if(type.id() == ID_pointer)
+  {
+    initialize_pointer(lhs, depth, body);
+  }
+  else
+  {
+    initialize_nondet(lhs, depth, body);
+  }
+}
+
+symbol_exprt recursive_initializationt::get_malloc_function()
+{
+  // unused for now, we'll need it for arrays
+  auto malloc_sym = goto_model.symbol_table.lookup("malloc");
+  if(malloc_sym == nullptr)
+  {
+    symbolt new_malloc_sym;
+    new_malloc_sym.type = code_typet{code_typet{
+      {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}};
+    new_malloc_sym.name = new_malloc_sym.pretty_name =
+      new_malloc_sym.base_name = "malloc";
+    new_malloc_sym.mode = initialization_config.mode;
+    goto_model.symbol_table.insert(new_malloc_sym);
+    return new_malloc_sym.symbol_expr();
+  }
+  return malloc_sym->symbol_expr();
+}
+
+void recursive_initializationt::initialize_struct_tag(
+  const exprt &lhs,
+  std::size_t depth,
+  code_blockt &body)
+{
+  PRECONDITION(lhs.type().id() == ID_struct_tag);
+  auto const &type = to_struct_tag_type(lhs.type());
+  auto const &ns = namespacet{goto_model.symbol_table};
+  for(auto const &component : ns.follow_tag(type).components())
+  {
+    initialize(member_exprt{lhs, component}, depth, body);
+  }
+}
+
+void recursive_initializationt::initialize_pointer(
+  const exprt &lhs,
+  std::size_t depth,
+  code_blockt &body)
+{
+  PRECONDITION(lhs.type().id() == ID_pointer);
+  auto const &type = to_pointer_type(lhs.type());
+  allocate_objectst allocate_objects{initialization_config.mode,
+                                     type.source_location(),
+                                     "initializer",
+                                     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");
+  allocate_objects.declare_created_symbols(body);
+  body.add(code_assignt{lhs, null_pointer_exprt{type}});
+  if(depth < initialization_config.max_nondet_tree_depth)
+  {
+    if(depth < initialization_config.min_null_tree_depth)
+    {
+      initialize(pointee, depth + 1, body);
+      body.add(code_assignt{lhs, address_of_exprt{pointee}});
+    }
+    else
+    {
+      code_blockt then_case{};
+      initialize(pointee, depth + 1, then_case);
+      then_case.add(code_assignt{lhs, address_of_exprt{pointee}});
+      body.add(code_ifthenelset{choice, then_case});
+    }
+  }
+}
+
+void recursive_initializationt::initialize_nondet(
+  const exprt &lhs,
+  std::size_t depth,
+  code_blockt &body)
+{
+  body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}});
+}