allocate_objects.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "allocate_objects.h"
 
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/symbol.h>
 
#include <goto-programs/goto_instruction_code.h>
 
exprt allocate_objectst::allocate_object(
  code_blockt &assignments,
  const exprt &target_expr,
  const typet &allocate_type,
  const lifetimet lifetime,
  const irep_idt &basename_prefix)
{
  switch(lifetime)
  {
  case lifetimet::AUTOMATIC_LOCAL:
    return allocate_automatic_local_object(
      assignments, target_expr, allocate_type, basename_prefix);
    break;
 
  case lifetimet::STATIC_GLOBAL:
    return allocate_static_global_object(
      assignments, target_expr, allocate_type, basename_prefix);
    break;
 
  case lifetimet::DYNAMIC:
    return allocate_dynamic_object(assignments, target_expr, allocate_type);
    break;
  }
 
  UNREACHABLE;
}
 
exprt allocate_objectst::allocate_automatic_local_object(
  code_blockt &assignments,
  const exprt &target_expr,
  const typet &allocate_type,
  const irep_idt &basename_prefix)
{
  return allocate_non_dynamic_object(
    assignments, target_expr, allocate_type, false, basename_prefix);
}
 
exprt allocate_objectst::allocate_static_global_object(
  code_blockt &assignments,
  const exprt &target_expr,
  const typet &allocate_type,
  const irep_idt &basename_prefix)
{
  return allocate_non_dynamic_object(
    assignments, target_expr, allocate_type, true, basename_prefix);
}
 
symbol_exprt allocate_objectst::allocate_automatic_local_object(
  const typet &allocate_type,
  const irep_idt &basename_prefix)
{
  symbolt &aux_symbol = get_fresh_aux_symbol(
    allocate_type,
    id2string(name_prefix),
    id2string(basename_prefix),
    source_location,
    symbol_mode,
    symbol_table);
 
  add_created_symbol(aux_symbol);
 
  return aux_symbol.symbol_expr();
}
 
exprt allocate_objectst::allocate_dynamic_object_symbol(
  code_blockt &output_code,
  const exprt &target_expr,
  const typet &allocate_type)
{
  if(allocate_type.id() == ID_empty)
  {
    // make null
    code_frontend_assignt code{
      target_expr,
      null_pointer_exprt{to_pointer_type(target_expr.type())},
      source_location};
    output_code.add(std::move(code));
 
    return exprt();
  }
 
  // build size expression
  auto object_size = size_of_expr(allocate_type, ns);
  INVARIANT(object_size.has_value(), "Size of objects should be known");
 
  // 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(name_prefix),
    "malloc_site",
    source_location,
    symbol_mode,
    symbol_table);
 
  add_created_symbol(malloc_sym);
 
  code_frontend_assignt assign =
    make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
  output_code.add(assign);
 
  exprt malloc_symbol_expr = typecast_exprt::conditional_cast(
    malloc_sym.symbol_expr(), target_expr.type());
 
  code_frontend_assignt code(target_expr, malloc_symbol_expr);
  code.add_source_location() = source_location;
  output_code.add(code);
 
  return malloc_sym.symbol_expr();
}
 
exprt allocate_objectst::allocate_dynamic_object(
  code_blockt &output_code,
  const exprt &target_expr,
  const typet &allocate_type)
{
  return dereference_exprt(
    allocate_dynamic_object_symbol(output_code, target_expr, allocate_type));
}
 
exprt allocate_objectst::allocate_non_dynamic_object(
  code_blockt &assignments,
  const exprt &target_expr,
  const typet &allocate_type,
  const bool static_lifetime,
  const irep_idt &basename_prefix)
{
  symbolt &aux_symbol = get_fresh_aux_symbol(
    allocate_type,
    id2string(name_prefix),
    id2string(basename_prefix),
    source_location,
    symbol_mode,
    symbol_table);
 
  aux_symbol.is_static_lifetime = static_lifetime;
  add_created_symbol(aux_symbol);
 
  exprt aoe = typecast_exprt::conditional_cast(
    address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
 
  code_frontend_assignt code(target_expr, aoe);
  code.add_source_location() = source_location;
  assignments.add(code);
 
  if(aoe.id() == ID_typecast)
  {
    return dereference_exprt(aoe);
  }
  else
  {
    return aux_symbol.symbol_expr();
  }
}
 
void allocate_objectst::add_created_symbol(const symbolt &symbol)
{
  symbols_created.push_back(symbol.name);
}
 
void allocate_objectst::declare_created_symbols(code_blockt &init_code)
{
  // Add the following code to init_code for each symbol that's been created:
  //   <type> <identifier>;
  for(const auto &symbol_id : symbols_created)
  {
    const symbolt &symbol = ns.lookup(symbol_id);
    if(!symbol.is_static_lifetime)
    {
      code_frontend_declt decl{symbol.symbol_expr()};
      decl.add_source_location() = source_location;
      init_code.add(decl);
    }
  }
}
 
void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
{
  // Add the following code to init_code for each symbol that's been created:
  //   INPUT("<identifier>", <identifier>);
  for(const auto &symbol_id : symbols_created)
  {
    const symbolt &symbol = ns.lookup(symbol_id);
    init_code.add(
      code_inputt{symbol.base_name, symbol.symbol_expr(), source_location});
  }
}
 
code_frontend_assignt
make_allocate_code(const symbol_exprt &lhs, const exprt &size)
{
  side_effect_exprt alloc{
    ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
  return code_frontend_assignt(lhs, alloc);
}