#include <java_bytecode_language.h>

Inheritance diagram for java_bytecode_languaget:

Collaboration diagram for java_bytecode_languaget:

Public Member Functions
void	set_language_options (const optionst &, message_handlert &) override
	Consume options that are java bytecode specific. More...

virtual bool	preprocess (std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
	ANSI-C preprocessing. More...

virtual bool	parse (message_handlert &)
	We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have have been given a main class. More...

bool	parse (std::istream &instream, const std::string &path, message_handlert &message_handler) override
	We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have a JAR file given via the -jar option: a) the argument of the –main-class command-line option, b) the manifest file of the JAR If no main class was found, all classes in the JAR file are loaded. More...

bool	generate_support_functions (symbol_table_baset &symbol_table, message_handlert &message_handler) override
	Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More...

bool	typecheck (symbol_table_baset &context, const std::string &module, message_handlert &message_handler) override

virtual bool	final (symbol_table_baset &context) override
	Final adjustments, e.g. More...

void	show_parse (std::ostream &out, message_handlert &) override

virtual	~java_bytecode_languaget ()

	java_bytecode_languaget (std::unique_ptr< select_pointer_typet > pointer_type_selector)

	java_bytecode_languaget ()

bool	from_expr (const exprt &expr, std::string &code, const namespacet &ns) override
	Formats the given expression in a language-specific way. More...

bool	from_type (const typet &type, std::string &code, const namespacet &ns) override
	Formats the given type in a language-specific way. More...

bool	to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
	Parses the given string into an expression. More...

std::unique_ptr< languaget >	new_language () override

std::string	id () const override

std::string	description () const override

std::set< std::string >	extensions () const override

void	modules_provided (std::set< std::string > &modules) override

virtual void	methods_provided (std::unordered_set< irep_idt > &methods) const override
	Provide feedback to `language_filest` so that when asked for a lazy method, it can delegate to this instance of java_bytecode_languaget. More...

virtual void	convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) override
	Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a fully-elaborated one. More...

Public Member Functions inherited from languaget
virtual void	dependencies (const std::string &module, std::set< std::string > &modules)

virtual bool	interfaces (symbol_table_baset &symbol_table, message_handlert &message_handler)

virtual bool	can_keep_file_local ()
	Is it possible to call three-argument typecheck() on this object? More...

virtual bool	typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local)
	typecheck without removing specified entries from the symbol table More...

virtual bool	type_to_name (const typet &type, std::string &name, const namespacet &ns)
	Encodes the given type in a language-specific way. More...

	languaget ()

virtual	~languaget ()

Protected Member Functions
void	convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &message_handler)

bool	convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)
	Convert a method (one whose type is known but whose body hasn't been converted) if it doesn't already have a body, and lift clinit calls if requested by the user. More...

bool	convert_single_method_code (const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)
	Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc. More...

bool	do_ci_lazy_method_conversion (symbol_table_baset &, message_handlert &)
	Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. More...

const select_pointer_typet &	get_pointer_type_selector () const

Protected Attributes
std::optional< java_bytecode_language_optionst >	language_options

irep_idt	main_class

std::vector< irep_idt >	main_jar_classes

java_class_loadert	java_class_loader

java_object_factory_parameterst	object_factory_parameters

method_bytecodet	method_bytecode

java_string_library_preprocesst	string_preprocess

Private Member Functions
virtual std::vector< load_extra_methodst >	build_extra_entry_points (const optionst &) const
	This method should be overloaded to provide alternative approaches for specifying extra entry points. More...

void	parse_from_main_class (message_handlert &)

void	initialize_class_loader (message_handlert &)

Private Attributes
const std::unique_ptr< const select_pointer_typet >	pointer_type_selector

synthetic_methods_mapt	synthetic_methods
	Maps synthetic method names on to the particular type of synthetic method (static initializer, initializer wrapper, etc). More...

stub_global_initializer_factoryt	stub_global_initializer_factory

class_hierarchyt	class_hierarchy

std::unordered_map< std::string, object_creation_referencet >	references
	Map used in all calls to functions that deterministically create objects (currently only assign_from_json). More...

Detailed Description

Definition at line 259 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )

virtual

Definition at line 1620 of file java_bytecode_language.cpp.

◆ java_bytecode_languaget() [1/2]

java_bytecode_languaget::java_bytecode_languaget ( std::unique_ptr< select_pointer_typet > pointer_type_selector )

inline

Definition at line 295 of file java_bytecode_language.h.

◆ java_bytecode_languaget() [2/2]

java_bytecode_languaget::java_bytecode_languaget ( )

inline

Definition at line 302 of file java_bytecode_language.h.

Member Function Documentation

◆ build_extra_entry_points()

std::vector< load_extra_methodst > java_bytecode_languaget::build_extra_entry_points ( const optionst & options ) const

privatevirtual

This method should be overloaded to provide alternative approaches for specifying extra entry points.

To provide a regex entry point, the command line option --lazy-methods-extra-entry-point can be used directly.

Definition at line 1628 of file java_bytecode_language.cpp.

◆ convert_lazy_method()

void java_bytecode_languaget::convert_lazy_method	(	const irep_idt &	function_id,
		symbol_table_baset &	symtab,
		message_handlert &	message_handler
	)

overridevirtual

Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a fully-elaborated one.

Remarks: Amends the symbol table entry for function function_id, which should be a method provided by this instance of java_bytecode_languaget to have a value representing the method body identical to that produced using eager method conversion.

Parameters

function_id	method ID to convert
symtab	global symbol table
message_handler	message handler

Reimplemented from languaget.

Definition at line 1194 of file java_bytecode_language.cpp.

◆ convert_single_method() [1/2]

void java_bytecode_languaget::convert_single_method	(	const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		lazy_class_to_declared_symbols_mapt &	class_to_declared_symbols,
		message_handlert &	message_handler
	)

inlineprotected

Definition at line 343 of file java_bytecode_language.h.

◆ convert_single_method() [2/2]

bool java_bytecode_languaget::convert_single_method	(	const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		std::optional< ci_lazy_methods_neededt >	needed_lazy_methods,
		lazy_class_to_declared_symbols_mapt &	class_to_declared_symbols,
		message_handlert &	message_handler
	)

protected

Convert a method (one whose type is known but whose body hasn't been converted) if it doesn't already have a body, and lift clinit calls if requested by the user.

Remarks: Amends the symbol table entry for function function_id, which should be a method provided by this instance of java_bytecode_languaget to have a value representing the method body.

Parameters

function_id	method ID to convert
symbol_table	global symbol table
needed_lazy_methods	optionally a collection of needed methods to update with any methods touched during the conversion
class_to_declared_symbols	maps classes to the symbols that they declare.
message_handler	message handler

Definition at line 1292 of file java_bytecode_language.cpp.

◆ convert_single_method_code()

bool java_bytecode_languaget::convert_single_method_code	(	const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		std::optional< ci_lazy_methods_neededt >	needed_lazy_methods,
		lazy_class_to_declared_symbols_mapt &	class_to_declared_symbols,
		message_handlert &	message_handler
	)

protected

Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc.

Remarks: Amends the symbol table entry for function function_id, which should be a method provided by this instance of java_bytecode_languaget to have a value representing the method body.

Parameters

function_id	method ID to convert
symbol_table	global symbol table
needed_lazy_methods	optionally a collection of needed methods to update with any methods touched during the conversion
class_to_declared_symbols	maps classes to the symbols that they declare.
message_handler	message handler

Definition at line 1351 of file java_bytecode_language.cpp.

◆ description()

std::string java_bytecode_languaget::description ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 331 of file java_bytecode_language.h.

◆ do_ci_lazy_method_conversion()

bool java_bytecode_languaget::do_ci_lazy_method_conversion	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

protected

Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point.

In brief, static methods are reachable if we find a callsite in another reachable site, while virtual methods are reachable if we find a virtual callsite targeting a compatible type and a constructor callsite indicating an object of that type may be instantiated (or evidence that an object of that type exists before the main function is entered, such as being passed as a parameter).

Parameters

symbol_table	global symbol table
message_handler	message handler

Returns: Elaborates lazily-converted methods that may be reachable starting from the main entry point (usually provided with the –function command- line option) (side-effect on the symbol_table). Returns false on success.

Definition at line 1122 of file java_bytecode_language.cpp.

◆ extensions()

std::set< std::string > java_bytecode_languaget::extensions ( ) const

overridevirtual

Implements languaget.

Definition at line 272 of file java_bytecode_language.cpp.

◆ final()

bool java_bytecode_languaget::final ( symbol_table_baset & symbol_table )

overridevirtual

Final adjustments, e.g.

initializing stub functions and globals that were discovered during function loading

Reimplemented from languaget.

Definition at line 1516 of file java_bytecode_language.cpp.

◆ from_expr()

bool java_bytecode_languaget::from_expr	(	const exprt &	expr,
		std::string &	code,
		const namespacet &	ns
	)

overridevirtual

Formats the given expression in a language-specific way.

Parameters

expr	the expression to format
code	the formatted expression
ns	a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 1547 of file java_bytecode_language.cpp.

◆ from_type()

bool java_bytecode_languaget::from_type	(	const typet &	type,
		std::string &	code,
		const namespacet &	ns
	)

overridevirtual

Formats the given type in a language-specific way.

Parameters

type	the type to format
code	the formatted type
ns	a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 1556 of file java_bytecode_language.cpp.

◆ generate_support_functions()

bool java_bytecode_languaget::generate_support_functions	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

overridevirtual

Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.

This runs after the typecheck phase but before lazy function loading. Anything that must wait until lazy function loading is done can be deferred until final, which runs after lazy function loading is complete. Functions introduced here are visible to lazy loading and can influence its decisions (e.g. picking the types of input parameters and globals), whereas anything introduced during final cannot.

Implements languaget.

Definition at line 1059 of file java_bytecode_language.cpp.

◆ get_pointer_type_selector()

const select_pointer_typet & java_bytecode_languaget::get_pointer_type_selector ( ) const

protected

Definition at line 1158 of file java_bytecode_language.cpp.

◆ id()

std::string java_bytecode_languaget::id ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 330 of file java_bytecode_language.h.

◆ initialize_class_loader()

void java_bytecode_languaget::initialize_class_loader ( message_handlert & message_handler )

private

Definition at line 293 of file java_bytecode_language.cpp.

◆ methods_provided()

void java_bytecode_languaget::methods_provided ( std::unordered_set< irep_idt > & methods ) const

overridevirtual

Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this instance of java_bytecode_languaget.

Parameters

[out] methods Populates methods with the complete list of lazy methods that are available to convert (those which are valid parameters for convert_lazy_method)

Reimplemented from languaget.

Definition at line 1169 of file java_bytecode_language.cpp.

◆ modules_provided()

void java_bytecode_languaget::modules_provided ( std::set< std::string > & modules )

overridevirtual

Reimplemented from languaget.

Definition at line 277 of file java_bytecode_language.cpp.

◆ new_language()

std::unique_ptr<languaget> java_bytecode_languaget::new_language ( )

inlineoverridevirtual

Implements languaget.

Definition at line 325 of file java_bytecode_language.h.

◆ parse() [1/2]

bool java_bytecode_languaget::parse ( message_handlert & message_handler )

virtual

We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have have been given a main class.

Definition at line 367 of file java_bytecode_language.cpp.

◆ parse() [2/2]

bool java_bytecode_languaget::parse	(	std::istream &	instream,
		const std::string &	path,
		message_handlert &	message_handler
	)

overridevirtual

We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have a JAR file given via the -jar option: a) the argument of the –main-class command-line option, b) the manifest file of the JAR If no main class was found, all classes in the JAR file are loaded.

Implements languaget.

Definition at line 382 of file java_bytecode_language.cpp.

◆ parse_from_main_class()

void java_bytecode_languaget::parse_from_main_class ( message_handlert & message_handler )

private

Definition at line 322 of file java_bytecode_language.cpp.

◆ preprocess()

bool java_bytecode_languaget::preprocess	(	std::istream &	instream,
		const std::string &	path,
		std::ostream &	outstream,
		message_handlert &	message_handler
	)

overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 283 of file java_bytecode_language.cpp.

◆ set_language_options()

void java_bytecode_languaget::set_language_options	(	const optionst &	options,
		message_handlert &	message_handler
	)

overridevirtual

Consume options that are java bytecode specific.

Reimplemented from languaget.

Definition at line 259 of file java_bytecode_language.cpp.

◆ show_parse()

void java_bytecode_languaget::show_parse	(	std::ostream &	out,
		message_handlert &	message_handler
	)

overridevirtual

Implements languaget.

Definition at line 1522 of file java_bytecode_language.cpp.

◆ to_expr()

bool java_bytecode_languaget::to_expr	(	const std::string &	code,
		const std::string &	module,
		exprt &	expr,
		const namespacet &	ns,
		message_handlert &	message_handler
	)

overridevirtual

Parses the given string into an expression.

Parameters

code	the string to parse
module	prefix to be used for identifiers
expr	the parsed expression
ns	a namespace
message_handler	a message handler

Returns: false if the conversion succeeds

Implements languaget.

Definition at line 1565 of file java_bytecode_language.cpp.

◆ typecheck()

bool java_bytecode_languaget::typecheck	(	symbol_table_baset &	context,
		const std::string &	module,
		message_handlert &	message_handler
	)

overridevirtual

Implements languaget.

Definition at line 804 of file java_bytecode_language.cpp.

Member Data Documentation

◆ class_hierarchy

class_hierarchyt java_bytecode_languaget::class_hierarchy

private

Definition at line 390 of file java_bytecode_language.h.

◆ java_class_loader

java_class_loadert java_bytecode_languaget::java_class_loader

protected

Definition at line 375 of file java_bytecode_language.h.

◆ language_options

std::optional<java_bytecode_language_optionst> java_bytecode_languaget::language_options

protected

Definition at line 372 of file java_bytecode_language.h.

◆ main_class

irep_idt java_bytecode_languaget::main_class

protected

Definition at line 373 of file java_bytecode_language.h.

◆ main_jar_classes

std::vector<irep_idt> java_bytecode_languaget::main_jar_classes

protected

Definition at line 374 of file java_bytecode_language.h.

◆ method_bytecode

method_bytecodet java_bytecode_languaget::method_bytecode

protected

Definition at line 377 of file java_bytecode_language.h.

◆ object_factory_parameters

java_object_factory_parameterst java_bytecode_languaget::object_factory_parameters

protected

Definition at line 376 of file java_bytecode_language.h.

◆ pointer_type_selector

const std::unique_ptr<const select_pointer_typet> java_bytecode_languaget::pointer_type_selector

private

Definition at line 383 of file java_bytecode_language.h.

◆ references

std::unordered_map<std::string, object_creation_referencet> java_bytecode_languaget::references

private

Map used in all calls to functions that deterministically create objects (currently only assign_from_json).

It tracks objects that should be reference-equal to each other by mapping IDs of such objects to symbols that store their values.

Definition at line 396 of file java_bytecode_language.h.

◆ string_preprocess

java_string_library_preprocesst java_bytecode_languaget::string_preprocess

protected

Definition at line 378 of file java_bytecode_language.h.

◆ stub_global_initializer_factory

stub_global_initializer_factoryt java_bytecode_languaget::stub_global_initializer_factory

private

Definition at line 389 of file java_bytecode_language.h.

◆ synthetic_methods

synthetic_methods_mapt java_bytecode_languaget::synthetic_methods

private

Maps synthetic method names on to the particular type of synthetic method (static initializer, initializer wrapper, etc).

For full documentation see synthetic_method_map.h

Definition at line 388 of file java_bytecode_language.h.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

◆ java_bytecode_languaget() [1/2]

◆ java_bytecode_languaget() [2/2]

Member Function Documentation

◆ build_extra_entry_points()

◆ convert_lazy_method()

◆ convert_single_method() [1/2]

◆ convert_single_method() [2/2]

◆ convert_single_method_code()

◆ description()

◆ do_ci_lazy_method_conversion()

◆ extensions()

◆ final()

◆ from_expr()

◆ from_type()

◆ generate_support_functions()

◆ get_pointer_type_selector()

◆ id()

◆ initialize_class_loader()

◆ methods_provided()

◆ modules_provided()

◆ new_language()

◆ parse() [1/2]

◆ parse() [2/2]

◆ parse_from_main_class()

◆ preprocess()

◆ set_language_options()

◆ show_parse()

◆ to_expr()

◆ typecheck()

Member Data Documentation

◆ class_hierarchy

◆ java_class_loader

◆ language_options

◆ main_class

◆ main_jar_classes

◆ method_bytecode

◆ object_factory_parameters

◆ pointer_type_selector

◆ references

◆ string_preprocess

◆ stub_global_initializer_factory

◆ synthetic_methods