#include <java_bytecode_convert_method_class.h>

Collaboration diagram for java_bytecode_convert_methodt:

Classes
struct	block_tree_nodet

struct	converted_instructiont

struct	holet

struct	local_variable_with_holest

struct	method_with_amapt

class	variablet

Public Member Functions
	java_bytecode_convert_methodt (symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, bool assert_no_exceptions_thrown)

void	operator() (const symbolt &class_symbol, const methodt &method, const std::optional< prefix_filtert > &method_context)

Protected Types
enum	instruction_sizet { INST_INDEX = 2 , INST_INDEX_CONST = 3 }

enum	variable_cast_argumentt { CAST_AS_NEEDED , NO_CAST }

enum class	bytecode_write_typet { VARIABLE , ARRAY_REF , STATIC_FIELD , FIELD }

typedef std::vector< variablet >	variablest

typedef std::vector< exprt >	stackt

Protected Member Functions
const variablet &	find_variable_for_slot (size_t address, variablest &var_list)
	See above.

exprt	variable (const exprt &arg, char type_char, size_t address)
	Returns an expression indicating a local variable suitable to load/store from a bytecode at address `address` a value of type `type_char` stored in the JVM's slot `arg`.

symbol_exprt	tmp_variable (const std::string &prefix, const typet &type)

exprt::operandst	pop (std::size_t n)

void	pop_residue (std::size_t n)
	removes minimum(n, stack.size()) elements from the stack

void	push (const exprt::operandst &o)

bool	is_parameter (const local_variablet &v)
	Returns true iff the slot index of the local variable of a method (coming from the LVT) is a parameter of that method.

void	find_initializers (local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
	See `find_initializers_for_slot` above for more detail.

void	find_initializers_for_slot (local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)
	Given a sequence of users of the same local variable slot, this figures out which ones are related by control flow, and combines them into a single entry with holes, such that after combination we can create a single GOTO variable per variable table entry, placed at the live range's start address, which may be moved back so that the declaration dominates all uses.

void	setup_local_variables (const methodt &m, const address_mapt &amap)
	See `find_initializers_for_slot` above for more detail.

code_blockt &	get_block_for_pcrange (block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address)
	'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are both trees with the same shape).

code_blockt &	get_or_create_block_for_pcrange (block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge=true)
	As above, but this version can additionally create a new branch in the block_tree-node and code_blockt trees to envelop the requested address range.

void	convert (const symbolt &class_symbol, const methodt &, const std::optional< prefix_filtert > &method_context)

code_blockt	convert_parameter_annotations (const methodt &method, const java_method_typet &method_type)

code_blockt	convert_instructions (const methodt &)

codet	get_clinit_call (const irep_idt &classname)
	Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check.

bool	is_method_inherited (const irep_idt &classname, const irep_idt &mangled_method_name) const
	Returns true iff method `methodid` from class `classname` is a method inherited from a class or interface from which `classname` inherits, either directly or indirectly.

irep_idt	get_static_field (const irep_idt &class_identifier, const irep_idt &component_name) const
	Get static field identifier referred to by `class_identifier.component_name` Note this may be inherited from either a parent or an interface.

void	save_stack_entries (const std::string &, code_blockt &, const bytecode_write_typet, const irep_idt &)
	Create temporary variables if a write instruction can have undesired side- effects.

void	create_stack_tmp_var (const std::string &, const typet &, code_blockt &, exprt &)
	actually create a temporary variable to hold the value of a stack entry

std::vector< method_offsett >	try_catch_handler (method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const

void	draw_edges_from_ret_to_jsr (address_mapt &address_map, const std::vector< method_offsett > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const

std::optional< exprt >	convert_invoke_dynamic (const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code)

code_blockt	convert_astore (const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)

code_blockt	convert_store (const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)

exprt	convert_load (const exprt &index, char type_char, size_t address)
	Load reference from local variable.

code_blockt	convert_ret (const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)

code_ifthenelset	convert_if_cmp (const java_bytecode_convert_methodt::address_mapt &address_map, const u1 bytecode, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const

code_ifthenelset	convert_if (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const

code_ifthenelset	convert_ifnonull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const

code_ifthenelset	convert_ifnull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const

code_blockt	convert_iinc (const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)

exprt::operandst &	convert_shl (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const

exprt::operandst &	convert_ushr (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const

exprt::operandst &	convert_cmp (const exprt::operandst &op, exprt::operandst &results) const

exprt::operandst &	convert_cmp2 (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const

void	convert_getstatic (const source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)

code_blockt	convert_putfield (const fieldref_exprt &arg0, const exprt::operandst &op)

code_blockt	convert_putstatic (const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)

void	convert_new (const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)

code_blockt	convert_newarray (const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)

code_blockt	convert_multianewarray (const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)

codet &	do_exception_handling (const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)

void	convert_athrow (const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const

void	convert_checkcast (const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const

codet	convert_monitorenterexit (const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)

codet &	replace_call_to_cprover_assume (source_locationt location, codet &c)

void	convert_invoke (source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results)

exprt::operandst &	convert_const (const irep_idt &statement, const constant_exprt &arg0, exprt::operandst &results) const

void	convert_dup2_x2 (exprt::operandst &op, exprt::operandst &results)

void	convert_dup2_x1 (exprt::operandst &op, exprt::operandst &results)

void	convert_dup2 (exprt::operandst &op, exprt::operandst &results)

code_switcht	convert_switch (const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)

codet	convert_pop (const irep_idt &statement, const exprt::operandst &op)

Static Protected Member Functions
static irep_idt	label (const irep_idt &address)

static void	replace_goto_target (codet &repl, const irep_idt &old_label, const irep_idt &new_label)
	Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.

static exprt	convert_aload (const irep_idt &statement, const exprt::operandst &op)

Protected Attributes
messaget	log

symbol_table_baset &	symbol_table

namespacet	ns

const size_t	max_array_length

const bool	throw_assertion_error

const bool	assert_no_exceptions_thrown

const bool	threading_support

std::optional< ci_lazy_methods_neededt >	needed_lazy_methods

irep_idt	method_id
	Fully qualified name of the method under translation.

irep_idt	current_method
	A copy of `method_id` :/.

typet	method_return_type
	Return type of the method under conversion.

java_string_library_preprocesst &	string_preprocess

method_offsett	slots_for_parameters
	Number of local variable slots used by the JVM to pass parameters upon invocation of the method under translation.

expanding_vectort< variablest >	variables

std::set< symbol_exprt >	used_local_names

bool	method_has_this

std::map< irep_idt, bool >	class_has_clinit_method

std::map< irep_idt, bool >	any_superclass_has_clinit_method

const class_hierarchyt &	class_hierarchy

std::list< symbol_exprt >	tmp_vars

stackt	stack

Friends
class	java_bytecode_convert_method_unit_testt

Detailed Description

Definition at line 35 of file java_bytecode_convert_method_class.h.

Member Typedef Documentation

◆ address_mapt

typedef std::map<method_offsett, converted_instructiont> java_bytecode_convert_methodt::address_mapt

Definition at line 242 of file java_bytecode_convert_method_class.h.

◆ instructionst

typedef methodt::instructionst java_bytecode_convert_methodt::instructionst

Definition at line 65 of file java_bytecode_convert_method_class.h.

◆ instructiont

typedef java_bytecode_parse_treet::instructiont java_bytecode_convert_methodt::instructiont

Definition at line 64 of file java_bytecode_convert_method_class.h.

◆ java_cfg_dominatorst

typedef cfg_dominators_templatet<method_with_amapt, method_offsett, false> java_bytecode_convert_methodt::java_cfg_dominatorst

Definition at line 261 of file java_bytecode_convert_method_class.h.

◆ local_variable_table_with_holest

typedef std::vector<local_variable_with_holest> java_bytecode_convert_methodt::local_variable_table_with_holest

Definition at line 123 of file java_bytecode_convert_method_class.h.

◆ local_variable_tablet

typedef methodt::local_variable_tablet java_bytecode_convert_methodt::local_variable_tablet

Definition at line 66 of file java_bytecode_convert_method_class.h.

◆ local_variablet

typedef methodt::local_variablet java_bytecode_convert_methodt::local_variablet

Definition at line 67 of file java_bytecode_convert_method_class.h.

◆ method_offsett

typedef uint16_t java_bytecode_convert_methodt::method_offsett

Definition at line 77 of file java_bytecode_convert_method_class.h.

◆ methodt

typedef java_bytecode_parse_treet::methodt java_bytecode_convert_methodt::methodt

Definition at line 63 of file java_bytecode_convert_method_class.h.

◆ stackt

typedef std::vector<exprt> java_bytecode_convert_methodt::stackt

protected

Definition at line 207 of file java_bytecode_convert_method_class.h.

◆ variablest

typedef std::vector<variablet> java_bytecode_convert_methodt::variablest

protected

Definition at line 170 of file java_bytecode_convert_method_class.h.

Member Enumeration Documentation

◆ bytecode_write_typet

enum class java_bytecode_convert_methodt::bytecode_write_typet

strongprotected

Enumerator
VARIABLE
ARRAY_REF
STATIC_FIELD
FIELD

Definition at line 339 of file java_bytecode_convert_method_class.h.

◆ instruction_sizet

enum java_bytecode_convert_methodt::instruction_sizet

protected

Enumerator
INST_INDEX
INST_INDEX_CONST

Definition at line 178 of file java_bytecode_convert_method_class.h.

◆ variable_cast_argumentt

enum java_bytecode_convert_methodt::variable_cast_argumentt

protected

Enumerator
CAST_AS_NEEDED
NO_CAST

Definition at line 190 of file java_bytecode_convert_method_class.h.

Constructor & Destructor Documentation

◆ java_bytecode_convert_methodt()

java_bytecode_convert_methodt::java_bytecode_convert_methodt	(	symbol_table_baset &	symbol_table,
		message_handlert &	_message_handler,
		size_t	_max_array_length,
		bool	throw_assertion_error,
		std::optional< ci_lazy_methods_neededt >	needed_lazy_methods,
		java_string_library_preprocesst &	_string_preprocess,
		const class_hierarchyt &	class_hierarchy,
		bool	threading_support,
		bool	assert_no_exceptions_thrown
	)

inline

Definition at line 38 of file java_bytecode_convert_method_class.h.

Member Function Documentation

◆ convert()

void java_bytecode_convert_methodt::convert	(	const symbolt &	class_symbol,
		const methodt &	m,
		const std::optional< prefix_filtert > &	method_context
	)

protected

Definition at line 534 of file java_bytecode_convert_method.cpp.

◆ convert_aload()

exprt java_bytecode_convert_methodt::convert_aload	(	const irep_idt &	statement,
		const exprt::operandst &	op
	)

staticprotected

Definition at line 2993 of file java_bytecode_convert_method.cpp.

◆ convert_astore()

code_blockt java_bytecode_convert_methodt::convert_astore	(	const irep_idt &	statement,
		const exprt::operandst &	op,
		const source_locationt &	location
	)

protected

Definition at line 3059 of file java_bytecode_convert_method.cpp.

◆ convert_athrow()

void java_bytecode_convert_methodt::convert_athrow	(	const source_locationt &	location,
		const exprt::operandst &	op,
		codet &	c,
		exprt::operandst &	results
	)		const

protected

Definition at line 2423 of file java_bytecode_convert_method.cpp.

◆ convert_checkcast()

void java_bytecode_convert_methodt::convert_checkcast	(	const exprt &	arg0,
		const exprt::operandst &	op,
		codet &	c,
		exprt::operandst &	results
	)		const

protected

Definition at line 2407 of file java_bytecode_convert_method.cpp.

◆ convert_cmp()

exprt::operandst & java_bytecode_convert_methodt::convert_cmp	(	const exprt::operandst &	op,
		exprt::operandst &	results
	)		const

protected

Definition at line 2767 of file java_bytecode_convert_method.cpp.

◆ convert_cmp2()

exprt::operandst & java_bytecode_convert_methodt::convert_cmp2	(	const irep_idt &	statement,
		const exprt::operandst &	op,
		exprt::operandst &	results
	)		const

protected

Definition at line 2739 of file java_bytecode_convert_method.cpp.

◆ convert_const()

exprt::operandst & java_bytecode_convert_methodt::convert_const	(	const irep_idt &	statement,
		const constant_exprt &	arg0,
		exprt::operandst &	results
	)		const

protected

Definition at line 2169 of file java_bytecode_convert_method.cpp.

◆ convert_dup2()

void java_bytecode_convert_methodt::convert_dup2	(	exprt::operandst &	op,
		exprt::operandst &	results
	)

protected

Definition at line 2122 of file java_bytecode_convert_method.cpp.

◆ convert_dup2_x1()

void java_bytecode_convert_methodt::convert_dup2_x1	(	exprt::operandst &	op,
		exprt::operandst &	results
	)

protected

Definition at line 2135 of file java_bytecode_convert_method.cpp.

◆ convert_dup2_x2()

void java_bytecode_convert_methodt::convert_dup2_x2	(	exprt::operandst &	op,
		exprt::operandst &	results
	)

protected

Definition at line 2148 of file java_bytecode_convert_method.cpp.

◆ convert_getstatic()

void java_bytecode_convert_methodt::convert_getstatic	(	const source_locationt &	source_location,
		const exprt &	arg0,
		const symbol_exprt &	symbol_expr,
		bool	is_assertions_disabled_field,
		codet &	c,
		exprt::operandst &	results
	)

protected

Definition at line 2693 of file java_bytecode_convert_method.cpp.

◆ convert_if()

code_ifthenelset java_bytecode_convert_methodt::convert_if	(	const java_bytecode_convert_methodt::address_mapt &	address_map,
		const exprt::operandst &	op,
		const irep_idt &	id,
		const mp_integer &	number,
		const source_locationt &	location
	)		const

protected

Definition at line 2896 of file java_bytecode_convert_method.cpp.

◆ convert_if_cmp()

code_ifthenelset java_bytecode_convert_methodt::convert_if_cmp	(	const java_bytecode_convert_methodt::address_mapt &	address_map,
		const u1	bytecode,
		const exprt::operandst &	op,
		const mp_integer &	number,
		const source_locationt &	location
	)		const

protected

Definition at line 2920 of file java_bytecode_convert_method.cpp.

◆ convert_ifnonull()

code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull	(	const java_bytecode_convert_methodt::address_mapt &	address_map,
		const exprt::operandst &	op,
		const mp_integer &	number,
		const source_locationt &	location
	)		const

protected

Definition at line 2874 of file java_bytecode_convert_method.cpp.

◆ convert_ifnull()

code_ifthenelset java_bytecode_convert_methodt::convert_ifnull	(	const java_bytecode_convert_methodt::address_mapt &	address_map,
		const exprt::operandst &	op,
		const mp_integer &	number,
		const source_locationt &	location
	)		const

protected

Definition at line 2852 of file java_bytecode_convert_method.cpp.

◆ convert_iinc()

code_blockt java_bytecode_convert_methodt::convert_iinc	(	const exprt &	arg0,
		const exprt &	arg1,
		const source_locationt &	location,
		method_offsett	address
	)

protected

Definition at line 2823 of file java_bytecode_convert_method.cpp.

◆ convert_instructions()

code_blockt java_bytecode_convert_methodt::convert_instructions ( const methodt & method )

protected

Definition at line 1055 of file java_bytecode_convert_method.cpp.

◆ convert_invoke()

void java_bytecode_convert_methodt::convert_invoke	(	source_locationt	location,
		const irep_idt &	statement,
		class_method_descriptor_exprt &	class_method_descriptor,
		codet &	c,
		exprt::operandst &	results
	)

protected

Definition at line 2231 of file java_bytecode_convert_method.cpp.

◆ convert_invoke_dynamic()

std::optional< exprt > java_bytecode_convert_methodt::convert_invoke_dynamic	(	const source_locationt &	location,
		std::size_t	instruction_address,
		const exprt &	arg0,
		codet &	result_code
	)

protected

Definition at line 3089 of file java_bytecode_convert_method.cpp.

◆ convert_load()

exprt java_bytecode_convert_methodt::convert_load	(	const exprt &	index,
		char	type_char,
		size_t	address
	)

protected

Load reference from local variable.

index must be an unsigned byte and an index in the local variable array of the current frame. The type of the local variable at index index must:

be a reference type if type_char is 'a'
be either boolean, byte, short, int, or char if type_char is 'i', a typecast to int is added if needed
match java_type_of_char(type_char) otherwise
Returns
the local variable at index

Definition at line 3013 of file java_bytecode_convert_method.cpp.

◆ convert_monitorenterexit()

codet java_bytecode_convert_methodt::convert_monitorenterexit	(	const irep_idt &	statement,
		const exprt::operandst &	op,
		const source_locationt &	source_location
	)

protected

Definition at line 2099 of file java_bytecode_convert_method.cpp.

◆ convert_multianewarray()

code_blockt java_bytecode_convert_methodt::convert_multianewarray	(	const source_locationt &	location,
		const exprt &	arg0,
		const exprt::operandst &	op,
		exprt::operandst &	results
	)

protected

Definition at line 2542 of file java_bytecode_convert_method.cpp.

◆ convert_new()

void java_bytecode_convert_methodt::convert_new	(	const source_locationt &	location,
		const exprt &	arg0,
		codet &	c,
		exprt::operandst &	results
	)

protected

Definition at line 2627 of file java_bytecode_convert_method.cpp.

◆ convert_newarray()

code_blockt java_bytecode_convert_methodt::convert_newarray	(	const source_locationt &	location,
		const irep_idt &	statement,
		const exprt &	arg0,
		const exprt::operandst &	op,
		exprt::operandst &	results
	)

protected

Definition at line 2569 of file java_bytecode_convert_method.cpp.

◆ convert_parameter_annotations()

code_blockt java_bytecode_convert_methodt::convert_parameter_annotations	(	const methodt &	method,
		const java_method_typet &	method_type
	)

protected

Definition at line 1006 of file java_bytecode_convert_method.cpp.

◆ convert_pop()

codet java_bytecode_convert_methodt::convert_pop	(	const irep_idt &	statement,
		const exprt::operandst &	op
	)

protected

Definition at line 2033 of file java_bytecode_convert_method.cpp.

◆ convert_putfield()

code_blockt java_bytecode_convert_methodt::convert_putfield	(	const fieldref_exprt &	arg0,
		const exprt::operandst &	op
	)

protected

Definition at line 2682 of file java_bytecode_convert_method.cpp.

◆ convert_putstatic()

code_blockt java_bytecode_convert_methodt::convert_putstatic	(	const source_locationt &	location,
		const exprt &	arg0,
		const exprt::operandst &	op,
		const symbol_exprt &	symbol_expr
	)

protected

Definition at line 2651 of file java_bytecode_convert_method.cpp.

◆ convert_ret()

code_blockt java_bytecode_convert_methodt::convert_ret	(	const std::vector< method_offsett > &	jsr_ret_targets,
		const exprt &	arg0,
		const source_locationt &	location,
		const method_offsett	address
	)

protected

Definition at line 2944 of file java_bytecode_convert_method.cpp.

◆ convert_shl()

exprt::operandst & java_bytecode_convert_methodt::convert_shl	(	const irep_idt &	statement,
		const exprt::operandst &	op,
		exprt::operandst &	results
	)		const

protected

Definition at line 2787 of file java_bytecode_convert_method.cpp.

◆ convert_store()

code_blockt java_bytecode_convert_methodt::convert_store	(	const irep_idt &	statement,
		const exprt &	arg0,
		const exprt::operandst &	op,
		const method_offsett	address,
		const source_locationt &	location
	)

protected

Definition at line 3034 of file java_bytecode_convert_method.cpp.

◆ convert_switch()

code_switcht java_bytecode_convert_methodt::convert_switch	(	const exprt::operandst &	op,
		const java_bytecode_parse_treet::instructiont::argst &	args,
		const source_locationt &	location
	)

protected

Definition at line 2049 of file java_bytecode_convert_method.cpp.

◆ convert_ushr()

exprt::operandst & java_bytecode_convert_methodt::convert_ushr	(	const irep_idt &	statement,
		const exprt::operandst &	op,
		exprt::operandst &	results
	)		const

protected

Definition at line 2804 of file java_bytecode_convert_method.cpp.

◆ create_stack_tmp_var()

void java_bytecode_convert_methodt::create_stack_tmp_var	(	const std::string &	tmp_var_prefix,
		const typet &	tmp_var_type,
		code_blockt &	block,
		exprt &	stack_entry
	)

protected

actually create a temporary variable to hold the value of a stack entry

Definition at line 3431 of file java_bytecode_convert_method.cpp.

◆ do_exception_handling()

codet & java_bytecode_convert_methodt::do_exception_handling	(	const methodt &	method,
		const std::set< method_offsett > &	working_set,
		method_offsett	cur_pc,
		codet &	c
	)

protected

Definition at line 2461 of file java_bytecode_convert_method.cpp.

◆ draw_edges_from_ret_to_jsr()

void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr	(	java_bytecode_convert_methodt::address_mapt &	address_map,
		const std::vector< method_offsett > &	jsr_ret_targets,
		const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &	ret_instructions
	)		const

protected

Definition at line 3160 of file java_bytecode_convert_method.cpp.

◆ find_initializers()

void java_bytecode_convert_methodt::find_initializers	(	local_variable_table_with_holest &	vars,
		const address_mapt &	amap,
		const java_cfg_dominatorst &	dominator_analysis
	)

protected

See find_initializers_for_slot above for more detail.

Combines entries in vars which flow together.

Parameters

vars	Local variable table
amap	Map from bytecode index to instruction
dominator_analysis	Already computed dominator tree for the Java function described by `amap`

Definition at line 691 of file java_local_variable_table.cpp.

◆ find_initializers_for_slot()

void java_bytecode_convert_methodt::find_initializers_for_slot	(	local_variable_table_with_holest::iterator	firstvar,
		local_variable_table_with_holest::iterator	varlimit,
		const address_mapt &	amap,
		const java_cfg_dominatorst &	dominator_analysis
	)

protected

Given a sequence of users of the same local variable slot, this figures out which ones are related by control flow, and combines them into a single entry with holes, such that after combination we can create a single GOTO variable per variable table entry, placed at the live range's start address, which may be moved back so that the declaration dominates all uses.

Side-effect: merges variable table entries which flow into one another (e.g. there are branches from one live range to another without re-initializing the local slot).

Parameters

firstvar	start of sequence of variable table entries, all of which should concern the same slot index.
varlimit	end of sequence of variable table entries
amap	map from bytecode address to instruction
dominator_analysis	already-calculated dominator tree

Definition at line 597 of file java_local_variable_table.cpp.

◆ find_variable_for_slot()

const java_bytecode_convert_methodt::variablet & java_bytecode_convert_methodt::find_variable_for_slot	(	size_t	address,
		variablest &	var_list
	)

protected

See above.

Parameters

address	Address to find a variable table entry for
var_list	List of candidates that use the slot we're interested in

Returns: Returns the list entry covering this address (taking live range holes into account), or creates/returns an anonymous variable entry if nothing covers address.

Definition at line 852 of file java_local_variable_table.cpp.

◆ get_block_for_pcrange()

code_blockt & java_bytecode_convert_methodt::get_block_for_pcrange	(	block_tree_nodet &	tree,
		code_blockt &	this_block,
		method_offsett	address_start,
		method_offsett	address_limit,
		method_offsett	next_block_start_address
	)

protected

'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are both trees with the same shape).

The caller is looking for the single block in the tree that most closely encloses bytecode address range [address_start,address_limit). 'next_block_start_address' is the start address of 'tree's successor sibling and is used to determine when the range spans out of its bounds.

Parameters

tree	A code block descriptor.
this_block	The corresponding actual code_blockt.
address_start	the Java bytecode offsets searched for.
address_limit	the Java bytecode offsets searched for.
next_block_start_address	The bytecode offset of tree/this_block's successor sibling, or UINT_MAX if none exists.

Returns: Returns the code_blockt most closely enclosing the given address range.

Definition at line 729 of file java_bytecode_convert_method.cpp.

◆ get_clinit_call()

codet java_bytecode_convert_methodt::get_clinit_call ( const irep_idt & classname )

protected

Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check.

Parameters

classname Class name

Returns: Returns a function call to the given class' static initializer wrapper if one is needed, or a skip instruction otherwise.

Definition at line 984 of file java_bytecode_convert_method.cpp.

◆ get_or_create_block_for_pcrange()

code_blockt & java_bytecode_convert_methodt::get_or_create_block_for_pcrange	(	block_tree_nodet &	tree,
		code_blockt &	this_block,
		method_offsett	address_start,
		method_offsett	address_limit,
		method_offsett	next_block_start_address,
		const address_mapt &	amap,
		bool	allow_merge = `true`
	)

protected

As above, but this version can additionally create a new branch in the block_tree-node and code_blockt trees to envelop the requested address range.

For example, if the tree was initially flat, with nodes (1-10), (11-20), (21-30) and the caller asked for range 13-28, this would build a surrounding tree node, leaving the tree of shape (1-10), ^( (11-20), (21-30) )^, and return a reference to the new branch highlighted with ^^. 'tree' and 'this_block' trees are always maintained with equal shapes. ('this_block' may additionally contain code_declt children which are ignored for this purpose).

Parameters

[in,out]	tree	A code block descriptor.
[in,out]	this_block	The corresponding actual code_blockt.
	address_start	the Java bytecode offsets searched for.
	address_limit	the Java bytecode offsets searched for.
	next_block_start_address	The bytecode offset of tree/this_block's successor sibling, or UINT_MAX if none exists.
	amap	The bytecode address map.
	allow_merge	Whether modifying the block tree is allowed. This is always true except when called from `get_block_for_pcrange`.

Returns: The code_blockt most closely enclosing the given address range.

Definition at line 766 of file java_bytecode_convert_method.cpp.

◆ get_static_field()

irep_idt java_bytecode_convert_methodt::get_static_field	(	const irep_idt &	class_identifier,
		const irep_idt &	component_name
	)		const

protected

Get static field identifier referred to by class_identifier.component_name Note this may be inherited from either a parent or an interface.

Parameters

class_identifier	class used to refer to the field
component_name	component (static field) name

Returns: identifier of the actual concrete field referred to

Definition at line 3330 of file java_bytecode_convert_method.cpp.

◆ is_method_inherited()

bool java_bytecode_convert_methodt::is_method_inherited	(	const irep_idt &	classname,
		const irep_idt &	mangled_method_name
	)		const

protected

Returns true iff method methodid from class classname is a method inherited from a class or interface from which classname inherits, either directly or indirectly.

Parameters

classname	class whose method is referenced
mangled_method_name	The particular overload of a given method.

Definition at line 3315 of file java_bytecode_convert_method.cpp.

◆ is_parameter()

bool java_bytecode_convert_methodt::is_parameter ( const local_variablet & v )

inlineprotected

Returns true iff the slot index of the local variable of a method (coming from the LVT) is a parameter of that method.

Assumes that slots_for_parameters is initialized upon call.

Definition at line 219 of file java_bytecode_convert_method_class.h.

◆ label()

irep_idt java_bytecode_convert_methodt::label ( const irep_idt & address )

staticprotected

Definition at line 158 of file java_bytecode_convert_method.cpp.

◆ operator()()

void java_bytecode_convert_methodt::operator()	(	const symbolt &	class_symbol,
		const methodt &	method,
		const std::optional< prefix_filtert > &	method_context
	)

inline

Definition at line 69 of file java_bytecode_convert_method_class.h.

◆ pop()

exprt::operandst java_bytecode_convert_methodt::pop ( std::size_t n )

protected

Definition at line 124 of file java_bytecode_convert_method.cpp.

◆ pop_residue()

void java_bytecode_convert_methodt::pop_residue ( std::size_t n )

protected

removes minimum(n, stack.size()) elements from the stack

Definition at line 142 of file java_bytecode_convert_method.cpp.

◆ push()

void java_bytecode_convert_methodt::push ( const exprt::operandst & o )

protected

Definition at line 149 of file java_bytecode_convert_method.cpp.

◆ replace_call_to_cprover_assume()

codet & java_bytecode_convert_methodt::replace_call_to_cprover_assume	(	source_locationt	location,
		codet &	c
	)

protected

Definition at line 2392 of file java_bytecode_convert_method.cpp.

◆ replace_goto_target()

void java_bytecode_convert_methodt::replace_goto_target	(	codet &	repl,
		const irep_idt &	old_label,
		const irep_idt &	new_label
	)

staticprotected

Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.

Parameters

[in,out]	repl	A block of code in which to perform replacement.
	old_label	The label to be replaced.
	new_label	The label to replace `old_label` with.

Definition at line 695 of file java_bytecode_convert_method.cpp.

◆ save_stack_entries()

void java_bytecode_convert_methodt::save_stack_entries	(	const std::string &	tmp_var_prefix,
		code_blockt &	block,
		const bytecode_write_typet	write_type,
		const irep_idt &	identifier
	)

protected

Create temporary variables if a write instruction can have undesired side- effects.

Parameters

	tmp_var_prefix	The prefix string to use for new temporary variables
[out]	block	The code block the assignment is added to if required.
	write_type	The enumeration type of the write instruction.
	identifier	The identifier of the symbol in the write instruction.

Definition at line 3349 of file java_bytecode_convert_method.cpp.

◆ setup_local_variables()

void java_bytecode_convert_methodt::setup_local_variables	(	const methodt &	m,
		const address_mapt &	amap
	)

protected

See find_initializers_for_slot above for more detail.

Populates this->vars_with_holes equal to this->local_variable_table, only with variable table entries that flow together combined. Also symbol-table registers all locals.

Parameters

m	Java method
amap	Map from bytecode indices to instructions in `m`

Definition at line 740 of file java_local_variable_table.cpp.

◆ tmp_variable()

symbol_exprt java_bytecode_convert_methodt::tmp_variable	(	const std::string &	prefix,
		const typet &	type
	)

protected

Definition at line 163 of file java_bytecode_convert_method.cpp.

◆ try_catch_handler()

std::vector< java_bytecode_convert_methodt::method_offsett > java_bytecode_convert_methodt::try_catch_handler	(	method_offsett	address,
		const java_bytecode_parse_treet::methodt::exception_tablet &	exception_table
	)		const

protected

Definition at line 3177 of file java_bytecode_convert_method.cpp.

◆ variable()

exprt java_bytecode_convert_methodt::variable	(	const exprt &	arg,
		char	type_char,
		size_t	address
	)

protected

Returns an expression indicating a local variable suitable to load/store from a bytecode at address address a value of type type_char stored in the JVM's slot arg.

Parameters

arg	The local variable slot
type_char	The type of the value stored in the slot pointed to by `arg`, this is only used in the case where a new unnamed local variable is created
address	Bytecode address used to find a variable that the LVT declares to be live and living in the slot pointed by `arg` for this bytecode

Returns: symbol_exprt or type-cast symbol_exprt

Definition at line 196 of file java_bytecode_convert_method.cpp.

Friends And Related Symbol Documentation

◆ java_bytecode_convert_method_unit_testt

friend class java_bytecode_convert_method_unit_testt

friend

Definition at line 545 of file java_bytecode_convert_method_class.h.

Member Data Documentation

◆ any_superclass_has_clinit_method

std::map<irep_idt, bool> java_bytecode_convert_methodt::any_superclass_has_clinit_method

protected

Definition at line 175 of file java_bytecode_convert_method_class.h.

◆ assert_no_exceptions_thrown

const bool java_bytecode_convert_methodt::assert_no_exceptions_thrown

protected

Definition at line 85 of file java_bytecode_convert_method_class.h.

◆ class_has_clinit_method

std::map<irep_idt, bool> java_bytecode_convert_methodt::class_has_clinit_method

protected

Definition at line 174 of file java_bytecode_convert_method_class.h.

◆ class_hierarchy

const class_hierarchyt& java_bytecode_convert_methodt::class_hierarchy

protected

Definition at line 176 of file java_bytecode_convert_method_class.h.

◆ current_method

irep_idt java_bytecode_convert_methodt::current_method

protected

A copy of method_id :/.

Definition at line 95 of file java_bytecode_convert_method_class.h.

◆ log

messaget java_bytecode_convert_methodt::log

protected

Definition at line 80 of file java_bytecode_convert_method_class.h.

◆ max_array_length

const size_t java_bytecode_convert_methodt::max_array_length

protected

Definition at line 83 of file java_bytecode_convert_method_class.h.

◆ method_has_this

bool java_bytecode_convert_methodt::method_has_this

protected

Definition at line 173 of file java_bytecode_convert_method_class.h.

◆ method_id

irep_idt java_bytecode_convert_methodt::method_id

protected

Fully qualified name of the method under translation.

Initialized by convert. Example: "my.package.ClassName.myMethodName:(II)I"

Definition at line 92 of file java_bytecode_convert_method_class.h.

◆ method_return_type

typet java_bytecode_convert_methodt::method_return_type

protected

Return type of the method under conversion.

Initialized by convert.

Definition at line 99 of file java_bytecode_convert_method_class.h.

◆ needed_lazy_methods

std::optional<ci_lazy_methods_neededt> java_bytecode_convert_methodt::needed_lazy_methods

protected

Definition at line 87 of file java_bytecode_convert_method_class.h.

◆ ns

namespacet java_bytecode_convert_methodt::ns

protected

Definition at line 82 of file java_bytecode_convert_method_class.h.

◆ slots_for_parameters

method_offsett java_bytecode_convert_methodt::slots_for_parameters

protected

Number of local variable slots used by the JVM to pass parameters upon invocation of the method under translation.

Initialized in convert.

Definition at line 106 of file java_bytecode_convert_method_class.h.

◆ stack

stackt java_bytecode_convert_methodt::stack

protected

Definition at line 208 of file java_bytecode_convert_method_class.h.

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_methodt::string_preprocess

protected

Definition at line 101 of file java_bytecode_convert_method_class.h.

◆ symbol_table

symbol_table_baset& java_bytecode_convert_methodt::symbol_table

protected

Definition at line 81 of file java_bytecode_convert_method_class.h.

◆ threading_support

const bool java_bytecode_convert_methodt::threading_support

protected

Definition at line 86 of file java_bytecode_convert_method_class.h.

◆ throw_assertion_error

const bool java_bytecode_convert_methodt::throw_assertion_error

protected

Definition at line 84 of file java_bytecode_convert_method_class.h.

◆ tmp_vars

std::list<symbol_exprt> java_bytecode_convert_methodt::tmp_vars

protected

Definition at line 199 of file java_bytecode_convert_method_class.h.

◆ used_local_names

std::set<symbol_exprt> java_bytecode_convert_methodt::used_local_names

protected

Definition at line 172 of file java_bytecode_convert_method_class.h.

◆ variables

expanding_vectort<variablest> java_bytecode_convert_methodt::variables

protected

Definition at line 171 of file java_bytecode_convert_method_class.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_local_variable_table.cpp

Public Types
typedef java_bytecode_parse_treet::methodt	methodt

typedef java_bytecode_parse_treet::instructiont	instructiont

typedef methodt::instructionst	instructionst

typedef methodt::local_variable_tablet	local_variable_tablet

typedef methodt::local_variablet	local_variablet

typedef uint16_t	method_offsett

typedef std::vector< local_variable_with_holest >	local_variable_table_with_holest

typedef std::map< method_offsett, converted_instructiont >	address_mapt

typedef cfg_dominators_templatet< method_with_amapt, method_offsett, false >	java_cfg_dominatorst

Classes

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ address_mapt

◆ instructionst

◆ instructiont

◆ java_cfg_dominatorst

◆ local_variable_table_with_holest

◆ local_variable_tablet

◆ local_variablet

◆ method_offsett

◆ methodt

◆ stackt

◆ variablest

Member Enumeration Documentation

◆ bytecode_write_typet

◆ instruction_sizet

◆ variable_cast_argumentt

Constructor & Destructor Documentation

◆ java_bytecode_convert_methodt()

Member Function Documentation

◆ convert()

◆ convert_aload()

◆ convert_astore()

◆ convert_athrow()

◆ convert_checkcast()

◆ convert_cmp()

◆ convert_cmp2()

◆ convert_const()

◆ convert_dup2()

◆ convert_dup2_x1()

◆ convert_dup2_x2()

◆ convert_getstatic()

◆ convert_if()

◆ convert_if_cmp()

◆ convert_ifnonull()

◆ convert_ifnull()

◆ convert_iinc()

◆ convert_instructions()

◆ convert_invoke()

◆ convert_invoke_dynamic()

◆ convert_load()

◆ convert_monitorenterexit()

◆ convert_multianewarray()

◆ convert_new()

◆ convert_newarray()

◆ convert_parameter_annotations()

◆ convert_pop()

◆ convert_putfield()

◆ convert_putstatic()

◆ convert_ret()

◆ convert_shl()

◆ convert_store()

◆ convert_switch()

◆ convert_ushr()

◆ create_stack_tmp_var()

◆ do_exception_handling()

◆ draw_edges_from_ret_to_jsr()

◆ find_initializers()

◆ find_initializers_for_slot()

◆ find_variable_for_slot()

◆ get_block_for_pcrange()

◆ get_clinit_call()

◆ get_or_create_block_for_pcrange()

◆ get_static_field()

◆ is_method_inherited()

◆ is_parameter()

◆ label()

◆ operator()()

◆ pop()

◆ pop_residue()

◆ push()

◆ replace_call_to_cprover_assume()