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 "ai.h"
16 
17 #include "replace_symbol_ext.h"
18 
20 {
21 public:
22  void transform(
23  locationt,
24  locationt,
25  ai_baset &,
26  const namespacet &) final;
27  void output(
28  std::ostream &,
29  const ai_baset &,
30  const namespacet &) const final;
31  void make_top() final { values.set_to_top(); }
32  void make_bottom() final { values.set_to_bottom(); }
33  void make_entry() final { values.set_to_top(); }
35 
36  virtual bool ai_simplify(
37  exprt &condition,
38  const namespacet &ns) const override;
39 
40  struct valuest
41  {
42  public:
43  valuest():is_bottom(true) { }
44 
45  // maps variables to constants
47  bool is_bottom;
48 
49  void output(std::ostream &, const namespacet &) const;
50 
51  bool merge(const valuest &src);
52  bool meet(const valuest &src);
53 
55  {
56  replace_const.clear();
57  is_bottom = true;
58  }
59 
60  void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
61  {
62  replace_const.expr_map[lhs_id] = rhs_val;
63  is_bottom = false;
64  }
65 
66  void set_to(const symbol_exprt &lhs, const exprt &rhs_val)
67  {
68  set_to(lhs.get_identifier(), rhs_val);
69  }
70 
71  bool is_constant(const exprt &expr) const;
72  bool is_array_constant(const exprt &expr) const;
73  bool is_constant_address_of(const exprt &expr) const;
74  bool set_to_top(const irep_idt &id);
75 
76  bool set_to_top(const symbol_exprt &expr)
77  {
78  return set_to_top(expr.get_identifier());
79  }
80 
81  void set_to_top()
82  {
83  replace_const.clear();
84  is_bottom = false;
85  }
86 
87  };
88 
90 
91 private:
92  void assign(
93  valuest &dest,
94  const symbol_exprt &lhs,
95  exprt rhs,
96  const namespacet &ns) const;
97 
98  void assign_rec(
99  valuest &values,
100  const exprt &lhs,
101  const exprt &rhs,
102  const namespacet &ns);
103 
105  const exprt &expr,
106  const namespacet &ns);
107 };
108 
109 class constant_propagator_ait:public ait<constant_propagator_domaint>
110 {
111 public:
113  goto_functionst &goto_functions,
114  const namespacet &ns)
115  {
116  operator()(goto_functions, ns);
117  replace(goto_functions, ns);
118  }
119 
121  goto_functionst::goto_functiont &goto_function,
122  const namespacet &ns)
123  {
124  operator()(goto_function, ns);
125  replace(goto_function, ns);
126  }
127 
128 protected:
130 
131  void replace_array_symbol(
132  exprt &expr);
133 
134  void replace(
136  const namespacet &);
137 
138  void replace(
139  goto_functionst &,
140  const namespacet &);
141 
142  void replace_types_rec(
144  exprt &expr);
145 
146 };
147 
148 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
void assign(valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const
bool is_array_constant(const exprt &expr) const
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
bool is_constant_address_of(const exprt &expr) const
void transform(locationt, locationt, ai_baset &, const namespacet &) final
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Definition: ai.h:342
bool meet(const valuest &src)
meet
bool merge(const valuest &src)
join
bool is_constant(const exprt &expr) const
TO_BE_DOCUMENTED.
Definition: namespace.h:62
constant_propagator_ait(goto_functionst::goto_functiont &goto_function, const namespacet &ns)
void set_to(const symbol_exprt &lhs, const exprt &rhs_val)
goto_function_templatet< goto_programt > goto_functiont
constant_propagator_ait(goto_functionst &goto_functions, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
Abstract Interpretation.
Modified expression replacement for constant propagator.
bool set_to_top(const irep_idt &id)
Do not call this when iterating over replace_const.expr_map!
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
void output(std::ostream &, const namespacet &) const
bool set_to_top(const symbol_exprt &expr)
void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
goto_programt::const_targett locationt
Definition: ai.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:82
expr_mapt expr_map
bool merge(const constant_propagator_domaint &, locationt, locationt)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
void output(std::ostream &, const ai_baset &, const namespacet &) const final