cprover
java_bytecode_parsert Class Reference
Inheritance diagram for java_bytecode_parsert:
[legend]
Collaboration diagram for java_bytecode_parsert:
[legend]

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 ()
 
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 mstream using output_generator if the configured verbosity is at least as high as that of mstream. 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 get_bytecodes ()
 
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 rclass_attribute (classt &parsed_class)
 
void rRuntimeAnnotation_attribute (annotationst &)
 
void rRuntimeAnnotation (annotationt &)
 
void relement_value_pairs (annotationt::element_value_pairst &)
 
void relement_value_pair (annotationt::element_value_pairt &)
 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 ()
 
void get_class_refs_rec (const typet &)
 
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
 
- 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 32 of file java_bytecode_parser.cpp.

Member Typedef Documentation

◆ annotationst

◆ annotationt

◆ classt

◆ constant_poolt

Definition at line 69 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 ( )
inline

Definition at line 35 of file java_bytecode_parser.cpp.

References get_bytecodes().

Member Function Documentation

◆ constant()

exprt& java_bytecode_parsert::constant ( u2  index)
inlineprotected

◆ get_bytecodes()

void java_bytecode_parsert::get_bytecodes ( )
inlineprotected

Definition at line 104 of file java_bytecode_parser.cpp.

References bytecode_info, bytecodes, and bytecode_infot::mnemonic.

Referenced by java_bytecode_parsert().

◆ get_class_refs()

◆ get_class_refs_rec()

◆ parse()

bool java_bytecode_parsert::parse ( )
virtual

Implements parsert.

Definition at line 417 of file java_bytecode_parser.cpp.

References messaget::eom(), messaget::error(), and rClassFile().

Referenced by java_bytecode_parse().

◆ 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 1735 of file java_bytecode_parser.cpp.

References id2string(), INVARIANT, java_bytecode_parse_treet::methodt::local_variable_table, pool_entry(), and read_u2().

Referenced by rcode_attribute().

◆ 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 1777 of file java_bytecode_parser.cpp.

References base_ref_infot::get_class(), name_and_type_infot::get_descriptor(), class_infot::get_name(), name_and_type_infot::get_name(), base_ref_infot::get_name_and_type(), method_handle_infot::get_reference(), java_bytecode_parse_treet::classt::lambda_method_handlet::handle_type, has_prefix(), java_bytecode_parse_treet::classt::LAMBDA_METHOD_HANDLE, java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_name, java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_ref, and pool_entry().

Referenced by read_bootstrapmethods_entry().

◆ pool_entry()

◆ rbytecode()

◆ rclass_attribute()

◆ rClassFile()

◆ rcode_attribute()

◆ rconstant_pool()

◆ read_bootstrapmethods_entry()

void java_bytecode_parsert::read_bootstrapmethods_entry ( classt parsed_class)
protected

◆ read_bytes()

u8 java_bytecode_parsert::read_bytes ( size_t  bytes)
inlineprotected

◆ read_u1()

u1 java_bytecode_parsert::read_u1 ( )
inlineprotected

◆ read_u2()

◆ read_u4()

u4 java_bytecode_parsert::read_u4 ( )
inlineprotected

◆ read_u8()

u8 java_bytecode_parsert::read_u8 ( )
inlineprotected

Definition at line 183 of file java_bytecode_parser.cpp.

References read_bytes().

Referenced by rconstant_pool().

◆ read_verification_type_info()

◆ relement_value_pair()

void java_bytecode_parsert::relement_value_pair ( annotationt::element_value_pairt element_value_pair)
protected

◆ relement_value_pairs()

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

◆ rfield_attribute()

◆ rfields()

◆ rinterfaces()

void java_bytecode_parsert::rinterfaces ( classt parsed_class)
protected

◆ rmethod()

◆ rmethod_attribute()

◆ rmethods()

void java_bytecode_parsert::rmethods ( classt parsed_class)
protected

Definition at line 1647 of file java_bytecode_parser.cpp.

References read_u2(), and rmethod().

Referenced by rClassFile().

◆ rRuntimeAnnotation()

◆ rRuntimeAnnotation_attribute()

void java_bytecode_parsert::rRuntimeAnnotation_attribute ( annotationst annotations)
protected

◆ skip_bytes()

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

◆ 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 1963 of file java_bytecode_parser.cpp.

References java_bytecode_parse_treet::classt::add_method_handle(), and java_bytecode_parse_treet::classt::lambda_method_handlet::create_unknown_handle().

Referenced by read_bootstrapmethods_entry().

◆ type_entry()

const typet java_bytecode_parsert::type_entry ( u2  index)
inlineprotected

Definition at line 99 of file java_bytecode_parser.cpp.

References id2string(), java_type_from_string(), and pool_entry().

Referenced by rconstant_pool(), and rRuntimeAnnotation().

Member Data Documentation

◆ bytecodes

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

Definition at line 80 of file java_bytecode_parser.cpp.

Referenced by get_bytecodes(), and rbytecode().

◆ constant_pool

constant_poolt java_bytecode_parsert::constant_pool

Definition at line 70 of file java_bytecode_parser.cpp.

Referenced by get_class_refs(), pool_entry(), and rconstant_pool().

◆ parse_tree


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