CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_rw.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening
6
7Date: April 2010
8
9\*******************************************************************/
10
11
12#ifndef CPROVER_ANALYSES_GOTO_RW_H
13#define CPROVER_ANALYSES_GOTO_RW_H
14
15#include <iosfwd>
16#include <map>
17#include <memory> // unique_ptr
18
19#include "guard.h"
20
22
23class goto_functionst;
25class rw_range_sett;
26
27void goto_rw(
28 const irep_idt &function,
31
32void goto_rw(
33 const irep_idt &function,
34 const goto_programt &,
36
37void goto_rw(const goto_functionst &,
38 const irep_idt &function,
40
42{
43public:
45
48
51
52 virtual ~range_domain_baset();
53
54 virtual void output(const namespacet &ns, std::ostream &out) const=0;
55};
56
61{
62public:
63 using value_type = int;
64
65 explicit range_spect(value_type v) : v(v)
66 {
67 }
68
70 {
71 return range_spect{-1};
72 }
73
74 bool is_unknown() const
75 {
76 return *this == unknown();
77 }
78
80 {
81 // The size need not fit into the analysis platform's width of a signed long
82 // (as an example, it could be an unsigned size_t max, or perhaps the source
83 // platform has much wider types than the analysis platform.
84 if(!size.is_long())
85 return range_spect::unknown();
86
87 mp_integer::llong_t ll = size.to_long();
88 if(
89 ll > std::numeric_limits<range_spect::value_type>::max() ||
90 ll < std::numeric_limits<range_spect::value_type>::min())
91 {
92 return range_spect::unknown();
93 }
94
95 return range_spect{(value_type)ll};
96 }
97
98 bool operator<(const range_spect &other) const
99 {
100 PRECONDITION(!is_unknown() && !other.is_unknown());
101 return v < other.v;
102 }
103
104 bool operator<=(const range_spect &other) const
105 {
106 PRECONDITION(!is_unknown() && !other.is_unknown());
107 return v <= other.v;
108 }
109
110 bool operator>(const range_spect &other) const
111 {
112 PRECONDITION(!is_unknown() && !other.is_unknown());
113 return v > other.v;
114 }
115
116 bool operator>=(const range_spect &other) const
117 {
118 PRECONDITION(!is_unknown() && !other.is_unknown());
119 return v >= other.v;
120 }
121
122 bool operator==(const range_spect &other) const
123 {
124 return v == other.v;
125 }
126
128 {
129 if(is_unknown() || other.is_unknown())
130 return range_spect::unknown();
132 }
133
135 {
136 range_spect result = *this + other;
137 v = result.v;
138 return *this;
139 }
140
142 {
143 if(is_unknown() || other.is_unknown())
144 return range_spect::unknown();
146 }
147
149 {
150 range_spect result = *this - other;
151 v = result.v;
152 return *this;
153 }
154
156 {
157 if(is_unknown() || other.is_unknown())
158 return range_spect::unknown();
160 }
161
162private:
164 friend std::ostream &operator<<(std::ostream &, const range_spect &);
165};
166
167inline std::ostream &operator<<(std::ostream &os, const range_spect &r)
168{
169 os << r.v;
170 return os;
171}
172
173// each element x represents a range of bits [x.first, x.second.first)
175{
176 typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
178
179public:
180 void output(const namespacet &ns, std::ostream &out) const override;
181
182 // NOLINTNEXTLINE(readability/identifiers)
183 typedef sub_typet::iterator iterator;
184 // NOLINTNEXTLINE(readability/identifiers)
185 typedef sub_typet::const_iterator const_iterator;
186
187 iterator begin() { return data.begin(); }
188 const_iterator begin() const { return data.begin(); }
189 const_iterator cbegin() const { return data.begin(); }
190
191 iterator end() { return data.end(); }
192 const_iterator end() const { return data.end(); }
193 const_iterator cend() const { return data.end(); }
194
195 void push_back(const sub_typet::value_type &v) { data.push_back(v); }
196 void push_back(sub_typet::value_type &&v) { data.push_back(std::move(v)); }
197};
198
201class shift_exprt;
202
204{
205public:
206 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
207
208 virtual ~rw_range_sett();
209
214
215 const objectst &get_r_set() const
216 {
217 return r_range_set;
218 }
219
220 const objectst &get_w_set() const
221 {
222 return w_range_set;
223 }
224
225 const range_domaint &
226 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
227 {
228 PRECONDITION(dynamic_cast<range_domaint *>(ranges.get()) != nullptr);
229 return static_cast<const range_domaint &>(*ranges);
230 }
231
232 enum class get_modet { LHS_W, READ };
233
234 virtual void get_objects_rec(
235 const irep_idt &,
237 get_modet mode,
238 const exprt &expr)
239 {
240 get_objects_rec(mode, expr);
241 }
242
243 virtual void get_objects_rec(
244 const irep_idt &,
246 const typet &type)
247 {
248 get_objects_rec(type);
249 }
250
251 virtual void get_array_objects(
252 const irep_idt &,
254 get_modet,
255 const exprt &);
256
257 void output(std::ostream &out) const;
258
259protected:
262
264
265 virtual void get_objects_rec(
266 get_modet mode,
267 const exprt &expr);
268
269 virtual void get_objects_rec(const typet &type);
270
271 virtual void get_objects_complex_real(
272 get_modet mode,
273 const complex_real_exprt &expr,
275 const range_spect &size);
276
277 virtual void get_objects_complex_imag(
278 get_modet mode,
279 const complex_imag_exprt &expr,
281 const range_spect &size);
282
283 virtual void get_objects_if(
284 get_modet mode,
285 const if_exprt &if_expr,
287 const range_spect &size);
288
289 // overload to include expressions read/written
290 // through dereferencing
291 virtual void get_objects_dereference(
292 get_modet mode,
295 const range_spect &size);
296
297 virtual void get_objects_byte_extract(
298 get_modet mode,
299 const byte_extract_exprt &be,
301 const range_spect &size);
302
303 virtual void get_objects_shift(
304 get_modet mode,
305 const shift_exprt &shift,
307 const range_spect &size);
308
309 virtual void get_objects_member(
310 get_modet mode,
311 const member_exprt &expr,
313 const range_spect &size);
314
315 virtual void get_objects_index(
316 get_modet mode,
317 const index_exprt &expr,
319 const range_spect &size);
320
321 virtual void get_objects_array(
322 get_modet mode,
323 const array_exprt &expr,
325 const range_spect &size);
326
327 virtual void get_objects_struct(
328 get_modet mode,
329 const struct_exprt &expr,
331 const range_spect &size);
332
333 virtual void get_objects_typecast(
334 get_modet mode,
335 const typecast_exprt &tc,
337 const range_spect &size);
338
339 virtual void get_objects_address_of(const exprt &object);
340
341 virtual void get_objects_rec(
342 get_modet mode,
343 const exprt &expr,
345 const range_spect &size);
346
347 virtual void add(
348 get_modet mode,
349 const irep_idt &identifier,
351 const range_spect &range_end);
352};
353
354inline std::ostream &operator << (
355 std::ostream &out,
356 const rw_range_sett &rw_set)
357{
358 rw_set.output(out);
359 return out;
360}
361
362class value_setst;
363
365{
366public:
374
376 const irep_idt &_function,
378 get_modet mode,
379 const exprt &expr) override
380 {
383
385 }
386
388 const irep_idt &_function,
390 const typet &type) override
391 {
393 target = _target;
394
396 }
397
399 const irep_idt &_function,
401 get_modet mode,
402 const exprt &pointer) override
403 {
405 target = _target;
406
408 }
409
410protected:
414
416
418 get_modet mode,
421 const range_spect &size) override;
422};
423
425{
426 typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
428
429public:
430 virtual void output(const namespacet &ns, std::ostream &out) const override;
431
432 // NOLINTNEXTLINE(readability/identifiers)
433 typedef sub_typet::iterator iterator;
434 // NOLINTNEXTLINE(readability/identifiers)
435 typedef sub_typet::const_iterator const_iterator;
436
437 iterator begin() { return data.begin(); }
438 const_iterator begin() const { return data.begin(); }
439 const_iterator cbegin() const { return data.begin(); }
440
441 iterator end() { return data.end(); }
442 const_iterator end() const { return data.end(); }
443 const_iterator cend() const { return data.end(); }
444
445 iterator insert(const sub_typet::value_type &v)
446 {
447 return data.insert(v);
448 }
449
450 iterator insert(sub_typet::value_type &&v)
451 {
452 return data.insert(std::move(v));
453 }
454};
455
457{
458public:
469
471 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
472 {
474 dynamic_cast<guarded_range_domaint *>(ranges.get()) != nullptr);
475 return static_cast<const guarded_range_domaint &>(*ranges);
476 }
477
479 const irep_idt &_function,
481 get_modet mode,
482 const exprt &expr) override
483 {
485
487 }
488
490 const irep_idt &function,
492 const typet &type) override
493 {
495 }
496
497protected:
500
502
503 void get_objects_if(
504 get_modet mode,
505 const if_exprt &if_expr,
507 const range_spect &size) override;
508
509 void add(
510 get_modet mode,
511 const irep_idt &identifier,
513 const range_spect &range_end) override;
514};
515
516#endif // CPROVER_ANALYSES_GOTO_RW_H
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Expression of type type extracted from some object op starting at position offset (given in number of...
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
Operator to dereference a pointer.
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
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
const_iterator cbegin() const
Definition goto_rw.h:439
iterator insert(const sub_typet::value_type &v)
Definition goto_rw.h:445
iterator insert(sub_typet::value_type &&v)
Definition goto_rw.h:450
const_iterator begin() const
Definition goto_rw.h:438
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:714
sub_typet::const_iterator const_iterator
Definition goto_rw.h:435
sub_typet::iterator iterator
Definition goto_rw.h:433
const_iterator cend() const
Definition goto_rw.h:443
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition goto_rw.h:426
const_iterator end() const
Definition goto_rw.h:442
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
Extract member of struct or union.
Definition std_expr.h:2971
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
virtual ~range_domain_baset()
Definition goto_rw.cpp:30
range_domain_baset & operator=(range_domain_baset &&rhs)=delete
virtual void output(const namespacet &ns, std::ostream &out) const =0
range_domain_baset(range_domain_baset &&rhs)=delete
range_domain_baset()=default
range_domain_baset(const range_domain_baset &rhs)=delete
range_domain_baset & operator=(const range_domain_baset &rhs)=delete
sub_typet::iterator iterator
Definition goto_rw.h:183
void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:34
iterator end()
Definition goto_rw.h:191
std::list< std::pair< range_spect, range_spect > > sub_typet
Definition goto_rw.h:176
sub_typet::const_iterator const_iterator
Definition goto_rw.h:185
iterator begin()
Definition goto_rw.h:187
sub_typet data
Definition goto_rw.h:177
const_iterator cbegin() const
Definition goto_rw.h:189
const_iterator cend() const
Definition goto_rw.h:193
void push_back(sub_typet::value_type &&v)
Definition goto_rw.h:196
void push_back(const sub_typet::value_type &v)
Definition goto_rw.h:195
const_iterator end() const
Definition goto_rw.h:192
const_iterator begin() const
Definition goto_rw.h:188
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition goto_rw.h:61
friend std::ostream & operator<<(std::ostream &, const range_spect &)
Definition goto_rw.h:167
bool operator>(const range_spect &other) const
Definition goto_rw.h:110
static range_spect unknown()
Definition goto_rw.h:69
range_spect operator*(const range_spect &other) const
Definition goto_rw.h:155
range_spect & operator+=(const range_spect &other)
Definition goto_rw.h:134
range_spect operator+(const range_spect &other) const
Definition goto_rw.h:127
range_spect(value_type v)
Definition goto_rw.h:65
static range_spect to_range_spect(const mp_integer &size)
Definition goto_rw.h:79
bool is_unknown() const
Definition goto_rw.h:74
value_type v
Definition goto_rw.h:163
bool operator<=(const range_spect &other) const
Definition goto_rw.h:104
bool operator==(const range_spect &other) const
Definition goto_rw.h:122
bool operator>=(const range_spect &other) const
Definition goto_rw.h:116
int value_type
Definition goto_rw.h:63
bool operator<(const range_spect &other) const
Definition goto_rw.h:98
range_spect operator-(const range_spect &other) const
Definition goto_rw.h:141
range_spect & operator-=(const range_spect &other)
Definition goto_rw.h:148
void get_objects_rec(const irep_idt &function, goto_programt::const_targett target, const typet &type) override
Definition goto_rw.h:489
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager, message_handlert &message_handler)
Definition goto_rw.h:459
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:478
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition goto_rw.h:471
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
Definition goto_rw.cpp:732
guard_managert & guard_manager
Definition goto_rw.h:498
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition goto_rw.cpp:758
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
Definition goto_rw.cpp:676
void get_array_objects(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &pointer) override
Definition goto_rw.h:398
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, message_handlert &message_handler)
Definition goto_rw.h:367
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
Definition goto_rw.h:387
value_setst & value_sets
Definition goto_rw.h:411
goto_programt::const_targett target
Definition goto_rw.h:413
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:375
void output(std::ostream &out) const
Definition goto_rw.cpp:61
objectst r_range_set
Definition goto_rw.h:263
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:132
std::map< irep_idt, std::unique_ptr< range_domain_baset > > objectst
Definition goto_rw.h:206
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:82
message_handlert & message_handler
Definition goto_rw.h:261
virtual ~rw_range_sett()
Definition goto_rw.cpp:48
const objectst & get_w_set() const
Definition goto_rw.h:220
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:186
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:271
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:366
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:91
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:113
virtual void get_objects_address_of(const exprt &object)
Definition goto_rw.cpp:468
rw_range_sett(const namespacet &_ns, message_handlert &message_handler)
Definition goto_rw.h:210
objectst w_range_set
Definition goto_rw.h:263
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
Definition goto_rw.cpp:664
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, const typet &type)
Definition goto_rw.h:243
const objectst & get_r_set() const
Definition goto_rw.h:215
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:144
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition goto_rw.h:234
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:237
const namespacet & ns
Definition goto_rw.h:260
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition goto_rw.cpp:520
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:440
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition goto_rw.h:226
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition goto_rw.cpp:322
A base class for shift and rotate operators.
Struct constructor from list of elements.
Definition std_expr.h:1877
The Boolean constant true.
Definition std_expr.h:3190
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Concrete Goto Program.
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
Definition goto_rw.cpp:867
std::ostream & operator<<(std::ostream &os, const range_spect &r)
Definition goto_rw.h:167
Guard Data Structure.
guard_exprt guardt
Definition guard.h:29
static int8_t r
Definition irep_hash.h:60
get_modet
Definition object_id.cpp:18
#define PRECONDITION(CONDITION)
Definition invariant.h:463
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20