Class responsible to load .class files. More...

#include <java_class_loader.h>

Inheritance diagram for java_class_loadert:

Collaboration diagram for java_class_loadert:

Public Types
typedef std::list< java_bytecode_parse_treet >	parse_tree_with_overlayst
	A list of parse trees supporting overlay classes. More...

typedef std::map< irep_idt, parse_tree_with_overlayst >	parse_tree_with_overridest_mapt
	A map from class names to list of parse tree where multiple entries can exist in case of overlay classes. More...

typedef std::function< std::vector< irep_idt >const irep_idt &)>	get_extra_class_refs_functiont
	A function that yields a list of extra dependencies based on a class name. More...

Public Member Functions
	java_class_loadert ()

parse_tree_with_overlayst &	operator() (const irep_idt &class_name, message_handlert &)

bool	can_load_class (const irep_idt &class_name, message_handlert &)
	Checks whether `class_name` is parseable from the classpath, ignoring class loading limits. More...

parse_tree_with_overlayst &	get_parse_tree (java_class_loader_limitt &class_loader_limit, const irep_idt &class_name, message_handlert &)
	Check through all the places class parse trees can appear and returns the first implementation it finds plus any overlay class implementations. More...

void	set_java_cp_include_files (const std::string &cp_include_files)
	Set the argument of the class loader limit java_class_loader_limitt. More...

void	set_extra_class_refs_function (get_extra_class_refs_functiont func)
	Sets a function that provides extra dependencies for a particular class. More...

void	add_load_classes (const std::vector< irep_idt > &classes)
	Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference. More...

std::vector< irep_idt >	load_entire_jar (const std::string &jar_path, message_handlert &)
	Load all class files from a .jar file. More...

fixed_keys_map_wrappert< parse_tree_with_overridest_mapt >	get_class_with_overlays_map ()
	Map from class names to the bytecode parse trees. More...

const java_bytecode_parse_treet &	get_original_class (const irep_idt &class_name)

Public Member Functions inherited from java_class_loader_baset
void	clear_classpath ()
	Clear all classpath entries. More...

void	add_classpath_entry (const std::string &, message_handlert &)
	Appends an entry to the class path, used for loading classes. More...

Private Member Functions
std::optional< std::vector< irep_idt > >	read_jar_file (const std::string &jar_path, message_handlert &)

Private Attributes
std::string	java_cp_include_files
	Either a regular expression matching files that will be allowed to be loaded or a string of the form `@PATH` where PATH is the file path of a json file storing an explicit list of files allowed to be loaded. More...

std::vector< irep_idt >	java_load_classes
	Classes to be explicitly loaded. More...

get_extra_class_refs_functiont	get_extra_class_refs

parse_tree_with_overridest_mapt	class_map
	Map from class names to the bytecode parse trees. More...

Additional Inherited Members
Static Public Member Functions inherited from java_class_loader_baset
static std::string	file_to_class_name (const std::string &)
	Convert a file name to the class name. More...

static std::string	class_name_to_os_file (const irep_idt &)
	Convert a class name to a file name, with OS-dependent syntax. More...

static std::string	class_name_to_jar_file (const irep_idt &)
	Convert a class name to a file name, does the inverse of file_to_class_name. More...

Public Attributes inherited from java_class_loader_baset
jar_poolt	jar_pool
	a cache for jar_filet, by path name More...

Protected Member Functions inherited from java_class_loader_baset
std::optional< java_bytecode_parse_treet >	load_class (const irep_idt &class_name, const classpath_entryt &, message_handlert &)
	attempt to load a class from a classpath_entry More...

std::optional< java_bytecode_parse_treet >	get_class_from_jar (const irep_idt &class_name, const std::string &jar_file, message_handlert &)
	attempt to load a class from a given jar file More...

std::optional< java_bytecode_parse_treet >	get_class_from_directory (const irep_idt &class_name, const std::string &path, message_handlert &)
	attempt to load a class from a given directory More...

Protected Attributes inherited from java_class_loader_baset
std::list< classpath_entryt >	classpath_entries
	List of entries in the classpath. More...

Detailed Description

Class responsible to load .class files.

Either directly from a specific file, from a classpath specification or from a Java archive (JAR) file.

Definition at line 25 of file java_class_loader.h.

Member Typedef Documentation

◆ get_extra_class_refs_functiont

typedef std::function<std::vector<irep_idt>const irep_idt &)> java_class_loadert::get_extra_class_refs_functiont

A function that yields a list of extra dependencies based on a class name.

Definition at line 37 of file java_class_loader.h.

◆ parse_tree_with_overlayst

typedef std::list<java_bytecode_parse_treet> java_class_loadert::parse_tree_with_overlayst

A list of parse trees supporting overlay classes.

Definition at line 29 of file java_class_loader.h.

◆ parse_tree_with_overridest_mapt

typedef std::map<irep_idt, parse_tree_with_overlayst> java_class_loadert::parse_tree_with_overridest_mapt

A map from class names to list of parse tree where multiple entries can exist in case of overlay classes.

Definition at line 33 of file java_class_loader.h.

Constructor & Destructor Documentation

◆ java_class_loadert()

java_class_loadert::java_class_loadert ( )

inline

Definition at line 39 of file java_class_loader.h.

Member Function Documentation

◆ add_load_classes()

void java_class_loadert::add_load_classes ( const std::vector< irep_idt > & classes )

inline

Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference.

Parameters

classes list of class identifiers

Definition at line 72 of file java_class_loader.h.

◆ can_load_class()

bool java_class_loadert::can_load_class	(	const irep_idt &	class_name,
		message_handlert &	message_handler
	)

Checks whether class_name is parseable from the classpath, ignoring class loading limits.

Definition at line 107 of file java_class_loader.cpp.

◆ get_class_with_overlays_map()

fixed_keys_map_wrappert<parse_tree_with_overridest_mapt> java_class_loadert::get_class_with_overlays_map ( )

inline

Map from class names to the bytecode parse trees.

Definition at line 83 of file java_class_loader.h.

◆ get_original_class()

const java_bytecode_parse_treet& java_class_loadert::get_original_class ( const irep_idt & class_name )

inline

Definition at line 87 of file java_class_loader.h.

◆ get_parse_tree()

java_class_loadert::parse_tree_with_overlayst & java_class_loadert::get_parse_tree	(	java_class_loader_limitt &	class_loader_limit,
		const irep_idt &	class_name,
		message_handlert &	message_handler
	)

Check through all the places class parse trees can appear and returns the first implementation it finds plus any overlay class implementations.

Uses class_loader_limit to limit the class files that it might (directly or indirectly) load and returns a default-constructed parse tree when unable to find the .class file.

Parameters

class_loader_limit	Filter to decide whether to load classes
class_name	Name of class to load
message_handler	message handler

Returns: The list of valid implementations, including overlays

Remarks: Allows multiple definitions of the same class to appear on the classpath, so long as all but the first definition are marked with the attribute \@java::org.cprover.OverlayClassImplementation.

Definition at line 134 of file java_class_loader.cpp.

◆ load_entire_jar()

std::vector< irep_idt > java_class_loadert::load_entire_jar	(	const std::string &	jar_path,
		message_handlert &	message_handler
	)

Load all class files from a .jar file.

Parameters

jar_path	the path for the .jar to load
message_handler	message handler

Definition at line 212 of file java_class_loader.cpp.

◆ operator()()

java_class_loadert::parse_tree_with_overlayst & java_class_loadert::operator()	(	const irep_idt &	class_name,
		message_handlert &	message_handler
	)

Definition at line 18 of file java_class_loader.cpp.

◆ read_jar_file()

std::optional< std::vector< irep_idt > > java_class_loadert::read_jar_file	(	const std::string &	jar_path,
		message_handlert &	message_handler
	)

private

Definition at line 231 of file java_class_loader.cpp.

◆ set_extra_class_refs_function()

void java_class_loadert::set_extra_class_refs_function ( get_extra_class_refs_functiont func )

inline

Sets a function that provides extra dependencies for a particular class.

Currently used by the string preprocessor to note that even if we don't have a definition of core string types, it will nontheless give them certain known superclasses and interfaces, such as Serializable.

Definition at line 65 of file java_class_loader.h.

◆ set_java_cp_include_files()

void java_class_loadert::set_java_cp_include_files ( const std::string & cp_include_files )

inline

Set the argument of the class loader limit java_class_loader_limitt.

Parameters

cp_include_files argument string for java_class_loader_limit

Definition at line 57 of file java_class_loader.h.

Member Data Documentation

◆ class_map

parse_tree_with_overridest_mapt java_class_loadert::class_map

private

Map from class names to the bytecode parse trees.

Definition at line 106 of file java_class_loader.h.

◆ get_extra_class_refs

get_extra_class_refs_functiont java_class_loadert::get_extra_class_refs

private

Definition at line 103 of file java_class_loader.h.

◆ java_cp_include_files

std::string java_class_loadert::java_cp_include_files

private

Either a regular expression matching files that will be allowed to be loaded or a string of the form @PATH where PATH is the file path of a json file storing an explicit list of files allowed to be loaded.

See java_class_loader_limitt::setup_class_load_limit() for further information.

Definition at line 99 of file java_class_loader.h.

◆ java_load_classes

std::vector<irep_idt> java_class_loadert::java_load_classes

private

Classes to be explicitly loaded.

Definition at line 102 of file java_class_loader.h.

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

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

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ get_extra_class_refs_functiont

◆ parse_tree_with_overlayst

◆ parse_tree_with_overridest_mapt

Constructor & Destructor Documentation

◆ java_class_loadert()

Member Function Documentation

◆ add_load_classes()

◆ can_load_class()

◆ get_class_with_overlays_map()

◆ get_original_class()

◆ get_parse_tree()

◆ load_entire_jar()

◆ operator()()

◆ read_jar_file()

◆ set_extra_class_refs_function()

◆ set_java_cp_include_files()

Member Data Documentation

◆ class_map

◆ get_extra_class_refs

◆ java_cp_include_files

◆ java_load_classes