cprover
java_local_variable_table.cpp File Reference

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>
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, unsigned >
 
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 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...
 

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

parameters: vars_with_holes: variable table
Returns
Removes zero-size entries from vars_with_holes

Definition at line 678 of file java_local_variable_table.cpp.

Referenced by java_bytecode_convert_methodt::setup_local_variables().

◆ 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 start: Variable to find the predecessors of predecessor_map: Map from local variables to sets of predecessors.

Parameters
Outputsresult: 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().

◆ get_common_dominator()

static unsigned 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_vars: Set of variables we want the common dominator
for. dominator_analysis: Already-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 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().

◆ is_store_to_slot()

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

See above.

parameters: inst: Java bytecode instruction
slotidx: local variable slot number
Returns
Returns true if 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().

◆ lt_index()

◆ lt_startpc()

◆ maybe_add_hole()

static void maybe_add_hole ( local_variable_with_holest var,
unsigned  from,
unsigned  to 
)
static

See above.

parameters: from, to: bounds of a gap in var's live range,
inclusive and exclusive respectively
Returns
Adds a hole to 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().

◆ 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_vars: a set of 2+ variable table entries to merge
dominator_analysis: already-calculated dominator tree
Returns
Populates 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().

◆ 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,
unsigned  expanded_live_range_start 
)
static

See above.

parameters: merge_vars: a set of 2+ variable table entries to merge
expanded_live_range_start: address where the merged variable will be declared
Returns
Adds holes 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 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().

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

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

◆ 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: firstvar-varlimit: range of local variable table
entries to consider
Returns
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().

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

parameters: it1 and it2, which are iterators into the same vector,
of which itend is the end() iterator.
Returns
Moves 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().