CBMC
java_local_variable_table.cpp File Reference

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>
+ Include dependency graph for java_local_variable_table.cpp:

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
 

Typedefs

typedef java_bytecode_convert_methodt::holet holet
 
typedef java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest
 
typedef java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
 
typedef java_bytecode_convert_methodt::address_mapt address_mapt
 
typedef java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
 
typedef std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
 

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. 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, java_bytecode_convert_methodt::method_offsett from, java_bytecode_convert_methodt::method_offsett 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 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. More...
 
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. 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...
 

Detailed Description

Java local variable table processing.

Definition in file java_local_variable_table.cpp.

Typedef Documentation

◆ address_mapt

◆ holet

◆ java_cfg_dominatorst

◆ local_variable_table_with_holest

◆ local_variable_with_holest

◆ predecessor_mapt

Definition at line 159 of file java_local_variable_table.cpp.

Function Documentation

◆ cleanup_var_table()

static void cleanup_var_table ( std::vector< local_variable_with_holest > &  vars_with_holes)
static

See above.

Removes zero-size entries from vars_with_holes.

Parameters
vars_with_holesvariable table

Definition at line 712 of file java_local_variable_table.cpp.

◆ gather_transitive_predecessors()

static void gather_transitive_predecessors ( local_variable_with_holest start,
const predecessor_mapt predecessor_map,
std::set< local_variable_with_holest * > &  result 
)
static

See above.

Parameters
startVariable to find the predecessors of
predecessor_mapMap from local variables to sets of predecessors
[out]resultpopulated with all transitive predecessors of start found in predecessor_map

Definition at line 185 of file java_local_variable_table.cpp.

◆ get_common_dominator()

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 
)
static

Used to find out where to put a variable declaration that subsumes several variable live ranges.

Parameters
merge_varsSet of variables we want the common dominator for
dominator_analysisAlready-initialized dominator tree
Returns
Returns the bytecode address of the closest common dominator of all given variable table entries. In the worst case the function entry point should always satisfy this criterion.

Definition at line 448 of file java_local_variable_table.cpp.

◆ is_store_to_slot()

static bool is_store_to_slot ( const java_bytecode_convert_methodt::instructiont inst,
unsigned  slotidx 
)
static

See above.

Parameters
instJava bytecode instruction
slotidxlocal variable slot number
Returns
Returns true if inst is any form of store instruction targeting slot slotidx

Definition at line 204 of file java_local_variable_table.cpp.

◆ lt_index()

static bool lt_index ( const local_variable_with_holest a,
const local_variable_with_holest b 
)
static

Definition at line 141 of file java_local_variable_table.cpp.

◆ lt_startpc()

static bool lt_startpc ( const local_variable_with_holest a,
const local_variable_with_holest b 
)
static

Definition at line 147 of file java_local_variable_table.cpp.

◆ maybe_add_hole()

See above.

Parameters
frombound of a gap in var's live range (inclusive)
tobound of a gap in var's live range (exclusive)
[out]varA hole is added to var, unless it would be of zero size

Definition at line 239 of file java_local_variable_table.cpp.

◆ merge_variable_table_entries()

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 
)
static

See above.

Parameters
merge_varsa set of 2+ variable table entries to merge
dominator_analysisalready-calculated dominator tree
[out]merge_intoPopulated 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_outstream for debug output

Definition at line 539 of file java_local_variable_table.cpp.

◆ populate_live_range_holes()

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 
)
static

See above.

Parameters
merge_varsa set of 2+ variable table entries to merge
expanded_live_range_startaddress where the merged variable will be declared
[out]merge_intoHoles 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.

◆ populate_predecessor_map()

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 
)
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.

Parameters
firstvarrange of local variable table entries to consider
varlimitrange of local variable table entries to consider
live_variable_at_addressmap from bytecode address to table entry (drawn from firstvar-varlimit) live at that address
amapmap from bytecode address to instructions, this is the CFG of the java method
[out]predecessor_mapthe output of the function, populated as described above
msg_handlerfor reporting warnings

Definition at line 303 of file java_local_variable_table.cpp.

◆ populate_variable_address_map()

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 
)
static

See above.

Parameters
firstvarstart of range of local variable table entries to consider
varlimitend of range of local variable table entries to consider
[out]live_variable_at_addresspopulated 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.

◆ walk_to_next_index()

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 
)
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.