#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 &) override
	Consume options that are java bytecode specific. More...

void	set_message_handler (message_handlert &message_handler) override

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

virtual bool	parse ()
	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) 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_tablet &symbol_table) override
	Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More...

bool	typecheck (symbol_tablet &context, const std::string &module) override

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

void	show_parse (std::ostream &out) 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) 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) 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_tablet &symbol_table)

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

virtual bool	typecheck (symbol_tablet &symbol_table, const std::string &module, 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 ()

Public Member Functions inherited from messaget
message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`. More...

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)

bool	convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
	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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
	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_tablet &)
	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
optionalt< 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

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

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 ()

void	initialize_class_loader ()

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...

Additional Inherited Members
Public Types inherited from messaget
enum	message_levelt { M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6, M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Static Public Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

Detailed Description

Definition at line 274 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )

virtual

Definition at line 1600 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 308 of file java_bytecode_language.h.

◆ java_bytecode_languaget() [2/2]

java_bytecode_languaget::java_bytecode_languaget ( )

inline

Definition at line 315 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 1608 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
	)

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

Reimplemented from languaget.

Definition at line 1186 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
	)

inlineprotected

Definition at line 352 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,
		optionalt< ci_lazy_methods_neededt >	needed_lazy_methods,
		lazy_class_to_declared_symbols_mapt &	class_to_declared_symbols
	)

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.

Definition at line 1283 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,
		optionalt< ci_lazy_methods_neededt >	needed_lazy_methods,
		lazy_class_to_declared_symbols_mapt &	class_to_declared_symbols
	)

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.

Definition at line 1336 of file java_bytecode_language.cpp.

◆ description()

std::string java_bytecode_languaget::description ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 341 of file java_bytecode_language.h.

◆ do_ci_lazy_method_conversion()

bool java_bytecode_languaget::do_ci_lazy_method_conversion ( symbol_tablet & symbol_table )

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

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 1117 of file java_bytecode_language.cpp.

◆ extensions()

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

overridevirtual

Implements languaget.

Definition at line 273 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 1500 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 1529 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 1538 of file java_bytecode_language.cpp.

◆ generate_support_functions()

bool java_bytecode_languaget::generate_support_functions ( symbol_tablet & symbol_table )

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 1057 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 1151 of file java_bytecode_language.cpp.

◆ id()

std::string java_bytecode_languaget::id ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 340 of file java_bytecode_language.h.

◆ initialize_class_loader()

void java_bytecode_languaget::initialize_class_loader ( )

private

Definition at line 299 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.

Returns: 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 1162 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 278 of file java_bytecode_language.cpp.

◆ new_language()

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

inlineoverridevirtual

Implements languaget.

Definition at line 337 of file java_bytecode_language.h.

◆ parse() [1/2]

bool java_bytecode_languaget::parse ( )

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 369 of file java_bytecode_language.cpp.

◆ parse() [2/2]

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

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 384 of file java_bytecode_language.cpp.

◆ parse_from_main_class()

void java_bytecode_languaget::parse_from_main_class ( )

private

Definition at line 327 of file java_bytecode_language.cpp.

◆ preprocess()

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

overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 284 of file java_bytecode_language.cpp.

◆ set_language_options()

void java_bytecode_languaget::set_language_options ( const optionst & options )

overridevirtual

Consume options that are java bytecode specific.

Reimplemented from languaget.

Definition at line 262 of file java_bytecode_language.cpp.

◆ set_message_handler()

void java_bytecode_languaget::set_message_handler ( message_handlert & message_handler )

overridevirtual

Reimplemented from messaget.

Definition at line 293 of file java_bytecode_language.cpp.

◆ show_parse()

void java_bytecode_languaget::show_parse ( std::ostream & out )

overridevirtual

Implements languaget.

Definition at line 1506 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
	)

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

Returns: false if the conversion succeeds

Implements languaget.

Definition at line 1547 of file java_bytecode_language.cpp.

◆ typecheck()

bool java_bytecode_languaget::typecheck	(	symbol_tablet &	context,
		const std::string &	module
	)

overridevirtual

Implements languaget.

Definition at line 808 of file java_bytecode_language.cpp.

Member Data Documentation

◆ class_hierarchy

class_hierarchyt java_bytecode_languaget::class_hierarchy

private

Definition at line 395 of file java_bytecode_language.h.

◆ java_class_loader

java_class_loadert java_bytecode_languaget::java_class_loader

protected

Definition at line 380 of file java_bytecode_language.h.

◆ language_options

optionalt<java_bytecode_language_optionst> java_bytecode_languaget::language_options

protected

Definition at line 377 of file java_bytecode_language.h.

◆ main_class

irep_idt java_bytecode_languaget::main_class

protected

Definition at line 378 of file java_bytecode_language.h.

◆ main_jar_classes

std::vector<irep_idt> java_bytecode_languaget::main_jar_classes

protected

Definition at line 379 of file java_bytecode_language.h.

◆ method_bytecode

method_bytecodet java_bytecode_languaget::method_bytecode

protected

Definition at line 382 of file java_bytecode_language.h.

◆ object_factory_parameters

java_object_factory_parameterst java_bytecode_languaget::object_factory_parameters

protected

Definition at line 381 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 388 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 401 of file java_bytecode_language.h.

◆ string_preprocess

java_string_library_preprocesst java_bytecode_languaget::string_preprocess

protected

Definition at line 383 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 394 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 393 of file java_bytecode_language.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Additional Inherited Members

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()

◆ set_message_handler()

◆ 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