#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>

Include dependency graph for java_types.cpp:

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...

signedbv_typet	java_int_type ()

empty_typet	java_void_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 ()

reference_typet	java_reference_type (const typet &subtype)

java_reference_typet	java_reference_type (const struct_tag_typet &subtype)

java_reference_typet	java_lang_object_type ()

java_reference_typet	java_array_type (const char subtype)
	Construct an array pointer type. More...

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)

bool	is_java_array_tag (const irep_idt &tag)
	See above. More...

typet	java_type_from_char (char t)
	Constructs a type indicated by the given character: More...

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...

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. 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...

java_reference_typet	java_reference_array_type (const struct_tag_typet &subtype)

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

struct_tag_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...

std::vector< java_generic_parametert >	get_all_generic_parameters (const typet &type)

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 java_method_typet &method_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

[out]	generic_type	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 299 of file java_types.cpp.

◆ 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

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

Returns: The reference type if parsed correctly, no value if parsing fails.

Definition at line 472 of file java_types.cpp.

◆ 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

type1	First type to compare
type2	Second type to compare

Returns: True if the types are equal, including elemnt types if they are both arrays

Definition at line 895 of file java_types.cpp.

◆ 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

src	The input string

Returns: The input string with everything between angle brackets removed

Definition at line 334 of file java_types.cpp.

◆ 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

src	The input string to work on.
starting_point	The 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 516 of file java_types.cpp.

◆ gather_full_class_name()

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

Returns the full class name, skipping over the generics.

Parameters

src	a type descriptor or signature Signature: Lcom/package/OuterClass<TT;>.Inner; Descriptor: Lcom.package.OuterClass$Inner;

Returns: The full name of the class like com.package.OuterClass.Inner (for both examples).

Definition at line 365 of file java_types.cpp.

◆ get_all_generic_parameters()

std::vector<java_generic_parametert> get_all_generic_parameters ( const typet & type )

Parameters

type	Source type

Returns: The vector of implicitly generic and (explicitly) generic type parameters of the given type.

Definition at line 924 of file java_types.cpp.

◆ get_array_dimension_field()

exprt get_array_dimension_field ( const exprt & pointer )

Parameters

pointer pointer to an array[reference] object

Returns: member expression to access its array dimension field

Definition at line 206 of file java_types.cpp.

◆ get_array_element_type_field()

exprt get_array_element_type_field ( const exprt & pointer )

Parameters

pointer pointer to an array[reference] object

Returns: member expression to access its array element_type field

Definition at line 218 of file java_types.cpp.

◆ 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

	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.

◆ 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

	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.

◆ get_dependencies_from_generic_parameters_rec()

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

Definition at line 948 of file java_types.cpp.

◆ is_java_array_tag()

bool is_java_array_tag ( const irep_idt & tag )

See above.

Parameters

tag	Tag of a struct

Returns: True if the given string is a Java array tag, i.e., has a prefix of java::array[

Definition at line 233 of file java_types.cpp.

◆ is_java_array_type()

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.

◆ is_multidim_java_array_type()

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.

◆ 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:

@java.lang.Object: of type struct {java.lang.Object} containing the base class data
length: of type Java integer - the length of the array
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

type A type that might represent a Java array

Returns
True if it is a Java array type, false otherwise

Definition at line 838 of file java_types.cpp.

◆ java_array_dimension_and_element_type()

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.

◆ java_array_element_type() [1/2]

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.

Parameters

array_symbol The java array type

Definition at line 144 of file java_types.cpp.

◆ java_array_element_type() [2/2]

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.

Parameters

array_symbol The java array type

Definition at line 154 of file java_types.cpp.

◆ java_array_type()

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.

Parameters

subtype Character indicating the type of array

Definition at line 109 of file java_types.cpp.

◆ java_boolean_type()

c_bool_typet java_boolean_type ( )

Definition at line 79 of file java_types.cpp.

◆ java_byte_type()

signedbv_typet java_byte_type ( )

Definition at line 55 of file java_types.cpp.

◆ java_bytecode_promotion() [1/2]

exprt java_bytecode_promotion ( const exprt & expr )

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

Definition at line 281 of file java_types.cpp.

◆ java_bytecode_promotion() [2/2]

typet java_bytecode_promotion ( const typet & type )

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

Definition at line 269 of file java_types.cpp.

◆ java_char_from_type()

char java_char_from_type ( const typet & type )

Definition at line 708 of file java_types.cpp.

◆ java_char_type()

unsignedbv_typet java_char_type ( )

Definition at line 61 of file java_types.cpp.

◆ java_classname()

struct_tag_typet java_classname ( const std::string & id )

Definition at line 809 of file java_types.cpp.

◆ java_double_type()

floatbv_typet java_double_type ( )

Definition at line 73 of file java_types.cpp.

◆ java_float_type()

floatbv_typet java_float_type ( )

Definition at line 67 of file java_types.cpp.

◆ 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 749 of file java_types.cpp.

◆ java_int_type()

signedbv_typet java_int_type ( )

Definition at line 31 of file java_types.cpp.

◆ java_lang_object_type()

java_reference_typet java_lang_object_type ( )

Definition at line 98 of file java_types.cpp.

◆ java_long_type()

signedbv_typet java_long_type ( )

Definition at line 43 of file java_types.cpp.

◆ java_reference_array_type()

java_reference_typet java_reference_array_type ( const struct_tag_typet & subtype )

Definition at line 541 of file java_types.cpp.

◆ java_reference_type() [1/2]

java_reference_typet java_reference_type ( const struct_tag_typet & subtype )

Definition at line 93 of file java_types.cpp.

◆ java_reference_type() [2/2]

reference_typet java_reference_type ( const typet & subtype )

Definition at line 88 of file java_types.cpp.

◆ java_short_type()

signedbv_typet java_short_type ( )

Definition at line 49 of file java_types.cpp.

◆ java_type_from_char()

typet java_type_from_char ( char t )

Constructs a type indicated by the given character:

i integer
l long
s short
b byte
c character
f float
d double
z boolean
a reference

Definition at line 248 of file java_types.cpp.

◆ java_type_from_string()

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.

Parameters

src	the string representation as used in the class file
class_name_prefix	name of class to append to generic type variables/parameters

Returns: internal type representation for GOTO programs

Definition at line 561 of file java_types.cpp.

◆ java_void_type()

empty_typet java_void_type ( )

Definition at line 37 of file java_types.cpp.

◆ 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

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 '>').

Returns: A vector of types that the string represents

Definition at line 392 of file java_types.cpp.

◆ parse_raw_list_types()

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.

Parameters

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 '>').

Returns: A vector of strings that represent the bytecode type.

Definition at line 419 of file java_types.cpp.

◆ pretty_java_type()

std::string pretty_java_type ( const typet & type )

Definition at line 1089 of file java_types.cpp.

◆ pretty_signature()

std::string pretty_signature ( const java_method_typet & method_type )

Definition at line 1131 of file java_types.cpp.

◆ slash_to_dot()

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

static

Definition at line 800 of file java_types.cpp.

Functions

Function Documentation

◆ add_generic_type_information()

◆ build_class_name()

◆ equal_java_types()

◆ erase_type_arguments()

◆ find_closing_semi_colon_for_reference_type()

◆ gather_full_class_name()

◆ get_all_generic_parameters()

◆ get_array_dimension_field()

◆ get_array_element_type_field()

◆ get_dependencies_from_generic_parameters() [1/2]

◆ get_dependencies_from_generic_parameters() [2/2]

◆ get_dependencies_from_generic_parameters_rec()

◆ is_java_array_tag()

◆ is_java_array_type()

◆ is_multidim_java_array_type()

◆ is_valid_java_array()

◆ java_array_dimension_and_element_type()

◆ java_array_element_type() [1/2]

◆ java_array_element_type() [2/2]

◆ java_array_type()

◆ java_boolean_type()

◆ java_byte_type()

◆ java_bytecode_promotion() [1/2]

◆ java_bytecode_promotion() [2/2]

◆ java_char_from_type()

◆ java_char_type()

◆ java_classname()

◆ java_double_type()

◆ java_float_type()

◆ java_generic_type_from_string()

◆ java_int_type()

◆ java_lang_object_type()

◆ java_long_type()

◆ java_reference_array_type()

◆ java_reference_type() [1/2]

◆ java_reference_type() [2/2]

◆ java_short_type()

◆ java_type_from_char()

◆ java_type_from_string()

◆ java_void_type()

◆ parse_list_types()

◆ parse_raw_list_types()

◆ pretty_java_type()

◆ pretty_signature()

◆ slash_to_dot()