cprover
|
Java local variable table processing. More...
#include "java_bytecode_convert_method_class.h"
#include "java_types.h"
#include "java_utils.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) |
Populates the 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). 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 109 of file java_local_variable_table.cpp.
Definition at line 103 of file java_local_variable_table.cpp.
Definition at line 111 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 107 of file java_local_variable_table.cpp.
Definition at line 105 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 133 of file java_local_variable_table.cpp.
|
static |
See above.
vars_with_holes
Definition at line 678 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 159 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::find_initializers_for_slot().
|
static |
Used to find out where to put a variable declaration that subsumes several variable live ranges.
dominator_analysis
: Already-initialized dominator tree Definition at line 420 of file java_local_variable_table.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, cfg_baset< T, P, I >::entry_map, and PRECONDITION.
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 178 of file java_local_variable_table.cpp.
References java_bytecode_parse_treet::instructiont::args, CHECK_RETURN, id2string(), INVARIANT, safe_string2unsigned(), java_bytecode_parse_treet::instructiont::statement, to_constant_expr(), and to_unsigned_integer().
Referenced by populate_predecessor_map().
|
static |
Definition at line 115 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_initializers().
|
static |
Definition at line 121 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 213 of file java_local_variable_table.cpp.
References java_bytecode_convert_methodt::local_variable_with_holest::holes, and PRECONDITION.
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 506 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_initializers_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 477 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 |
Populates the 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).
Usually a live variable range begins with a store instruction initializing 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 (or which fall under no table entry at all), but which has the same variable name and type descriptor. This indicates a split live range, and will be recorded in the predecessor map.
firstvar | range of local variable table entries to consider | |
varlimit | range of local variable table entries to consider | |
live_variable_at_address | map from bytecode address to table entry (drawn from firstvar-varlimit) | |
amap | map from bytecode address to instructions, this is the CFG of the java method | |
[out] | predecessor_map | the output of the function, populated as described above |
Definition at line 274 of file java_local_variable_table.cpp.
References messaget::debug(), messaget::eom(), INVARIANT, is_store_to_slot(), and messaget::warning().
Referenced by java_bytecode_convert_methodt::find_initializers_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 230 of file java_local_variable_table.cpp.
References INVARIANT.
Referenced by java_bytecode_convert_methodt::find_initializers_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 633 of file java_local_variable_table.cpp.
Referenced by java_bytecode_convert_methodt::find_initializers().