cprover
Loading...
Searching...
No Matches
java_bytecode_parse_tree.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
11#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
12
13#include <set>
14#include <map>
15
16#include <util/optional.h>
17#include <util/std_types.h>
18
19#include "bytecode_info.h"
20#include "java_types.h"
21
23{
24 // Disallow copy construction and copy assignment, but allow move construction
25 // and move assignment.
31
33 {
35
37 {
40 void output(std::ostream &) const;
41 };
42
43 typedef std::vector<element_value_pairt> element_value_pairst;
45
46 void output(std::ostream &) const;
47 };
48
49 typedef std::vector<annotationt> annotationst;
50
52 const annotationst &annotations,
53 const irep_idt &annotation_type_name);
54
56 {
58 unsigned address;
60 typedef std::vector<exprt> argst;
62 };
63
64 struct membert
65 {
66 std::string descriptor;
71
73 is_public(false), is_protected(false),
74 is_private(false), is_static(false), is_final(false)
75 {
76 }
77
78 bool has_annotation(const irep_idt &annotation_id) const
79 {
80 return find_annotation(annotations, annotation_id).has_value();
81 }
82 };
83
84 struct methodt : public membert
85 {
87 bool is_native = false, is_abstract = false, is_synchronized = false,
88 is_bridge = false, is_varargs = false, is_synthetic = false;
90
91 typedef std::vector<instructiont> instructionst;
93
95 {
96 instructions.push_back(instructiont());
97 return instructions.back();
98 }
99
106 std::vector<annotationst> parameter_annotations;
107
109 {
112 {
113 }
114
115 std::size_t start_pc;
116 std::size_t end_pc;
117 std::size_t handler_pc;
119 };
120
121 typedef std::vector<exceptiont> exception_tablet;
123
124 std::vector<irep_idt> throws_exception_table;
125
127 {
129 std::string descriptor;
131 std::size_t index;
132 std::size_t start_pc;
133 std::size_t length;
134 };
135
136 typedef std::vector<local_variablet> local_variable_tablet;
138
140 {
148 };
149
151 {
153 {
156 };
159 size_t chops;
160 size_t appends;
161
162 typedef std::vector<verification_type_infot>
164 typedef std::vector<verification_type_infot>
166
169 };
170
171 typedef std::vector<stack_map_table_entryt> stack_map_tablet;
173
174 void output(std::ostream &out) const;
175
177 : is_native(false),
178 is_abstract(false),
179 is_synchronized(false),
180 is_bridge(false)
181 {
182 }
183 };
184
185 struct fieldt : public membert
186 {
188
189 void output(std::ostream &out) const;
190
191 fieldt() : is_enum(false)
192 {
193 }
194 };
195
196 struct classt
197 {
198 classt() = default;
199
201 explicit classt(const irep_idt &name) : name(name)
202 {
203 }
204
205 // Disallow copy construction and copy assignment, but allow move
206 // construction and move assignment.
207 classt(const classt &) = delete;
208 classt &operator=(const classt &) = delete;
209 classt(classt &&) = default;
210 classt &operator=(classt &&) = default;
211
213 bool is_abstract=false;
214 bool is_enum=false;
215 bool is_public=false, is_protected=false, is_private=false;
216 bool is_final = false;
217 bool is_interface = false;
218 bool is_synthetic = false;
219 bool is_annotation = false;
220 bool is_inner_class = false;
221 bool is_static_class = false;
222 bool is_anonymous_class = false;
224 irep_idt outer_class; // when no outer class is set, there is no outer class
226
227 typedef std::vector<u2> u2_valuest;
229 {
232
238 {
241 }
242
244 : handle_type(java_class_typet::method_handle_kindt::UNKNOWN_HANDLE),
246 {
247 }
248
250 {
251 return lambda_method_handlet{};
252 }
253
254 bool is_unknown_handle() const
255 {
256 return handle_type ==
258 }
259
261 {
263 return *method_descriptor;
264 }
265 };
266
267 // TODO(tkiley): This map shouldn't be interacted with directly (instead
268 // TODO(tkiley): using add_method_handle and get_method_handle and instead
269 // TODO(tkiley): should be made private. TG-2785
270 typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
273
274 typedef std::list<irep_idt> implementst;
277 typedef std::list<fieldt> fieldst;
278 typedef std::list<methodt> methodst;
282
284 {
285 fields.push_back(fieldt());
286 return fields.back();
287 }
288
290 {
291 methods.push_back(methodt());
292 return methods.back();
293 }
294
296 size_t bootstrap_index,
297 const lambda_method_handlet &handle)
298 {
299 lambda_method_handle_map[{name, bootstrap_index}] = handle;
300 }
301
302 const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
303 {
304 return lambda_method_handle_map.at({name, bootstrap_index});
305 }
306
307 void output(std::ostream &out) const;
308 };
309
311
312
313 void output(std::ostream &out) const;
314
315 typedef std::set<irep_idt> class_refst;
317
318 bool loading_successful = false;
319
322
324 explicit java_bytecode_parse_treet(const irep_idt &class_name)
325 : parsed_class(class_name)
326 {
327 }
328};
329
333class fieldref_exprt : public exprt
334{
335public:
337 const typet &type,
339 const irep_idt &class_name)
340 : exprt(ID_empty_string, type)
341 {
342 set(ID_class, class_name);
343 set(ID_component_name, component_name);
344 }
345
347 {
348 return get(ID_class);
349 }
350
352 {
353 return get(ID_component_name);
354 }
355};
356
357template <>
358inline bool can_cast_expr<fieldref_exprt>(const exprt &base)
359{
360 return !base.get(ID_class).empty() && !base.get(ID_component_name).empty();
361}
362
363#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
uint16_t u2
Definition: bytecode_info.h:56
uint8_t u1
Definition: bytecode_info.h:55
uint64_t u8
Definition: bytecode_info.h:58
An expression describing a method on a class.
Definition: std_expr.h:3272
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
irep_idt class_name() const
irep_idt component_name() const
fieldref_exprt(const typet &type, const irep_idt &component_name, const irep_idt &class_name)
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition: java_types.h:465
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
The type of an expression, extends irept.
Definition: type.h:29
bool can_cast_expr< fieldref_exprt >(const exprt &base)
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.
std::vector< element_value_pairt > element_value_pairst
optionalt< class_method_descriptor_exprt > method_descriptor
lambda_method_handlet(const class_method_descriptor_exprt &method_descriptor, java_class_typet::method_handle_kindt handle_type)
Construct a lambda method handle with parameters params.
const class_method_descriptor_exprt & get_method_descriptor() const
classt(const classt &)=delete
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt
classt & operator=(classt &&)=default
lambda_method_handle_mapt lambda_method_handle_map
void output(std::ostream &out) const
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
classt(const irep_idt &name)
Create a class name.
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
classt & operator=(const classt &)=delete
bool has_annotation(const irep_idt &annotation_id) const
std::vector< verification_type_infot > stack_verification_type_infot
std::vector< verification_type_infot > local_verification_type_infot
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
std::vector< local_variablet > local_variable_tablet
std::vector< instructiont > instructionst
std::vector< stack_map_table_entryt > stack_map_tablet
java_bytecode_parse_treet & operator=(java_bytecode_parse_treet &&)=default
java_bytecode_parse_treet(const irep_idt &class_name)
Create a blank parse tree for class class_name.
java_bytecode_parse_treet & operator=(const java_bytecode_parse_treet &)=delete
java_bytecode_parse_treet(java_bytecode_parse_treet &&)=default
std::vector< annotationt > annotationst
java_bytecode_parse_treet(const java_bytecode_parse_treet &)=delete
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
java_bytecode_parse_treet()=default
An empty bytecode parse tree, no class name set.
void output(std::ostream &out) const