CBMC
ci_lazy_methodst Class Reference

#include <ci_lazy_methods.h>

+ Collaboration diagram for ci_lazy_methodst:

Classes

struct  convert_method_resultt
 

Public Member Functions

 ci_lazy_methodst (const symbol_table_baset &symbol_table, const irep_idt &main_class, const std::vector< irep_idt > &main_jar_classes, const std::vector< load_extra_methodst > &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)
 Constructor for lazy-method loading. More...
 
bool operator() (symbol_table_baset &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter, message_handlert &message_handler)
 Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. More...
 

Private Member Functions

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< class_method_descriptor_exprt, irep_hash > &result)
 Get places where virtual functions are called. More...
 
void get_virtual_method_targets (const class_method_descriptor_exprt &called_function, const std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< irep_idt > &callable_methods, symbol_table_baset &symbol_table)
 Find possible callees, excluding types that are not known to be instantiated. More...
 
void gather_needed_globals (const exprt &e, const symbol_table_baset &symbol_table, symbol_table_baset &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_table_baset &symbol_table)
 Find a virtual callee, if one is defined and the callee type is known to exist. More...
 
std::unordered_set< irep_idtentry_point_methods (const symbol_table_baset &symbol_table, message_handlert &message_handler)
 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_table_baset &symbol_table, std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< class_method_descriptor_exprt, irep_hash > &called_virtual_functions, message_handlert &message_handler)
 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_functions. 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< class_method_descriptor_exprt, irep_hash > &virtual_functions, symbol_table_baset &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_idtmain_jar_classes
 
const std::vector< load_extra_methodst > & lazy_methods_extra_entry_points
 
java_class_loadertjava_class_loader
 
const std::vector< irep_idt > & extra_instantiated_classes
 
const select_pointer_typetpointer_type_selector
 
const synthetic_methods_maptsynthetic_methods
 

Detailed Description

Definition at line 98 of file ci_lazy_methods.h.

Constructor & Destructor Documentation

◆ ci_lazy_methodst()

ci_lazy_methodst::ci_lazy_methodst ( const symbol_table_baset symbol_table,
const irep_idt main_class,
const std::vector< irep_idt > &  main_jar_classes,
const std::vector< load_extra_methodst > &  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 
)

Constructor for lazy-method loading.

Parameters
symbol_tablethe symbol table to use
main_classidentifier of the entry point / main class
main_jar_classesspecify main class of jar if main_class is empty
lazy_methods_extra_entry_pointsentry point functions to use
java_class_loaderthe Java class loader to use
extra_instantiated_classeslist 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_selectorselector to handle correct pointer types
synthetic_methodsmap from synthetic method names to the type of synthetic method (e.g. stub class static initialiser). Indicates that these method bodies are produced internally, rather than generated from Java bytecode.

Definition at line 39 of file ci_lazy_methods.cpp.

Member Function Documentation

◆ build_virtual_method_name()

static irep_idt ci_lazy_methodst::build_virtual_method_name ( const irep_idt class_name,
const irep_idt component_method_name 
)
staticprivate

◆ convert_and_analyze_method()

ci_lazy_methodst::convert_method_resultt ci_lazy_methodst::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_table_baset symbol_table,
std::unordered_set< irep_idt > &  methods_to_convert_later,
std::unordered_set< irep_idt > &  instantiated_classes,
std::unordered_set< class_method_descriptor_exprt, irep_hash > &  called_virtual_functions,
message_handlert message_handler 
)
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_functions.

Returns
structure containing two Booleans:
  • class_initializer_seen which is true if the class_initializer_seen argument was false and the class_model is referenced in the body of the method
  • new_method_seen if the method was not converted before and was converted successfully here

Definition at line 331 of file ci_lazy_methods.cpp.

◆ entry_point_methods()

std::unordered_set< irep_idt > ci_lazy_methodst::entry_point_methods ( const symbol_table_baset symbol_table,
message_handlert message_handler 
)
private

Entry point methods are either:

  • the "main" function of the main_class if it exists
  • all the methods of the main class if it is not empty
  • all the methods of the main jar file
    Returns
    set of identifiers of entry point methods

Definition at line 381 of file ci_lazy_methods.cpp.

◆ gather_needed_globals()

void ci_lazy_methodst::gather_needed_globals ( const exprt e,
const symbol_table_baset symbol_table,
symbol_table_baset needed 
)
private

See output.

Parameters
eexpression tree to search
symbol_tableglobal symbol table
[out]neededPopulated with global variable symbols referenced from e or its children.

Definition at line 519 of file ci_lazy_methods.cpp.

◆ gather_virtual_callsites()

void ci_lazy_methodst::gather_virtual_callsites ( const exprt e,
std::unordered_set< class_method_descriptor_exprt, irep_hash > &  result 
)
private

Get places where virtual functions are called.

Parameters
eexpression tree to search
[out]resultfilled with pointers to each function call within e that calls a virtual function.

Definition at line 460 of file ci_lazy_methods.cpp.

◆ get_virtual_method_target()

irep_idt ci_lazy_methodst::get_virtual_method_target ( const std::unordered_set< irep_idt > &  instantiated_classes,
const irep_idt call_basename,
const irep_idt classname,
const symbol_table_baset symbol_table 
)
private

Find a virtual callee, if one is defined and the callee type is known to exist.

Parameters
instantiated_classesset of classes that can be instantiated. Any potential callee not in this set will be ignored.
call_basenameunqualified function name with type signature (e.g. "f:(I)")
classnameclass name that may define or override a function named call_basename.
symbol_tableglobal symtab
Returns
Returns the fully qualified name of classname's definition of call_basename if found and classname is present in instantiated_classes, or irep_idt() otherwise.

Definition at line 559 of file ci_lazy_methods.cpp.

◆ get_virtual_method_targets()

void ci_lazy_methodst::get_virtual_method_targets ( const class_method_descriptor_exprt called_function,
const std::unordered_set< irep_idt > &  instantiated_classes,
std::unordered_set< irep_idt > &  callable_methods,
symbol_table_baset symbol_table 
)
private

Find possible callees, excluding types that are not known to be instantiated.

Parameters
called_functionvirtual function call whose concrete function calls should be determined.
instantiated_classesset of classes that can be instantiated. Any potential callee not in this set will be ignored.
[out]callable_methodsPopulated with all possible c callees, taking instantiated_classes into account (virtual function overrides defined on classes that are not 'needed' are ignored)
symbol_tableglobal symbol table

Definition at line 492 of file ci_lazy_methods.cpp.

◆ handle_virtual_methods_with_no_callees()

bool ci_lazy_methodst::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< class_method_descriptor_exprt, irep_hash > &  virtual_functions,
symbol_table_baset symbol_table 
)
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.

Returns
whether a new class was encountered

Definition at line 248 of file ci_lazy_methods.cpp.

◆ initialize_instantiated_classes()

void ci_lazy_methodst::initialize_instantiated_classes ( const std::unordered_set< irep_idt > &  entry_points,
const namespacet ns,
ci_lazy_methods_neededt needed_lazy_methods 
)
private

Build up a list of methods whose type may be passed around reachable from the entry point.

Parameters
entry_pointslist of fully-qualified function names that we should assume are reachable
nsglobal namespace
[out]needed_lazy_methodsPopulated with all Java reference types whose references may be passed, directly or indirectly, to any of the functions in entry_points.

Definition at line 425 of file ci_lazy_methods.cpp.

◆ operator()()

bool ci_lazy_methodst::operator() ( symbol_table_baset symbol_table,
method_bytecodet method_bytecode,
const method_convertert method_converter,
message_handlert message_handler 
)

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

Parameters
symbol_tableglobal symbol table
[out]method_bytecodemap from method names to relevant symbol and parsed-method objects.
method_converterFunction for converting methods on demand.
message_handlerthe message handler to use for output
Returns
Returns false on success

Definition at line 101 of file ci_lazy_methods.cpp.

Member Data Documentation

◆ class_hierarchy

class_hierarchyt ci_lazy_methodst::class_hierarchy
private

Definition at line 149 of file ci_lazy_methods.h.

◆ extra_instantiated_classes

const std::vector<irep_idt>& ci_lazy_methodst::extra_instantiated_classes
private

Definition at line 154 of file ci_lazy_methods.h.

◆ java_class_loader

java_class_loadert& ci_lazy_methodst::java_class_loader
private

Definition at line 153 of file ci_lazy_methods.h.

◆ lazy_methods_extra_entry_points

const std::vector<load_extra_methodst>& ci_lazy_methodst::lazy_methods_extra_entry_points
private

Definition at line 152 of file ci_lazy_methods.h.

◆ main_class

irep_idt ci_lazy_methodst::main_class
private

Definition at line 150 of file ci_lazy_methods.h.

◆ main_jar_classes

std::vector<irep_idt> ci_lazy_methodst::main_jar_classes
private

Definition at line 151 of file ci_lazy_methods.h.

◆ pointer_type_selector

const select_pointer_typet& ci_lazy_methodst::pointer_type_selector
private

Definition at line 155 of file ci_lazy_methods.h.

◆ synthetic_methods

const synthetic_methods_mapt& ci_lazy_methodst::synthetic_methods
private

Definition at line 156 of file ci_lazy_methods.h.


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