cprover
Loading...
Searching...
No Matches
java_bytecode_convert_method_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Language Conversion
4
5Author: 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
18
20#include <util/message.h>
21#include <util/std_code.h>
22#include <util/std_expr.h>
23
25
26#include <vector>
27#include <list>
28
30class prefix_filtert;
31class symbol_tablet;
32class symbolt;
33
35{
36public:
39 message_handlert &_message_handler,
40 size_t _max_array_length,
43 java_string_library_preprocesst &_string_preprocess,
47 : log(_message_handler),
50 max_array_length(_max_array_length),
55 string_preprocess(_string_preprocess),
57 method_has_this(false),
59 {
60 }
61
67
69 const symbolt &class_symbol,
70 const methodt &method,
71 const optionalt<prefix_filtert> &method_context)
72 {
73 convert(class_symbol, method, method_context);
74 }
75
76 typedef uint16_t method_offsett;
77
78protected:
82 const size_t max_array_length;
87
92
95
99
101
106
107public:
108 struct holet
109 {
112 };
113
115 {
118 std::vector<holet> holes;
119 };
120
121 typedef std::vector<local_variable_with_holest>
123
125 {
126 public:
128 size_t start_pc;
129 size_t length;
130 bool is_parameter = false;
131 std::vector<holet> holes;
132
134 const symbol_exprt &_symbol_expr,
135 std::size_t _start_pc,
136 std::size_t _length)
137 : symbol_expr(_symbol_expr), start_pc(_start_pc), length(_length)
138 {
139 }
140
142 const symbol_exprt &_symbol_expr,
143 std::size_t _start_pc,
144 std::size_t _length,
145 bool _is_parameter)
146 : symbol_expr(_symbol_expr),
147 start_pc(_start_pc),
148 length(_length),
149 is_parameter(_is_parameter)
150 {
151 }
152
154 const symbol_exprt &_symbol_expr,
155 std::size_t _start_pc,
156 std::size_t _length,
157 bool _is_parameter,
158 std::vector<holet> &&_holes)
159 : symbol_expr(_symbol_expr),
160 start_pc(_start_pc),
161 length(_length),
162 is_parameter(_is_parameter),
163 holes(std::move(_holes))
164 {
165 }
166 };
167
168protected:
169 typedef std::vector<variablet> variablest;
171 std::set<symbol_exprt> used_local_names;
173 std::map<irep_idt, bool> class_has_clinit_method;
174 std::map<irep_idt, bool> any_superclass_has_clinit_method;
176
178 {
181 };
182
183 // return corresponding reference of variable
184 const variablet &find_variable_for_slot(
185 size_t address,
186 variablest &var_list);
187
188 // JVM local variables
190 {
192 NO_CAST
193 };
194
195 exprt variable(const exprt &arg, char type_char, size_t address);
196
197 // temporary variables
198 std::list<symbol_exprt> tmp_vars;
199
200 symbol_exprt tmp_variable(const std::string &prefix, const typet &type);
201
202 // JVM program locations
203 static irep_idt label(const irep_idt &address);
204
205 // JVM Stack
206 typedef std::vector<exprt> stackt;
208
209 exprt::operandst pop(std::size_t n);
210
211 void pop_residue(std::size_t n);
212
213 void push(const exprt::operandst &o);
214
219 {
220 return v.index < slots_for_parameters;
221 }
222
224 {
226 const instructionst::const_iterator &it,
227 const codet &_code)
228 : source(it), code(_code), done(false)
229 {
230 }
231
232 instructionst::const_iterator source;
233 std::list<method_offsett> successors;
234 std::set<method_offsett> predecessors;
237 bool done;
238 };
239
240public:
241 typedef std::map<method_offsett, converted_instructiont> address_mapt;
242 typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
245
246protected:
249 const address_mapt &amap,
250 const java_cfg_dominatorst &doms);
251
253 local_variable_table_with_holest::iterator firstvar,
254 local_variable_table_with_holest::iterator varlimit,
255 const address_mapt &amap,
256 const java_cfg_dominatorst &doms);
257
258 void setup_local_variables(const methodt &m, const address_mapt &amap);
259
261 {
262 bool leaf;
263 std::vector<method_offsett> branch_addresses;
264 std::vector<block_tree_nodet> branch;
265
267 {
268 }
269
270 explicit block_tree_nodet(bool l) : leaf(l)
271 {
272 }
273
275 {
276 return block_tree_nodet(true);
277 }
278 };
279
280 static void replace_goto_target(
281 codet &repl,
282 const irep_idt &old_label,
283 const irep_idt &new_label);
284
286 block_tree_nodet &tree,
287 code_blockt &this_block,
288 method_offsett address_start,
289 method_offsett address_limit,
290 method_offsett next_block_start_address);
291
293 block_tree_nodet &tree,
294 code_blockt &this_block,
295 method_offsett address_start,
296 method_offsett address_limit,
297 method_offsett next_block_start_address,
298 const address_mapt &amap,
299 bool allow_merge = true);
300
301 // conversion
302 void convert(
303 const symbolt &class_symbol,
304 const methodt &,
305 const optionalt<prefix_filtert> &method_context);
306
308 const methodt &method,
309 const java_method_typet &method_type);
310
312
313 codet get_clinit_call(const irep_idt &classname);
314
316 const irep_idt &classname,
317 const irep_idt &mangled_method_name) const;
318
320 const irep_idt &class_identifier, const irep_idt &component_name) const;
321
323 {
324 VARIABLE,
325 ARRAY_REF,
327 FIELD
328 };
329
331 const std::string &,
332 code_blockt &,
334 const irep_idt &);
335
337 const std::string &,
338 const typet &,
339 code_blockt &,
340 exprt &);
341
342 std::vector<method_offsett> try_catch_handler(
343 method_offsett address,
345 const;
346
348 address_mapt &address_map,
349 const std::vector<method_offsett> &jsr_ret_targets,
350 const std::vector<
351 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
352 &ret_instructions) const;
353
355 const source_locationt &location,
356 std::size_t instruction_address,
357 const exprt &arg0,
358 codet &result_code);
359
361 const irep_idt &statement,
362 const exprt::operandst &op,
363 const source_locationt &location);
364
366 const irep_idt &statement,
367 const exprt &arg0,
368 const exprt::operandst &op,
369 const method_offsett address,
370 const source_locationt &location);
371
372 static exprt
373 convert_aload(const irep_idt &statement, const exprt::operandst &op);
374
384 exprt convert_load(const exprt &index, char type_char, size_t address);
385
387 const std::vector<method_offsett> &jsr_ret_targets,
388 const exprt &arg0,
389 const source_locationt &location,
390 const method_offsett address);
391
394 const u1 bytecode,
395 const exprt::operandst &op,
396 const mp_integer &number,
397 const source_locationt &location) const;
398
401 const exprt::operandst &op,
402 const irep_idt &id,
403 const mp_integer &number,
404 const source_locationt &location) const;
405
408 const exprt::operandst &op,
409 const mp_integer &number,
410 const source_locationt &location) const;
411
414 const exprt::operandst &op,
415 const mp_integer &number,
416 const source_locationt &location) const;
417
419 const exprt &arg0,
420 const exprt &arg1,
421 const source_locationt &location,
422 method_offsett address);
423
425 const irep_idt &statement,
426 const exprt::operandst &op,
427 exprt::operandst &results) const;
428
430 const irep_idt &statement,
431 const exprt::operandst &op,
432 exprt::operandst &results) const;
433
435 convert_cmp(const exprt::operandst &op, exprt::operandst &results) const;
436
438 const irep_idt &statement,
439 const exprt::operandst &op,
440 exprt::operandst &results) const;
441
443 const source_locationt &source_location,
444 const exprt &arg0,
445 const symbol_exprt &symbol_expr,
446 bool is_assertions_disabled_field,
447 codet &c,
448 exprt::operandst &results);
449
451 convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op);
452
454 const source_locationt &location,
455 const exprt &arg0,
456 const exprt::operandst &op,
457 const symbol_exprt &symbol_expr);
458
459 void convert_new(
460 const source_locationt &location,
461 const exprt &arg0,
462 codet &c,
463 exprt::operandst &results);
464
466 const source_locationt &location,
467 const irep_idt &statement,
468 const exprt &arg0,
469 const exprt::operandst &op,
470 exprt::operandst &results);
471
473 const source_locationt &location,
474 const exprt &arg0,
475 const exprt::operandst &op,
476 exprt::operandst &results);
477
479 const methodt &method,
480 const std::set<method_offsett> &working_set,
481 method_offsett cur_pc,
482 codet &c);
483
484 void convert_athrow(
485 const source_locationt &location,
486 const exprt::operandst &op,
487 codet &c,
488 exprt::operandst &results) const;
489
491 const exprt &arg0,
492 const exprt::operandst &op,
493 codet &c,
494 exprt::operandst &results) const;
495
497 const irep_idt &statement,
498 const exprt::operandst &op,
499 const source_locationt &source_location);
500
502
503 void convert_invoke(
504 source_locationt location,
505 const irep_idt &statement,
506 class_method_descriptor_exprt &class_method_descriptor,
507 codet &c,
508 exprt::operandst &results);
509
511 const irep_idt &statement,
512 const constant_exprt &arg0,
513 exprt::operandst &results) const;
514
516
518
520
522 const exprt::operandst &op,
524 const source_locationt &location);
525
526 codet convert_pop(const irep_idt &statement, const exprt::operandst &op);
527
529};
530#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:3272
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of an if-then-else statement.
Definition: std_code.h:460
codet representing a switch statement.
Definition: std_code.h:548
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
A constant literal expression.
Definition: std_expr.h:2807
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:91
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
Definition: prefix_filter.h:20
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
JAVA Bytecode Language Conversion.
java_bytecode_convert_methodt::address_mapt address_mapt
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12
API to expression classes.
converted_instructiont(const instructionst::const_iterator &it, const codet &_code)
std::vector< local_variablet > local_variable_tablet
std::vector< instructiont > instructionst