JAVA Bytecode Language Conversion. More...

#include "java_bytecode_convert_method.h"
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_types.h"
#include "java_utils.h"
#include "remove_exceptions.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <util/string_constant.h>
#include <util/threeval.h>
#include <goto-programs/cfg.h>
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/resolve_inherited_component.h>
#include <analyses/cfg_dominators.h>
#include <analyses/uncaught_exceptions_analysis.h>
#include <limits>
#include <algorithm>
#include <functional>
#include <unordered_set>
#include <regex>

Include dependency graph for java_bytecode_convert_method.cpp:

Go to the source code of this file.

Classes
class	patternt
	Given a string of the format '?blah?', will return true when compared against a string that matches appart from any characters that are '?' in the original string. More...

Functions
static void	assign_parameter_names (java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
	Iterates through the parameters of the function type `ftype`, finds a new new name for each parameter and renames them in `ftype.parameters()` as well as in the `symbol_table`. More...

static bool	operator== (const irep_idt &what, const patternt &pattern)

static bool	is_constructor (const irep_idt &method_name)

java_method_typet	member_type_lazy (const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler)
	Returns the member type for a method, based on signature or descriptor. More...

void	java_bytecode_convert_method_lazy (const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler)
	This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More...

static irep_idt	get_if_cmp_operator (const irep_idt &stmt)

static member_exprt	to_member (const exprt &pointer, const exprt &fieldref)

static void	gather_symbol_live_ranges (java_bytecode_convert_methodt::method_offsett pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)

static std::size_t	get_bytecode_type_width (const typet &ty)

void	java_bytecode_initialize_parameter_names (symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
	This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode. More...

void	java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.cpp.

Function Documentation

◆ assign_parameter_names()

static void assign_parameter_names	(	java_method_typet &	ftype,
		const irep_idt &	name_prefix,
		symbol_table_baset &	symbol_table
	)

static

Iterates through the parameters of the function type ftype, finds a new new name for each parameter and renames them in ftype.parameters() as well as in the symbol_table.

Parameters

[in,out]	ftype	Function type whose parameters should be named.
	name_prefix	Prefix for parameter names, typically the parent function's name.
[in,out]	symbol_table	Global symbol table.

Returns: Assigns parameter names (side-effects on ftype) to function stub parameters, which are initially nameless as method conversion hasn't happened. Also creates symbols in symbol_table.

Definition at line 89 of file java_bytecode_convert_method.cpp.

◆ gather_symbol_live_ranges()

static void gather_symbol_live_ranges	(	java_bytecode_convert_methodt::method_offsett	pc,
		const exprt &	e,
		std::map< irep_idt, java_bytecode_convert_methodt::variablet > &	result
	)

static

Definition at line 927 of file java_bytecode_convert_method.cpp.

◆ get_bytecode_type_width()

static std::size_t get_bytecode_type_width ( const typet & ty )

static

Definition at line 984 of file java_bytecode_convert_method.cpp.

◆ get_if_cmp_operator()

static irep_idt get_if_cmp_operator ( const irep_idt & stmt )

static

Definition at line 638 of file java_bytecode_convert_method.cpp.

◆ is_constructor()

static bool is_constructor ( const irep_idt & method_name )

static

Definition at line 126 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_convert_method()

void java_bytecode_convert_method	(	const symbolt &	class_symbol,
		const java_bytecode_parse_treet::methodt &	method,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		size_t	max_array_length,
		bool	throw_assertion_error,
		optionalt< ci_lazy_methods_neededt >	needed_lazy_methods,
		java_string_library_preprocesst &	string_preprocess,
		const class_hierarchyt &	class_hierarchy,
		bool	threading_support
	)

Definition at line 3065 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_convert_method_lazy()

void java_bytecode_convert_method_lazy	(	const symbolt &	class_symbol,
		const irep_idt &	method_identifier,
		const java_bytecode_parse_treet::methodt &	m,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.

The caller should call java_bytecode_convert_method later to give the symbol/method a body.

Parameters

class_symbol	The class this method belongs to
method_identifier	The fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)")
m	The parsed method object to convert.
symbol_table	The global symbol table (will be modified).
message_handler	A message handler to collect warnings.

Definition at line 337 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_initialize_parameter_names()

void java_bytecode_initialize_parameter_names	(	symbolt &	method_symbol,
		const java_bytecode_parse_treet::methodt::local_variable_tablet &	local_variable_table,
		symbol_table_baset &	symbol_table
	)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode.

Remarks: This is useful for pre-initialization for methods generated by the string solver

Parameters

method_symbol	The symbol for the method for which to initialize the parameters
local_variable_table	The local variable table containing the bytecode for the parameters
symbol_table	The symbol table into which to insert symbols for the parameters

Definition at line 2987 of file java_bytecode_convert_method.cpp.

◆ member_type_lazy()

java_method_typet member_type_lazy	(	const std::string &	descriptor,
		const optionalt< std::string > &	signature,
		const std::string &	class_name,
		const std::string &	method_name,
		message_handlert &	message_handler
	)

Returns the member type for a method, based on signature or descriptor.

Parameters

descriptor	descriptor of the method
signature	signature of the method
class_name	string containing the name of the corresponding class
method_name	string containing the name of the method
message_handler	message handler to collect warnings

Returns: the constructed member type

Definition at line 255 of file java_bytecode_convert_method.cpp.

◆ operator==()

static bool operator==	(	const irep_idt &	what,
		const patternt &	pattern
	)

static

Definition at line 121 of file java_bytecode_convert_method.cpp.

◆ to_member()

static member_exprt to_member	(	const exprt &	pointer,
		const exprt &	fieldref
	)

static

Definition at line 656 of file java_bytecode_convert_method.cpp.

Classes

Functions

Detailed Description

Function Documentation

◆ assign_parameter_names()

◆ gather_symbol_live_ranges()

◆ get_bytecode_type_width()

◆ get_if_cmp_operator()

◆ is_constructor()

◆ java_bytecode_convert_method()

◆ java_bytecode_convert_method_lazy()

◆ java_bytecode_initialize_parameter_names()

◆ member_type_lazy()

◆ operator==()

◆ to_member()