cprover
constant_propagator.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Constant propagation
4 
5 Author: 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 {
35 public:
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  locationt from,
52  locationt 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 
100  void set_to_top()
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 
145 protected:
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 
164  static bool replace_constants_and_simplify(
165  const valuest &known_values,
166  exprt &expr,
167  const namespacet &ns);
168 };
169 
170 class constant_propagator_ait:public ait<constant_propagator_domaint>
171 {
172 public:
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,
213  : dirty(goto_function), should_track_value(should_track_value)
214  {
215  operator()(function_identifier, goto_function, ns);
216  replace(goto_function, ns);
217  }
218 
220 
221 protected:
223 
224  void replace(
226  const namespacet &);
227 
228  void replace(
229  goto_functionst &,
230  const namespacet &);
231 
232  void replace_types_rec(
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:120
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:144
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
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
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
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.
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:27
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:92
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:81
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)