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  : messaget(_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:
79  const size_t max_array_length;
82  const bool threading_support;
84 
89 
92 
96 
98 
103 
104 public:
105  struct holet
106  {
109  };
110 
112  {
115  std::vector<holet> holes;
116  };
117 
118  typedef std::vector<local_variable_with_holest>
120 
121  class variablet
122  {
123  public:
125  size_t start_pc;
126  size_t length;
127  bool is_parameter = false;
128  std::vector<holet> holes;
129 
131  const symbol_exprt &_symbol_expr,
132  std::size_t _start_pc,
133  std::size_t _length)
134  : symbol_expr(_symbol_expr), start_pc(_start_pc), length(_length)
135  {
136  }
137 
139  const symbol_exprt &_symbol_expr,
140  std::size_t _start_pc,
141  std::size_t _length,
142  bool _is_parameter)
143  : symbol_expr(_symbol_expr),
144  start_pc(_start_pc),
145  length(_length),
146  is_parameter(_is_parameter)
147  {
148  }
149 
151  const symbol_exprt &_symbol_expr,
152  std::size_t _start_pc,
153  std::size_t _length,
154  bool _is_parameter,
155  std::vector<holet> &&_holes)
156  : symbol_expr(_symbol_expr),
157  start_pc(_start_pc),
158  length(_length),
159  is_parameter(_is_parameter),
160  holes(std::move(_holes))
161  {
162  }
163  };
164 
165 protected:
166  typedef std::vector<variablet> variablest;
168  std::set<symbol_exprt> used_local_names;
170  std::map<irep_idt, bool> class_has_clinit_method;
171  std::map<irep_idt, bool> any_superclass_has_clinit_method;
173 
175  {
177  INST_INDEX_CONST = 3
178  };
179 
180  // return corresponding reference of variable
181  const variablet &find_variable_for_slot(
182  size_t address,
183  variablest &var_list);
184 
185  // JVM local variables
187  {
189  NO_CAST
190  };
191 
192  exprt variable(const exprt &arg, char type_char, size_t address);
193 
194  // temporary variables
195  std::list<symbol_exprt> tmp_vars;
196 
197  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
198 
199  // JVM program locations
200  static irep_idt label(const irep_idt &address);
201 
202  // JVM Stack
203  typedef std::vector<exprt> stackt;
205 
206  exprt::operandst pop(std::size_t n);
207 
208  void pop_residue(std::size_t n);
209 
210  void push(const exprt::operandst &o);
211 
216  {
217  return v.index < slots_for_parameters;
218  }
219 
221  {
223  const instructionst::const_iterator &it,
224  const codet &_code)
225  : source(it), code(_code), done(false)
226  {
227  }
228 
229  instructionst::const_iterator source;
230  std::list<method_offsett> successors;
231  std::set<method_offsett> predecessors;
234  bool done;
235  };
236 
237 public:
238  typedef std::map<method_offsett, converted_instructiont> address_mapt;
239  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
242 
243 protected:
244  void find_initializers(
246  const address_mapt &amap,
247  const java_cfg_dominatorst &doms);
248 
250  local_variable_table_with_holest::iterator firstvar,
251  local_variable_table_with_holest::iterator varlimit,
252  const address_mapt &amap,
253  const java_cfg_dominatorst &doms);
254 
255  void setup_local_variables(const methodt &m, const address_mapt &amap);
256 
258  {
259  bool leaf;
260  std::vector<method_offsett> branch_addresses;
261  std::vector<block_tree_nodet> branch;
262 
264  {
265  }
266 
267  explicit block_tree_nodet(bool l) : leaf(l)
268  {
269  }
270 
272  {
273  return block_tree_nodet(true);
274  }
275  };
276 
277  static void replace_goto_target(
278  codet &repl,
279  const irep_idt &old_label,
280  const irep_idt &new_label);
281 
283  block_tree_nodet &tree,
284  code_blockt &this_block,
285  method_offsett address_start,
286  method_offsett address_limit,
287  method_offsett next_block_start_address);
288 
290  block_tree_nodet &tree,
291  code_blockt &this_block,
292  method_offsett address_start,
293  method_offsett address_limit,
294  method_offsett next_block_start_address,
295  const address_mapt &amap,
296  bool allow_merge = true);
297 
298  // conversion
299  void convert(
300  const symbolt &class_symbol,
301  const methodt &,
302  const optionalt<prefix_filtert> &method_context);
303 
305  const methodt &method,
306  const java_method_typet &method_type);
307 
309 
310  codet get_clinit_call(const irep_idt &classname);
311 
312  bool is_method_inherited(
313  const irep_idt &classname,
314  const irep_idt &mangled_method_name) const;
315 
317  const irep_idt &class_identifier, const irep_idt &component_name) const;
318 
320  {
321  VARIABLE,
322  ARRAY_REF,
323  STATIC_FIELD,
324  FIELD
325  };
326 
327  void save_stack_entries(
328  const std::string &,
329  code_blockt &,
330  const bytecode_write_typet,
331  const irep_idt &);
332 
334  const std::string &,
335  const typet &,
336  code_blockt &,
337  exprt &);
338 
339  std::vector<method_offsett> try_catch_handler(
340  method_offsett address,
342  const;
343 
345  address_mapt &address_map,
346  const std::vector<method_offsett> &jsr_ret_targets,
347  const std::vector<
348  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
349  &ret_instructions) const;
350 
352  const source_locationt &location,
353  std::size_t instruction_address,
354  const exprt &arg0,
355  codet &result_code);
356 
358  const irep_idt &statement,
359  const exprt::operandst &op,
360  const source_locationt &location);
361 
363  const irep_idt &statement,
364  const exprt &arg0,
365  const exprt::operandst &op,
366  const method_offsett address,
367  const source_locationt &location);
368 
369  static exprt
370  convert_aload(const irep_idt &statement, const exprt::operandst &op);
371 
381  exprt convert_load(const exprt &index, char type_char, size_t address);
382 
384  const std::vector<method_offsett> &jsr_ret_targets,
385  const exprt &arg0,
386  const source_locationt &location,
387  const method_offsett address);
388 
391  const u1 bytecode,
392  const exprt::operandst &op,
393  const mp_integer &number,
394  const source_locationt &location) const;
395 
398  const exprt::operandst &op,
399  const irep_idt &id,
400  const mp_integer &number,
401  const source_locationt &location) const;
402 
405  const exprt::operandst &op,
406  const mp_integer &number,
407  const source_locationt &location) const;
408 
411  const exprt::operandst &op,
412  const mp_integer &number,
413  const source_locationt &location) const;
414 
416  const exprt &arg0,
417  const exprt &arg1,
418  const source_locationt &location,
419  method_offsett address);
420 
422  const irep_idt &statement,
423  const exprt::operandst &op,
424  exprt::operandst &results) const;
425 
427  convert_cmp(const exprt::operandst &op, exprt::operandst &results) const;
428 
430  const irep_idt &statement,
431  const exprt::operandst &op,
432  exprt::operandst &results) const;
433 
434  void convert_getstatic(
435  const source_locationt &source_location,
436  const exprt &arg0,
437  const symbol_exprt &symbol_expr,
438  bool is_assertions_disabled_field,
439  codet &c,
440  exprt::operandst &results);
441 
443  convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op);
444 
446  const source_locationt &location,
447  const exprt &arg0,
448  const exprt::operandst &op,
449  const symbol_exprt &symbol_expr);
450 
451  void convert_new(
452  const source_locationt &location,
453  const exprt &arg0,
454  codet &c,
455  exprt::operandst &results);
456 
458  const source_locationt &location,
459  const irep_idt &statement,
460  const exprt &arg0,
461  const exprt::operandst &op,
462  exprt::operandst &results);
463 
465  const source_locationt &location,
466  const exprt &arg0,
467  const exprt::operandst &op,
468  exprt::operandst &results);
469 
471  const methodt &method,
472  const std::set<method_offsett> &working_set,
473  method_offsett cur_pc,
474  codet &c);
475 
476  void convert_athrow(
477  const source_locationt &location,
478  const exprt::operandst &op,
479  codet &c,
480  exprt::operandst &results) const;
481 
482  void convert_checkcast(
483  const exprt &arg0,
484  const exprt::operandst &op,
485  codet &c,
486  exprt::operandst &results) const;
487 
489  const irep_idt &statement,
490  const exprt::operandst &op,
491  const source_locationt &source_location);
492 
494 
495  void convert_invoke(
496  source_locationt location,
497  const irep_idt &statement,
498  class_method_descriptor_exprt &class_method_descriptor,
499  codet &c,
500  exprt::operandst &results);
501 
503  const irep_idt &statement,
504  const constant_exprt &arg0,
505  exprt::operandst &results) const;
506 
508 
510 
511  void convert_dup2(exprt::operandst &op, exprt::operandst &results);
512 
514  const exprt::operandst &op,
516  const source_locationt &location);
517 
518  codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
519 
521 };
522 #endif
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
java_bytecode_convert_methodt::instructionst
methodt::instructionst instructionst
Definition: java_bytecode_convert_method_class.h:62
java_bytecode_convert_methodt::convert_invoke
void convert_invoke(source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2196
java_bytecode_convert_methodt::convert_pop
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2001
java_bytecode_convert_methodt::is_parameter
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...
Definition: java_bytecode_convert_method_class.h:215
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_convert_methodt::converted_instructiont::stack
stackt stack
Definition: java_bytecode_convert_method_class.h:233
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_bytecode_convert_methodt::threading_support
const bool threading_support
Definition: java_bytecode_convert_method_class.h:82
java_bytecode_convert_methodt::holet
Definition: java_bytecode_convert_method_class.h:106
java_bytecode_convert_methodt::variable_cast_argumentt
variable_cast_argumentt
Definition: java_bytecode_convert_method_class.h:187
java_bytecode_convert_methodt::convert_load
exprt convert_load(const exprt &index, char type_char, size_t address)
Load reference from local variable.
Definition: java_bytecode_convert_method.cpp:2961
java_bytecode_convert_methodt::local_variable_with_holest::var
local_variablet var
Definition: java_bytecode_convert_method_class.h:113
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
java_bytecode_convert_methodt::current_method
irep_idt current_method
A copy of method_id :/.
Definition: java_bytecode_convert_method_class.h:91
java_bytecode_convert_methodt::method_id
irep_idt method_id
Fully qualified name of the method under translation.
Definition: java_bytecode_convert_method_class.h:88
java_bytecode_parse_treet::methodt::local_variablet
Definition: java_bytecode_parse_tree.h:128
java_bytecode_convert_methodt::setup_local_variables
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
Definition: java_local_variable_table.cpp:744
java_bytecode_convert_methodt::convert_if_cmp
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
Definition: java_bytecode_convert_method.cpp:2868
java_bytecode_convert_methodt::convert_dup2
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2090
java_bytecode_convert_methodt::java_bytecode_convert_methodt
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)
Definition: java_bytecode_convert_method_class.h:35
typet
The type of an expression, extends irept.
Definition: type.h:29
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:86
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:92
java_bytecode_convert_methodt::try_catch_handler
std::vector< method_offsett > try_catch_handler(method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
Definition: java_bytecode_convert_method.cpp:3125
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
java_bytecode_convert_methodt::needed_lazy_methods
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
Definition: java_bytecode_convert_method_class.h:83
fieldref_exprt
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Definition: java_bytecode_parse_tree.h:335
java_bytecode_convert_methodt::ns
namespacet ns
Definition: java_bytecode_convert_method_class.h:78
java_bytecode_convert_methodt::label
static irep_idt label(const irep_idt &address)
Definition: java_bytecode_convert_method.cpp:167
java_bytecode_convert_methodt::find_initializers
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.
Definition: java_local_variable_table.cpp:695
java_bytecode_convert_methodt::variablet::length
size_t length
Definition: java_bytecode_convert_method_class.h:126
java_bytecode_convert_methodt::variable
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...
Definition: java_bytecode_convert_method.cpp:205
java_bytecode_convert_methodt::class_hierarchy
const class_hierarchyt & class_hierarchy
Definition: java_bytecode_convert_method_class.h:172
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:57
java_bytecode_convert_methodt::convert_iinc
code_blockt convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)
Definition: java_bytecode_convert_method.cpp:2771
exprt
Base class for all expressions.
Definition: expr.h:53
java_bytecode_convert_methodt::local_variable_with_holest::holes
std::vector< holet > holes
Definition: java_bytecode_convert_method_class.h:115
java_bytecode_convert_methodt::convert_ifnonull
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
Definition: java_bytecode_convert_method.cpp:2822
java_bytecode_convert_methodt::variablet::variablet
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length)
Definition: java_bytecode_convert_method_class.h:130
java_bytecode_convert_methodt::block_tree_nodet::branch
std::vector< block_tree_nodet > branch
Definition: java_bytecode_convert_method_class.h:261
java_bytecode_convert_methodt::convert_multianewarray
code_blockt convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2507
java_bytecode_convert_methodt::NO_CAST
@ NO_CAST
Definition: java_bytecode_convert_method_class.h:189
java_bytecode_convert_methodt::converted_instructiont
Definition: java_bytecode_convert_method_class.h:221
java_bytecode_convert_methodt::INST_INDEX_CONST
@ INST_INDEX_CONST
Definition: java_bytecode_convert_method_class.h:177
java_bytecode_convert_methodt::convert_newarray
code_blockt convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2534
java_bytecode_convert_methodt::convert_ret
code_blockt convert_ret(const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
Definition: java_bytecode_convert_method.cpp:2892
java_bytecode_convert_methodt::local_variable_tablet
methodt::local_variable_tablet local_variable_tablet
Definition: java_bytecode_convert_method_class.h:63
java_bytecode_convert_methodt::holet::start_pc
method_offsett start_pc
Definition: java_bytecode_convert_method_class.h:107
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
java_bytecode_convert_methodt::variables
expanding_vectort< variablest > variables
Definition: java_bytecode_convert_method_class.h:167
java_bytecode_convert_methodt::convert_cmp2
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2704
java_bytecode_convert_methodt::methodt
java_bytecode_parse_treet::methodt methodt
Definition: java_bytecode_convert_method_class.h:60
java_bytecode_convert_methodt::convert_cmp
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2732
expanding_vectort< variablest >
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
java_bytecode_convert_methodt::variablet::variablet
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter)
Definition: java_bytecode_convert_method_class.h:138
java_bytecode_convert_methodt::convert_instructions
code_blockt convert_instructions(const methodt &)
Definition: java_bytecode_convert_method.cpp:1067
cfg_dominators.h
Compute dominators for CFG of goto_function.
java_bytecode_convert_methodt::block_tree_nodet::get_leaf
static block_tree_nodet get_leaf()
Definition: java_bytecode_convert_method_class.h:271
java_bytecode_convert_methodt::converted_instructiont::code
codet code
Definition: java_bytecode_convert_method_class.h:232
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
java_bytecode_convert_methodt::variablet::symbol_expr
symbol_exprt symbol_expr
Definition: java_bytecode_convert_method_class.h:124
java_bytecode_convert_methodt::converted_instructiont::successors
std::list< method_offsett > successors
Definition: java_bytecode_convert_method_class.h:230
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_bytecode_convert_methodt::convert_new
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2592
java_bytecode_convert_methodt::variablet::start_pc
size_t start_pc
Definition: java_bytecode_convert_method_class.h:125
java_bytecode_convert_methodt::convert_switch
code_switcht convert_switch(const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:2017
java_bytecode_convert_methodt::get_clinit_call
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...
Definition: java_bytecode_convert_method.cpp:996
java_bytecode_convert_methodt::convert_if
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
Definition: java_bytecode_convert_method.cpp:2844
java_bytecode_convert_methodt::method_return_type
typet method_return_type
Return type of the method under conversion.
Definition: java_bytecode_convert_method_class.h:95
java_bytecode_convert_methodt::max_array_length
const size_t max_array_length
Definition: java_bytecode_convert_method_class.h:79
java_bytecode_convert_methodt::tmp_vars
std::list< symbol_exprt > tmp_vars
Definition: java_bytecode_convert_method_class.h:195
java_bytecode_convert_methodt::get_static_field
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...
Definition: java_bytecode_convert_method.cpp:3278
java_bytecode_convert_methodt::get_or_create_block_for_pcrange
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...
Definition: java_bytecode_convert_method.cpp:778
java_bytecode_convert_methodt::method_offsett
uint16_t method_offsett
Definition: java_bytecode_convert_method_class.h:74
java_bytecode_convert_methodt::variablet::is_parameter
bool is_parameter
Definition: java_bytecode_convert_method_class.h:127
java_bytecode_convert_methodt::throw_assertion_error
const bool throw_assertion_error
Definition: java_bytecode_convert_method_class.h:80
address_mapt
java_bytecode_convert_methodt::address_mapt address_mapt
Definition: java_local_variable_table.cpp:136
java_bytecode_convert_methodt::local_variable_with_holest::is_parameter
bool is_parameter
Definition: java_bytecode_convert_method_class.h:114
java_bytecode_convert_methodt::assert_no_exceptions_thrown
const bool assert_no_exceptions_thrown
Definition: java_bytecode_convert_method_class.h:81
java_bytecode_convert_methodt::bytecode_write_typet::STATIC_FIELD
@ STATIC_FIELD
java_bytecode_parse_tree.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_bytecode_convert_methodt::converted_instructiont::converted_instructiont
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
Definition: java_bytecode_convert_method_class.h:222
java_bytecode_convert_methodt::local_variable_table_with_holest
std::vector< local_variable_with_holest > local_variable_table_with_holest
Definition: java_bytecode_convert_method_class.h:119
java_bytecode_convert_methodt::find_variable_for_slot
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
Definition: java_local_variable_table.cpp:858
ci_lazy_methods_needed.h
Context-insensitive lazy methods container.
std_types.h
Pre-defined types.
java_bytecode_convert_methodt::class_has_clinit_method
std::map< irep_idt, bool > class_has_clinit_method
Definition: java_bytecode_convert_method_class.h:170
java_bytecode_convert_methodt::block_tree_nodet::branch_addresses
std::vector< method_offsett > branch_addresses
Definition: java_bytecode_convert_method_class.h:260
java_bytecode_convert_methodt::slots_for_parameters
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
Definition: java_bytecode_convert_method_class.h:102
java_bytecode_convert_methodt::instruction_sizet
instruction_sizet
Definition: java_bytecode_convert_method_class.h:175
java_bytecode_convert_methodt::variablet::variablet
variablet(const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter, std::vector< holet > &&_holes)
Definition: java_bytecode_convert_method_class.h:150
java_bytecode_convert_methodt::java_cfg_dominatorst
cfg_dominators_templatet< method_with_amapt, method_offsett, false > java_cfg_dominatorst
Definition: java_bytecode_convert_method_class.h:241
java_bytecode_convert_methodt::convert_dup2_x1
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2103
java_bytecode_convert_methodt::method_has_this
bool method_has_this
Definition: java_bytecode_convert_method_class.h:169
java_bytecode_convert_methodt::convert_putstatic
code_blockt convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
Definition: java_bytecode_convert_method.cpp:2616
java_bytecode_convert_methodt::bytecode_write_typet::VARIABLE
@ VARIABLE
message_handlert
Definition: message.h:28
java_bytecode_convert_methodt::convert_ushr
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2752
java_bytecode_convert_methodt::convert_getstatic
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)
Definition: java_bytecode_convert_method.cpp:2658
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
java_bytecode_convert_methodt::bytecode_write_typet::ARRAY_REF
@ ARRAY_REF
expanding_vector.h
java_bytecode_convert_methodt::variablet::holes
std::vector< holet > holes
Definition: java_bytecode_convert_method_class.h:128
java_bytecode_convert_methodt::convert_checkcast
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2372
java_bytecode_convert_methodt::get_block_for_pcrange
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 ...
Definition: java_bytecode_convert_method.cpp:741
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_bytecode_convert_methodt::converted_instructiont::predecessors
std::set< method_offsett > predecessors
Definition: java_bytecode_convert_method_class.h:231
java_bytecode_convert_methodt::local_variablet
methodt::local_variablet local_variablet
Definition: java_bytecode_convert_method_class.h:64
java_bytecode_parse_treet::methodt::exception_tablet
std::vector< exceptiont > exception_tablet
Definition: java_bytecode_parse_tree.h:122
java_bytecode_convert_methodt::INST_INDEX
@ INST_INDEX
Definition: java_bytecode_convert_method_class.h:176
java_bytecode_convert_methodt
Definition: java_bytecode_convert_method_class.h:33
source_locationt
Definition: source_location.h:20
java_bytecode_convert_methodt::convert_putfield
code_blockt convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2647
java_bytecode_convert_methodt::convert_const
exprt::operandst & convert_const(const irep_idt &statement, const constant_exprt &arg0, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2137
java_bytecode_convert_methodt::CAST_AS_NEEDED
@ CAST_AS_NEEDED
Definition: java_bytecode_convert_method_class.h:188
java_bytecode_convert_methodt::string_preprocess
java_string_library_preprocesst & string_preprocess
Definition: java_bytecode_convert_method_class.h:97
java_bytecode_convert_methodt::do_exception_handling
codet & do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)
Definition: java_bytecode_convert_method.cpp:2426
java_bytecode_convert_methodt::converted_instructiont::source
instructionst::const_iterator source
Definition: java_bytecode_convert_method_class.h:229
java_bytecode_convert_methodt::create_stack_tmp_var
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
Definition: java_bytecode_convert_method.cpp:3379
java_bytecode_convert_methodt::block_tree_nodet::leaf
bool leaf
Definition: java_bytecode_convert_method_class.h:259
java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:137
java_bytecode_parse_treet::instructiont::argst
std::vector< exprt > argst
Definition: java_bytecode_parse_tree.h:61
java_bytecode_convert_methodt::find_initializers_for_slot
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...
Definition: java_local_variable_table.cpp:598
java_bytecode_convert_methodt::convert_ifnull
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
Definition: java_bytecode_convert_method.cpp:2800
u1
uint8_t u1
Definition: bytecode_info.h:55
java_bytecode_convert_methodt::pop
exprt::operandst pop(std::size_t n)
Definition: java_bytecode_convert_method.cpp:133
java_bytecode_convert_methodt::used_local_names
std::set< symbol_exprt > used_local_names
Definition: java_bytecode_convert_method_class.h:168
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
symbolt
Symbol table entry.
Definition: symbol.h:28
java_bytecode_convert_methodt::instructiont
java_bytecode_parse_treet::instructiont instructiont
Definition: java_bytecode_convert_method_class.h:61
java_bytecode_convert_methodt::address_mapt
std::map< method_offsett, converted_instructiont > address_mapt
Definition: java_bytecode_convert_method_class.h:238
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:36
java_bytecode_convert_methodt::any_superclass_has_clinit_method
std::map< irep_idt, bool > any_superclass_has_clinit_method
Definition: java_bytecode_convert_method_class.h:171
java_bytecode_convert_methodt::block_tree_nodet::block_tree_nodet
block_tree_nodet()
Definition: java_bytecode_convert_method_class.h:263
java_bytecode_convert_methodt::push
void push(const exprt::operandst &o)
Definition: java_bytecode_convert_method.cpp:158
java_bytecode_convert_methodt::stackt
std::vector< exprt > stackt
Definition: java_bytecode_convert_method_class.h:203
java_bytecode_convert_methodt::convert_monitorenterexit
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
Definition: java_bytecode_convert_method.cpp:2067
java_bytecode_convert_methodt::convert_parameter_annotations
code_blockt convert_parameter_annotations(const methodt &method, const java_method_typet &method_type)
Definition: java_bytecode_convert_method.cpp:1018
java_bytecode_convert_methodt::block_tree_nodet
Definition: java_bytecode_convert_method_class.h:258
java_bytecode_convert_methodt::java_bytecode_convert_method_unit_testt
friend class java_bytecode_convert_method_unit_testt
Definition: java_bytecode_convert_method_class.h:520
java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr
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
Definition: java_bytecode_convert_method.cpp:3108
java_bytecode_convert_methodt::tmp_variable
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
Definition: java_bytecode_convert_method.cpp:172
java_bytecode_convert_methodt::convert_astore
code_blockt convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:3007
java_bytecode_convert_methodt::variablest
std::vector< variablet > variablest
Definition: java_bytecode_convert_method_class.h:166
java_bytecode_convert_methodt::convert
void convert(const symbolt &class_symbol, const methodt &, const optionalt< prefix_filtert > &method_context)
Definition: java_bytecode_convert_method.cpp:546
java_bytecode_convert_methodt::operator()
void operator()(const symbolt &class_symbol, const methodt &method, const optionalt< prefix_filtert > &method_context)
Definition: java_bytecode_convert_method_class.h:66
java_bytecode_convert_methodt::local_variable_with_holest
Definition: java_bytecode_convert_method_class.h:112
java_bytecode_convert_methodt::convert_dup2_x2
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2116
java_bytecode_convert_methodt::pop_residue
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
Definition: java_bytecode_convert_method.cpp:151
java_bytecode_convert_methodt::convert_invoke_dynamic
optionalt< exprt > convert_invoke_dynamic(const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code)
Definition: java_bytecode_convert_method.cpp:3037
message.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
std_expr.h
API to expression classes.
java_bytecode_convert_methodt::variablet
Definition: java_bytecode_convert_method_class.h:122
java_bytecode_convert_methodt::bytecode_write_typet
bytecode_write_typet
Definition: java_bytecode_convert_method_class.h:320
java_bytecode_parse_treet::methodt::local_variablet::index
std::size_t index
Definition: java_bytecode_parse_tree.h:132
java_bytecode_convert_methodt::convert_athrow
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2388
java_method_typet
Definition: java_types.h:103
java_bytecode_convert_methodt::method_with_amapt
std::pair< const methodt &, const address_mapt & > method_with_amapt
Definition: java_bytecode_convert_method_class.h:239
java_bytecode_convert_methodt::converted_instructiont::done
bool done
Definition: java_bytecode_convert_method_class.h:234
java_bytecode_convert_methodt::replace_call_to_cprover_assume
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
Definition: java_bytecode_convert_method.cpp:2357
java_bytecode_convert_methodt::is_method_inherited
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...
Definition: java_bytecode_convert_method.cpp:3263
java_bytecode_convert_methodt::replace_goto_target
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'.
Definition: java_bytecode_convert_method.cpp:707
java_bytecode_convert_methodt::stack
stackt stack
Definition: java_bytecode_convert_method_class.h:204
java_bytecode_convert_methodt::bytecode_write_typet::FIELD
@ FIELD
java_bytecode_convert_methodt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_convert_method_class.h:77
java_bytecode_convert_class.h
JAVA Bytecode Language Conversion.
java_bytecode_convert_methodt::convert_aload
static exprt convert_aload(const irep_idt &statement, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2941
java_bytecode_convert_methodt::holet::length
method_offsett length
Definition: java_bytecode_convert_method_class.h:108
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:38
java_bytecode_convert_methodt::block_tree_nodet::block_tree_nodet
block_tree_nodet(bool l)
Definition: java_bytecode_convert_method_class.h:267
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
java_bytecode_convert_methodt::convert_store
code_blockt convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:2982
java_bytecode_convert_methodt::save_stack_entries
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.
Definition: java_bytecode_convert_method.cpp:3297