cprover
|
#include <java_bytecode_convert_method_class.h>
Classes | |
struct | block_tree_nodet |
struct | converted_instructiont |
struct | holet |
struct | local_variable_with_holest |
class | variablet |
Public Types | |
typedef java_bytecode_parse_treet::methodt | methodt |
typedef java_bytecode_parse_treet::instructiont | instructiont |
typedef methodt::instructionst | instructionst |
typedef methodt::local_variable_tablet | local_variable_tablet |
typedef methodt::local_variablet | local_variablet |
typedef uint16_t | method_offsett |
typedef std::vector< local_variable_with_holest > | local_variable_table_with_holest |
typedef std::map< method_offsett, converted_instructiont > | address_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 Member Functions | |
java_bytecode_convert_methodt (symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support) | |
void | operator() (const symbolt &class_symbol, const methodt &method) |
Protected Types | |
enum | instruction_sizet { INST_INDEX = 2, INST_INDEX_CONST = 3 } |
enum | variable_cast_argumentt { CAST_AS_NEEDED, NO_CAST } |
enum | bytecode_write_typet { bytecode_write_typet::VARIABLE, bytecode_write_typet::ARRAY_REF, bytecode_write_typet::STATIC_FIELD, bytecode_write_typet::FIELD } |
typedef std::vector< variablet > | variablest |
typedef std::vector< exprt > | stackt |
Protected Member Functions | |
const variablet & | find_variable_for_slot (size_t address, variablest &var_list) |
See above. More... | |
exprt | variable (const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast) |
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 . More... | |
symbol_exprt | tmp_variable (const std::string &prefix, const typet &type) |
exprt::operandst | pop (std::size_t n) |
void | pop_residue (std::size_t n) |
removes minimum(n, stack.size()) elements from the stack More... | |
void | push (const exprt::operandst &o) |
bool | is_parameter (const local_variablet &v) |
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a parameter of that method. More... | |
void | find_initializers (local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms) |
See find_initializers_for_slot above for more detail. More... | |
void | find_initializers_for_slot (local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms) |
Given a sequence of users of the same local variable slot, this figures out which ones are related by control flow, and combines them into a single entry with holes, such that after combination we can create a single GOTO variable per variable table entry, placed at the live range's start address, which may be moved back so that the declaration dominates all uses. More... | |
void | setup_local_variables (const methodt &m, const address_mapt &amap) |
See find_initializers_for_slot above for more detail. More... | |
code_blockt & | get_block_for_pcrange (block_tree_nodet &tree, code_blockt &this_block, 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_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. More... | |
optionalt< symbolt > | get_lambda_method_symbol (const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index) |
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method). More... | |
void | convert (const symbolt &class_symbol, const methodt &) |
code_blockt | convert_instructions (const methodt &, const java_class_typet::java_lambda_method_handlest &) |
const bytecode_infot & | get_bytecode_info (const irep_idt &statement) |
codet | get_clinit_call (const irep_idt &classname) |
Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check. More... | |
bool | is_method_inherited (const irep_idt &classname, const irep_idt &methodid) const |
Returns true iff method methodid from class classname is a method inherited from a class (and not an interface!) from which classname inherits, either directly or indirectly. More... | |
irep_idt | get_static_field (const irep_idt &class_identifier, const irep_idt &component_name) const |
Get static field identifier referred to by class_identifier.component_name Note this may be inherited from either a parent or an interface. More... | |
void | save_stack_entries (const std::string &, 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_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 |
optionalt< exprt > | convert_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::operandst & | convert_ushr (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const |
exprt::operandst & | convert_cmp (const exprt::operandst &op, exprt::operandst &results) const |
exprt::operandst & | convert_cmp2 (const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const |
void | convert_getstatic (const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results) |
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) |
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, exprt &arg0, codet &c, exprt::operandst &results) |
exprt::operandst & | convert_const (const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const |
void | convert_dup2_x2 (exprt::operandst &op, exprt::operandst &results) |
void | convert_dup2_x1 (exprt::operandst &op, exprt::operandst &results) |
void | convert_dup2 (exprt::operandst &op, exprt::operandst &results) |
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_baset & | symbol_table |
const size_t | max_array_length |
const bool | throw_assertion_error |
const bool | threading_support |
optionalt< ci_lazy_methods_neededt > | needed_lazy_methods |
irep_idt | method_id |
Fully qualified name of the method under translation. More... | |
irep_idt | current_method |
A copy of method_id :/. More... | |
typet | method_return_type |
Return type of the method under conversion. More... | |
java_string_library_preprocesst & | string_preprocess |
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< 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 |
Additional Inherited Members |
Definition at line 32 of file java_bytecode_convert_method_class.h.
typedef std::map<method_offsett, converted_instructiont> java_bytecode_convert_methodt::address_mapt |
Definition at line 204 of file java_bytecode_convert_method_class.h.
Definition at line 59 of file java_bytecode_convert_method_class.h.
Definition at line 58 of file java_bytecode_convert_method_class.h.
typedef cfg_dominators_templatet<method_with_amapt, method_offsett, false> java_bytecode_convert_methodt::java_cfg_dominatorst |
Definition at line 207 of file java_bytecode_convert_method_class.h.
typedef std::vector<local_variable_with_holest> java_bytecode_convert_methodt::local_variable_table_with_holest |
Definition at line 111 of file java_bytecode_convert_method_class.h.
Definition at line 60 of file java_bytecode_convert_method_class.h.
Definition at line 61 of file java_bytecode_convert_method_class.h.
typedef uint16_t java_bytecode_convert_methodt::method_offsett |
Definition at line 68 of file java_bytecode_convert_method_class.h.
typedef std::pair<const methodt &, const address_mapt &> java_bytecode_convert_methodt::method_with_amapt |
Definition at line 205 of file java_bytecode_convert_method_class.h.
Definition at line 57 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 169 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 128 of file java_bytecode_convert_method_class.h.
|
strongprotected |
Enumerator | |
---|---|
VARIABLE | |
ARRAY_REF | |
STATIC_FIELD | |
FIELD |
Definition at line 286 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
INST_INDEX | |
INST_INDEX_CONST |
Definition at line 136 of file java_bytecode_convert_method_class.h.
|
protected |
Enumerator | |
---|---|
CAST_AS_NEEDED | |
NO_CAST |
Definition at line 148 of file java_bytecode_convert_method_class.h.
|
inline |
Definition at line 35 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 431 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2826 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2874 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2265 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2249 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2633 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2605 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2039 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 1992 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2005 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2018 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2562 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2746 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2770 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2724 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2702 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2676 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 991 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2074 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2906 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 1969 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2409 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2493 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2437 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 1902 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2548 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2517 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2794 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2847 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 1918 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2653 of file java_bytecode_convert_method.cpp.
|
protected |
actually create a temporary variable to hold the value of a stack entry
Definition at line 3231 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2304 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2944 of file java_bytecode_convert_method.cpp.
|
protected |
See find_initializers_for_slot
above for more detail.
Combines entries in vars
which flow together.
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 672 of file java_local_variable_table.cpp.
|
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).
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 575 of file java_local_variable_table.cpp.
|
protected |
See above.
address | Address to find a variable table entry for |
var_list | List of candidates that use the slot we're interested in |
address
. Definition at line 839 of file java_local_variable_table.cpp.
|
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.
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. |
Definition at line 711 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 626 of file java_bytecode_convert_method.cpp.
Each static access to classname should be prefixed with a check for necessary static init; this returns a call implementing that check.
classname | Class name |
Definition at line 969 of file java_bytecode_convert_method.cpp.
|
protected |
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).
lambda_method_handles | Vector of lambda method handles (bootstrap methods) of the class where the lambda is called |
index | Index of the lambda method handle in the vector |
Definition at line 316 of file java_bytecode_convert_method.cpp.
|
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).
[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 . |
Definition at line 748 of file java_bytecode_convert_method.cpp.
|
protected |
Get static field identifier referred to by class_identifier.component_name
Note this may be inherited from either a parent or an interface.
class_identifier | class used to refer to the field |
component_name | component (static field) name |
Definition at line 3125 of file java_bytecode_convert_method.cpp.
|
protected |
Returns true iff method methodid
from class classname
is a method inherited from a class (and not an interface!) from which classname
inherits, either directly or indirectly.
classname | class whose method is referenced |
methodid | method basename |
Definition at line 3106 of file java_bytecode_convert_method.cpp.
|
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.
Definition at line 165 of file java_bytecode_convert_method.cpp.
|
inline |
Definition at line 63 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 131 of file java_bytecode_convert_method.cpp.
|
protected |
removes minimum(n, stack.size()) elements from the stack
Definition at line 149 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 156 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2234 of file java_bytecode_convert_method.cpp.
|
staticprotected |
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
[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 677 of file java_bytecode_convert_method.cpp.
|
protected |
Create temporary variables if a write instruction can have undesired side- effects.
tmp_var_prefix | The prefix string to use for new temporary variables | |
[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 3149 of file java_bytecode_convert_method.cpp.
|
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.
m | Java method |
amap | Map from bytecode indices to instructions in m |
Definition at line 721 of file java_local_variable_table.cpp.
|
protected |
Definition at line 170 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 2961 of file java_bytecode_convert_method.cpp.
|
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
.
arg | The local variable slot |
type_char | The type of the value stored in the slot pointed by arg . |
address | Bytecode address used to find a variable that the LVT declares to be live and living in the slot pointed by arg for this bytecode. |
do_cast | Indicates whether we should return the original symbol_exprt or a typecast_exprt if the type of the symbol_exprt does not equal that represented by type_char . |
Definition at line 208 of file java_bytecode_convert_method.cpp.
|
protected |
Definition at line 133 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 132 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 134 of file java_bytecode_convert_method_class.h.
|
protected |
A copy of method_id
:/.
Definition at line 83 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 72 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 131 of file java_bytecode_convert_method_class.h.
|
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.
|
protected |
Return type of the method under conversion.
Initialized by convert
.
Definition at line 87 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 75 of file java_bytecode_convert_method_class.h.
|
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.
|
protected |
Definition at line 170 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 89 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 71 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 74 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 73 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 161 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 130 of file java_bytecode_convert_method_class.h.
|
protected |
Definition at line 129 of file java_bytecode_convert_method_class.h.