cprover
ci_lazy_methodst Class Reference

#include <ci_lazy_methods.h>

+ Inheritance diagram for ci_lazy_methodst:
+ Collaboration diagram for ci_lazy_methodst:

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

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< 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_idtentry_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_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
 

Additional Inherited Members

- 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
}
 
- 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...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 97 of file ci_lazy_methods.h.

Constructor & Destructor Documentation

◆ ci_lazy_methodst()

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< 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,
message_handlert message_handler,
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
message_handlerthe message handler to use for output
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 37 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_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 
)
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.

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 280 of file ci_lazy_methods.cpp.

◆ entry_point_methods()

std::unordered_set< irep_idt > ci_lazy_methodst::entry_point_methods ( const symbol_tablet symbol_table)
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 328 of file ci_lazy_methods.cpp.

◆ gather_needed_globals()

void ci_lazy_methodst::gather_needed_globals ( const exprt e,
const symbol_tablet symbol_table,
symbol_tablet 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 468 of file ci_lazy_methods.cpp.

◆ gather_virtual_callsites()

void ci_lazy_methodst::gather_virtual_callsites ( const exprt e,
std::unordered_set< 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 405 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_tablet 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 506 of file ci_lazy_methods.cpp.

◆ get_virtual_method_targets()

void ci_lazy_methodst::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 
)
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 434 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< exprt, irep_hash > &  virtual_function_calls,
symbol_tablet 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 231 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 370 of file ci_lazy_methods.cpp.

◆ 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

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.
Returns
Returns false on success

Definition at line 100 of file ci_lazy_methods.cpp.

Member Data Documentation

◆ class_hierarchy

class_hierarchyt ci_lazy_methodst::class_hierarchy
private

Definition at line 148 of file ci_lazy_methods.h.

◆ extra_instantiated_classes

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

Definition at line 153 of file ci_lazy_methods.h.

◆ java_class_loader

java_class_loadert& ci_lazy_methodst::java_class_loader
private

Definition at line 152 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 151 of file ci_lazy_methods.h.

◆ main_class

irep_idt ci_lazy_methodst::main_class
private

Definition at line 149 of file ci_lazy_methods.h.

◆ main_jar_classes

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

Definition at line 150 of file ci_lazy_methods.h.

◆ pointer_type_selector

const select_pointer_typet& ci_lazy_methodst::pointer_type_selector
private

Definition at line 154 of file ci_lazy_methods.h.

◆ synthetic_methods

const synthetic_methods_mapt& ci_lazy_methodst::synthetic_methods
private

Definition at line 155 of file ci_lazy_methods.h.


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