cprover
|
#include <ci_lazy_methods.h>
Classes | |
struct | convert_method_resultt |
Public Member Functions | |
ci_lazy_methodst (const symbol_tablet &symbol_table, const irep_idt &main_class, const std::vector< irep_idt > &main_jar_classes, const std::vector< irep_idt > &lazy_methods_extra_entry_points, java_class_loadert &java_class_loader, const std::vector< irep_idt > &extra_instantiated_classes, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler, const synthetic_methods_mapt &synthetic_methods) | |
Constructor for lazy-method loading. More... | |
bool | operator() (symbol_tablet &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter) |
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. More... | |
Private Member Functions | |
void | resolve_method_names (std::vector< irep_idt > &methods, const symbol_tablet &symbol_table) |
Translates the given list of method names from human-readable to internal syntax. More... | |
void | initialize_instantiated_classes (const std::unordered_set< irep_idt > &entry_points, const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods) |
Build up a list of methods whose type may be passed around reachable from the entry point. More... | |
void | gather_virtual_callsites (const exprt &e, std::unordered_set< exprt, irep_hash > &result) |
Get places where virtual functions are called. More... | |
void | get_virtual_method_targets (const exprt &called_function, const std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< irep_idt > &callable_methods, symbol_tablet &symbol_table) |
Find possible callees, excluding types that are not known to be instantiated. More... | |
void | gather_needed_globals (const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed) |
See output. More... | |
irep_idt | get_virtual_method_target (const std::unordered_set< irep_idt > &instantiated_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table) |
Find a virtual callee, if one is defined and the callee type is known to exist. More... | |
std::unordered_set< irep_idt > | entry_point_methods (const symbol_tablet &symbol_table) |
Entry point methods are either: More... | |
convert_method_resultt | convert_and_analyze_method (const method_convertert &method_converter, std::unordered_set< irep_idt > &methods_already_populated, const bool class_initializer_already_seen, const irep_idt &method_name, symbol_tablet &symbol_table, std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< exprt, irep_hash > &virtual_function_calls) |
Convert a method, add it to the populated set, add needed methods to methods_to_convert_later and add virtual calls from the method to virtual_function_calls. More... | |
bool | handle_virtual_methods_with_no_callees (std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, const std::unordered_set< exprt, irep_hash > &virtual_function_calls, symbol_tablet &symbol_table) |
Look for virtual callsites with no candidate targets. More... | |
Static Private Member Functions | |
static irep_idt | build_virtual_method_name (const irep_idt &class_name, const irep_idt &component_method_name) |
Private Attributes | |
class_hierarchyt | class_hierarchy |
irep_idt | main_class |
std::vector< irep_idt > | main_jar_classes |
std::vector< irep_idt > | lazy_methods_extra_entry_points |
java_class_loadert & | java_class_loader |
const std::vector< irep_idt > & | extra_instantiated_classes |
const select_pointer_typet & | pointer_type_selector |
const synthetic_methods_mapt & | synthetic_methods |
Additional Inherited Members |
Definition at line 94 of file ci_lazy_methods.h.
ci_lazy_methodst::ci_lazy_methodst | ( | const symbol_tablet & | symbol_table, |
const irep_idt & | main_class, | ||
const std::vector< irep_idt > & | main_jar_classes, | ||
const std::vector< irep_idt > & | lazy_methods_extra_entry_points, | ||
java_class_loadert & | java_class_loader, | ||
const std::vector< irep_idt > & | extra_instantiated_classes, | ||
const select_pointer_typet & | pointer_type_selector, | ||
message_handlert & | message_handler, | ||
const synthetic_methods_mapt & | synthetic_methods | ||
) |
Constructor for lazy-method loading.
symbol_table | the symbol table to use |
main_class | identifier of the entry point / main class |
main_jar_classes | specify main class of jar if main_class is empty |
lazy_methods_extra_entry_points | entry point functions to use |
java_class_loader | the Java class loader to use |
extra_instantiated_classes | list of class identifiers which are considered to be required and therefore their methods should not be removed via lazy-methods . Example of use: ArrayList as general implementation for List interface. |
pointer_type_selector | selector to handle correct pointer types |
message_handler | the message handler to use for output |
Definition at line 33 of file ci_lazy_methods.cpp.
References class_hierarchy.
|
staticprivate |
|
private |
Convert a method, add it to the populated set, add needed methods to methods_to_convert_later and add virtual calls from the method to virtual_function_calls.
Definition at line 274 of file ci_lazy_methods.cpp.
References messaget::debug(), messaget::eom(), gather_virtual_callsites(), get_java_class_literal_initializer_signature(), symbol_table_baset::has_symbol(), symbol_table_baset::lookup_ref(), pointer_type_selector, references_class_model(), messaget::result(), and symbolt::value.
Referenced by operator()().
|
private |
Entry point methods are either:
main_class
if it existsDefinition at line 324 of file ci_lazy_methods.cpp.
References dstringt::empty(), get_main_symbol(), messaget::get_message_handler(), java_class_loadert::get_original_class(), id2string(), main_function_resultt::is_success(), java_class_loader, main_class, main_function_resultt::main_function, main_jar_classes, java_bytecode_parse_treet::classt::methods, symbolt::name, and java_bytecode_parse_treet::parsed_class.
Referenced by operator()().
|
private |
See output.
e | expression tree to search | |
symbol_table | global symbol table | |
[out] | needed | Populated with global variable symbols referenced from e or its children. |
Definition at line 513 of file ci_lazy_methods.cpp.
References symbol_table_baset::add(), forall_operands, irept::id(), symbol_table_baset::symbols, and to_symbol_expr().
Referenced by operator()().
|
private |
Get places where virtual functions are called.
e | expression tree to search | |
[out] | result | filled with pointers to each function call within e that calls a virtual function. |
Definition at line 450 of file ci_lazy_methods.cpp.
References code_function_callt::function(), codet::get_statement(), irept::id(), exprt::operands(), messaget::result(), to_code(), and to_code_function_call().
Referenced by convert_and_analyze_method().
|
private |
Find a virtual callee, if one is defined and the callee type is known to exist.
instantiated_classes | set of classes that can be instantiated. Any potential callee not in this set will be ignored. |
call_basename | unqualified function name with type signature (e.g. "f:(I)") |
classname | class name that may define or override a function named call_basename . |
symbol_table | global symtab |
classname
's definition of call_basename
if found and classname
is present in instantiated_classes
, or irep_idt() otherwise. Definition at line 551 of file ci_lazy_methods.cpp.
References class_hierarchy, resolve_inherited_componentt::inherited_componentt::get_full_component_identifier(), and resolve_inherited_componentt::inherited_componentt::is_valid().
Referenced by get_virtual_method_targets(), and handle_virtual_methods_with_no_callees().
|
private |
Find possible callees, excluding types that are not known to be instantiated.
called_function | virtual function call whose concrete function calls should be determined. | |
instantiated_classes | set of classes that can be instantiated. Any potential callee not in this set will be ignored. | |
[out] | callable_methods | Populated with all possible c callees, taking instantiated_classes into account (virtual function overrides defined on classes that are not 'needed' are ignored) |
symbol_table | global symbol table |
Definition at line 479 of file ci_lazy_methods.cpp.
References class_hierarchy, dstringt::empty(), irept::get(), class_hierarchyt::get_children_trans(), get_virtual_method_target(), irept::id(), INVARIANT, and PRECONDITION.
Referenced by handle_virtual_methods_with_no_callees(), and operator()().
|
private |
Look for virtual callsites with no candidate targets.
If we have invokevirtual A.f and we don't believe either A or any of its children may exist, we assume specifically A is somehow instantiated. Note this may result in an abstract class being classified as instantiated, which stands in for some unknown concrete subclass: in this case the called method will be a stub.
Definition at line 225 of file ci_lazy_methods.cpp.
References CHECK_RETURN, dstringt::empty(), get_virtual_method_target(), and get_virtual_method_targets().
Referenced by operator()().
|
private |
Build up a list of methods whose type may be passed around reachable from the entry point.
entry_points | list of fully-qualified function names that we should assume are reachable | |
ns | global namespace | |
[out] | needed_lazy_methods | Populated with all Java reference types whose references may be passed, directly or indirectly, to any of the functions in entry_points . |
Definition at line 414 of file ci_lazy_methods.cpp.
References ci_lazy_methods_neededt::add_all_needed_classes(), ci_lazy_methods_neededt::add_needed_class(), extra_instantiated_classes, id2string(), namespacet::lookup(), to_code_type(), and to_pointer_type().
Referenced by operator()().
bool ci_lazy_methodst::operator() | ( | symbol_tablet & | symbol_table, |
method_bytecodet & | method_bytecode, | ||
const method_convertert & | method_converter | ||
) |
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point.
In brief, static methods are reachable if we find a callsite in another reachable site, while virtual methods are reachable if we find a virtual callsite targeting a compatible type and a constructor callsite indicating an object of that type may be instantiated (or evidence that an object of that type exists before the main function is entered, such as being passed as a parameter). Elaborates lazily-converted methods that may be reachable starting from the main entry point (usually provided with the –function command- line option
symbol_table | global symbol table | |
[out] | method_bytecode | map from method names to relevant symbol and parsed-method objects. |
method_converter | Function for converting methods on demand. |
Definition at line 96 of file ci_lazy_methods.cpp.
References symbol_table_baset::add(), method_bytecodet::contains_method(), convert_and_analyze_method(), messaget::debug(), entry_point_methods(), messaget::eom(), gather_needed_globals(), get_virtual_method_targets(), handle_virtual_methods_with_no_callees(), INFLIGHT_EXCEPTION_VARIABLE_NAME, initialize_instantiated_classes(), lazy_methods_extra_entry_points, symbol_table_baset::lookup_ref(), pointer_type_selector, resolve_method_names(), symbol_tablet::swap(), symbol_table_baset::symbols, and synthetic_methods.
|
private |
Translates the given list of method names from human-readable to internal syntax.
Expands any wildcards (entries ending in '.*') in the given method list to include all non-static methods defined on the given class.
[in,out] | methods | List of methods to expand. Any wildcard entries will be deleted and the expanded entries appended to the end. |
symbol_table | global symbol table |
Definition at line 365 of file ci_lazy_methods.cpp.
References has_prefix(), has_suffix(), symbol_table_baset::has_symbol(), code_typet::has_this(), id2string(), resolve_friendly_method_name(), symbol_table_baset::symbols, and to_code_type().
Referenced by operator()().
|
private |
Definition at line 149 of file ci_lazy_methods.h.
Referenced by ci_lazy_methodst(), get_virtual_method_target(), and get_virtual_method_targets().
|
private |
Definition at line 154 of file ci_lazy_methods.h.
Referenced by initialize_instantiated_classes().
|
private |
Definition at line 153 of file ci_lazy_methods.h.
Referenced by entry_point_methods().
|
private |
Definition at line 152 of file ci_lazy_methods.h.
Referenced by operator()().
|
private |
Definition at line 150 of file ci_lazy_methods.h.
Referenced by entry_point_methods().
|
private |
Definition at line 151 of file ci_lazy_methods.h.
Referenced by entry_point_methods().
|
private |
Definition at line 155 of file ci_lazy_methods.h.
Referenced by convert_and_analyze_method(), and operator()().
|
private |
Definition at line 156 of file ci_lazy_methods.h.
Referenced by operator()().