cprover
java_bytecode_convert_classt Class Reference
+ Inheritance diagram for java_bytecode_convert_classt:
+ Collaboration diagram for java_bytecode_convert_classt:

Public Types

typedef java_bytecode_parse_treet::classt classt
 
typedef java_bytecode_parse_treet::fieldt fieldt
 
typedef java_bytecode_parse_treet::methodt methodt
 
typedef java_bytecode_parse_treet::annotationt annotationt
 
- 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_bytecode_convert_classt (symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes)
 
void operator() (const java_class_loadert::parse_tree_with_overlayst &parse_trees)
 Converts all the class parse trees into a class symbol and adds it to the symbol table. 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 Types

typedef std::list< std::reference_wrapper< const classt > > overlay_classest
 

Private Member Functions

void convert (const classt &c, const overlay_classest &overlay_classes)
 Convert a class, adding symbols to the symbol table for its members. More...
 
void convert (symbolt &class_symbol, const fieldt &f)
 Convert a field, adding a symbol to teh symbol table for it. More...
 
bool check_field_exists (const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const
 

Static Private Member Functions

static void add_array_types (symbol_tablet &symbol_table)
 Register in the symbol_table new symbols for the objects java::array[X] where X is byte, float, int, char... More...
 
static bool is_overlay_method (const methodt &method)
 Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations. More...
 
static bool is_ignored_method (const methodt &method)
 Check if a method is an ignored method by searching for ID_ignored_method in its list of annotations. More...
 

Private Attributes

symbol_tabletsymbol_table
 
const size_t max_array_length
 
method_bytecodetmethod_bytecode
 
java_string_library_preprocesststring_preprocess
 
std::unordered_set< std::string > no_load_classes
 

Additional Inherited Members

- 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...
 
- 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 Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 31 of file java_bytecode_convert_class.cpp.

Member Typedef Documentation

◆ annotationt

◆ classt

◆ fieldt

◆ methodt

◆ overlay_classest

typedef std::list<std::reference_wrapper<const classt> > java_bytecode_convert_classt::overlay_classest
private

Definition at line 114 of file java_bytecode_convert_class.cpp.

Constructor & Destructor Documentation

◆ java_bytecode_convert_classt()

java_bytecode_convert_classt::java_bytecode_convert_classt ( symbol_tablet _symbol_table,
message_handlert _message_handler,
size_t  _max_array_length,
method_bytecodet method_bytecode,
java_string_library_preprocesst _string_preprocess,
const std::unordered_set< std::string > &  no_load_classes 
)
inline

Definition at line 34 of file java_bytecode_convert_class.cpp.

Member Function Documentation

◆ add_array_types()

void java_bytecode_convert_classt::add_array_types ( symbol_tablet symbol_table)
staticprivate

Register in the symbol_table new symbols for the objects java::array[X] where X is byte, float, int, char...

Definition at line 771 of file java_bytecode_convert_class.cpp.

◆ check_field_exists()

bool java_bytecode_convert_classt::check_field_exists ( const fieldt field,
const irep_idt qualified_fieldname,
const struct_union_typet::componentst fields 
) const
private

Definition at line 611 of file java_bytecode_convert_class.cpp.

◆ convert() [1/2]

void java_bytecode_convert_classt::convert ( const classt c,
const overlay_classest overlay_classes 
)
private

Convert a class, adding symbols to the symbol table for its members.

Parameters
cBytecode of the class to convert
overlay_classesBytecode of any overlays for the class to convert

Definition at line 263 of file java_bytecode_convert_class.cpp.

◆ convert() [2/2]

void java_bytecode_convert_classt::convert ( symbolt class_symbol,
const fieldt f 
)
private

Convert a field, adding a symbol to teh symbol table for it.

Parameters
class_symbolThe already added symbol for the containing class
fThe bytecode for the field to convert

this is for a free type variable, e.g., a field of the form T f;

this is for a field that holds a generic type, either with instantiated or with free type variables, e.g., List<T> l; or List<Integer> l;

Definition at line 632 of file java_bytecode_convert_class.cpp.

◆ is_ignored_method()

static bool java_bytecode_convert_classt::is_ignored_method ( const methodt method)
inlinestaticprivate

Check if a method is an ignored method by searching for ID_ignored_method in its list of annotations.

An ignored method is a method with the annotation @IgnoredMethodImplementation. They will be ignored by JBMC. They are intended for use in overlay classes, in particular for methods which must exist in the overlay class so that it will compile, e.g. default constructors, but which we do not want to overlay the corresponding method in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.

Parameters
methoda methodt object from a java bytecode parse tree
Returns
true if the method is an ignored method, else false

Definition at line 159 of file java_bytecode_convert_class.cpp.

◆ is_overlay_method()

static bool java_bytecode_convert_classt::is_overlay_method ( const methodt method)
inlinestaticprivate

Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.

An overlay method is a method with the annotation @OverlayMethodImplementation. They should only appear in overlay classes. They will be loaded by JBMC instead of the method with the same signature in the underlying class. It is an error if there is no method with the same signature in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.

Parameters
methoda methodt object from a java bytecode parse tree
Returns
true if the method is an overlay method, else false

Definition at line 136 of file java_bytecode_convert_class.cpp.

◆ operator()()

void java_bytecode_convert_classt::operator() ( const java_class_loadert::parse_tree_with_overlayst parse_trees)
inline

Converts all the class parse trees into a class symbol and adds it to the symbol table.

Parameters
parse_treesThe parse trees found for the class to be converted.
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. Overlay class definitions can contain methods with the same signature as methods in the original class, so long as these are marked with the attribute \@java::org.cprover.OverlayMethodImplementation; such overlay methods are replaced in the original file with the version found in the last overlay on the classpath. Later definitions can also contain new supporting methods and fields that are merged in. This will allow insertion of Java methods into library classes to handle, for example, modelling dependency injection.

Definition at line 65 of file java_bytecode_convert_class.cpp.

Member Data Documentation

◆ max_array_length

const size_t java_bytecode_convert_classt::max_array_length
private

Definition at line 109 of file java_bytecode_convert_class.cpp.

◆ method_bytecode

method_bytecodet& java_bytecode_convert_classt::method_bytecode
private

Definition at line 110 of file java_bytecode_convert_class.cpp.

◆ no_load_classes

std::unordered_set<std::string> java_bytecode_convert_classt::no_load_classes
private

Definition at line 169 of file java_bytecode_convert_class.cpp.

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_classt::string_preprocess
private

Definition at line 111 of file java_bytecode_convert_class.cpp.

◆ symbol_table

symbol_tablet& java_bytecode_convert_classt::symbol_table
private

Definition at line 108 of file java_bytecode_convert_class.cpp.


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