#include "java_bytecode_convert_class.h"
#include "ci_lazy_methods.h"
#include "java_bytecode_convert_method.h"
#include "java_root_class.h"
#include "java_types.h"
#include "java_utils.h"
#include <util/arith_tools.h>
#include <util/expr_initializer.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/std_expr.h>

Include dependency graph for java_bytecode_convert_class.cpp:

Classes
class	java_bytecode_convert_classt

Functions
static optionalt< std::string >	extract_generic_superclass_reference (const optionalt< std::string > &signature)
	Auxiliary function to extract the generic superclass reference from the class signature. More...

static optionalt< std::string >	extract_generic_interface_reference (const optionalt< std::string > &signature, const std::string &interface_name)
	Auxiliary function to extract the generic interface reference of an interface with the specified name from the class signature. More...

void	add_java_array_types (symbol_tablet &symbol_table)
	Register in the `symbol_table` new symbols for the objects java::array[X] where X is byte, short, int, long, char, boolean, float, double and reference. More...

bool	java_bytecode_convert_class (const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &string_preprocess, const std::unordered_set< std::string > &no_load_classes)
	See class java_bytecode_convert_classt. More...

static std::string	get_final_name_component (const std::string &name)

static std::string	get_without_final_name_component (const std::string &name)

static void	find_and_replace_parameter (java_generic_parametert &parameter, const std::vector< java_generic_parametert > &replacement_parameters)
	For a given generic type parameter, check if there is a parameter in the given vector of replacement parameters with a matching name. More...

static void	find_and_replace_parameters (typet &type, const std::vector< java_generic_parametert > &replacement_parameters)
	Recursively find all generic type parameters of a given type and replace their identifiers if matching replacement parameter exist. More...

void	convert_annotations (const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
	Convert parsed annotations into the symbol table. More...

void	convert_java_annotations (const std::vector< java_annotationt > &java_annotations, java_bytecode_parse_treet::annotationst &annotations)
	Convert java annotations, e.g. More...

void	mark_java_implicitly_generic_class_type (const irep_idt &class_name, symbol_tablet &symbol_table)
	Checks if the class is implicitly generic, i.e., it is an inner class of any generic class. More...

Detailed Description

JAVA Bytecode Language Conversion

Definition in file java_bytecode_convert_class.cpp.

Function Documentation

◆ add_java_array_types()

void add_java_array_types ( symbol_tablet & symbol_table )

Register in the symbol_table new symbols for the objects java::array[X] where X is byte, short, int, long, char, boolean, float, double and reference.

Also registers a java::array[X].clone():Ljava/lang/Object; method for each type.

Definition at line 793 of file java_bytecode_convert_class.cpp.

◆ convert_annotations()

void convert_annotations	(	const java_bytecode_parse_treet::annotationst &	parsed_annotations,
		std::vector< java_annotationt > &	java_annotations
	)

Convert parsed annotations into the symbol table.

Parameters

parsed_annotations	The parsed annotations to convert
java_annotations	The java_annotationt collection to populate

Definition at line 1141 of file java_bytecode_convert_class.cpp.

◆ convert_java_annotations()

void convert_java_annotations	(	const std::vector< java_annotationt > &	java_annotations,
		java_bytecode_parse_treet::annotationst &	annotations
	)

Convert java annotations, e.g.

as retrieved from the symbol table, back to type annotationt (inverse of convert_annotations())

Parameters

java_annotations	The java_annotationt collection to convert
annotations	The annotationt collection to populate

Definition at line 1164 of file java_bytecode_convert_class.cpp.

◆ extract_generic_interface_reference()

static optionalt<std::string> extract_generic_interface_reference	(	const optionalt< std::string > &	signature,
		const std::string &	interface_name
	)

static

Auxiliary function to extract the generic interface reference of an interface with the specified name from the class signature.

If the signature is empty or the interface is not generic it returns empty. Example:

class: A<T> extends B<T, Integer> implements C, D<T>
signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
returned interface reference for C: LC;
returned interface reference for D: LD<TT;>;
Parameters

signature Signature of the class

interface_name The interface name

Returns
Reference of the generic interface, or empty if the interface is not generic

Definition at line 226 of file java_bytecode_convert_class.cpp.

◆ extract_generic_superclass_reference()

static optionalt<std::string> extract_generic_superclass_reference ( const optionalt< std::string > & signature )

static

Auxiliary function to extract the generic superclass reference from the class signature.

If the signature is empty or the superclass is not generic it returns empty. Example:

class: A<T> extends B<T, Integer> implements C, D<T>
signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
returned superclass reference: B<TT;Ljava/lang/Integer;>;
Parameters

signature Signature of the class

Returns
Reference of the generic superclass, or empty if the superclass is not generic

Definition at line 187 of file java_bytecode_convert_class.cpp.

◆ find_and_replace_parameter()

static void find_and_replace_parameter	(	java_generic_parametert &	parameter,
		const std::vector< java_generic_parametert > &	replacement_parameters
	)

static

For a given generic type parameter, check if there is a parameter in the given vector of replacement parameters with a matching name.

If yes, replace the identifier of the parameter at hand by the identifier of the matching parameter. Example: if parameter has identifier java::Outer$Inner::T and there is a replacement parameter with identifier java::Outer::T, the identifier of parameter gets set to java::Outer::T.

Parameters

parameter	The given generic type parameter
replacement_parameters	vector of generic parameters (only viable ones, i.e., only those that can actually appear here such as generic parameters of outer classes of the class specified by the prefix of `parameter` identifier)

Definition at line 1068 of file java_bytecode_convert_class.cpp.

◆ find_and_replace_parameters()

static void find_and_replace_parameters	(	typet &	type,
		const std::vector< java_generic_parametert > &	replacement_parameters
	)

static

Recursively find all generic type parameters of a given type and replace their identifiers if matching replacement parameter exist.

Example: class Outer<T> has an inner class Inner that has a field t of type Generic<T>. This function ensures that the parameter points to java::Outer::T instead of java::Outer$Inner::T.

Definition at line 1107 of file java_bytecode_convert_class.cpp.

◆ get_final_name_component()

static std::string get_final_name_component ( const std::string & name )

static

Definition at line 1046 of file java_bytecode_convert_class.cpp.

◆ get_without_final_name_component()

static std::string get_without_final_name_component ( const std::string & name )

static

Definition at line 1051 of file java_bytecode_convert_class.cpp.

◆ java_bytecode_convert_class()

bool java_bytecode_convert_class	(	const java_class_loadert::parse_tree_with_overlayst &	parse_trees,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler,
		size_t	max_array_length,
		method_bytecodet &	method_bytecode,
		java_string_library_preprocesst &	string_preprocess,
		const std::unordered_set< std::string > &	no_load_classes
	)

See class java_bytecode_convert_classt.

Definition at line 1004 of file java_bytecode_convert_class.cpp.

◆ mark_java_implicitly_generic_class_type()

void mark_java_implicitly_generic_class_type	(	const irep_idt &	class_name,
		symbol_tablet &	symbol_table
	)

Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.

All uses of the implicit generic type parameters within the inner class are updated to point to the type parameters of the corresponding outer classes.

Definition at line 1189 of file java_bytecode_convert_class.cpp.

signature	Signature of the class
interface_name	The interface name

Classes

Functions

Detailed Description

Function Documentation

◆ add_java_array_types()

◆ convert_annotations()

◆ convert_java_annotations()

◆ extract_generic_interface_reference()

◆ extract_generic_superclass_reference()

◆ find_and_replace_parameter()

◆ find_and_replace_parameters()

◆ get_final_name_component()

◆ get_without_final_name_component()

◆ java_bytecode_convert_class()

◆ mark_java_implicitly_generic_class_type()