CBMC
java_bytecode_parser.cpp File Reference
#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"
+ Include dependency graph for java_bytecode_parser.cpp:

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

Macro Definition Documentation

◆ ACC_ABSTRACT [1/2]

#define ACC_ABSTRACT   0x0400u

Definition at line 1770 of file java_bytecode_parser.cpp.

◆ ACC_ABSTRACT [2/2]

#define ACC_ABSTRACT   0x0400u

Definition at line 1770 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION [1/2]

#define ACC_ANNOTATION   0x2000u

Definition at line 1772 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION [2/2]

#define ACC_ANNOTATION   0x2000u

Definition at line 1772 of file java_bytecode_parser.cpp.

◆ ACC_BRIDGE

#define ACC_BRIDGE   0x0040u

Definition at line 416 of file java_bytecode_parser.cpp.

◆ ACC_ENUM [1/2]

#define ACC_ENUM   0x4000u

Definition at line 1773 of file java_bytecode_parser.cpp.

◆ ACC_ENUM [2/2]

#define ACC_ENUM   0x4000u

Definition at line 1773 of file java_bytecode_parser.cpp.

◆ ACC_FINAL [1/2]

#define ACC_FINAL   0x0010u

Definition at line 1764 of file java_bytecode_parser.cpp.

◆ ACC_FINAL [2/2]

#define ACC_FINAL   0x0010u

Definition at line 1764 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE [1/2]

#define ACC_INTERFACE   0x0200u

Definition at line 1769 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE [2/2]

#define ACC_INTERFACE   0x0200u

Definition at line 1769 of file java_bytecode_parser.cpp.

◆ ACC_NATIVE

#define ACC_NATIVE   0x0100u

Definition at line 417 of file java_bytecode_parser.cpp.

◆ ACC_PRIVATE [1/2]

#define ACC_PRIVATE   0x0002u

Definition at line 1761 of file java_bytecode_parser.cpp.

◆ ACC_PRIVATE [2/2]

#define ACC_PRIVATE   0x0002u

Definition at line 1761 of file java_bytecode_parser.cpp.

◆ ACC_PROTECTED [1/2]

#define ACC_PROTECTED   0x0004u

Definition at line 1762 of file java_bytecode_parser.cpp.

◆ ACC_PROTECTED [2/2]

#define ACC_PROTECTED   0x0004u

Definition at line 1762 of file java_bytecode_parser.cpp.

◆ ACC_PUBLIC [1/2]

#define ACC_PUBLIC   0x0001u

Definition at line 1760 of file java_bytecode_parser.cpp.

◆ ACC_PUBLIC [2/2]

#define ACC_PUBLIC   0x0001u

Definition at line 1760 of file java_bytecode_parser.cpp.

◆ ACC_STATIC [1/2]

#define ACC_STATIC   0x0008u

Definition at line 1763 of file java_bytecode_parser.cpp.

◆ ACC_STATIC [2/2]

#define ACC_STATIC   0x0008u

Definition at line 1763 of file java_bytecode_parser.cpp.

◆ ACC_STRICT

#define ACC_STRICT   0x0800u

Definition at line 420 of file java_bytecode_parser.cpp.

◆ ACC_SUPER

#define ACC_SUPER   0x0020u

Definition at line 1766 of file java_bytecode_parser.cpp.

◆ ACC_SYNCHRONIZED

#define ACC_SYNCHRONIZED   0x0020u

Definition at line 415 of file java_bytecode_parser.cpp.

◆ ACC_SYNTHETIC [1/2]

#define ACC_SYNTHETIC   0x1000u

Definition at line 1771 of file java_bytecode_parser.cpp.

◆ ACC_SYNTHETIC [2/2]

#define ACC_SYNTHETIC   0x1000u

Definition at line 1771 of file java_bytecode_parser.cpp.

◆ ACC_TRANSIENT

#define ACC_TRANSIENT   0x0080u

Definition at line 1768 of file java_bytecode_parser.cpp.

◆ ACC_VARARGS

#define ACC_VARARGS   0x0080u

Definition at line 1765 of file java_bytecode_parser.cpp.

◆ ACC_VOLATILE

#define ACC_VOLATILE   0x0040u

Definition at line 1767 of file java_bytecode_parser.cpp.

◆ CONSTANT_Class

#define CONSTANT_Class   7

Definition at line 154 of file java_bytecode_parser.cpp.

◆ CONSTANT_Double

#define CONSTANT_Double   6

Definition at line 162 of file java_bytecode_parser.cpp.

◆ CONSTANT_Fieldref

#define CONSTANT_Fieldref   9

Definition at line 155 of file java_bytecode_parser.cpp.

◆ CONSTANT_Float

#define CONSTANT_Float   4

Definition at line 160 of file java_bytecode_parser.cpp.

◆ CONSTANT_Integer

#define CONSTANT_Integer   3

Definition at line 159 of file java_bytecode_parser.cpp.

◆ CONSTANT_InterfaceMethodref

#define CONSTANT_InterfaceMethodref   11

Definition at line 157 of file java_bytecode_parser.cpp.

◆ CONSTANT_InvokeDynamic

#define CONSTANT_InvokeDynamic   18

Definition at line 167 of file java_bytecode_parser.cpp.

◆ CONSTANT_Long

#define CONSTANT_Long   5

Definition at line 161 of file java_bytecode_parser.cpp.

◆ CONSTANT_MethodHandle

#define CONSTANT_MethodHandle   15

Definition at line 165 of file java_bytecode_parser.cpp.

◆ CONSTANT_Methodref

#define CONSTANT_Methodref   10

Definition at line 156 of file java_bytecode_parser.cpp.

◆ CONSTANT_MethodType

#define CONSTANT_MethodType   16

Definition at line 166 of file java_bytecode_parser.cpp.

◆ CONSTANT_NameAndType

#define CONSTANT_NameAndType   12

Definition at line 163 of file java_bytecode_parser.cpp.

◆ CONSTANT_String

#define CONSTANT_String   8

Definition at line 158 of file java_bytecode_parser.cpp.

◆ CONSTANT_Utf8

#define CONSTANT_Utf8   1

Definition at line 164 of file java_bytecode_parser.cpp.

◆ T_BOOLEAN

#define T_BOOLEAN   4

Definition at line 875 of file java_bytecode_parser.cpp.

◆ T_BYTE

#define T_BYTE   8

Definition at line 879 of file java_bytecode_parser.cpp.

◆ T_CHAR

#define T_CHAR   5

Definition at line 876 of file java_bytecode_parser.cpp.

◆ T_DOUBLE

#define T_DOUBLE   7

Definition at line 878 of file java_bytecode_parser.cpp.

◆ T_FLOAT

#define T_FLOAT   6

Definition at line 877 of file java_bytecode_parser.cpp.

◆ T_INT

#define T_INT   10

Definition at line 881 of file java_bytecode_parser.cpp.

◆ T_LONG

#define T_LONG   11

Definition at line 882 of file java_bytecode_parser.cpp.

◆ T_SHORT

#define T_SHORT   9

Definition at line 880 of file java_bytecode_parser.cpp.

◆ UNUSED_u2

#define UNUSED_u2 (   x)
Value:
{ \
const u2 x = read<u2>(); \
(void)x; \
} \
(void)0
uint16_t u2
Definition: bytecode_info.h:56

Definition at line 425 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_DOUBLE

#define VTYPE_INFO_DOUBLE   4

Definition at line 173 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_FLOAT

#define VTYPE_INFO_FLOAT   2

Definition at line 171 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_INTEGER

#define VTYPE_INFO_INTEGER   1

Definition at line 170 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_ITEM_NULL

#define VTYPE_INFO_ITEM_NULL   5

Definition at line 174 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_LONG

#define VTYPE_INFO_LONG   3

Definition at line 172 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_OBJECT

#define VTYPE_INFO_OBJECT   7

Definition at line 176 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_TOP

#define VTYPE_INFO_TOP   0

Definition at line 169 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_UNINIT

#define VTYPE_INFO_UNINIT   8

Definition at line 177 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_UNINIT_THIS

#define VTYPE_INFO_UNINIT_THIS   6

Definition at line 175 of file java_bytecode_parser.cpp.

Function Documentation

◆ get_method_handle_type()

static java_class_typet::method_handle_kindt get_method_handle_type ( method_handle_infot::method_handle_kindt  java_handle_kind)
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.

◆ java_bytecode_parse() [1/2]

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.

Parameters
filefile to load from
class_namename of the class to load
msghandles log messages
skip_instructionsif true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info.
Returns
parse tree, or empty std::optional on failure

Definition at line 1830 of file java_bytecode_parser.cpp.

◆ java_bytecode_parse() [2/2]

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.

Parameters
streamstream to load from
class_namename of the class to load
msghandles log messages
skip_instructionsif true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info.
Returns
parse tree, or empty std::optional on failure

Definition at line 1808 of file java_bytecode_parser.cpp.