CBMC
|
#include <util/invariant.h>
#include <algorithm>
#include <set>
#include <util/c_types.h>
#include <util/narrow.h>
#include <util/std_expr.h>
Go to the source code of this file.
Classes | |
class | java_annotationt |
class | java_annotationt::valuet |
class | annotated_typet |
class | java_method_typet |
class | java_class_typet |
class | java_class_typet::componentt |
class | java_class_typet::methodt |
class | java_class_typet::java_lambda_method_handlet |
Represents a lambda call to a method. More... | |
class | java_reference_typet |
This is a specialization of reference_typet. More... | |
class | java_generic_parameter_tagt |
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> . More... | |
class | java_generic_parametert |
Reference that points to a java_generic_parameter_tagt. More... | |
class | java_generic_struct_tag_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_typet |
Reference that points to a java_generic_struct_tag_typet. 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... | |
Macros | |
#define | JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]" |
#define | JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions" |
#define | JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier" |
Functions | |
const annotated_typet & | to_annotated_type (const typet &type) |
annotated_typet & | to_annotated_type (typet &type) |
template<> | |
bool | can_cast_type< annotated_typet > (const typet &) |
template<> | |
bool | can_cast_type< java_method_typet > (const typet &type) |
const java_method_typet & | to_java_method_type (const typet &type) |
java_method_typet & | to_java_method_type (typet &type) |
const java_class_typet & | to_java_class_type (const typet &type) |
java_class_typet & | to_java_class_type (typet &type) |
template<> | |
bool | can_cast_type< java_class_typet > (const typet &type) |
template<> | |
bool | can_cast_type< java_reference_typet > (const typet &type) |
const java_reference_typet & | to_java_reference_type (const typet &type) |
java_reference_typet & | to_java_reference_type (typet &type) |
signedbv_typet | java_int_type () |
signedbv_typet | java_long_type () |
signedbv_typet | java_short_type () |
signedbv_typet | java_byte_type () |
unsignedbv_typet | java_char_type () |
floatbv_typet | java_float_type () |
floatbv_typet | java_double_type () |
c_bool_typet | java_boolean_type () |
empty_typet | java_void_type () |
java_reference_typet | java_reference_type (const struct_tag_typet &subtype) |
reference_typet | java_reference_type (const typet &subtype) |
java_reference_typet | java_lang_object_type () |
struct_tag_typet | java_classname (const std::string &) |
java_reference_typet | java_array_type (const char subtype) |
Construct an array pointer type. More... | |
java_reference_typet | java_reference_array_type (const struct_tag_typet &element_type) |
const typet & | java_array_element_type (const struct_tag_typet &array_symbol) |
Return a const reference to the element type of a given java array type. More... | |
typet & | java_array_element_type (struct_tag_typet &array_symbol) |
Return a non-const reference to the element type of a given java array type. More... | |
bool | is_java_array_type (const typet &type) |
Checks whether the given type is an array pointer type. More... | |
bool | is_multidim_java_array_type (const typet &type) |
Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array type with element type also being a pointer to an array type. More... | |
std::pair< typet, std::size_t > | java_array_dimension_and_element_type (const struct_tag_typet &type) |
Returns the underlying element type and array dimensionality of Java struct type . More... | |
exprt | get_array_dimension_field (const exprt &pointer) |
exprt | get_array_element_type_field (const exprt &pointer) |
typet | java_type_from_char (char t) |
Constructs a type indicated by the given character: More... | |
std::optional< 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< typet > | java_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... | |
std::vector< std::string > | parse_raw_list_types (std::string src, char opening_bracket, char closing_bracket) |
Given a substring of a descriptor or signature that contains one or more types parse out the individual type strings. 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_tag (const typet &type) |
Checks whether the type is a java generic parameter/variable, e.g., T in List<T> . More... | |
const java_generic_parameter_tagt & | to_java_generic_parameter_tag (const typet &type) |
java_generic_parameter_tagt & | to_java_generic_parameter_tag (typet &type) |
template<> | |
bool | can_cast_type< java_generic_parametert > (const typet &base) |
Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T> . 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_parametert & | to_java_generic_parameter (const typet &type) |
java_generic_parametert & | to_java_generic_parameter (typet &type) |
bool | is_java_generic_struct_tag_type (const typet &type) |
const java_generic_struct_tag_typet & | to_java_generic_struct_tag_type (const typet &type) |
java_generic_struct_tag_typet & | to_java_generic_struct_tag_type (typet &type) |
template<> | |
bool | can_cast_type< java_generic_typet > (const typet &type) |
bool | is_java_generic_type (const typet &type) |
const java_generic_typet & | to_java_generic_type (const typet &type) |
java_generic_typet & | to_java_generic_type (typet &type) |
bool | is_java_generic_class_type (const typet &type) |
const java_generic_class_typet & | to_java_generic_class_type (const java_class_typet &type) |
java_generic_class_typet & | to_java_generic_class_type (java_class_typet &type) |
const typet & | java_generic_get_inst_type (size_t index, const java_generic_typet &type) |
Access information of type arguments of java instantiated type. More... | |
const irep_idt & | java_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 typet & | java_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_typet & | to_java_implicitly_generic_class_type (const java_class_typet &type) |
java_implicitly_generic_class_typet & | to_java_implicitly_generic_class_type (java_class_typet &type) |
std::vector< java_generic_parametert > | get_all_generic_parameters (const typet &type) |
std::optional< typet > | java_type_from_string_with_exception (const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name) |
const std::optional< 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... | |
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 java_method_typet &) |
#define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions" |
Definition at line 668 of file java_types.h.
#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier" |
Definition at line 670 of file java_types.h.
#define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]" |
Definition at line 655 of file java_types.h.
|
inline |
Definition at line 94 of file java_types.h.
|
inline |
Definition at line 594 of file java_types.h.
|
inline |
Check whether a reference to a typet is a Java generic parameter/variable, e.g., T
in List<T>
.
base | Source type. |
type
is a generic Java parameter type Definition at line 809 of file java_types.h.
|
inline |
Definition at line 938 of file java_types.h.
|
inline |
Definition at line 178 of file java_types.h.
|
inline |
Definition at line 623 of file java_types.h.
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 895 of file java_types.cpp.
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
src | The input string |
Definition at line 334 of file java_types.cpp.
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 516 of file java_types.cpp.
std::string gather_full_class_name | ( | const std::string & | src | ) |
Returns the full class name, skipping over the generics.
This turns any of these:
com.package.OuterClass.Inner
src | a type descriptor or signature
|
Definition at line 365 of file java_types.cpp.
std::vector<java_generic_parametert> get_all_generic_parameters | ( | const typet & | type | ) |
type | Source type |
Definition at line 924 of file java_types.cpp.
pointer | pointer to an array[reference] object |
Definition at line 206 of file java_types.cpp.
pointer | pointer to an array[reference] object |
Definition at line 218 of file java_types.cpp.
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 | |
[out] | refs | the set to insert the names of the found dependencies |
Definition at line 996 of file java_types.cpp.
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 | |
[out] | refs | the set to insert the names of the found dependencies |
Definition at line 1032 of file java_types.cpp.
bool is_java_array_tag | ( | const irep_idt & | tag | ) |
See above.
tag | Tag of a struct |
Definition at line 233 of file java_types.cpp.
bool is_java_array_type | ( | const typet & | type | ) |
Checks whether the given type is an array pointer type.
Definition at line 163 of file java_types.cpp.
|
inline |
type | the type to check |
Definition at line 994 of file java_types.h.
|
inline |
Checks whether the type is a java generic parameter/variable, e.g., T
in List<T>
.
type | the type to check |
Definition at line 819 of file java_types.h.
|
inline |
Checks whether the type is a java generic parameter/variable, e.g., T
in List<T>
.
type | the type to check |
Definition at line 750 of file java_types.h.
|
inline |
type | the type to check |
Definition at line 888 of file java_types.h.
|
inline |
type | the type to check |
Definition at line 946 of file java_types.h.
|
inline |
type | the type to check |
Definition at line 1099 of file java_types.h.
bool is_multidim_java_array_type | ( | const typet & | type | ) |
Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array type with element type also being a pointer to an array type.
Definition at line 179 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 838 of file java_types.cpp.
std::pair<typet, std::size_t> java_array_dimension_and_element_type | ( | const struct_tag_typet & | type | ) |
Returns the underlying element type and array dimensionality of Java struct type
.
If this is not an array type the return value will be {type, 0}
.
Definition at line 189 of file java_types.cpp.
const typet& java_array_element_type | ( | const struct_tag_typet & | array_symbol | ) |
Return a const reference to the element type of a given java array type.
array_symbol | The java array type |
Definition at line 144 of file java_types.cpp.
typet& java_array_element_type | ( | struct_tag_typet & | array_symbol | ) |
Return a non-const reference to the element type of a given java array type.
array_symbol | The java array type |
Definition at line 154 of file java_types.cpp.
java_reference_typet java_array_type | ( | const char | subtype | ) |
Construct an array pointer type.
It is a pointer to a symbol with identifier java::array[]. Its ID_element_type is set to the corresponding primitive type, or void* for arrays of references.
subtype | Character indicating the type of array |
Definition at line 109 of file java_types.cpp.
c_bool_typet java_boolean_type | ( | ) |
Definition at line 79 of file java_types.cpp.
signedbv_typet java_byte_type | ( | ) |
Definition at line 55 of file java_types.cpp.
Java does not support byte/short return types. These are always promoted.
Definition at line 281 of file java_types.cpp.
Java does not support byte/short return types. These are always promoted.
Definition at line 269 of file java_types.cpp.
char java_char_from_type | ( | const typet & | type | ) |
Definition at line 708 of file java_types.cpp.
unsignedbv_typet java_char_type | ( | ) |
Definition at line 61 of file java_types.cpp.
struct_tag_typet java_classname | ( | const std::string & | id | ) |
Definition at line 809 of file java_types.cpp.
floatbv_typet java_double_type | ( | ) |
Definition at line 73 of file java_types.cpp.
floatbv_typet java_float_type | ( | ) |
Definition at line 67 of file java_types.cpp.
Access information of the type bound of a generic java class type.
index | the index of the type variable |
t | the type from which to extract the type bound |
Definition at line 1050 of file java_types.h.
|
inline |
Access information of type variables of a generic java class type.
index | the index of the type variable |
type | the type from which to extract the type variable |
Definition at line 1036 of file java_types.h.
|
inline |
Access information of type arguments of java instantiated type.
index | the index of the type argument |
type | the type from which to extract the type argument |
Definition at line 1021 of file java_types.h.
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 749 of file java_types.cpp.
|
inline |
Get the index in the subtypes array for a given component.
gen_types | The subtypes array. |
identifier | The string identifier of the type of the component. |
Definition at line 1159 of file java_types.h.
signedbv_typet java_int_type | ( | ) |
Definition at line 31 of file java_types.cpp.
java_reference_typet java_lang_object_type | ( | ) |
Definition at line 98 of file java_types.cpp.
signedbv_typet java_long_type | ( | ) |
Definition at line 43 of file java_types.cpp.
java_reference_typet java_reference_array_type | ( | const struct_tag_typet & | element_type | ) |
Definition at line 541 of file java_types.cpp.
java_reference_typet java_reference_type | ( | const struct_tag_typet & | subtype | ) |
Definition at line 93 of file java_types.cpp.
reference_typet java_reference_type | ( | const typet & | subtype | ) |
Definition at line 88 of file java_types.cpp.
signedbv_typet java_short_type | ( | ) |
Definition at line 49 of file java_types.cpp.
typet java_type_from_char | ( | char | t | ) |
Constructs a type indicated by the given character:
Definition at line 248 of file java_types.cpp.
std::optional<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 561 of file java_types.cpp.
|
inline |
Definition at line 1140 of file java_types.h.
empty_typet java_void_type | ( | ) |
Definition at line 37 of file java_types.cpp.
std::vector<std::string> parse_raw_list_types | ( | const std::string | src, |
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 type strings.
src | The input string that is wrapped in either ( ) or < > |
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 419 of file java_types.cpp.
std::string pretty_java_type | ( | const typet & | type | ) |
Definition at line 1089 of file java_types.cpp.
std::string pretty_signature | ( | const java_method_typet & | method_type | ) |
Definition at line 1131 of file java_types.cpp.
|
inline |
Definition at line 83 of file java_types.h.
|
inline |
Definition at line 88 of file java_types.h.
|
inline |
Definition at line 581 of file java_types.h.
|
inline |
Definition at line 587 of file java_types.h.
|
inline |
type | the type to check |
Definition at line 1002 of file java_types.h.
|
inline |
type | source type |
Definition at line 1011 of file java_types.h.
|
inline |
type | source type |
Definition at line 826 of file java_types.h.
|
inline |
type | source type |
Definition at line 835 of file java_types.h.
|
inline |
type | source type |
Definition at line 758 of file java_types.h.
|
inline |
type | source type |
Definition at line 766 of file java_types.h.
|
inline |
type | the type to convert |
Definition at line 896 of file java_types.h.
|
inline |
type | the type to convert |
Definition at line 905 of file java_types.h.
|
inline |
type | source type |
Definition at line 953 of file java_types.h.
|
inline |
type | source type |
Definition at line 962 of file java_types.h.
|
inline |
type | the type to check |
Definition at line 1107 of file java_types.h.
|
inline |
type | source type |
Definition at line 1116 of file java_types.h.
|
inline |
Definition at line 183 of file java_types.h.
|
inline |
Definition at line 189 of file java_types.h.
|
inline |
Definition at line 629 of file java_types.h.
|
inline |
Definition at line 635 of file java_types.h.