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_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)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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

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)
 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_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...
 
optionalt< symboltget_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_infotget_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< exprtconvert_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::operandstconvert_ushr (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
 
exprt::operandstconvert_cmp (const exprt::operandst &op, exprt::operandst &results) const
 
exprt::operandstconvert_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)
 
codetdo_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)
 
codetreplace_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::operandstconvert_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_basetsymbol_table
 
const size_t max_array_length
 
const bool throw_assertion_error
 
const bool threading_support
 
optionalt< ci_lazy_methods_neededtneeded_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_preprocesststring_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< variablestvariables
 
std::set< symbol_exprtused_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_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 unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 32 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 167 of file java_bytecode_convert_method_class.h.

◆ variablest

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

Definition at line 126 of file java_bytecode_convert_method_class.h.

Member Enumeration Documentation

◆ bytecode_write_typet

Enumerator
VARIABLE 
ARRAY_REF 
STATIC_FIELD 
FIELD 

Definition at line 284 of file java_bytecode_convert_method_class.h.

◆ instruction_sizet

Enumerator
INST_INDEX 
INST_INDEX_CONST 

Definition at line 134 of file java_bytecode_convert_method_class.h.

◆ variable_cast_argumentt

Enumerator
CAST_AS_NEEDED 
NO_CAST 

Definition at line 146 of file java_bytecode_convert_method_class.h.

Constructor & Destructor Documentation

◆ java_bytecode_convert_methodt()

java_bytecode_convert_methodt::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 
)
inline

Definition at line 35 of file java_bytecode_convert_method_class.h.

Member Function Documentation

◆ convert()

void java_bytecode_convert_methodt::convert ( const symbolt class_symbol,
const methodt m 
)
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()().

◆ convert_aload()

exprt java_bytecode_convert_methodt::convert_aload ( const irep_idt statement,
const exprt::operandst op 
) const
protected

◆ convert_astore()

codet java_bytecode_convert_methodt::convert_astore ( const irep_idt statement,
const exprt::operandst op,
const source_locationt location 
)
protected

◆ convert_athrow()

◆ convert_checkcast()

void java_bytecode_convert_methodt::convert_checkcast ( const exprt arg0,
const exprt::operandst op,
codet c,
exprt::operandst results 
) const
protected

◆ convert_cmp()

exprt::operandst & java_bytecode_convert_methodt::convert_cmp ( const exprt::operandst op,
exprt::operandst results 
) const
protected

Definition at line 2679 of file java_bytecode_convert_method.cpp.

References from_integer(), and java_int_type().

Referenced by convert_instructions().

◆ convert_cmp2()

exprt::operandst & java_bytecode_convert_methodt::convert_cmp2 ( const irep_idt statement,
const exprt::operandst op,
exprt::operandst results 
) const
protected

Definition at line 2651 of file java_bytecode_convert_method.cpp.

References from_integer(), and java_int_type().

Referenced by convert_instructions().

◆ convert_const()

◆ convert_dup2()

void java_bytecode_convert_methodt::convert_dup2 ( exprt::operandst op,
exprt::operandst results 
)
protected

Definition at line 2013 of file java_bytecode_convert_method.cpp.

References get_bytecode_type_width(), pop(), and stack.

Referenced by convert_instructions().

◆ convert_dup2_x1()

void java_bytecode_convert_methodt::convert_dup2_x1 ( exprt::operandst op,
exprt::operandst results 
)
protected

Definition at line 2026 of file java_bytecode_convert_method.cpp.

References get_bytecode_type_width(), pop(), and stack.

Referenced by convert_instructions().

◆ convert_dup2_x2()

void java_bytecode_convert_methodt::convert_dup2_x2 ( exprt::operandst op,
exprt::operandst results 
)
protected

Definition at line 2039 of file java_bytecode_convert_method.cpp.

References get_bytecode_type_width(), pop(), and stack.

Referenced by convert_instructions().

◆ convert_getstatic()

void java_bytecode_convert_methodt::convert_getstatic ( const exprt arg0,
const symbol_exprt symbol_expr,
bool  is_assertions_disabled_field,
codet c,
exprt::operandst results 
)
protected

◆ convert_if()

codet java_bytecode_convert_methodt::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
protected

◆ convert_if_cmp()

codet java_bytecode_convert_methodt::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
protected

◆ convert_ifnonull()

codet java_bytecode_convert_methodt::convert_ifnonull ( const java_bytecode_convert_methodt::address_mapt address_map,
const exprt::operandst op,
const mp_integer number,
const source_locationt location 
) const
protected

◆ convert_ifnull()

codet java_bytecode_convert_methodt::convert_ifnull ( const java_bytecode_convert_methodt::address_mapt address_map,
const exprt::operandst op,
const mp_integer number,
const source_locationt location 
) const
protected

◆ convert_iinc()

codet java_bytecode_convert_methodt::convert_iinc ( const exprt arg0,
const exprt arg1,
const source_locationt location,
unsigned  address 
)
protected

◆ convert_instructions()

codet java_bytecode_convert_methodt::convert_instructions ( const methodt method,
const java_class_typet::java_lambda_method_handlest lambda_method_handles 
)
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().

◆ convert_invoke()

◆ convert_invoke_dynamic()

◆ convert_monitorenterexit()

codet java_bytecode_convert_methodt::convert_monitorenterexit ( const irep_idt statement,
const exprt::operandst op,
const source_locationt source_location 
)
protected

◆ convert_multianewarray()

void java_bytecode_convert_methodt::convert_multianewarray ( const source_locationt location,
const exprt arg0,
const exprt::operandst op,
codet c,
exprt::operandst results 
)
protected

◆ convert_new()

void java_bytecode_convert_methodt::convert_new ( const source_locationt location,
const exprt arg0,
codet c,
exprt::operandst results 
)
protected

◆ convert_newarray()

void java_bytecode_convert_methodt::convert_newarray ( const source_locationt location,
const irep_idt statement,
const exprt arg0,
const exprt::operandst op,
codet c,
exprt::operandst results 
)
protected

◆ convert_pop()

codet java_bytecode_convert_methodt::convert_pop ( const irep_idt statement,
const exprt::operandst op 
)
protected

Definition at line 1919 of file java_bytecode_convert_method.cpp.

References get_bytecode_type_width(), and pop().

Referenced by convert_instructions().

◆ convert_putfield()

codet java_bytecode_convert_methodt::convert_putfield ( const exprt arg0,
const exprt::operandst op 
)
protected

◆ convert_putstatic()

◆ convert_ret()

code_blockt java_bytecode_convert_methodt::convert_ret ( const std::vector< unsigned int > &  jsr_ret_targets,
const exprt arg0,
const source_locationt location,
const unsigned  address 
)
protected

◆ convert_store()

codet java_bytecode_convert_methodt::convert_store ( const irep_idt statement,
const exprt arg0,
const exprt::operandst op,
const unsigned  address,
const source_locationt location 
)
protected

◆ convert_switch()

◆ convert_ushr()

exprt::operandst & java_bytecode_convert_methodt::convert_ushr ( const irep_idt statement,
const exprt::operandst op,
exprt::operandst results 
) const
protected

◆ 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 3263 of file java_bytecode_convert_method.cpp.

References exprt::copy_to_operands(), and tmp_variable().

Referenced by save_stack_entries().

◆ do_exception_handling()

codet & java_bytecode_convert_methodt::do_exception_handling ( const methodt method,
const std::set< unsigned int > &  working_set,
unsigned int  cur_pc,
codet c 
)
protected

◆ draw_edges_from_ret_to_jsr()

void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr ( java_bytecode_convert_methodt::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
protected

Definition at line 2976 of file java_bytecode_convert_method.cpp.

Referenced by convert_instructions().

◆ find_initializers()

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

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

◆ find_initializers_for_slot()

void java_bytecode_convert_methodt::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 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 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.

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-initializing the local slot).

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

◆ 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 813 of file java_local_variable_table.cpp.

References java_bytecode_convert_methodt::variablet::start_pc.

Referenced by variable().

◆ 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 712 of file java_bytecode_convert_method.cpp.

References get_or_create_block_for_pcrange().

Referenced by convert_instructions().

◆ get_bytecode_info()

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

◆ get_clinit_call()

codet java_bytecode_convert_methodt::get_clinit_call ( const irep_idt classname)
protected

Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check.

Parameters
classnameClass name
Returns
Returns a function call to the given class' static initializer wrapper if one is needed, or a skip instruction otherwise.

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

◆ get_lambda_method_symbol()

optionalt< symbolt > java_bytecode_convert_methodt::get_lambda_method_symbol ( const java_class_typet::java_lambda_method_handlest lambda_method_handles,
const size_t  index 
)
protected

Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).

Parameters
lambda_method_handlesVector of lambda method handles (bootstrap methods) of the class where the lambda is called
indexIndex of the lambda method handle in the vector
Returns
Symbol of the lambda method if the method handle has a known type

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

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

◆ get_static_field()

irep_idt java_bytecode_convert_methodt::get_static_field ( const irep_idt class_identifier,
const irep_idt component_name 
) const
protected

Get static field identifier referred to by class_identifier.component_name Note this may be inherited from either a parent or an interface.

Parameters
class_identifierclass used to refer to the field
component_namecomponent (static field) name
Returns
identifier of the actual concrete field referred to

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

◆ is_method_inherited()

bool java_bytecode_convert_methodt::is_method_inherited ( const irep_idt classname,
const irep_idt methodid 
) const
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.

Parameters
classnameclass whose method is referenced
methodidmethod 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().

◆ is_parameter()

bool java_bytecode_convert_methodt::is_parameter ( const local_variablet v)
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().

◆ label()

irep_idt java_bytecode_convert_methodt::label ( const irep_idt address)
staticprotected

◆ operator()()

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

Definition at line 63 of file java_bytecode_convert_method_class.h.

References convert().

◆ pop()

◆ 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 149 of file java_bytecode_convert_method.cpp.

References stack.

◆ push()

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

Definition at line 156 of file java_bytecode_convert_method.cpp.

References stack.

Referenced by convert_instructions().

◆ replace_call_to_cprover_assume()

codet & java_bytecode_convert_methodt::replace_call_to_cprover_assume ( source_locationt  location,
codet c 
)
protected

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

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

Parameters
tmp_var_prefixThe prefix string to use for new temporary variables
tmp_var_typeThe type of the temporary variable.
[out]blockThe code block the assignment is added to if required.
write_typeThe enumeration type of the write instruction.
identifierThe 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().

◆ setup_local_variables()

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

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

◆ tmp_variable()

◆ try_catch_handler()

std::vector< unsigned > java_bytecode_convert_methodt::try_catch_handler ( unsigned int  address,
const java_bytecode_parse_treet::methodt::exception_tablet exception_table 
) const
protected

Definition at line 2992 of file java_bytecode_convert_method.cpp.

References messaget::result().

Referenced by convert_instructions().

◆ variable()

const exprt java_bytecode_convert_methodt::variable ( const exprt arg,
char  type_char,
size_t  address,
java_bytecode_convert_methodt::variable_cast_argumentt  do_cast 
)
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.

Parameters
argThe local variable slot
type_charThe type of the value stored in the slot pointed by arg.
addressBytecode 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_castIndicates 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().

Member Data Documentation

◆ any_superclass_has_clinit_method

std::map<irep_idt, bool> java_bytecode_convert_methodt::any_superclass_has_clinit_method
protected

Definition at line 131 of file java_bytecode_convert_method_class.h.

◆ class_has_clinit_method

std::map<irep_idt, bool> java_bytecode_convert_methodt::class_has_clinit_method
protected

Definition at line 130 of file java_bytecode_convert_method_class.h.

◆ class_hierarchy

class_hierarchyt java_bytecode_convert_methodt::class_hierarchy
protected

Definition at line 132 of file java_bytecode_convert_method_class.h.

Referenced by get_static_field(), and is_method_inherited().

◆ current_method

irep_idt java_bytecode_convert_methodt::current_method
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().

◆ max_array_length

const size_t java_bytecode_convert_methodt::max_array_length
protected

◆ method_has_this

bool java_bytecode_convert_methodt::method_has_this
protected

Definition at line 129 of file java_bytecode_convert_method_class.h.

Referenced by convert().

◆ method_id

irep_idt java_bytecode_convert_methodt::method_id
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().

◆ method_return_type

typet java_bytecode_convert_methodt::method_return_type
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().

◆ needed_lazy_methods

optionalt<ci_lazy_methods_neededt> java_bytecode_convert_methodt::needed_lazy_methods
protected

◆ slots_for_parameters

unsigned java_bytecode_convert_methodt::slots_for_parameters
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().

◆ stack

stackt java_bytecode_convert_methodt::stack
protected

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_methodt::string_preprocess
protected

Definition at line 87 of file java_bytecode_convert_method_class.h.

Referenced by convert_invoke().

◆ symbol_table

◆ threading_support

const bool java_bytecode_convert_methodt::threading_support
protected

◆ throw_assertion_error

const bool java_bytecode_convert_methodt::throw_assertion_error
protected

Definition at line 71 of file java_bytecode_convert_method_class.h.

Referenced by convert_athrow().

◆ tmp_vars

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

Definition at line 159 of file java_bytecode_convert_method_class.h.

Referenced by convert_instructions(), and tmp_variable().

◆ used_local_names

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

Definition at line 128 of file java_bytecode_convert_method_class.h.

Referenced by convert_instructions(), and variable().

◆ variables

expanding_vectort<variablest> java_bytecode_convert_methodt::variables
protected

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