cprover
java_bytecode_convert_methodt Class Reference

#include <java_bytecode_convert_method_class.h>

Inheritance diagram for java_bytecode_convert_methodt:
[legend]
Collaboration diagram for java_bytecode_convert_methodt:
[legend]

Classes

struct  block_tree_nodet
 
struct  converted_instructiont
 
struct  holet
 
struct  local_variable_with_holest
 
class  variablet
 

Public Types

typedef java_bytecode_parse_treet::methodt methodt
 
typedef java_bytecode_parse_treet::instructiont instructiont
 
typedef methodt::instructionst instructionst
 
typedef methodt::local_variable_tablet local_variable_tablet
 
typedef methodt::local_variablet local_variablet
 
typedef std::vector< local_variable_with_holestlocal_variable_table_with_holest
 
typedef std::map< unsigned, converted_instructiontaddress_mapt
 
typedef std::pair< const methodt &, const address_mapt & > method_with_amapt
 
typedef cfg_dominators_templatet< method_with_amapt, unsigned, false > java_cfg_dominatorst
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 java_bytecode_convert_methodt (symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, safe_pointer< ci_lazy_methodst > _lazy_methods, const character_refine_preprocesst &_character_preprocess)
 
void operator() (const symbolt &class_symbol, const methodt &method)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Types

enum  instruction_sizet { INST_INDEX =2, INST_INDEX_CONST =3 }
 
enum  variable_cast_argumentt { CAST_AS_NEEDED, NO_CAST }
 
enum  bytecode_write_typet { bytecode_write_typet::VARIABLE, bytecode_write_typet::ARRAY_REF, bytecode_write_typet::STATIC_FIELD, bytecode_write_typet::FIELD }
 
typedef std::vector< variabletvariablest
 
typedef std::vector< exprtstackt
 

Protected Member Functions

codet get_array_bounds_check (const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc)
 
const variabletfind_variable_for_slot (size_t address, variablest &var_list)
 See above. More...
 
const exprt variable (const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
 
symbol_exprt tmp_variable (const std::string &prefix, const typet &type)
 
irep_idt label (const irep_idt &address)
 
exprt::operandst pop (std::size_t n)
 
void pop_residue (std::size_t n)
 removes minimum(n, stack.size()) elements from the stack More...
 
void push (const exprt::operandst &o)
 
bool is_constructor (const class_typet::methodt &method)
 
void find_initialisers (local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
 See find_initialisers_for_slot above for more detail. More...
 
void find_initialisers_for_slot (local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)
 Given a sequence of users of the same local variable slot, this figures out which ones are related by control flow, and combines them into a single entry with holes, such that after combination we can create a single declaration per variable table entry, placed at the live range's start address, which may be moved back so that the declaration dominates all uses. More...
 
void setup_local_variables (const methodt &m, const address_mapt &amap)
 See find_initialisers_for_slot above for more detail. More...
 
code_blocktget_block_for_pcrange (block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
 'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are both trees with the same shape). More...
 
code_blocktget_or_create_block_for_pcrange (block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address, const address_mapt &amap, bool allow_merge=true)
 As above, but this version can additionally create a new branch in the block_tree-node and code_blockt trees to envelop the requested address range. More...
 
void convert (const symbolt &class_symbol, const methodt &)
 
codet convert_instructions (const methodt &, const code_typet &)
 
const bytecode_infotget_bytecode_info (const irep_idt &statement)
 
void save_stack_entries (const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
 create temporary variables if a write instruction can have undesired side- effects More...
 
void create_stack_tmp_var (const std::string &, const typet &, code_blockt &, exprt &)
 actually create a temporary variable to hold the value of a stack entry More...
 

Static Protected Member Functions

static void replace_goto_target (codet &repl, const irep_idt &old_label, const irep_idt &new_label)
 Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'. More...
 

Protected Attributes

symbol_tabletsymbol_table
 
const size_t max_array_length
 
safe_pointer< ci_lazy_methodstlazy_methods
 
irep_idt method_id
 
irep_idt current_method
 
typet method_return_type
 
character_refine_preprocesst character_preprocess
 
expanding_vectort< variablestvariables
 
std::set< symbol_exprtused_local_names
 
bool method_has_this
 
std::list< symbol_exprttmp_vars
 
stackt stack
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 31 of file java_bytecode_convert_method_class.h.

Member Typedef Documentation

§ address_mapt

§ instructionst

§ instructiont

§ java_cfg_dominatorst

§ local_variable_table_with_holest

§ local_variable_tablet

§ local_variablet

§ method_with_amapt

§ methodt

§ stackt

typedef std::vector<exprt> java_bytecode_convert_methodt::stackt
protected

Definition at line 140 of file java_bytecode_convert_method_class.h.

§ variablest

typedef std::vector<variablet> java_bytecode_convert_methodt::variablest
protected

Definition at line 97 of file java_bytecode_convert_method_class.h.

Member Enumeration Documentation

§ bytecode_write_typet

Enumerator
VARIABLE 
ARRAY_REF 
STATIC_FIELD 
FIELD 

Definition at line 225 of file java_bytecode_convert_method_class.h.

§ instruction_sizet

Enumerator
INST_INDEX 
INST_INDEX_CONST 

Definition at line 102 of file java_bytecode_convert_method_class.h.

§ variable_cast_argumentt

Enumerator
CAST_AS_NEEDED 
NO_CAST 

Definition at line 119 of file java_bytecode_convert_method_class.h.

Constructor & Destructor Documentation

§ java_bytecode_convert_methodt()

java_bytecode_convert_methodt::java_bytecode_convert_methodt ( symbol_tablet _symbol_table,
message_handlert _message_handler,
size_t  _max_array_length,
safe_pointer< ci_lazy_methodst _lazy_methods,
const character_refine_preprocesst _character_preprocess 
)
inline

Definition at line 34 of file java_bytecode_convert_method_class.h.

Member Function Documentation

§ convert()

§ convert_instructions()

codet java_bytecode_convert_methodt::convert_instructions ( const methodt method,
const code_typet method_type 
)
protected

Definition at line 779 of file java_bytecode_convert_method.cpp.

References code_blockt::add(), exprt::add_source_location(), code_function_callt::arguments(), as_string(), symbolt::base_name, branch(), java_bytecode_convert_methodt::block_tree_nodet::branch, java_bytecode_convert_methodt::block_tree_nodet::branch_addresses, bytecode_info, code_switch_caset::case_op(), code_labelt::code(), code_switch_caset::code(), code_ifthenelset::cond(), exprt::copy_to_operands(), DATA_INVARIANT, ieee_float_spect::double_precision(), java_bytecode_parse_treet::methodt::exception_table, code_blockt::find_last_statement(), forall_operands, ieee_floatt::from_expr(), from_integer(), ieee_floatt::from_integer(), code_function_callt::function(), gather_symbol_live_ranges(), irept::get(), get_bytecode_type_width(), symbol_exprt::get_identifier(), get_if_cmp_operator(), get_nil_irep(), codet::get_statement(), irept::get_string(), irept::get_sub(), has_prefix(), irept::id(), id2string(), java_bytecode_parse_treet::methodt::instructions, integer2size_t(), integer2string(), INVARIANT, symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_thread_local, symbolt::is_type, java_array_type(), java_boolean_type(), java_byte_type(), java_bytecode_promotion(), java_char_type(), java_int_type(), java_reference_type(), java_short_type(), java_type_from_char(), code_assignt::lhs(), binary_relation_exprt::lhs(), code_function_callt::lhs(), loc, codet::make_block(), irept::make_nil(), exprt::make_typecast(), symbolt::mode, exprt::move_to_operands(), symbolt::name, ieee_floatt::NaN(), exprt::operands(), code_typet::parameters(), patternt::patternt(), pointer_type(), bytecode_infot::pop, pos(), PRECONDITION, symbolt::pretty_name, bytecode_infot::push, r, code_typet::return_type(), code_assignt::rhs(), binary_relation_exprt::rhs(), irept::set(), code_typet::parametert::set_base_name(), source_locationt::set_comment(), code_switch_caset::set_default(), source_locationt::set_function(), source_locationt::set_property_class(), code_typet::parametert::set_this(), ieee_float_spect::single_precision(), dstringt::size(), stack, string2integer(), strip_java_namespace_prefix(), typet::subtype(), irept::swap(), code_ifthenelset::then_case(), to_code(), to_code_block(), to_code_label(), to_code_type(), to_constant_expr(), ieee_floatt::to_expr(), to_floatbv_type(), to_integer(), to_member(), to_pointer_type(), to_symbol_expr(), to_symbol_type(), to_unsigned_integer(), symbolt::type, exprt::type(), symbolt::value, and zero_initializer().

Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().

§ create_stack_tmp_var()

void java_bytecode_convert_methodt::create_stack_tmp_var ( const std::string &  tmp_var_prefix,
const typet tmp_var_type,
code_blockt block,
exprt stack_entry 
)
protected

actually create a temporary variable to hold the value of a stack entry

Definition at line 2497 of file java_bytecode_convert_method.cpp.

References exprt::copy_to_operands().

§ find_initialisers()

void java_bytecode_convert_methodt::find_initialisers ( local_variable_table_with_holest vars,
const address_mapt amap,
const java_cfg_dominatorst dominator_analysis 
)
protected

See find_initialisers_for_slot above for more detail.

parameters: vars: Local variable table
amap: Map from bytecode index to instruction dominator_analysis: Already computed dominator tree for the Java function described by amap
Returns
Combines entries in vars which flow together

Definition at line 600 of file java_local_variable_table.cpp.

References lt_index(), and walk_to_next_index().

§ find_initialisers_for_slot()

void java_bytecode_convert_methodt::find_initialisers_for_slot ( local_variable_table_with_holest::iterator  firstvar,
local_variable_table_with_holest::iterator  varlimit,
const address_mapt amap,
const java_cfg_dominatorst dominator_analysis 
)
protected

Given a sequence of users of the same local variable slot, this figures out which ones are related by control flow, and combines them into a single entry with holes, such that after combination we can create a single declaration per variable table entry, placed at the live range's start address, which may be moved back so that the declaration dominates all uses.

parameters: firstvar-varlimit: sequence of variable table entries,
all of which should concern the same slot index. amap: Map from bytecode address to instruction
Returns
Side-effect: merges variable table entries which flow into one another (e.g. there are branches from one live range to another without re-initialising the local slot).

Definition at line 503 of file java_local_variable_table.cpp.

References gather_transitive_predecessors(), merge_variable_table_entries(), populate_predecessor_map(), and populate_variable_address_map().

§ find_variable_for_slot()

const java_bytecode_convert_methodt::variablet & java_bytecode_convert_methodt::find_variable_for_slot ( size_t  address,
variablest var_list 
)
protected

See above.

parameters: address: Address to find a variable table entry for
var_list: List of candidates that use the slot we're interested in
Returns
Returns the list entry covering this address (taking live range holes into account), or creates/returns an anonymous variable entry if nothing covers address.

Definition at line 718 of file java_local_variable_table.cpp.

References java_bytecode_convert_methodt::variablet::start_pc.

§ get_array_bounds_check()

codet java_bytecode_convert_methodt::get_array_bounds_check ( const exprt arraystruct,
const exprt idx,
const source_locationt original_sloc 
)
protected

§ get_block_for_pcrange()

code_blockt & java_bytecode_convert_methodt::get_block_for_pcrange ( block_tree_nodet tree,
code_blockt this_block,
unsigned  address_start,
unsigned  address_limit,
unsigned  next_block_start_address 
)
protected

'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are both trees with the same shape).

The caller is looking for the single block in the tree that most closely encloses bytecode address range [address_start,address_limit). 'next_block_start_address' is the start address of 'tree's successor sibling and is used to determine when the range spans out of its bounds.

parameters: 'tree', a code block descriptor, and 'this_block', the
corresponding actual code_blockt. 'address_start' and 'address_limit', the Java bytecode offsets searched for. 'next_block_start_address', the bytecode offset of tree/this_block's successor sibling, or UINT_MAX if none exists.
Returns
Returns the code_blockt most closely enclosing the given address range.

Definition at line 523 of file java_bytecode_convert_method.cpp.

Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().

§ get_bytecode_info()

const bytecode_infot & java_bytecode_convert_methodt::get_bytecode_info ( const irep_idt statement)
protected

§ get_or_create_block_for_pcrange()

code_blockt & java_bytecode_convert_methodt::get_or_create_block_for_pcrange ( block_tree_nodet tree,
code_blockt this_block,
unsigned  address_start,
unsigned  address_limit,
unsigned  next_block_start_address,
const address_mapt amap,
bool  allow_merge = true 
)
protected

As above, but this version can additionally create a new branch in the block_tree-node and code_blockt trees to envelop the requested address range.

For example, if the tree was initially flat, with nodes (1-10), (11-20), (21-30) and the caller asked for range 13-28, this would build a surrounding tree node, leaving the tree of shape (1-10), ^( (11-20), (21-30) )^, and return a reference to the new branch highlighted with ^^. 'tree' and 'this_block' trees are always maintained with equal shapes. ('this_block' may additionally contain code_declt children which are ignored for this purpose)

parameters: See above, plus the bytecode address map 'amap' and
'allow_merge' which is always true except when called from get_block_for_pcrange
Returns
See above, plus potential side-effects on 'tree' and 'this_block' as described in 'Purpose'

Definition at line 555 of file java_bytecode_convert_method.cpp.

References as_string(), java_bytecode_convert_methodt::block_tree_nodet::branch, java_bytecode_convert_methodt::block_tree_nodet::branch_addresses, code_labelt::code(), irept::find(), codet::get_statement(), java_bytecode_convert_methodt::block_tree_nodet::leaf, exprt::move_to_operands(), exprt::operands(), patternt::p, code_labelt::set_label(), to_code(), to_code_block(), and to_code_label().

Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().

§ is_constructor()

bool java_bytecode_convert_methodt::is_constructor ( const class_typet::methodt method)
protected

§ label()

irep_idt java_bytecode_convert_methodt::label ( const irep_idt address)
protected

Definition at line 134 of file java_bytecode_convert_method.cpp.

References id2string().

§ operator()()

void java_bytecode_convert_methodt::operator() ( const symbolt class_symbol,
const methodt method 
)
inline

Definition at line 54 of file java_bytecode_convert_method_class.h.

References convert().

§ pop()

exprt::operandst java_bytecode_convert_methodt::pop ( std::size_t  n)
protected

Definition at line 100 of file java_bytecode_convert_method.cpp.

References stack.

§ pop_residue()

void java_bytecode_convert_methodt::pop_residue ( std::size_t  n)
protected

removes minimum(n, stack.size()) elements from the stack

Definition at line 118 of file java_bytecode_convert_method.cpp.

References stack.

§ push()

void java_bytecode_convert_methodt::push ( const exprt::operandst o)
protected

Definition at line 125 of file java_bytecode_convert_method.cpp.

References stack.

§ replace_goto_target()

void java_bytecode_convert_methodt::replace_goto_target ( codet repl,
const irep_idt old_label,
const irep_idt new_label 
)
staticprotected

Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.

parameters: 'repl', a block of code in which to perform replacement,
and an old_label that should be replaced throughout by new_label.
Returns
None (side-effects on repl)

Definition at line 489 of file java_bytecode_convert_method.cpp.

References codet::get_statement(), exprt::operands(), to_code(), and to_code_goto().

Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().

§ save_stack_entries()

void java_bytecode_convert_methodt::save_stack_entries ( const std::string &  tmp_var_prefix,
const typet tmp_var_type,
code_blockt block,
const bytecode_write_typet  write_type,
const irep_idt identifier 
)
protected

create temporary variables if a write instruction can have undesired side- effects

Definition at line 2456 of file java_bytecode_convert_method.cpp.

References member_exprt::get_component_name(), symbol_exprt::get_identifier(), typecast_exprt::op(), stack, to_member_expr(), to_symbol_expr(), and to_typecast_expr().

§ setup_local_variables()

void java_bytecode_convert_methodt::setup_local_variables ( const methodt m,
const address_mapt amap 
)
protected

See find_initialisers_for_slot above for more detail.

parameters: m: Java method
amap: Map from bytecode indices to instructions in m
Returns
Populates this->vars_with_holes equal to this->local_variable_table, only with variable table entries that flow together combined. Also symbol-table registers all locals.

Definition at line 649 of file java_local_variable_table.cpp.

References symbolt::base_name, cleanup_var_table(), id2string(), symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_thread_local, symbolt::is_type, java_type_from_string(), java_bytecode_parse_treet::methodt::local_variable_table, symbolt::mode, symbolt::name, symbolt::pretty_name, and symbolt::type.

§ tmp_variable()

symbol_exprt java_bytecode_convert_methodt::tmp_variable ( const std::string &  prefix,
const typet type 
)
protected

§ variable()

Member Data Documentation

§ character_preprocess

character_refine_preprocesst java_bytecode_convert_methodt::character_preprocess
protected

Definition at line 67 of file java_bytecode_convert_method_class.h.

§ current_method

irep_idt java_bytecode_convert_methodt::current_method
protected

Definition at line 65 of file java_bytecode_convert_method_class.h.

§ lazy_methods

safe_pointer<ci_lazy_methodst> java_bytecode_convert_methodt::lazy_methods
protected

Definition at line 62 of file java_bytecode_convert_method_class.h.

§ max_array_length

const size_t java_bytecode_convert_methodt::max_array_length
protected

Definition at line 61 of file java_bytecode_convert_method_class.h.

§ method_has_this

bool java_bytecode_convert_methodt::method_has_this
protected

Definition at line 100 of file java_bytecode_convert_method_class.h.

§ method_id

irep_idt java_bytecode_convert_methodt::method_id
protected

Definition at line 64 of file java_bytecode_convert_method_class.h.

§ method_return_type

typet java_bytecode_convert_methodt::method_return_type
protected

Definition at line 66 of file java_bytecode_convert_method_class.h.

§ stack

stackt java_bytecode_convert_methodt::stack
protected

Definition at line 141 of file java_bytecode_convert_method_class.h.

§ symbol_table

symbol_tablet& java_bytecode_convert_methodt::symbol_table
protected

Definition at line 60 of file java_bytecode_convert_method_class.h.

§ tmp_vars

std::list<symbol_exprt> java_bytecode_convert_methodt::tmp_vars
protected

Definition at line 132 of file java_bytecode_convert_method_class.h.

§ used_local_names

std::set<symbol_exprt> java_bytecode_convert_methodt::used_local_names
protected

Definition at line 99 of file java_bytecode_convert_method_class.h.

§ variables

expanding_vectort<variablest> java_bytecode_convert_methodt::variables
protected

Definition at line 98 of file java_bytecode_convert_method_class.h.


The documentation for this class was generated from the following files: