Add recursive nondet struct initialization

Author: danpoe

src/ansi-c/ansi_c_entry_point.cpp

@@ -42,7 +42,6 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      true,
       object_factory_parameters);
   }
 

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -11,6 +11,8 @@ Author: Diffblue Ltd.
 
 #include "c_nondet_symbol_factory.h"
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
@@ -31,6 +33,8 @@ class symbol_factoryt
   namespacet ns;
   const c_object_factory_parameterst &object_factory_params;
 
+  typedef std::set<irep_idt> recursion_sett;
+
   const symbolt &c_new_tmp_symbol(
     const typet &type,
     const bool static_lifetime,
@@ -57,7 +61,11 @@ class symbol_factoryt
     const typet &allocate_type,
     const bool static_lifetime);
 
-  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
+  void gen_nondet_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const std::size_t depth = 0,
+    recursion_sett recursion_set = recursion_sett());
 };
 
 /// Create a new temporary static symbol
@@ -121,9 +129,13 @@ exprt symbol_factoryt::allocate_object(
 /// \param assignments: The code block to add code to
 /// \param expr: The expression which we are generating a non-determinate value
 ///   for
+/// \param depth number of pointers followed so far during initialisation
+/// \param recursion_set names of structs seen so far on current pointer chain
 void symbol_factoryt::gen_nondet_init(
   code_blockt &assignments,
-  const exprt &expr)
+  const exprt &expr,
+  const std::size_t depth,
+  recursion_sett recursion_set)
 {
   const typet &type=ns.follow(expr.type());
 
@@ -133,6 +145,22 @@ void symbol_factoryt::gen_nondet_init(
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype=ns.follow(pointer_type.subtype());
 
+    if(subtype.id() == ID_struct)
+    {
+      const struct_typet &struct_type = to_struct_type(subtype);
+      const irep_idt struct_tag = struct_type.get_tag();
+
+      if(
+        recursion_set.find(struct_tag) != recursion_set.end() &&
+        depth >= object_factory_params.max_nondet_tree_depth)
+      {
+        code_assignt c(expr, null_pointer_exprt(pointer_type));
+        assignments.move(c);
+
+        return;
+      }
+    }
+
     code_blockt non_null_inst;
 
     exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
@@ -146,7 +174,7 @@ void symbol_factoryt::gen_nondet_init(
     {
       init_expr=dereference_exprt(allocated, allocated.type().subtype());
     }
-    gen_nondet_init(non_null_inst, init_expr);
+    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
 
     if(assume_non_null)
     {
@@ -175,7 +203,25 @@ void symbol_factoryt::gen_nondet_init(
       assignments.move(null_check);
     }
   }
-  // TODO(OJones): Add support for structs and arrays
+  else if(type.id() == ID_struct)
+  {
+    const struct_typet &struct_type = to_struct_type(type);
+
+    const irep_idt struct_tag = struct_type.get_tag();
+
+    recursion_set.insert(struct_tag);
+
+    for(const auto &component : struct_type.components())
+    {
+      const typet &component_type = component.type();
+      const irep_idt name = component.get_name();
+
+      member_exprt me(expr, name, component_type);
+      me.add_source_location() = loc;
+
+      gen_nondet_init(assignments, me, depth, recursion_set);
+    }
+  }
   else
   {
     // If type is a ID_c_bool then add the following code to assignments:
@@ -207,7 +253,6 @@ exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &loc,
-  bool allow_null,
   const c_object_factory_parameterst &object_factory_parameters)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
@@ -230,6 +275,8 @@ exprt c_nondet_symbol_factory(
   std::vector<const symbolt *> symbols_created;
   symbols_created.push_back(main_symbol_ptr);
 
+  const bool allow_null = (object_factory_parameters.min_null_tree_depth == 0);
+
   symbol_factoryt state(
     symbols_created, symbol_table, loc, !allow_null, object_factory_parameters);
   code_blockt assignments;

src/ansi-c/c_nondet_symbol_factory.h

@@ -23,7 +23,6 @@ exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &,
-  bool allow_null,
   const c_object_factory_parameterst &object_factory_parameters);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H