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  : messaget(_message_handler),
45  max_array_length(_max_array_length),
48  string_preprocess(_string_preprocess),
50  method_has_this(false),
52  {
53  }
54 
60 
61  void operator()(const symbolt &class_symbol, const methodt &method)
62  {
63  convert(class_symbol, method);
64  }
65 
66 protected:
68  const size_t max_array_length;
71 
76 
79 
83 
85 
90 
91 public:
92  struct holet
93  {
94  unsigned start_pc;
95  unsigned length;
96  };
97 
99  {
102  std::vector<holet> holes;
103  };
104 
105  typedef std::vector<local_variable_with_holest>
107 
108  class variablet
109  {
110  public:
112  size_t start_pc;
113  size_t length;
115  std::vector<holet> holes;
116 
118  {
119  }
120  };
121 
122 protected:
123  typedef std::vector<variablet> variablest;
125  std::set<symbol_exprt> used_local_names;
127  std::map<irep_idt, bool> class_has_clinit_method;
128  std::map<irep_idt, bool> any_superclass_has_clinit_method;
130 
132  {
135  };
136 
137  // return corresponding reference of variable
138  const variablet &find_variable_for_slot(
139  size_t address,
140  variablest &var_list);
141 
142  // JVM local variables
144  {
147  };
148 
149  const exprt variable(
150  const exprt &arg,
151  char type_char,
152  size_t address,
153  variable_cast_argumentt do_cast);
154 
155  // temporary variables
156  std::list<symbol_exprt> tmp_vars;
157 
158  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
159 
160  // JVM program locations
161  static irep_idt label(const irep_idt &address);
162 
163  // JVM Stack
164  typedef std::vector<exprt> stackt;
166 
167  exprt::operandst pop(std::size_t n);
168 
169  void pop_residue(std::size_t n);
170 
171  void push(const exprt::operandst &o);
172 
177  {
178  return v.index < slots_for_parameters;
179  }
180 
182  {
184  const instructionst::const_iterator &it,
185  const codet &_code)
186  : source(it), code(_code), done(false)
187  {
188  }
189 
190  instructionst::const_iterator source;
191  std::list<unsigned> successors;
192  std::set<unsigned> predecessors;
195  bool done;
196  };
197 
198 public:
199  typedef std::map<unsigned, converted_instructiont> address_mapt;
200  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
203 
204 protected:
205  void find_initializers(
207  const address_mapt &amap,
208  const java_cfg_dominatorst &doms);
209 
211  local_variable_table_with_holest::iterator firstvar,
212  local_variable_table_with_holest::iterator varlimit,
213  const address_mapt &amap,
214  const java_cfg_dominatorst &doms);
215 
216  void setup_local_variables(const methodt &m, const address_mapt &amap);
217 
219  {
220  bool leaf;
221  std::vector<unsigned> branch_addresses;
222  std::vector<block_tree_nodet> branch;
223 
225  {
226  }
227 
228  explicit block_tree_nodet(bool l) : leaf(l)
229  {
230  }
231 
233  {
234  return block_tree_nodet(true);
235  }
236  };
237 
238  static void replace_goto_target(
239  codet &repl,
240  const irep_idt &old_label,
241  const irep_idt &new_label);
242 
244  block_tree_nodet &tree,
245  code_blockt &this_block,
246  unsigned address_start,
247  unsigned address_limit,
248  unsigned next_block_start_address);
249 
251  block_tree_nodet &tree,
252  code_blockt &this_block,
253  unsigned address_start,
254  unsigned address_limit,
255  unsigned next_block_start_address,
256  const address_mapt &amap,
257  bool allow_merge = true);
258 
260  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
261  const size_t index);
262 
263  // conversion
264  void convert(const symbolt &class_symbol, const methodt &);
265 
267  const methodt &,
268  const code_typet &,
269  const irep_idt &,
271 
272  const bytecode_infot &get_bytecode_info(const irep_idt &statement);
273 
274  codet get_clinit_call(const irep_idt &classname);
275 
276  bool is_method_inherited(
277  const irep_idt &classname,
278  const irep_idt &methodid) const;
279 
281  const irep_idt &class_identifier, const irep_idt &component_name) const;
282 
284  {
285  VARIABLE,
286  ARRAY_REF,
287  STATIC_FIELD,
288  FIELD
289  };
290 
291  void save_stack_entries(
292  const std::string &,
293  const typet &,
294  code_blockt &,
295  const bytecode_write_typet,
296  const irep_idt &);
297 
299  const std::string &,
300  const typet &,
301  code_blockt &,
302  exprt &);
303 
304  std::vector<unsigned int> try_catch_handler(
305  unsigned int address,
307  const;
308 
310  address_mapt &address_map,
311  const std::vector<unsigned int> &jsr_ret_targets,
312  const std::vector<
313  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
314  &ret_instructions) const;
315 
317  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
318  const source_locationt &location,
319  const exprt &arg0);
320 
322  const irep_idt &statement,
323  const exprt::operandst &op,
324  const source_locationt &location);
325 
327  const irep_idt &statement,
328  const exprt &arg0,
329  const exprt::operandst &op,
330  const unsigned address,
331  const source_locationt &location);
332 
333  exprt
334  convert_aload(const irep_idt &statement, const exprt::operandst &op) const;
335 
337  const std::vector<unsigned int> &jsr_ret_targets,
338  const exprt &arg0,
339  const source_locationt &location,
340  const unsigned address);
341 
344  const irep_idt &statement,
345  const exprt::operandst &op,
346  const mp_integer &number,
347  const source_locationt &location) const;
348 
351  const exprt::operandst &op,
352  const irep_idt &id,
353  const mp_integer &number,
354  const source_locationt &location) const;
355 
358  const exprt::operandst &op,
359  const mp_integer &number,
360  const source_locationt &location) const;
361 
364  const exprt::operandst &op,
365  const mp_integer &number,
366  const source_locationt &location) const;
367 
369  const exprt &arg0,
370  const exprt &arg1,
371  const source_locationt &location,
372  unsigned address);
373 
375  const irep_idt &statement,
376  const exprt::operandst &op,
377  exprt::operandst &results) const;
378 
380  convert_cmp(const exprt::operandst &op, exprt::operandst &results) const;
381 
383  const irep_idt &statement,
384  const exprt::operandst &op,
385  exprt::operandst &results) const;
386 
387  void convert_getstatic(
388  const exprt &arg0,
389  const symbol_exprt &symbol_expr,
390  bool is_assertions_disabled_field,
391  codet &c,
392  exprt::operandst &results);
393 
394  codet convert_putfield(const exprt &arg0, const exprt::operandst &op);
395 
397  const source_locationt &location,
398  const exprt &arg0,
399  const exprt::operandst &op,
400  const symbol_exprt &symbol_expr);
401 
402  void convert_new(
403  const source_locationt &location,
404  const exprt &arg0,
405  codet &c,
406  exprt::operandst &results);
407 
408  void convert_newarray(
409  const source_locationt &location,
410  const irep_idt &statement,
411  const exprt &arg0,
412  const exprt::operandst &op,
413  codet &c,
414  exprt::operandst &results);
415 
417  const source_locationt &location,
418  const exprt &arg0,
419  const exprt::operandst &op,
420  codet &c,
421  exprt::operandst &results);
422 
424  const source_locationt &location,
425  const exprt::operandst &op) const;
426 
428  const source_locationt &location,
429  const exprt::operandst &op) const;
430 
432  const methodt &method,
433  const std::set<unsigned int> &working_set,
434  unsigned int cur_pc,
435  codet &c);
436 
437  void convert_athrow(
438  const source_locationt &location,
439  const exprt::operandst &op,
440  codet &c,
441  exprt::operandst &results) const;
442 
443  void convert_checkcast(
444  const exprt &arg0,
445  const exprt::operandst &op,
446  codet &c,
447  exprt::operandst &results) const;
448 
450 
451  void convert_invoke(
452  source_locationt location,
453  const irep_idt &statement,
454  exprt &arg0,
455  codet &c,
456  exprt::operandst &results);
457 
459  const irep_idt &statement,
460  const exprt &arg0,
461  exprt::operandst &results) const;
462 
464 
466 
467  void convert_dup2(exprt::operandst &op, exprt::operandst &results);
468 
471  const exprt::operandst &op,
473  const source_locationt &location);
474 
475  codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
476 };
477 #endif
The type of an expression.
Definition: type.h:22
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
codet convert_monitorenter(const source_locationt &location, const exprt::operandst &op) const
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
codet convert_monitorexit(const source_locationt &location, const exprt::operandst &op) const
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 convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
Base type of functions.
Definition: std_types.h:764
void convert(const symbolt &class_symbol, const methodt &)
codet convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:124
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
irep_idt method_id
Fully qualified name of the method under translation.
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address ...
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...
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
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned 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...
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.
STL namespace.
codet convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::vector< unsigned int > try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
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...
std::map< unsigned, converted_instructiont > address_mapt
codet convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
codet convert_instructions(const methodt &, const code_typet &, const irep_idt &, const java_class_typet::java_lambda_method_handlest &)
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
&#39;tree&#39; describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
codet convert_putfield(const exprt &arg0, const exprt::operandst &op)
irep_idt current_method
A copy of method_id :/.
std::vector< local_variable_with_holest > local_variable_table_with_holest
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
JAVA Bytecode Language Conversion.
void convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
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...
codet convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location)
The symbol table.
Definition: symbol_table.h:19
std::vector< instructiont > instructionst
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
java_string_library_preprocesst & string_preprocess
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:45
API to type classes.
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
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:42
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
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
create temporary variables if a write instruction can have undesired side- effects ...
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
void push(const exprt::operandst &o)
Sequential composition.
Definition: std_code.h:88
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< unsigned int > &working_set, unsigned int cur_pc, codet &c)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
A statement in a programming language.
Definition: std_code.h:21
unsigned slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
codet convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
Compute dominators for CFG of goto_function.
codet 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
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in &#39;repl&#39; that target &#39;old_label&#39; and redirect them to &#39;new_label&#39;.
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
void convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
codet convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
cfg_dominators_templatet< method_with_amapt, unsigned, false > java_cfg_dominatorst
codet 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
exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const
code_blockt convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address)
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)