cprover
|
#include <java_class_loader.h>
Public Types | |
typedef std::map< irep_idt, std::string > | jar_indext |
A map associating logical class names with the name of the .class file implementing it for all classes inside a single JAR file. More... | |
typedef std::list< java_bytecode_parse_treet > | parse_tree_with_overlayst |
typedef std::map< irep_idt, parse_tree_with_overlayst > | parse_tree_with_overridest_mapt |
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) |
parse_tree_with_overlayst & | get_parse_tree (java_class_loader_limitt &class_loader_limit, const irep_idt &class_name) |
Given a class_name (e.g. More... | |
void | set_java_cp_include_files (const std::string &java_cp_include_files) |
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... | |
void | add_jar_file (const std::string &f) |
void | load_entire_jar (java_class_loader_limitt &, const std::string &jar_path) |
const jar_indext & | get_jar_index (const std::string &jar_path) |
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) |
jar_filet & | jar_pool (java_class_loader_limitt &limit, const std::string &filename) |
Load jar archive or retrieve from cache if already loaded. More... | |
jar_filet & | jar_pool (java_class_loader_limitt &limit, const std::string &buffer_name, const void *pmem, size_t size) |
Load jar archive or retrieve from cache if already loaded. More... | |
Static Public Member Functions | |
static std::string | file_to_class_name (const std::string &) |
static std::string | class_name_to_file (const irep_idt &) |
Private Types | |
typedef optionalt< std::reference_wrapper< const jar_indext > > | jar_index_optcreft |
Private Member Functions | |
jar_index_optcreft | read_jar_file (java_class_loader_limitt &class_loader_limit, const std::string &jar_path) |
optionalt< java_bytecode_parse_treet > | get_class_from_jar (const irep_idt &class_name, const std::string &jar_file, const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit) |
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::list< std::string > | jar_files |
List of filesystem paths to .jar files that will be used, in the given order, to find and load a class, provided its name (see get_parse_tree). More... | |
std::vector< irep_idt > | java_load_classes |
Classes to be explicitly loaded. More... | |
get_extra_class_refs_functiont | get_extra_class_refs |
std::map< std::string, jar_indext > | jars_by_path |
The jar_indext for each jar file we've read. More... | |
std::map< std::string, jar_filet > | m_archives |
Jar files that have been loaded. More... | |
parse_tree_with_overridest_mapt | class_map |
Map from class names to the bytecode parse trees. More... | |
Additional Inherited Members |
Definition at line 24 of file java_class_loader.h.
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.
|
private |
Definition at line 147 of file java_class_loader.h.
typedef std::map<irep_idt, std::string> java_class_loadert::jar_indext |
A map associating logical class names with the name of the .class file implementing it for all classes inside a single JAR file.
Definition at line 29 of file java_class_loader.h.
typedef std::list<java_bytecode_parse_treet> java_class_loadert::parse_tree_with_overlayst |
Definition at line 31 of file java_class_loader.h.
typedef std::map<irep_idt, parse_tree_with_overlayst> java_class_loadert::parse_tree_with_overridest_mapt |
Definition at line 33 of file java_class_loader.h.
|
inline |
Definition at line 39 of file java_class_loader.h.
|
inline |
Definition at line 76 of file java_class_loader.h.
References jar_files.
Referenced by java_bytecode_languaget::parse().
|
inline |
Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference.
classes | list of class identifiers |
Definition at line 71 of file java_class_loader.h.
References java_load_classes.
Referenced by java_bytecode_languaget::parse().
|
static |
Definition at line 312 of file java_class_loader.cpp.
References id2string(), and messaget::result().
Referenced by get_parse_tree().
|
static |
Definition at line 285 of file java_class_loader.cpp.
References has_prefix(), has_suffix(), and messaget::result().
Referenced by java_bytecode_languaget::parse(), and read_jar_file().
|
private |
Definition at line 72 of file java_class_loader.cpp.
References messaget::debug(), messaget::eom(), jar_filet::get_entry(), messaget::get_message_handler(), jar_pool(), and java_bytecode_parse().
Referenced by get_parse_tree().
|
inline |
Map from class names to the bytecode parse trees.
Definition at line 92 of file java_class_loader.h.
References class_map.
Referenced by java_bytecode_languaget::typecheck().
|
inline |
Definition at line 86 of file java_class_loader.h.
References jars_by_path.
Referenced by java_bytecode_languaget::parse().
|
inline |
Definition at line 96 of file java_class_loader.h.
References class_map.
Referenced by ci_lazy_methodst::entry_point_methods().
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 | ||
) |
Given a class_name
(e.g.
Check through all the places class parse trees can appear and returns the first implementation it finds plus any overlay class implementations.
"java.lang.Thread") try to load the corresponding .class file by first scanning all .jar files whose pathname is stored in jar_files, and if that doesn't work, then scan the actual filesystem using config.java.classpath
as class path. Uses 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.
class_loader_limit | Filter to decide whether to load classes |
class_name | Name of class to load |
\@java::com.diffblue.OverlayClassImplementation
. Definition at line 112 of file java_class_loader.cpp.
References class_map, class_name_to_file(), configt::javat::classpath, config, messaget::debug(), messaget::eom(), get_class_from_jar(), messaget::get_message_handler(), has_suffix(), is_overlay_class(), jar_files, configt::java, java_bytecode_parse(), java_class_loader_limitt::load_class_file(), java_bytecode_parse_treet::classt::name, java_bytecode_parse_treet::parsed_class, PRECONDITION, read_jar_file(), and messaget::warning().
Referenced by operator()().
jar_filet & java_class_loadert::jar_pool | ( | java_class_loader_limitt & | limit, |
const std::string & | filename | ||
) |
Load jar archive or retrieve from cache if already loaded.
limit | |
filename | name of the file |
Definition at line 333 of file java_class_loader.cpp.
References m_archives.
Referenced by get_class_from_jar(), java_bytecode_languaget::parse(), and read_jar_file().
jar_filet & java_class_loadert::jar_pool | ( | java_class_loader_limitt & | limit, |
const std::string & | buffer_name, | ||
const void * | pmem, | ||
size_t | size | ||
) |
Load jar archive or retrieve from cache if already loaded.
limit | |
buffer_name | name of the original file |
pmem | memory pointer to the contents of the file |
size | size of the memory buffer Note that this mocks the existence of a file which may or may not exist since the actual data bis retrieved from memory. |
Definition at line 348 of file java_class_loader.cpp.
References m_archives.
void java_class_loadert::load_entire_jar | ( | java_class_loader_limitt & | class_loader_limit, |
const std::string & | jar_path | ||
) |
Definition at line 232 of file java_class_loader.cpp.
References jar_files, and read_jar_file().
Referenced by java_bytecode_languaget::parse().
java_class_loadert::parse_tree_with_overlayst & java_class_loadert::operator() | ( | const irep_idt & | class_name | ) |
Definition at line 20 of file java_class_loader.cpp.
References class_map, messaget::debug(), messaget::eom(), get_extra_class_refs, messaget::get_message_handler(), get_parse_tree(), java_cp_include_files, and java_load_classes.
|
private |
Definition at line 248 of file java_class_loader.cpp.
References messaget::debug(), messaget::eom(), messaget::error(), file_to_class_name(), jar_filet::filenames(), has_suffix(), jar_pool(), and jars_by_path.
Referenced by get_parse_tree(), and load_entire_jar().
|
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 64 of file java_class_loader.h.
References get_extra_class_refs.
Referenced by java_bytecode_languaget::parse().
|
inline |
Definition at line 56 of file java_class_loader.h.
References java_cp_include_files.
Referenced by java_bytecode_languaget::parse().
|
private |
Map from class names to the bytecode parse trees.
Definition at line 144 of file java_class_loader.h.
Referenced by get_class_with_overlays_map(), get_original_class(), get_parse_tree(), and operator()().
|
private |
Definition at line 136 of file java_class_loader.h.
Referenced by operator()(), and set_extra_class_refs_function().
|
private |
List of filesystem paths to .jar files that will be used, in the given order, to find and load a class, provided its name (see get_parse_tree).
Definition at line 132 of file java_class_loader.h.
Referenced by add_jar_file(), get_parse_tree(), and load_entire_jar().
|
private |
The jar_indext for each jar file we've read.
Definition at line 139 of file java_class_loader.h.
Referenced by get_jar_index(), and read_jar_file().
|
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 127 of file java_class_loader.h.
Referenced by operator()(), and set_java_cp_include_files().
|
private |
Classes to be explicitly loaded.
Definition at line 135 of file java_class_loader.h.
Referenced by add_load_classes(), and operator()().
|
private |
Jar files that have been loaded.
Definition at line 142 of file java_class_loader.h.
Referenced by jar_pool().