cprover
java_bytecode_parser.cpp File Reference
#include "java_bytecode_parser.h"
#include <algorithm>
#include <fstream>
#include <map>
#include <string>
#include <util/parser.h>
#include <util/std_expr.h>
#include <util/arith_tools.h>
#include <util/ieee_float.h>
#include <util/prefix.h>
#include <ansi-c/string_constant.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
 

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_ABSTRACT   0x0400
 
#define ACC_STRICT   0x0800
 
#define ACC_SYNTHETIC   0x1000
 
#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

bool java_bytecode_parse (std::istream &istream, java_bytecode_parse_treet &parse_tree, message_handlert &message_handler)
 
bool java_bytecode_parse (const std::string &file, java_bytecode_parse_treet &parse_tree, 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 1333 of file java_bytecode_parser.cpp.

◆ ACC_ANNOTATION

#define ACC_ANNOTATION   0x2000

Definition at line 1335 of file java_bytecode_parser.cpp.

◆ ACC_BRIDGE

#define ACC_BRIDGE   0x0040

Definition at line 238 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 1336 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 1328 of file java_bytecode_parser.cpp.

◆ ACC_INTERFACE

#define ACC_INTERFACE   0x0200

Definition at line 1332 of file java_bytecode_parser.cpp.

◆ ACC_NATIVE

#define ACC_NATIVE   0x0100

Definition at line 240 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 1325 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 1326 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 1324 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 1327 of file java_bytecode_parser.cpp.

◆ ACC_STRICT

#define ACC_STRICT   0x0800

Definition at line 242 of file java_bytecode_parser.cpp.

◆ ACC_SUPER

#define ACC_SUPER   0x0020

Definition at line 1329 of file java_bytecode_parser.cpp.

◆ ACC_SYNCHRONIZED

#define ACC_SYNCHRONIZED   0x0020

Definition at line 237 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rmethod().

◆ ACC_SYNTHETIC [1/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1334 of file java_bytecode_parser.cpp.

◆ ACC_SYNTHETIC [2/2]

#define ACC_SYNTHETIC   0x1000

Definition at line 1334 of file java_bytecode_parser.cpp.

◆ ACC_TRANSIENT

#define ACC_TRANSIENT   0x0080

Definition at line 1331 of file java_bytecode_parser.cpp.

◆ ACC_VARARGS

#define ACC_VARARGS   0x0080

Definition at line 239 of file java_bytecode_parser.cpp.

◆ ACC_VOLATILE

#define ACC_VOLATILE   0x0040

Definition at line 1330 of file java_bytecode_parser.cpp.

◆ CONSTANT_Class

#define CONSTANT_Class   7

◆ CONSTANT_Double

#define CONSTANT_Double   6

Definition at line 187 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Fieldref

#define CONSTANT_Fieldref   9

Definition at line 180 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Float

#define CONSTANT_Float   4

Definition at line 185 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Integer

#define CONSTANT_Integer   3

Definition at line 184 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_InterfaceMethodref

#define CONSTANT_InterfaceMethodref   11

Definition at line 182 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_InvokeDynamic

#define CONSTANT_InvokeDynamic   18

Definition at line 192 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Long

#define CONSTANT_Long   5

Definition at line 186 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_MethodHandle

#define CONSTANT_MethodHandle   15

Definition at line 190 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Methodref

#define CONSTANT_Methodref   10

Definition at line 181 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_MethodType

#define CONSTANT_MethodType   16

Definition at line 191 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_NameAndType

#define CONSTANT_NameAndType   12

◆ CONSTANT_String

#define CONSTANT_String   8

Definition at line 183 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ CONSTANT_Utf8

#define CONSTANT_Utf8   1

Definition at line 189 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rconstant_pool().

◆ T_BOOLEAN

#define T_BOOLEAN   4

Definition at line 642 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_BYTE

#define T_BYTE   8

Definition at line 646 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_CHAR

#define T_CHAR   5

Definition at line 643 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_DOUBLE

#define T_DOUBLE   7

Definition at line 645 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_FLOAT

#define T_FLOAT   6

Definition at line 644 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_INT

#define T_INT   10

Definition at line 648 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_LONG

#define T_LONG   11

Definition at line 649 of file java_bytecode_parser.cpp.

Referenced by java_bytecode_parsert::rbytecode().

◆ T_SHORT

#define T_SHORT   9

Definition at line 647 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]

bool java_bytecode_parse ( const std::string &  file,
java_bytecode_parse_treet parse_tree,
message_handlert message_handler 
)