cprover
ci_lazy_methods_neededt Class Reference

#include <ci_lazy_methods_needed.h>

+ Collaboration diagram for ci_lazy_methods_neededt:

Public Member Functions

 ci_lazy_methods_neededt (std::unordered_set< irep_idt > &_callable_methods, std::unordered_set< irep_idt > &_instantiated_classes, symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector)
 
void add_needed_method (const irep_idt &)
 Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborated. More...
 
bool add_needed_class (const irep_idt &)
 Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accessed. More...
 
void add_all_needed_classes (const pointer_typet &pointer_type)
 Add to the needed classes all classes specified, the replacement type if it will be replaced, and all fields it contains. More...
 

Private Member Functions

void add_clinit_call (const irep_idt &class_id, const symbol_tablet &symbol_table)
 For a given class id, note that its static initializer is needed. More...
 
void initialize_instantiated_classes_from_pointer (const pointer_typet &pointer_type, const namespacet &ns)
 Build up list of methods for types for a specific pointer type. More...
 
void gather_field_types (const typet &class_type, const namespacet &ns)
 For a given type, gather all fields referenced by that type. More...
 

Private Attributes

std::unordered_set< irep_idt > & callable_methods
 
std::unordered_set< irep_idt > & instantiated_classes
 
symbol_tabletsymbol_table
 
const select_pointer_typetpointer_type_selector
 

Detailed Description

Definition at line 24 of file ci_lazy_methods_needed.h.

Constructor & Destructor Documentation

◆ ci_lazy_methods_neededt()

ci_lazy_methods_neededt::ci_lazy_methods_neededt ( std::unordered_set< irep_idt > &  _callable_methods,
std::unordered_set< irep_idt > &  _instantiated_classes,
symbol_tablet _symbol_table,
const select_pointer_typet pointer_type_selector 
)
inline

Definition at line 27 of file ci_lazy_methods_needed.h.

Member Function Documentation

◆ add_all_needed_classes()

void ci_lazy_methods_neededt::add_all_needed_classes ( const pointer_typet pointer_type)

Add to the needed classes all classes specified, the replacement type if it will be replaced, and all fields it contains.

Parameters
pointer_typeThe type to add

Definition at line 78 of file ci_lazy_methods_needed.cpp.

◆ add_clinit_call()

void ci_lazy_methods_neededt::add_clinit_call ( const irep_idt class_id,
const symbol_tablet symbol_table 
)
private

For a given class id, note that its static initializer is needed.

This applies the same logic to the given class that java_bytecode_convert_methodt::get_clinit_call applies e.g. to classes whose constructor we call in a method body. This duplication is unavoidable because ci_lazy_methods essentially has to go through the same logic as __CPROVER_start in its initial setup, and because return values of opaque methods need to be considered in ci_lazy_methods too.

Parameters
class_idThe given class id
symbol_tableUsed to look up occurrences of static initializers

Definition at line 38 of file ci_lazy_methods_needed.cpp.

◆ add_needed_class()

bool ci_lazy_methods_neededt::add_needed_class ( const irep_idt class_symbol_name)

Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accessed.

Also notes that its static initializer is therefore reachable.

Parameters
class_symbol_name: class name; must exist in symbol table.
Returns
Returns true if class_symbol_name is new (not seen before).

Definition at line 52 of file ci_lazy_methods_needed.cpp.

◆ add_needed_method()

void ci_lazy_methods_neededt::add_needed_method ( const irep_idt method_symbol_name)

Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborated.

Parameters
method_symbol_name: method name; must exist in symbol table.

Definition at line 23 of file ci_lazy_methods_needed.cpp.

◆ gather_field_types()

void ci_lazy_methods_neededt::gather_field_types ( const typet class_type,
const namespacet ns 
)
private

For a given type, gather all fields referenced by that type.

Parameters
class_typeroot of class tree to search
nsglobal namespaces.

Definition at line 133 of file ci_lazy_methods_needed.cpp.

◆ initialize_instantiated_classes_from_pointer()

void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer ( const pointer_typet pointer_type,
const namespacet ns 
)
private

Build up list of methods for types for a specific pointer type.

See add_all_needed_classes for more details.

Parameters
pointer_typeThe type to gather methods for.
nsglobal namespace

Definition at line 100 of file ci_lazy_methods_needed.cpp.

Member Data Documentation

◆ callable_methods

std::unordered_set<irep_idt>& ci_lazy_methods_neededt::callable_methods
private

Definition at line 50 of file ci_lazy_methods_needed.h.

◆ instantiated_classes

std::unordered_set<irep_idt>& ci_lazy_methods_neededt::instantiated_classes
private

Definition at line 54 of file ci_lazy_methods_needed.h.

◆ pointer_type_selector

const select_pointer_typet& ci_lazy_methods_neededt::pointer_type_selector
private

Definition at line 57 of file ci_lazy_methods_needed.h.

◆ symbol_table

symbol_tablet& ci_lazy_methods_neededt::symbol_table
private

Definition at line 55 of file ci_lazy_methods_needed.h.


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