cprover
|
Java local variable table processing. More...
#include "java_bytecode_convert_method_class.h"
#include "java_types.h"
#include <util/arith_tools.h>
#include <util/invariant.h>
#include <util/string2int.h>
#include <climits>
#include <iostream>
Go to the source code of this file.
Classes | |
struct | procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned > |
struct | is_predecessor_oft |
Functions | |
static bool | lt_index (const local_variable_with_holest &a, const local_variable_with_holest &b) |
static bool | lt_startpc (const local_variable_with_holest *a, const local_variable_with_holest *b) |
static void | gather_transitive_predecessors (local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest *> &result) |
See above start : Variable to find the predecessors of predecessor_map : Map from local variables to sets of predecessors. More... | |
static bool | is_store_to_slot (const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx) |
See above. More... | |
static void | maybe_add_hole (local_variable_with_holest &var, unsigned from, unsigned to) |
See above. More... | |
static void | populate_variable_address_map (local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, std::vector< local_variable_with_holest *> &live_variable_at_address) |
See above. More... | |
static void | populate_predecessor_map (local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const std::vector< local_variable_with_holest *> &live_variable_at_address, const address_mapt &amap, predecessor_mapt &predecessor_map, message_handlert &msg_handler) |
Usually a live variable range begins with a store instruction initialising the relevant local variable slot, but instead of or in addition to this, control flow edges may exist from bytecode addresses that fall under a table entry which differs, but which has the same variable name and type descriptor. More... | |
static unsigned | get_common_dominator (const std::set< local_variable_with_holest *> &merge_vars, const java_cfg_dominatorst &dominator_analysis) |
Used to find out where to put a variable declaration that subsumes several variable live ranges. More... | |
static void | populate_live_range_holes (local_variable_with_holest &merge_into, const std::set< local_variable_with_holest *> &merge_vars, unsigned expanded_live_range_start) |
See above. More... | |
static void | merge_variable_table_entries (local_variable_with_holest &merge_into, const std::set< local_variable_with_holest *> &merge_vars, const java_cfg_dominatorst &dominator_analysis, std::ostream &debug_out) |
See above. More... | |
static void | walk_to_next_index (local_variable_table_with_holest::iterator &it1, local_variable_table_with_holest::iterator &it2, local_variable_table_with_holest::iterator itend) |
Walk a vector, a contiguous block of entries with equal slot index at a time. More... | |
static void | cleanup_var_table (std::vector< local_variable_with_holest > &vars_with_holes) |
See above. More... | |
Java local variable table processing.
Definition in file java_local_variable_table.cpp.
Definition at line 105 of file java_local_variable_table.cpp.
Definition at line 99 of file java_local_variable_table.cpp.
Definition at line 107 of file java_local_variable_table.cpp.
typedef java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest |
Definition at line 103 of file java_local_variable_table.cpp.
Definition at line 101 of file java_local_variable_table.cpp.
typedef std::map< local_variable_with_holest *, std::set<local_variable_with_holest *> > predecessor_mapt |
Definition at line 129 of file java_local_variable_table.cpp.
|
static |
See above.
vars_with_holes
Definition at line 621 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::setup_local_variables().
|
static |
See above start
: Variable to find the predecessors of predecessor_map
: Map from local variables to sets of predecessors.
Outputs | result : populated with all transitive predecessors of start found in predecessor_map |
Definition at line 155 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::find_initialisers_for_slot().
|
static |
Used to find out where to put a variable declaration that subsumes several variable live ranges.
dominator_analysis
: Already-initialised dominator tree Definition at line 363 of file java_local_variable_table.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, and cfg_baset< T, P, I >::entry_map.
Referenced by merge_variable_table_entries().
|
static |
See above.
slotidx
: local variable slot number inst
is any form of store instruction targeting slot slotidx
Definition at line 174 of file java_local_variable_table.cpp.
References java_bytecode_parse_treet::instructiont::args, CHECK_RETURN, id2string(), safe_string2unsigned(), java_bytecode_parse_treet::instructiont::statement, to_constant_expr(), and to_unsigned_integer().
Referenced by populate_predecessor_map().
|
static |
Definition at line 111 of file java_local_variable_table.cpp.
References java_bytecode_parse_treet::methodt::local_variablet::index, and java_bytecode_convert_methodt::local_variable_with_holest::var.
Referenced by java_bytecode_convert_methodt::find_initialisers().
|
static |
Definition at line 117 of file java_local_variable_table.cpp.
References java_bytecode_parse_treet::methodt::local_variablet::start_pc, and java_bytecode_convert_methodt::local_variable_with_holest::var.
Referenced by populate_live_range_holes().
|
static |
See above.
var
, unless it would be of zero size. Definition at line 205 of file java_local_variable_table.cpp.
References java_bytecode_convert_methodt::local_variable_with_holest::holes.
Referenced by populate_live_range_holes().
|
static |
See above.
dominator_analysis
: already-calculated dominator tree merge_into
as a combined variable table entry, with live range holes if the merge_vars
entries do not cover a contiguous address range, beginning the combined live range at the common dominator of all merge_vars
. Definition at line 449 of file java_local_variable_table.cpp.
References get_common_dominator(), java_bytecode_parse_treet::methodt::local_variablet::length, java_bytecode_parse_treet::methodt::local_variablet::name, populate_live_range_holes(), java_bytecode_parse_treet::methodt::local_variablet::start_pc, and java_bytecode_convert_methodt::local_variable_with_holest::var.
Referenced by java_bytecode_convert_methodt::find_initialisers_for_slot().
|
static |
See above.
expanded_live_range_start
: address where the merged variable will be declared merge_into
, indicating where gaps in the variable's live range fall. For example, if the declaration happens at address 10 and the entries in merge_into
have live ranges [(20-30), (40-50)] then holes will be added at (10-20) and (30-40). Definition at line 420 of file java_local_variable_table.cpp.
References java_bytecode_parse_treet::methodt::local_variablet::length, lt_startpc(), maybe_add_hole(), and java_bytecode_convert_methodt::local_variable_with_holest::var.
Referenced by merge_variable_table_entries().
|
static |
Usually a live variable range begins with a store instruction initialising the relevant local variable slot, but instead of or in addition to this, control flow edges may exist from bytecode addresses that fall under a table entry which differs, but which has the same variable name and type descriptor.
This indicates a split live range, and will be recorded in the predecessor map.
live_variable_at_address
: map from bytecode address to table entry (drawn from firstvar-varlimit) live at that address amap
: map from bytecode address to instructions predecessor_map
with a graph from local variable table entries to their predecessors (table entries which may flow together and thus may be considered the same live range). Definition at line 257 of file java_local_variable_table.cpp.
References messaget::eom(), is_store_to_slot(), and messaget::warning().
Referenced by java_bytecode_convert_methodt::find_initialisers_for_slot().
|
static |
See above.
live_variable_at_address
is populated with a sequence of local variable table entry pointers, such that live_variable_at_address[addr]
yields the unique table entry covering that address. Asserts if entries overlap. Definition at line 222 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::find_initialisers_for_slot().
|
static |
Walk a vector, a contiguous block of entries with equal slot index at a time.
itend
is the end() iterator. it1
and it2
to delimit a sequence of variable table entries with slot index equal to it2->var.index on entering this function, or to both equal itend if it2==itend on entry. Definition at line 576 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::find_initialisers().