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.

std::vector< irep_idt > java_load_classes

Classes to be explicitly loaded.

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.

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.

static std::string class_name_to_os_file (const irep_idt &)

Convert a class name to a file name, with OS-dependent syntax.

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.

- Public Attributes inherited from java_class_loader_baset

jar_poolt jar_pool

a cache for jar_filet, by path name

- 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

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

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

- Protected Attributes inherited from java_class_loader_baset

std::list< classpath_entryt > classpath_entries

List of entries in the classpath.

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