cprover
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 <set>
14 #include <map>
15 
16 #include <util/optional.h>
17 #include <util/std_code.h>
18 #include <util/std_types.h>
19 
20 #include "bytecode_info.h"
21 
23 {
24  // Disallow copy construction and copy assignment, but allow move construction
25  // and move assignment.
26  #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
29  operator=(const java_bytecode_parse_treet &) = delete;
32  #endif
33 
34  struct annotationt
35  {
37 
39  {
42  void output(std::ostream &) const;
43  };
44 
45  typedef std::vector<element_value_pairt> element_value_pairst;
47 
48  void output(std::ostream &) const;
49  };
50 
51  typedef std::vector<annotationt> annotationst;
52 
54  const annotationst &annotations,
55  const irep_idt &annotation_type_name);
56 
57  struct instructiont
58  {
60  unsigned address;
62  typedef std::vector<exprt> argst;
64  };
65 
66  struct membert
67  {
68  std::string descriptor;
73 
75  is_public(false), is_protected(false),
76  is_private(false), is_static(false), is_final(false)
77  {
78  }
79 
80  bool has_annotation(const irep_idt &annotation_id) const
81  {
82  return find_annotation(annotations, annotation_id).has_value();
83  }
84  };
85 
86  struct methodt : public membert
87  {
89  bool is_native = false, is_abstract = false, is_synchronized = false,
90  is_bridge = false, is_varargs = false;
92 
93  typedef std::vector<instructiont> instructionst;
95 
97  {
98  instructions.push_back(instructiont());
99  return instructions.back();
100  }
101 
108  std::vector<annotationst> parameter_annotations;
109 
110  struct exceptiont
111  {
113  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
114  {
115  }
116 
117  std::size_t start_pc;
118  std::size_t end_pc;
119  std::size_t handler_pc;
121  };
122 
123  typedef std::vector<exceptiont> exception_tablet;
125 
126  std::vector<irep_idt> throws_exception_table;
127 
129  {
131  std::string descriptor;
133  std::size_t index;
134  std::size_t start_pc;
135  std::size_t length;
136  };
137 
138  typedef std::vector<local_variablet> local_variable_tablet;
140 
142  {
150  };
151 
153  {
155  {
158  };
160  size_t offset_delta;
161  size_t chops;
162  size_t appends;
163 
164  typedef std::vector<verification_type_infot>
166  typedef std::vector<verification_type_infot>
168 
171  };
172 
173  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
175 
176  void output(std::ostream &out) const;
177 
179  : is_native(false),
180  is_abstract(false),
181  is_synchronized(false),
182  is_bridge(false)
183  {
184  }
185  };
186 
187  struct fieldt : public membert
188  {
189  bool is_enum;
190 
191  void output(std::ostream &out) const;
192 
193  fieldt() : is_enum(false)
194  {
195  }
196  };
197 
198  struct classt
199  {
200  classt() = default;
201 
203  explicit classt(const irep_idt &name) : name(name)
204  {
205  }
206 
207  // Disallow copy construction and copy assignment, but allow move
208  // construction and move assignment.
209  #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
210  classt(const classt &) = delete;
211  classt &operator=(const classt &) = delete;
212  classt(classt &&) = default;
213  classt &operator=(classt &&) = default;
214  #endif
215 
217  bool is_abstract=false;
218  bool is_enum=false;
219  bool is_public=false, is_protected=false, is_private=false;
220  bool is_final = false;
221  bool is_interface = false;
222  bool is_synthetic = false;
223  bool is_annotation = false;
224  bool is_inner_class = false;
225  bool is_static_class = false;
226  bool is_anonymous_class = false;
228  irep_idt outer_class; // when no outer class is set, there is no outer class
229  size_t enum_elements=0;
230 
232  {
235  };
236 
237  typedef std::vector<u2> u2_valuest;
239  {
246  lambda_method_handlet() = default;
247 
249  explicit lambda_method_handlet(const u2_valuest &params)
250  : u2_values(params)
251  {
252  }
253 
256  : u2_values(std::move(params))
257  {
258  }
259 
260  bool is_unknown_handle() const
261  {
263  }
264  };
265 
266  // TODO(tkiley): This map shouldn't be interacted with directly (instead
267  // TODO(tkiley): using add_method_handle and get_method_handle and instead
268  // TODO(tkiley): should be made private. TG-2785
269  typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
272 
273  typedef std::list<irep_idt> implementst;
276  typedef std::list<fieldt> fieldst;
277  typedef std::list<methodt> methodst;
281 
283  {
284  fields.push_back(fieldt());
285  return fields.back();
286  }
287 
289  {
290  methods.push_back(methodt());
291  return methods.back();
292  }
293 
295  size_t bootstrap_index,
296  const lambda_method_handlet &handle)
297  {
298  lambda_method_handle_map[{name, bootstrap_index}] = handle;
299  }
300 
301  const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
302  {
303  return lambda_method_handle_map.at({name, bootstrap_index});
304  }
305 
306  void output(std::ostream &out) const;
307  };
308 
310 
311 
312  void output(std::ostream &out) const;
313 
314  typedef std::set<irep_idt> class_refst;
316 
317  bool loading_successful = false;
318 
320  java_bytecode_parse_treet() = default;
321 
323  explicit java_bytecode_parse_treet(const irep_idt &class_name)
324  : parsed_class(class_name)
325  {
326  }
327 };
328 
332 class fieldref_exprt : public exprt
333 {
334 public:
336  const typet &type,
337  const irep_idt &component_name,
338  const irep_idt &class_name)
339  : exprt(ID_empty_string, type)
340  {
341  set(ID_class, class_name);
342  set(ID_component_name, component_name);
343  }
344 };
345 
346 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
The type of an expression, extends irept.
Definition: type.h:27
java_bytecode_parse_treet()=default
An empty bytecode parse tree, no class name set.
std::vector< instructiont > instructionst
lambda_method_handlet(u2_valuest &&params)
Construct a lambda method handle with parameters params.
lambda_method_handlet(const u2_valuest &params)
Construct a lambda method handle with parameters params.
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
typet & type()
Return the type of the expression.
Definition: expr.h:68
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
STL namespace.
std::vector< annotationt > annotationst
bool has_annotation(const irep_idt &annotation_id) const
classt & operator=(const classt &)=delete
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt
std::vector< verification_type_infot > stack_verification_type_infot
nonstd::optional< T > optionalt
Definition: optional.h:35
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
uint16_t u2
Definition: bytecode_info.h:56
java_bytecode_parse_treet::methodt methodt
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
std::vector< stack_map_table_entryt > stack_map_tablet
java_bytecode_parse_treet & operator=(const java_bytecode_parse_treet &)=delete
std::vector< element_value_pairt > element_value_pairst
Pre-defined types.
lambda_method_handle_mapt lambda_method_handle_map
uint8_t u1
Definition: bytecode_info.h:55
void output(std::ostream &out) const
Base class for all expressions.
Definition: expr.h:54
classt(const irep_idt &name)
Create a class name.
void output(std::ostream &out) const
std::vector< local_variablet > local_variable_tablet
std::vector< verification_type_infot > local_verification_type_infot
fieldref_exprt(const typet &type, const irep_idt &component_name, const irep_idt &class_name)
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
java_bytecode_parse_treet(const irep_idt &class_name)
Create a blank parse tree for class class_name.