CBMC
Loading...
Searching...
No Matches
Classes | Macros | Functions
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_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.
 
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.
 
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.
 

Macro Definition Documentation

◆  ACC_ABSTRACT [1/2]

#define ACC_ABSTRACT   0x0400u

Definition at line 429 of file java_bytecode_parser.cpp.

◆  ACC_ABSTRACT [2/2]

#define ACC_ABSTRACT   0x0400u

Definition at line 429 of file java_bytecode_parser.cpp.

◆  ACC_ANNOTATION [1/2]

#define ACC_ANNOTATION   0x2000u

Definition at line 432 of file java_bytecode_parser.cpp.

◆  ACC_ANNOTATION [2/2]

#define ACC_ANNOTATION   0x2000u

Definition at line 432 of file java_bytecode_parser.cpp.

◆  ACC_BRIDGE

#define ACC_BRIDGE   0x0040u

Definition at line 426 of file java_bytecode_parser.cpp.

◆  ACC_ENUM [1/2]

#define ACC_ENUM   0x4000u

Definition at line 433 of file java_bytecode_parser.cpp.

◆  ACC_ENUM [2/2]

#define ACC_ENUM   0x4000u

Definition at line 433 of file java_bytecode_parser.cpp.

◆  ACC_FINAL [1/2]

#define ACC_FINAL   0x0010u

Definition at line 424 of file java_bytecode_parser.cpp.

◆  ACC_FINAL [2/2]

#define ACC_FINAL   0x0010u

Definition at line 424 of file java_bytecode_parser.cpp.

◆  ACC_INTERFACE [1/2]

#define ACC_INTERFACE   0x0200u

Definition at line 428 of file java_bytecode_parser.cpp.

◆  ACC_INTERFACE [2/2]

#define ACC_INTERFACE   0x0200u

Definition at line 428 of file java_bytecode_parser.cpp.

◆  ACC_NATIVE

#define ACC_NATIVE   0x0100u

Definition at line 427 of file java_bytecode_parser.cpp.

◆  ACC_PRIVATE [1/2]

#define ACC_PRIVATE   0x0002u

Definition at line 421 of file java_bytecode_parser.cpp.

◆  ACC_PRIVATE [2/2]

#define ACC_PRIVATE   0x0002u

Definition at line 421 of file java_bytecode_parser.cpp.

◆  ACC_PROTECTED [1/2]

#define ACC_PROTECTED   0x0004u

Definition at line 422 of file java_bytecode_parser.cpp.

◆  ACC_PROTECTED [2/2]

#define ACC_PROTECTED   0x0004u

Definition at line 422 of file java_bytecode_parser.cpp.

◆  ACC_PUBLIC [1/2]

#define ACC_PUBLIC   0x0001u

Definition at line 420 of file java_bytecode_parser.cpp.

◆  ACC_PUBLIC [2/2]

#define ACC_PUBLIC   0x0001u

Definition at line 420 of file java_bytecode_parser.cpp.

◆  ACC_STATIC [1/2]

#define ACC_STATIC   0x0008u

Definition at line 423 of file java_bytecode_parser.cpp.

◆  ACC_STATIC [2/2]

#define ACC_STATIC   0x0008u

Definition at line 423 of file java_bytecode_parser.cpp.

◆  ACC_STRICT

#define ACC_STRICT   0x0800u

Definition at line 430 of file java_bytecode_parser.cpp.

◆  ACC_SUPER

#define ACC_SUPER   0x0020u

Definition at line 1776 of file java_bytecode_parser.cpp.

◆  ACC_SYNCHRONIZED

#define ACC_SYNCHRONIZED   0x0020u

Definition at line 425 of file java_bytecode_parser.cpp.

◆  ACC_SYNTHETIC [1/2]

#define ACC_SYNTHETIC   0x1000u

Definition at line 431 of file java_bytecode_parser.cpp.

◆  ACC_SYNTHETIC [2/2]

#define ACC_SYNTHETIC   0x1000u

Definition at line 431 of file java_bytecode_parser.cpp.

◆  ACC_TRANSIENT

#define ACC_TRANSIENT   0x0080u

Definition at line 1778 of file java_bytecode_parser.cpp.

◆  ACC_VARARGS

#define ACC_VARARGS   0x0080u

Definition at line 1775 of file java_bytecode_parser.cpp.

◆  ACC_VOLATILE

#define ACC_VOLATILE   0x0040u

Definition at line 1777 of file java_bytecode_parser.cpp.

◆  CONSTANT_Class

#define CONSTANT_Class   7

Definition at line 164 of file java_bytecode_parser.cpp.

◆  CONSTANT_Double

#define CONSTANT_Double   6

Definition at line 172 of file java_bytecode_parser.cpp.

◆  CONSTANT_Fieldref

#define CONSTANT_Fieldref   9

Definition at line 165 of file java_bytecode_parser.cpp.

◆  CONSTANT_Float

#define CONSTANT_Float   4

Definition at line 170 of file java_bytecode_parser.cpp.

◆  CONSTANT_Integer

#define CONSTANT_Integer   3

Definition at line 169 of file java_bytecode_parser.cpp.

◆  CONSTANT_InterfaceMethodref

#define CONSTANT_InterfaceMethodref   11

Definition at line 167 of file java_bytecode_parser.cpp.

◆  CONSTANT_InvokeDynamic

#define CONSTANT_InvokeDynamic   18

Definition at line 177 of file java_bytecode_parser.cpp.

◆  CONSTANT_Long

#define CONSTANT_Long   5

Definition at line 171 of file java_bytecode_parser.cpp.

◆  CONSTANT_MethodHandle

#define CONSTANT_MethodHandle   15

Definition at line 175 of file java_bytecode_parser.cpp.

◆  CONSTANT_Methodref

#define CONSTANT_Methodref   10

Definition at line 166 of file java_bytecode_parser.cpp.

◆  CONSTANT_MethodType

#define CONSTANT_MethodType   16

Definition at line 176 of file java_bytecode_parser.cpp.

◆  CONSTANT_NameAndType

#define CONSTANT_NameAndType   12

Definition at line 173 of file java_bytecode_parser.cpp.

◆  CONSTANT_String

#define CONSTANT_String   8

Definition at line 168 of file java_bytecode_parser.cpp.

◆  CONSTANT_Utf8

#define CONSTANT_Utf8   1

Definition at line 174 of file java_bytecode_parser.cpp.

◆  T_BOOLEAN

#define T_BOOLEAN   4

Definition at line 885 of file java_bytecode_parser.cpp.

◆  T_BYTE

#define T_BYTE   8

Definition at line 889 of file java_bytecode_parser.cpp.

◆  T_CHAR

#define T_CHAR   5

Definition at line 886 of file java_bytecode_parser.cpp.

◆  T_DOUBLE

#define T_DOUBLE   7

Definition at line 888 of file java_bytecode_parser.cpp.

◆  T_FLOAT

#define T_FLOAT   6

Definition at line 887 of file java_bytecode_parser.cpp.

◆  T_INT

#define T_INT   10

Definition at line 891 of file java_bytecode_parser.cpp.

◆  T_LONG

#define T_LONG   11

Definition at line 892 of file java_bytecode_parser.cpp.

◆  T_SHORT

#define T_SHORT   9

Definition at line 890 of file java_bytecode_parser.cpp.

◆  UNUSED_u2

#define UNUSED_u2 (   x )
Value:
{ \
const u2 x = read<u2>(); \
(void)x; \
} \
(void)0
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566

Definition at line 435 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_DOUBLE

#define VTYPE_INFO_DOUBLE   4

Definition at line 183 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_FLOAT

#define VTYPE_INFO_FLOAT   2

Definition at line 181 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_INTEGER

#define VTYPE_INFO_INTEGER   1

Definition at line 180 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_ITEM_NULL

#define VTYPE_INFO_ITEM_NULL   5

Definition at line 184 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_LONG

#define VTYPE_INFO_LONG   3

Definition at line 182 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_OBJECT

#define VTYPE_INFO_OBJECT   7

Definition at line 186 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_TOP

#define VTYPE_INFO_TOP   0

Definition at line 179 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_UNINIT

#define VTYPE_INFO_UNINIT   8

Definition at line 187 of file java_bytecode_parser.cpp.

◆  VTYPE_INFO_UNINIT_THIS

#define VTYPE_INFO_UNINIT_THIS   6

Definition at line 185 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 1902 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
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.
Returns
parse tree, or empty std::optional on failure

Definition at line 1840 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
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.
Returns
parse tree, or empty std::optional on failure

Definition at line 1818 of file java_bytecode_parser.cpp.

AltStyle によって変換されたページ (->オリジナル) /