cprover
java_types.h File Reference
#include <util/invariant.h>
#include <algorithm>
#include <set>
#include <util/type.h>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/optional.h>
#include <util/std_expr.h>
Include dependency graph for java_types.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  java_annotationt
 
class  java_annotationt::valuet
 
class  annotated_typet
 
class  java_class_typet
 
class  java_generic_parametert
 Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>. More...
 
class  java_generic_typet
 Class to hold type with generic type arguments, for example java.util.List in either a reference of type List<Integer> or List<T> (here T must have been concretized already to create this object so technically it is an argument rather than parameter/variable, but in the symbol table this still shows as the parameter T). More...
 
class  java_generic_class_typet
 Class to hold a class with generics, extends the java class type with a vector of java generic type parameters (also called type variables). More...
 
class  java_implicitly_generic_class_typet
 Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class or a derived class of a generic base class. More...
 
class  unsupported_java_class_signature_exceptiont
 An exception that is raised for unsupported class signature. More...
 
class  java_generic_symbol_typet
 Type for a generic symbol, extends symbol_typet with a vector of java generic types. More...
 

Functions

const annotated_typetto_annotated_type (const typet &type)
 
annotated_typetto_annotated_type (typet &type)
 
template<>
bool can_cast_type< annotated_typet > (const typet &type)
 
const java_class_typetto_java_class_type (const typet &type)
 
java_class_typetto_java_class_type (typet &type)
 
template<>
bool can_cast_type< java_class_typet > (const typet &type)
 
typet java_int_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 ()
 
symbol_typet java_classname (const std::string &)
 
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_reference_type (char t)
 
typet java_type_from_char (char t)
 
typet java_type_from_string (const std::string &, 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 &, const std::string &)
 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...
 
typet java_bytecode_promotion (const typet &)
 Java does not support byte/short return types. These are always promoted. More...
 
exprt java_bytecode_promotion (const exprt &)
 Java does not support byte/short return types. These are always promoted. More...
 
size_t find_closing_semi_colon_for_reference_type (const std::string src, size_t starting_point=0)
 Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point. More...
 
bool is_java_array_tag (const irep_idt &tag)
 See above. More...
 
bool is_valid_java_array (const struct_typet &)
 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...
 
bool is_java_generic_parameter (const typet &type)
 Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. More...
 
const java_generic_parametertto_java_generic_parameter (const typet &type)
 
java_generic_parametertto_java_generic_parameter (typet &type)
 
bool is_java_generic_type (const typet &type)
 
const java_generic_typetto_java_generic_type (const typet &type)
 
java_generic_typetto_java_generic_type (typet &type)
 
bool is_java_generic_class_type (const typet &type)
 
const java_generic_class_typetto_java_generic_class_type (const java_class_typet &type)
 
java_generic_class_typetto_java_generic_class_type (java_class_typet &type)
 
const typetjava_generic_get_inst_type (size_t index, const java_generic_typet &type)
 Access information of type arguments of java instantiated type. More...
 
const irep_idtjava_generic_class_type_var (size_t index, const java_generic_class_typet &type)
 Access information of type variables of a generic java class type. More...
 
const typetjava_generic_class_type_bound (size_t index, const typet &t)
 Access information of the type bound of a generic java class type. More...
 
bool is_java_implicitly_generic_class_type (const typet &type)
 
const java_implicitly_generic_class_typetto_java_implicitly_generic_class_type (const java_class_typet &type)
 
java_implicitly_generic_class_typetto_java_implicitly_generic_class_type (java_class_typet &type)
 
typet java_type_from_string_with_exception (const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
 
const optionalt< size_t > java_generics_get_index_for_subtype (const std::vector< java_generic_parametert > &gen_types, const irep_idt &identifier)
 Get the index in the subtypes array for a given component. More...
 
void get_dependencies_from_generic_parameters (const std::string &, std::set< irep_idt > &)
 Collect information about generic type parameters from a given signature. More...
 
void get_dependencies_from_generic_parameters (const typet &, std::set< irep_idt > &)
 Collect information about generic type parameters from a given type. More...
 
bool is_java_generic_symbol_type (const typet &type)
 
const java_generic_symbol_typetto_java_generic_symbol_type (const typet &type)
 
java_generic_symbol_typetto_java_generic_symbol_type (typet &type)
 
std::string erase_type_arguments (const std::string &)
 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 More...
 
std::string gather_full_class_name (const std::string &)
 Returns the full class name, skipping over the generics. More...
 
std::string pretty_java_type (const typet &)
 
std::string pretty_signature (const code_typet &)
 

Function Documentation

◆ can_cast_type< annotated_typet >()

template<>
bool can_cast_type< annotated_typet > ( const typet type)
inline

Definition at line 96 of file java_types.h.

◆ can_cast_type< java_class_typet >()

template<>
bool can_cast_type< java_class_typet > ( const typet type)
inline

Definition at line 176 of file java_types.h.

References can_cast_type< class_typet >().

◆ 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, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet

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.

This turns any of these:

  1. Signature: Lcom/package/OuterClass<TT;>.Inner;
  2. Descriptor: Lcom.pacakge.OuterClass$Inner; into com.package.OuterClass.Inner
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().

◆ is_java_array_tag()

◆ is_java_generic_class_type()

◆ is_java_generic_parameter()

◆ is_java_generic_symbol_type()

bool is_java_generic_symbol_type ( const typet type)
inline
Parameters
typethe type to check
Returns
true if the type is a symbol type with generics

Definition at line 613 of file java_types.h.

References irept::get_bool().

Referenced by generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), require_type::require_java_generic_symbol_type(), and to_java_generic_symbol_type().

◆ is_java_generic_type()

◆ is_java_implicitly_generic_class_type()

bool is_java_implicitly_generic_class_type ( const typet type)
inline

◆ is_reference_type()

bool is_reference_type ( 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 )

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 &  )

◆ java_double_type()

◆ java_float_type()

◆ java_generic_class_type_bound()

const typet& java_generic_class_type_bound ( size_t  index,
const typet t 
)
inline

Access information of the type bound of a generic java class type.

Parameters
indexthe index of the type variable
tthe type from which to extract the type bound
Returns
the type of the bound of the type variable

Definition at line 454 of file java_types.h.

References java_generic_class_typet::generic_types(), is_java_generic_class_type(), PRECONDITION, to_java_class_type(), and to_java_generic_class_type().

◆ java_generic_class_type_var()

const irep_idt& java_generic_class_type_var ( size_t  index,
const java_generic_class_typet type 
)
inline

Access information of type variables of a generic java class type.

Parameters
indexthe index of the type variable
typethe type from which to extract the type variable
Returns
the name of the generic type variable of t at the given index

Definition at line 440 of file java_types.h.

References java_generic_class_typet::generic_types(), and PRECONDITION.

◆ java_generic_get_inst_type()

const typet& java_generic_get_inst_type ( size_t  index,
const java_generic_typet type 
)
inline

Access information of type arguments of java instantiated type.

Parameters
indexthe index of the type argument
typethe type from which to extract the type argument
Returns
the type variable of t at the given index

Definition at line 425 of file java_types.h.

References java_generic_typet::generic_type_arguments(), and PRECONDITION.

◆ 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_generics_get_index_for_subtype()

const optionalt<size_t> java_generics_get_index_for_subtype ( const std::vector< java_generic_parametert > &  gen_types,
const irep_idt identifier 
)
inline

Get the index in the subtypes array for a given component.

Parameters
tThe type we search for the subtypes in.
identifierThe string identifier of the type of the component.
Returns
Optional with the size if the identifier was found.

Definition at line 557 of file java_types.h.

◆ 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_type_from_string_with_exception()

typet java_type_from_string_with_exception ( const std::string &  descriptor,
const optionalt< std::string > &  signature,
const std::string &  class_name 
)
inline

◆ pretty_java_type()

◆ pretty_signature()

std::string pretty_signature ( const code_typet )

◆ to_annotated_type() [1/2]

const annotated_typet& to_annotated_type ( const typet type)
inline

Definition at line 85 of file java_types.h.

◆ to_annotated_type() [2/2]

annotated_typet& to_annotated_type ( typet type)
inline

Definition at line 90 of file java_types.h.

◆ to_java_class_type() [1/2]

◆ to_java_class_type() [2/2]

java_class_typet& to_java_class_type ( typet type)
inline

Definition at line 169 of file java_types.h.

References irept::id().

◆ to_java_generic_class_type() [1/2]

const java_generic_class_typet& to_java_generic_class_type ( const java_class_typet type)
inline
Parameters
typethe type to check
Returns
cast of type to java_generics_class_typet

Definition at line 406 of file java_types.h.

References is_java_generic_class_type(), and PRECONDITION.

Referenced by get_all_generic_parameters(), java_generic_class_type_bound(), and require_type::require_java_generic_class().

◆ to_java_generic_class_type() [2/2]

java_generic_class_typet& to_java_generic_class_type ( java_class_typet type)
inline
Parameters
typesource type
Returns
cast of type into a java class type with generics

Definition at line 415 of file java_types.h.

References is_java_generic_class_type(), and PRECONDITION.

◆ to_java_generic_parameter() [1/2]

◆ to_java_generic_parameter() [2/2]

java_generic_parametert& to_java_generic_parameter ( typet type)
inline
Parameters
typesource type
Returns
cast of type into a java_generic_parameter

Definition at line 297 of file java_types.h.

References is_java_generic_parameter(), and PRECONDITION.

◆ to_java_generic_symbol_type() [1/2]

const java_generic_symbol_typet& to_java_generic_symbol_type ( const typet type)
inline
Parameters
typethe type to convert
Returns
the converted type

Definition at line 621 of file java_types.h.

References is_java_generic_symbol_type(), and PRECONDITION.

Referenced by generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), and require_type::require_java_generic_symbol_type().

◆ to_java_generic_symbol_type() [2/2]

java_generic_symbol_typet& to_java_generic_symbol_type ( typet type)
inline
Parameters
typethe type to convert
Returns
the converted type

Definition at line 629 of file java_types.h.

References is_java_generic_symbol_type(), and PRECONDITION.

◆ to_java_generic_type() [1/2]

◆ to_java_generic_type() [2/2]

java_generic_typet& to_java_generic_type ( typet type)
inline
Parameters
typesource type
Returns
cast of type into java type with generics

Definition at line 364 of file java_types.h.

References irept::id(), is_java_generic_type(), and PRECONDITION.

◆ to_java_implicitly_generic_class_type() [1/2]

const java_implicitly_generic_class_typet& to_java_implicitly_generic_class_type ( const java_class_typet type)
inline
Parameters
typethe type to check
Returns
cast of type to java_generics_class_typet

Definition at line 511 of file java_types.h.

References is_java_implicitly_generic_class_type(), and PRECONDITION.

Referenced by get_all_generic_parameters(), and require_type::require_java_implicitly_generic_class().

◆ to_java_implicitly_generic_class_type() [2/2]

java_implicitly_generic_class_typet& to_java_implicitly_generic_class_type ( java_class_typet type)
inline
Parameters
typesource type
Returns
cast of type into a java class type with generics

Definition at line 520 of file java_types.h.

References is_java_implicitly_generic_class_type(), and PRECONDITION.