cprover
remove_const_function_pointers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs
4
5Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
13#define CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
14
15#include <list>
16#include <unordered_set>
17
18#include <util/expr.h>
19#include <util/message.h>
20#include <util/mp_arith.h>
21
24class index_exprt;
25class member_exprt;
26class namespacet;
27class struct_exprt;
28class symbol_exprt;
29class symbol_tablet;
30class typecast_exprt;
31
33{
34public:
35 typedef std::unordered_set<symbol_exprt, irep_hash> functionst;
36 typedef std::list<exprt> expressionst;
38 message_handlert &message_handler,
39 const namespacet &ns,
41
42 bool operator()(const exprt &base_expression, functionst &out_functions);
43
44private:
45 exprt replace_const_symbols(const exprt &expression) const;
46 exprt resolve_symbol(const symbol_exprt &symbol_expr) const;
47
48 // recursive functions for dealing with the function pointer
49 bool try_resolve_function_call(const exprt &expr, functionst &out_functions);
50
52 const expressionst &exprs, functionst &out_functions);
53
55 const index_exprt &index_expr, functionst &out_functions);
56
58 const member_exprt &member_expr, functionst &out_functions);
59
61 const address_of_exprt &address_expr, functionst &out_functions);
62
64 const dereference_exprt &deref_expr, functionst &out_functions);
65
67 const typecast_exprt &typecast_expr, functionst &out_functions);
68
69 // recursive functions for dealing with the auxiliary elements
71 const exprt &expr,
72 expressionst &out_resolved_expression,
73 bool &out_is_const);
74
76 const index_exprt &index_expr,
77 expressionst &out_expressions,
78 bool &out_is_const);
79
81 const member_exprt &member_expr,
82 expressionst &out_expressions,
83 bool &out_is_const);
84
86 const dereference_exprt &deref_expr,
87 expressionst &out_expressions,
88 bool &out_is_const);
89
91 const typecast_exprt &typecast_expr,
92 expressionst &out_expressions,
93 bool &out_is_const);
94
95 bool is_const_expression(const exprt &expression) const;
96 bool is_const_type(const typet &type) const;
97
99 const exprt &index_value_expr, mp_integer &out_array_index);
100
102 const struct_exprt &struct_expr, const member_exprt &member_expr);
103
107};
108
109#define OPT_REMOVE_CONST_FUNCTION_POINTERS \
110 "(remove-const-function-pointers)"
111
112#define HELP_REMOVE_CONST_FUNCTION_POINTERS \
113 " --remove-const-function-pointers\n" \
114 " remove function pointers that are constant" \
115 " or constant part of an array\n"
116
117#endif // CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
Operator to return the address of an object.
Definition: pointer_expr.h:361
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Base class for all expressions.
Definition: expr.h:54
Array index operator.
Definition: std_expr.h:1328
Extract member of struct or union.
Definition: std_expr.h:2667
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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 po...
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
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.
bool try_resolve_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
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.
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
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.
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...
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
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.
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.
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 po...
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
std::unordered_set< symbol_exprt, irep_hash > functionst
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.
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.
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
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 resolve...
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.
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.
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach,...
Struct constructor from list of elements.
Definition: std_expr.h:1722
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
BigInt mp_integer
Definition: smt_terms.h:12