cprover
constant_propagator.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Constant propagation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
21
22#ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
23#define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
24
25#include <iosfwd>
26#include <util/replace_symbol.h>
27
28#include "ai.h"
29#include "dirty.h"
30
32
34{
35public:
36 virtual void transform(
37 const irep_idt &function_from,
38 trace_ptrt trace_from,
39 const irep_idt &function_to,
40 trace_ptrt trace_to,
41 ai_baset &ai_base,
42 const namespacet &ns) final override;
43
44 virtual void output(
45 std::ostream &out,
46 const ai_baset &ai_base,
47 const namespacet &ns) const override;
48
49 bool merge(
50 const constant_propagator_domaint &other,
51 trace_ptrt from,
52 trace_ptrt to);
53
54 virtual bool ai_simplify(
55 exprt &condition,
56 const namespacet &ns) const final override;
57
58 virtual void make_bottom() final override
59 {
61 }
62
63 virtual void make_top() final override
64 {
66 }
67
68 virtual void make_entry() final override
69 {
70 make_top();
71 }
72
73 virtual bool is_bottom() const final override
74 {
75 return values.is_bot();
76 }
77
78 virtual bool is_top() const final override
79 {
80 return values.is_top();
81 }
82
83 struct valuest
84 {
85 // maps variables to constants
87 bool is_bottom = true;
88
89 bool merge(const valuest &src);
90 bool meet(const valuest &src, const namespacet &ns);
91
92 // set whole state
93
95 {
97 is_bottom=true;
98 }
99
101 {
103 is_bottom=false;
104 }
105
106 bool is_bot() const
107 {
108 return is_bottom && replace_const.empty();
109 }
110
111 bool is_top() const
112 {
113 return !is_bottom && replace_const.empty();
114 }
115
116 void set_to(const symbol_exprt &lhs, const exprt &rhs)
117 {
118 replace_const.set(lhs, rhs);
119 is_bottom=false;
120 }
121
122 bool set_to_top(const symbol_exprt &expr);
123
124 void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);
125
126 bool is_constant(const exprt &expr) const;
127
128 bool is_constant(const irep_idt &id) const;
129
130 bool is_empty() const
131 {
132 return replace_const.empty();
133 }
134
135 void output(std::ostream &out, const namespacet &ns) const;
136 };
137
139
140 static bool partial_evaluate(
141 const valuest &known_values,
142 exprt &expr,
143 const namespacet &ns);
144
145protected:
146 static void assign_rec(
147 valuest &dest_values,
148 const exprt &lhs,
149 const exprt &rhs,
150 const namespacet &ns,
151 const constant_propagator_ait *cp,
152 bool is_assignment);
153
155 const exprt &expr,
156 const namespacet &ns,
157 const constant_propagator_ait *cp);
158
160 const valuest &known_values,
161 exprt &expr,
162 const namespacet &ns);
163
165 const valuest &known_values,
166 exprt &expr,
167 const namespacet &ns);
168};
169
170class constant_propagator_ait:public ait<constant_propagator_domaint>
171{
172public:
173 typedef std::function<bool(const exprt &, const namespacet &)>
175
176 static bool track_all_values(const exprt &, const namespacet &)
177 {
178 return true;
179 }
180
182 const goto_functionst &goto_functions,
184 dirty(goto_functions),
186 {
187 }
188
190 const goto_functiont &goto_function,
192 dirty(goto_function),
194 {
195 }
196
198 goto_modelt &goto_model,
200 dirty(goto_model.goto_functions),
202 {
203 const namespacet ns(goto_model.symbol_table);
204 operator()(goto_model.goto_functions, ns);
205 replace(goto_model.goto_functions, ns);
206 }
207
209 const irep_idt &function_identifier,
210 goto_functionst::goto_functiont &goto_function,
211 const namespacet &ns,
214 {
215 operator()(function_identifier, goto_function, ns);
216 replace(goto_function, ns);
217 }
218
220
221protected:
223
224 void replace(
226 const namespacet &);
227
228 void replace(
230 const namespacet &);
231
233 const replace_symbolt &replace_const,
234 exprt &expr);
235
237};
238
239#endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
Abstract Interpretation.
Replace symbols with constants while maintaining syntactically valid expressions.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
void operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
Definition: ai.h:145
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
std::function< bool(const exprt &, const namespacet &)> should_track_valuet
constant_propagator_ait(goto_modelt &goto_model, should_track_valuet should_track_value=track_all_values)
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
static bool track_all_values(const exprt &, const namespacet &)
constant_propagator_ait(const goto_functionst &goto_functions, should_track_valuet should_track_value=track_all_values)
should_track_valuet should_track_value
constant_propagator_ait(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
void replace(goto_functionst::goto_functiont &, const namespacet &)
static void assign_rec(valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
Assign value rhs to lhs, recording any newly-known constants in dest_values.
virtual bool is_bottom() const final override
virtual bool is_top() const final override
static bool partial_evaluate(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
static bool partial_evaluate_with_all_rounding_modes(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate an expression in all rounding modes.
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai_base, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
virtual void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
virtual void make_entry() final override
Make this domain a reasonable entry-point state.
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
virtual void make_bottom() final override
no states
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Replace expression or type symbols by an expression or type, respectively.
bool empty() const
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Variables whose address is taken.
bool is_constant(const exprt &expr) const
bool meet(const valuest &src, const namespacet &ns)
meet
void output(std::ostream &out, const namespacet &ns) const
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
void set_to(const symbol_exprt &lhs, const exprt &rhs)