java_bytecode_convert_method.h File Reference

JAVA Bytecode Language Conversion. More...

#include "java_bytecode_convert_method_class.h"
#include "java_bytecode_parse_tree.h"

Include dependency graph for java_bytecode_convert_method.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

Functions
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 &, 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, const std::optional< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
void	create_method_stub_symbol (const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &message_handler)
void	java_bytecode_convert_method_lazy (symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_table_baset &symbol_table, message_handlert &)
	This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More...
void	create_parameter_names (const java_bytecode_parse_treet::methodt &m, const irep_idt &method_identifier, java_method_typet::parameterst &parameters, const java_bytecode_convert_methodt::method_offsett &slots_for_parameters)
	Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the java_method_typet and the external variables vector. More...
void	create_parameter_symbols (const java_method_typet::parameterst &parameters, variablest &variables, symbol_table_baset &symbol_table)
	Adds the parameter symbols to the symbol table. More...

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.h.

Typedef Documentation

variablest

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

Definition at line 58 of file java_bytecode_convert_method.h.

Function Documentation

create_method_stub_symbol()

void create_method_stub_symbol	(	const irep_idt &	identifier,
		const irep_idt &	base_name,
		const irep_idt &	pretty_name,
		const typet &	type,
		const irep_idt &	declaring_class,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

Definition at line 94 of file java_bytecode_convert_method.cpp.

create_parameter_names()

void create_parameter_names	(	const java_bytecode_parse_treet::methodt &	m,
		const irep_idt &	method_identifier,
		java_method_typet::parameterst &	parameters,
		const java_bytecode_convert_methodt::method_offsett &	slots_for_parameters
	)

Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the java_method_typet and the external variables vector.

Parameters

m	the parsed method whose local variable table contains the name of the parameters
method_identifier	the identifier of the method
parameters	the java_method_typet's parameters [out]
slots_for_parameters	the number of parameter slots available, i.e. a positive integer

Definition at line 422 of file java_bytecode_convert_method.cpp.

create_parameter_symbols()

void create_parameter_symbols	(	const java_method_typet::parameterst &	parameters,
		variablest &	variables,
		symbol_table_baset &	symbol_table
	)

Adds the parameter symbols to the symbol table.

Parameters

parameters	the java_method_typet's parameters [out]
variables	external storage of jvm variables [out]
symbol_table	the symbol table [out]

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,
		std::optional< ci_lazy_methods_neededt >	needed_lazy_methods,
		java_string_library_preprocesst &	string_preprocess,
		const class_hierarchyt &	class_hierarchy,
		bool	threading_support,
		const std::optional< prefix_filtert > &	method_context,
		bool	assert_no_exceptions_thrown
	)

Definition at line 3278 of file java_bytecode_convert_method.cpp.

java_bytecode_convert_method_lazy()

void java_bytecode_convert_method_lazy	(	symbolt &	class_symbol,
		const irep_idt &	method_identifier,
		const java_bytecode_parse_treet::methodt &	m,
		symbol_table_baset &	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. The method, if not static, will be added to the class' list of methods.
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 299 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 3200 of file java_bytecode_convert_method.cpp.