cprover
|
#include <remove_const_function_pointers.h>
Public Types | |
typedef std::unordered_set< exprt, irep_hash > | functionst |
typedef std::list< exprt > | expressionst |
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... | |
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 namespacet & | ns |
const symbol_tablet & | symbol_table |
Additional Inherited Members |
Definition at line 23 of file remove_const_function_pointers.h.
typedef std::list<exprt> remove_const_function_pointerst::expressionst |
Definition at line 27 of file remove_const_function_pointers.h.
typedef std::unordered_set<exprt, irep_hash> remove_const_function_pointerst::functionst |
Definition at line 26 of file remove_const_function_pointers.h.
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.
message_handler | The message handler for messaget |
ns | The namespace to use to resolve types |
symbol_table | The symbol table to look up symbols in |
Definition at line 27 of file remove_const_function_pointers.cpp.
|
private |
To extract the value of the specific component within a struct.
struct_expr | The expression of the structure being accessed |
member_expr | The expression saying which component is being accessed |
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().
|
private |
To evaluate the const-ness of the expression type.
expression | The expression to check |
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().
|
private |
To evaluate the const-ness of the type.
type | The type to check |
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().
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.
base_expression | The function call through a function pointer |
out_functions | The functions that (symbols of type ID_code) the base expression could take. |
Definition at line 47 of file remove_const_function_pointers.cpp.
References replace_const_symbols(), and try_resolve_function_call().
|
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.
expression | The expression to resolve symbols in |
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()().
|
private |
Look up a symbol in the symbol table and return its value.
symbol_expr | The symbol expression |
Definition at line 104 of file remove_const_function_pointers.cpp.
References symbol_exprt::get_identifier(), symbol_tablet::lookup(), symbol_table, and symbolt::value.
|
private |
To resolve an expression to the specific function calls it can be.
Specifically, this function deals with address_of expressions.
address_expr | The address_of expression to resolve to possible function calls |
out_functions | The functions this expression could be |
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().
|
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.
deref_expr | The dereference expression to resolve. |
out_expressions | The expressions this dereference could be |
out_is_const | Is the squashed expression 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().
|
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.
deref_expr | The dereference expression to resolve to possible function calls |
out_functions | The functions this expression could be |
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().
|
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
expr | The expression to try and squash |
out_resolved_expression | The squashed version of this expression |
out_is_const | Is the squashed expression constant |
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().
|
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.
expr | The expression to get the possible function calls |
out_functions | The functions this expression could be resolved to |
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().
|
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.
exprs | The expressions to evaluate |
out_functions | The functions these expressions resolve to |
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().
|
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.
index_expr | The index expression to to resolve |
out_expressions | The expressions this expression could be |
out_is_const | Is the squashed expression constant |
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().
|
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
index_expr | The index expression to resolve to possible function calls |
out_functions | The functions this expression could be |
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().
|
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.
expr | The expression of the index of the index expression (e.g. index_exprt::index()) |
out_array_index | The constant value the index takes |
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().
|
private |
To squash an member access by first finding the struct it is accessing Then return the squashed value of the relevant component.
member_expr | The member expression to resolve. |
out_expressions | The expressions this component could be |
out_is_const | Is the squashed expression constant |
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().
|
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.
member_expr | The member expression to resolve to possible function calls |
out_functions | The functions this expression could be |
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().
|
private |
To squash a typecast access.
typecast_expr | The typecast expression to resolve. |
out_expressions | The expressions this typecast could be |
out_is_const | Is the squashed expression constant |
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().
|
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.
typecast_expr | The typecast expression to resolve to possible function calls |
out_functions | The functions this expression could be |
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().
|
private |
Definition at line 95 of file remove_const_function_pointers.h.
Referenced by get_component_value(), try_resolve_expression(), and try_resolve_function_call().
|
private |
Definition at line 96 of file remove_const_function_pointers.h.
Referenced by replace_const_symbols(), and resolve_symbol().