ci_lazy_methods_needed.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Context-insensitive lazy methods container
 
Author: Chris Smowton, chris.smowton@diffblue.com
 
\*******************************************************************/
 
 
#include "ci_lazy_methods_needed.h"
 
#include <goto-programs/resolve_inherited_component.h>
 
#include <util/namespace.h>
#include <util/std_types.h>
#include <util/symbol_table.h>
 
#include "generic_parameter_specialization_map.h"
#include "java_static_initializers.h"
#include "java_types.h"
#include "select_pointer_type.h"
 
void ci_lazy_methods_neededt::add_needed_method(
  const irep_idt &method_symbol_name)
{
  callable_methods.insert(method_symbol_name);
}
 
void ci_lazy_methods_neededt::add_clinit_call(const irep_idt &class_id)
{
  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
  if(symbol_table.symbols.count(clinit_wrapper))
    add_needed_method(clinit_wrapper);
}
 
void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
  const irep_idt &class_id)
{
  resolve_inherited_componentt resolve_inherited_component{symbol_table};
  optionalt<resolve_inherited_componentt::inherited_componentt>
    cprover_nondet_initialize = resolve_inherited_component(
      class_id, "cproverNondetInitialize:()V", true);
 
  if(cprover_nondet_initialize)
  {
    add_needed_method(
      cprover_nondet_initialize->get_full_component_identifier());
  }
}
 
bool ci_lazy_methods_neededt::add_needed_class(
  const irep_idt &class_symbol_name)
{
  if(!instantiated_classes.insert(class_symbol_name).second)
    return false;
 
  add_cprover_nondet_initialize_if_it_exists(class_symbol_name);
 
  // Special case for enums. We may want to generalise this, the comment in
  // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).
  namespacet ns(symbol_table);
  const auto &class_type =
    to_java_class_type(ns.lookup(class_symbol_name).type);
  if(class_type.get_base("java::java.lang.Enum"))
    add_clinit_call(class_symbol_name);
 
  return true;
}
 
void ci_lazy_methods_neededt::add_all_needed_classes(
  const pointer_typet &pointer_type)
{
  namespacet ns{symbol_table};
 
  initialize_instantiated_classes_from_pointer(pointer_type, ns);
 
  // TODO we should be passing here a map that maps generic parameters
  // to concrete types in the current context TG-2664
  const pointer_typet &subbed_pointer_type =
    pointer_type_selector.convert_pointer_type(pointer_type, {}, ns);
 
  if(subbed_pointer_type != pointer_type)
  {
    initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns);
  }
}
 
void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(
  const pointer_typet &pointer_type,
  const namespacet &ns)
{
  const auto &class_type = to_struct_tag_type(pointer_type.base_type());
  const auto &param_classid = class_type.get_identifier();
 
  // Note here: different arrays may have different element types, so we should
  // explore again even if we've seen this classid before in the array case.
  if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
  {
    gather_field_types(pointer_type.base_type(), ns);
  }
 
  if(is_java_generic_type(pointer_type))
  {
    // Assume if this is a generic like X<A, B, C>, then any concrete parameters
    // will at some point be instantiated.
    const auto &generic_args =
      to_java_generic_type(pointer_type).generic_type_arguments();
    for(const auto &generic_arg : generic_args)
    {
      if(!is_java_generic_parameter(generic_arg))
        add_all_needed_classes(generic_arg);
    }
  }
}
 
void ci_lazy_methods_neededt::gather_field_types(
  const typet &class_type,
  const namespacet &ns)
{
  const auto &underlying_type = to_struct_type(ns.follow(class_type));
  if(is_java_array_tag(underlying_type.get_tag()))
  {
    // If class_type is not a symbol this may be a reference array,
    // but we can't tell what type.
    if(class_type.id() == ID_struct_tag)
    {
      const typet &element_type =
        java_array_element_type(to_struct_tag_type(class_type));
      if(
        element_type.id() == ID_pointer &&
        to_pointer_type(element_type).base_type().id() != ID_empty)
      {
        // This is a reference array -- mark its element type available.
        add_all_needed_classes(to_pointer_type(element_type));
      }
    }
  }
  else
  {
    for(const auto &field : underlying_type.components())
    {
      if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag)
        gather_field_types(field.type(), ns);
      else if(field.type().id() == ID_pointer)
      {
        if(to_pointer_type(field.type()).base_type().id() == ID_struct_tag)
        {
          add_all_needed_classes(to_pointer_type(field.type()));
        }
        else
        {
          // If raw structs were possible this would lead to missed
          // dependencies, as both array element and specialised generic type
          // information cannot be obtained in this case.
          // We should therefore only be skipping pointers such as the uint16t*
          // in our internal String representation.
          INVARIANT(
            to_pointer_type(field.type()).base_type().id() != ID_struct,
            "struct types should be referred to by symbol at this stage");
        }
      }
    }
  }
}