Removed extra code and just combined into gen_nondet_pointer_init

Since the code had to go in the same file and meant in multiple places
would have to construct a different class, I concluded that this half
way refactoring was a step back. I think it is more confusing to follow
without really being any easier to merge.

The changes between the class and the master branch version introduced
by this change are highly isolated (a since if statement inside one
function).

Author: thk123

src/java_bytecode/java_object_factory.cpp

@@ -49,7 +49,6 @@ static symbolt &new_tmp_symbol(
 
 class java_object_factoryt
 {
-protected:
   std::vector<const symbolt *> &symbols_created;
   const source_locationt &loc;
   std::unordered_set<irep_idt, irep_id_hash> recursion_set;
@@ -66,14 +65,13 @@ class java_object_factoryt
   code_assignt get_null_assignment(
     const exprt &expr,
     const pointer_typet &ptr_type);
-protected:
-  virtual void gen_pointer_target_init(
+
+  void gen_pointer_target_init(
     code_blockt &assignments,
     const exprt &expr,
     const typet &target_type,
     bool create_dynamic_objects,
     update_in_placet update_in_place);
-protected:
 
   void allocate_nondet_length_array(
     code_blockt &assignments,
@@ -96,8 +94,6 @@ class java_object_factoryt
       ns(_symbol_table)
   {}
 
-  virtual ~java_object_factoryt()=default;
-
   exprt allocate_object(
     code_blockt &assignments,
     const exprt &,
@@ -109,7 +105,7 @@ class java_object_factoryt
     const exprt &expr,
     update_in_placet);
 
-  virtual void gen_nondet_init(
+  void gen_nondet_init(
     code_blockt &assignments,
     const exprt &expr,
     bool is_sub,
@@ -138,36 +134,11 @@ class java_object_factoryt
     bool create_dynamic_objects,
     const struct_typet &struct_type,
     const update_in_placet &update_in_place);
-};
-
 
-class java_object_factory_with_randomt:java_object_factoryt
-{
-public:
-  java_object_factory_with_randomt(
-    std::vector<const symbolt *> &_symbols_created,
-    const source_locationt &loc,
-    bool _assume_non_null,
-    size_t _max_nondet_array_length,
-    symbol_tablet &_symbol_table):
-      java_object_factoryt(
-        _symbols_created,
-        loc,
-        _assume_non_null,
-        _max_nondet_array_length,
-        _symbol_table)
-  {}
-
-  void gen_nondet_init(
+  symbol_exprt gen_nondet_subtype_pointer_init(
     code_blockt &assignments,
-    const exprt &expr,
-    bool is_sub,
-    irep_idt class_identifier,
-    bool skip_classid,
     bool create_dynamic_objects,
-    bool override,
-    const typet &override_type,
-    update_in_placet update_in_place) override;
+    const pointer_typet &substitute_pointer_type);
 };
 
 /// Generates code for allocating a dynamic object. This is used in
@@ -427,6 +398,27 @@ void java_object_factoryt::gen_nondet_pointer_init(
   const pointer_typet &pointer_type,
   const update_in_placet &update_in_place)
 {
+  select_pointer_typet pointer_type_selector(ns);
+  const pointer_typet &replacement_pointer_type=
+    pointer_type_selector(pointer_type);
+
+  // If we are changing the pointer, we generate code for creating a pointer
+  // to the substituted type instead
+  if(replacement_pointer_type!=pointer_type)
+  {
+    const symbol_exprt real_pointer_symbol=gen_nondet_subtype_pointer_init(
+      assignments,
+      create_dynamic_objects,
+      replacement_pointer_type);
+
+    // Having created a pointer to object of type replacement_pointer_type
+    // we now assign it back to the original pointer with a cast
+    // from pointer_type to replacement_pointer_type
+    assignments.add(
+      code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
+    return;
+  }
+
   const typet &subtype=ns.follow(pointer_type.subtype());
   if(subtype.id()==ID_struct)
   {
@@ -532,6 +524,41 @@ void java_object_factoryt::gen_nondet_pointer_init(
   }
 }
 
+/// Generate GOTO code to initalize the selected concrete type
+/// A { ... } tmp_object;
+/// A.x = NONDET ...
+/// // non-det init of all the fields of A
+/// A * p = &tmp_object
+/// expr = (I *)p
+/// \param assignments: the code to append to
+/// \param create_dynamic_objects: if true, use malloc to allocate objects;
+///   otherwise generate fresh static symbols.
+/// \param replacement_pointer: The type of the pointer we actually want to
+///   to create.
+/// \return The symbol expression that corresponds to the pointer to object
+///   created of the required type.
+symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
+  code_blockt &assignments,
+  bool create_dynamic_objects,
+  const pointer_typet &replacement_pointer)
+{
+  symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer);
+
+  // Generate a new object into this new symbol
+  gen_nondet_init(
+    assignments,
+    new_symbol.symbol_expr(),
+    false,
+    "",
+    false,
+    create_dynamic_objects,
+    false,
+    typet(),
+    update_in_placet::NO_UPDATE_IN_PLACE);
+
+  return new_symbol.symbol_expr();
+}
+
 /// Initialises an object tree rooted at `expr`, allocating child objects as
 /// necessary and nondet-initialising their members, or if MUST_UPDATE_IN_PLACE
 /// is set, re-initialising already-allocated objects.
@@ -907,7 +934,7 @@ exprt object_factory(
 
   std::vector<const symbolt *> symbols_created;
   symbols_created.push_back(main_symbol_ptr);
-  java_object_factory_with_randomt state(
+  java_object_factoryt state(
     symbols_created,
     loc,
     !allow_null,
@@ -970,7 +997,7 @@ void gen_nondet_init(
 {
   std::vector<const symbolt *> symbols_created;
 
-  java_object_factory_with_randomt state(
+  java_object_factoryt state(
     symbols_created,
     loc,
     assume_non_null,
@@ -999,69 +1026,3 @@ void gen_nondet_init(
 
   init_code.append(assignments);
 }
-
-
-void java_object_factory_with_randomt::gen_nondet_init(
-  code_blockt &assignments,
-  const exprt &expr,
-  bool is_sub,
-  irep_idt class_identifier,
-  bool skip_classid,
-  bool create_dynamic_objects,
-  bool override,
-  const typet &override_type,
-  update_in_placet update_in_place)
-{
-  const typet &type=
-    override ? ns.follow(override_type) : ns.follow(expr.type());
-  typet real_type=type;
-
-  if(type.id()==ID_pointer && type.subtype().id()==ID_symbol)
-  {
-    const pointer_typet &pointer_type=to_pointer_type(type);
-    const namespacet ns(symbol_table);
-
-    select_pointer_typet pointer_type_selector(ns);
-    const pointer_typet &replacement_pointer=
-      pointer_type_selector(pointer_type);
-
-    if(replacement_pointer!=real_type)
-    {
-      // Generate GOTO code to initalize the selected concrete type
-      // A { ... } tmp_object;
-      // A.x = NONDET ...
-      // // non-det init of all the fields of A
-      // A * p = &tmp_object
-      // expr = (I *)p
-
-      symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer);
-
-      // Generate a new object into this new symbol
-      gen_nondet_init(
-        assignments,
-        new_symbol.symbol_expr(),
-        is_sub,
-        class_identifier,
-        skip_classid,
-        create_dynamic_objects,
-        override,
-        override_type,
-        update_in_placet::NO_UPDATE_IN_PLACE);
-
-      assignments.add(
-        code_assignt(expr, typecast_exprt(new_symbol.symbol_expr(), type)));
-
-      return;
-    }
-  }
-  java_object_factoryt::gen_nondet_init(
-    assignments,
-    expr,
-    is_sub,
-    class_identifier,
-    skip_classid,
-    create_dynamic_objects,
-    override,
-    override_type,
-    update_in_place);
-}