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 public:
25  // Disallow copy construction and copy assignment, but allow move construction
26  // and move assignment.
27  #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
30  operator=(const java_bytecode_parse_treet &) = delete;
33  #endif
34 
35  virtual ~java_bytecode_parse_treet() = default;
37  {
38  public:
40 
42  {
43  public:
46  void output(std::ostream &) const;
47  };
48 
49  typedef std::vector<element_value_pairt> element_value_pairst;
51 
52  void output(std::ostream &) const;
53  };
54 
55  typedef std::vector<annotationt> annotationst;
56 
58  const annotationst &annotations,
59  const irep_idt &annotation_type_name);
60 
62  {
63  public:
65  unsigned address;
67  typedef std::vector<exprt> argst;
69  };
70 
71  class membert
72  {
73  public:
74  std::string descriptor;
79 
80  virtual void output(std::ostream &out) const = 0;
81 
83  is_public(false), is_protected(false),
84  is_private(false), is_static(false), is_final(false)
85  {
86  }
87  };
88 
89  class methodt:public membert
90  {
91  public:
95 
96  typedef std::vector<instructiont> instructionst;
98 
100  {
101  instructions.push_back(instructiont());
102  return instructions.back();
103  }
104 
105  struct exceptiont
106  {
107  public:
109  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
110  {
111  }
112 
113  std::size_t start_pc;
114  std::size_t end_pc;
115  std::size_t handler_pc;
117  };
118 
119  typedef std::vector<exceptiont> exception_tablet;
121 
123  {
124  public:
126  std::string descriptor;
128  std::size_t index;
129  std::size_t start_pc;
130  std::size_t length;
131  };
132 
133  typedef std::vector<local_variablet> local_variable_tablet;
135 
137  {
138  public:
146  };
147 
149  {
150  public:
152  {
155  };
157  size_t offset_delta;
158  size_t chops;
159  size_t appends;
160 
161  typedef std::vector<verification_type_infot>
163  typedef std::vector<verification_type_infot>
165 
168  };
169 
170  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
172 
173  virtual void output(std::ostream &out) const;
174 
176  is_native(false),
177  is_abstract(false),
178  is_synchronized(false)
179  {
180  }
181 
182  virtual ~methodt() = default;
183  };
184 
185  class fieldt:public membert
186  {
187  public:
188  virtual ~fieldt() = default;
189  virtual void output(std::ostream &out) const;
190  bool is_enum;
191  };
192 
193  class classt
194  {
195  public:
196  classt() = default;
197 
198  // Disallow copy construction and copy assignment, but allow move
199  // construction and move assignment.
200  #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
201  classt(const classt &) = delete;
202  classt &operator=(const classt &) = delete;
203  classt(classt &&) = default;
204  classt &operator=(classt &&) = default;
205  #endif
206 
208  bool is_abstract=false;
209  bool is_enum=false;
210  bool is_public=false, is_protected=false, is_private=false;
211  bool is_final = false;
212  bool is_interface = false;
213  bool is_synthetic = false;
214  bool is_annotation = false;
216  size_t enum_elements=0;
217 
219  {
222  };
223 
224  typedef std::vector<u2> u2_valuest;
226  {
227  public:
235  {
236  }
237 
238  static lambda_method_handlet
240  {
241  lambda_method_handlet lambda_method_handle;
242  lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE;
243  lambda_method_handle.u2_values = std::move(params);
244  return lambda_method_handle;
245  }
246 
247  bool is_unknown_handle() const
248  {
250  }
251  };
252 
253  // TODO(tkiley): This map shouldn't be interacted with directly (instead
254  // TODO(tkiley): using add_method_handle and get_method_handle and instead
255  // TODO(tkiley): should be made private. TG-2785
256  typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
259 
260  typedef std::list<irep_idt> implementst;
263  typedef std::list<fieldt> fieldst;
264  typedef std::list<methodt> methodst;
268 
270  {
271  fields.push_back(fieldt());
272  return fields.back();
273  }
274 
276  {
277  methods.push_back(methodt());
278  return methods.back();
279  }
280 
281  void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle)
282  {
283  lambda_method_handle_map[{name, bootstrap_index}] = handle;
284  }
285 
286  const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
287  {
288  return lambda_method_handle_map.at({name, bootstrap_index});
289  }
290 
291  void output(std::ostream &out) const;
292 
293  };
294 
296 
297 
298  void output(std::ostream &out) const;
299 
300  typedef std::set<irep_idt> class_refst;
302 
304 
306  {
307  }
308 };
309 
313 class fieldref_exprt : public exprt
314 {
315 public:
317  const typet &type,
318  const irep_idt &component_name,
319  const irep_idt &class_name)
320  : exprt(ID_empty_string, type)
321  {
322  set(ID_class, class_name);
323  set(ID_component_name, component_name);
324  }
325 };
326 
327 #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)
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
virtual void output(std::ostream &out) const =0
virtual void output(std::ostream &out) const
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
typet & type()
Definition: expr.h:56
java_bytecode_parse_treet & operator=(const java_bytecode_parse_treet &)=delete
lambda_method_handle_mapt lambda_method_handle_map
std::vector< annotationt > annotationst
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
A reference into the symbol table.
Definition: std_types.h:110
nonstd::optional< T > optionalt
Definition: optional.h:35
std::vector< verification_type_infot > stack_verification_type_infot
void output(std::ostream &out) const
std::vector< instructiont > instructionst
classt & operator=(const classt &)=delete
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
virtual ~java_bytecode_parse_treet()=default
std::vector< verification_type_infot > local_verification_type_infot
void output(std::ostream &out) const
std::vector< element_value_pairt > element_value_pairst
API to type classes.
std::vector< stack_map_table_entryt > stack_map_tablet
uint8_t u1
Definition: bytecode_info.h:55
Base class for all expressions.
Definition: expr.h:42
std::vector< local_variablet > local_variable_tablet
virtual void output(std::ostream &out) const
void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle)
fieldref_exprt(const typet &type, const irep_idt &component_name, const irep_idt &class_name)
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt