cprover
java_class_loadert Class Reference

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_treetparse_tree_with_overlayst
 A list of parse trees supporting overlay classes. More...
 
typedef std::map< irep_idt, parse_tree_with_overlaystparse_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 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)
 
bool can_load_class (const irep_idt &class_name)
 Checks whether class_name is parseable from the classpath, ignoring class loading limits. More...
 
parse_tree_with_overlaystget_parse_tree (java_class_loader_limitt &class_loader_limit, const irep_idt &class_name)
 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_idtload_entire_jar (const std::string &jar_path)
 Load all class files from a .jar file. More...
 
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)
 
- Public Member Functions inherited from java_class_loader_baset
void clear_classpath ()
 Clear all classpath entries. More...
 
void add_classpath_entry (const std::string &)
 Appends an entry to the class path, used for loading classes. 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Private Member Functions

optionalt< std::vector< irep_idt > > read_jar_file (const std::string &jar_path)
 

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_idtjava_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...
 
- 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...
 
- Public Attributes inherited from java_class_loader_baset
jar_poolt jar_pool
 a cache for jar_filet, by path name 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...
 
- Protected Member Functions inherited from java_class_loader_baset
optionalt< java_bytecode_parse_treetload_class (const irep_idt &class_name, const classpath_entryt &)
 attempt to load a class from a classpath_entry More...
 
optionalt< java_bytecode_parse_treetget_class_from_jar (const irep_idt &class_name, const std::string &jar_file)
 attempt to load a class from a given jar file More...
 
optionalt< java_bytecode_parse_treetget_class_from_directory (const irep_idt &class_name, const std::string &path)
 attempt to load a class from a given directory More...
 
- Protected Attributes inherited from java_class_loader_baset
std::list< classpath_entrytclasspath_entries
 List of entries in the classpath. More...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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

◆ parse_tree_with_overlayst

A list of parse trees supporting overlay classes.

Definition at line 30 of file java_class_loader.h.

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

Constructor & Destructor Documentation

◆ java_class_loadert()

java_class_loadert::java_class_loadert ( )
inline

Definition at line 40 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
classeslist of class identifiers

Definition at line 71 of file java_class_loader.h.

◆ can_load_class()

bool java_class_loadert::can_load_class ( const irep_idt class_name)

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

Definition at line 106 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 81 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 85 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 
)

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_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::org.cprover.OverlayClassImplementation.

Definition at line 130 of file java_class_loader.cpp.

◆ load_entire_jar()

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

Load all class files from a .jar file.

Parameters
jar_paththe path for the .jar to load

Definition at line 202 of file java_class_loader.cpp.

◆ operator()()

java_class_loadert::parse_tree_with_overlayst & java_class_loadert::operator() ( const irep_idt class_name)

Definition at line 19 of file java_class_loader.cpp.

◆ read_jar_file()

optionalt< std::vector< irep_idt > > java_class_loadert::read_jar_file ( const std::string &  jar_path)
private

Definition at line 221 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 64 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_filesargument string for java_class_loader_limit

Definition at line 56 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 104 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 101 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 97 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 100 of file java_class_loader.h.


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