cprover
|
#include <java_bytecode_convert_method_class.h>
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_holest > | local_variable_table_with_holest |
typedef std::map< unsigned, converted_instructiont > | address_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 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) |
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< variablet > | variablest |
typedef std::vector< exprt > | stackt |
Protected Member Functions | |
codet | get_array_bounds_check (const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc) |
const variablet & | find_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_blockt & | get_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_blockt & | 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) |
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_infot & | get_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_tablet & | symbol_table |
const size_t | max_array_length |
safe_pointer< ci_lazy_methodst > | lazy_methods |
irep_idt | method_id |
irep_idt | current_method |
typet | method_return_type |
character_refine_preprocesst | character_preprocess |
expanding_vectort< variablest > | variables |
std::set< symbol_exprt > | used_local_names |
bool | method_has_this |
std::list< symbol_exprt > | tmp_vars |
stackt | stack |
Additional Inherited Members |
Definition at line 31 of file java_bytecode_convert_method_class.h.
typedef std::map<unsigned, converted_instructiont> java_bytecode_convert_methodt::address_mapt |
Definition at line 166 of file java_bytecode_convert_method_class.h.
Definition at line 50 of file java_bytecode_convert_method_class.h.
Definition at line 49 of file java_bytecode_convert_method_class.h.
typedef cfg_dominators_templatet<method_with_amapt, unsigned, false> java_bytecode_convert_methodt::java_cfg_dominatorst |
Definition at line 169 of file java_bytecode_convert_method_class.h.
typedef std::vector<local_variable_with_holest> java_bytecode_convert_methodt::local_variable_table_with_holest |
Definition at line 83 of file java_bytecode_convert_method_class.h.
Definition at line 51 of file java_bytecode_convert_method_class.h.
Definition at line 52 of file java_bytecode_convert_method_class.h.
typedef std::pair<const methodt &, const address_mapt &> java_bytecode_convert_methodt::method_with_amapt |
Definition at line 167 of file java_bytecode_convert_method_class.h.
Definition at line 48 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 140 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 97 of file java_bytecode_convert_method_class.h.
|
strongprotected |
Enumerator | |
---|---|
VARIABLE | |
ARRAY_REF | |
STATIC_FIELD | |
FIELD |
Definition at line 225 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
INST_INDEX | |
INST_INDEX_CONST |
Definition at line 102 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
CAST_AS_NEEDED | |
NO_CAST |
Definition at line 119 of file java_bytecode_convert_method_class.h.
|
inline |
Definition at line 34 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 259 of file java_bytecode_convert_method.cpp.
References irept::add(), symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, dstringt::empty(), struct_union_typet::componentt::get_base_name(), struct_union_typet::componentt::get_name(), get_variable_slots(), code_typet::has_this(), id2string(), java_bytecode_parse_treet::methodt::is_abstract, java_bytecode_parse_treet::membert::is_final, java_bytecode_parse_treet::methodt::is_native, java_bytecode_parse_treet::membert::is_static, java_char_from_type(), java_type_from_string(), java_bytecode_parse_treet::methodt::local_variable_table, symbolt::location, symbolt::mode, symbolt::name, java_bytecode_parse_treet::membert::name, code_typet::parameters(), symbolt::pretty_name, code_typet::return_type(), irept::set(), struct_union_typet::componentt::set_base_name(), source_locationt::set_function(), struct_union_typet::componentt::set_name(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, symbolt::symbol_expr(), to_code_type(), symbolt::type, exprt::type(), and symbolt::value.
Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf(), and operator()().
|
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().
|
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().
|
protected |
See find_initialisers_for_slot
above for more detail.
amap
: Map from bytecode index to instruction dominator_analysis
: Already computed dominator tree for the Java function described by amap
vars
which flow together Definition at line 600 of file java_local_variable_table.cpp.
References lt_index(), and walk_to_next_index().
|
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.
amap
: Map from bytecode address to instruction 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().
|
protected |
See above.
var_list
: List of candidates that use the slot we're interested in address
. Definition at line 718 of file java_local_variable_table.cpp.
References java_bytecode_convert_methodt::variablet::start_pc.
|
protected |
Definition at line 454 of file java_bytecode_convert_method.cpp.
References code_blockt::add(), from_integer(), java_int_type(), and exprt::operands().
|
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.
Definition at line 523 of file java_bytecode_convert_method.cpp.
Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().
|
protected |
Definition at line 409 of file java_bytecode_convert_method.cpp.
References bytecode_info, and patternt::p.
Referenced by java_bytecode_convert_methodt::block_tree_nodet::get_leaf().
|
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)
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().
|
protected |
Definition at line 92 of file java_bytecode_convert_method.cpp.
References struct_union_typet::componentt::get_name(), id2string(), and size_type().
Definition at line 134 of file java_bytecode_convert_method.cpp.
References id2string().
|
inline |
Definition at line 54 of file java_bytecode_convert_method_class.h.
References convert().
|
protected |
Definition at line 100 of file java_bytecode_convert_method.cpp.
References stack.
|
protected |
removes minimum(n, stack.size()) elements from the stack
Definition at line 118 of file java_bytecode_convert_method.cpp.
References stack.
|
protected |
Definition at line 125 of file java_bytecode_convert_method.cpp.
References stack.
|
staticprotected |
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
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().
|
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().
|
protected |
See find_initialisers_for_slot
above for more detail.
amap
: Map from bytecode indices to instructions in m
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.
|
protected |
Definition at line 139 of file java_bytecode_convert_method.cpp.
References irept::add(), symbolt::base_name, id2string(), symbolt::is_static_lifetime, symbolt::mode, symbolt::name, irept::set(), and symbolt::type.
|
protected |
Definition at line 161 of file java_bytecode_convert_method.cpp.
References CHECK_RETURN, dstringt::empty(), symbol_exprt::get_identifier(), id2string(), integer2size_t(), java_type_from_char(), irept::set(), java_bytecode_convert_methodt::variablet::symbol_expr, to_constant_expr(), to_integer(), and exprt::type().
|
protected |
Definition at line 67 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 65 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 62 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 61 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 100 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 64 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 66 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 141 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 60 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 132 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 99 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 98 of file java_bytecode_convert_method_class.h.