cprover
java_bytecode_convert_method_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
14 
15 #include "ci_lazy_methods_needed.h"
18 
19 #include <util/expanding_vector.h>
20 #include <util/message.h>
21 #include <util/std_types.h>
22 #include <util/std_expr.h>
23 
25 
26 #include <vector>
27 #include <list>
28 
29 class symbol_tablet;
30 class symbolt;
31 
33 {
34 public:
37  message_handlert &_message_handler,
38  size_t _max_array_length,
41  java_string_library_preprocesst &_string_preprocess,
43  bool threading_support)
44  : messaget(_message_handler),
46  max_array_length(_max_array_length),
50  string_preprocess(_string_preprocess),
52  method_has_this(false),
54  {
55  }
56 
62 
63  void operator()(const symbolt &class_symbol, const methodt &method)
64  {
65  convert(class_symbol, method);
66  }
67 
68  typedef uint16_t method_offsett;
69 
70 protected:
72  const size_t max_array_length;
74  const bool threading_support;
76 
81 
84 
88 
90 
95 
96 public:
97  struct holet
98  {
101  };
102 
104  {
107  std::vector<holet> holes;
108  };
109 
110  typedef std::vector<local_variable_with_holest>
112 
113  class variablet
114  {
115  public:
117  size_t start_pc;
118  size_t length;
120  std::vector<holet> holes;
121 
123  {
124  }
125  };
126 
127 protected:
128  typedef std::vector<variablet> variablest;
130  std::set<symbol_exprt> used_local_names;
132  std::map<irep_idt, bool> class_has_clinit_method;
133  std::map<irep_idt, bool> any_superclass_has_clinit_method;
135 
137  {
140  };
141 
142  // return corresponding reference of variable
143  const variablet &find_variable_for_slot(
144  size_t address,
145  variablest &var_list);
146 
147  // JVM local variables
149  {
152  };
153 
154  exprt variable(
155  const exprt &arg,
156  char type_char,
157  size_t address,
158  variable_cast_argumentt do_cast);
159 
160  // temporary variables
161  std::list<symbol_exprt> tmp_vars;
162 
163  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
164 
165  // JVM program locations
166  static irep_idt label(const irep_idt &address);
167 
168  // JVM Stack
169  typedef std::vector<exprt> stackt;
171 
172  exprt::operandst pop(std::size_t n);
173 
174  void pop_residue(std::size_t n);
175 
176  void push(const exprt::operandst &o);
177 
182  {
183  return v.index < slots_for_parameters;
184  }
185 
187  {
189  const instructionst::const_iterator &it,
190  const codet &_code)
191  : source(it), code(_code), done(false)
192  {
193  }
194 
195  instructionst::const_iterator source;
196  std::list<method_offsett> successors;
197  std::set<method_offsett> predecessors;
200  bool done;
201  };
202 
203 public:
204  typedef std::map<method_offsett, converted_instructiont> address_mapt;
205  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
208 
209 protected:
210  void find_initializers(
212  const address_mapt &amap,
213  const java_cfg_dominatorst &doms);
214 
216  local_variable_table_with_holest::iterator firstvar,
217  local_variable_table_with_holest::iterator varlimit,
218  const address_mapt &amap,
219  const java_cfg_dominatorst &doms);
220 
221  void setup_local_variables(const methodt &m, const address_mapt &amap);
222 
224  {
225  bool leaf;
226  std::vector<method_offsett> branch_addresses;
227  std::vector<block_tree_nodet> branch;
228 
230  {
231  }
232 
233  explicit block_tree_nodet(bool l) : leaf(l)
234  {
235  }
236 
238  {
239  return block_tree_nodet(true);
240  }
241  };
242 
243  static void replace_goto_target(
244  codet &repl,
245  const irep_idt &old_label,
246  const irep_idt &new_label);
247 
249  block_tree_nodet &tree,
250  code_blockt &this_block,
251  method_offsett address_start,
252  method_offsett address_limit,
253  method_offsett next_block_start_address);
254 
256  block_tree_nodet &tree,
257  code_blockt &this_block,
258  method_offsett address_start,
259  method_offsett address_limit,
260  method_offsett next_block_start_address,
261  const address_mapt &amap,
262  bool allow_merge = true);
263 
265  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
266  const size_t index);
267 
268  // conversion
269  void convert(const symbolt &class_symbol, const methodt &);
270 
272  const methodt &,
274 
275  const bytecode_infot &get_bytecode_info(const irep_idt &statement);
276 
277  codet get_clinit_call(const irep_idt &classname);
278 
279  bool is_method_inherited(
280  const irep_idt &classname,
281  const irep_idt &methodid) const;
282 
284  const irep_idt &class_identifier, const irep_idt &component_name) const;
285 
287  {
288  VARIABLE,
289  ARRAY_REF,
290  STATIC_FIELD,
291  FIELD
292  };
293 
294  void save_stack_entries(
295  const std::string &,
296  code_blockt &,
297  const bytecode_write_typet,
298  const irep_idt &);
299 
301  const std::string &,
302  const typet &,
303  code_blockt &,
304  exprt &);
305 
306  std::vector<method_offsett> try_catch_handler(
307  method_offsett address,
309  const;
310 
312  address_mapt &address_map,
313  const std::vector<method_offsett> &jsr_ret_targets,
314  const std::vector<
315  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
316  &ret_instructions) const;
317 
319  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
320  const source_locationt &location,
321  const exprt &arg0);
322 
324  const irep_idt &statement,
325  const exprt::operandst &op,
326  const source_locationt &location);
327 
329  const irep_idt &statement,
330  const exprt &arg0,
331  const exprt::operandst &op,
332  const method_offsett address,
333  const source_locationt &location);
334 
335  exprt
336  convert_aload(const irep_idt &statement, const exprt::operandst &op) const;
337 
339  const std::vector<method_offsett> &jsr_ret_targets,
340  const exprt &arg0,
341  const source_locationt &location,
342  const method_offsett address);
343 
346  const irep_idt &statement,
347  const exprt::operandst &op,
348  const mp_integer &number,
349  const source_locationt &location) const;
350 
353  const exprt::operandst &op,
354  const irep_idt &id,
355  const mp_integer &number,
356  const source_locationt &location) const;
357 
360  const exprt::operandst &op,
361  const mp_integer &number,
362  const source_locationt &location) const;
363 
366  const exprt::operandst &op,
367  const mp_integer &number,
368  const source_locationt &location) const;
369 
371  const exprt &arg0,
372  const exprt &arg1,
373  const source_locationt &location,
374  method_offsett address);
375 
377  const irep_idt &statement,
378  const exprt::operandst &op,
379  exprt::operandst &results) const;
380 
382  convert_cmp(const exprt::operandst &op, exprt::operandst &results) const;
383 
385  const irep_idt &statement,
386  const exprt::operandst &op,
387  exprt::operandst &results) const;
388 
389  void convert_getstatic(
390  const exprt &arg0,
391  const symbol_exprt &symbol_expr,
392  bool is_assertions_disabled_field,
393  codet &c,
394  exprt::operandst &results);
395 
396  code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op);
397 
399  const source_locationt &location,
400  const exprt &arg0,
401  const exprt::operandst &op,
402  const symbol_exprt &symbol_expr);
403 
404  void convert_new(
405  const source_locationt &location,
406  const exprt &arg0,
407  codet &c,
408  exprt::operandst &results);
409 
411  const source_locationt &location,
412  const irep_idt &statement,
413  const exprt &arg0,
414  const exprt::operandst &op,
415  exprt::operandst &results);
416 
418  const source_locationt &location,
419  const exprt &arg0,
420  const exprt::operandst &op,
421  exprt::operandst &results);
422 
424  const methodt &method,
425  const std::set<method_offsett> &working_set,
426  method_offsett cur_pc,
427  codet &c);
428 
429  void convert_athrow(
430  const source_locationt &location,
431  const exprt::operandst &op,
432  codet &c,
433  exprt::operandst &results) const;
434 
435  void convert_checkcast(
436  const exprt &arg0,
437  const exprt::operandst &op,
438  codet &c,
439  exprt::operandst &results) const;
440 
442  const irep_idt &statement,
443  const exprt::operandst &op,
444  const source_locationt &source_location);
445 
447 
448  void convert_invoke(
449  source_locationt location,
450  const irep_idt &statement,
451  exprt &arg0,
452  codet &c,
453  exprt::operandst &results);
454 
456  const irep_idt &statement,
457  const exprt &arg0,
458  exprt::operandst &results) const;
459 
461 
463 
464  void convert_dup2(exprt::operandst &op, exprt::operandst &results);
465 
467  const exprt::operandst &op,
469  const source_locationt &location);
470 
471  codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
472 };
473 #endif
code_blockt convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
The type of an expression, extends irept.
Definition: type.h:27
java_bytecode_convert_methodt::address_mapt address_mapt
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
methodt::local_variable_tablet local_variable_tablet
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
BigInt mp_integer
Definition: mp_arith.h:22
codet representing a switch statement.
Definition: std_code.h:705
void convert(const symbolt &class_symbol, const methodt &)
void find_initializers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
See find_initializers_for_slot above for more detail.
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
std::pair< const methodt &, const address_mapt & > method_with_amapt
exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns an expression indicating a local variable suitable to load/store from a bytecode at address a...
irep_idt method_id
Fully qualified name of the method under translation.
Non-graph-based representation of the class hierarchy.
optionalt< symbolt > get_lambda_method_symbol(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
code_ifthenelset convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< instructiont > instructionst
code_blockt convert_ret(const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
void operator()(const symbolt &class_symbol, const methodt &method)
bool is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const
Returns true iff method methodid from class classname is a method inherited from a class (and not an ...
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
static irep_idt label(const irep_idt &address)
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
code_blockt convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)
Symbol table entry.
Definition: symbol.h:27
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
code_ifthenelset convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
irept::subt java_lambda_method_handlest
Definition: java_types.h:196
code_blockt convert_instructions(const methodt &, const java_class_typet::java_lambda_method_handlest &)
irep_idt current_method
A copy of method_id :/.
std::vector< local_variable_with_holest > local_variable_table_with_holest
code_blockt convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
java_bytecode_parse_treet::methodt methodt
cfg_dominators_templatet< method_with_amapt, method_offsett, false > java_cfg_dominatorst
JAVA Bytecode Language Conversion.
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
API to expression classes.
exprt::operandst & convert_const(const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const
irep_idt get_static_field(const irep_idt &class_identifier, const irep_idt &component_name) const
Get static field identifier referred to by class_identifier.component_name Note this may be inherited...
The symbol table.
Definition: symbol_table.h:19
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op)
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
code_ifthenelset convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
code_ifthenelset convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
java_string_library_preprocesst & string_preprocess
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge=true)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
codet get_clinit_call(const irep_idt &classname)
Each static access to classname should be prefixed with a check for necessary static init; this retur...
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
java_bytecode_parse_treet::instructiont instructiont
typet method_return_type
Return type of the method under conversion.
exprt::operandst pop(std::size_t n)
std::vector< exprt > operandst
Definition: expr.h:57
code_switcht convert_switch(const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< method_offsett > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
Pre-defined types.
code_blockt convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
code_blockt convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
void create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)
actually create a temporary variable to hold the value of a stack entry
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
void convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
Base class for all expressions.
Definition: expr.h:54
The symbol table base class interface.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
std::vector< local_variablet > local_variable_tablet
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
void push(const exprt::operandst &o)
A codet representing sequential composition of program statements.
Definition: std_code.h:150
void find_initializers_for_slot(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)
Given a sequence of users of the same local variable slot, this figures out which ones are related by...
Context-insensitive lazy methods container.
codet & do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)
codet representation of an if-then-else statement.
Definition: std_code.h:614
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
code_blockt convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
std::map< method_offsett, converted_instructiont > address_mapt
Compute dominators for CFG of goto_function.
std::vector< method_offsett > try_catch_handler(method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
optionalt< exprt > convert_invoke_dynamic(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0)
std::map< irep_idt, bool > any_superclass_has_clinit_method
exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const
void save_stack_entries(const std::string &, code_blockt &, const bytecode_write_typet, const irep_idt &)
Create temporary variables if a write instruction can have undesired side- effects.
java_bytecode_convert_methodt(symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)