cprover
|
#include "java_bytecode_parser.h"
#include <algorithm>
#include <fstream>
#include <map>
#include <string>
#include <util/arith_tools.h>
#include <util/ieee_float.h>
#include <util/parser.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <util/optional.h>
#include "java_bytecode_parse_tree.h"
#include "java_types.h"
#include "bytecode_info.h"
Go to the source code of this file.
Classes | |
class | java_bytecode_parsert |
struct | java_bytecode_parsert::pool_entryt |
class | java_bytecode_parsert::bytecodet |
class | structured_pool_entryt |
class | class_infot |
Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1. More... | |
class | name_and_type_infot |
Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6. More... | |
class | base_ref_infot |
class | method_handle_infot |
Macros | |
#define | CONSTANT_Class 7 |
#define | CONSTANT_Fieldref 9 |
#define | CONSTANT_Methodref 10 |
#define | CONSTANT_InterfaceMethodref 11 |
#define | CONSTANT_String 8 |
#define | CONSTANT_Integer 3 |
#define | CONSTANT_Float 4 |
#define | CONSTANT_Long 5 |
#define | CONSTANT_Double 6 |
#define | CONSTANT_NameAndType 12 |
#define | CONSTANT_Utf8 1 |
#define | CONSTANT_MethodHandle 15 |
#define | CONSTANT_MethodType 16 |
#define | CONSTANT_InvokeDynamic 18 |
#define | VTYPE_INFO_TOP 0 |
#define | VTYPE_INFO_INTEGER 1 |
#define | VTYPE_INFO_FLOAT 2 |
#define | VTYPE_INFO_LONG 3 |
#define | VTYPE_INFO_DOUBLE 4 |
#define | VTYPE_INFO_ITEM_NULL 5 |
#define | VTYPE_INFO_UNINIT_THIS 6 |
#define | VTYPE_INFO_OBJECT 7 |
#define | VTYPE_INFO_UNINIT 8 |
#define | ACC_PUBLIC 0x0001 |
#define | ACC_PRIVATE 0x0002 |
#define | ACC_PROTECTED 0x0004 |
#define | ACC_STATIC 0x0008 |
#define | ACC_FINAL 0x0010 |
#define | ACC_SYNCHRONIZED 0x0020 |
#define | ACC_BRIDGE 0x0040 |
#define | ACC_VARARGS 0x0080 |
#define | ACC_NATIVE 0x0100 |
#define | ACC_INTERFACE 0x0200 |
#define | ACC_ABSTRACT 0x0400 |
#define | ACC_STRICT 0x0800 |
#define | ACC_SYNTHETIC 0x1000 |
#define | ACC_ANNOTATION 0x2000 |
#define | ACC_ENUM 0x4000 |
#define | UNUSED_u2(x) { const u2 x = read_u2(); (void)x; } (void)0 |
#define | T_BOOLEAN 4 |
#define | T_CHAR 5 |
#define | T_FLOAT 6 |
#define | T_DOUBLE 7 |
#define | T_BYTE 8 |
#define | T_SHORT 9 |
#define | T_INT 10 |
#define | T_LONG 11 |
#define | ACC_PUBLIC 0x0001 |
#define | ACC_PRIVATE 0x0002 |
#define | ACC_PROTECTED 0x0004 |
#define | ACC_STATIC 0x0008 |
#define | ACC_FINAL 0x0010 |
#define | ACC_SUPER 0x0020 |
#define | ACC_VOLATILE 0x0040 |
#define | ACC_TRANSIENT 0x0080 |
#define | ACC_INTERFACE 0x0200 |
#define | ACC_ABSTRACT 0x0400 |
#define | ACC_SYNTHETIC 0x1000 |
#define | ACC_ANNOTATION 0x2000 |
#define | ACC_ENUM 0x4000 |
Functions | |
optionalt< java_bytecode_parse_treet > | java_bytecode_parse (std::istream &istream, message_handlert &message_handler) |
optionalt< java_bytecode_parse_treet > | java_bytecode_parse (const std::string &file, message_handlert &message_handler) |
#define ACC_ABSTRACT 0x0400 |
Definition at line 1772 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), and java_bytecode_parsert::rmethod().
#define ACC_ABSTRACT 0x0400 |
Definition at line 1772 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000 |
Definition at line 1774 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile().
#define ACC_ANNOTATION 0x2000 |
Definition at line 1774 of file java_bytecode_parser.cpp.
#define ACC_BRIDGE 0x0040 |
Definition at line 454 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rmethod().
#define ACC_ENUM 0x4000 |
Definition at line 1775 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), and java_bytecode_parsert::rfields().
#define ACC_ENUM 0x4000 |
Definition at line 1775 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010 |
Definition at line 1767 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_FINAL 0x0010 |
Definition at line 1767 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200 |
Definition at line 1771 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile().
#define ACC_INTERFACE 0x0200 |
Definition at line 1771 of file java_bytecode_parser.cpp.
#define ACC_NATIVE 0x0100 |
Definition at line 456 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rmethod().
#define ACC_PRIVATE 0x0002 |
Definition at line 1764 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rinner_classes_attribute(), and java_bytecode_parsert::rmethod().
#define ACC_PRIVATE 0x0002 |
Definition at line 1764 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004 |
Definition at line 1765 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rinner_classes_attribute(), and java_bytecode_parsert::rmethod().
#define ACC_PROTECTED 0x0004 |
Definition at line 1765 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001 |
Definition at line 1763 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rinner_classes_attribute(), and java_bytecode_parsert::rmethod().
#define ACC_PUBLIC 0x0001 |
Definition at line 1763 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008 |
Definition at line 1766 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), java_bytecode_parsert::rinner_classes_attribute(), and java_bytecode_parsert::rmethod().
#define ACC_STATIC 0x0008 |
Definition at line 1766 of file java_bytecode_parser.cpp.
#define ACC_STRICT 0x0800 |
Definition at line 459 of file java_bytecode_parser.cpp.
#define ACC_SUPER 0x0020 |
Definition at line 1768 of file java_bytecode_parser.cpp.
#define ACC_SYNCHRONIZED 0x0020 |
Definition at line 453 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rmethod().
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1773 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile().
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1773 of file java_bytecode_parser.cpp.
#define ACC_TRANSIENT 0x0080 |
Definition at line 1770 of file java_bytecode_parser.cpp.
#define ACC_VARARGS 0x0080 |
Definition at line 455 of file java_bytecode_parser.cpp.
#define ACC_VOLATILE 0x0040 |
Definition at line 1769 of file java_bytecode_parser.cpp.
#define CONSTANT_Class 7 |
Definition at line 197 of file java_bytecode_parser.cpp.
Referenced by class_infot::class_infot(), java_bytecode_parsert::get_class_refs(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Double 6 |
Definition at line 205 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Fieldref 9 |
Definition at line 198 of file java_bytecode_parser.cpp.
Referenced by base_ref_infot::base_ref_infot(), method_handle_infot::get_reference(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Float 4 |
Definition at line 203 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Integer 3 |
Definition at line 202 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool(), and java_bytecode_parsert::read_bootstrapmethods_entry().
#define CONSTANT_InterfaceMethodref 11 |
Definition at line 200 of file java_bytecode_parser.cpp.
Referenced by base_ref_infot::base_ref_infot(), method_handle_infot::get_reference(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_InvokeDynamic 18 |
Definition at line 210 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Long 5 |
Definition at line 204 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_MethodHandle 15 |
Definition at line 208 of file java_bytecode_parser.cpp.
Referenced by method_handle_infot::method_handle_infot(), java_bytecode_parsert::rconstant_pool(), and java_bytecode_parsert::read_bootstrapmethods_entry().
#define CONSTANT_Methodref 10 |
Definition at line 199 of file java_bytecode_parser.cpp.
Referenced by base_ref_infot::base_ref_infot(), method_handle_infot::get_reference(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_MethodType 16 |
Definition at line 209 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool(), and java_bytecode_parsert::read_bootstrapmethods_entry().
#define CONSTANT_NameAndType 12 |
Definition at line 206 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::get_class_refs(), base_ref_infot::get_name_and_type(), name_and_type_infot::name_and_type_infot(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_String 8 |
Definition at line 201 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Utf8 1 |
Definition at line 207 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool(), and structured_pool_entryt::read_utf8_constant().
#define T_BOOLEAN 4 |
Definition at line 901 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_BYTE 8 |
Definition at line 905 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_CHAR 5 |
Definition at line 902 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_DOUBLE 7 |
Definition at line 904 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_FLOAT 6 |
Definition at line 903 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_INT 10 |
Definition at line 907 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_LONG 11 |
Definition at line 908 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_SHORT 9 |
Definition at line 906 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define UNUSED_u2 | ( | x | ) | { const u2 x = read_u2(); (void)x; } (void)0 |
Definition at line 464 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::relement_value_pair(), and java_bytecode_parsert::rmethod_attribute().
#define VTYPE_INFO_DOUBLE 4 |
Definition at line 216 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_FLOAT 2 |
Definition at line 214 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_INTEGER 1 |
Definition at line 213 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_ITEM_NULL 5 |
Definition at line 217 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_LONG 3 |
Definition at line 215 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_OBJECT 7 |
Definition at line 219 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_TOP 0 |
Definition at line 212 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_UNINIT 8 |
Definition at line 220 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_UNINIT_THIS 6 |
Definition at line 218 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
optionalt<java_bytecode_parse_treet> java_bytecode_parse | ( | std::istream & | istream, |
message_handlert & | message_handler | ||
) |
Definition at line 1809 of file java_bytecode_parser.cpp.
References parsert::in, message_handler, java_bytecode_parsert::parse(), java_bytecode_parsert::parse_tree, and messaget::set_message_handler().
Referenced by java_class_loadert::get_class_from_jar(), java_class_loadert::get_parse_tree(), and java_bytecode_parse().
optionalt<java_bytecode_parse_treet> java_bytecode_parse | ( | const std::string & | file, |
message_handlert & | message_handler | ||
) |
Definition at line 1826 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), java_bytecode_parse(), and message_handler.