cprover
java_types.cpp File Reference
#include <cctype>
#include <iterator>
#include <util/prefix.h>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include "java_types.h"
#include "java_utils.h"
Include dependency graph for java_types.cpp:

Go to the source code of this file.

Functions

std::vector< typetparse_list_types (const std::string src, const std::string class_name_prefix, const char opening_bracket, const char closing_bracket)
 Given a substring of a descriptor or signature that contains one or more types parse out the individual types. More...
 
typet java_int_type ()
 
typet java_void_type ()
 
typet java_long_type ()
 
typet java_short_type ()
 
typet java_byte_type ()
 
typet java_char_type ()
 
typet java_float_type ()
 
typet java_double_type ()
 
typet java_boolean_type ()
 
reference_typet java_reference_type (const typet &subtype)
 
reference_typet java_lang_object_type ()
 
reference_typet java_array_type (const char subtype)
 
typet java_array_element_type (const symbol_typet &array_type)
 Return the type of the elements of a given java array type. More...
 
bool is_java_array_tag (const irep_idt &tag)
 See above. More...
 
bool is_reference_type (const char t)
 
typet java_type_from_char (char t)
 
typet java_bytecode_promotion (const typet &type)
 Java does not support byte/short return types. These are always promoted. More...
 
exprt java_bytecode_promotion (const exprt &expr)
 Java does not support byte/short return types. These are always promoted. More...
 
void add_generic_type_information (java_generic_typet &generic_type, const std::string &type_arguments, const std::string &class_name_prefix)
 Take a list of generic type arguments and parse them into the generic type. More...
 
std::string erase_type_arguments (const std::string &src)
 Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally. More...
 
std::string gather_full_class_name (const std::string &src)
 Returns the full class name, skipping over the generics. More...
 
reference_typet build_class_name (const std::string &src, const std::string &class_name_prefix)
 For parsing a class type reference. More...
 
size_t find_closing_semi_colon_for_reference_type (const std::string src, size_t starting_point)
 Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point. More...
 
typet java_type_from_string (const std::string &src, const std::string &class_name_prefix)
 Transforms a string representation of a Java type into an internal type representation thereof. More...
 
char java_char_from_type (const typet &type)
 
std::vector< typetjava_generic_type_from_string (const std::string &class_name, const std::string &src)
 Converts the content of a generic class type into a vector of Java types, that is each type variable of the class has one entry in the returned vector. More...
 
static std::string slash_to_dot (const std::string &src)
 
symbol_typet java_classname (const std::string &id)
 
bool is_valid_java_array (const struct_typet &type)
 Programmatic documentation of the structure of a Java array (of either primitives or references) type. More...
 
bool equal_java_types (const typet &type1, const typet &type2)
 Compares the types, including checking element types if both types are arrays. More...
 
void get_dependencies_from_generic_parameters_rec (const typet &t, std::set< irep_idt > &refs)
 
void get_dependencies_from_generic_parameters (const std::string &signature, std::set< irep_idt > &refs)
 Collect information about generic type parameters from a given signature. More...
 
void get_dependencies_from_generic_parameters (const typet &t, std::set< irep_idt > &refs)
 Collect information about generic type parameters from a given type. More...
 
std::string pretty_java_type (const typet &type)
 
std::string pretty_signature (const code_typet &code_type)
 

Function Documentation

◆ add_generic_type_information()

void add_generic_type_information ( java_generic_typet generic_type,
const std::string &  type_arguments,
const std::string &  class_name_prefix 
)

Take a list of generic type arguments and parse them into the generic type.

Parameters
generic_type[out]: The existing generic type to add the information to
type_argumentsThe string representing the generic type arguments for a signature. For example <TT;Ljava/lang/Foo;LList<LInteger;>;> (including the wrapping angle brackets).
class_name_prefixThe name of the class to use to prefix any found generic types

Definition at line 196 of file java_types.cpp.

References CHECK_RETURN, java_generic_typet::generic_type_arguments(), INVARIANT, is_reference(), parse_list_types(), PRECONDITION, and to_reference_type().

Referenced by build_class_name().

◆ build_class_name()

reference_typet build_class_name ( const std::string &  src,
const std::string &  class_name_prefix 
)

For parsing a class type reference.

Parameters
srcThe input string Either a signature: "Lpackage/class<TT;>.innerclass<Ljava/lang/Foo;>; Or a descriptor: "Lpackage.class$inner;
class_name_prefixThe name of the class to use to prefix any found generic types
Returns
The reference type if parsed correctly, no value if parsing fails.

Definition at line 346 of file java_types.cpp.

References add_generic_type_information(), find_closing_delimiter(), gather_full_class_name(), java_reference_type(), PRECONDITION, and irept::set().

Referenced by java_type_from_string().

◆ equal_java_types()

bool equal_java_types ( const typet type1,
const typet type2 
)

Compares the types, including checking element types if both types are arrays.

Parameters
type1First type to compare
type2Second type to compare
Returns
True if the types are equal, including elemnt types if they are both arrays

Definition at line 733 of file java_types.cpp.

References equal_java_types(), symbol_typet::get_identifier(), irept::id(), is_java_array_tag(), java_array_element_type(), typet::subtype(), and to_symbol_type().

Referenced by equal_java_types(), and java_object_factoryt::gen_nondet_pointer_init().

◆ erase_type_arguments()

std::string erase_type_arguments ( const std::string &  src)

Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally.

Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet

Parameters
srcThe input string
Returns
The input string with everything between angle brackets removed

Definition at line 231 of file java_types.cpp.

References find_closing_delimiter().

Referenced by gather_full_class_name(), and get_dependencies_from_generic_parameters().

◆ find_closing_semi_colon_for_reference_type()

size_t find_closing_semi_colon_for_reference_type ( const std::string  src,
size_t  starting_point 
)

Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.

Parameters
srcThe input string to work on.
starting_pointThe string position where the opening 'L' we want to find the closing ';' for.
Returns
The string position corresponding to the matching ';'. For example: LA;, we would return 2. For LA<TT;>; we would return 7. See unit/java_bytecode/java_util_tests.cpp for more examples.

Definition at line 390 of file java_types.cpp.

References find_closing_delimiter(), INVARIANT, and PRECONDITION.

Referenced by extract_generic_interface_reference(), extract_generic_superclass_reference(), and parse_list_types().

◆ gather_full_class_name()

std::string gather_full_class_name ( const std::string &  src)

Returns the full class name, skipping over the generics.

Parameters
srca type descriptor or signature
  1. Signature: Lcom/package/OuterClass<TT;>.Inner;
  2. Descriptor: Lcom.package.OuterClass$Inner;
Returns
The full name of the class like com.package.OuterClass.Inner (for both examples).

Definition at line 262 of file java_types.cpp.

References erase_type_arguments(), and PRECONDITION.

Referenced by build_class_name().

◆ get_dependencies_from_generic_parameters() [1/2]

void get_dependencies_from_generic_parameters ( const std::string &  signature,
std::set< irep_idt > &  refs 
)

Collect information about generic type parameters from a given signature.

This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.

Parameters
signaturethe string representation of the signature to analyze
refs[out]: the set to insert the names of the found dependencies

Definition at line 805 of file java_types.cpp.

References erase_type_arguments(), get_dependencies_from_generic_parameters_rec(), java_generic_type_from_string(), and java_type_from_string().

Referenced by java_bytecode_parsert::get_class_refs(), get_dependencies_from_generic_parameters_rec(), and java_bytecode_parsert::rclass_attribute().

◆ get_dependencies_from_generic_parameters() [2/2]

void get_dependencies_from_generic_parameters ( const typet t,
std::set< irep_idt > &  refs 
)

Collect information about generic type parameters from a given type.

This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.

Parameters
tthe type to analyze
refs[out]: the set to insert the names of the found dependencies

Definition at line 841 of file java_types.cpp.

References get_dependencies_from_generic_parameters_rec().

◆ get_dependencies_from_generic_parameters_rec()

◆ is_java_array_tag()

◆ is_reference_type()

bool is_reference_type ( const char  t)

Definition at line 142 of file java_types.cpp.

◆ is_valid_java_array()

bool is_valid_java_array ( const struct_typet type)

Programmatic documentation of the structure of a Java array (of either primitives or references) type.

A Java array is represented in GOTO in the following way: A struct component with a tag like java::array[type] where type is either a primitive like int, or reference. The struct has precisely three components:

  1. @java.lang.Object: of type struct {java.lang.Object} containing the base class data
  2. length: of type Java integer - the length of the array
  3. data: of type pointer to either pointer to a primitive type, or pointer to pointer to empty (i.e. a void**) pointing to the contents of the array
    Parameters
    typeA type that might represent a Java array
    Returns
    True if it is a Java array type, false otherwise

Definition at line 696 of file java_types.cpp.

References struct_union_typet::components(), struct_union_typet::componentt::get_name(), irept::id(), java_int_type(), and exprt::type().

Referenced by java_object_factoryt::gen_nondet_array_init().

◆ java_array_element_type()

typet java_array_element_type ( const symbol_typet array_type)

Return the type of the elements of a given java array type.

Parameters
array_typeThe java array type
Returns
The type of the elements of the array

Definition at line 126 of file java_types.cpp.

References typet::find_type(), symbol_typet::get_identifier(), INVARIANT, and is_java_array_tag().

Referenced by equal_java_types(), ci_lazy_methods_neededt::gather_field_types(), get_dependencies_from_generic_parameters_rec(), pretty_java_type(), and select_pointer_typet::specialize_generics().

◆ java_array_type()

◆ java_boolean_type()

◆ java_byte_type()

◆ java_bytecode_promotion() [1/2]

◆ java_bytecode_promotion() [2/2]

exprt java_bytecode_promotion ( const exprt expr)

Java does not support byte/short return types. These are always promoted.

Definition at line 178 of file java_types.cpp.

References java_bytecode_promotion(), and exprt::type().

◆ java_char_from_type()

◆ java_char_type()

◆ java_classname()

symbol_typet java_classname ( const std::string &  id)

◆ java_double_type()

◆ java_float_type()

◆ java_generic_type_from_string()

std::vector<typet> java_generic_type_from_string ( const std::string &  class_name,
const std::string &  src 
)

Converts the content of a generic class type into a vector of Java types, that is each type variable of the class has one entry in the returned vector.

This also supports parsing of bounds in the form of <T:CBound> for classes or <T::IBound> for interfaces.

For example for HashMap<K, V> a vector with two elements would be returned

Returns
vector of java types representing the generic type variables

the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;> or of the form <TX::Bound_X;:BoundZ;TY:Bound_Y;> if Bound_X is an interface

Definition at line 610 of file java_types.cpp.

References find_closing_delimiter(), INVARIANT, java_type_from_string(), PRECONDITION, and to_symbol_type().

Referenced by java_bytecode_convert_classt::convert(), and get_dependencies_from_generic_parameters().

◆ java_int_type()

typet java_int_type ( )

Definition at line 32 of file java_types.cpp.

Referenced by add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), java_object_factoryt::allocate_nondet_length_array(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_convert_methodt::convert_cmp(), java_bytecode_convert_methodt::convert_cmp2(), java_bytecode_convert_methodt::convert_iinc(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_newarray(), expr2javat::convert_rec(), java_object_factoryt::gen_nondet_array_init(), java_string_library_preprocesst::get_object_at_index(), get_or_create_string_literal_symbol(), java_string_library_preprocesst::get_primitive_value_of_object(), initialize_nondet_string_struct(), instrument_getCurrentThreadID(), instrument_start_thread(), is_valid_java_array(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_nondet_string_expr(), java_string_library_preprocesst::make_object_get_class_code(), java_string_library_preprocesst::make_string_format_code(), pretty_java_type(), java_bytecode_parsert::rconstant_pool(), java_string_library_preprocesst::replace_char_array(), java_string_library_preprocesst::string_expr_of_function(), string_length_type(), and utf16_to_array().

◆ java_lang_object_type()

reference_typet java_lang_object_type ( )

Definition at line 85 of file java_types.cpp.

References java_reference_type().

Referenced by remove_instanceoft::lower_instanceof().

◆ java_long_type()

◆ java_reference_type()

◆ java_short_type()

◆ java_type_from_char()

◆ java_type_from_string()

typet java_type_from_string ( const std::string &  src,
const std::string &  class_name_prefix 
)

Transforms a string representation of a Java type into an internal type representation thereof.

Example use are object types like "Ljava/lang/Integer;", type variables/parameters like "TE;" which require a non-empty class_name_prefix or generic types like "Ljava/util/List<TE;>;" or "Ljava/util/List<Ljava/lang/Integer;>;" also requiring class_name_prefix.

Parameters
srcthe string representation as used in the class file
class_name_prefixname of class to append to generic type variables/parameters
Returns
internal type representation for GOTO programs

Definition at line 428 of file java_types.cpp.

References build_class_name(), find_closing_delimiter(), irept::id(), INVARIANT, java_array_type(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), java_type_from_string(), java_void_type(), parse_list_types(), PRECONDITION, irept::set(), typet::subtype(), and to_symbol_type().

Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_parsert::get_class_refs(), get_dependencies_from_generic_parameters(), is_java_main(), java_classname(), java_generic_symbol_typet::java_generic_symbol_typet(), java_generic_type_from_string(), java_type_from_string(), java_type_from_string_with_exception(), member_type_lazy(), parse_list_types(), java_bytecode_convert_methodt::setup_local_variables(), and java_bytecode_parsert::type_entry().

◆ java_void_type()

typet java_void_type ( )

Definition at line 37 of file java_types.cpp.

Referenced by java_type_from_string().

◆ parse_list_types()

std::vector< typet > parse_list_types ( const std::string  src,
const std::string  class_name_prefix,
const char  opening_bracket,
const char  closing_bracket 
)

Given a substring of a descriptor or signature that contains one or more types parse out the individual types.

This is used for parsing the parameters of a function or the generic type variables/parameters or arguments contained within angle brackets.

Parameters
srcThe input string that is wrapped in either ( ) or < >
class_name_prefixThe name of the class to use to prefix any found generic types
opening_bracketFor checking string is passed in as expected, the opening bracket (i.e. '(' or '<').
closing_bracketFor checking string is passed in as expected, the closing bracket (i.e. ')' or '>').
Returns
A vector of types that the string represents

Definition at line 289 of file java_types.cpp.

References find_closing_semi_colon_for_reference_type(), INVARIANT, java_type_from_string(), and PRECONDITION.

Referenced by add_generic_type_information(), and java_type_from_string().

◆ pretty_java_type()

◆ pretty_signature()

std::string pretty_signature ( const code_typet code_type)

◆ slash_to_dot()

static std::string slash_to_dot ( const std::string &  src)
static

Definition at line 659 of file java_types.cpp.

Referenced by java_classname().