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
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition: invariant_set.cpp:391
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
invariant_sett::boundst
interval_templatet< mp_integer > boundst
Definition: invariant_set.h:91
union_find.h
invariant_sett::is_ge
tvt is_ge(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:256
mp_arith.h
inv_object_storet::inv_object_storet
inv_object_storet(const namespacet &_ns)
Definition: invariant_set.h:28
inv_object_storet
Definition: invariant_set.h:25
invariant_sett::implies
tvt implies(const exprt &expr) const
Definition: invariant_set.cpp:595
invariant_sett::ineq_sett
std::set< std::pair< unsigned, unsigned > > ineq_sett
Definition: invariant_set.h:84
invariant_sett::get_bounds
void get_bounds(unsigned a, boundst &dest) const
Definition: invariant_set.cpp:686
typet
The type of an expression, extends irept.
Definition: type.h:27
unsigned_union_find
Definition: union_find.h:23
invariant_sett::add_type_bounds
void add_type_bounds(const exprt &expr, const typet &type)
Definition: invariant_set.cpp:371
invariant_sett::make_threaded
void make_threaded()
Definition: invariant_set.h:132
threeval.h
invariant_sett::is_lt
tvt is_lt(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:251
invariant_sett::threaded
bool threaded
Definition: invariant_set.h:95
template_numberingt
Definition: numbering.h:21
inv_object_storet::entryt::is_constant
bool is_constant
Definition: invariant_set.h:66
exprt
Base class for all expressions.
Definition: expr.h:54
invariant_sett::is_le
tvt is_le(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.cpp:299
invariant_sett::set_namespace
void set_namespace(const namespacet &_ns)
Definition: invariant_set.h:158
invariant_sett::make_union_bounds_map
bool make_union_bounds_map(const bounds_mapt &other)
Definition: invariant_set.cpp:953
inv_object_storet::to_string
std::string to_string(unsigned n, const irep_idt &identifier) const
Definition: invariant_set.cpp:887
inv_object_storet::entryt
Definition: invariant_set.h:64
invariant_sett::ns
const namespacet * ns
Definition: invariant_set.h:202
inv_object_storet::map
mapt map
Definition: invariant_set.h:62
invariant_sett::nnf
static void nnf(exprt &expr, bool negate=false)
Definition: invariant_set.cpp:710
inv_object_storet::entries
std::vector< entryt > entries
Definition: invariant_set.h:70
invariant_sett::set_value_sets
void set_value_sets(value_setst &_value_sets)
Definition: invariant_set.h:148
invariant_sett::apply_code
void apply_code(const codet &code)
Definition: invariant_set.cpp:1072
interval_templatet
Definition: interval_template.h:18
value_sets.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
inv_object_storet::add
unsigned add(const exprt &expr)
Definition: invariant_set.cpp:64
interval_template.h
invariant_sett::intersection
static void intersection(ineq_sett &dest, const ineq_sett &other)
Definition: invariant_set.h:163
invariant_sett::is_false
bool is_false
Definition: invariant_set.h:96
invariant_sett::eq_set
unsigned_union_find eq_set
Definition: invariant_set.h:81
invariant_sett::add_le
void add_le(const std::pair< unsigned, unsigned > &p)
Definition: invariant_set.h:274
invariant_sett::value_sets
value_setst * value_sets
Definition: invariant_set.h:200
invariant_sett::add_eq
void add_eq(const std::pair< unsigned, unsigned > &eq)
Definition: invariant_set.cpp:210
inv_object_storet::operator[]
const irep_idt & operator[](unsigned n) const
Definition: invariant_set.h:41
invariant_sett::output
void output(const irep_idt &identifier, std::ostream &out) const
Definition: invariant_set.cpp:317
inv_object_storet::get_expr
const exprt & get_expr(unsigned n) const
Definition: invariant_set.h:46
inv_object_storet::get
bool get(const exprt &expr, unsigned &n)
Definition: invariant_set.cpp:35
inv_object_storet::mapt
hash_numbering< irep_idt, irep_id_hash > mapt
Definition: invariant_set.h:61
invariant_sett::invariant_sett
invariant_sett()
Definition: invariant_set.h:98
invariant_sett::is_gt
tvt is_gt(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:262
invariant_sett::modifies
void modifies(const exprt &lhs)
Definition: invariant_set.cpp:993
inv_object_storet::is_constant
bool is_constant(unsigned n) const
Definition: invariant_set.cpp:82
numbering.h
invariant_sett::remove
static void remove(ineq_sett &dest, unsigned a)
Definition: invariant_set.h:179
invariant_sett::implies_rec
tvt implies_rec(const exprt &expr) const
Definition: invariant_set.cpp:602
std_code.h
invariant_sett::add_ne
void add_ne(const std::pair< unsigned, unsigned > &p)
Definition: invariant_set.h:279
unsigned_union_find::same_set
bool same_set(size_type a, size_type b) const
Definition: union_find.h:92
tvt
Definition: threeval.h:19
invariant_sett::has_le
bool has_le(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:238
invariant_sett::object_store
inv_object_storet * object_store
Definition: invariant_set.h:201
inv_object_storet::output
void output(std::ostream &out) const
Definition: invariant_set.cpp:29
invariant_sett::add
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
Definition: invariant_set.cpp:188
invariant_sett::bounds_mapt
std::map< unsigned, boundst > bounds_mapt
Definition: invariant_set.h:92
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:124
invariant_sett::le_set
ineq_sett le_set
Definition: invariant_set.h:85
invariant_sett::ne_set
ineq_sett ne_set
Definition: invariant_set.h:88
value_setst
Definition: value_sets.h:21
invariant_sett
Definition: invariant_set.h:77
invariant_sett::assignment
void assignment(const exprt &lhs, const exprt &rhs)
Definition: invariant_set.cpp:1053
inv_object_storet::build_string
std::string build_string(const exprt &expr) const
Definition: invariant_set.cpp:94
invariant_sett::simplify
void simplify(exprt &expr) const
Definition: invariant_set.cpp:821
unsigned_union_find::clear
void clear()
Definition: union_find.h:77
invariant_sett::get_object
bool get_object(const exprt &expr, unsigned &n) const
Definition: invariant_set.cpp:156
invariant_sett::make_union
bool make_union(const invariant_sett &other_invariants)
Definition: invariant_set.cpp:902
invariant_sett::set_object_store
void set_object_store(inv_object_storet &_object_store)
Definition: invariant_set.h:153
invariant_sett::is_ne
tvt is_ne(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.h:267
inv_object_storet::entryt::expr
exprt expr
Definition: invariant_set.h:67
invariant_sett::get_constant
exprt get_constant(const exprt &expr) const
Definition: invariant_set.cpp:839
inv_object_storet::is_constant_address_rec
static bool is_constant_address_rec(const exprt &expr)
Definition: invariant_set.cpp:172
invariant_sett::to_string
std::string to_string(unsigned a, const irep_idt &identifier) const
Definition: invariant_set.cpp:894
inv_object_storet::ns
const namespacet & ns
Definition: invariant_set.h:59
invariant_sett::strengthen_rec
void strengthen_rec(const exprt &expr)
Definition: invariant_set.cpp:398
invariant_sett::bounds_map
bounds_mapt bounds_map
Definition: invariant_set.h:93
invariant_sett::is_eq
tvt is_eq(std::pair< unsigned, unsigned > p) const
Definition: invariant_set.cpp:285
inv_object_storet::is_constant_address
static bool is_constant_address(const exprt &expr)
Definition: invariant_set.cpp:164
invariant_sett::add_bounds
void add_bounds(unsigned a, const boundst &bound)
Definition: invariant_set.h:210
invariant_sett::has_ne
bool has_ne(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:243
invariant_sett::has_eq
bool has_eq(const std::pair< unsigned, unsigned > &p) const
Definition: invariant_set.h:233
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:116
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34