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 <util/expanding_vector.h>
16 #include <util/message.h>
17 #include <util/std_types.h>
18 #include <util/std_expr.h>
19 #include <util/safe_pointer.h>
23 #include "ci_lazy_methods.h"
24 
25 #include <vector>
26 #include <list>
27 
28 class symbol_tablet;
29 class symbolt;
30 
32 {
33 public:
35  symbol_tablet &_symbol_table,
36  message_handlert &_message_handler,
37  size_t _max_array_length,
38  safe_pointer<ci_lazy_methodst> _lazy_methods,
39  const character_refine_preprocesst &_character_preprocess):
40  messaget(_message_handler),
41  symbol_table(_symbol_table),
42  max_array_length(_max_array_length),
43  lazy_methods(_lazy_methods),
44  character_preprocess(_character_preprocess)
45  {
46  }
47 
53 
54  void operator()(const symbolt &class_symbol, const methodt &method)
55  {
56  convert(class_symbol, method);
57  }
58 
59 protected:
61  const size_t max_array_length;
63 
68 
69 public:
70  struct holet
71  {
72  unsigned start_pc;
73  unsigned length;
74  };
75 
77  {
79  std::vector<holet> holes;
80  };
81 
82  typedef std::vector<local_variable_with_holest>
84 
85  class variablet
86  {
87  public:
89  size_t start_pc;
90  size_t length;
92  std::vector<holet> holes;
94  };
95 
96  protected:
97  typedef std::vector<variablet> variablest;
99  std::set<symbol_exprt> used_local_names;
101 
103  {
106  };
107 
109  const exprt &arraystruct,
110  const exprt &idx,
111  const source_locationt &original_sloc);
112 
113  // return corresponding reference of variable
114  const variablet &find_variable_for_slot(
115  size_t address,
116  variablest &var_list);
117 
118  // JVM local variables
120  {
123  };
124 
125  const exprt variable(
126  const exprt &arg,
127  char type_char,
128  size_t address,
129  variable_cast_argumentt do_cast);
130 
131  // temporary variables
132  std::list<symbol_exprt> tmp_vars;
133 
134  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
135 
136  // JVM program locations
137  irep_idt label(const irep_idt &address);
138 
139  // JVM Stack
140  typedef std::vector<exprt> stackt;
142 
143  exprt::operandst pop(std::size_t n);
144 
145  void pop_residue(std::size_t n);
146  void push(const exprt::operandst &o);
147 
148  bool is_constructor(const class_typet::methodt &method);
149 
151  {
153  const instructionst::const_iterator &it,
154  const codet &_code):source(it), code(_code), done(false)
155  {}
156 
157  instructionst::const_iterator source;
158  std::list<unsigned> successors;
159  std::set<unsigned> predecessors;
162  bool done;
163  };
164 
165 public:
166  typedef std::map<unsigned, converted_instructiont> address_mapt;
167  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
170 
171 protected:
172  void find_initialisers(
174  const address_mapt &amap,
175  const java_cfg_dominatorst &doms);
176 
178  local_variable_table_with_holest::iterator firstvar,
179  local_variable_table_with_holest::iterator varlimit,
180  const address_mapt &amap,
181  const java_cfg_dominatorst &doms);
182 
183  void setup_local_variables(const methodt &m, const address_mapt &amap);
184 
186  {
187  bool leaf;
188  std::vector<unsigned> branch_addresses;
189  std::vector<block_tree_nodet> branch;
190  block_tree_nodet():leaf(false) {}
191  explicit block_tree_nodet(bool l):leaf(l) {}
192  static block_tree_nodet get_leaf() { return block_tree_nodet(true); }
193  };
194 
195  static void replace_goto_target(
196  codet &repl,
197  const irep_idt &old_label,
198  const irep_idt &new_label);
199 
201  block_tree_nodet &tree,
202  code_blockt &this_block,
203  unsigned address_start,
204  unsigned address_limit,
205  unsigned next_block_start_address);
206 
208  block_tree_nodet &tree,
209  code_blockt &this_block,
210  unsigned address_start,
211  unsigned address_limit,
212  unsigned next_block_start_address,
213  const address_mapt &amap,
214  bool allow_merge=true);
215 
216  // conversion
217  void convert(const symbolt &class_symbol, const methodt &);
218 
220  const methodt &,
221  const code_typet &);
222 
223  const bytecode_infot &get_bytecode_info(const irep_idt &statement);
224 
226  void save_stack_entries(
227  const std::string &,
228  const typet &,
229  code_blockt &,
230  const bytecode_write_typet,
231  const irep_idt &);
233  const std::string &,
234  const typet &,
235  code_blockt &,
236  exprt &);
237 };
238 
239 #endif
void find_initialisers_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...
The type of an expression.
Definition: type.h:20
java_bytecode_convert_methodt::address_mapt address_mapt
methodt::local_variable_tablet local_variable_tablet
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
Base type of functions.
Definition: std_types.h:734
void convert(const symbolt &class_symbol, const methodt &)
std::pair< const methodt &, const address_mapt & > method_with_amapt
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
void operator()(const symbolt &class_symbol, const methodt &method)
safe_pointer< ci_lazy_methodst > 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...
irep_idt label(const irep_idt &address)
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initialisers_for_slot above for more detail.
character_refine_preprocesst character_preprocess
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
std::map< unsigned, converted_instructiont > address_mapt
expanding_vectort< variablest > variables
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 ...
std::vector< local_variable_with_holest > local_variable_table_with_holest
bool is_constructor(const class_typet::methodt &method)
java_bytecode_convert_methodt(symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, safe_pointer< ci_lazy_methodst > _lazy_methods, const character_refine_preprocesst &_character_preprocess)
java_bytecode_parse_treet::methodt methodt
JAVA Bytecode Language Conversion.
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
Context-insensitive lazy methods container.
std::vector< instructiont > instructionst
Simple checked pointers.
java_bytecode_parse_treet::instructiont instructiont
void find_initialisers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
See find_initialisers_for_slot above for more detail.
exprt::operandst pop(std::size_t n)
std::vector< exprt > operandst
Definition: expr.h:49
codet convert_instructions(const methodt &, const code_typet &)
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
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
Base class for all expressions.
Definition: expr.h:46
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 ...
void push(const exprt::operandst &o)
Sequential composition.
Definition: std_code.h:63
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
Compute dominators for CFG of goto_function.
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;.
cfg_dominators_templatet< method_with_amapt, unsigned, false > java_cfg_dominatorst
codet get_array_bounds_check(const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc)