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,
45  : log(_message_handler),
48  max_array_length(_max_array_length),
53  string_preprocess(_string_preprocess),
55  method_has_this(false),
57  {
58  }
59 
65 
66  void operator()(
67  const symbolt &class_symbol,
68  const methodt &method,
69  const optionalt<prefix_filtert> &method_context)
70  {
71  convert(class_symbol, method, method_context);
72  }
73 
74  typedef uint16_t method_offsett;
75 
76 protected:
80  const size_t max_array_length;
83  const bool threading_support;
85 
90 
93 
97 
99 
104 
105 public:
106  struct holet
107  {
110  };
111 
113  {
116  std::vector<holet> holes;
117  };
118 
119  typedef std::vector<local_variable_with_holest>
121 
122  class variablet
123  {
124  public:
126  size_t start_pc;
127  size_t length;
128  bool is_parameter = false;
129  std::vector<holet> holes;
130 
132  const symbol_exprt &_symbol_expr,
133  std::size_t _start_pc,
134  std::size_t _length)
135  : symbol_expr(_symbol_expr), start_pc(_start_pc), length(_length)
136  {
137  }
138 
140  const symbol_exprt &_symbol_expr,
141  std::size_t _start_pc,
142  std::size_t _length,
143  bool _is_parameter)
144  : symbol_expr(_symbol_expr),
145  start_pc(_start_pc),
146  length(_length),
147  is_parameter(_is_parameter)
148  {
149  }
150 
152  const symbol_exprt &_symbol_expr,
153  std::size_t _start_pc,
154  std::size_t _length,
155  bool _is_parameter,
156  std::vector<holet> &&_holes)
157  : symbol_expr(_symbol_expr),
158  start_pc(_start_pc),
159  length(_length),
160  is_parameter(_is_parameter),
161  holes(std::move(_holes))
162  {
163  }
164  };
165 
166 protected:
167  typedef std::vector<variablet> variablest;
169  std::set<symbol_exprt> used_local_names;
171  std::map<irep_idt, bool> class_has_clinit_method;
172  std::map<irep_idt, bool> any_superclass_has_clinit_method;
174 
176  {
178  INST_INDEX_CONST = 3
179  };
180 
181  // return corresponding reference of variable
182  const variablet &find_variable_for_slot(
183  size_t address,
184  variablest &var_list);
185 
186  // JVM local variables
188  {
190  NO_CAST
191  };
192 
193  exprt variable(const exprt &arg, char type_char, size_t address);
194 
195  // temporary variables
196  std::list<symbol_exprt> tmp_vars;
197 
198  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
199 
200  // JVM program locations
201  static irep_idt label(const irep_idt &address);
202 
203  // JVM Stack
204  typedef std::vector<exprt> stackt;
206 
207  exprt::operandst pop(std::size_t n);
208 
209  void pop_residue(std::size_t n);
210 
211  void push(const exprt::operandst &o);
212 
217  {
218  return v.index < slots_for_parameters;
219  }
220 
222  {
224  const instructionst::const_iterator &it,
225  const codet &_code)
226  : source(it), code(_code), done(false)
227  {
228  }
229 
230  instructionst::const_iterator source;
231  std::list<method_offsett> successors;
232  std::set<method_offsett> predecessors;
235  bool done;
236  };
237 
238 public:
239  typedef std::map<method_offsett, converted_instructiont> address_mapt;
240  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
243 
244 protected:
245  void find_initializers(
247  const address_mapt &amap,
248  const java_cfg_dominatorst &doms);
249 
251  local_variable_table_with_holest::iterator firstvar,
252  local_variable_table_with_holest::iterator varlimit,
253  const address_mapt &amap,
254  const java_cfg_dominatorst &doms);
255 
256  void setup_local_variables(const methodt &m, const address_mapt &amap);
257 
259  {
260  bool leaf;
261  std::vector<method_offsett> branch_addresses;
262  std::vector<block_tree_nodet> branch;
263 
265  {
266  }
267 
268  explicit block_tree_nodet(bool l) : leaf(l)
269  {
270  }
271 
273  {
274  return block_tree_nodet(true);
275  }
276  };
277 
278  static void replace_goto_target(
279  codet &repl,
280  const irep_idt &old_label,
281  const irep_idt &new_label);
282 
284  block_tree_nodet &tree,
285  code_blockt &this_block,
286  method_offsett address_start,
287  method_offsett address_limit,
288  method_offsett next_block_start_address);
289 
291  block_tree_nodet &tree,
292  code_blockt &this_block,
293  method_offsett address_start,
294  method_offsett address_limit,
295  method_offsett next_block_start_address,
296  const address_mapt &amap,
297  bool allow_merge = true);
298 
299  // conversion
300  void convert(
301  const symbolt &class_symbol,
302  const methodt &,
303  const optionalt<prefix_filtert> &method_context);
304 
306  const methodt &method,
307  const java_method_typet &method_type);
308 
310 
311  codet get_clinit_call(const irep_idt &classname);
312 
313  bool is_method_inherited(
314  const irep_idt &classname,
315  const irep_idt &mangled_method_name) const;
316 
318  const irep_idt &class_identifier, const irep_idt &component_name) const;
319 
321  {
322  VARIABLE,
323  ARRAY_REF,
324  STATIC_FIELD,
325  FIELD
326  };
327 
328  void save_stack_entries(
329  const std::string &,
330  code_blockt &,
331  const bytecode_write_typet,
332  const irep_idt &);
333 
335  const std::string &,
336  const typet &,
337  code_blockt &,
338  exprt &);
339 
340  std::vector<method_offsett> try_catch_handler(
341  method_offsett address,
343  const;
344 
346  address_mapt &address_map,
347  const std::vector<method_offsett> &jsr_ret_targets,
348  const std::vector<
349  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
350  &ret_instructions) const;
351 
353  const source_locationt &location,
354  std::size_t instruction_address,
355  const exprt &arg0,
356  codet &result_code);
357 
359  const irep_idt &statement,
360  const exprt::operandst &op,
361  const source_locationt &location);
362 
364  const irep_idt &statement,
365  const exprt &arg0,
366  const exprt::operandst &op,
367  const method_offsett address,
368  const source_locationt &location);
369 
370  static exprt
371  convert_aload(const irep_idt &statement, const exprt::operandst &op);
372 
382  exprt convert_load(const exprt &index, char type_char, size_t address);
383 
385  const std::vector<method_offsett> &jsr_ret_targets,
386  const exprt &arg0,
387  const source_locationt &location,
388  const method_offsett address);
389 
392  const u1 bytecode,
393  const exprt::operandst &op,
394  const mp_integer &number,
395  const source_locationt &location) const;
396 
399  const exprt::operandst &op,
400  const irep_idt &id,
401  const mp_integer &number,
402  const source_locationt &location) const;
403 
406  const exprt::operandst &op,
407  const mp_integer &number,
408  const source_locationt &location) const;
409 
412  const exprt::operandst &op,
413  const mp_integer &number,
414  const source_locationt &location) const;
415 
417  const exprt &arg0,
418  const exprt &arg1,
419  const source_locationt &location,
420  method_offsett address);
421 
423  const irep_idt &statement,
424  const exprt::operandst &op,
425  exprt::operandst &results) const;
426 
428  const irep_idt &statement,
429  const exprt::operandst &op,
430  exprt::operandst &results) const;
431 
433  convert_cmp(const exprt::operandst &op, exprt::operandst &results) const;
434 
436  const irep_idt &statement,
437  const exprt::operandst &op,
438  exprt::operandst &results) const;
439 
440  void convert_getstatic(
441  const source_locationt &source_location,
442  const exprt &arg0,
443  const symbol_exprt &symbol_expr,
444  bool is_assertions_disabled_field,
445  codet &c,
446  exprt::operandst &results);
447 
449  convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op);
450 
452  const source_locationt &location,
453  const exprt &arg0,
454  const exprt::operandst &op,
455  const symbol_exprt &symbol_expr);
456 
457  void convert_new(
458  const source_locationt &location,
459  const exprt &arg0,
460  codet &c,
461  exprt::operandst &results);
462 
464  const source_locationt &location,
465  const irep_idt &statement,
466  const exprt &arg0,
467  const exprt::operandst &op,
468  exprt::operandst &results);
469 
471  const source_locationt &location,
472  const exprt &arg0,
473  const exprt::operandst &op,
474  exprt::operandst &results);
475 
477  const methodt &method,
478  const std::set<method_offsett> &working_set,
479  method_offsett cur_pc,
480  codet &c);
481 
482  void convert_athrow(
483  const source_locationt &location,
484  const exprt::operandst &op,
485  codet &c,
486  exprt::operandst &results) const;
487 
488  void convert_checkcast(
489  const exprt &arg0,
490  const exprt::operandst &op,
491  codet &c,
492  exprt::operandst &results) const;
493 
495  const irep_idt &statement,
496  const exprt::operandst &op,
497  const source_locationt &source_location);
498 
500 
501  void convert_invoke(
502  source_locationt location,
503  const irep_idt &statement,
504  class_method_descriptor_exprt &class_method_descriptor,
505  codet &c,
506  exprt::operandst &results);
507 
509  const irep_idt &statement,
510  const constant_exprt &arg0,
511  exprt::operandst &results) const;
512 
514 
516 
517  void convert_dup2(exprt::operandst &op, exprt::operandst &results);
518 
520  const exprt::operandst &op,
522  const source_locationt &location);
523 
524  codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
525 
527 };
528 #endif
uint8_t u1
Definition: bytecode_info.h:55
Compute dominators for CFG of goto_function.
Context-insensitive lazy methods container.
Non-graph-based representation of the class hierarchy.
An expression describing a method on a class.
Definition: std_expr.h:3111
A codet representing sequential composition of program statements.
Definition: std_code.h:170
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representing a switch statement.
Definition: std_code.h:866
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
A constant literal expression.
Definition: std_expr.h:2668
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter, std::vector< holet > &&_holes)
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter)
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length)
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
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...
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
code_ifthenelset convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const u1 bytecode, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
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
cfg_dominators_templatet< method_with_amapt, method_offsett, false > java_cfg_dominatorst
codet & do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
exprt convert_load(const exprt &index, char type_char, size_t address)
Load reference from local variable.
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void push(const exprt::operandst &o)
code_blockt convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
code_blockt convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
static irep_idt label(const irep_idt &address)
std::vector< method_offsett > try_catch_handler(method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
code_blockt convert_instructions(const methodt &)
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
java_string_library_preprocesst & string_preprocess
code_blockt convert_ret(const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
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.
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...
code_blockt convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
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
java_bytecode_parse_treet::methodt methodt
std::vector< local_variable_with_holest > local_variable_table_with_holest
std::pair< const methodt &, const address_mapt & > method_with_amapt
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
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 ...
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...
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
exprt::operandst pop(std::size_t n)
java_bytecode_parse_treet::instructiont instructiont
exprt::operandst & convert_const(const irep_idt &statement, const constant_exprt &arg0, exprt::operandst &results) const
void operator()(const symbolt &class_symbol, const methodt &method, const optionalt< prefix_filtert > &method_context)
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
code_blockt convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op)
code_blockt convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
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
void convert(const symbolt &class_symbol, const methodt &, const optionalt< prefix_filtert > &method_context)
code_blockt convert_parameter_annotations(const methodt &method, const java_method_typet &method_type)
code_switcht convert_switch(const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
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.
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...
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
exprt variable(const exprt &arg, char type_char, size_t address)
Returns an expression indicating a local variable suitable to load/store from a bytecode at address a...
std::map< method_offsett, converted_instructiont > address_mapt
methodt::local_variable_tablet local_variable_tablet
std::map< irep_idt, bool > any_superclass_has_clinit_method
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'.
code_blockt convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
optionalt< exprt > convert_invoke_dynamic(const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code)
bool is_method_inherited(const irep_idt &classname, const irep_idt &mangled_method_name) const
Returns true iff method methodid from class classname is a method inherited from a class or interface...
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
typet method_return_type
Return type of the method under conversion.
void convert_getstatic(const source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
irep_idt method_id
Fully qualified name of the method under translation.
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_shl(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
void convert_invoke(source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results)
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...
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, bool assert_no_exceptions_thrown)
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
irep_idt current_method
A copy of method_id :/.
static exprt convert_aload(const irep_idt &statement, const exprt::operandst &op)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
JAVA Bytecode Language Conversion.
java_bytecode_convert_methodt::address_mapt address_mapt
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.
Pre-defined types.
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
std::vector< local_variablet > local_variable_tablet
std::vector< instructiont > instructionst