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 
11 
12 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
13 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
14 
15 #include <iosfwd>
16 #include <util/replace_symbol.h>
17 
18 #include "ai.h"
19 #include "dirty.h"
20 
22 
24 {
25 public:
26  virtual void transform(
27  locationt from,
28  locationt to,
29  ai_baset &ai_base,
30  const namespacet &ns) final override;
31 
32  virtual void output(
33  std::ostream &out,
34  const ai_baset &ai_base,
35  const namespacet &ns) const override;
36 
37  bool merge(
38  const constant_propagator_domaint &other,
39  locationt from,
40  locationt to);
41 
42  virtual bool ai_simplify(
43  exprt &condition,
44  const namespacet &ns) const final override;
45 
46  virtual void make_bottom() final override
47  {
49  }
50 
51  virtual void make_top() final override
52  {
54  }
55 
56  virtual void make_entry() final override
57  {
58  make_top();
59  }
60 
61  virtual bool is_bottom() const final override
62  {
63  return values.is_bot();
64  }
65 
66  virtual bool is_top() const final override
67  {
68  return values.is_top();
69  }
70 
71  struct valuest
72  {
73  // maps variables to constants
75  bool is_bottom = true;
76 
77  bool merge(const valuest &src);
78  bool meet(const valuest &src, const namespacet &ns);
79 
80  // set whole state
81 
83  {
85  is_bottom=true;
86  }
87 
88  void set_to_top()
89  {
91  is_bottom=false;
92  }
93 
94  bool is_bot() const
95  {
96  return is_bottom && replace_const.empty();
97  }
98 
99  bool is_top() const
100  {
101  return !is_bottom && replace_const.empty();
102  }
103 
104  // set single identifier
105 
106  void set_to(const irep_idt &lhs, const exprt &rhs)
107  {
108  replace_const.expr_map[lhs]=rhs;
109  is_bottom=false;
110  }
111 
112  void set_to(const symbol_exprt &lhs, const exprt &rhs)
113  {
114  set_to(lhs.get_identifier(), rhs);
115  }
116 
117  bool set_to_top(const symbol_exprt &expr)
118  {
119  return set_to_top(expr.get_identifier());
120  }
121 
122  bool set_to_top(const irep_idt &id);
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.expr_map.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  goto_functionst::goto_functiont &goto_function,
202  const namespacet &ns,
204  dirty(goto_function),
206  {
207  operator()(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
virtual void transform(locationt from, 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...
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)
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Definition: ai.h:294
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
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
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
constant_propagator_ait(goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
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...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
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)
void operator()(const goto_programt &goto_program, const namespacet &ns)
Running the interpreter.
Definition: ai.h:47
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
virtual void make_entry() final override
a reasonable entry-point state
Definition: dirty.h:23
bool set_to_top(const symbol_exprt &expr)
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:90
void set_to(const irep_idt &lhs, const exprt &rhs)
expr_mapt expr_map
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)