CBMC
java_bytecode_parse_tree.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_JAVA_BYTECODE_PARSE_TREE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
12 
13 #include <util/std_types.h>
14 
15 #include "bytecode_info.h"
16 #include "java_types.h"
17 
18 #include <list>
19 #include <map>
20 #include <set>
21 
23 {
24  // Disallow copy construction and copy assignment, but allow move construction
25  // and move assignment.
31 
32  struct annotationt
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 
51  static std::optional<annotationt> find_annotation(
52  const annotationst &annotations,
53  const irep_idt &annotation_type_name);
54 
55  struct instructiont
56  {
58  unsigned address;
60  typedef std::vector<exprt> argst;
62  };
63 
64  struct membert
65  {
66  std::string descriptor;
67  std::optional<std::string> signature;
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 
108  struct exceptiont
109  {
111  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
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;
130  std::optional<std::string> signature;
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  };
158  size_t offset_delta;
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  {
187  bool is_enum;
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
225  size_t enum_elements=0;
226 
227  typedef std::vector<u2> u2_valuest;
229  {
231  std::optional<class_method_descriptor_exprt> method_descriptor;
232 
238  {
239  PRECONDITION(
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;
276  std::optional<std::string> signature;
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 
333 class fieldref_exprt : public exprt
334 {
335 public:
337  const typet &type,
338  const irep_idt &component_name,
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 
357 template <>
358 inline 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:3495
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
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:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition: java_types.h:464
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
The type of an expression, extends irept.
Definition: type.h:29
bool can_cast_expr< fieldref_exprt >(const exprt &base)
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
java_bytecode_parse_treet::methodt methodt
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.
std::vector< element_value_pairt > element_value_pairst
std::optional< 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
classt & operator=(const classt &)=delete
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
lambda_method_handle_mapt lambda_method_handle_map
void output(std::ostream &out) const
std::optional< std::string > signature
classt(const irep_idt &name)
Create a class name.
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
classt & operator=(classt &&)=default
bool has_annotation(const irep_idt &annotation_id) const
std::optional< std::string > signature
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=(const java_bytecode_parse_treet &)=delete
java_bytecode_parse_treet(const irep_idt &class_name)
Create a blank parse tree for class class_name.
java_bytecode_parse_treet(java_bytecode_parse_treet &&)=default
std::vector< annotationt > annotationst
static std::optional< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
java_bytecode_parse_treet(const java_bytecode_parse_treet &)=delete
java_bytecode_parse_treet & operator=(java_bytecode_parse_treet &&)=default
java_bytecode_parse_treet()=default
An empty bytecode parse tree, no class name set.
void output(std::ostream &out) const