cprover
remove_const_function_pointerst Class Reference

#include <remove_const_function_pointers.h>

Inheritance diagram for remove_const_function_pointerst:
[legend]
Collaboration diagram for remove_const_function_pointerst:
[legend]

Public Types

typedef std::unordered_set< exprt, irep_hashfunctionst
 
typedef std::list< exprtexpressionst
 
- 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
}
 

Public Member Functions

 remove_const_function_pointerst (message_handlert &message_handler, const namespacet &ns, const symbol_tablet &symbol_table)
 To take a function call on a function pointer, and if possible resolve it to a small collection of possible values. More...
 
bool operator() (const exprt &base_expression, functionst &out_functions)
 To take a function call on a function pointer, and if possible resolve it to a small collection of possible values. 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)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Private Member Functions

exprt replace_const_symbols (const exprt &expression) const
 To collapse the symbols down to their values where possible This takes a very general approach, recreating the expr tree exactly as it was and ignoring what type of expressions are found and instead recurses over all the operands. More...
 
exprt resolve_symbol (const symbol_exprt &symbol_expr) const
 Look up a symbol in the symbol table and return its value. More...
 
bool try_resolve_function_call (const exprt &expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_function_calls (const expressionst &exprs, functionst &out_functions)
 To resolve a collection of expressions to the specific function calls they can be. More...
 
bool try_resolve_index_of_function_call (const index_exprt &index_expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_member_function_call (const member_exprt &member_expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_address_of_function_call (const address_of_exprt &address_expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_dereference_function_call (const dereference_exprt &deref_expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_typecast_function_call (const typecast_exprt &typecast_expr, functionst &out_functions)
 To resolve an expression to the specific function calls it can be. More...
 
bool try_resolve_expression (const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
 To squash various expr types to simplify the expression. More...
 
bool try_resolve_index_of (const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
 To squash an index access by first finding the array it is accessing Then if the index can be resolved, return the squashed value. More...
 
bool try_resolve_member (const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
 To squash an member access by first finding the struct it is accessing Then return the squashed value of the relevant component. More...
 
bool try_resolve_dereference (const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
 To squash a dereference access by first finding the address_of the dereference is dereferencing. More...
 
bool try_resolve_typecast (const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
 To squash a typecast access. More...
 
bool is_const_expression (const exprt &expression) const
 To evaluate the const-ness of the expression type. More...
 
bool is_const_type (const typet &type) const
 To evaluate the const-ness of the type. More...
 
bool try_resolve_index_value (const exprt &index_value_expr, mp_integer &out_array_index)
 Given an index into an array, resolve, if possible, the index that is being accessed. More...
 
exprt get_component_value (const struct_exprt &struct_expr, const member_exprt &member_expr)
 To extract the value of the specific component within a struct. More...
 

Private Attributes

const namespacetns
 
const symbol_tabletsymbol_table
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 23 of file remove_const_function_pointers.h.

Member Typedef Documentation

§ expressionst

§ functionst

Definition at line 26 of file remove_const_function_pointers.h.

Constructor & Destructor Documentation

§ remove_const_function_pointerst()

remove_const_function_pointerst::remove_const_function_pointerst ( message_handlert message_handler,
const namespacet ns,
const symbol_tablet symbol_table 
)

To take a function call on a function pointer, and if possible resolve it to a small collection of possible values.

Parameters
message_handlerThe message handler for messaget
nsThe namespace to use to resolve types
symbol_tableThe symbol table to look up symbols in

Definition at line 27 of file remove_const_function_pointers.cpp.

Member Function Documentation

§ get_component_value()

exprt remove_const_function_pointerst::get_component_value ( const struct_exprt struct_expr,
const member_exprt member_expr 
)
private

To extract the value of the specific component within a struct.

Parameters
struct_exprThe expression of the structure being accessed
member_exprThe expression saying which component is being accessed
Returns
Returns the value of a specific component for a given struct expression.

Definition at line 801 of file remove_const_function_pointers.cpp.

References struct_union_typet::component_number(), namespace_baset::follow(), member_exprt::get_component_name(), ns, exprt::operands(), to_struct_type(), and exprt::type().

Referenced by try_resolve_member().

§ is_const_expression()

bool remove_const_function_pointerst::is_const_expression ( const exprt expression) const
private

To evaluate the const-ness of the expression type.

Parameters
expressionThe expression to check
Returns
Returns true if the type of the expression is constant.

Definition at line 772 of file remove_const_function_pointers.cpp.

References is_const_type(), and exprt::type().

Referenced by replace_const_symbols(), and try_resolve_expression().

§ is_const_type()

bool remove_const_function_pointerst::is_const_type ( const typet type) const
private

To evaluate the const-ness of the type.

Parameters
typeThe type to check
Returns
Returns true if the type has ID_C_constant or is an array since arrays are implicitly const in C.

Definition at line 782 of file remove_const_function_pointers.cpp.

References irept::id(), c_qualifierst::is_constant, and typet::subtype().

Referenced by is_const_expression(), and try_resolve_index_of().

§ operator()()

bool remove_const_function_pointerst::operator() ( const exprt base_expression,
functionst out_functions 
)

To take a function call on a function pointer, and if possible resolve it to a small collection of possible values.

It will resolve function pointers that are const and: - assigned directly to a function - assigned to a value in an array of functions - assigned to a const struct component Or variations within.

Parameters
base_expressionThe function call through a function pointer
out_functionsThe functions that (symbols of type ID_code) the base expression could take.
Returns
Returns true if it was able to resolve the call, false if not. If it returns true, out_functions will be populated by all the possible values the function pointer could be.

Definition at line 47 of file remove_const_function_pointers.cpp.

References replace_const_symbols(), and try_resolve_function_call().

§ replace_const_symbols()

exprt remove_const_function_pointerst::replace_const_symbols ( const exprt expression) const
private

To collapse the symbols down to their values where possible This takes a very general approach, recreating the expr tree exactly as it was and ignoring what type of expressions are found and instead recurses over all the operands.

Parameters
expressionThe expression to resolve symbols in
Returns
Returns a modified version of the expression, with all const symbols resolved to their actual values.

Definition at line 63 of file remove_const_function_pointers.cpp.

References irept::get(), irept::id(), is_const_expression(), symbol_tablet::lookup(), exprt::operands(), symbol_table, symbolt::type, and symbolt::value.

Referenced by operator()().

§ resolve_symbol()

exprt remove_const_function_pointerst::resolve_symbol ( const symbol_exprt symbol_expr) const
private

Look up a symbol in the symbol table and return its value.

Parameters
symbol_exprThe symbol expression
Returns
The expression value of the symbol.

Definition at line 104 of file remove_const_function_pointers.cpp.

References symbol_exprt::get_identifier(), symbol_tablet::lookup(), symbol_table, and symbolt::value.

§ try_resolve_address_of_function_call()

bool remove_const_function_pointerst::try_resolve_address_of_function_call ( const address_of_exprt address_expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with address_of expressions.

Parameters
address_exprThe address_of expression to resolve to possible function calls
out_functionsThe functions this expression could be
Returns
Returns true if it was able to resolve the address_of expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 302 of file remove_const_function_pointers.cpp.

References LOG, address_of_exprt::object(), and try_resolve_function_call().

Referenced by try_resolve_function_call().

§ try_resolve_dereference()

bool remove_const_function_pointerst::try_resolve_dereference ( const dereference_exprt deref_expr,
expressionst out_expressions,
bool &  out_is_const 
)
private

To squash a dereference access by first finding the address_of the dereference is dereferencing.

Then return the squashed value of the relevant component.

Parameters
deref_exprThe dereference expression to resolve.
out_expressionsThe expressions this dereference could be
out_is_constIs the squashed expression constant
Returns
Returns true if it was able to squash the dereference expression If this is the case, out_expressions will contain the possible values this dereference could return The out_is_const will return whether the object that gets dereferenced is constant.

Definition at line 671 of file remove_const_function_pointers.cpp.

References LOG, address_of_exprt::object(), dereference_exprt::pointer(), to_address_of_expr(), and try_resolve_expression().

Referenced by try_resolve_dereference_function_call(), and try_resolve_expression().

§ try_resolve_dereference_function_call()

bool remove_const_function_pointerst::try_resolve_dereference_function_call ( const dereference_exprt deref_expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with dereference expressions by using try_resolve_dereferebce and then recursing on its value.

Parameters
deref_exprThe dereference expression to resolve to possible function calls
out_functionsThe functions this expression could be
Returns
Returns true if it was able to resolve the dereference expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 323 of file remove_const_function_pointers.cpp.

References LOG, try_resolve_dereference(), and try_resolve_function_calls().

Referenced by try_resolve_function_call().

§ try_resolve_expression()

bool remove_const_function_pointerst::try_resolve_expression ( const exprt expr,
expressionst out_resolved_expression,
bool &  out_is_const 
)
private

To squash various expr types to simplify the expression.

ID_index -> dig to find ID_array and get the values out of it ID_member -> dig to find ID_struct and extract the component value ID_dereference -> dig to find ID_address_of and extract the value ID_typecast -> return the value ID_symbol -> return false, const symbols are squashed first and non const symbols cannot be squashed Everything else -> unchanged

Parameters
exprThe expression to try and squash
out_resolved_expressionThe squashed version of this expression
out_is_constIs the squashed expression constant
Returns
Returns true providing the squashing went OK (note it may not have squashed anything). The out_resolved_expression will in this case be all the possible squashed versions of the supplied expression. The out_is_const will return whether the squashed value is suitably const (e.g. if we squashed a struct access, was the struct const).

Definition at line 392 of file remove_const_function_pointers.cpp.

References irept::id(), is_const_expression(), LOG, ns, simplify_expr(), to_dereference_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), try_resolve_dereference(), try_resolve_index_of(), try_resolve_member(), and try_resolve_typecast().

Referenced by try_resolve_dereference(), try_resolve_index_of(), try_resolve_index_value(), try_resolve_member(), and try_resolve_typecast().

§ try_resolve_function_call()

bool remove_const_function_pointerst::try_resolve_function_call ( const exprt expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

This is different to try_resolve_expression which isn't explicitly looking for functions and is instead just trying to squash particular exprt structures.

Parameters
exprThe expression to get the possible function calls
out_functionsThe functions this expression could be resolved to
Returns
Returns true if it was able to resolve the expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 120 of file remove_const_function_pointers.cpp.

References LOG, ns, simplify_expr(), to_address_of_expr(), to_dereference_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), try_resolve_address_of_function_call(), try_resolve_dereference_function_call(), try_resolve_index_of_function_call(), try_resolve_member_function_call(), and try_resolve_typecast_function_call().

Referenced by operator()(), try_resolve_address_of_function_call(), try_resolve_function_calls(), and try_resolve_typecast_function_call().

§ try_resolve_function_calls()

bool remove_const_function_pointerst::try_resolve_function_calls ( const expressionst exprs,
functionst out_functions 
)
private

To resolve a collection of expressions to the specific function calls they can be.

Returns a collection if and only if all of them can be resolved.

Parameters
exprsThe expressions to evaluate
out_functionsThe functions these expressions resolve to
Returns
Returns true if able to resolve each of the expressions down to one or more functions.

Definition at line 204 of file remove_const_function_pointers.cpp.

References LOG, and try_resolve_function_call().

Referenced by try_resolve_dereference_function_call(), try_resolve_index_of_function_call(), and try_resolve_member_function_call().

§ try_resolve_index_of()

bool remove_const_function_pointerst::try_resolve_index_of ( const index_exprt index_expr,
expressionst out_expressions,
bool &  out_is_const 
)
private

To squash an index access by first finding the array it is accessing Then if the index can be resolved, return the squashed value.

If the index can't be determined then squash each value in the array and return them all.

Parameters
index_exprThe index expression to to resolve
out_expressionsThe expressions this expression could be
out_is_constIs the squashed expression constant
Returns
Returns true if it was able to squash the index expression If this is the case, out_expressions will contain the possible values this index_of could return The out_is_const will return whether either the array itself is const, or the values of the array are const.

Definition at line 503 of file remove_const_function_pointers.cpp.

References index_exprt::array(), index_exprt::index(), integer2size_t(), is_const_type(), LOG, exprt::operands(), try_resolve_expression(), and try_resolve_index_value().

Referenced by try_resolve_expression(), and try_resolve_index_of_function_call().

§ try_resolve_index_of_function_call()

bool remove_const_function_pointerst::try_resolve_index_of_function_call ( const index_exprt index_expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with index expressions where it squashes its array and squash its index If we can get a precise number for the index, we try_resolve_function_call on its value otherwise try_resolve_function_call on each and return the union of them all

Parameters
index_exprThe index expression to resolve to possible function calls
out_functionsThe functions this expression could be
Returns
Returns true if it was able to resolve the index expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 239 of file remove_const_function_pointers.cpp.

References LOG, try_resolve_function_calls(), and try_resolve_index_of().

Referenced by try_resolve_function_call().

§ try_resolve_index_value()

bool remove_const_function_pointerst::try_resolve_index_value ( const exprt expr,
mp_integer out_array_index 
)
private

Given an index into an array, resolve, if possible, the index that is being accessed.

This deals with symbols and typecasts to constant values.

Parameters
exprThe expression of the index of the index expression (e.g. index_exprt::index())
out_array_indexThe constant value the index takes
Returns
Returns true if was able to find a constant value for the index expression. If true, then out_array_index will be the index within the array that the function pointer is pointing to.

Definition at line 461 of file remove_const_function_pointers.cpp.

References to_constant_expr(), to_integer(), and try_resolve_expression().

Referenced by try_resolve_index_of().

§ try_resolve_member()

bool remove_const_function_pointerst::try_resolve_member ( const member_exprt member_expr,
expressionst out_expressions,
bool &  out_is_const 
)
private

To squash an member access by first finding the struct it is accessing Then return the squashed value of the relevant component.

Parameters
member_exprThe member expression to resolve.
out_expressionsThe expressions this component could be
out_is_constIs the squashed expression constant
Returns
Returns true if it was able to squash the member expression If this is the case, out_expressions will contain the possible values this member could return The out_is_const will return whether the struct is const.

Definition at line 604 of file remove_const_function_pointers.cpp.

References member_exprt::compound(), get_component_value(), LOG, to_struct_expr(), and try_resolve_expression().

Referenced by try_resolve_expression(), and try_resolve_member_function_call().

§ try_resolve_member_function_call()

bool remove_const_function_pointerst::try_resolve_member_function_call ( const member_exprt member_expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with member expressions by using try_resolve_member and then recursing on its value.

Parameters
member_exprThe member expression to resolve to possible function calls
out_functionsThe functions this expression could be
Returns
Returns true if it was able to resolve the member expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 271 of file remove_const_function_pointers.cpp.

References LOG, try_resolve_function_calls(), and try_resolve_member().

Referenced by try_resolve_function_call().

§ try_resolve_typecast()

bool remove_const_function_pointerst::try_resolve_typecast ( const typecast_exprt typecast_expr,
expressionst out_expressions,
bool &  out_is_const 
)
private

To squash a typecast access.

Parameters
typecast_exprThe typecast expression to resolve.
out_expressionsThe expressions this typecast could be
out_is_constIs the squashed expression constant
Returns
Returns true if it was able to squash the typecast expression If this is the case, out_expressions will contain the possible values after removing the typecast.

Definition at line 742 of file remove_const_function_pointers.cpp.

References LOG, typecast_exprt::op(), and try_resolve_expression().

Referenced by try_resolve_expression().

§ try_resolve_typecast_function_call()

bool remove_const_function_pointerst::try_resolve_typecast_function_call ( const typecast_exprt typecast_expr,
functionst out_functions 
)
private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with typecast expressions by looking at the type cast values.

Parameters
typecast_exprThe typecast expression to resolve to possible function calls
out_functionsThe functions this expression could be
Returns
Returns true if it was able to resolve the typecast expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 355 of file remove_const_function_pointers.cpp.

References LOG, typecast_exprt::op(), and try_resolve_function_call().

Referenced by try_resolve_function_call().

Member Data Documentation

§ ns

const namespacet& remove_const_function_pointerst::ns
private

§ symbol_table

const symbol_tablet& remove_const_function_pointerst::symbol_table
private

Definition at line 96 of file remove_const_function_pointers.h.

Referenced by replace_const_symbols(), and resolve_symbol().


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