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_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support) | |
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 | |
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) |
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address address a value of type type_char stored in the JVM's slot arg . More... | |
symbol_exprt | tmp_variable (const std::string &prefix, const typet &type) |
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_parameter (const local_variablet &v) |
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a parameter of that method. More... | |
void | find_initializers (local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms) |
See find_initializers_for_slot above for more detail. More... | |
void | find_initializers_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 GOTO variable 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_initializers_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... | |
optionalt< symbolt > | get_lambda_method_symbol (const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index) |
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method). More... | |
void | convert (const symbolt &class_symbol, const methodt &) |
codet | convert_instructions (const methodt &, const java_class_typet::java_lambda_method_handlest &) |
const bytecode_infot & | get_bytecode_info (const irep_idt &statement) |
codet | get_clinit_call (const irep_idt &classname) |
Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check. More... | |
bool | is_method_inherited (const irep_idt &classname, const irep_idt &methodid) const |
Returns true iff method methodid from class classname is a method inherited from a class (and not an interface!) from which classname inherits, either directly or indirectly. More... | |
irep_idt | get_static_field (const irep_idt &class_identifier, const irep_idt &component_name) const |
Get static field identifier referred to by class_identifier.component_name Note this may be inherited from either a parent or an interface. More... | |
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... | |
std::vector< unsigned int > | try_catch_handler (unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const |
void | draw_edges_from_ret_to_jsr (address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const |
optionalt< exprt > | convert_invoke_dynamic (const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0) |
codet | convert_astore (const irep_idt &statement, const exprt::operandst &op, const source_locationt &location) |
codet | convert_store (const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location) |
exprt | convert_aload (const irep_idt &statement, const exprt::operandst &op) const |
code_blockt | convert_ret (const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address) |
codet | convert_if_cmp (const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const |
codet | convert_if (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const |
codet | convert_ifnonull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const |
codet | convert_ifnull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const |
codet | convert_iinc (const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address) |
exprt::operandst & | convert_ushr (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const |
exprt::operandst & | convert_cmp (const exprt::operandst &op, exprt::operandst &results) const |
exprt::operandst & | convert_cmp2 (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const |
void | convert_getstatic (const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results) |
codet | convert_putfield (const exprt &arg0, const exprt::operandst &op) |
codet | convert_putstatic (const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr) |
void | convert_new (const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results) |
void | convert_newarray (const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) |
void | convert_multianewarray (const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) |
codet & | do_exception_handling (const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c) |
void | convert_athrow (const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const |
void | convert_checkcast (const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const |
codet | convert_monitorenterexit (const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location) |
codet & | replace_call_to_cprover_assume (source_locationt location, codet &c) |
void | convert_invoke (source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results) |
exprt::operandst & | convert_const (const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const |
void | convert_dup2_x2 (exprt::operandst &op, exprt::operandst &results) |
void | convert_dup2_x1 (exprt::operandst &op, exprt::operandst &results) |
void | convert_dup2 (exprt::operandst &op, exprt::operandst &results) |
codet | convert_switch (java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location) |
codet | convert_pop (const irep_idt &statement, const exprt::operandst &op) |
Static Protected Member Functions | |
static irep_idt | label (const irep_idt &address) |
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_table_baset & | symbol_table |
const size_t | max_array_length |
const bool | throw_assertion_error |
const bool | threading_support |
optionalt< ci_lazy_methods_neededt > | needed_lazy_methods |
irep_idt | method_id |
Fully qualified name of the method under translation. More... | |
irep_idt | current_method |
A copy of method_id :/. More... | |
typet | method_return_type |
Return type of the method under conversion. More... | |
java_string_library_preprocesst & | string_preprocess |
unsigned | slots_for_parameters |
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under translation. More... | |
expanding_vectort< variablest > | variables |
std::set< symbol_exprt > | used_local_names |
bool | method_has_this |
std::map< irep_idt, bool > | class_has_clinit_method |
std::map< irep_idt, bool > | any_superclass_has_clinit_method |
class_hierarchyt | class_hierarchy |
std::list< symbol_exprt > | tmp_vars |
stackt | stack |
Additional Inherited Members |
Definition at line 32 of file java_bytecode_convert_method_class.h.
typedef std::map<unsigned, converted_instructiont> java_bytecode_convert_methodt::address_mapt |
Definition at line 202 of file java_bytecode_convert_method_class.h.
Definition at line 59 of file java_bytecode_convert_method_class.h.
Definition at line 58 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 205 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 109 of file java_bytecode_convert_method_class.h.
Definition at line 60 of file java_bytecode_convert_method_class.h.
Definition at line 61 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 203 of file java_bytecode_convert_method_class.h.
Definition at line 57 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 167 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 126 of file java_bytecode_convert_method_class.h.
|
strongprotected |
Enumerator | |
---|---|
VARIABLE | |
ARRAY_REF | |
STATIC_FIELD | |
FIELD |
Definition at line 284 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
INST_INDEX | |
INST_INDEX_CONST |
Definition at line 134 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
CAST_AS_NEEDED | |
NO_CAST |
Definition at line 146 of file java_bytecode_convert_method_class.h.
|
inline |
Definition at line 35 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 432 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), java_method_typet::add_throws_exceptions(), symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, expanding_vectort< T >::clear(), convert_instructions(), current_method, messaget::debug(), java_bytecode_parse_treet::membert::descriptor, dstringt::empty(), messaget::eom(), code_typet::get_is_constructor(), symbol_table_baset::get_writeable(), code_typet::has_this(), id2string(), INVARIANT, java_bytecode_parse_treet::methodt::is_abstract, is_constructor(), java_bytecode_parse_treet::methodt::is_native, is_parameter(), java_char_from_type(), java_local_variable_slots(), java_method_parameter_slots(), java_type_from_string(), java_type_from_string_with_exception(), java_class_typet::lambda_method_handles(), java_bytecode_parse_treet::methodt::local_variable_table, symbolt::location, method_has_this, method_id, method_return_type, symbolt::mode, symbolt::module, symbolt::name, java_bytecode_parse_treet::membert::name, code_typet::parameters(), symbolt::pretty_name, pretty_signature(), expanding_vectort< T >::push_back(), messaget::result(), code_typet::return_type(), irept::set(), source_locationt::set_function(), slots_for_parameters, java_bytecode_parse_treet::methodt::source_location, symbolt::symbol_expr(), symbol_table, java_bytecode_parse_treet::methodt::throws_exception_table, to_java_class_type(), to_java_method_type(), to_string(), symbolt::type, symbolt::value, and variables.
Referenced by operator()().
|
protected |
Definition at line 2864 of file java_bytecode_convert_method.cpp.
References java_array_type(), java_bytecode_promotion(), java_type_from_char(), pointer_type(), irept::set(), typet::subtype(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2913 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), ARRAY_REF, java_array_type(), java_type_from_char(), code_blockt::move(), pointer_type(), save_stack_entries(), irept::set(), typet::subtype(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2298 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), source_locationt::as_string(), code_assertt::assertion(), code_assumet::assumption(), exprt::copy_to_operands(), uncaught_exceptions_domaint::get_exception_type(), exprt::move_to_operands(), irept::set(), source_locationt::set_comment(), source_locationt::set_property_class(), and throw_assertion_error.
Referenced by convert_instructions().
|
protected |
Definition at line 2282 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), source_locationt::set_comment(), and source_locationt::set_property_class().
Referenced by convert_instructions().
|
protected |
Definition at line 2679 of file java_bytecode_convert_method.cpp.
References from_integer(), and java_int_type().
Referenced by convert_instructions().
|
protected |
Definition at line 2651 of file java_bytecode_convert_method.cpp.
References from_integer(), and java_int_type().
Referenced by convert_instructions().
|
protected |
Definition at line 2060 of file java_bytecode_convert_method.cpp.
References DATA_INVARIANT, ieee_float_spect::double_precision(), ieee_floatt::from_expr(), from_integer(), ieee_floatt::from_integer(), irept::id(), java_type_from_char(), ieee_float_spect::single_precision(), to_constant_expr(), ieee_floatt::to_expr(), to_integer(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2013 of file java_bytecode_convert_method.cpp.
References get_bytecode_type_width(), pop(), and stack.
Referenced by convert_instructions().
|
protected |
Definition at line 2026 of file java_bytecode_convert_method.cpp.
References get_bytecode_type_width(), pop(), and stack.
Referenced by convert_instructions().
|
protected |
Definition at line 2039 of file java_bytecode_convert_method.cpp.
References get_bytecode_type_width(), pop(), and stack.
Referenced by convert_instructions().
|
protected |
Definition at line 2608 of file java_bytecode_convert_method.cpp.
References get_clinit_call(), codet::get_statement(), irept::get_string(), irept::id(), java_bytecode_promotion(), needed_lazy_methods, pointer_type(), typet::subtype(), to_pointer_type(), to_symbol_type(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2784 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), code_ifthenelset::cond(), from_integer(), integer2string(), integer2unsigned(), label(), method_id, source_locationt::set_function(), and code_ifthenelset::then_case().
Referenced by convert_instructions().
|
protected |
Definition at line 2805 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), code_ifthenelset::cond(), get_if_cmp_operator(), integer2string(), integer2unsigned(), label(), binary_relation_exprt::lhs(), binary_relation_exprt::rhs(), and code_ifthenelset::then_case().
Referenced by convert_instructions().
|
protected |
Definition at line 2767 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), code_ifthenelset::cond(), integer2string(), integer2unsigned(), java_reference_type(), label(), code_ifthenelset::then_case(), to_pointer_type(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2750 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), code_ifthenelset::cond(), integer2string(), integer2unsigned(), java_reference_type(), label(), code_ifthenelset::then_case(), to_pointer_type(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2722 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), CAST_AS_NEEDED, exprt::copy_to_operands(), java_int_type(), code_assignt::lhs(), exprt::make_typecast(), NO_CAST, code_assignt::rhs(), save_stack_entries(), to_symbol_expr(), exprt::type(), variable(), and VARIABLE.
Referenced by convert_instructions().
|
protected |
Definition at line 989 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), code_blockt::add(), symbolt::base_name, java_bytecode_convert_methodt::block_tree_nodet::branch, java_bytecode_convert_methodt::block_tree_nodet::branch_addresses, bytecode_info, CAST_AS_NEEDED, CHECK_RETURN, convert_aload(), convert_astore(), convert_athrow(), convert_checkcast(), convert_cmp(), convert_cmp2(), convert_const(), convert_dup2(), convert_dup2_x1(), convert_dup2_x2(), convert_getstatic(), convert_if(), convert_if_cmp(), convert_ifnonull(), convert_ifnull(), convert_iinc(), convert_invoke(), convert_invoke_dynamic(), convert_monitorenterexit(), convert_multianewarray(), convert_new(), convert_newarray(), convert_pop(), convert_putfield(), convert_putstatic(), convert_ret(), convert_store(), convert_switch(), convert_ushr(), exprt::copy_to_operands(), DATA_INVARIANT, do_exception_handling(), draw_edges_from_ret_to_jsr(), java_bytecode_parse_treet::methodt::exception_table, code_blockt::find_last_statement(), forall_operands, from_integer(), gather_symbol_live_ranges(), irept::get(), get_block_for_pcrange(), get_bytecode_info(), java_bytecode_convert_methodt::block_tree_nodet::get_leaf(), get_or_create_block_for_pcrange(), codet::get_statement(), get_static_field(), irept::get_string(), has_prefix(), symbol_table_baset::has_symbol(), 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_bytecode_promotion(), java_int_type(), java_reference_type(), java_type_from_char(), label(), codet::make_block(), merge_source_location_rec(), method_return_type, symbolt::mode, exprt::move_to_operands(), symbolt::name, exprt::operands(), code_typet::parameters(), pointer_type(), bytecode_infot::pop, pop(), PRECONDITION, symbolt::pretty_name, bytecode_infot::push, push(), r, replace_call_to_cprover_assume(), irept::set(), setup_local_variables(), dstringt::size(), exprt::source_location(), stack, string2integer(), strip_java_namespace_prefix(), irept::swap(), symbol_table, threading_support, tmp_variable(), tmp_vars, to_code(), to_code_block(), to_code_label(), to_constant_expr(), to_integer(), to_java_method_type(), to_member(), to_string(), to_symbol_expr(), to_unsigned_integer(), try_catch_handler(), symbolt::type, exprt::type(), used_local_names, variable(), and variables.
Referenced by convert().
|
protected |
Definition at line 2099 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), exprt::add_source_location(), code_function_callt::arguments(), assign_parameter_names(), symbolt::base_name, messaget::debug(), messaget::eom(), code_function_callt::function(), irept::get(), get_clinit_call(), codet::get_statement(), irept::id(), id2string(), INVARIANT, is_constructor(), is_method_inherited(), java_boolean_type(), java_byte_type(), java_bytecode_promotion(), java_char_type(), java_reference_type(), java_short_type(), code_function_callt::lhs(), irept::make_nil(), method_id, symbolt::mode, exprt::move_to_operands(), symbolt::name, needed_lazy_methods, code_typet::parameters(), pop(), symbolt::pretty_name, java_string_library_preprocesst::replace_character_call(), code_typet::return_type(), irept::set(), code_typet::parametert::set_base_name(), source_locationt::set_function(), code_typet::set_is_constructor(), code_typet::parametert::set_this(), string_preprocess, symbol_table, symbol_table_baset::symbols, tmp_variable(), to_java_method_type(), symbolt::type, exprt::type(), and symbolt::value.
Referenced by convert_instructions().
|
protected |
Definition at line 2945 of file java_bytecode_convert_method.cpp.
References messaget::debug(), messaget::eom(), irept::get_int(), get_lambda_method_symbol(), messaget::get_message_handler(), code_typet::parameters(), pop(), code_typet::return_type(), symbol_table, to_java_method_type(), exprt::type(), and zero_initializer().
Referenced by convert_instructions().
|
protected |
Definition at line 1987 of file java_bytecode_convert_method.cpp.
References code_function_callt::function(), symbol_table_baset::has_symbol(), java_reference_type(), needed_lazy_methods, symbol_table, and threading_support.
Referenced by convert_instructions().
|
protected |
Definition at line 2451 of file java_bytecode_convert_method.cpp.
References exprt::copy_to_operands(), dstringt::empty(), from_integer(), source_locationt::get_line(), java_int_type(), java_reference_type(), max_array_length, exprt::move_to_operands(), PRECONDITION, tmp_variable(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2534 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), dstringt::empty(), get_clinit_call(), source_locationt::get_line(), codet::get_statement(), java_reference_type(), exprt::move_to_operands(), tmp_variable(), to_symbol_type(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2479 of file java_bytecode_convert_method.cpp.
References exprt::copy_to_operands(), from_integer(), irept::id(), java_array_type(), java_int_type(), max_array_length, exprt::move_to_operands(), tmp_variable(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 1919 of file java_bytecode_convert_method.cpp.
References get_bytecode_type_width(), and pop().
Referenced by convert_instructions().
|
protected |
Definition at line 2593 of file java_bytecode_convert_method.cpp.
References exprt::copy_to_operands(), FIELD, irept::get(), save_stack_entries(), and to_member().
Referenced by convert_instructions().
|
protected |
Definition at line 2561 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), get_clinit_call(), symbol_exprt::get_identifier(), codet::get_statement(), irept::get_string(), irept::id(), exprt::move_to_operands(), needed_lazy_methods, save_stack_entries(), STATIC_FIELD, to_symbol_type(), and exprt::type().
Referenced by convert_instructions().
|
protected |
Definition at line 2833 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), branch(), from_integer(), label(), exprt::move_to_operands(), NO_CAST, pointer_type(), to_string(), and variable().
Referenced by convert_instructions().
|
protected |
Definition at line 2885 of file java_bytecode_convert_method.cpp.
References symbol_exprt::get_identifier(), code_blockt::move(), NO_CAST, save_stack_entries(), to_symbol_expr(), exprt::type(), variable(), and VARIABLE.
Referenced by convert_instructions().
|
protected |
Definition at line 1935 of file java_bytecode_convert_method.cpp.
References code_blockt::add(), exprt::add_source_location(), code_switcht::body(), code_switch_caset::case_op(), code_switch_caset::code(), DATA_INVARIANT, integer2string(), label(), exprt::make_typecast(), code_switch_caset::set_default(), to_constant_expr(), to_integer(), exprt::type(), and code_switcht::value().
Referenced by convert_instructions().
|
protected |
Definition at line 2699 of file java_bytecode_convert_method.cpp.
References irept::get_size_t(), java_type_from_char(), exprt::make_typecast(), and exprt::type().
Referenced by convert_instructions().
|
protected |
actually create a temporary variable to hold the value of a stack entry
Definition at line 3263 of file java_bytecode_convert_method.cpp.
References exprt::copy_to_operands(), and tmp_variable().
Referenced by save_stack_entries().
|
protected |
Definition at line 2340 of file java_bytecode_convert_method.cpp.
References code_push_catcht::exception_list(), java_bytecode_parse_treet::methodt::exception_table, INVARIANT, label(), exprt::move_to_operands(), pos(), and to_string().
Referenced by convert_instructions().
|
protected |
Definition at line 2976 of file java_bytecode_convert_method.cpp.
Referenced by convert_instructions().
|
protected |
See find_initializers_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 657 of file java_local_variable_table.cpp.
References find_initializers_for_slot(), lt_index(), and walk_to_next_index().
Referenced by setup_local_variables().
|
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 GOTO variable 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 560 of file java_local_variable_table.cpp.
References gather_transitive_predecessors(), messaget::get_message_handler(), INVARIANT, merge_variable_table_entries(), populate_predecessor_map(), populate_variable_address_map(), and messaget::status().
Referenced by find_initializers().
|
protected |
See above.
var_list
: List of candidates that use the slot we're interested in address
. Definition at line 813 of file java_local_variable_table.cpp.
References java_bytecode_convert_methodt::variablet::start_pc.
Referenced by variable().
|
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 712 of file java_bytecode_convert_method.cpp.
References get_or_create_block_for_pcrange().
Referenced by convert_instructions().
|
protected |
Definition at line 626 of file java_bytecode_convert_method.cpp.
References bytecode_info, messaget::eom(), messaget::error(), and bytecode_infot::mnemonic.
Referenced by convert_instructions().
Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check.
classname | Class name |
Definition at line 966 of file java_bytecode_convert_method.cpp.
References clinit_wrapper_name(), code_function_callt::function(), needed_lazy_methods, symbol_table, and symbol_table_baset::symbols.
Referenced by convert_getstatic(), convert_invoke(), convert_new(), and convert_putstatic().
|
protected |
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).
lambda_method_handles | Vector of lambda method handles (bootstrap methods) of the class where the lambda is called |
index | Index of the lambda method handle in the vector |
Definition at line 319 of file java_bytecode_convert_method.cpp.
References dstringt::empty(), symbol_exprt::get_identifier(), symbol_table_baset::lookup_ref(), and symbol_table.
Referenced by convert_invoke_dynamic().
|
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 744 of file java_bytecode_convert_method.cpp.
References java_bytecode_convert_methodt::block_tree_nodet::branch, java_bytecode_convert_methodt::block_tree_nodet::branch_addresses, code_labelt::code(), messaget::debug(), messaget::eom(), irept::find(), codet::get_statement(), id2string(), java_bytecode_convert_methodt::block_tree_nodet::leaf, exprt::move_to_operands(), exprt::operands(), replace_goto_target(), code_labelt::set_label(), to_code(), to_code_block(), and to_code_label().
Referenced by convert_instructions(), and get_block_for_pcrange().
|
protected |
Get static field identifier referred to by class_identifier.component_name
Note this may be inherited from either a parent or an interface.
class_identifier | class used to refer to the field |
component_name | component (static field) name |
Definition at line 3156 of file java_bytecode_convert_method.cpp.
References class_hierarchy, resolve_inherited_componentt::inherited_componentt::get_full_component_identifier(), get_inherited_component(), INVARIANT, resolve_inherited_componentt::inherited_componentt::is_valid(), and symbol_table.
Referenced by convert_instructions().
|
protected |
Returns true iff method methodid
from class classname
is a method inherited from a class (and not an interface!) from which classname
inherits, either directly or indirectly.
classname | class whose method is referenced |
methodid | method basename |
Definition at line 3137 of file java_bytecode_convert_method.cpp.
References class_hierarchy, get_inherited_component(), resolve_inherited_componentt::inherited_componentt::is_valid(), and symbol_table.
Referenced by convert_invoke().
|
inlineprotected |
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a parameter of that method.
Assumes that slots_for_parameters
is initialized upon call.
Definition at line 179 of file java_bytecode_convert_method_class.h.
References java_bytecode_parse_treet::methodt::local_variablet::index, and slots_for_parameters.
Referenced by convert(), and setup_local_variables().
Definition at line 165 of file java_bytecode_convert_method.cpp.
References id2string().
Referenced by convert_if(), convert_if_cmp(), convert_ifnonull(), convert_ifnull(), convert_instructions(), convert_ret(), convert_switch(), and do_exception_handling().
|
inline |
Definition at line 63 of file java_bytecode_convert_method_class.h.
References convert().
|
protected |
Definition at line 131 of file java_bytecode_convert_method.cpp.
References messaget::eom(), messaget::error(), and stack.
Referenced by convert_dup2(), convert_dup2_x1(), convert_dup2_x2(), convert_instructions(), convert_invoke(), convert_invoke_dynamic(), convert_pop(), and replace_call_to_cprover_assume().
|
protected |
removes minimum(n, stack.size()) elements from the stack
Definition at line 149 of file java_bytecode_convert_method.cpp.
References stack.
|
protected |
Definition at line 156 of file java_bytecode_convert_method.cpp.
References stack.
Referenced by convert_instructions().
|
protected |
Definition at line 2267 of file java_bytecode_convert_method.cpp.
References exprt::add_source_location(), exprt::make_typecast(), method_id, pop(), source_locationt::set_function(), and exprt::type().
Referenced by convert_instructions().
|
staticprotected |
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
Definition at line 678 of file java_bytecode_convert_method.cpp.
References codet::get_statement(), exprt::operands(), to_code(), and to_code_goto().
Referenced by get_or_create_block_for_pcrange().
|
protected |
Create temporary variables if a write instruction can have undesired side- effects.
tmp_var_prefix | The prefix string to use for new temporary variables | |
tmp_var_type | The type of the temporary variable. | |
[out] | block | The code block the assignment is added to if required. |
write_type | The enumeration type of the write instruction. | |
identifier | The identifier of the symbol in the write instruction. |
Definition at line 3181 of file java_bytecode_convert_method.cpp.
References ARRAY_REF, create_stack_tmp_var(), expr_try_dynamic_cast(), FIELD, tvt::is_true(), tvt::is_unknown(), exprt::operands(), stack, STATIC_FIELD, tvt::unknown(), and VARIABLE.
Referenced by convert_astore(), convert_iinc(), convert_putfield(), convert_putstatic(), and convert_store().
|
protected |
See find_initializers_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 706 of file java_local_variable_table.cpp.
References symbol_table_baset::add(), symbolt::base_name, cleanup_var_table(), messaget::debug(), java_bytecode_parse_treet::membert::descriptor, messaget::eom(), find_initializers(), id2string(), symbolt::is_file_local, symbolt::is_lvalue, is_parameter(), java_bytecode_parse_treet::membert::is_static, symbolt::is_thread_local, symbolt::is_type, java_type_from_string(), java_bytecode_parse_treet::methodt::local_variable_table, method_id, symbolt::mode, symbolt::name, symbolt::pretty_name, expanding_vectort< T >::push_back(), messaget::result(), slots_for_parameters, symbol_table, symbolt::type, variables, and messaget::warning().
Referenced by convert_instructions().
|
protected |
Definition at line 170 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), symbolt::base_name, current_method, id2string(), symbolt::is_static_lifetime, symbolt::mode, symbolt::name, messaget::result(), symbol_table, tmp_vars, to_string(), and symbolt::type.
Referenced by convert_instructions(), convert_invoke(), convert_multianewarray(), convert_new(), convert_newarray(), and create_stack_tmp_var().
|
protected |
Definition at line 2992 of file java_bytecode_convert_method.cpp.
References messaget::result().
Referenced by convert_instructions().
|
protected |
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address address
a value of type type_char
stored in the JVM's slot arg
.
arg | The local variable slot |
type_char | The type of the value stored in the slot pointed by arg . |
address | Bytecode address used to find a variable that the LVT declares to be live and living in the slot pointed by arg for this bytecode. |
do_cast | Indicates whether we should return the original symbol_exprt or a typecast_exprt if the type of the symbol_exprt does not equal that represented by type_char . |
Definition at line 207 of file java_bytecode_convert_method.cpp.
References CAST_AS_NEEDED, CHECK_RETURN, current_method, dstringt::empty(), find_variable_for_slot(), symbol_exprt::get_identifier(), id2string(), integer2size_t(), java_type_from_char(), messaget::result(), java_bytecode_convert_methodt::variablet::symbol_expr, to_constant_expr(), to_integer(), to_string(), used_local_names, and variables.
Referenced by convert_iinc(), convert_instructions(), convert_ret(), and convert_store().
|
protected |
Definition at line 131 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 130 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 132 of file java_bytecode_convert_method_class.h.
Referenced by get_static_field(), and is_method_inherited().
|
protected |
A copy of method_id
:/.
Definition at line 81 of file java_bytecode_convert_method_class.h.
Referenced by convert(), tmp_variable(), and variable().
|
protected |
Definition at line 70 of file java_bytecode_convert_method_class.h.
Referenced by convert_multianewarray(), and convert_newarray().
|
protected |
Definition at line 129 of file java_bytecode_convert_method_class.h.
Referenced by convert().
|
protected |
Fully qualified name of the method under translation.
Initialized by convert
. Example: "my.package.ClassName.myMethodName:(II)I"
Definition at line 78 of file java_bytecode_convert_method_class.h.
Referenced by convert(), convert_if(), convert_invoke(), replace_call_to_cprover_assume(), and setup_local_variables().
|
protected |
Return type of the method under conversion.
Initialized by convert
.
Definition at line 85 of file java_bytecode_convert_method_class.h.
Referenced by convert(), and convert_instructions().
|
protected |
Definition at line 73 of file java_bytecode_convert_method_class.h.
Referenced by convert_getstatic(), convert_invoke(), convert_monitorenterexit(), convert_putstatic(), and get_clinit_call().
|
protected |
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under translation.
Initialized in convert
.
Definition at line 92 of file java_bytecode_convert_method_class.h.
Referenced by convert(), is_parameter(), and setup_local_variables().
|
protected |
Definition at line 168 of file java_bytecode_convert_method_class.h.
Referenced by convert_dup2(), convert_dup2_x1(), convert_dup2_x2(), convert_instructions(), pop(), pop_residue(), push(), and save_stack_entries().
|
protected |
Definition at line 87 of file java_bytecode_convert_method_class.h.
Referenced by convert_invoke().
|
protected |
Definition at line 69 of file java_bytecode_convert_method_class.h.
Referenced by convert(), convert_instructions(), convert_invoke(), convert_invoke_dynamic(), convert_monitorenterexit(), get_clinit_call(), get_lambda_method_symbol(), get_static_field(), is_method_inherited(), setup_local_variables(), and tmp_variable().
|
protected |
Definition at line 72 of file java_bytecode_convert_method_class.h.
Referenced by convert_instructions(), and convert_monitorenterexit().
|
protected |
Definition at line 71 of file java_bytecode_convert_method_class.h.
Referenced by convert_athrow().
|
protected |
Definition at line 159 of file java_bytecode_convert_method_class.h.
Referenced by convert_instructions(), and tmp_variable().
|
protected |
Definition at line 128 of file java_bytecode_convert_method_class.h.
Referenced by convert_instructions(), and variable().
|
protected |
Definition at line 127 of file java_bytecode_convert_method_class.h.
Referenced by convert(), convert_instructions(), setup_local_variables(), and variable().