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  locationt from,
39  const irep_idt &function_to,
40  locationt 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  bool is_array_constant(const exprt &expr) const;
128  bool is_constant_address_of(const exprt &expr) 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  bool partial_evaluate(exprt &expr, const namespacet &ns) const;
141 
142 protected:
143  void assign_rec(
144  valuest &values,
145  const exprt &lhs,
146  const exprt &rhs,
147  const namespacet &ns,
148  const constant_propagator_ait *cp);
149 
151  const exprt &expr,
152  const namespacet &ns,
153  const constant_propagator_ait *cp);
154 
156  exprt &expr,
157  const namespacet &ns) const;
158 
159  bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const;
160 };
161 
162 class constant_propagator_ait:public ait<constant_propagator_domaint>
163 {
164 public:
165  typedef std::function<bool(const exprt &, const namespacet &)>
167 
168  static bool track_all_values(const exprt &, const namespacet &)
169  {
170  return true;
171  }
172 
174  const goto_functionst &goto_functions,
176  dirty(goto_functions),
178  {
179  }
180 
182  const goto_functiont &goto_function,
184  dirty(goto_function),
186  {
187  }
188 
190  goto_modelt &goto_model,
192  dirty(goto_model.goto_functions),
194  {
195  const namespacet ns(goto_model.symbol_table);
196  operator()(goto_model.goto_functions, ns);
197  replace(goto_model.goto_functions, ns);
198  }
199 
201  const irep_idt &function_identifier,
202  goto_functionst::goto_functiont &goto_function,
203  const namespacet &ns,
205  : dirty(goto_function), should_track_value(should_track_value)
206  {
207  operator()(function_identifier, goto_function, ns);
208  replace(goto_function, ns);
209  }
210 
212 
213 protected:
215 
216  void replace(
218  const namespacet &);
219 
220  void replace(
221  goto_functionst &,
222  const namespacet &);
223 
224  void replace_types_rec(
225  const replace_symbolt &replace_const,
226  exprt &expr);
227 
229 };
230 
231 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
bool empty() const
bool is_array_constant(const exprt &expr) const
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
bool is_constant_address_of(const exprt &expr) const
Variables whose address is taken.
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
Definition: ai.h:365
void set_to(const symbol_exprt &lhs, const exprt &rhs)
virtual bool is_top() const final override
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
bool merge(const valuest &src)
join
void operator()(const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
Definition: ai.h:47
bool is_constant(const exprt &expr) const
constant_propagator_ait(const goto_functionst &goto_functions, should_track_valuet should_track_value=track_all_values)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
Replace expression or type symbols by an expression or type, respectively.
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)
Replace symbols with constants while maintaining syntactically valid expressions. ...
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
should_track_valuet should_track_value
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
virtual void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it...
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt 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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26
virtual bool is_bottom() const final override
virtual void make_bottom() final override
no states
std::function< bool(const exprt &, const namespacet &)> should_track_valuet
bool partial_evaluate_with_all_rounding_modes(exprt &expr, const namespacet &ns) const
Attempt to evaluate an expression in all rounding modes.
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
virtual void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: dirty.h:23
constant_propagator_ait(goto_modelt &goto_model, should_track_valuet should_track_value=track_all_values)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void replace(goto_functionst::goto_functiont &, const namespacet &)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void output(std::ostream &out, const namespacet &ns) const
static bool track_all_values(const exprt &, const namespacet &)
bool meet(const valuest &src, const namespacet &ns)
meet
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)