Use allocate_objectst in the java object factory

Author: danpoe

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -94,12 +94,6 @@ class java_object_factoryt
       pointer_type_selector(pointer_type_selector)
   {}
 
-  exprt allocate_object(
-    code_blockt &assignments,
-    const exprt &,
-    const typet &,
-    allocation_typet alloc_type);
-
   void gen_nondet_array_init(
     code_blockt &assignments,
     const exprt &expr,
@@ -168,182 +162,6 @@ class java_object_factoryt
     const irep_idt &method_name);
 };
 
-/// Generates code for allocating a dynamic object. This is used in
-/// allocate_object() and also in the library preprocessing for allocating
-/// strings.
-/// \param target_expr: expression to which the necessary memory will be
-///   allocated, its type should be pointer to `allocate_type`
-/// \param allocate_type: type of the object allocated
-/// \param symbol_table: symbol table
-/// \param loc: location in the source
-/// \param function_id: function ID to associate with auxiliary variables
-/// \param output_code: code block to which the necessary code is added
-/// \param symbols_created: created symbols to be declared by the caller
-/// \param cast_needed: Boolean flags saying where we need to cast the malloc
-///   site
-/// \return Expression representing the malloc site allocated.
-exprt allocate_dynamic_object(
-  const exprt &target_expr,
-  const typet &allocate_type,
-  symbol_table_baset &symbol_table,
-  const source_locationt &loc,
-  const irep_idt &function_id,
-  code_blockt &output_code,
-  std::vector<const symbolt *> &symbols_created,
-  bool cast_needed)
-{
-  // build size expression
-  exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table));
-
-  if(allocate_type.id()!=ID_empty)
-  {
-    INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
-    // malloc expression
-    side_effect_exprt malloc_expr(
-      ID_allocate, pointer_type(allocate_type), loc);
-    malloc_expr.copy_to_operands(object_size);
-    malloc_expr.copy_to_operands(false_exprt());
-    // create a symbol for the malloc expression so we can initialize
-    // without having to do it potentially through a double-deref, which
-    // breaks the to-SSA phase.
-    symbolt &malloc_sym = get_fresh_aux_symbol(
-      pointer_type(allocate_type),
-      id2string(function_id),
-      "malloc_site",
-      loc,
-      ID_java,
-      symbol_table);
-    symbols_created.push_back(&malloc_sym);
-    code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
-    assign.add_source_location()=loc;
-    output_code.add(assign);
-    exprt malloc_symbol_expr=malloc_sym.symbol_expr();
-    if(cast_needed)
-      malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type());
-    code_assignt code(target_expr, malloc_symbol_expr);
-    code.add_source_location()=loc;
-    output_code.add(code);
-    return malloc_sym.symbol_expr();
-  }
-  else
-  {
-    // make null
-    null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type()));
-    code_assignt code(target_expr, null_pointer_expr);
-    code.add_source_location()=loc;
-    output_code.add(code);
-    return exprt();
-  }
-}
-
-/// Generates code for allocating a dynamic object. This is a static version of
-/// allocate_dynamic_object that can be called from outside java_object_factory
-/// and which takes care of creating the associated declarations.
-/// \param target_expr: expression to which the necessary memory will be
-///   allocated
-/// \param symbol_table: symbol table
-/// \param loc: location in the source
-/// \param function_id: function ID to associate with auxiliary variables
-/// \param output_code: code block to which the necessary code is added
-/// \return the dynamic object created
-exprt allocate_dynamic_object_with_decl(
-  const exprt &target_expr,
-  symbol_table_baset &symbol_table,
-  const source_locationt &loc,
-  const irep_idt &function_id,
-  code_blockt &output_code)
-{
-  std::vector<const symbolt *> symbols_created;
-  code_blockt tmp_block;
-  const typet &allocate_type=target_expr.type().subtype();
-  const exprt dynamic_object = allocate_dynamic_object(
-    target_expr,
-    allocate_type,
-    symbol_table,
-    loc,
-    function_id,
-    tmp_block,
-    symbols_created,
-    false);
-
-  // Add the following code to output_code for each symbol that's been created:
-  //   <type> <identifier>;
-  for(const symbolt * const symbol_ptr : symbols_created)
-  {
-    code_declt decl(symbol_ptr->symbol_expr());
-    decl.add_source_location()=loc;
-    output_code.add(decl);
-  }
-
-  for(const auto &code : tmp_block.statements())
-    output_code.add(code);
-
-  return dynamic_object;
-}
-
-/// Installs a new symbol in the symbol table, pushing the corresponding symbolt
-/// object to the field `symbols_created` and emits to \p assignments a new
-/// assignment of the form `<target_expr> := address-of(new_object)`.  The
-/// \p allocate_type may differ from `target_expr.type()`, e.g. for target_expr
-/// having type int* and allocate_type being an int[10].
-///
-/// \param assignments: The code block to add code to.
-/// \param target_expr: The expression which we are allocating a symbol for.
-/// \param allocate_type:
-/// \param alloc_type: Allocation type (global, local or dynamic)
-/// \return An address_of_exprt of the newly allocated object.
-exprt java_object_factoryt::allocate_object(
-  code_blockt &assignments,
-  const exprt &target_expr,
-  const typet &allocate_type,
-  allocation_typet alloc_type)
-{
-  const typet &allocate_type_resolved=ns.follow(allocate_type);
-  const typet &target_type=ns.follow(target_expr.type().subtype());
-  bool cast_needed=allocate_type_resolved!=target_type;
-  switch(alloc_type)
-  {
-    case allocation_typet::LOCAL:
-    case allocation_typet::GLOBAL:
-    {
-      symbolt &aux_symbol = get_fresh_aux_symbol(
-        allocate_type,
-        id2string(object_factory_parameters.function_id),
-        "tmp_object_factory",
-        loc,
-        ID_java,
-        symbol_table);
-      if(alloc_type==allocation_typet::GLOBAL)
-        aux_symbol.is_static_lifetime=true;
-      symbols_created.push_back(&aux_symbol);
-
-      exprt object=aux_symbol.symbol_expr();
-      exprt aoe=address_of_exprt(object);
-      if(cast_needed)
-        aoe=typecast_exprt(aoe, target_expr.type());
-      code_assignt code(target_expr, aoe);
-      code.add_source_location()=loc;
-      assignments.add(code);
-      return aoe;
-    }
-    case allocation_typet::DYNAMIC:
-    {
-      return allocate_dynamic_object(
-        target_expr,
-        allocate_type,
-        symbol_table,
-        loc,
-        object_factory_parameters.function_id,
-        assignments,
-        symbols_created,
-        cast_needed);
-    }
-    default:
-      UNREACHABLE;
-      return exprt();
-  } // End switch
-}
-
 /// Returns a codet that assigns \p expr, of type \p ptr_type, a NULL value.
 code_assignt java_object_factoryt::get_null_assignment(
   const exprt &expr,
@@ -433,7 +251,12 @@ void java_object_factoryt::gen_pointer_target_init(
   exprt target;
   if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
   {
-    target = allocate_object(assignments, expr, target_type, alloc_type);
+    allocate_objectst allocate_objects(
+      ID_java, loc, object_factory_parameters.function_id, symbol_table);
+
+    target = allocate_objects.allocate_object(
+      assignments, expr, target_type, alloc_type, symbols_created);
+
     INVARIANT(
       target.type().id() == ID_pointer, "Pointer-typed expression expected");
   }

jbmc/src/java_bytecode/java_object_factory.h

@@ -74,21 +74,11 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_language.h"
 #include "select_pointer_type.h"
 
+#include <util/allocate_objects.h>
 #include <util/message.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
-/// Selects the kind of allocation used by the object factories
-enum class allocation_typet
-{
-  /// Allocate global objects
-  GLOBAL,
-  /// Allocate local stacked objects
-  LOCAL,
-  /// Allocate dynamic objects (using MALLOC)
-  DYNAMIC
-};
-
 exprt object_factory(
   const typet &type,
   const irep_idt base_name,
@@ -136,21 +126,4 @@ void gen_nondet_init(
   const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 
-exprt allocate_dynamic_object(
-  const exprt &target_expr,
-  const typet &allocate_type,
-  symbol_table_baset &symbol_table,
-  const source_locationt &loc,
-  const irep_idt &function_id,
-  code_blockt &output_code,
-  std::vector<const symbolt *> &symbols_created,
-  bool cast_needed = false);
-
-exprt allocate_dynamic_object_with_decl(
-  const exprt &target_expr,
-  symbol_table_baset &symbol_table,
-  const source_locationt &loc,
-  const irep_idt &function_id,
-  code_blockt &output_code);
-
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H