cprover
java_class_loadert Class Reference

#include <java_class_loader.h>

Inheritance diagram for java_class_loadert:
[legend]
Collaboration diagram for java_class_loadert:
[legend]

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_treetparse_tree_with_overlayst
 
typedef std::map< irep_idt, parse_tree_with_overlaystparse_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 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
}
 

Public Member Functions

 java_class_loadert ()
 
parse_tree_with_overlaystoperator() (const irep_idt &class_name)
 
parse_tree_with_overlaystget_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_indextget_jar_index (const std::string &jar_path)
 
fixed_keys_map_wrappert< parse_tree_with_overridest_maptget_class_with_overlays_map ()
 Map from class names to the bytecode parse trees. More...
 
const java_bytecode_parse_treetget_original_class (const irep_idt &class_name)
 
jar_filetjar_pool (java_class_loader_limitt &limit, const std::string &filename)
 Load jar archive or retrieve from cache if already loaded. More...
 
jar_filetjar_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...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. 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 &)
 
- 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

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_treetget_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_idtjava_load_classes
 Classes to be explicitly loaded. More...
 
get_extra_class_refs_functiont get_extra_class_refs
 
std::map< std::string, jar_indextjars_by_path
 The jar_indext for each jar file we've read. More...
 
std::map< std::string, jar_filetm_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

- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

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

◆ jar_index_optcreft

typedef optionalt<std::reference_wrapper<const jar_indext> > java_class_loadert::jar_index_optcreft
private

Definition at line 147 of file java_class_loader.h.

◆ jar_indext

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.

◆ parse_tree_with_overlayst

◆ parse_tree_with_overridest_mapt

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

void java_class_loadert::add_jar_file ( const std::string &  f)
inline

Definition at line 76 of file java_class_loader.h.

References jar_files.

Referenced by java_bytecode_languaget::parse().

◆ 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
classeslist of class identifiers

Definition at line 71 of file java_class_loader.h.

References java_load_classes.

Referenced by java_bytecode_languaget::parse().

◆ class_name_to_file()

std::string java_class_loadert::class_name_to_file ( const irep_idt class_name)
static

Definition at line 304 of file java_class_loader.cpp.

References id2string(), and messaget::result().

Referenced by get_parse_tree().

◆ file_to_class_name()

std::string java_class_loadert::file_to_class_name ( const std::string &  file)
static

◆ get_class_from_jar()

optionalt< java_bytecode_parse_treet > java_class_loadert::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

◆ 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 92 of file java_class_loader.h.

References class_map.

Referenced by java_bytecode_languaget::typecheck().

◆ get_jar_index()

const jar_indext& java_class_loadert::get_jar_index ( const std::string &  jar_path)
inline

Definition at line 86 of file java_class_loader.h.

References jars_by_path.

Referenced by java_bytecode_languaget::parse().

◆ get_original_class()

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

Definition at line 96 of file java_class_loader.h.

References class_map.

Referenced by ci_lazy_methodst::entry_point_methods().

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

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.

Parameters
class_loader_limitFilter to decide whether to load classes
class_nameName of class to load
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::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_pool() [1/2]

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.

Parameters
limit
filenamename of the file

Definition at line 325 of file java_class_loader.cpp.

References m_archives.

Referenced by get_class_from_jar(), java_bytecode_languaget::parse(), and read_jar_file().

◆ jar_pool() [2/2]

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.

Parameters
limit
buffer_namename of the original file
pmemmemory pointer to the contents of the file
sizesize 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 340 of file java_class_loader.cpp.

References m_archives.

◆ load_entire_jar()

void java_class_loadert::load_entire_jar ( java_class_loader_limitt class_loader_limit,
const std::string &  jar_path 
)

Definition at line 224 of file java_class_loader.cpp.

References jar_files, and read_jar_file().

Referenced by java_bytecode_languaget::parse().

◆ operator()()

◆ read_jar_file()

java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file ( java_class_loader_limitt class_loader_limit,
const std::string &  jar_path 
)
private

◆ 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 64 of file java_class_loader.h.

References get_extra_class_refs.

Referenced by java_bytecode_languaget::parse().

◆ set_java_cp_include_files()

void java_class_loadert::set_java_cp_include_files ( const std::string &  java_cp_include_files)
inline

Definition at line 56 of file java_class_loader.h.

References java_cp_include_files.

Referenced by java_bytecode_languaget::parse().

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 144 of file java_class_loader.h.

Referenced by get_class_with_overlays_map(), get_original_class(), get_parse_tree(), and operator()().

◆ get_extra_class_refs

get_extra_class_refs_functiont java_class_loadert::get_extra_class_refs
private

Definition at line 136 of file java_class_loader.h.

Referenced by operator()(), and set_extra_class_refs_function().

◆ jar_files

std::list<std::string> java_class_loadert::jar_files
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().

◆ jars_by_path

std::map<std::string, jar_indext> java_class_loadert::jars_by_path
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().

◆ 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 127 of file java_class_loader.h.

Referenced by operator()(), and set_java_cp_include_files().

◆ java_load_classes

std::vector<irep_idt> java_class_loadert::java_load_classes
private

Classes to be explicitly loaded.

Definition at line 135 of file java_class_loader.h.

Referenced by add_load_classes(), and operator()().

◆ m_archives

std::map<std::string, jar_filet> java_class_loadert::m_archives
private

Jar files that have been loaded.

Definition at line 142 of file java_class_loader.h.

Referenced by jar_pool().


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