CBMC
|
#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/std_expr.h>
#include <util/string_constant.h>
#include "bytecode_info.h"
#include "java_bytecode_parse_tree.h"
#include "java_string_literal_expr.h"
#include "java_types.h"
Go to the source code of this file.
Classes | |
class | java_bytecode_parsert |
struct | java_bytecode_parsert::pool_entryt |
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 0x0001u |
#define | ACC_PRIVATE 0x0002u |
#define | ACC_PROTECTED 0x0004u |
#define | ACC_STATIC 0x0008u |
#define | ACC_FINAL 0x0010u |
#define | ACC_SYNCHRONIZED 0x0020u |
#define | ACC_BRIDGE 0x0040u |
#define | ACC_NATIVE 0x0100u |
#define | ACC_INTERFACE 0x0200u |
#define | ACC_ABSTRACT 0x0400u |
#define | ACC_STRICT 0x0800u |
#define | ACC_SYNTHETIC 0x1000u |
#define | ACC_ANNOTATION 0x2000u |
#define | ACC_ENUM 0x4000u |
#define | UNUSED_u2(x) |
#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 0x0001u |
#define | ACC_PRIVATE 0x0002u |
#define | ACC_PROTECTED 0x0004u |
#define | ACC_STATIC 0x0008u |
#define | ACC_FINAL 0x0010u |
#define | ACC_VARARGS 0x0080u |
#define | ACC_SUPER 0x0020u |
#define | ACC_VOLATILE 0x0040u |
#define | ACC_TRANSIENT 0x0080u |
#define | ACC_INTERFACE 0x0200u |
#define | ACC_ABSTRACT 0x0400u |
#define | ACC_SYNTHETIC 0x1000u |
#define | ACC_ANNOTATION 0x2000u |
#define | ACC_ENUM 0x4000u |
Functions | |
std::optional< java_bytecode_parse_treet > | java_bytecode_parse (std::istream &istream, const irep_idt &class_name, message_handlert &message_handler, bool skip_instructions) |
Attempt to parse a Java class from the given stream. More... | |
std::optional< java_bytecode_parse_treet > | java_bytecode_parse (const std::string &file, const irep_idt &class_name, message_handlert &message_handler, bool skip_instructions) |
Attempt to parse a Java class from the given file. More... | |
static java_class_typet::method_handle_kindt | get_method_handle_type (method_handle_infot::method_handle_kindt java_handle_kind) |
Translate the lambda method reference kind in a class file into the kind of handling the method requires. More... | |
#define ACC_ABSTRACT 0x0400u |
Definition at line 1770 of file java_bytecode_parser.cpp.
#define ACC_ABSTRACT 0x0400u |
Definition at line 1770 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000u |
Definition at line 1772 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000u |
Definition at line 1772 of file java_bytecode_parser.cpp.
#define ACC_BRIDGE 0x0040u |
Definition at line 416 of file java_bytecode_parser.cpp.
#define ACC_ENUM 0x4000u |
Definition at line 1773 of file java_bytecode_parser.cpp.
#define ACC_ENUM 0x4000u |
Definition at line 1773 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010u |
Definition at line 1764 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010u |
Definition at line 1764 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200u |
Definition at line 1769 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200u |
Definition at line 1769 of file java_bytecode_parser.cpp.
#define ACC_NATIVE 0x0100u |
Definition at line 417 of file java_bytecode_parser.cpp.
#define ACC_PRIVATE 0x0002u |
Definition at line 1761 of file java_bytecode_parser.cpp.
#define ACC_PRIVATE 0x0002u |
Definition at line 1761 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004u |
Definition at line 1762 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004u |
Definition at line 1762 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001u |
Definition at line 1760 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001u |
Definition at line 1760 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008u |
Definition at line 1763 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008u |
Definition at line 1763 of file java_bytecode_parser.cpp.
#define ACC_STRICT 0x0800u |
Definition at line 420 of file java_bytecode_parser.cpp.
#define ACC_SUPER 0x0020u |
Definition at line 1766 of file java_bytecode_parser.cpp.
#define ACC_SYNCHRONIZED 0x0020u |
Definition at line 415 of file java_bytecode_parser.cpp.
#define ACC_SYNTHETIC 0x1000u |
Definition at line 1771 of file java_bytecode_parser.cpp.
#define ACC_SYNTHETIC 0x1000u |
Definition at line 1771 of file java_bytecode_parser.cpp.
#define ACC_TRANSIENT 0x0080u |
Definition at line 1768 of file java_bytecode_parser.cpp.
#define ACC_VARARGS 0x0080u |
Definition at line 1765 of file java_bytecode_parser.cpp.
#define ACC_VOLATILE 0x0040u |
Definition at line 1767 of file java_bytecode_parser.cpp.
#define CONSTANT_Class 7 |
Definition at line 154 of file java_bytecode_parser.cpp.
#define CONSTANT_Double 6 |
Definition at line 162 of file java_bytecode_parser.cpp.
#define CONSTANT_Fieldref 9 |
Definition at line 155 of file java_bytecode_parser.cpp.
#define CONSTANT_Float 4 |
Definition at line 160 of file java_bytecode_parser.cpp.
#define CONSTANT_Integer 3 |
Definition at line 159 of file java_bytecode_parser.cpp.
#define CONSTANT_InterfaceMethodref 11 |
Definition at line 157 of file java_bytecode_parser.cpp.
#define CONSTANT_InvokeDynamic 18 |
Definition at line 167 of file java_bytecode_parser.cpp.
#define CONSTANT_Long 5 |
Definition at line 161 of file java_bytecode_parser.cpp.
#define CONSTANT_MethodHandle 15 |
Definition at line 165 of file java_bytecode_parser.cpp.
#define CONSTANT_Methodref 10 |
Definition at line 156 of file java_bytecode_parser.cpp.
#define CONSTANT_MethodType 16 |
Definition at line 166 of file java_bytecode_parser.cpp.
#define CONSTANT_NameAndType 12 |
Definition at line 163 of file java_bytecode_parser.cpp.
#define CONSTANT_String 8 |
Definition at line 158 of file java_bytecode_parser.cpp.
#define CONSTANT_Utf8 1 |
Definition at line 164 of file java_bytecode_parser.cpp.
#define T_BOOLEAN 4 |
Definition at line 875 of file java_bytecode_parser.cpp.
#define T_BYTE 8 |
Definition at line 879 of file java_bytecode_parser.cpp.
#define T_CHAR 5 |
Definition at line 876 of file java_bytecode_parser.cpp.
#define T_DOUBLE 7 |
Definition at line 878 of file java_bytecode_parser.cpp.
#define T_FLOAT 6 |
Definition at line 877 of file java_bytecode_parser.cpp.
#define T_INT 10 |
Definition at line 881 of file java_bytecode_parser.cpp.
#define T_LONG 11 |
Definition at line 882 of file java_bytecode_parser.cpp.
#define T_SHORT 9 |
Definition at line 880 of file java_bytecode_parser.cpp.
#define UNUSED_u2 | ( | x | ) |
Definition at line 425 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_DOUBLE 4 |
Definition at line 173 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_FLOAT 2 |
Definition at line 171 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_INTEGER 1 |
Definition at line 170 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_ITEM_NULL 5 |
Definition at line 174 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_LONG 3 |
Definition at line 172 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_OBJECT 7 |
Definition at line 176 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_TOP 0 |
Definition at line 169 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_UNINIT 8 |
Definition at line 177 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_UNINIT_THIS 6 |
Definition at line 175 of file java_bytecode_parser.cpp.
|
static |
Translate the lambda method reference kind in a class file into the kind of handling the method requires.
invokestatic/special translate into direct method calls; invokevirtual/interface translate into virtual dispatch, newinvokespecial translates into a special instantiate-and-construct sequence. The field-manipulation reference kinds appear never to happen in reality and don't have syntax in the Java language.
Definition at line 1892 of file java_bytecode_parser.cpp.
std::optional<java_bytecode_parse_treet> java_bytecode_parse | ( | const std::string & | file, |
const irep_idt & | class_name, | ||
class message_handlert & | msg, | ||
bool | skip_instructions = false |
||
) |
Attempt to parse a Java class from the given file.
file | file to load from |
class_name | name of the class to load |
msg | handles log messages |
skip_instructions | if true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info. |
Definition at line 1830 of file java_bytecode_parser.cpp.
std::optional<java_bytecode_parse_treet> java_bytecode_parse | ( | std::istream & | stream, |
const irep_idt & | class_name, | ||
class message_handlert & | msg, | ||
bool | skip_instructions = false |
||
) |
Attempt to parse a Java class from the given stream.
stream | stream to load from |
class_name | name of the class to load |
msg | handles log messages |
skip_instructions | if true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info. |
Definition at line 1808 of file java_bytecode_parser.cpp.