cprover
invariant_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_INVARIANT_SET_H
13 #define CPROVER_ANALYSES_INVARIANT_SET_H
14 
15 #include <util/std_code.h>
16 #include <util/numbering.h>
17 #include <util/union_find.h>
18 #include <util/threeval.h>
19 #include <util/mp_arith.h>
20 
22 
23 #include "interval_template.h"
24 
26 {
27 public:
28  explicit inv_object_storet(const namespacet &_ns):ns(_ns)
29  {
30  }
31 
32  bool get(const exprt &expr, unsigned &n);
33 
34  unsigned add(const exprt &expr);
35 
36  bool is_constant(unsigned n) const;
37  bool is_constant(const exprt &expr) const;
38 
39  static bool is_constant_address(const exprt &expr);
40 
41  const irep_idt &operator[](unsigned n) const
42  {
43  return map[n];
44  }
45 
46  const exprt &get_expr(unsigned n) const
47  {
48  assert(n<entries.size());
49  return entries[n].expr;
50  }
51 
52  void output(std::ostream &out) const;
53 
54  std::string to_string(
55  unsigned n,
56  const irep_idt &identifier) const;
57 
58 protected:
59  const namespacet &ns;
60 
63 
64  struct entryt
65  {
68  };
69 
70  std::vector<entryt> entries;
71 
72  std::string build_string(const exprt &expr) const;
73 
74  static bool is_constant_address_rec(const exprt &expr);
75 };
76 
78 {
79 public:
80  // equalities ==
82 
83  // <=
84  typedef std::set<std::pair<unsigned, unsigned> > ineq_sett;
86 
87  // !=
89 
90  // bounds
92  typedef std::map<unsigned, boundst> bounds_mapt;
94 
95  bool threaded;
96  bool is_false;
97 
99  threaded(false),
100  is_false(false),
101  value_sets(nullptr),
102  object_store(nullptr),
103  ns(nullptr)
104  {
105  }
106 
107  void output(
108  const irep_idt &identifier,
109  std::ostream &out) const;
110 
111  // true = added something
112  bool make_union(const invariant_sett &other_invariants);
113 
114  void strengthen(const exprt &expr);
115 
116  void make_true()
117  {
118  eq_set.clear();
119  le_set.clear();
120  ne_set.clear();
121  is_false=false;
122  }
123 
124  void make_false()
125  {
126  eq_set.clear();
127  le_set.clear();
128  ne_set.clear();
129  is_false=true;
130  }
131 
133  {
134  make_true();
135  threaded=true;
136  }
137 
138  void apply_code(
139  const codet &code);
140 
141  void modifies(
142  const exprt &lhs);
143 
144  void assignment(
145  const exprt &lhs,
146  const exprt &rhs);
147 
148  void set_value_sets(value_setst &_value_sets)
149  {
150  value_sets=&_value_sets;
151  }
152 
153  void set_object_store(inv_object_storet &_object_store)
154  {
155  object_store=&_object_store;
156  }
157 
158  void set_namespace(const namespacet &_ns)
159  {
160  ns=&_ns;
161  }
162 
163  static void intersection(ineq_sett &dest, const ineq_sett &other)
164  {
165  ineq_sett::iterator it_d=dest.begin();
166 
167  while(it_d!=dest.end())
168  {
169  ineq_sett::iterator next_d(it_d);
170  next_d++;
171 
172  if(other.find(*it_d)==other.end())
173  dest.erase(it_d);
174 
175  it_d=next_d;
176  }
177  }
178 
179  static void remove(ineq_sett &dest, unsigned a)
180  {
181  for(ineq_sett::iterator it=dest.begin();
182  it!=dest.end();
183  ) // no it++
184  {
185  ineq_sett::iterator next(it);
186  next++;
187 
188  if(it->first==a || it->second==a)
189  dest.erase(it);
190 
191  it=next;
192  }
193  }
194 
195  tvt implies(const exprt &expr) const;
196 
197  void simplify(exprt &expr) const;
198 
199 protected:
202  const namespacet *ns;
203 
204  tvt implies_rec(const exprt &expr) const;
205  static void nnf(exprt &expr, bool negate=false);
206  void strengthen_rec(const exprt &expr);
207 
208  void add_type_bounds(const exprt &expr, const typet &type);
209 
210  void add_bounds(unsigned a, const boundst &bound)
211  {
212  bounds_map[a].intersect_with(bound);
213  }
214 
215  void get_bounds(unsigned a, boundst &dest) const;
216 
217  // true = added something
218  bool make_union_bounds_map(const bounds_mapt &other);
219 
220  void modifies(unsigned a);
221 
222  std::string to_string(
223  unsigned a,
224  const irep_idt &identifier) const;
225 
226  bool get_object(
227  const exprt &expr,
228  unsigned &n) const;
229 
230  exprt get_constant(const exprt &expr) const;
231 
232  // queries
233  bool has_eq(const std::pair<unsigned, unsigned> &p) const
234  {
235  return eq_set.same_set(p.first, p.second);
236  }
237 
238  bool has_le(const std::pair<unsigned, unsigned> &p) const
239  {
240  return le_set.find(p)!=le_set.end();
241  }
242 
243  bool has_ne(const std::pair<unsigned, unsigned> &p) const
244  {
245  return ne_set.find(p)!=ne_set.end();
246  }
247 
248  tvt is_eq(std::pair<unsigned, unsigned> p) const;
249  tvt is_le(std::pair<unsigned, unsigned> p) const;
250 
251  tvt is_lt(std::pair<unsigned, unsigned> p) const
252  {
253  return is_le(p) && !is_eq(p);
254  }
255 
256  tvt is_ge(std::pair<unsigned, unsigned> p) const
257  {
258  std::swap(p.first, p.second);
259  return is_eq(p) || is_lt(p);
260  }
261 
262  tvt is_gt(std::pair<unsigned, unsigned> p) const
263  {
264  return !is_le(p);
265  }
266 
267  tvt is_ne(std::pair<unsigned, unsigned> p) const
268  {
269  return !is_eq(p);
270  }
271 
272  void add(const std::pair<unsigned, unsigned> &p, ineq_sett &dest);
273 
274  void add_le(const std::pair<unsigned, unsigned> &p)
275  {
276  add(p, le_set);
277  }
278 
279  void add_ne(const std::pair<unsigned, unsigned> &p)
280  {
281  add(p, ne_set);
282  }
283 
284  void add_eq(const std::pair<unsigned, unsigned> &eq);
285 
286  void add_eq(
287  ineq_sett &dest,
288  const std::pair<unsigned, unsigned> &eq,
289  const std::pair<unsigned, unsigned> &ineq);
290 };
291 
292 #endif // CPROVER_ANALYSES_INVARIANT_SET_H
void get_bounds(unsigned a, boundst &dest) const
The type of an expression.
Definition: type.h:22
tvt is_lt(std::pair< unsigned, unsigned > p) const
void strengthen_rec(const exprt &expr)
static bool is_constant_address(const exprt &expr)
static void nnf(exprt &expr, bool negate=false)
static void intersection(ineq_sett &dest, const ineq_sett &other)
void strengthen(const exprt &expr)
ineq_sett le_set
Definition: invariant_set.h:85
bool make_union(const invariant_sett &other_invariants)
void add_ne(const std::pair< unsigned, unsigned > &p)
const exprt & get_expr(unsigned n) const
Definition: invariant_set.h:46
hash_numbering< irep_idt, irep_id_hash > mapt
Definition: invariant_set.h:61
const namespacet & ns
Definition: invariant_set.h:59
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
tvt is_eq(std::pair< unsigned, unsigned > p) const
std::string build_string(const exprt &expr) const
void add_type_bounds(const exprt &expr, const typet &type)
void add_bounds(unsigned a, const boundst &bound)
void assignment(const exprt &lhs, const exprt &rhs)
tvt is_gt(std::pair< unsigned, unsigned > p) const
exprt get_constant(const exprt &expr) const
void output(std::ostream &out) const
tvt implies(const exprt &expr) const
void make_threaded()
bool has_eq(const std::pair< unsigned, unsigned > &p) const
Value Set Propagation.
const irep_idt & operator[](unsigned n) const
Definition: invariant_set.h:41
void set_value_sets(value_setst &_value_sets)
void apply_code(const codet &code)
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
unsigned add(const exprt &expr)
bool is_constant(unsigned n) const
tvt is_ge(std::pair< unsigned, unsigned > p) const
unsigned_union_find eq_set
Definition: invariant_set.h:81
std::map< unsigned, boundst > bounds_mapt
Definition: invariant_set.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::string to_string(unsigned n, const irep_idt &identifier) const
interval_templatet< mp_integer > boundst
Definition: invariant_set.h:91
tvt is_ne(std::pair< unsigned, unsigned > p) const
void simplify(exprt &expr) const
bounds_mapt bounds_map
Definition: invariant_set.h:93
bool has_ne(const std::pair< unsigned, unsigned > &p) const
void set_object_store(inv_object_storet &_object_store)
Base class for all expressions.
Definition: expr.h:42
const namespacet * ns
value_setst * value_sets
inv_object_storet * object_store
std::string to_string(unsigned a, const irep_idt &identifier) const
void add_eq(const std::pair< unsigned, unsigned > &eq)
ineq_sett ne_set
Definition: invariant_set.h:88
static bool is_constant_address_rec(const exprt &expr)
std::vector< entryt > entries
Definition: invariant_set.h:70
bool make_union_bounds_map(const bounds_mapt &other)
std::set< std::pair< unsigned, unsigned > > ineq_sett
Definition: invariant_set.h:84
tvt implies_rec(const exprt &expr) const
A statement in a programming language.
Definition: std_code.h:21
void modifies(const exprt &lhs)
bool has_le(const std::pair< unsigned, unsigned > &p) const
bool get_object(const exprt &expr, unsigned &n) const
bool same_set(size_type a, size_type b) const
Definition: union_find.h:88
void output(const irep_idt &identifier, std::ostream &out) const
inv_object_storet(const namespacet &_ns)
Definition: invariant_set.h:28
tvt is_le(std::pair< unsigned, unsigned > p) const
void set_namespace(const namespacet &_ns)
void add_le(const std::pair< unsigned, unsigned > &p)