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  {
91 
92  typedef std::vector<instructiont> instructionst;
94 
96  {
97  instructions.push_back(instructiont());
98  return instructions.back();
99  }
100 
101  struct exceptiont
102  {
104  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
105  {
106  }
107 
108  std::size_t start_pc;
109  std::size_t end_pc;
110  std::size_t handler_pc;
112  };
113 
114  typedef std::vector<exceptiont> exception_tablet;
116 
117  std::vector<irep_idt> throws_exception_table;
118 
120  {
122  std::string descriptor;
124  std::size_t index;
125  std::size_t start_pc;
126  std::size_t length;
127  };
128 
129  typedef std::vector<local_variablet> local_variable_tablet;
131 
133  {
141  };
142 
144  {
146  {
149  };
151  size_t offset_delta;
152  size_t chops;
153  size_t appends;
154 
155  typedef std::vector<verification_type_infot>
157  typedef std::vector<verification_type_infot>
159 
162  };
163 
164  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
166 
167  void output(std::ostream &out) const;
168 
170  : is_native(false),
171  is_abstract(false),
172  is_synchronized(false),
173  is_bridge(false)
174  {
175  }
176  };
177 
178  struct fieldt : public membert
179  {
180  bool is_enum;
181 
182  void output(std::ostream &out) const;
183 
184  fieldt() : is_enum(false)
185  {
186  }
187  };
188 
189  struct classt
190  {
191  classt() = default;
192 
193  // Disallow copy construction and copy assignment, but allow move
194  // construction and move assignment.
195  #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
196  classt(const classt &) = delete;
197  classt &operator=(const classt &) = delete;
198  classt(classt &&) = default;
199  classt &operator=(classt &&) = default;
200  #endif
201 
203  bool is_abstract=false;
204  bool is_enum=false;
205  bool is_public=false, is_protected=false, is_private=false;
206  bool is_final = false;
207  bool is_interface = false;
208  bool is_synthetic = false;
209  bool is_annotation = false;
210  bool is_inner_class = false;
211  bool is_static_class = false;
212  bool is_anonymous_class = false;
214  irep_idt outer_class; // when no outer class is set, there is no outer class
215  size_t enum_elements=0;
216 
218  {
221  };
222 
223  typedef std::vector<u2> u2_valuest;
225  {
233  {
234  }
235 
236  static lambda_method_handlet
238  {
239  lambda_method_handlet lambda_method_handle;
240  lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE;
241  lambda_method_handle.u2_values = std::move(params);
242  return lambda_method_handle;
243  }
244 
245  bool is_unknown_handle() const
246  {
248  }
249  };
250 
251  // TODO(tkiley): This map shouldn't be interacted with directly (instead
252  // TODO(tkiley): using add_method_handle and get_method_handle and instead
253  // TODO(tkiley): should be made private. TG-2785
254  typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
257 
258  typedef std::list<irep_idt> implementst;
261  typedef std::list<fieldt> fieldst;
262  typedef std::list<methodt> methodst;
266 
268  {
269  fields.push_back(fieldt());
270  return fields.back();
271  }
272 
274  {
275  methods.push_back(methodt());
276  return methods.back();
277  }
278 
279  void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle)
280  {
281  lambda_method_handle_map[{name, bootstrap_index}] = handle;
282  }
283 
284  const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
285  {
286  return lambda_method_handle_map.at({name, bootstrap_index});
287  }
288 
289  void output(std::ostream &out) const;
290 
291  };
292 
294 
295 
296  void output(std::ostream &out) const;
297 
298  typedef std::set<irep_idt> class_refst;
300 
302 
304  {
305  }
306 };
307 
311 class fieldref_exprt : public exprt
312 {
313 public:
315  const typet &type,
316  const irep_idt &component_name,
317  const irep_idt &class_name)
318  : exprt(ID_empty_string, type)
319  {
320  set(ID_class, class_name);
321  set(ID_component_name, component_name);
322  }
323 };
324 
325 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
The type of an expression.
Definition: type.h:22
static lambda_method_handlet create_unknown_handle(const u2_valuest params)
std::vector< instructiont > instructionst
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
typet & type()
Definition: expr.h:56
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
A reference into the symbol table.
Definition: std_types.h:110
std::vector< verification_type_infot > stack_verification_type_infot
void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle)
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:33
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
API to type classes.
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:42
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