java_types.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "java_types.h"
 
#include <util/c_types.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/std_expr.h>
 
#include "java_utils.h"
 
#include <cctype>
#include <iterator>
 
#ifdef DEBUG
#include <iostream>
#endif
 
std::vector<typet> parse_list_types(
  const std::string src,
  const std::string class_name_prefix,
  const char opening_bracket,
  const char closing_bracket);
 
signedbv_typet java_int_type()
{
  static const auto result = signedbv_typet(32);
  return result;
}
 
empty_typet java_void_type()
{
  static const auto result = empty_typet();
  return result;
}
 
signedbv_typet java_long_type()
{
  static const auto result = signedbv_typet(64);
  return result;
}
 
signedbv_typet java_short_type()
{
  static const auto result = signedbv_typet(16);
  return result;
}
 
signedbv_typet java_byte_type()
{
  static const auto result = signedbv_typet(8);
  return result;
}
 
unsignedbv_typet java_char_type()
{
  static const auto result = unsignedbv_typet(16);
  return result;
}
 
floatbv_typet java_float_type()
{
  static const auto result = ieee_float_spect::single_precision().to_type();
  return result;
}
 
floatbv_typet java_double_type()
{
  static const auto result = ieee_float_spect::double_precision().to_type();
  return result;
}
 
c_bool_typet java_boolean_type()
{
  // The Java standard doesn't really prescribe the width
  // of a boolean. However, JNI suggests that it's 8 bits.
  // http://docs.oracle.com/javase/7/docs/technotes/guides/jni/spec/types.html
  static const auto result = c_bool_typet(8);
  return result;
}
 
reference_typet java_reference_type(const typet &subtype)
{
  return reference_type(subtype);
}
 
java_reference_typet java_reference_type(const struct_tag_typet &subtype)
{
  return to_java_reference_type(reference_type(subtype));
}
 
java_reference_typet java_lang_object_type()
{
  static const auto result =
    java_reference_type(struct_tag_typet("java::java.lang.Object"));
  return result;
}
 
java_reference_typet java_array_type(const char subtype)
{
  std::string subtype_str;
 
  switch(subtype)
  {
  case 'b': subtype_str="byte"; break;
  case 'f': subtype_str="float"; break;
  case 'd': subtype_str="double"; break;
  case 'i': subtype_str="int"; break;
  case 'c': subtype_str="char"; break;
  case 's': subtype_str="short"; break;
  case 'z': subtype_str="boolean"; break;
  case 'v': subtype_str="void"; break;
  case 'j': subtype_str="long"; break;
  case 'l': subtype_str="long"; break;
  case 'a': subtype_str="reference"; break;
  default:
#ifdef DEBUG
    std::cout << "Unrecognised subtype str: " << subtype << std::endl;
#endif
    UNREACHABLE;
  }
 
  irep_idt class_name="array["+subtype_str+"]";
 
  struct_tag_typet struct_tag_type("java::" + id2string(class_name));
  struct_tag_type.set(ID_C_base_name, class_name);
  struct_tag_type.set(ID_element_type, java_type_from_char(subtype));
 
  return java_reference_type(struct_tag_type);
}
 
const typet &java_array_element_type(const struct_tag_typet &array_symbol)
{
  DATA_INVARIANT(
    is_java_array_tag(array_symbol.get_identifier()),
    "Symbol should have array tag");
  return array_symbol.find_type(ID_element_type);
}
 
typet &java_array_element_type(struct_tag_typet &array_symbol)
{
  DATA_INVARIANT(
    is_java_array_tag(array_symbol.get_identifier()),
    "Symbol should have array tag");
  return array_symbol.add_type(ID_element_type);
}
 
bool is_java_array_type(const typet &type)
{
  if(
    !can_cast_type<pointer_typet>(type) ||
    !can_cast_type<struct_tag_typet>(to_pointer_type(type).base_type()))
  {
    return false;
  }
  const auto &subtype_struct_tag =
    to_struct_tag_type(to_pointer_type(type).base_type());
  return is_java_array_tag(subtype_struct_tag.get_identifier());
}
 
bool is_multidim_java_array_type(const typet &type)
{
  return is_java_array_type(type) &&
         is_java_array_type(java_array_element_type(
           to_struct_tag_type(to_pointer_type(type).base_type())));
}
 
std::pair<typet, std::size_t>
java_array_dimension_and_element_type(const struct_tag_typet &type)
{
  std::size_t array_dimensions = 0;
  typet underlying_type;
  for(underlying_type = java_reference_type(type);
      is_java_array_type(underlying_type);
      underlying_type = java_array_element_type(to_struct_tag_type(
        to_java_reference_type(underlying_type).base_type())))
  {
    ++array_dimensions;
  }
 
  return {underlying_type, array_dimensions};
}
 
exprt get_array_dimension_field(const exprt &pointer)
{
  PRECONDITION(pointer.type().id() == ID_pointer);
 
  struct_tag_typet java_reference_array_type(JAVA_REFERENCE_ARRAY_CLASSID);
  exprt deref = dereference_exprt(typecast_exprt::conditional_cast(
    pointer, java_reference_type(java_reference_array_type)));
  return member_exprt(deref, JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
}
 
exprt get_array_element_type_field(const exprt &pointer)
{
  PRECONDITION(pointer.type().id() == ID_pointer);
 
  struct_tag_typet java_reference_array_type(JAVA_REFERENCE_ARRAY_CLASSID);
  exprt deref = dereference_exprt(typecast_exprt::conditional_cast(
    pointer, java_reference_type(java_reference_array_type)));
  return member_exprt(
    deref, JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
}
 
bool is_java_array_tag(const irep_idt& tag)
{
  return tag.starts_with("java::array[");
}
 
typet java_type_from_char(char t)
{
  switch(t)
  {
  case 'i': return java_int_type();
  case 'j': return java_long_type();
  case 'l': return java_long_type();
  case 's': return java_short_type();
  case 'b': return java_byte_type();
  case 'c': return java_char_type();
  case 'f': return java_float_type();
  case 'd': return java_double_type();
  case 'z': return java_boolean_type();
  case 'a':
    return java_reference_type(java_void_type());
  default:
    UNREACHABLE;
  }
}
 
typet java_bytecode_promotion(const typet &type)
{
  if(type==java_boolean_type() ||
     type==java_char_type() ||
     type==java_byte_type() ||
     type==java_short_type())
    return java_int_type();
 
  return type;
}
 
exprt java_bytecode_promotion(const exprt &expr)
{
  typet new_type=java_bytecode_promotion(expr.type());
 
  if(new_type==expr.type())
    return expr;
  else
    return typecast_exprt(expr, new_type);
}
 
void add_generic_type_information(
  java_generic_typet &generic_type,
  const std::string &type_arguments,
  const std::string &class_name_prefix)
{
  PRECONDITION(type_arguments.size() >= 2);
  PRECONDITION(type_arguments[0] == '<');
  PRECONDITION(type_arguments[type_arguments.size() - 1] == '>');
 
  // Parse contained arguments, can be either type parameters (`TT;`)
  // or instantiated types - either generic types (`LList<LInteger;>;`) or
  // just references (`Ljava/lang/Foo;`)
  std::vector<typet> type_arguments_types =
    parse_list_types(type_arguments, class_name_prefix, '<', '>');
 
  // We should have at least one generic type argument
  CHECK_RETURN(!type_arguments_types.empty());
 
  // Add the type arguments to the generic type
  std::transform(
    type_arguments_types.begin(),
    type_arguments_types.end(),
    std::back_inserter(generic_type.generic_type_arguments()),
    [](const typet &type) -> reference_typet
    {
      INVARIANT(
        is_reference(type), "All generic type arguments should be references");
      return to_reference_type(type);
    });
}
 
std::string erase_type_arguments(const std::string &src)
{
  std::string class_name = src;
  std::size_t f_pos = class_name.find('<', 1);
 
  while(f_pos != std::string::npos)
  {
    std::size_t e_pos = find_closing_delimiter(class_name, f_pos, '<', '>');
    if(e_pos == std::string::npos)
    {
      throw unsupported_java_class_signature_exceptiont(
        "Failed to find generic signature closing delimiter (or recursive "
        "generic): " +
        src);
    }
 
    // erase generic information between brackets
    class_name.erase(f_pos, e_pos - f_pos + 1);
 
    // Search the remainder of the string for generic signature
    f_pos = class_name.find('<', f_pos + 1);
  }
  return class_name;
}
 
std::string gather_full_class_name(const std::string &src)
{
  PRECONDITION(src.size() >= 2);
  PRECONDITION(src[0] == 'L');
  PRECONDITION(src[src.size() - 1] == ';');
 
  std::string class_name = src.substr(1, src.size() - 2);
 
  class_name = erase_type_arguments(class_name);
 
  std::replace(class_name.begin(), class_name.end(), '.', '$');
  std::replace(class_name.begin(), class_name.end(), '/', '.');
  return class_name;
}
 
std::vector<typet> parse_list_types(
  const std::string src,
  const std::string class_name_prefix,
  const char opening_bracket,
  const char closing_bracket)
{
  // Loop over the types in the given string, parsing each one in turn
  // and adding to the type_list
  std::vector<typet> type_list;
  for(const std::string &raw_type :
      parse_raw_list_types(src, opening_bracket, closing_bracket))
  {
    auto new_type = java_type_from_string(raw_type, class_name_prefix);
    INVARIANT(new_type.has_value(), "Failed to parse type");
    type_list.push_back(std::move(*new_type));
  }
  return type_list;
}
 
std::vector<std::string> parse_raw_list_types(
  const std::string src,
  const char opening_bracket,
  const char closing_bracket)
{
  PRECONDITION(src.size() >= 2);
  PRECONDITION(src[0] == opening_bracket);
  PRECONDITION(src[src.size() - 1] == closing_bracket);
 
  // Loop over the types in the given string, parsing each one in turn
  // and adding to the type_list
  std::vector<std::string> type_list;
  for(std::size_t i = 1; i < src.size() - 1; i++)
  {
    size_t start = i;
    while(i < src.size())
    {
      // type is an object type or instantiated generic type
      if(src[i] == 'L')
      {
        i = find_closing_semi_colon_for_reference_type(src, i);
        break;
      }
 
      // type is an array
      else if(src[i] == '[')
        i++;
 
      // type is a type variable/parameter
      else if(src[i] == 'T')
        i = src.find(';', i); // ends on ;
 
      // type is an atomic type (just one character)
      else
      {
        break;
      }
    }
 
    std::string sub_str = src.substr(start, i - start + 1);
    type_list.emplace_back(sub_str);
  }
  return type_list;
}
 
reference_typet
build_class_name(const std::string &src, const std::string &class_name_prefix)
{
  PRECONDITION(src[0] == 'L');
 
  // All reference types must end on a ;
  PRECONDITION(src[src.size() - 1] == ';');
 
  std::string container_class = gather_full_class_name(src);
  std::string identifier = "java::" + container_class;
  struct_tag_typet struct_tag_type(identifier);
  struct_tag_type.set(ID_C_base_name, container_class);
 
  std::size_t f_pos = src.find('<', 1);
  if(f_pos != std::string::npos)
  {
    java_generic_typet result(struct_tag_type);
    // get generic type information
    do
    {
      std::size_t e_pos = find_closing_delimiter(src, f_pos, '<', '>');
      if(e_pos == std::string::npos)
        throw unsupported_java_class_signature_exceptiont(
          "Parsing type with unmatched generic bracket: " + src);
 
      add_generic_type_information(
        result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
 
      // Look for the next generic type info (if it exists)
      f_pos = src.find('<', e_pos + 1);
    } while(f_pos != std::string::npos);
    return std::move(result);
  }
 
  return java_reference_type(struct_tag_type);
}
 
size_t find_closing_semi_colon_for_reference_type(
  const std::string src,
  size_t starting_point)
{
  PRECONDITION(src[starting_point] == 'L');
  size_t next_semi_colon = src.find(';', starting_point);
  INVARIANT(
    next_semi_colon != std::string::npos,
    "There must be a semi-colon somewhere in the input");
  size_t next_angle_bracket = src.find('<', starting_point);
 
  while(next_angle_bracket < next_semi_colon)
  {
    size_t end_bracket =
      find_closing_delimiter(src, next_angle_bracket, '<', '>');
    INVARIANT(
      end_bracket != std::string::npos, "Must find matching angle bracket");
 
    next_semi_colon = src.find(';', end_bracket + 1);
    next_angle_bracket = src.find('<', end_bracket + 1);
  }
 
  return next_semi_colon;
}
 
java_reference_typet java_reference_array_type(const struct_tag_typet &subtype)
{
  java_reference_typet result = java_array_type('a');
  result.base_type().set(ID_element_type, java_reference_type(subtype));
  return result;
}
 
std::optional<typet> java_type_from_string(
  const std::string &src,
  const std::string &class_name_prefix)
{
  if(src.empty())
    return {};
 
  // a java type is encoded in different ways
  //  - a method type is encoded as '(...)R' where the parenthesis include the
  //    parameter types and R is the type of the return value
  //  - atomic types are encoded as single characters
  //  - array types are encoded as '[' followed by the type of the array
  //    content
  //  - object types are named with prefix 'L' and suffix ';', e.g.,
  //    Ljava/lang/Object;
  //  - type variables are similar to object types but have the prefix 'T'
  switch(src[0])
  {
  case '<':
    {
      // The method signature can optionally have a collection of formal
      // type parameters (e.g. on generic methods on non-generic classes
      // or generic static methods). For now we skip over this part of the
      // signature and continue parsing the rest of the signature as normal
      // So for example, the following java method:
      // static void <T, U> foo(T t, U u, int x);
      // Would have a signature that looks like:
      // <T:Ljava/lang/Object;U:Ljava/lang/Object;>(TT;TU;I)V
      // So we skip all inside the angle brackets and parse the rest of the
      // string:
      // (TT;TU;I)V
      size_t closing_generic=find_closing_delimiter(src, 0, '<', '>');
      if(closing_generic==std::string::npos)
      {
        throw unsupported_java_class_signature_exceptiont(
          "Failed to find generic signature closing delimiter");
      }
 
      // If there are any bounds between '<' and '>' then we cannot currently
      // parse them, so we give up. This only happens when parsing the
      // signature, so we'll fall back to the result of parsing the
      // descriptor, which will respect the bounds correctly.
      const size_t colon_pos = src.find(':');
      if(colon_pos != std::string::npos && colon_pos < closing_generic)
      {
        throw unsupported_java_class_signature_exceptiont(
          "Cannot currently parse bounds on generic types");
      }
 
      auto method_type = java_type_from_string(
        src.substr(closing_generic + 1, std::string::npos), class_name_prefix);
 
      // This invariant being violated means that tkiley has not understood
      // part of the signature spec.
      // Only class and method signatures can start with a '<' and classes are
      // handled separately.
      INVARIANT(
        method_type.has_value() && method_type->id() == ID_code,
        "This should correspond to method signatures only");
 
      return method_type;
    }
  case '(': // function type
    {
      std::size_t e_pos=src.rfind(')');
      if(e_pos==std::string::npos)
        return {};
 
      auto return_type = java_type_from_string(
        std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
 
      std::vector<typet> param_types =
        parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
 
      // create parameters for each type
      java_method_typet::parameterst parameters;
      std::transform(
        param_types.begin(),
        param_types.end(),
        std::back_inserter(parameters),
        [](const typet &type) { return java_method_typet::parametert(type); });
 
      return java_method_typet(std::move(parameters), std::move(*return_type));
    }
 
  case '[': // array type
    {
      // If this is a reference array, we generate a plain array[reference]
      // with void* members, but note the real type in ID_element_type.
      if(src.size()<=1)
        return {};
      char subtype_letter=src[1];
      auto subtype = java_type_from_string(
        src.substr(1, std::string::npos), class_name_prefix);
      if(subtype_letter=='L' || // [L denotes a reference array of some sort.
         subtype_letter=='[' || // Array-of-arrays
         subtype_letter=='T')   // Array of generic types
        subtype_letter='A';
      subtype_letter = std::tolower(subtype_letter);
      if(subtype_letter == 'a')
      {
        return java_reference_array_type(
          to_struct_tag_type(to_java_reference_type(*subtype).base_type()));
      }
      else
        return java_array_type(subtype_letter);
    }
 
  case 'B': return java_byte_type();
  case 'F': return java_float_type();
  case 'D': return java_double_type();
  case 'I': return java_int_type();
  case 'C': return java_char_type();
  case 'S': return java_short_type();
  case 'Z': return java_boolean_type();
  case 'V': return java_void_type();
  case 'J': return java_long_type();
  case 'T':
  {
    // parse name of type variable
    INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
    PRECONDITION(!class_name_prefix.empty());
    irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
    return java_generic_parametert(
      type_var_name,
      to_struct_tag_type(
        to_java_reference_type(*java_type_from_string("Ljava/lang/Object;"))
          .base_type()));
  }
  case 'L':
    {
      return build_class_name(src, class_name_prefix);
    }
  case '*':
  case '+':
  case '-':
  {
#ifdef DEBUG
    std::cout << class_name_prefix << std::endl;
#endif
    throw unsupported_java_class_signature_exceptiont("wild card generic");
  }
  default:
    return {};
  }
}
 
char java_char_from_type(const typet &type)
{
  const irep_idt &id=type.id();
 
  if(id==ID_signedbv)
  {
    const size_t width=to_signedbv_type(type).get_width();
    if(java_int_type().get_width() == width)
      return 'i';
    else if(java_long_type().get_width() == width)
      return 'l';
    else if(java_short_type().get_width() == width)
      return 's';
    else if(java_byte_type().get_width() == width)
      return 'b';
  }
  else if(id==ID_unsignedbv)
    return 'c';
  else if(id==ID_floatbv)
  {
    const size_t width(to_floatbv_type(type).get_width());
    if(java_float_type().get_width() == width)
      return 'f';
    else if(java_double_type().get_width() == width)
      return 'd';
  }
  else if(id==ID_c_bool)
    return 'z';
 
  return 'a';
}
 
std::vector<typet> java_generic_type_from_string(
  const std::string &class_name,
  const std::string &src)
{
  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
  INVARIANT(
    src[0]=='<' && signature_end!=std::string::npos,
    "Class signature has unexpected format");
  std::string signature(src.substr(1, signature_end-1));
 
  if(signature.find(";:")!=std::string::npos)
    throw unsupported_java_class_signature_exceptiont("multiple bounds");
 
  PRECONDITION(signature[signature.size()-1]==';');
 
  std::vector<typet> types;
  size_t var_sep=signature.find(';');
  while(var_sep!=std::string::npos)
  {
    size_t bound_sep=signature.find(':');
    INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
 
    // is bound an interface?
    // in this case the separator is '::'
    if(signature[bound_sep + 1] == ':')
    {
      INVARIANT(
        signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
      bound_sep++;
    }
 
    std::string type_var_name(
      "java::"+class_name+"::"+signature.substr(0, bound_sep));
    std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
 
    java_generic_parametert type_var_type(
      type_var_name,
      to_struct_tag_type(
        to_java_reference_type(*java_type_from_string(bound_type, class_name))
          .base_type()));
 
    types.push_back(type_var_type);
    signature=signature.substr(var_sep+1, std::string::npos);
    var_sep=signature.find(';');
  }
  return types;
}
 
// java/lang/Object -> java.lang.Object
static std::string slash_to_dot(const std::string &src)
{
  std::string result=src;
  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
    if(*it=='/')
      *it='.';
  return result;
}
 
struct_tag_typet java_classname(const std::string &id)
{
  if(!id.empty() && id[0]=='[')
    return to_struct_tag_type(
      to_java_reference_type(*java_type_from_string(id)).base_type());
 
  std::string class_name=id;
 
  class_name=slash_to_dot(class_name);
  irep_idt identifier="java::"+class_name;
  struct_tag_typet struct_tag_type(identifier);
  struct_tag_type.set(ID_C_base_name, class_name);
 
  return struct_tag_type;
}
 
bool is_valid_java_array(const struct_typet &type)
{
  bool correct_num_components =
    type.components().size() ==
    (type.get_tag() == JAVA_REFERENCE_ARRAY_CLASSID ? 5 : 3);
  if(!correct_num_components)
    return false;
 
  // First component, the base class (Object) data
  const struct_union_typet::componentt base_class_component=
    type.components()[0];
 
  if(base_class_component.get_name() != "@java.lang.Object")
    return false;
 
  const struct_union_typet::componentt length_component=
    type.components()[1];
  if(length_component.get_name() != "length")
    return false;
  if(length_component.type() != java_int_type())
    return false;
 
  const struct_union_typet::componentt data_component=
    type.components()[2];
  if(data_component.get_name() != "data")
    return false;
  if(data_component.type().id() != ID_pointer)
    return false;
 
  if(type.get_tag() == JAVA_REFERENCE_ARRAY_CLASSID)
  {
    const struct_union_typet::componentt array_element_type_component =
      type.components()[3];
    if(
      array_element_type_component.get_name() !=
      JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME)
      return false;
    if(array_element_type_component.type() != string_typet())
      return false;
 
    const struct_union_typet::componentt array_dimension_component =
      type.components()[4];
    if(array_dimension_component.get_name() != JAVA_ARRAY_DIMENSION_FIELD_NAME)
      return false;
    if(array_dimension_component.type() != java_int_type())
      return false;
  }
 
  return true;
}
 
bool equal_java_types(const typet &type1, const typet &type2)
{
  bool arrays_with_same_element_type = true;
  if(
    type1.id() == ID_pointer && type2.id() == ID_pointer &&
    to_pointer_type(type1).base_type().id() == ID_struct_tag &&
    to_pointer_type(type2).base_type().id() == ID_struct_tag)
  {
    const auto &subtype_symbol1 =
      to_struct_tag_type(to_pointer_type(type1).base_type());
    const auto &subtype_symbol2 =
      to_struct_tag_type(to_pointer_type(type2).base_type());
    if(
      subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
      is_java_array_tag(subtype_symbol1.get_identifier()))
    {
      const typet &array_element_type1 =
        java_array_element_type(subtype_symbol1);
      const typet &array_element_type2 =
        java_array_element_type(subtype_symbol2);
 
      arrays_with_same_element_type =
        equal_java_types(array_element_type1, array_element_type2);
    }
  }
  return (type1 == type2 && arrays_with_same_element_type);
}
 
std::vector<java_generic_parametert>
get_all_generic_parameters(const typet &type)
{
  std::vector<java_generic_parametert> generic_parameters;
  if(is_java_implicitly_generic_class_type(type))
  {
    const java_implicitly_generic_class_typet &implicitly_generic_class =
      to_java_implicitly_generic_class_type(to_java_class_type(type));
    generic_parameters.insert(
      generic_parameters.end(),
      implicitly_generic_class.implicit_generic_types().begin(),
      implicitly_generic_class.implicit_generic_types().end());
  }
  if(is_java_generic_class_type(type))
  {
    const java_generic_class_typet &generic_class =
      to_java_generic_class_type(to_java_class_type(type));
    generic_parameters.insert(
      generic_parameters.end(),
      generic_class.generic_types().begin(),
      generic_class.generic_types().end());
  }
  return generic_parameters;
}
 
void get_dependencies_from_generic_parameters_rec(
  const typet &t,
  std::set<irep_idt> &refs)
{
  // Java generic type that holds different types in its type arguments
  if(is_java_generic_type(t))
  {
    for(const auto &type_arg : to_java_generic_type(t).generic_type_arguments())
      get_dependencies_from_generic_parameters_rec(type_arg, refs);
  }
 
  // Java reference type
  else if(t.id() == ID_pointer)
  {
    get_dependencies_from_generic_parameters_rec(
      to_pointer_type(t).base_type(), refs);
  }
 
  // method type with parameters and return value
  else if(t.id() == ID_code)
  {
    const java_method_typet &c = to_java_method_type(t);
    get_dependencies_from_generic_parameters_rec(c.return_type(), refs);
    for(const auto &param : c.parameters())
      get_dependencies_from_generic_parameters_rec(param.type(), refs);
  }
 
  // struct tag
  else if(t.id() == ID_struct_tag)
  {
    const auto &struct_tag_type = to_struct_tag_type(t);
    const irep_idt class_name(struct_tag_type.get_identifier());
    if(is_java_array_tag(class_name))
    {
      get_dependencies_from_generic_parameters(
        java_array_element_type(struct_tag_type), refs);
    }
    else
      refs.insert(strip_java_namespace_prefix(class_name));
  }
}
 
void get_dependencies_from_generic_parameters(
  const std::string &signature,
  std::set<irep_idt> &refs)
{
  try
  {
    // class signature with bounds
    if(signature[0] == '<')
    {
      const std::vector<typet> types = java_generic_type_from_string(
        erase_type_arguments(signature), signature);
 
      for(const auto &t : types)
        get_dependencies_from_generic_parameters_rec(t, refs);
    }
 
    // class signature without bounds and without wildcards
    else if(signature.find('*') == std::string::npos)
    {
      auto type_from_string =
        java_type_from_string(signature, erase_type_arguments(signature));
      get_dependencies_from_generic_parameters_rec(*type_from_string, refs);
    }
  }
  catch(unsupported_java_class_signature_exceptiont &)
  {
    // skip for now, if we cannot parse it, we cannot detect which additional
    // classes should be loaded as dependencies
  }
}
 
void get_dependencies_from_generic_parameters(
  const typet &t,
  std::set<irep_idt> &refs)
{
  get_dependencies_from_generic_parameters_rec(t, refs);
}
 
java_generic_struct_tag_typet::java_generic_struct_tag_typet(
  const struct_tag_typet &type,
  const std::string &base_ref,
  const std::string &class_name_prefix)
  : struct_tag_typet(type)
{
  set(ID_C_java_generic_symbol, true);
  const auto base_type = java_type_from_string(base_ref, class_name_prefix);
  PRECONDITION(is_java_generic_type(*base_type));
  const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
  INVARIANT(
    type.get_identifier() ==
      to_struct_tag_type(gen_base_type.base_type()).get_identifier(),
    "identifier of " + type.pretty() + "\n and identifier of type " +
      gen_base_type.base_type().pretty() +
      "\ncreated by java_type_from_string for " + base_ref +
      " should be equal");
  generic_types().insert(
    generic_types().end(),
    gen_base_type.generic_type_arguments().begin(),
    gen_base_type.generic_type_arguments().end());
}
 
std::optional<size_t> java_generic_struct_tag_typet::generic_type_index(
  const java_generic_parametert &type) const
{
  const auto &type_variable = type.get_name();
  const auto &generics = generic_types();
  for(std::size_t i = 0; i < generics.size(); ++i)
  {
    auto param = type_try_dynamic_cast<java_generic_parametert>(generics[i]);
    if(param && param->get_name() == type_variable)
      return i;
  }
  return {};
}
 
std::string pretty_java_type(const typet &type)
{
  if(type == java_void_type())
    return "void";
  if(type == java_int_type())
    return "int";
  else if(type == java_long_type())
    return "long";
  else if(type == java_short_type())
    return "short";
  else if(type == java_byte_type())
    return "byte";
  else if(type == java_char_type())
    return "char";
  else if(type == java_float_type())
    return "float";
  else if(type == java_double_type())
    return "double";
  else if(type == java_boolean_type())
    return "boolean";
  else if(type == java_byte_type())
    return "byte";
  else if(is_reference(type))
  {
    if(to_reference_type(type).base_type().id() == ID_struct_tag)
    {
      const auto &struct_tag_type =
        to_struct_tag_type(to_reference_type(type).base_type());
      const irep_idt &id = struct_tag_type.get_identifier();
      if(is_java_array_tag(id))
        return pretty_java_type(java_array_element_type(struct_tag_type)) +
               "[]";
      else
        return id2string(strip_java_namespace_prefix(id));
    }
    else
      return "?";
  }
  else
    return "?";
}
 
std::string pretty_signature(const java_method_typet &method_type)
{
  std::ostringstream result;
  result << '(';
 
  bool first = true;
  for(const auto &p : method_type.parameters())
  {
    if(p.get_this())
      continue;
 
    if(first)
      first = false;
    else
      result << ", ";
 
    result << pretty_java_type(p.type());
  }
 
  result << ')';
  return result.str();
}