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