cprover
java_bytecode_convert_methodt Class Reference

#include <java_bytecode_convert_method_class.h>

+ Inheritance diagram for java_bytecode_convert_methodt:
+ Collaboration diagram for java_bytecode_convert_methodt:

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 uint16_t method_offsett
 
typedef std::vector< local_variable_with_holestlocal_variable_table_with_holest
 
typedef std::map< method_offsett, converted_instructiontaddress_mapt
 
typedef std::pair< const methodt &, const address_mapt & > method_with_amapt
 
typedef cfg_dominators_templatet< method_with_amapt, method_offsett, 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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, method_offsett address_start, method_offsett address_limit, method_offsett 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, method_offsett address_start, method_offsett address_limit, method_offsett 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 &)
 
code_blockt 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 &, 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< method_offsetttry_catch_handler (method_offsett 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< method_offsett > &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)
 
code_blockt convert_astore (const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
 
code_blockt convert_store (const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
 
exprt convert_aload (const irep_idt &statement, const exprt::operandst &op) const
 
code_blockt convert_ret (const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
 
code_ifthenelset 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
 
code_ifthenelset 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
 
code_ifthenelset convert_ifnonull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
 
code_ifthenelset convert_ifnull (const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
 
code_blockt convert_iinc (const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett 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)
 
code_blockt convert_putfield (const exprt &arg0, const exprt::operandst &op)
 
code_blockt 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)
 
code_blockt convert_newarray (const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
 
code_blockt convert_multianewarray (const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
 
codetdo_exception_handling (const methodt &method, const std::set< method_offsett > &working_set, method_offsett 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)
 
code_switcht convert_switch (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
 
method_offsett 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
 
const class_hierarchytclass_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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

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_offsett

◆ method_with_amapt

◆ methodt

◆ stackt

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

Definition at line 169 of file java_bytecode_convert_method_class.h.

◆ variablest

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

Definition at line 128 of file java_bytecode_convert_method_class.h.

Member Enumeration Documentation

◆ bytecode_write_typet

Enumerator
VARIABLE 
ARRAY_REF 
STATIC_FIELD 
FIELD 

Definition at line 286 of file java_bytecode_convert_method_class.h.

◆ instruction_sizet

Enumerator
INST_INDEX 
INST_INDEX_CONST 

Definition at line 136 of file java_bytecode_convert_method_class.h.

◆ variable_cast_argumentt

Enumerator
CAST_AS_NEEDED 
NO_CAST 

Definition at line 148 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 430 of file java_bytecode_convert_method.cpp.

◆ convert_aload()

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

Definition at line 2811 of file java_bytecode_convert_method.cpp.

◆ convert_astore()

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

Definition at line 2859 of file java_bytecode_convert_method.cpp.

◆ convert_athrow()

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

Definition at line 2262 of file java_bytecode_convert_method.cpp.

◆ convert_checkcast()

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

Definition at line 2246 of file java_bytecode_convert_method.cpp.

◆ convert_cmp()

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

Definition at line 2630 of file java_bytecode_convert_method.cpp.

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

◆ convert_const()

exprt::operandst & java_bytecode_convert_methodt::convert_const ( const irep_idt statement,
const exprt arg0,
exprt::operandst results 
) const
protected

Definition at line 2036 of file java_bytecode_convert_method.cpp.

◆ convert_dup2()

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

Definition at line 1989 of file java_bytecode_convert_method.cpp.

◆ convert_dup2_x1()

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

Definition at line 2002 of file java_bytecode_convert_method.cpp.

◆ convert_dup2_x2()

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

Definition at line 2015 of file java_bytecode_convert_method.cpp.

◆ 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

Definition at line 2559 of file java_bytecode_convert_method.cpp.

◆ convert_if()

code_ifthenelset 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

Definition at line 2735 of file java_bytecode_convert_method.cpp.

◆ convert_if_cmp()

code_ifthenelset 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

Definition at line 2757 of file java_bytecode_convert_method.cpp.

◆ convert_ifnonull()

code_ifthenelset 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

Definition at line 2717 of file java_bytecode_convert_method.cpp.

◆ convert_ifnull()

code_ifthenelset 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

Definition at line 2699 of file java_bytecode_convert_method.cpp.

◆ convert_iinc()

code_blockt java_bytecode_convert_methodt::convert_iinc ( const exprt arg0,
const exprt arg1,
const source_locationt location,
method_offsett  address 
)
protected

Definition at line 2673 of file java_bytecode_convert_method.cpp.

◆ convert_instructions()

code_blockt java_bytecode_convert_methodt::convert_instructions ( const methodt method,
const java_class_typet::java_lambda_method_handlest lambda_method_handles 
)
protected

Definition at line 990 of file java_bytecode_convert_method.cpp.

◆ convert_invoke()

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

Definition at line 2071 of file java_bytecode_convert_method.cpp.

◆ convert_invoke_dynamic()

optionalt< exprt > java_bytecode_convert_methodt::convert_invoke_dynamic ( const java_class_typet::java_lambda_method_handlest lambda_method_handles,
const source_locationt location,
const exprt arg0 
)
protected

Definition at line 2891 of file java_bytecode_convert_method.cpp.

◆ convert_monitorenterexit()

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

Definition at line 1966 of file java_bytecode_convert_method.cpp.

◆ convert_multianewarray()

code_blockt java_bytecode_convert_methodt::convert_multianewarray ( const source_locationt location,
const exprt arg0,
const exprt::operandst op,
exprt::operandst results 
)
protected

Definition at line 2406 of file java_bytecode_convert_method.cpp.

◆ convert_new()

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

Definition at line 2490 of file java_bytecode_convert_method.cpp.

◆ convert_newarray()

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

Definition at line 2434 of file java_bytecode_convert_method.cpp.

◆ convert_pop()

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

Definition at line 1899 of file java_bytecode_convert_method.cpp.

◆ convert_putfield()

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

Definition at line 2545 of file java_bytecode_convert_method.cpp.

◆ convert_putstatic()

code_blockt java_bytecode_convert_methodt::convert_putstatic ( const source_locationt location,
const exprt arg0,
const exprt::operandst op,
const symbol_exprt symbol_expr 
)
protected

Definition at line 2514 of file java_bytecode_convert_method.cpp.

◆ convert_ret()

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

Definition at line 2780 of file java_bytecode_convert_method.cpp.

◆ convert_store()

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

Definition at line 2832 of file java_bytecode_convert_method.cpp.

◆ convert_switch()

code_switcht java_bytecode_convert_methodt::convert_switch ( const exprt::operandst op,
const java_bytecode_parse_treet::instructiont::argst args,
const source_locationt location 
)
protected

Definition at line 1915 of file java_bytecode_convert_method.cpp.

◆ convert_ushr()

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

Definition at line 2650 of file java_bytecode_convert_method.cpp.

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

◆ do_exception_handling()

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

Definition at line 2301 of file java_bytecode_convert_method.cpp.

◆ 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< method_offsett > &  jsr_ret_targets,
const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &  ret_instructions 
) const
protected

Definition at line 2929 of file java_bytecode_convert_method.cpp.

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

Combines entries in vars which flow together.

Parameters
varsLocal variable table
amapMap from bytecode index to instruction
dominator_analysisAlready computed dominator tree for the Java function described by amap

Definition at line 672 of file java_local_variable_table.cpp.

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

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

Parameters
firstvarstart of sequence of variable table entries, all of which should concern the same slot index.
varlimitend of sequence of variable table entries
amapmap from bytecode address to instruction
dominator_analysisalready-calculated dominator tree

Definition at line 575 of file java_local_variable_table.cpp.

◆ 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
addressAddress to find a variable table entry for
var_listList 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 839 of file java_local_variable_table.cpp.

◆ get_block_for_pcrange()

code_blockt & java_bytecode_convert_methodt::get_block_for_pcrange ( block_tree_nodet tree,
code_blockt this_block,
method_offsett  address_start,
method_offsett  address_limit,
method_offsett  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
treeA code block descriptor.
this_blockThe corresponding actual code_blockt.
address_startthe Java bytecode offsets searched for.
address_limitthe Java bytecode offsets searched for.
next_block_start_addressThe 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 710 of file java_bytecode_convert_method.cpp.

◆ get_bytecode_info()

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

Definition at line 625 of file java_bytecode_convert_method.cpp.

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

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

◆ 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,
method_offsett  address_start,
method_offsett  address_limit,
method_offsett  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
[in,out]treeA code block descriptor.
[in,out]this_blockThe corresponding actual code_blockt.
address_startthe Java bytecode offsets searched for.
address_limitthe Java bytecode offsets searched for.
next_block_start_addressThe bytecode offset of tree/this_block's successor sibling, or UINT_MAX if none exists.
amapThe bytecode address map.
allow_mergeWhether modifying the block tree is allowed. This is always true except when called from get_block_for_pcrange.
Returns
The code_blockt most closely enclosing the given address range.

Definition at line 747 of file java_bytecode_convert_method.cpp.

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

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

◆ 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 181 of file java_bytecode_convert_method_class.h.

◆ label()

irep_idt java_bytecode_convert_methodt::label ( const irep_idt address)
staticprotected

Definition at line 165 of file java_bytecode_convert_method.cpp.

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

◆ pop()

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

Definition at line 131 of file java_bytecode_convert_method.cpp.

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

◆ push()

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

Definition at line 156 of file java_bytecode_convert_method.cpp.

◆ replace_call_to_cprover_assume()

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

Definition at line 2231 of file java_bytecode_convert_method.cpp.

◆ 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
[in,out]replA block of code in which to perform replacement.
old_labelThe label to be replaced.
new_labelThe label to replace old_label with.

Definition at line 676 of file java_bytecode_convert_method.cpp.

◆ save_stack_entries()

void java_bytecode_convert_methodt::save_stack_entries ( const std::string &  tmp_var_prefix,
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
[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 3134 of file java_bytecode_convert_method.cpp.

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

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.

Parameters
mJava method
amapMap from bytecode indices to instructions in m

Definition at line 721 of file java_local_variable_table.cpp.

◆ tmp_variable()

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

Definition at line 170 of file java_bytecode_convert_method.cpp.

◆ try_catch_handler()

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

Definition at line 2946 of file java_bytecode_convert_method.cpp.

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

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 133 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 132 of file java_bytecode_convert_method_class.h.

◆ class_hierarchy

const class_hierarchyt& java_bytecode_convert_methodt::class_hierarchy
protected

Definition at line 134 of file java_bytecode_convert_method_class.h.

◆ current_method

irep_idt java_bytecode_convert_methodt::current_method
protected

A copy of method_id :/.

Definition at line 83 of file java_bytecode_convert_method_class.h.

◆ max_array_length

const size_t java_bytecode_convert_methodt::max_array_length
protected

Definition at line 72 of file java_bytecode_convert_method_class.h.

◆ method_has_this

bool java_bytecode_convert_methodt::method_has_this
protected

Definition at line 131 of file java_bytecode_convert_method_class.h.

◆ 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 80 of file java_bytecode_convert_method_class.h.

◆ 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 87 of file java_bytecode_convert_method_class.h.

◆ needed_lazy_methods

optionalt<ci_lazy_methods_neededt> java_bytecode_convert_methodt::needed_lazy_methods
protected

Definition at line 75 of file java_bytecode_convert_method_class.h.

◆ slots_for_parameters

method_offsett 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 94 of file java_bytecode_convert_method_class.h.

◆ stack

stackt java_bytecode_convert_methodt::stack
protected

Definition at line 170 of file java_bytecode_convert_method_class.h.

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_methodt::string_preprocess
protected

Definition at line 89 of file java_bytecode_convert_method_class.h.

◆ symbol_table

symbol_table_baset& java_bytecode_convert_methodt::symbol_table
protected

Definition at line 71 of file java_bytecode_convert_method_class.h.

◆ threading_support

const bool java_bytecode_convert_methodt::threading_support
protected

Definition at line 74 of file java_bytecode_convert_method_class.h.

◆ throw_assertion_error

const bool java_bytecode_convert_methodt::throw_assertion_error
protected

Definition at line 73 of file java_bytecode_convert_method_class.h.

◆ tmp_vars

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

Definition at line 161 of file java_bytecode_convert_method_class.h.

◆ used_local_names

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

Definition at line 130 of file java_bytecode_convert_method_class.h.

◆ variables

expanding_vectort<variablest> java_bytecode_convert_methodt::variables
protected

Definition at line 129 of file java_bytecode_convert_method_class.h.


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