Returns an expression 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.

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

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.

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.

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.

void setup_local_variables (const methodt &m, const address_mapt &amap)

See find_initializers_for_slot above for more detail.

code_blockt & 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)

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

code_blockt & 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)

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.

void convert (const symbolt &class_symbol, const methodt &, const std::optional< prefix_filtert > &method_context)

code_blockt convert_parameter_annotations (const methodt &method, const java_method_typet &method_type)

code_blockt convert_instructions (const methodt &)

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.

bool is_method_inherited (const irep_idt &classname, const irep_idt &mangled_method_name) const

Returns true iff method methodid from class classname is a method inherited from a class or interface from which classname inherits, either directly or indirectly.

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.

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.

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

std::vector< method_offsett > try_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

std::optional< exprt > convert_invoke_dynamic (const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code)

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_load (const exprt &index, char type_char, size_t address)

Load reference from local variable.

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 u1 bytecode, 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::operandst & convert_shl (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const

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 source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)

code_blockt convert_putfield (const fieldref_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)

codet & do_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)

codet & replace_call_to_cprover_assume (source_locationt location, codet &c)

void convert_invoke (source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results)

exprt::operandst & convert_const (const irep_idt &statement, const constant_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'.

static exprt convert_aload (const irep_idt &statement, const exprt::operandst &op)

Protected Attributes

messaget log

symbol_table_baset & symbol_table

namespacet ns

const size_t max_array_length

const bool throw_assertion_error

const bool assert_no_exceptions_thrown

const bool threading_support

std::optional< ci_lazy_methods_neededt > needed_lazy_methods

irep_idt method_id

Fully qualified name of the method under translation.

irep_idt current_method

A copy of method_id :/.

typet method_return_type

Return type of the method under conversion.

java_string_library_preprocesst & string_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.

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

const class_hierarchyt & class_hierarchy

std::list< symbol_exprt > tmp_vars

stackt stack

Friends

class java_bytecode_convert_method_unit_testt

Detailed Description

Definition at line 35 of file java_bytecode_convert_method_class.h.

Member Typedef Documentation

◆ address_mapt

typedef std::map<method_offsett, converted_instructiont> java_bytecode_convert_methodt::address_mapt

Definition at line 242 of file java_bytecode_convert_method_class.h.

◆ instructionst

typedef methodt::instructionst java_bytecode_convert_methodt::instructionst

Definition at line 65 of file java_bytecode_convert_method_class.h.

◆ instructiont

typedef java_bytecode_parse_treet::instructiont java_bytecode_convert_methodt::instructiont

Definition at line 64 of file java_bytecode_convert_method_class.h.

◆ java_cfg_dominatorst

typedef cfg_dominators_templatet<method_with_amapt, method_offsett, false> java_bytecode_convert_methodt::java_cfg_dominatorst

Definition at line 261 of file java_bytecode_convert_method_class.h.

◆ local_variable_table_with_holest

typedef std::vector<local_variable_with_holest> java_bytecode_convert_methodt::local_variable_table_with_holest

Definition at line 123 of file java_bytecode_convert_method_class.h.

◆ local_variable_tablet

typedef methodt::local_variable_tablet java_bytecode_convert_methodt::local_variable_tablet

Definition at line 66 of file java_bytecode_convert_method_class.h.

◆ local_variablet

typedef methodt::local_variablet java_bytecode_convert_methodt::local_variablet

Definition at line 67 of file java_bytecode_convert_method_class.h.

◆ method_offsett

typedef uint16_t java_bytecode_convert_methodt::method_offsett

Definition at line 77 of file java_bytecode_convert_method_class.h.

◆ methodt

typedef java_bytecode_parse_treet::methodt java_bytecode_convert_methodt::methodt

Definition at line 63 of file java_bytecode_convert_method_class.h.

◆ stackt

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

protected

Definition at line 207 of file java_bytecode_convert_method_class.h.

◆ variablest

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

protected

Definition at line 170 of file java_bytecode_convert_method_class.h.

Member Enumeration Documentation

◆ bytecode_write_typet

enum class java_bytecode_convert_methodt::bytecode_write_typet

strongprotected

Enumerator
VARIABLE
ARRAY_REF
STATIC_FIELD
FIELD

Definition at line 339 of file java_bytecode_convert_method_class.h.

◆ instruction_sizet

enum java_bytecode_convert_methodt::instruction_sizet

protected

Enumerator
INST_INDEX
INST_INDEX_CONST

Definition at line 178 of file java_bytecode_convert_method_class.h.

◆ variable_cast_argumentt

enum java_bytecode_convert_methodt::variable_cast_argumentt

protected

Enumerator
CAST_AS_NEEDED
NO_CAST

Definition at line 190 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,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods,

java_string_library_preprocesst & _string_preprocess,

const class_hierarchyt & class_hierarchy,

bool threading_support,

bool assert_no_exceptions_thrown

)

inline

Definition at line 38 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,

const std::optional< prefix_filtert > & method_context

)

protected

Definition at line 534 of file java_bytecode_convert_method.cpp.

◆ convert_aload()

exprt java_bytecode_convert_methodt::convert_aload ( const irep_idt & statement,

const exprt::operandst & op

)

staticprotected

Definition at line 2993 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 3059 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 2423 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 2407 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 2767 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 2739 of file java_bytecode_convert_method.cpp.

◆ convert_const()

exprt::operandst & java_bytecode_convert_methodt::convert_const ( const irep_idt & statement,

const constant_exprt & arg0,

exprt::operandst & results

) const

protected

Definition at line 2169 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 2122 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 2135 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 2148 of file java_bytecode_convert_method.cpp.

◆ convert_getstatic()

void java_bytecode_convert_methodt::convert_getstatic ( const source_locationt & source_location,

const exprt & arg0,

const symbol_exprt & symbol_expr,

bool is_assertions_disabled_field,

codet & c,

exprt::operandst & results

)

protected

Definition at line 2693 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 2896 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 u1 bytecode,

const exprt::operandst & op,

const mp_integer & number,

const source_locationt & location

) const

protected

Definition at line 2920 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 2874 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 2852 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 2823 of file java_bytecode_convert_method.cpp.

◆ convert_instructions()

code_blockt java_bytecode_convert_methodt::convert_instructions ( const methodt & method )

protected

Definition at line 1055 of file java_bytecode_convert_method.cpp.

◆ convert_invoke()

void java_bytecode_convert_methodt::convert_invoke ( source_locationt location,

const irep_idt & statement,

class_method_descriptor_exprt & class_method_descriptor,

codet & c,

exprt::operandst & results

)

protected

Definition at line 2231 of file java_bytecode_convert_method.cpp.

◆ convert_invoke_dynamic()

std::optional< exprt > java_bytecode_convert_methodt::convert_invoke_dynamic ( const source_locationt & location,

std::size_t instruction_address,

const exprt & arg0,

codet & result_code

)

protected

Definition at line 3089 of file java_bytecode_convert_method.cpp.

◆ convert_load()

exprt java_bytecode_convert_methodt::convert_load ( const exprt & index,

char type_char,

size_t address

)

protected

Load reference from local variable.

index must be an unsigned byte and an index in the local variable array of the current frame. The type of the local variable at index index must:

be a reference type if type_char is 'a'
be either boolean, byte, short, int, or char if type_char is 'i', a typecast to int is added if needed
match java_type_of_char(type_char) otherwise
Returns
the local variable at index

Definition at line 3013 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 2099 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 2542 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 2627 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 2569 of file java_bytecode_convert_method.cpp.

◆ convert_parameter_annotations()

code_blockt java_bytecode_convert_methodt::convert_parameter_annotations ( const methodt & method,

const java_method_typet & method_type

)

protected

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

◆ convert_putfield()

code_blockt java_bytecode_convert_methodt::convert_putfield ( const fieldref_exprt & arg0,

const exprt::operandst & op

)

protected

Definition at line 2682 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 2651 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 2944 of file java_bytecode_convert_method.cpp.

◆ convert_shl()

exprt::operandst & java_bytecode_convert_methodt::convert_shl ( const irep_idt & statement,

const exprt::operandst & op,

exprt::operandst & results

) const

protected

Definition at line 2787 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 3034 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 2049 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 2804 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 3431 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 2461 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 3160 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: vars Local variable table

amap Map from bytecode index to instruction

dominator_analysis Already computed dominator tree for the Java function described by amap

Definition at line 691 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: firstvar start of sequence of variable table entries, all of which should concern the same slot index.

varlimit end of sequence of variable table entries

amap map from bytecode address to instruction

dominator_analysis already-calculated dominator tree

Definition at line 597 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: 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 852 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: tree A code block descriptor.

this_block The corresponding actual code_blockt.

address_start the Java bytecode offsets searched for.

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 729 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: classname Class 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 984 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] tree A code block descriptor.

[in,out] this_block The corresponding actual code_blockt.

address_start the Java bytecode offsets searched for.

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.

amap The bytecode address map.

allow_merge Whether 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 766 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_identifier class used to refer to the field

component_name component (static field) name

Returns: identifier of the actual concrete field referred to

Definition at line 3330 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 & mangled_method_name

) const

protected

Returns true iff method methodid from class classname is a method inherited from a class or interface from which classname inherits, either directly or indirectly.

Parameters: classname class whose method is referenced

mangled_method_name The particular overload of a given method.

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

◆ label()

irep_idt java_bytecode_convert_methodt::label ( const irep_idt & address )

staticprotected

Definition at line 158 of file java_bytecode_convert_method.cpp.

◆ operator()()

void java_bytecode_convert_methodt::operator() ( const symbolt & class_symbol,

const methodt & method,

const std::optional< prefix_filtert > & method_context

)

inline

Definition at line 69 of file java_bytecode_convert_method_class.h.

◆ pop()

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

protected

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

◆ push()

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

protected

Definition at line 149 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 2392 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] repl A block of code in which to perform replacement.

old_label The label to be replaced.

new_label The label to replace old_label with.

Definition at line 695 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_prefix The prefix string to use for new temporary variables

[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 3349 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: m Java method

amap Map from bytecode indices to instructions in m

Definition at line 740 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 163 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 3177 of file java_bytecode_convert_method.cpp.

◆ variable()

exprt java_bytecode_convert_methodt::variable ( const exprt & arg,

char type_char,

size_t address

)

protected

Returns an expression 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: arg The local variable slot

type_char The type of the value stored in the slot pointed to by arg, this is only used in the case where a new unnamed local variable is created

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

Returns: symbol_exprt or type-cast symbol_exprt

Definition at line 196 of file java_bytecode_convert_method.cpp.

Friends And Related Symbol Documentation

◆ java_bytecode_convert_method_unit_testt

friend class java_bytecode_convert_method_unit_testt

friend

Definition at line 545 of file java_bytecode_convert_method_class.h.

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

◆ assert_no_exceptions_thrown

const bool java_bytecode_convert_methodt::assert_no_exceptions_thrown

protected

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

◆ class_hierarchy

const class_hierarchyt& java_bytecode_convert_methodt::class_hierarchy

protected

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

◆ log

messaget java_bytecode_convert_methodt::log

protected

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

◆ method_has_this

bool java_bytecode_convert_methodt::method_has_this

protected

Definition at line 173 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 92 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 99 of file java_bytecode_convert_method_class.h.

◆ needed_lazy_methods

std::optional<ci_lazy_methods_neededt> java_bytecode_convert_methodt::needed_lazy_methods

protected

Definition at line 87 of file java_bytecode_convert_method_class.h.

◆ ns

namespacet java_bytecode_convert_methodt::ns

protected

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

◆ stack

stackt java_bytecode_convert_methodt::stack

protected

Definition at line 208 of file java_bytecode_convert_method_class.h.

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_methodt::string_preprocess

protected

Definition at line 101 of file java_bytecode_convert_method_class.h.

◆ symbol_table

symbol_table_baset& java_bytecode_convert_methodt::symbol_table

protected

Definition at line 81 of file java_bytecode_convert_method_class.h.

◆ threading_support

const bool java_bytecode_convert_methodt::threading_support

protected

Definition at line 86 of file java_bytecode_convert_method_class.h.

◆ throw_assertion_error

const bool java_bytecode_convert_methodt::throw_assertion_error

protected

Definition at line 84 of file java_bytecode_convert_method_class.h.

◆ tmp_vars

std::list<symbol_exprt> java_bytecode_convert_methodt::tmp_vars

protected

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

◆ variables

expanding_vectort<variablest> java_bytecode_convert_methodt::variables

protected

Definition at line 171 of file java_bytecode_convert_method_class.h.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_local_variable_table.cpp

java_bytecode_convert_methodt
Generated by doxygen 1.9.8