cprover
select_pointer_typet Class Reference

#include <select_pointer_type.h>

Public Member Functions

virtual ~select_pointer_typet ()=default
 
virtual pointer_typet convert_pointer_type (const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
 Select what type should be used for a given pointer type. More...
 
pointer_typet specialize_generics (const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited) const
 Specialize generic parameters in a pointer type based on the current map of parameters -> types. More...
 

Private Member Functions

optionalt< pointer_typetget_recursively_instantiated_type (const irep_idt &, const generic_parameter_specialization_mapt &, generic_parameter_recursion_trackingt &, const size_t) const
 See get_recursively instantiated_type, the additional parameters just track the recursion to prevent visiting the same depth again and specify which stack depth is analyzed. More...
 
optionalt< pointer_typetget_recursively_instantiated_type (const irep_idt &parameter_name, const generic_parameter_specialization_mapt &visited) const
 Return the first concrete type instantiation if any such exists. More...
 

Detailed Description

Definition at line 26 of file select_pointer_type.h.

Constructor & Destructor Documentation

◆ ~select_pointer_typet()

virtual select_pointer_typet::~select_pointer_typet ( )
virtualdefault

Member Function Documentation

◆ convert_pointer_type()

pointer_typet select_pointer_typet::convert_pointer_type ( const pointer_typet pointer_type,
const generic_parameter_specialization_mapt generic_parameter_specialization_map,
const namespacet ns 
) const
virtual

Select what type should be used for a given pointer type.

For the base class we just use the supplied type. Derived classes can override this behaviour to provide more sophisticated type selection. Generic parameters are replaced with their concrete type.

Parameters
pointer_typeThe pointer type replace
generic_parameter_specialization_mapmap of types for all generic parameters in the current scope
nsNamespace for type lookups
Returns
A pointer type where the subtype may have been modified

Definition at line 26 of file select_pointer_type.cpp.

References INVARIANT, pointer_type(), and specialize_generics().

Referenced by ci_lazy_methods_neededt::add_all_needed_classes(), and java_object_factoryt::gen_nondet_pointer_init().

◆ get_recursively_instantiated_type() [1/2]

optionalt< pointer_typet > select_pointer_typet::get_recursively_instantiated_type ( const irep_idt parameter_name,
const generic_parameter_specialization_mapt generic_parameter_specialization_map,
generic_parameter_recursion_trackingt visited,
const size_t  depth 
) const
private

See get_recursively instantiated_type, the additional parameters just track the recursion to prevent visiting the same depth again and specify which stack depth is analyzed.

Parameters
parameter_nameThe name of the generic parameter type we want to have instantiated
generic_parameter_specialization_mapMap of type names to specialization stack
visitedTracks the visited parameter names
depthStack depth to analyze
Returns
if this type is not a generic type, it is returned as a valid instantiation, if nothing can be found at the given depth, en empty optional is returned

Definition at line 186 of file select_pointer_type.cpp.

References INVARIANT, is_java_generic_parameter(), and to_java_generic_parameter().

Referenced by get_recursively_instantiated_type(), and specialize_generics().

◆ get_recursively_instantiated_type() [2/2]

optionalt< pointer_typet > select_pointer_typet::get_recursively_instantiated_type ( const irep_idt parameter_name,
const generic_parameter_specialization_mapt generic_parameter_specialization_map 
) const
private

Return the first concrete type instantiation if any such exists.

This method is only to be called when the specialize_generics cannot find an instantiation due to a loop in its recursion.

Parameters
parameter_nameThe name of the generic parameter type we want to have instantiated
generic_parameter_specialization_mapMap of type names to specialization stack
Returns
The first instantiated type for the generic type or nothing if no such instantiation exists.

Definition at line 144 of file select_pointer_type.cpp.

References CHECK_RETURN, java_generic_parametert::get_name(), get_recursively_instantiated_type(), is_java_generic_parameter(), and to_java_generic_parameter().

◆ specialize_generics()

pointer_typet select_pointer_typet::specialize_generics ( const pointer_typet pointer_type,
const generic_parameter_specialization_mapt generic_parameter_specialization_map,
generic_parameter_recursion_trackingt visited_nodes 
) const

Specialize generic parameters in a pointer type based on the current map of parameters -> types.

We specialize generics if the pointer is a java generic parameter or an array with generic parameters (java generic types are specialized recursively, their concrete types are already stored in the map and will be retrieved when needed e.g., to initialize fields). Example:

  • generic type: T
  • map: T -> U; U -> String
  • result: String
  • generic type: T[]
  • map: T -> U; U -> String
  • result: String
    Parameters
    pointer_typepointer to be specialized
    generic_parameter_specialization_mapmap of types for all generic parameters in the current scope
    Returns
    pointer type where generic parameters are replaced with concrete types, if set in the current scope

Definition at line 66 of file select_pointer_type.cpp.

References irept::find(), symbol_typet::get_identifier(), java_generic_parametert::get_name(), get_recursively_instantiated_type(), irept::id(), is_java_array_tag(), is_java_generic_parameter(), java_array_element_type(), java_array_type(), pointer_type(), irept::set(), typet::subtype(), to_java_generic_parameter(), to_pointer_type(), and to_symbol_type().

Referenced by convert_pointer_type().


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