cprover
Loading...
Searching...
No Matches
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;
24
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 #ifdef USE_DSTRING
207 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
208 #else
209 typedef std::unordered_map<
210 irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
211 #endif
212
213 virtual ~rw_range_sett();
214
215 explicit rw_range_sett(const namespacet &_ns):
216 ns(_ns)
217 {
218 }
219
220 const objectst &get_r_set() const
221 {
222 return r_range_set;
223 }
224
225 const objectst &get_w_set() const
226 {
227 return w_range_set;
228 }
229
230 const range_domaint &
231 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
232 {
233 PRECONDITION(dynamic_cast<range_domaint *>(ranges.get()) != nullptr);
234 return static_cast<const range_domaint &>(*ranges);
235 }
236
237 enum class get_modet { LHS_W, READ };
238
239 virtual void get_objects_rec(
240 const irep_idt &,
242 get_modet mode,
243 const exprt &expr)
244 {
245 get_objects_rec(mode, expr);
246 }
247
248 virtual void get_objects_rec(
249 const irep_idt &,
251 const typet &type)
252 {
253 get_objects_rec(type);
254 }
255
256 virtual void get_array_objects(
257 const irep_idt &,
259 get_modet,
260 const exprt &);
261
262 void output(std::ostream &out) const;
263
264protected:
266
268
269 virtual void get_objects_rec(
270 get_modet mode,
271 const exprt &expr);
272
273 virtual void get_objects_rec(const typet &type);
274
275 virtual void get_objects_complex_real(
276 get_modet mode,
277 const complex_real_exprt &expr,
279 const range_spect &size);
280
281 virtual void get_objects_complex_imag(
282 get_modet mode,
283 const complex_imag_exprt &expr,
285 const range_spect &size);
286
287 virtual void get_objects_if(
288 get_modet mode,
289 const if_exprt &if_expr,
291 const range_spect &size);
292
293 // overload to include expressions read/written
294 // through dereferencing
295 virtual void get_objects_dereference(
296 get_modet mode,
299 const range_spect &size);
300
301 virtual void get_objects_byte_extract(
302 get_modet mode,
303 const byte_extract_exprt &be,
305 const range_spect &size);
306
307 virtual void get_objects_shift(
308 get_modet mode,
309 const shift_exprt &shift,
311 const range_spect &size);
312
313 virtual void get_objects_member(
314 get_modet mode,
315 const member_exprt &expr,
317 const range_spect &size);
318
319 virtual void get_objects_index(
320 get_modet mode,
321 const index_exprt &expr,
323 const range_spect &size);
324
325 virtual void get_objects_array(
326 get_modet mode,
327 const array_exprt &expr,
329 const range_spect &size);
330
331 virtual void get_objects_struct(
332 get_modet mode,
333 const struct_exprt &expr,
335 const range_spect &size);
336
337 virtual void get_objects_typecast(
338 get_modet mode,
339 const typecast_exprt &tc,
341 const range_spect &size);
342
343 virtual void get_objects_address_of(const exprt &object);
344
345 virtual void get_objects_rec(
346 get_modet mode,
347 const exprt &expr,
349 const range_spect &size);
350
351 virtual void add(
352 get_modet mode,
353 const irep_idt &identifier,
355 const range_spect &range_end);
356};
357
358inline std::ostream &operator << (
359 std::ostream &out,
360 const rw_range_sett &rw_set)
361{
362 rw_set.output(out);
363 return out;
364}
365
366class value_setst;
367
369{
370public:
378
380 const irep_idt &_function,
382 get_modet mode,
383 const exprt &expr) override
384 {
387
389 }
390
392 const irep_idt &_function,
394 const typet &type) override
395 {
397 target = _target;
398
400 }
401
403 const irep_idt &_function,
405 get_modet mode,
406 const exprt &pointer) override
407 {
409 target = _target;
410
412 }
413
414protected:
418
420
422 get_modet mode,
425 const range_spect &size) override;
426};
427
429{
430 typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
432
433public:
434 virtual void output(const namespacet &ns, std::ostream &out) const override;
435
436 // NOLINTNEXTLINE(readability/identifiers)
437 typedef sub_typet::iterator iterator;
438 // NOLINTNEXTLINE(readability/identifiers)
439 typedef sub_typet::const_iterator const_iterator;
440
441 iterator begin() { return data.begin(); }
442 const_iterator begin() const { return data.begin(); }
443 const_iterator cbegin() const { return data.begin(); }
444
445 iterator end() { return data.end(); }
446 const_iterator end() const { return data.end(); }
447 const_iterator cend() const { return data.end(); }
448
449 iterator insert(const sub_typet::value_type &v)
450 {
451 return data.insert(v);
452 }
453
454 iterator insert(sub_typet::value_type &&v)
455 {
456 return data.insert(std::move(v));
457 }
458};
459
461{
462public:
472
474 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
475 {
477 dynamic_cast<guarded_range_domaint *>(ranges.get()) != nullptr);
478 return static_cast<const guarded_range_domaint &>(*ranges);
479 }
480
482 const irep_idt &_function,
484 get_modet mode,
485 const exprt &expr) override
486 {
488
490 }
491
493 const irep_idt &function,
495 const typet &type) override
496 {
498 }
499
500protected:
503
505
506 void get_objects_if(
507 get_modet mode,
508 const if_exprt &if_expr,
510 const range_spect &size) override;
511
512 void add(
513 get_modet mode,
514 const irep_idt &identifier,
516 const range_spect &range_end) override;
517};
518
519#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:563
Array constructor from list of elements.
Definition std_expr.h:1563
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:1971
Real part of the expression describing a complex number.
Definition std_expr.h:1926
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:39
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:443
iterator insert(const sub_typet::value_type &v)
Definition goto_rw.h:449
iterator insert(sub_typet::value_type &&v)
Definition goto_rw.h:454
const_iterator begin() const
Definition goto_rw.h:442
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition goto_rw.cpp:711
sub_typet::const_iterator const_iterator
Definition goto_rw.h:439
sub_typet::iterator iterator
Definition goto_rw.h:437
const_iterator cend() const
Definition goto_rw.h:447
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition goto_rw.h:430
const_iterator end() const
Definition goto_rw.h:446
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
Extract member of struct or union.
Definition std_expr.h:2794
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:31
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:35
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:492
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:481
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager)
Definition goto_rw.h:463
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition goto_rw.h:474
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:729
guard_managert & guard_manager
Definition goto_rw.h:501
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition goto_rw.cpp:755
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:673
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition goto_rw.h:371
void get_array_objects(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &pointer) override
Definition goto_rw.h:402
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
Definition goto_rw.h:391
value_setst & value_sets
Definition goto_rw.h:415
goto_programt::const_targett target
Definition goto_rw.h:417
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition goto_rw.h:379
void output(std::ostream &out) const
Definition goto_rw.cpp:62
objectst r_range_set
Definition goto_rw.h:267
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:133
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:83
virtual ~rw_range_sett()
Definition goto_rw.cpp:49
const objectst & get_w_set() const
Definition goto_rw.h:225
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:187
rw_range_sett(const namespacet &_ns)
Definition goto_rw.h:215
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:270
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:365
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:92
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:114
virtual void get_objects_address_of(const exprt &object)
Definition goto_rw.cpp:465
objectst w_range_set
Definition goto_rw.h:267
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
Definition goto_rw.cpp:661
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, const typet &type)
Definition goto_rw.h:248
const objectst & get_r_set() const
Definition goto_rw.h:220
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:145
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition goto_rw.h:239
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:238
const namespacet & ns
Definition goto_rw.h:265
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition goto_rw.cpp:517
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:437
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition goto_rw.h:210
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition goto_rw.h:231
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:321
A base class for shift and rotate operators.
Struct constructor from list of elements.
Definition std_expr.h:1819
The Boolean constant true.
Definition std_expr.h:3008
Semantic type conversion.
Definition std_expr.h:2017
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:864
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
Definition kdev_t.h:24
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
dstringt irep_idt