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

Classes

class  bytecodet
 
struct  pool_entryt
 

Public Types

typedef java_bytecode_parse_treet::classt classt
 
typedef java_bytecode_parse_treet::classt::fieldst fieldst
 
typedef java_bytecode_parse_treet::classt::methodst methodst
 
typedef java_bytecode_parse_treet::methodt methodt
 
typedef java_bytecode_parse_treet::fieldt fieldt
 
typedef java_bytecode_parse_treet::methodt::instructionst instructionst
 
typedef java_bytecode_parse_treet::instructiont instructiont
 
typedef java_bytecode_parse_treet::annotationt annotationt
 
typedef java_bytecode_parse_treet::annotationst annotationst
 
typedef java_bytecode_parse_treet::classt::method_handle_typet method_handle_typet
 
typedef java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
 
typedef java_bytecode_parse_treet::classt::u2_valuest u2_valuest
 
typedef std::vector< pool_entrytconstant_poolt
 
- 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_parsert (bool skip_instructions)
 
virtual bool parse ()
 
- Public Member Functions inherited from parsert
virtual void clear ()
 
 parsert ()
 
virtual ~parsert ()
 
bool read (char &ch)
 
bool eof ()
 
void parse_error (const std::string &message, const std::string &before)
 
void inc_line_no ()
 
void set_line_no (unsigned _line_no)
 
void set_file (const irep_idt &file)
 
irep_idt get_file () const
 
unsigned get_line_no () const
 
unsigned get_column () const
 
void set_column (unsigned _column)
 
void set_source_location (exprt &e)
 
void set_function (const irep_idt &function)
 
void advance_column (unsigned token_width)
 
- 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...
 

Public Attributes

java_bytecode_parse_treet parse_tree
 
constant_poolt constant_pool
 
- Public Attributes inherited from parsert
std::istream * in
 
std::string this_line
 
std::string last_line
 
std::vector< exprtstack
 

Protected Member Functions

pool_entrytpool_entry (u2 index)
 
exprtconstant (u2 index)
 
const typet type_entry (u2 index)
 
void populate_bytecode_mnemonics_table ()
 
void rClassFile ()
 
void rconstant_pool ()
 
void rinterfaces (classt &parsed_class)
 
void rfields (classt &parsed_class)
 
void rmethods (classt &parsed_class)
 
void rmethod (classt &parsed_class)
 
void rinner_classes_attribute (classt &parsed_class, const u4 &attribute_length)
 Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6 Parses the InnerClasses attribute for the current parsed class, which contains an array of information about its inner classes. More...
 
std::vector< irep_idtrexceptions_attribute ()
 Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5 Parses the Exceptions attribute for the current method, and returns a vector of exceptions. More...
 
void rclass_attribute (classt &parsed_class)
 
void rRuntimeAnnotation_attribute (annotationst &)
 
void rRuntimeAnnotation (annotationt &)
 
void relement_value_pairs (annotationt::element_value_pairst &)
 
exprt get_relement_value ()
 Corresponds to the element_value structure Described in Java 8 specification 4.7.16.1 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1. More...
 
void rmethod_attribute (methodt &method)
 
void rfield_attribute (fieldt &)
 
void rcode_attribute (methodt &method)
 
void read_verification_type_info (methodt::verification_type_infot &)
 
void rbytecode (methodt::instructionst &)
 
void get_class_refs ()
 Get the class references for the benefit of a dependency analysis. More...
 
void get_class_refs_rec (const typet &)
 
void get_annotation_class_refs (const java_bytecode_parse_treet::annotationst &annotations)
 For each of the given annotations, get a reference to its class and recursively get class references of the values it stores. More...
 
void get_annotation_value_class_refs (const exprt &value)
 See java_bytecode_parsert::get_annotation_class_refs. More...
 
void parse_local_variable_type_table (methodt &method)
 Parses the local variable type table of a method. More...
 
optionalt< lambda_method_handletparse_method_handle (const class method_handle_infot &entry)
 Read method handle pointed to from constant pool entry at index, return type of method handle and name if lambda function is found. More...
 
void read_bootstrapmethods_entry (classt &)
 Read all entries of the BootstrapMethods attribute of a class file. More...
 
void skip_bytes (std::size_t bytes)
 
u8 read_bytes (size_t bytes)
 
u1 read_u1 ()
 
u2 read_u2 ()
 
u4 read_u4 ()
 
u8 read_u8 ()
 
void store_unknown_method_handle (classt &parsed_class, size_t bootstrap_method_index, u2_valuest u2_values) const
 Creates an unknown method handle and puts it into the parsed_class. More...
 

Protected Attributes

std::vector< bytecodetbytecodes
 
const bool skip_instructions = false
 
- Protected Attributes inherited from parsert
source_locationt source_location
 
unsigned line_no
 
unsigned previous_line_no
 
unsigned column
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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...
 

Detailed Description

Definition at line 32 of file java_bytecode_parser.cpp.

Member Typedef Documentation

◆ annotationst

◆ annotationt

◆ classt

◆ constant_poolt

Definition at line 70 of file java_bytecode_parser.cpp.

◆ fieldst

◆ fieldt

◆ instructionst

◆ instructiont

◆ lambda_method_handlet

◆ method_handle_typet

◆ methodst

◆ methodt

◆ u2_valuest

Constructor & Destructor Documentation

◆ java_bytecode_parsert()

java_bytecode_parsert::java_bytecode_parsert ( bool  skip_instructions)
inlineexplicit

Definition at line 35 of file java_bytecode_parser.cpp.

Member Function Documentation

◆ constant()

exprt& java_bytecode_parsert::constant ( u2  index)
inlineprotected

Definition at line 96 of file java_bytecode_parser.cpp.

◆ get_annotation_class_refs()

void java_bytecode_parsert::get_annotation_class_refs ( const java_bytecode_parse_treet::annotationst annotations)
protected

For each of the given annotations, get a reference to its class and recursively get class references of the values it stores.

Definition at line 656 of file java_bytecode_parser.cpp.

◆ get_annotation_value_class_refs()

void java_bytecode_parsert::get_annotation_value_class_refs ( const exprt value)
protected

◆ get_class_refs()

void java_bytecode_parsert::get_class_refs ( )
protected

Get the class references for the benefit of a dependency analysis.

Definition at line 539 of file java_bytecode_parser.cpp.

◆ get_class_refs_rec()

void java_bytecode_parsert::get_class_refs_rec ( const typet src)
protected

Definition at line 622 of file java_bytecode_parser.cpp.

◆ get_relement_value()

exprt java_bytecode_parsert::get_relement_value ( )
protected

Corresponds to the element_value structure Described in Java 8 specification 4.7.16.1 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1.

Returns
An exprt that represents the particular value of annotations field. This is usually one of: a byte, number of some sort, string, character, enum, Class type, array or another annotation.

Definition at line 1586 of file java_bytecode_parser.cpp.

◆ parse()

bool java_bytecode_parsert::parse ( )
virtual

Implements parsert.

Definition at line 430 of file java_bytecode_parser.cpp.

◆ parse_local_variable_type_table()

void java_bytecode_parsert::parse_local_variable_type_table ( methodt method)
protected

Parses the local variable type table of a method.

The LVTT holds generic type information for variables in the local variable table (LVT). At most as many variables as present in the LVT can be in the LVTT.

Definition at line 1911 of file java_bytecode_parser.cpp.

◆ parse_method_handle()

optionalt< java_bytecode_parsert::lambda_method_handlet > java_bytecode_parsert::parse_method_handle ( const class method_handle_infot entry)
protected

Read method handle pointed to from constant pool entry at index, return type of method handle and name if lambda function is found.

Parameters
entrythe constant pool entry of the methodhandle_info structure
Returns
: the method_handle type of the methodhandle_structure, either for a recognized bootstrap method or for a lambda function

Definition at line 1953 of file java_bytecode_parser.cpp.

◆ pool_entry()

pool_entryt& java_bytecode_parsert::pool_entry ( u2  index)
inlineprotected

Definition at line 84 of file java_bytecode_parser.cpp.

◆ populate_bytecode_mnemonics_table()

void java_bytecode_parsert::populate_bytecode_mnemonics_table ( )
inlineprotected

Definition at line 106 of file java_bytecode_parser.cpp.

◆ rbytecode()

void java_bytecode_parsert::rbytecode ( methodt::instructionst instructions)
protected

Definition at line 954 of file java_bytecode_parser.cpp.

◆ rclass_attribute()

void java_bytecode_parsert::rclass_attribute ( classt parsed_class)
protected

Definition at line 1741 of file java_bytecode_parser.cpp.

◆ rClassFile()

void java_bytecode_parsert::rClassFile ( )
protected

Definition at line 475 of file java_bytecode_parser.cpp.

◆ rcode_attribute()

void java_bytecode_parsert::rcode_attribute ( methodt method)
protected

Definition at line 1337 of file java_bytecode_parser.cpp.

◆ rconstant_pool()

void java_bytecode_parsert::rconstant_pool ( )
protected

Definition at line 689 of file java_bytecode_parser.cpp.

◆ read_bootstrapmethods_entry()

void java_bytecode_parsert::read_bootstrapmethods_entry ( classt parsed_class)
protected

Read all entries of the BootstrapMethods attribute of a class file.

Parameters
parsed_classthe class representation of the class file that is currently parsed

Definition at line 1996 of file java_bytecode_parser.cpp.

◆ read_bytes()

u8 java_bytecode_parsert::read_bytes ( size_t  bytes)
inlineprotected

Definition at line 165 of file java_bytecode_parser.cpp.

◆ read_u1()

u1 java_bytecode_parsert::read_u1 ( )
inlineprotected

Definition at line 181 of file java_bytecode_parser.cpp.

◆ read_u2()

u2 java_bytecode_parsert::read_u2 ( )
inlineprotected

Definition at line 186 of file java_bytecode_parser.cpp.

◆ read_u4()

u4 java_bytecode_parsert::read_u4 ( )
inlineprotected

Definition at line 191 of file java_bytecode_parser.cpp.

◆ read_u8()

u8 java_bytecode_parsert::read_u8 ( )
inlineprotected

Definition at line 196 of file java_bytecode_parser.cpp.

◆ read_verification_type_info()

void java_bytecode_parsert::read_verification_type_info ( methodt::verification_type_infot v)
protected

Definition at line 1505 of file java_bytecode_parser.cpp.

◆ relement_value_pairs()

void java_bytecode_parsert::relement_value_pairs ( annotationt::element_value_pairst element_value_pairs)
protected

Definition at line 1566 of file java_bytecode_parser.cpp.

◆ rexceptions_attribute()

std::vector< irep_idt > java_bytecode_parsert::rexceptions_attribute ( )
protected

Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5 Parses the Exceptions attribute for the current method, and returns a vector of exceptions.

Definition at line 1726 of file java_bytecode_parser.cpp.

◆ rfield_attribute()

void java_bytecode_parsert::rfield_attribute ( fieldt field)
protected

Definition at line 1316 of file java_bytecode_parser.cpp.

◆ rfields()

void java_bytecode_parsert::rfields ( classt parsed_class)
protected

Definition at line 913 of file java_bytecode_parser.cpp.

◆ rinner_classes_attribute()

void java_bytecode_parsert::rinner_classes_attribute ( classt parsed_class,
const u4 attribute_length 
)
protected

Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6 Parses the InnerClasses attribute for the current parsed class, which contains an array of information about its inner classes.

We are interested in getting information only for inner classes, which is determined by checking if the parsed class matches any of the inner classes in its inner class array. If the parsed class is not an inner class, then it is ignored. When a parsed class is an inner class, the accessibility information for the parsed class is overwritten, and the parsed class is marked as an inner class.

Definition at line 1651 of file java_bytecode_parser.cpp.

◆ rinterfaces()

void java_bytecode_parsert::rinterfaces ( classt parsed_class)
protected

Definition at line 904 of file java_bytecode_parser.cpp.

◆ rmethod()

void java_bytecode_parsert::rmethod ( classt parsed_class)
protected

Definition at line 1837 of file java_bytecode_parser.cpp.

◆ rmethod_attribute()

void java_bytecode_parsert::rmethod_attribute ( methodt method)
protected

Definition at line 1217 of file java_bytecode_parser.cpp.

◆ rmethods()

void java_bytecode_parsert::rmethods ( classt parsed_class)
protected

Definition at line 1814 of file java_bytecode_parser.cpp.

◆ rRuntimeAnnotation()

void java_bytecode_parsert::rRuntimeAnnotation ( annotationt annotation)
protected

Definition at line 1558 of file java_bytecode_parser.cpp.

◆ rRuntimeAnnotation_attribute()

void java_bytecode_parsert::rRuntimeAnnotation_attribute ( annotationst annotations)
protected

Definition at line 1545 of file java_bytecode_parser.cpp.

◆ skip_bytes()

void java_bytecode_parsert::skip_bytes ( std::size_t  bytes)
inlineprotected

Definition at line 152 of file java_bytecode_parser.cpp.

◆ store_unknown_method_handle()

void java_bytecode_parsert::store_unknown_method_handle ( java_bytecode_parsert::classt parsed_class,
size_t  bootstrap_method_index,
java_bytecode_parsert::u2_valuest  u2_values 
) const
protected

Creates an unknown method handle and puts it into the parsed_class.

Parameters
parsed_classThe class whose bootstrap method handles we are using
bootstrap_method_indexThe current index in the bootstrap entry table
u2_valuesThe indices of the arguments for the call

Definition at line 2139 of file java_bytecode_parser.cpp.

◆ type_entry()

const typet java_bytecode_parsert::type_entry ( u2  index)
inlineprotected

Definition at line 101 of file java_bytecode_parser.cpp.

Member Data Documentation

◆ bytecodes

std::vector<bytecodet> java_bytecode_parsert::bytecodes
protected

Definition at line 81 of file java_bytecode_parser.cpp.

◆ constant_pool

constant_poolt java_bytecode_parsert::constant_pool

Definition at line 71 of file java_bytecode_parser.cpp.

◆ parse_tree

java_bytecode_parse_treet java_bytecode_parsert::parse_tree

Definition at line 58 of file java_bytecode_parser.cpp.

◆ skip_instructions

const bool java_bytecode_parsert::skip_instructions = false
protected

Definition at line 82 of file java_bytecode_parser.cpp.


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