Adapt c nondet symbol factory for use in function body generation

Author: danpoe

src/ansi-c/ansi_c_entry_point.cpp

@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
       base_name,
       p.type(),
       p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      allocation_typet::LOCAL);
   }
 
   return main_arguments;

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -25,51 +25,29 @@ Author: Diffblue Ltd.
 
 #include <goto-programs/goto_functions.h>
 
-class symbol_factoryt
-{
-  std::vector<const symbolt *> &symbols_created;
-  symbol_tablet &symbol_table;
-  const source_locationt &loc;
-  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 c_object_factory_parameterst &object_factory_params)
-    : symbols_created(_symbols_created),
-      symbol_table(_symbol_table),
-      loc(loc),
-      ns(_symbol_table),
-      object_factory_params(object_factory_params)
-  {}
-
-  void gen_nondet_init(
-    code_blockt &assignments,
-    const exprt &expr,
-    const std::size_t depth = 0,
-    recursion_sett recursion_set = recursion_sett());
-};
-
 /// Creates a nondet for expr, including calling itself recursively to make
 /// appropriate symbols to point to if expr is a pointer.
 /// \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
+/// \param assign_const Indicates whether const objects should be nondet
+///   initialized
 void symbol_factoryt::gen_nondet_init(
   code_blockt &assignments,
   const exprt &expr,
   const std::size_t depth,
-  recursion_sett recursion_set)
+  recursion_sett recursion_set,
+  const bool assign_const)
 {
   const typet &type=ns.follow(expr.type());
 
+  if(!assign_const && expr.type().get_bool(ID_C_constant))
+  {
+    return;
+  }
+
   if(type.id()==ID_pointer)
   {
     // dereferenced type
@@ -97,8 +75,8 @@ void symbol_factoryt::gen_nondet_init(
     allocate_objectst allocate_objects(
       ID_C, loc, loc.get_function(), symbol_table);
 
-    exprt allocated = allocate_objects.allocate_non_dynamic_object(
-      non_null_inst, expr, subtype, false, symbols_created);
+    exprt allocated = allocate_objects.allocate_object(
+      non_null_inst, expr, subtype, allocation_type, symbols_created);
 
     exprt init_expr;
     if(allocated.id()==ID_address_of)
@@ -109,7 +87,7 @@ void symbol_factoryt::gen_nondet_init(
     {
       init_expr=dereference_exprt(allocated, allocated.type().subtype());
     }
-    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
+    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
 
     if(depth < object_factory_params.min_null_tree_depth)
     {
@@ -149,12 +127,18 @@ void symbol_factoryt::gen_nondet_init(
     for(const auto &component : struct_type.components())
     {
       const typet &component_type = component.type();
+
+      if(!assign_const && component_type.get_bool(ID_C_constant))
+      {
+        continue;
+      }
+
       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);
+      gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
     }
   }
   else
@@ -182,14 +166,17 @@ void symbol_factoryt::gen_nondet_init(
 /// \param loc: The location to assign to generated code
 /// \param object_factory_parameters configuration parameters for the object
 ///   factory
+/// \param allocation_type Indicates whether the new objects should be allocated
+///   locally, globally, or dynamically
 /// \return Returns the symbol_exprt for the symbol created
 symbol_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,
-  const c_object_factory_parameterst &object_factory_parameters)
+  const c_object_factory_parameterst &object_factory_parameters,
+  const allocation_typet allocation_type)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -212,7 +199,12 @@ symbol_exprt c_nondet_symbol_factory(
   symbols_created.push_back(main_symbol_ptr);
 
   symbol_factoryt state(
-    symbols_created, symbol_table, loc, object_factory_parameters);
+    symbols_created,
+    symbol_table,
+    loc,
+    object_factory_parameters,
+    allocation_type);
+
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 

src/ansi-c/c_nondet_symbol_factory.h

@@ -14,15 +14,55 @@ Author: Diffblue Ltd.
 
 #include "c_object_factory_parameters.h"
 
+#include <set>
+#include <vector>
+
+#include <util/allocate_objects.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+class symbol_factoryt
+{
+  std::vector<const symbolt *> &symbols_created;
+  symbol_tablet &symbol_table;
+  const source_locationt &loc;
+  namespacet ns;
+  const c_object_factory_parameterst &object_factory_params;
+  const allocation_typet allocation_type;
+
+public:
+  typedef std::set<irep_idt> recursion_sett;
+
+  symbol_factoryt(
+    std::vector<const symbolt *> &symbols_created,
+    symbol_tablet &symbol_table,
+    const source_locationt &loc,
+    const c_object_factory_parameterst &object_factory_params,
+    const allocation_typet allocation_type)
+    : symbols_created(symbols_created),
+      symbol_table(symbol_table),
+      loc(loc),
+      ns(symbol_table),
+      object_factory_params(object_factory_params),
+      allocation_type(allocation_type)
+  {
+  }
+
+  void gen_nondet_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const std::size_t depth = 0,
+    recursion_sett recursion_set = recursion_sett(),
+    const bool assign_const = true);
+};
+
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const irep_idt base_name,
   const typet &type,
   const source_locationt &,
-  const c_object_factory_parameterst &object_factory_parameters);
+  const c_object_factory_parameterst &object_factory_parameters,
+  const allocation_typet allocation_type);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H