CBMC
bytecode_info.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_BYTECODE_INFO_H
11 #define CPROVER_JAVA_BYTECODE_BYTECODE_INFO_H
12 
13 #include <cstdint>
14 
15 // http://en.wikipedia.org/wiki/Java_bytecode_instruction_listings
16 
17 // The 'result_type' is one of the following:
18 // i integer
19 // l long
20 // s short
21 // b byte
22 // c character
23 // f float
24 // d double
25 // z boolean
26 // a reference
27 
28 // The 'format' is:
29 // ' ' - just one byte
30 // 'c' - a constant_pool index, one byte
31 // 'C' - a constant_pool index, two bytes
32 // 'b' - a byte, signed
33 // 'o' - two byte branch offset
34 // 'O' - four byte branch offset
35 // 'v' - local variable index, one byte
36 // 'V' - local variable index, one byte, plus one byte, signed
37 // 'I' - two byte constant_pool index, plus two bytes
38 // 'L' - lookupswitch
39 // 'T' - tableswitch
40 // 'm' - multianewarray
41 // 't' - array subtype, one byte
42 // 's' - a short, signed
43 
45 {
46  const char *mnemonic;
47  unsigned char opcode;
48  char format;
49  unsigned pop, push;
51 };
52 
53 extern struct bytecode_infot const bytecode_info[];
54 
55 typedef uint8_t u1; // NOLINT(readability/identifiers)
56 typedef uint16_t u2; // NOLINT(readability/identifiers)
57 typedef uint32_t u4; // NOLINT(readability/identifiers)
58 typedef uint64_t u8; // NOLINT(readability/identifiers)
59 typedef int8_t s1; // NOLINT(readability/identifiers)
60 typedef int16_t s2; // NOLINT(readability/identifiers)
61 typedef int32_t s4; // NOLINT(readability/identifiers)
62 typedef int64_t s8; // NOLINT(readability/identifiers)
63 
64 // clang-format off
65 #define BC_nop 0x00
66 #define BC_aconst_null 0x01
67 #define BC_iconst_m1 0x02
68 #define BC_iconst_0 0x03
69 #define BC_iconst_1 0x04
70 #define BC_iconst_2 0x05
71 #define BC_iconst_3 0x06
72 #define BC_iconst_4 0x07
73 #define BC_iconst_5 0x08
74 #define BC_lconst_0 0x09
75 #define BC_lconst_1 0x0a
76 #define BC_fconst_0 0x0b
77 #define BC_fconst_1 0x0c
78 #define BC_fconst_2 0x0d
79 #define BC_dconst_0 0x0e
80 #define BC_dconst_1 0x0f
81 #define BC_bipush 0x10
82 #define BC_sipush 0x11
83 #define BC_ldc 0x12
84 #define BC_ldc_w 0x13
85 #define BC_ldc2_w 0x14
86 #define BC_iload 0x15
87 #define BC_lload 0x16
88 #define BC_fload 0x17
89 #define BC_dload 0x18
90 #define BC_aload 0x19
91 #define BC_iload_0 0x1a
92 #define BC_iload_1 0x1b
93 #define BC_iload_2 0x1c
94 #define BC_iload_3 0x1d
95 #define BC_lload_0 0x1e
96 #define BC_lload_1 0x1f
97 #define BC_lload_2 0x20
98 #define BC_lload_3 0x21
99 #define BC_fload_0 0x22
100 #define BC_fload_1 0x23
101 #define BC_fload_2 0x24
102 #define BC_fload_3 0x25
103 #define BC_dload_0 0x26
104 #define BC_dload_1 0x27
105 #define BC_dload_2 0x28
106 #define BC_dload_3 0x29
107 #define BC_aload_0 0x2a
108 #define BC_aload_1 0x2b
109 #define BC_aload_2 0x2c
110 #define BC_aload_3 0x2d
111 #define BC_iaload 0x2e
112 #define BC_laload 0x2f
113 #define BC_faload 0x30
114 #define BC_daload 0x31
115 #define BC_aaload 0x32
116 #define BC_baload 0x33
117 #define BC_caload 0x34
118 #define BC_saload 0x35
119 #define BC_istore 0x36
120 #define BC_lstore 0x37
121 #define BC_fstore 0x38
122 #define BC_dstore 0x39
123 #define BC_astore 0x3a
124 #define BC_istore_0 0x3b
125 #define BC_istore_1 0x3c
126 #define BC_istore_2 0x3d
127 #define BC_istore_3 0x3e
128 #define BC_lstore_0 0x3f
129 #define BC_lstore_1 0x40
130 #define BC_lstore_2 0x41
131 #define BC_lstore_3 0x42
132 #define BC_fstore_0 0x43
133 #define BC_fstore_1 0x44
134 #define BC_fstore_2 0x45
135 #define BC_fstore_3 0x46
136 #define BC_dstore_0 0x47
137 #define BC_dstore_1 0x48
138 #define BC_dstore_2 0x49
139 #define BC_dstore_3 0x4a
140 #define BC_astore_0 0x4b
141 #define BC_astore_1 0x4c
142 #define BC_astore_2 0x4d
143 #define BC_astore_3 0x4e
144 #define BC_iastore 0x4f
145 #define BC_lastore 0x50
146 #define BC_fastore 0x51
147 #define BC_dastore 0x52
148 #define BC_aastore 0x53
149 #define BC_bastore 0x54
150 #define BC_castore 0x55
151 #define BC_sastore 0x56
152 #define BC_pop 0x57
153 #define BC_pop2 0x58
154 #define BC_dup 0x59
155 #define BC_dup_x1 0x5a
156 #define BC_dup_x2 0x5b
157 #define BC_dup2 0x5c
158 #define BC_dup2_x1 0x5d
159 #define BC_dup2_x2 0x5e
160 #define BC_swap 0x5f
161 #define BC_iadd 0x60
162 #define BC_ladd 0x61
163 #define BC_fadd 0x62
164 #define BC_dadd 0x63
165 #define BC_isub 0x64
166 #define BC_lsub 0x65
167 #define BC_fsub 0x66
168 #define BC_dsub 0x67
169 #define BC_imul 0x68
170 #define BC_lmul 0x69
171 #define BC_fmul 0x6a
172 #define BC_dmul 0x6b
173 #define BC_idiv 0x6c
174 #define BC_ldiv 0x6d
175 #define BC_fdiv 0x6e
176 #define BC_ddiv 0x6f
177 #define BC_irem 0x70
178 #define BC_lrem 0x71
179 #define BC_frem 0x72
180 #define BC_drem 0x73
181 #define BC_ineg 0x74
182 #define BC_lneg 0x75
183 #define BC_fneg 0x76
184 #define BC_dneg 0x77
185 #define BC_ishl 0x78
186 #define BC_lshl 0x79
187 #define BC_ishr 0x7a
188 #define BC_lshr 0x7b
189 #define BC_iushr 0x7c
190 #define BC_lushr 0x7d
191 #define BC_iand 0x7e
192 #define BC_land 0x7f
193 #define BC_ior 0x80
194 #define BC_lor 0x81
195 #define BC_ixor 0x82
196 #define BC_lxor 0x83
197 #define BC_iinc 0x84
198 #define BC_i2l 0x85
199 #define BC_i2f 0x86
200 #define BC_i2d 0x87
201 #define BC_l2i 0x88
202 #define BC_l2f 0x89
203 #define BC_l2d 0x8a
204 #define BC_f2i 0x8b
205 #define BC_f2l 0x8c
206 #define BC_f2d 0x8d
207 #define BC_d2i 0x8e
208 #define BC_d2l 0x8f
209 #define BC_d2f 0x90
210 #define BC_i2b 0x91
211 #define BC_i2c 0x92
212 #define BC_i2s 0x93
213 #define BC_lcmp 0x94
214 #define BC_fcmpl 0x95
215 #define BC_fcmpg 0x96
216 #define BC_dcmpl 0x97
217 #define BC_dcmpg 0x98
218 #define BC_ifeq 0x99
219 #define BC_ifne 0x9a
220 #define BC_iflt 0x9b
221 #define BC_ifge 0x9c
222 #define BC_ifgt 0x9d
223 #define BC_ifle 0x9e
224 #define BC_if_icmpeq 0x9f
225 #define BC_if_icmpne 0xa0
226 #define BC_if_icmplt 0xa1
227 #define BC_if_icmpge 0xa2
228 #define BC_if_icmpgt 0xa3
229 #define BC_if_icmple 0xa4
230 #define BC_if_acmpeq 0xa5
231 #define BC_if_acmpne 0xa6
232 #define BC_goto 0xa7
233 #define BC_jsr 0xa8
234 #define BC_ret 0xa9
235 #define BC_tableswitch 0xaa
236 #define BC_lookupswitch 0xab
237 #define BC_ireturn 0xac
238 #define BC_lreturn 0xad
239 #define BC_freturn 0xae
240 #define BC_dreturn 0xaf
241 #define BC_areturn 0xb0
242 #define BC_return 0xb1
243 #define BC_getstatic 0xb2
244 #define BC_putstatic 0xb3
245 #define BC_getfield 0xb4
246 #define BC_putfield 0xb5
247 #define BC_invokevirtual 0xb6
248 #define BC_invokespecial 0xb7
249 #define BC_invokestatic 0xb8
250 #define BC_invokeinterface 0xb9
251 #define BC_invokedynamic 0xba
252 #define BC_new 0xbb
253 #define BC_newarray 0xbc
254 #define BC_anewarray 0xbd
255 #define BC_arraylength 0xbe
256 #define BC_athrow 0xbf
257 #define BC_checkcast 0xc0
258 #define BC_instanceof 0xc1
259 #define BC_monitorenter 0xc2
260 #define BC_monitorexit 0xc3
261 #define BC_wide 0xc4
262 #define BC_multianewarray 0xc5
263 #define BC_ifnull 0xc6
264 #define BC_ifnonnull 0xc7
265 #define BC_goto_w 0xc8
266 #define BC_jsr_w 0xc9
267 #define BC_breakpoint 0xca
268 #define BC_impdep1 0xfe
269 #define BC_impdep2 0xff
270 // clang-format on
271 
272 #endif // CPROVER_JAVA_BYTECODE_BYTECODE_INFO_H
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
int32_t s4
Definition: bytecode_info.h:61
uint16_t u2
Definition: bytecode_info.h:56
int64_t s8
Definition: bytecode_info.h:62
struct bytecode_infot const bytecode_info[]
uint8_t u1
Definition: bytecode_info.h:55
uint64_t u8
Definition: bytecode_info.h:58
uint32_t u4
Definition: bytecode_info.h:57
unsigned char opcode
Definition: bytecode_info.h:47
const char * mnemonic
Definition: bytecode_info.h:46