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