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 {
23 public:
24  virtual void transform(
25  locationt from,
26  locationt to,
27  ai_baset &ai_base,
28  const namespacet &ns) final override;
29 
30  virtual void output(
31  std::ostream &out,
32  const ai_baset &ai_base,
33  const namespacet &ns) const override;
34 
35  bool merge(
36  const constant_propagator_domaint &other,
37  locationt from,
38  locationt to);
39 
40  virtual bool ai_simplify(
41  exprt &condition,
42  const namespacet &ns) const final override;
43 
44  virtual void make_bottom() final override
45  {
47  }
48 
49  virtual void make_top() final override
50  {
52  }
53 
54  virtual void make_entry() final override
55  {
56  make_top();
57  }
58 
59  virtual bool is_bottom() const final override
60  {
61  return values.is_bot();
62  }
63 
64  virtual bool is_top() const final override
65  {
66  return values.is_top();
67  }
68 
69  struct valuest
70  {
71  public:
72  valuest():is_bottom(true) {}
73 
74  // maps variables to constants
76  bool is_bottom;
77 
78  bool merge(const valuest &src);
79  bool meet(const valuest &src);
80 
81  // set whole state
82 
84  {
86  is_bottom=true;
87  }
88 
89  void set_to_top()
90  {
92  is_bottom=false;
93  }
94 
95  bool is_bot() const
96  {
97  return is_bottom && replace_const.empty();
98  }
99 
100  bool is_top() const
101  {
102  return !is_bottom && replace_const.empty();
103  }
104 
105  // set single identifier
106 
107  void set_to(const irep_idt &lhs, const exprt &rhs)
108  {
109  replace_const.expr_map[lhs]=rhs;
110  is_bottom=false;
111  }
112 
113  void set_to(const symbol_exprt &lhs, const exprt &rhs)
114  {
115  set_to(lhs.get_identifier(), rhs);
116  }
117 
118  bool set_to_top(const symbol_exprt &expr)
119  {
120  return set_to_top(expr.get_identifier());
121  }
122 
123  bool set_to_top(const irep_idt &id);
124 
125  void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);
126 
127  bool is_constant(const exprt &expr) const;
128  bool is_array_constant(const exprt &expr) const;
129  bool is_constant_address_of(const exprt &expr) const;
130 
131  bool is_empty() const
132  {
133  return replace_const.expr_map.empty();
134  }
135 
136  void output(std::ostream &out, const namespacet &ns) const;
137  };
138 
140 
141  bool partial_evaluate(exprt &expr, const namespacet &ns) const;
142 
143 protected:
144  void assign_rec(
145  valuest &values,
146  const exprt &lhs, const exprt &rhs,
147  const namespacet &ns);
148 
150  const exprt &expr,
151  const namespacet &ns);
152 
154  exprt &expr,
155  const namespacet &ns) const;
156 
157  bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const;
158 };
159 
160 class constant_propagator_ait:public ait<constant_propagator_domaint>
161 {
162 public:
163  explicit constant_propagator_ait(const goto_functionst &goto_functions):
164  dirty(goto_functions)
165  {
166  }
167 
169  goto_modelt &goto_model):dirty(goto_model.goto_functions)
170  {
171  const namespacet ns(goto_model.symbol_table);
172  operator()(goto_model.goto_functions, ns);
173  replace(goto_model.goto_functions, ns);
174  }
175 
177  goto_functionst::goto_functiont &goto_function,
178  const namespacet &ns):dirty(goto_function)
179  {
180  operator()(goto_function, ns);
181  replace(goto_function, ns);
182  }
183 
185 
186 protected:
188 
189  void replace(
191  const namespacet &);
192 
193  void replace(
194  goto_functionst &,
195  const namespacet &);
196 
197  void replace_types_rec(
198  const replace_symbolt &replace_const,
199  exprt &expr);
200 };
201 
202 #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
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:377
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 meet(const valuest &src)
meet
bool merge(const valuest &src)
join
bool is_constant(const exprt &expr) const
bool partial_evaluate(exprt &expr, const namespacet &ns) const
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. ...
virtual void make_top() final override
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
constant_propagator_ait(goto_functionst::goto_functiont &goto_function, const namespacet &ns)
virtual bool is_bottom() const final override
virtual void make_bottom() final override
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
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
void operator()(const goto_programt &goto_program, const namespacet &ns)
Definition: ai.h:142
Abstract Interpretation.
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
virtual void make_entry() final override
Definition: dirty.h:23
bool set_to_top(const symbol_exprt &expr)
constant_propagator_ait(goto_modelt &goto_model)
goto_programt::const_targett locationt
Definition: ai.h:44
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 &)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
constant_propagator_ait(const goto_functionst &goto_functions)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void output(std::ostream &out, const namespacet &ns) const
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)