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>
@@ -27,21 +29,20 @@ class symbol_factoryt
   std::vector<const symbolt *> &symbols_created;
   symbol_tablet &symbol_table;
   const source_locationt &loc;
-  const bool assume_non_null;
   namespacet ns;
   const c_object_factory_parameterst &object_factory_params;
 
+  typedef std::set<irep_idt> recursion_sett;
+
 public:
   symbol_factoryt(
     std::vector<const symbolt *> &_symbols_created,
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
-    const bool _assume_non_null,
     const c_object_factory_parameterst &object_factory_params)
     : symbols_created(_symbols_created),
       symbol_table(_symbol_table),
       loc(loc),
-      assume_non_null(_assume_non_null),
       ns(_symbol_table),
       object_factory_params(object_factory_params)
   {}
@@ -52,7 +53,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 symbol for a pointer to point to
@@ -103,9 +108,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());
 
@@ -115,6 +124,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);
@@ -128,9 +153,9 @@ 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)
+    if(depth < object_factory_params.min_null_tree_depth)
     {
       // Add the following code to assignments:
       // <expr> = <aoe>;
@@ -157,7 +182,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:
@@ -181,15 +224,13 @@ void symbol_factoryt::gen_nondet_init(
 /// \param base_name: The name to use for the symbol created
 /// \param type: The type for the symbol created
 /// \param loc: The location to assign to generated code
-/// \param allow_null: Whether to allow a null value when type is a pointer
 /// \return Returns the symbol_exprt for the symbol created
 exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   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())+
@@ -213,7 +254,7 @@ exprt c_nondet_symbol_factory(
   symbols_created.push_back(main_symbol_ptr);
 
   symbol_factoryt state(
-    symbols_created, symbol_table, loc, !allow_null, object_factory_parameters);
+    symbols_created, symbol_table, loc, object_factory_parameters);
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 

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