cprover
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/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"
+ 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  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_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_VARARGS   0x0080
 
#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_treetjava_bytecode_parse (std::istream &istream, message_handlert &message_handler, bool skip_instructions)
 Attempt to parse a Java class from the given stream. More...
 
optionalt< java_bytecode_parse_treetjava_bytecode_parse (const std::string &file, message_handlert &message_handler, bool skip_instructions)
 Attempt to parse a Java class from the given file. More...
 

Macro Definition Documentation

◆ ACC_ABSTRACT [1/2]

#define ACC_ABSTRACT   0x0400

Definition at line 1832 of file java_bytecode_parser.cpp.

◆ ACC_ABSTRACT [2/2]

#define ACC_ABSTRACT   0x0400

Definition at line 1832 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION [1/2]

#define ACC_ANNOTATION   0x2000

Definition at line 1834 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION [2/2]

#define ACC_ANNOTATION   0x2000

Definition at line 1834 of file java_bytecode_parser.cpp.

◆ ACC_BRIDGE

#define ACC_BRIDGE   0x0040

Definition at line 464 of file java_bytecode_parser.cpp.

◆ ACC_ENUM [1/2]

#define ACC_ENUM   0x4000

Definition at line 1835 of file java_bytecode_parser.cpp.

◆ ACC_ENUM [2/2]

#define ACC_ENUM   0x4000

Definition at line 1835 of file java_bytecode_parser.cpp.

◆ ACC_FINAL [1/2]

#define ACC_FINAL   0x0010

Definition at line 1826 of file java_bytecode_parser.cpp.

◆ ACC_FINAL [2/2]

#define ACC_FINAL   0x0010

Definition at line 1826 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE [1/2]

#define ACC_INTERFACE   0x0200

Definition at line 1831 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE [2/2]

#define ACC_INTERFACE   0x0200

Definition at line 1831 of file java_bytecode_parser.cpp.

◆ ACC_NATIVE

#define ACC_NATIVE   0x0100

Definition at line 465 of file java_bytecode_parser.cpp.

◆ ACC_PRIVATE [1/2]

#define ACC_PRIVATE   0x0002

Definition at line 1823 of file java_bytecode_parser.cpp.

◆ ACC_PRIVATE [2/2]

#define ACC_PRIVATE   0x0002

Definition at line 1823 of file java_bytecode_parser.cpp.

◆ ACC_PROTECTED [1/2]

#define ACC_PROTECTED   0x0004

Definition at line 1824 of file java_bytecode_parser.cpp.

◆ ACC_PROTECTED [2/2]

#define ACC_PROTECTED   0x0004

Definition at line 1824 of file java_bytecode_parser.cpp.

◆ ACC_PUBLIC [1/2]

#define ACC_PUBLIC   0x0001

Definition at line 1822 of file java_bytecode_parser.cpp.

◆ ACC_PUBLIC [2/2]

#define ACC_PUBLIC   0x0001

Definition at line 1822 of file java_bytecode_parser.cpp.

◆ ACC_STATIC [1/2]

#define ACC_STATIC   0x0008

Definition at line 1825 of file java_bytecode_parser.cpp.

◆ ACC_STATIC [2/2]

#define ACC_STATIC   0x0008

Definition at line 1825 of file java_bytecode_parser.cpp.

◆ ACC_STRICT

#define ACC_STRICT   0x0800

Definition at line 468 of file java_bytecode_parser.cpp.

◆ ACC_SUPER

#define ACC_SUPER   0x0020

Definition at line 1828 of file java_bytecode_parser.cpp.

◆ ACC_SYNCHRONIZED

#define ACC_SYNCHRONIZED   0x0020

Definition at line 463 of file java_bytecode_parser.cpp.

◆ ACC_SYNTHETIC [1/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1833 of file java_bytecode_parser.cpp.

◆ ACC_SYNTHETIC [2/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1833 of file java_bytecode_parser.cpp.

◆ ACC_TRANSIENT

#define ACC_TRANSIENT   0x0080

Definition at line 1830 of file java_bytecode_parser.cpp.

◆ ACC_VARARGS

#define ACC_VARARGS   0x0080

Definition at line 1827 of file java_bytecode_parser.cpp.

◆ ACC_VOLATILE

#define ACC_VOLATILE   0x0040

Definition at line 1829 of file java_bytecode_parser.cpp.

◆ CONSTANT_Class

#define CONSTANT_Class   7

Definition at line 207 of file java_bytecode_parser.cpp.

◆ CONSTANT_Double

#define CONSTANT_Double   6

Definition at line 215 of file java_bytecode_parser.cpp.

◆ CONSTANT_Fieldref

#define CONSTANT_Fieldref   9

Definition at line 208 of file java_bytecode_parser.cpp.

◆ CONSTANT_Float

#define CONSTANT_Float   4

Definition at line 213 of file java_bytecode_parser.cpp.

◆ CONSTANT_Integer

#define CONSTANT_Integer   3

Definition at line 212 of file java_bytecode_parser.cpp.

◆ CONSTANT_InterfaceMethodref

#define CONSTANT_InterfaceMethodref   11

Definition at line 210 of file java_bytecode_parser.cpp.

◆ CONSTANT_InvokeDynamic

#define CONSTANT_InvokeDynamic   18

Definition at line 220 of file java_bytecode_parser.cpp.

◆ CONSTANT_Long

#define CONSTANT_Long   5

Definition at line 214 of file java_bytecode_parser.cpp.

◆ CONSTANT_MethodHandle

#define CONSTANT_MethodHandle   15

Definition at line 218 of file java_bytecode_parser.cpp.

◆ CONSTANT_Methodref

#define CONSTANT_Methodref   10

Definition at line 209 of file java_bytecode_parser.cpp.

◆ CONSTANT_MethodType

#define CONSTANT_MethodType   16

Definition at line 219 of file java_bytecode_parser.cpp.

◆ CONSTANT_NameAndType

#define CONSTANT_NameAndType   12

Definition at line 216 of file java_bytecode_parser.cpp.

◆ CONSTANT_String

#define CONSTANT_String   8

Definition at line 211 of file java_bytecode_parser.cpp.

◆ CONSTANT_Utf8

#define CONSTANT_Utf8   1

Definition at line 217 of file java_bytecode_parser.cpp.

◆ T_BOOLEAN

#define T_BOOLEAN   4

Definition at line 945 of file java_bytecode_parser.cpp.

◆ T_BYTE

#define T_BYTE   8

Definition at line 949 of file java_bytecode_parser.cpp.

◆ T_CHAR

#define T_CHAR   5

Definition at line 946 of file java_bytecode_parser.cpp.

◆ T_DOUBLE

#define T_DOUBLE   7

Definition at line 948 of file java_bytecode_parser.cpp.

◆ T_FLOAT

#define T_FLOAT   6

Definition at line 947 of file java_bytecode_parser.cpp.

◆ T_INT

#define T_INT   10

Definition at line 951 of file java_bytecode_parser.cpp.

◆ T_LONG

#define T_LONG   11

Definition at line 952 of file java_bytecode_parser.cpp.

◆ T_SHORT

#define T_SHORT   9

Definition at line 950 of file java_bytecode_parser.cpp.

◆ UNUSED_u2

#define UNUSED_u2 (   x)    { const u2 x = read_u2(); (void)x; } (void)0

Definition at line 473 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_DOUBLE

#define VTYPE_INFO_DOUBLE   4

Definition at line 226 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_FLOAT

#define VTYPE_INFO_FLOAT   2

Definition at line 224 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_INTEGER

#define VTYPE_INFO_INTEGER   1

Definition at line 223 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_ITEM_NULL

#define VTYPE_INFO_ITEM_NULL   5

Definition at line 227 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_LONG

#define VTYPE_INFO_LONG   3

Definition at line 225 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_OBJECT

#define VTYPE_INFO_OBJECT   7

Definition at line 229 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_TOP

#define VTYPE_INFO_TOP   0

Definition at line 222 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_UNINIT

#define VTYPE_INFO_UNINIT   8

Definition at line 230 of file java_bytecode_parser.cpp.

◆ VTYPE_INFO_UNINIT_THIS

#define VTYPE_INFO_UNINIT_THIS   6

Definition at line 228 of file java_bytecode_parser.cpp.

Function Documentation

◆ java_bytecode_parse() [1/2]

optionalt<java_bytecode_parse_treet> java_bytecode_parse ( const std::string &  file,
class message_handlert msg,
bool  skip_instructions = false 
)

Attempt to parse a Java class from the given file.

Parameters
filefile to load from
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 optionalt on failure

Definition at line 1890 of file java_bytecode_parser.cpp.

◆ java_bytecode_parse() [2/2]

optionalt<java_bytecode_parse_treet> java_bytecode_parse ( std::istream &  stream,
class message_handlert msg,
bool  skip_instructions = false 
)

Attempt to parse a Java class from the given stream.

Parameters
streamstream to load from
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 optionalt on failure

Definition at line 1870 of file java_bytecode_parser.cpp.