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_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   __attribute__((unused))
 
#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< class java_bytecode_parse_treetjava_bytecode_parse (std::istream &istream, message_handlert &message_handler)
 
optionalt< class java_bytecode_parse_treetjava_bytecode_parse (const std::string &file, message_handlert &message_handler)
 

Macro Definition Documentation

◆ ACC_ABSTRACT [1/2]

#define ACC_ABSTRACT   0x0400

◆ ACC_ABSTRACT [2/2]

#define ACC_ABSTRACT   0x0400

Definition at line 1664 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION [1/2]

#define ACC_ANNOTATION   0x2000

Definition at line 1666 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rClassFile().

◆ ACC_ANNOTATION [2/2]

#define ACC_ANNOTATION   0x2000

Definition at line 1666 of file java_bytecode_parser.cpp.

◆ ACC_BRIDGE

#define ACC_BRIDGE   0x0040

Definition at line 451 of file java_bytecode_parser.cpp.

◆ ACC_ENUM [1/2]

#define ACC_ENUM   0x4000

◆ ACC_ENUM [2/2]

#define ACC_ENUM   0x4000

Definition at line 1667 of file java_bytecode_parser.cpp.

◆ ACC_FINAL [1/2]

#define ACC_FINAL   0x0010

◆ ACC_FINAL [2/2]

#define ACC_FINAL   0x0010

Definition at line 1659 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE [1/2]

#define ACC_INTERFACE   0x0200

Definition at line 1663 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rClassFile().

◆ ACC_INTERFACE [2/2]

#define ACC_INTERFACE   0x0200

Definition at line 1663 of file java_bytecode_parser.cpp.

◆ ACC_NATIVE

#define ACC_NATIVE   0x0100

Definition at line 453 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rmethod().

◆ ACC_PRIVATE [1/2]

#define ACC_PRIVATE   0x0002

◆ ACC_PRIVATE [2/2]

#define ACC_PRIVATE   0x0002

Definition at line 1656 of file java_bytecode_parser.cpp.

◆ ACC_PROTECTED [1/2]

#define ACC_PROTECTED   0x0004

◆ ACC_PROTECTED [2/2]

#define ACC_PROTECTED   0x0004

Definition at line 1657 of file java_bytecode_parser.cpp.

◆ ACC_PUBLIC [1/2]

#define ACC_PUBLIC   0x0001

◆ ACC_PUBLIC [2/2]

#define ACC_PUBLIC   0x0001

Definition at line 1655 of file java_bytecode_parser.cpp.

◆ ACC_STATIC [1/2]

#define ACC_STATIC   0x0008

◆ ACC_STATIC [2/2]

#define ACC_STATIC   0x0008

Definition at line 1658 of file java_bytecode_parser.cpp.

◆ ACC_STRICT

#define ACC_STRICT   0x0800

Definition at line 456 of file java_bytecode_parser.cpp.

◆ ACC_SUPER

#define ACC_SUPER   0x0020

Definition at line 1660 of file java_bytecode_parser.cpp.

◆ ACC_SYNCHRONIZED

#define ACC_SYNCHRONIZED   0x0020

Definition at line 450 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rmethod().

◆ ACC_SYNTHETIC [1/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1665 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rClassFile().

◆ ACC_SYNTHETIC [2/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1665 of file java_bytecode_parser.cpp.

◆ ACC_TRANSIENT

#define ACC_TRANSIENT   0x0080

Definition at line 1662 of file java_bytecode_parser.cpp.

◆ ACC_VARARGS

#define ACC_VARARGS   0x0080

Definition at line 452 of file java_bytecode_parser.cpp.

◆ ACC_VOLATILE

#define ACC_VOLATILE   0x0040

Definition at line 1661 of file java_bytecode_parser.cpp.

◆ CONSTANT_Class

◆ CONSTANT_Double

#define CONSTANT_Double   6

Definition at line 202 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Fieldref

◆ CONSTANT_Float

#define CONSTANT_Float   4

Definition at line 200 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Integer

#define CONSTANT_Integer   3

◆ CONSTANT_InterfaceMethodref

#define CONSTANT_InterfaceMethodref   11

◆ CONSTANT_InvokeDynamic

#define CONSTANT_InvokeDynamic   18

Definition at line 207 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Long

#define CONSTANT_Long   5

Definition at line 201 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_MethodHandle

◆ CONSTANT_Methodref

#define CONSTANT_Methodref   10

◆ CONSTANT_MethodType

#define CONSTANT_MethodType   16

◆ CONSTANT_NameAndType

◆ CONSTANT_String

#define CONSTANT_String   8

Definition at line 198 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Utf8

#define CONSTANT_Utf8   1

◆ T_BOOLEAN

#define T_BOOLEAN   4

Definition at line 903 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_BYTE

#define T_BYTE   8

Definition at line 907 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_CHAR

#define T_CHAR   5

Definition at line 904 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_DOUBLE

#define T_DOUBLE   7

Definition at line 906 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_FLOAT

#define T_FLOAT   6

Definition at line 905 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_INT

#define T_INT   10

Definition at line 909 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_LONG

#define T_LONG   11

Definition at line 910 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_SHORT

#define T_SHORT   9

Definition at line 908 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ UNUSED

◆ VTYPE_INFO_DOUBLE

#define VTYPE_INFO_DOUBLE   4

◆ VTYPE_INFO_FLOAT

#define VTYPE_INFO_FLOAT   2

◆ VTYPE_INFO_INTEGER

#define VTYPE_INFO_INTEGER   1

◆ VTYPE_INFO_ITEM_NULL

#define VTYPE_INFO_ITEM_NULL   5

◆ VTYPE_INFO_LONG

#define VTYPE_INFO_LONG   3

◆ VTYPE_INFO_OBJECT

#define VTYPE_INFO_OBJECT   7

◆ VTYPE_INFO_TOP

#define VTYPE_INFO_TOP   0

◆ VTYPE_INFO_UNINIT

#define VTYPE_INFO_UNINIT   8

◆ VTYPE_INFO_UNINIT_THIS

#define VTYPE_INFO_UNINIT_THIS   6

Function Documentation

◆ java_bytecode_parse() [1/2]

◆ java_bytecode_parse() [2/2]

optionalt<class java_bytecode_parse_treet> java_bytecode_parse ( const std::string &  file,
message_handlert message_handler 
)