cprover
|
Classes | |
class | bytecodet |
struct | pool_entryt |
Public Member Functions | |
java_bytecode_parsert () | |
virtual bool | parse () |
![]() | |
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 Attributes | |
java_bytecode_parse_treet | parse_tree |
constant_poolt | constant_pool |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Protected Member Functions | |
pool_entryt & | pool_entry (u2 index) |
exprt & | constant (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_handlet > | parse_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< bytecodet > | bytecodes |
![]() | |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Additional Inherited Members |
Definition at line 32 of file java_bytecode_parser.cpp.
Definition at line 50 of file java_bytecode_parser.cpp.
Definition at line 49 of file java_bytecode_parser.cpp.
Definition at line 42 of file java_bytecode_parser.cpp.
typedef std::vector<pool_entryt> java_bytecode_parsert::constant_poolt |
Definition at line 69 of file java_bytecode_parser.cpp.
Definition at line 43 of file java_bytecode_parser.cpp.
Definition at line 46 of file java_bytecode_parser.cpp.
Definition at line 47 of file java_bytecode_parser.cpp.
Definition at line 48 of file java_bytecode_parser.cpp.
typedef java_bytecode_parse_treet::classt::lambda_method_handlet java_bytecode_parsert::lambda_method_handlet |
Definition at line 54 of file java_bytecode_parser.cpp.
typedef java_bytecode_parse_treet::classt::method_handle_typet java_bytecode_parsert::method_handle_typet |
Definition at line 52 of file java_bytecode_parser.cpp.
Definition at line 44 of file java_bytecode_parser.cpp.
Definition at line 45 of file java_bytecode_parser.cpp.
Definition at line 55 of file java_bytecode_parser.cpp.
|
inline |
Definition at line 35 of file java_bytecode_parser.cpp.
References get_bytecodes().
Definition at line 94 of file java_bytecode_parser.cpp.
References java_bytecode_parsert::pool_entryt::expr, and pool_entry().
Referenced by rbytecode(), rClassFile(), relement_value_pair(), and rinterfaces().
|
inlineprotected |
Definition at line 104 of file java_bytecode_parser.cpp.
References bytecode_info, bytecodes, and bytecode_infot::mnemonic.
Referenced by java_bytecode_parsert().
|
protected |
Definition at line 531 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::class_refs, CONSTANT_Class, CONSTANT_NameAndType, constant_pool, java_bytecode_parse_treet::classt::fields, get_class_refs_rec(), get_dependencies_from_generic_parameters(), id2string(), java_type_from_string(), java_type_from_string_with_exception(), java_bytecode_parse_treet::classt::methods, java_bytecode_parse_treet::classt::name, parse_tree, java_bytecode_parse_treet::parsed_class, pool_entry(), and java_bytecode_parsert::pool_entryt::s.
Referenced by rClassFile().
|
protected |
Definition at line 611 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::class_refs, struct_union_typet::components(), irept::find(), irept::get(), has_prefix(), irept::id(), id2string(), code_typet::parameters(), parse_tree, code_typet::return_type(), typet::subtype(), to_code_type(), and to_struct_type().
Referenced by get_class_refs().
|
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().
|
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().
|
protected |
Read method handle pointed to from constant pool entry at index, return type of method handle and name if lambda function is found.
entry | the constant pool entry of the methodhandle_info structure |
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().
|
inlineprotected |
Definition at line 82 of file java_bytecode_parser.cpp.
References constant_pool, messaget::eom(), and messaget::error().
Referenced by constant(), get_class_refs(), parse_local_variable_type_table(), parse_method_handle(), rclass_attribute(), rcode_attribute(), rconstant_pool(), read_bootstrapmethods_entry(), relement_value_pair(), relement_value_pairs(), rfield_attribute(), rfields(), rmethod(), rmethod_attribute(), and type_entry().
|
protected |
Definition at line 912 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::instructiont::address, java_bytecode_parse_treet::instructiont::args, bytecodes, constant(), messaget::eom(), messaget::error(), format(), from_integer(), irept::id(), id2string(), INVARIANT, read_u1(), read_u2(), read_u4(), source_locationt::set_java_bytecode_index(), java_bytecode_parse_treet::instructiont::source_location, java_bytecode_parse_treet::instructiont::statement, T_BOOLEAN, T_BYTE, T_CHAR, T_DOUBLE, T_FLOAT, T_INT, T_LONG, T_SHORT, and to_string().
Referenced by rmethod_attribute().
|
protected |
Definition at line 1579 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::classt::annotations, java_bytecode_parse_treet::classt::attribute_bootstrapmethods_read, java_bytecode_parse_treet::class_refs, get_dependencies_from_generic_parameters(), id2string(), INVARIANT, java_bytecode_parse_treet::classt::methods, java_bytecode_parse_treet::classt::name, parse_tree, pool_entry(), read_bootstrapmethods_entry(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, java_bytecode_parse_treet::classt::signature, and skip_bytes().
Referenced by rClassFile().
|
protected |
Definition at line 467 of file java_bytecode_parser.cpp.
References ACC_ABSTRACT, ACC_ANNOTATION, ACC_ENUM, ACC_FINAL, ACC_INTERFACE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_SYNTHETIC, constant(), java_bytecode_parse_treet::classt::enum_elements, messaget::eom(), messaget::error(), java_bytecode_parse_treet::classt::extends, java_bytecode_parse_treet::classt::fields, irept::get(), get_class_refs(), java_bytecode_parse_treet::classt::is_abstract, java_bytecode_parse_treet::classt::is_annotation, java_bytecode_parse_treet::fieldt::is_enum, java_bytecode_parse_treet::classt::is_enum, java_bytecode_parse_treet::classt::is_final, java_bytecode_parse_treet::classt::is_interface, java_bytecode_parse_treet::classt::is_private, java_bytecode_parse_treet::classt::is_protected, java_bytecode_parse_treet::classt::is_public, java_bytecode_parse_treet::classt::is_synthetic, java_bytecode_parse_treet::loading_successful, java_bytecode_parse_treet::classt::name, parse_tree, java_bytecode_parse_treet::parsed_class, rclass_attribute(), rconstant_pool(), read_u2(), read_u4(), rfields(), rinterfaces(), rmethods(), exprt::type(), and UNUSED.
Referenced by parse().
|
protected |
Definition at line 1273 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::methodt::stack_map_table_entryt::APPEND, java_bytecode_parse_treet::methodt::stack_map_table_entryt::CHOP, java_bytecode_parse_treet::methodt::stack_map_table_entryt::FULL, id2string(), java_bytecode_parse_treet::methodt::instructions, java_bytecode_parse_treet::methodt::local_variable_table, parse_local_variable_type_table(), pool_entry(), read_u1(), read_u2(), read_u4(), read_verification_type_info(), java_bytecode_parsert::pool_entryt::s, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_EXTENDED, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK_EXTENDED, skip_bytes(), and java_bytecode_parse_treet::methodt::stack_map_table.
Referenced by rmethod_attribute().
|
protected |
Definition at line 643 of file java_bytecode_parser.cpp.
References CONSTANT_Class, CONSTANT_Double, CONSTANT_Fieldref, CONSTANT_Float, CONSTANT_Integer, CONSTANT_InterfaceMethodref, CONSTANT_InvokeDynamic, CONSTANT_Long, CONSTANT_MethodHandle, CONSTANT_Methodref, CONSTANT_MethodType, CONSTANT_NameAndType, constant_pool, CONSTANT_String, CONSTANT_Utf8, ieee_float_spect::double_precision(), messaget::eom(), messaget::error(), from_integer(), symbol_typet::get_identifier(), id2string(), java_classname(), java_int_type(), java_long_type(), pool_entry(), read_u1(), read_u2(), read_u4(), read_u8(), java_bytecode_parsert::pool_entryt::ref1, java_bytecode_parsert::pool_entryt::ref2, java_bytecode_parsert::pool_entryt::s, irept::set(), ieee_float_spect::single_precision(), ieee_floatt::to_expr(), type_entry(), and ieee_floatt::unpack().
Referenced by rClassFile().
|
protected |
Read all entries of the BootstrapMethods
attribute of a class file.
parsed_class | the class representation of the class file that is currently parsed |
Definition at line 1820 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::classt::add_method_handle(), CONSTANT_Integer, CONSTANT_MethodHandle, CONSTANT_MethodType, messaget::debug(), messaget::eom(), id2string(), java_bytecode_parse_treet::classt::name, parse_method_handle(), pool_entry(), POSTCONDITION, read_u2(), java_bytecode_parsert::pool_entryt::ref1, java_bytecode_parsert::pool_entryt::s, store_unknown_method_handle(), java_bytecode_parsert::pool_entryt::tag, and java_bytecode_parse_treet::classt::UNKNOWN_HANDLE.
Referenced by rclass_attribute().
|
inlineprotected |
Definition at line 152 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), parsert::in, and messaget::result().
Referenced by read_u1(), read_u2(), read_u4(), and read_u8().
|
inlineprotected |
Definition at line 168 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rbytecode(), rcode_attribute(), rconstant_pool(), read_verification_type_info(), and relement_value_pair().
|
inlineprotected |
Definition at line 173 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by parse_local_variable_type_table(), rbytecode(), rclass_attribute(), rClassFile(), rcode_attribute(), rconstant_pool(), read_bootstrapmethods_entry(), read_verification_type_info(), relement_value_pair(), relement_value_pairs(), rfield_attribute(), rfields(), rinterfaces(), rmethod(), rmethod_attribute(), rmethods(), rRuntimeAnnotation(), and rRuntimeAnnotation_attribute().
|
inlineprotected |
Definition at line 178 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rbytecode(), rclass_attribute(), rClassFile(), rcode_attribute(), rconstant_pool(), rfield_attribute(), and rmethod_attribute().
|
inlineprotected |
Definition at line 183 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rconstant_pool().
|
protected |
Definition at line 1441 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index, java_bytecode_parse_treet::methodt::verification_type_infot::DOUBLE, java_bytecode_parse_treet::methodt::verification_type_infot::FLOAT, java_bytecode_parse_treet::methodt::verification_type_infot::INTEGER, java_bytecode_parse_treet::methodt::verification_type_infot::ITEM_NULL, java_bytecode_parse_treet::methodt::verification_type_infot::LONG, java_bytecode_parse_treet::methodt::verification_type_infot::OBJECT, java_bytecode_parse_treet::methodt::verification_type_infot::offset, read_u1(), read_u2(), java_bytecode_parse_treet::methodt::verification_type_infot::TOP, java_bytecode_parse_treet::methodt::verification_type_infot::type, java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED, java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED_THIS, VTYPE_INFO_DOUBLE, VTYPE_INFO_FLOAT, VTYPE_INFO_INTEGER, VTYPE_INFO_ITEM_NULL, VTYPE_INFO_LONG, VTYPE_INFO_OBJECT, VTYPE_INFO_TOP, VTYPE_INFO_UNINIT, and VTYPE_INFO_UNINIT_THIS.
Referenced by rcode_attribute().
|
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.
Definition at line 1520 of file java_bytecode_parser.cpp.
References constant(), pool_entry(), read_u1(), read_u2(), rRuntimeAnnotation(), UNUSED, and java_bytecode_parse_treet::annotationt::element_value_pairt::value.
Referenced by relement_value_pairs().
|
protected |
Definition at line 1502 of file java_bytecode_parser.cpp.
References pool_entry(), read_u2(), relement_value_pair(), and java_bytecode_parsert::pool_entryt::s.
Referenced by rRuntimeAnnotation().
|
protected |
Definition at line 1252 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::membert::annotations, id2string(), pool_entry(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, java_bytecode_parse_treet::membert::signature, and skip_bytes().
Referenced by rfields().
|
protected |
Definition at line 871 of file java_bytecode_parser.cpp.
References ACC_ENUM, ACC_FINAL, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, java_bytecode_parse_treet::classt::add_field(), DATA_INVARIANT, java_bytecode_parse_treet::membert::descriptor, id2string(), java_bytecode_parse_treet::fieldt::is_enum, java_bytecode_parse_treet::membert::is_final, java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_bytecode_parse_treet::membert::name, pool_entry(), read_u2(), rfield_attribute(), and java_bytecode_parsert::pool_entryt::s.
Referenced by rClassFile().
|
protected |
Definition at line 862 of file java_bytecode_parser.cpp.
References constant(), java_bytecode_parse_treet::classt::implements, and read_u2().
Referenced by rClassFile().
|
protected |
Definition at line 1669 of file java_bytecode_parser.cpp.
References ACC_ABSTRACT, ACC_FINAL, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_SYNCHRONIZED, java_bytecode_parse_treet::classt::add_method(), java_bytecode_parse_treet::methodt::base_name, DATA_INVARIANT, java_bytecode_parse_treet::membert::descriptor, id2string(), java_bytecode_parse_treet::methodt::is_abstract, java_bytecode_parse_treet::membert::is_final, java_bytecode_parse_treet::methodt::is_native, java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_bytecode_parse_treet::methodt::is_synchronized, java_bytecode_parse_treet::membert::name, pool_entry(), read_u2(), rmethod_attribute(), and java_bytecode_parsert::pool_entryt::s.
Referenced by rmethods().
|
protected |
Definition at line 1172 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::membert::annotations, java_bytecode_parse_treet::membert::descriptor, dstringt::empty(), java_bytecode_parse_treet::methodt::exception_table, id2string(), java_bytecode_parse_treet::methodt::instructions, INVARIANT, java_bytecode_parse_treet::membert::name, java_bytecode_parse_treet::classt::name, parse_tree, java_bytecode_parse_treet::parsed_class, pool_entry(), rbytecode(), rcode_attribute(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, source_locationt::set_line(), java_bytecode_parse_treet::membert::signature, skip_bytes(), java_bytecode_parse_treet::methodt::source_location, to_symbol_type(), and UNUSED.
Referenced by rmethod().
|
protected |
Definition at line 1647 of file java_bytecode_parser.cpp.
References read_u2(), and rmethod().
Referenced by rClassFile().
|
protected |
Definition at line 1494 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::annotationt::element_value_pairs, read_u2(), relement_value_pairs(), java_bytecode_parse_treet::annotationt::type, and type_entry().
Referenced by relement_value_pair(), and rRuntimeAnnotation_attribute().
|
protected |
Definition at line 1481 of file java_bytecode_parser.cpp.
References read_u2(), and rRuntimeAnnotation().
Referenced by rclass_attribute(), rfield_attribute(), and rmethod_attribute().
|
inlineprotected |
Definition at line 139 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), and parsert::in.
Referenced by rclass_attribute(), rcode_attribute(), rfield_attribute(), and rmethod_attribute().
|
protected |
Creates an unknown method handle and puts it into the parsed_class.
parsed_class | The class whose bootstrap method handles we are using |
bootstrap_method_index | The current index in the bootstrap entry table |
u2_values | The 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().
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().
|
protected |
Definition at line 80 of file java_bytecode_parser.cpp.
Referenced by get_bytecodes(), and rbytecode().
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().
java_bytecode_parse_treet java_bytecode_parsert::parse_tree |
Definition at line 57 of file java_bytecode_parser.cpp.
Referenced by get_class_refs(), get_class_refs_rec(), java_bytecode_parse(), rclass_attribute(), rClassFile(), and rmethod_attribute().