|
cprover
|
Java local variable table processing. More...
#include "java_bytecode_convert_method_class.h"#include <util/arith_tools.h>#include <util/invariant.h>#include <util/string2int.h>#include <util/symbol_table_base.h>#include "java_types.h"#include <iostream>Go to the source code of this file.
Classes | |
| struct | procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett > |
| 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. | |
| static bool | is_store_to_slot (const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx) |
| See above. | |
| static void | maybe_add_hole (local_variable_with_holest &var, java_bytecode_convert_methodt::method_offsett from, java_bytecode_convert_methodt::method_offsett to) |
| See above. | |
| 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. | |
| 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). | |
| static java_bytecode_convert_methodt::method_offsett | 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. | |
| static void | populate_live_range_holes (local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, java_bytecode_convert_methodt::method_offsett expanded_live_range_start) |
| See above. | |
| 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. | |
| 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. | |
| static void | cleanup_var_table (std::vector< local_variable_with_holest > &vars_with_holes) |
| See above. | |
Java local variable table processing.
Definition in file java_local_variable_table.cpp.
Definition at line 135 of file java_local_variable_table.cpp.
Definition at line 129 of file java_local_variable_table.cpp.
Definition at line 137 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 133 of file java_local_variable_table.cpp.
Definition at line 131 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 159 of file java_local_variable_table.cpp.
|
static |
See above.
Removes zero-size entries from vars_with_holes.
| vars_with_holes | variable table |
Definition at line 712 of file java_local_variable_table.cpp.
|
static |
See above.
| start | Variable to find the predecessors of | |
| predecessor_map | Map from local variables to sets of predecessors | |
| [out] | result | populated with all transitive predecessors of start found in predecessor_map |
Definition at line 185 of file java_local_variable_table.cpp.
|
static |
Used to find out where to put a variable declaration that subsumes several variable live ranges.
| merge_vars | Set of variables we want the common dominator for |
| dominator_analysis | Already-initialized dominator tree |
Definition at line 448 of file java_local_variable_table.cpp.
|
static |
See above.
| inst | Java bytecode instruction |
| slotidx | local variable slot number |
Definition at line 204 of file java_local_variable_table.cpp.
|
static |
Definition at line 141 of file java_local_variable_table.cpp.
|
static |
Definition at line 147 of file java_local_variable_table.cpp.
|
static |
See above.
| from | bound of a gap in var's live range (inclusive) | |
| to | bound of a gap in var's live range (exclusive) | |
| [out] | var | A hole is added to var, unless it would be of zero size |
Definition at line 239 of file java_local_variable_table.cpp.
|
static |
See above.
| merge_vars | a set of 2+ variable table entries to merge | |
| dominator_analysis | already-calculated dominator tree | |
| [out] | merge_into | Populated 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. |
| debug_out | stream for debug output |
Definition at line 539 of file java_local_variable_table.cpp.
|
static |
See above.
| merge_vars | a set of 2+ variable table entries to merge | |
| expanded_live_range_start | address where the merged variable will be declared | |
| [out] | merge_into | Holes are added to 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 507 of file java_local_variable_table.cpp.
|
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) live at that address | |
| 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 |
| msg_handler | for reporting warnings |
Definition at line 303 of file java_local_variable_table.cpp.
|
static |
See above.
| firstvar | start of range of local variable table entries to consider | |
| varlimit | end of range of local variable table entries to consider | |
| [out] | live_variable_at_address | 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 258 of file java_local_variable_table.cpp.
|
static |
Walk a vector, a contiguous block of entries with equal slot index at a time.
it1 and it2 are iterators into the same vector, of which itend is the end() iterator. it1 and it2 are moved 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 667 of file java_local_variable_table.cpp.