cprover
|
#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"
Go to the source code of this file.
Functions | |
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. 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< 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. 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) |
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.
generic_type | [out]: The existing generic type to add the information to |
type_arguments | The string representing the generic type arguments for a signature. For example <TT;Ljava/lang/Foo;LList<LInteger;>;> (including the wrapping angle brackets). |
class_name_prefix | The 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().
reference_typet build_class_name | ( | const std::string & | src, |
const std::string & | class_name_prefix | ||
) |
For parsing a class type reference.
src | The input string Either a signature: "Lpackage/class<TT;>.innerclass<Ljava/lang/Foo;>; Or a descriptor: "Lpackage.class$inner; |
class_name_prefix | The name of the class to use to prefix any found generic types |
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().
Compares the types, including checking element types if both types are arrays.
type1 | First type to compare |
type2 | Second type to compare |
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().
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
src | The input string |
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().
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
.
src | The input string to work on. |
starting_point | The string position where the opening 'L' we want to find the closing ';' for. |
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().
std::string gather_full_class_name | ( | const std::string & | src | ) |
Returns the full class name, skipping over the generics.
src | a type descriptor or signature
|
Definition at line 262 of file java_types.cpp.
References erase_type_arguments(), and PRECONDITION.
Referenced by build_class_name().
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.
signature | the 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().
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.
t | the 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().
Definition at line 758 of file java_types.cpp.
References get_dependencies_from_generic_parameters(), symbol_typet::get_identifier(), irept::id(), is_java_array_tag(), is_java_generic_type(), java_array_element_type(), code_typet::parameters(), code_typet::return_type(), strip_java_namespace_prefix(), typet::subtype(), to_code_type(), to_java_generic_type(), and to_symbol_type().
Referenced by get_dependencies_from_generic_parameters().
bool is_java_array_tag | ( | const irep_idt & | tag | ) |
See above.
Definition at line 137 of file java_types.cpp.
References has_prefix(), and id2string().
Referenced by equal_java_types(), ci_lazy_methods_neededt::gather_field_types(), get_dependencies_from_generic_parameters_rec(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), java_array_element_type(), java_is_array_type(), java_static_lifetime_init(), pretty_java_type(), require_goto_statements::require_struct_array_component_assignment(), and select_pointer_typet::specialize_generics().
bool is_reference_type | ( | const char | t | ) |
Definition at line 142 of file java_types.cpp.
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:
type | A type that might represent a Java array |
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().
typet java_array_element_type | ( | const symbol_typet & | array_type | ) |
Return the type of the elements of a given java array type.
array_type | The java array type |
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().
reference_typet java_array_type | ( | const char | subtype | ) |
Definition at line 90 of file java_types.cpp.
References id2string(), java_reference_type(), java_type_from_char(), irept::set(), and UNREACHABLE.
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_newarray(), java_type_from_string(), and select_pointer_typet::specialize_generics().
typet java_boolean_type | ( | ) |
Definition at line 72 of file java_types.cpp.
Referenced by constant_bool(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_root_class(), java_static_lifetime_init(), java_type_from_char(), java_type_from_string(), java_string_library_preprocesst::make_string_format_code(), and pretty_java_type().
typet java_byte_type | ( | ) |
Definition at line 52 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
Java does not support byte/short return types. These are always promoted.
Definition at line 166 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_int_type(), and java_short_type().
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_getstatic(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), and java_bytecode_promotion().
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().
char java_char_from_type | ( | const typet & | type | ) |
Definition at line 569 of file java_types.cpp.
References bitvector_typet::get_width(), irept::id(), java_byte_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), to_floatbv_type(), and to_signedbv_type().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_initialize_parameter_names().
typet java_char_type | ( | ) |
Definition at line 57 of file java_types.cpp.
Referenced by java_string_library_preprocesst::add_string_type(), expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::decl_string_expr(), java_string_library_preprocesst::get_primitive_value_of_object(), initialize_nondet_string_struct(), java_bytecode_promotion(), java_type_from_char(), java_type_from_string(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_string_format_code(), pretty_java_type(), java_string_library_preprocesst::replace_char_array(), and utf16_to_array().
symbol_typet java_classname | ( | const std::string & | id | ) |
Definition at line 668 of file java_types.cpp.
References java_type_from_string(), irept::set(), slash_to_dot(), and to_symbol_type().
Referenced by java_bytecode_parsert::rconstant_pool().
typet java_double_type | ( | ) |
Definition at line 67 of file java_types.cpp.
References ieee_float_spect::double_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
typet java_float_type | ( | ) |
Definition at line 62 of file java_types.cpp.
References ieee_float_spect::single_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), java_string_library_preprocesst::make_string_format_code(), and pretty_java_type().
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
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().
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().
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().
typet java_long_type | ( | ) |
Definition at line 42 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), pretty_java_type(), and java_bytecode_parsert::rconstant_pool().
reference_typet java_reference_type | ( | const typet & | subtype | ) |
Definition at line 80 of file java_types.cpp.
References reference_type().
Referenced by build_class_name(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), generate_java_start_function(), java_array_type(), java_bytecode_convert_method_lazy(), java_lang_object_type(), java_type_from_char(), java_string_library_preprocesst::make_argument_for_format(), java_string_library_preprocesst::make_object_get_class_code(), and to_member().
typet java_short_type | ( | ) |
Definition at line 47 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
typet java_type_from_char | ( | char | t | ) |
Definition at line 147 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_reference_type(), java_short_type(), and UNREACHABLE.
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_const(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_ushr(), java_array_type(), and java_bytecode_convert_methodt::variable().
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
.
src | the string representation as used in the class file |
class_name_prefix | name of class to append to generic type variables/parameters |
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().
typet java_void_type | ( | ) |
Definition at line 37 of file java_types.cpp.
Referenced by java_type_from_string().
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.
src | The input string that is wrapped in either ( ) or < > |
class_name_prefix | The name of the class to use to prefix any found generic types |
opening_bracket | For checking string is passed in as expected, the opening bracket (i.e. '(' or '<'). |
closing_bracket | For checking string is passed in as expected, the closing bracket (i.e. ')' or '>'). |
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().
std::string pretty_java_type | ( | const typet & | type | ) |
Definition at line 897 of file java_types.cpp.
References irept::id(), id2string(), is_java_array_tag(), is_reference(), java_array_element_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(), pretty_java_type(), strip_java_namespace_prefix(), typet::subtype(), and to_symbol_type().
Referenced by pretty_java_type(), and pretty_signature().
std::string pretty_signature | ( | const code_typet & | code_type | ) |
Definition at line 935 of file java_types.cpp.
References code_typet::parameters(), and pretty_java_type().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_convert_method_lazy().
|
static |
Definition at line 659 of file java_types.cpp.
Referenced by java_classname().