Only apply tree limit to recursive struct

Now the depth limit only applies to structs if we have seen this struct
before (i.e. the initialisation chain is recursive)

Author: NlightNFotis

regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct A A;
+typedef struct B B;
+typedef struct C C;
+typedef struct D D;
+
+struct A
+{
+  B *b;
+};
+
+struct B
+{
+  C *c;
+};
+
+struct C
+{
+  D *d;
+};
+
+struct D
+{
+  A *a;
+};
+
+void func(A *a)
+{
+  assert(a != NULL);
+  assert(a->b != NULL);
+  assert(a->b->c != NULL);
+  assert(a->b->c->d != NULL);
+  assert(a->b->c->d->a == NULL);
+}

regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 1  --harness-type call-function
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/goto-harness/function_call_harness_generator.cpp

@@ -15,6 +15,7 @@ Author: Diffblue Ltd.
 #include <util/exception_utils.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
+#include <util/string2int.h>
 #include <util/ui_message.h>
 
 #include "function_harness_generator_options.h"
@@ -79,14 +80,34 @@ void function_call_harness_generatort::handle_option(
   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);
+    auto const min_null_tree_depth = string2optional<std::size_t>(value, 10);
+    if(min_null_tree_depth.has_value())
+    {
+      p_impl->recursive_initialization_config.min_null_tree_depth =
+        min_null_tree_depth.value();
+    }
+    else
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "failed to convert `" + value + "' to integer",
+        "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT};
+    }
   }
   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);
+    auto const max_nondet_tree_depth = string2optional<std::size_t>(value, 10);
+    if(max_nondet_tree_depth.has_value())
+    {
+      p_impl->recursive_initialization_config.max_nondet_tree_depth =
+        max_nondet_tree_depth.value();
+    }
+    else
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "failed to convert `" + value + "' to integer",
+        "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
+    }
   }
   else
   {
@@ -176,7 +197,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
   code_blockt &block,
   const exprt &lhs)
 {
-  recursive_initialization->initialize(lhs, 0, block);
+  recursive_initialization->initialize(lhs, 0, {}, block);
 }
 
 void function_call_harness_generatort::validate_options()

src/goto-harness/recursive_initialization.cpp

@@ -26,20 +26,21 @@ recursive_initializationt::recursive_initializationt(
 void recursive_initializationt::initialize(
   const exprt &lhs,
   std::size_t depth,
+  const recursion_sett &known_tags,
   code_blockt &body)
 {
   auto const &type = lhs.type();
   if(type.id() == ID_struct_tag)
   {
-    initialize_struct_tag(lhs, depth, body);
+    initialize_struct_tag(lhs, depth, known_tags, body);
   }
   else if(type.id() == ID_pointer)
   {
-    initialize_pointer(lhs, depth, body);
+    initialize_pointer(lhs, depth, known_tags, body);
   }
   else
   {
-    initialize_nondet(lhs, depth, body);
+    initialize_nondet(lhs, depth, known_tags, body);
   }
 }
 
@@ -64,20 +65,24 @@ symbol_exprt recursive_initializationt::get_malloc_function()
 void recursive_initializationt::initialize_struct_tag(
   const exprt &lhs,
   std::size_t depth,
+  const recursion_sett &known_tags,
   code_blockt &body)
 {
   PRECONDITION(lhs.type().id() == ID_struct_tag);
   auto const &type = to_struct_tag_type(lhs.type());
+  auto new_known_tags = known_tags;
+  new_known_tags.insert(type.get_identifier());
   auto const &ns = namespacet{goto_model.symbol_table};
   for(auto const &component : ns.follow_tag(type).components())
   {
-    initialize(member_exprt{lhs, component}, depth, body);
+    initialize(member_exprt{lhs, component}, depth, new_known_tags, body);
   }
 }
 
 void recursive_initializationt::initialize_pointer(
   const exprt &lhs,
   std::size_t depth,
+  const recursion_sett &known_tags,
   code_blockt &body)
 {
   PRECONDITION(lhs.type().id() == ID_pointer);
@@ -92,17 +97,24 @@ void recursive_initializationt::initialize_pointer(
     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)
+  bool is_unknown_struct_tag =
+    can_cast_type<tag_typet>(type.subtype()) &&
+    known_tags.find(to_tag_type(type.subtype()).get_identifier()) ==
+      known_tags.end();
+
+  if(
+    depth < initialization_config.max_nondet_tree_depth ||
+    is_unknown_struct_tag)
   {
     if(depth < initialization_config.min_null_tree_depth)
     {
-      initialize(pointee, depth + 1, body);
+      initialize(pointee, depth + 1, known_tags, body);
       body.add(code_assignt{lhs, address_of_exprt{pointee}});
     }
     else
     {
       code_blockt then_case{};
-      initialize(pointee, depth + 1, then_case);
+      initialize(pointee, depth + 1, known_tags, then_case);
       then_case.add(code_assignt{lhs, address_of_exprt{pointee}});
       body.add(code_ifthenelset{choice, then_case});
     }
@@ -112,6 +124,7 @@ void recursive_initializationt::initialize_pointer(
 void recursive_initializationt::initialize_nondet(
   const exprt &lhs,
   std::size_t depth,
+  const recursion_sett &known_tags,
   code_blockt &body)
 {
   body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}});

src/goto-harness/recursive_initialization.h

@@ -28,15 +28,22 @@ struct recursive_initialization_configt
 class recursive_initializationt
 {
 public:
+  using recursion_sett = std::set<irep_idt>;
+
   recursive_initializationt(
     recursive_initialization_configt initialization_config,
     goto_modelt &goto_model);
 
   /// Generate initialisation code for lhs into body.
   /// \param lhs: The expression to initialise.
   /// \param depth: The number of pointer follows. Starts at 0.
+  /// \param known_tags: The struct tags we've already seen during recursion.
   /// \param body: The code block to write initialisation code to.
-  void initialize(const exprt &lhs, std::size_t depth, code_blockt &body);
+  void initialize(
+    const exprt &lhs,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body);
 
 private:
   const recursive_initialization_configt initialization_config;
@@ -47,12 +54,21 @@ class recursive_initializationt
   /// exist already.
   symbol_exprt get_malloc_function();
 
-  void
-  initialize_struct_tag(const exprt &lhs, std::size_t depth, code_blockt &body);
-  void
-  initialize_pointer(const exprt &lhs, std::size_t depth, code_blockt &body);
-  void
-  initialize_nondet(const exprt &lhs, std::size_t depth, code_blockt &body);
+  void initialize_struct_tag(
+    const exprt &lhs,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body);
+  void initialize_pointer(
+    const exprt &lhs,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body);
+  void initialize_nondet(
+    const exprt &lhs,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body);
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H