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,
30 rw_range_sett &rw_set);
31
32void goto_rw(
33 const irep_idt &function,
34 const goto_programt &,
35 rw_range_sett &rw_set);
36
37void goto_rw(const goto_functionst &,
38 const irep_idt &function,
39 rw_range_sett &rw_set);
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
57typedef int range_spect;
58
60{
61 assert(size.is_long());
62 mp_integer::llong_t ll=size.to_long();
63 assert(ll<=std::numeric_limits<range_spect>::max());
64 assert(ll>=std::numeric_limits<range_spect>::min());
65 return (range_spect)ll;
66}
67
68// each element x represents a range of bits [x.first, x.second.first)
70{
71 typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
73
74public:
75 void output(const namespacet &ns, std::ostream &out) const override;
76
77 // NOLINTNEXTLINE(readability/identifiers)
78 typedef sub_typet::iterator iterator;
79 // NOLINTNEXTLINE(readability/identifiers)
80 typedef sub_typet::const_iterator const_iterator;
81
82 iterator begin() { return data.begin(); }
83 const_iterator begin() const { return data.begin(); }
84 const_iterator cbegin() const { return data.begin(); }
85
86 iterator end() { return data.end(); }
87 const_iterator end() const { return data.end(); }
88 const_iterator cend() const { return data.end(); }
89
90 void push_back(const sub_typet::value_type &v) { data.push_back(v); }
91 void push_back(sub_typet::value_type &&v) { data.push_back(std::move(v)); }
92};
93
96class shift_exprt;
97
99{
100public:
101 #ifdef USE_DSTRING
102 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
103 #else
104 typedef std::unordered_map<
105 irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
106 #endif
107
108 virtual ~rw_range_sett();
109
110 explicit rw_range_sett(const namespacet &_ns):
111 ns(_ns)
112 {
113 }
114
115 const objectst &get_r_set() const
116 {
117 return r_range_set;
118 }
119
120 const objectst &get_w_set() const
121 {
122 return w_range_set;
123 }
124
125 const range_domaint &
126 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
127 {
128 PRECONDITION(dynamic_cast<range_domaint *>(ranges.get()) != nullptr);
129 return static_cast<const range_domaint &>(*ranges);
130 }
131
132 enum class get_modet { LHS_W, READ };
133
134 virtual void get_objects_rec(
135 const irep_idt &,
137 get_modet mode,
138 const exprt &expr)
139 {
140 get_objects_rec(mode, expr);
141 }
142
143 virtual void get_objects_rec(
144 const irep_idt &,
146 const typet &type)
147 {
148 get_objects_rec(type);
149 }
150
151 void output(std::ostream &out) const;
152
153protected:
155
157
158 virtual void get_objects_rec(
159 get_modet mode,
160 const exprt &expr);
161
162 virtual void get_objects_rec(const typet &type);
163
164 virtual void get_objects_complex_real(
165 get_modet mode,
166 const complex_real_exprt &expr,
167 const range_spect &range_start,
168 const range_spect &size);
169
170 virtual void get_objects_complex_imag(
171 get_modet mode,
172 const complex_imag_exprt &expr,
173 const range_spect &range_start,
174 const range_spect &size);
175
176 virtual void get_objects_if(
177 get_modet mode,
178 const if_exprt &if_expr,
179 const range_spect &range_start,
180 const range_spect &size);
181
182 // overload to include expressions read/written
183 // through dereferencing
184 virtual void get_objects_dereference(
185 get_modet mode,
186 const dereference_exprt &deref,
187 const range_spect &range_start,
188 const range_spect &size);
189
190 virtual void get_objects_byte_extract(
191 get_modet mode,
192 const byte_extract_exprt &be,
193 const range_spect &range_start,
194 const range_spect &size);
195
196 virtual void get_objects_shift(
197 get_modet mode,
198 const shift_exprt &shift,
199 const range_spect &range_start,
200 const range_spect &size);
201
202 virtual void get_objects_member(
203 get_modet mode,
204 const member_exprt &expr,
205 const range_spect &range_start,
206 const range_spect &size);
207
208 virtual void get_objects_index(
209 get_modet mode,
210 const index_exprt &expr,
211 const range_spect &range_start,
212 const range_spect &size);
213
214 virtual void get_objects_array(
215 get_modet mode,
216 const array_exprt &expr,
217 const range_spect &range_start,
218 const range_spect &size);
219
220 virtual void get_objects_struct(
221 get_modet mode,
222 const struct_exprt &expr,
223 const range_spect &range_start,
224 const range_spect &size);
225
226 virtual void get_objects_typecast(
227 get_modet mode,
228 const typecast_exprt &tc,
229 const range_spect &range_start,
230 const range_spect &size);
231
232 virtual void get_objects_address_of(const exprt &object);
233
234 virtual void get_objects_rec(
235 get_modet mode,
236 const exprt &expr,
237 const range_spect &range_start,
238 const range_spect &size);
239
240 virtual void add(
241 get_modet mode,
242 const irep_idt &identifier,
243 const range_spect &range_start,
244 const range_spect &range_end);
245};
246
247inline std::ostream &operator << (
248 std::ostream &out,
249 const rw_range_sett &rw_set)
250{
251 rw_set.output(out);
252 return out;
253}
254
255class value_setst;
256
258{
259public:
261 const namespacet &_ns,
262 value_setst &_value_sets):
263 rw_range_sett(_ns),
264 value_sets(_value_sets)
265 {
266 }
267
269 const irep_idt &_function,
271 get_modet mode,
272 const exprt &expr) override
273 {
274 function = _function;
275 target=_target;
276
278 }
279
281 const irep_idt &_function,
283 const typet &type) override
284 {
285 function = _function;
286 target = _target;
287
289 }
290
291protected:
295
297
299 get_modet mode,
300 const dereference_exprt &deref,
301 const range_spect &range_start,
302 const range_spect &size) override;
303};
304
306{
307 typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
309
310public:
311 virtual void output(const namespacet &ns, std::ostream &out) const override;
312
313 // NOLINTNEXTLINE(readability/identifiers)
314 typedef sub_typet::iterator iterator;
315 // NOLINTNEXTLINE(readability/identifiers)
316 typedef sub_typet::const_iterator const_iterator;
317
318 iterator begin() { return data.begin(); }
319 const_iterator begin() const { return data.begin(); }
320 const_iterator cbegin() const { return data.begin(); }
321
322 iterator end() { return data.end(); }
323 const_iterator end() const { return data.end(); }
324 const_iterator cend() const { return data.end(); }
325
326 iterator insert(const sub_typet::value_type &v)
327 {
328 return data.insert(v);
329 }
330
331 iterator insert(sub_typet::value_type &&v)
332 {
333 return data.insert(std::move(v));
334 }
335};
336
338{
339public:
341 const namespacet &_ns,
342 value_setst &_value_sets,
344 : rw_range_set_value_sett(_ns, _value_sets),
347 {
348 }
349
351 get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
352 {
354 dynamic_cast<guarded_range_domaint *>(ranges.get()) != nullptr);
355 return static_cast<const guarded_range_domaint &>(*ranges);
356 }
357
359 const irep_idt &_function,
361 get_modet mode,
362 const exprt &expr) override
363 {
365
366 rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
367 }
368
370 const irep_idt &function,
372 const typet &type) override
373 {
375 }
376
377protected:
380
382
383 void get_objects_if(
384 get_modet mode,
385 const if_exprt &if_expr,
386 const range_spect &range_start,
387 const range_spect &size) override;
388
389 void add(
390 get_modet mode,
391 const irep_idt &identifier,
392 const range_spect &range_start,
393 const range_spect &range_end) override;
394};
395
396#endif // CPROVER_ANALYSES_GOTO_RW_H
Array constructor from list of elements.
Definition: std_expr.h:1476
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:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
const_iterator cbegin() const
Definition: goto_rw.h:320
iterator insert(const sub_typet::value_type &v)
Definition: goto_rw.h:326
iterator insert(sub_typet::value_type &&v)
Definition: goto_rw.h:331
const_iterator begin() const
Definition: goto_rw.h:319
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:657
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:316
sub_typet::iterator iterator
Definition: goto_rw.h:314
const_iterator cend() const
Definition: goto_rw.h:324
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition: goto_rw.h:307
const_iterator end() const
Definition: goto_rw.h:323
iterator end()
Definition: goto_rw.h:322
iterator begin()
Definition: goto_rw.h:318
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
Extract member of struct or union.
Definition: std_expr.h:2667
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:32
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:78
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:36
iterator end()
Definition: goto_rw.h:86
std::list< std::pair< range_spect, range_spect > > sub_typet
Definition: goto_rw.h:71
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:80
iterator begin()
Definition: goto_rw.h:82
sub_typet data
Definition: goto_rw.h:72
const_iterator cbegin() const
Definition: goto_rw.h:84
const_iterator cend() const
Definition: goto_rw.h:88
void push_back(sub_typet::value_type &&v)
Definition: goto_rw.h:91
void push_back(const sub_typet::value_type &v)
Definition: goto_rw.h:90
const_iterator end() const
Definition: goto_rw.h:87
const_iterator begin() const
Definition: goto_rw.h:83
void get_objects_rec(const irep_idt &function, goto_programt::const_targett target, const typet &type) override
Definition: goto_rw.h:369
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:358
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager)
Definition: goto_rw.h:340
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:351
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:675
guard_managert & guard_manager
Definition: goto_rw.h:378
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition: goto_rw.cpp:701
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:617
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:260
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
Definition: goto_rw.h:280
value_setst & value_sets
Definition: goto_rw.h:292
goto_programt::const_targett target
Definition: goto_rw.h:294
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:268
void output(std::ostream &out) const
Definition: goto_rw.cpp:63
objectst r_range_set
Definition: goto_rw.h:156
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:84
virtual ~rw_range_sett()
Definition: goto_rw.cpp:50
const objectst & get_w_set() const
Definition: goto_rw.h:120
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:172
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:110
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:250
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:339
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:93
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:428
objectst w_range_set
Definition: goto_rw.h:156
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, const typet &type)
Definition: goto_rw.h:143
const objectst & get_r_set() const
Definition: goto_rw.h:115
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:134
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:218
const namespacet & ns
Definition: goto_rw.h:154
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:480
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:402
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition: goto_rw.h:105
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:126
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:297
A base class for shift and rotate operators.
Struct constructor from list of elements.
Definition: std_expr.h:1722
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Concrete Goto Program.
int range_spect
Definition: goto_rw.h:57
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:755
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:59
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:247
Guard Data Structure.
guard_exprt guardt
Definition: guard.h:27
dstringt irep_idt
Definition: irep.h:37
BigInt mp_integer
Definition: smt_terms.h:12
#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