CBMC
goto_rw.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
23 class goto_functionst;
24 class message_handlert;
25 class rw_range_sett;
26 
27 void goto_rw(
28  const irep_idt &function,
30  rw_range_sett &rw_set);
31 
32 void goto_rw(
33  const irep_idt &function,
34  const goto_programt &,
35  rw_range_sett &rw_set);
36 
37 void goto_rw(const goto_functionst &,
38  const irep_idt &function,
39  rw_range_sett &rw_set);
40 
42 {
43 public:
44  range_domain_baset()=default;
45 
48 
51 
52  virtual ~range_domain_baset();
53 
54  virtual void output(const namespacet &ns, std::ostream &out) const=0;
55 };
56 
61 {
62 public:
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 
127  range_spect operator+(const range_spect &other) const
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 
141  range_spect operator-(const range_spect &other) const
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 
155  range_spect operator*(const range_spect &other) const
156  {
157  if(is_unknown() || other.is_unknown())
158  return range_spect::unknown();
160  }
161 
162 private:
164  friend std::ostream &operator<<(std::ostream &, const range_spect &);
165 };
166 
167 inline 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 
179 public:
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 
199 class byte_extract_exprt;
200 class dereference_exprt;
201 class shift_exprt;
202 
204 {
205 public:
206  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
207 
208  virtual ~rw_range_sett();
209 
212  {
213  }
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 
259 protected:
260  const namespacet &ns;
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,
274  const range_spect &range_start,
275  const range_spect &size);
276 
277  virtual void get_objects_complex_imag(
278  get_modet mode,
279  const complex_imag_exprt &expr,
280  const range_spect &range_start,
281  const range_spect &size);
282 
283  virtual void get_objects_if(
284  get_modet mode,
285  const if_exprt &if_expr,
286  const range_spect &range_start,
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,
293  const dereference_exprt &deref,
294  const range_spect &range_start,
295  const range_spect &size);
296 
297  virtual void get_objects_byte_extract(
298  get_modet mode,
299  const byte_extract_exprt &be,
300  const range_spect &range_start,
301  const range_spect &size);
302 
303  virtual void get_objects_shift(
304  get_modet mode,
305  const shift_exprt &shift,
306  const range_spect &range_start,
307  const range_spect &size);
308 
309  virtual void get_objects_member(
310  get_modet mode,
311  const member_exprt &expr,
312  const range_spect &range_start,
313  const range_spect &size);
314 
315  virtual void get_objects_index(
316  get_modet mode,
317  const index_exprt &expr,
318  const range_spect &range_start,
319  const range_spect &size);
320 
321  virtual void get_objects_array(
322  get_modet mode,
323  const array_exprt &expr,
324  const range_spect &range_start,
325  const range_spect &size);
326 
327  virtual void get_objects_struct(
328  get_modet mode,
329  const struct_exprt &expr,
330  const range_spect &range_start,
331  const range_spect &size);
332 
333  virtual void get_objects_typecast(
334  get_modet mode,
335  const typecast_exprt &tc,
336  const range_spect &range_start,
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,
344  const range_spect &range_start,
345  const range_spect &size);
346 
347  virtual void add(
348  get_modet mode,
349  const irep_idt &identifier,
350  const range_spect &range_start,
351  const range_spect &range_end);
352 };
353 
354 inline 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 
362 class value_setst;
363 
365 {
366 public:
368  const namespacet &_ns,
369  value_setst &_value_sets,
371  : rw_range_sett(_ns, message_handler), value_sets(_value_sets)
372  {
373  }
374 
376  const irep_idt &_function,
378  get_modet mode,
379  const exprt &expr) override
380  {
381  function = _function;
382  target=_target;
383 
384  rw_range_sett::get_objects_rec(mode, expr);
385  }
386 
388  const irep_idt &_function,
390  const typet &type) override
391  {
392  function = _function;
393  target = _target;
394 
396  }
397 
399  const irep_idt &_function,
401  get_modet mode,
402  const exprt &pointer) override
403  {
404  function = _function;
405  target = _target;
406 
407  rw_range_sett::get_array_objects(_function, _target, mode, pointer);
408  }
409 
410 protected:
412  irep_idt function;
414 
416 
418  get_modet mode,
419  const dereference_exprt &deref,
420  const range_spect &range_start,
421  const range_spect &size) override;
422 };
423 
425 {
426  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
428 
429 public:
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 {
458 public:
460  const namespacet &_ns,
461  value_setst &_value_sets,
464  : rw_range_set_value_sett(_ns, _value_sets, message_handler),
467  {
468  }
469 
470  const guarded_range_domaint &
471  get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
472  {
473  PRECONDITION(
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 
486  rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
487  }
488 
490  const irep_idt &function,
492  const typet &type) override
493  {
494  rw_range_sett::get_objects_rec(function, target, type);
495  }
496 
497 protected:
500 
502 
503  void get_objects_if(
504  get_modet mode,
505  const if_exprt &if_expr,
506  const range_spect &range_start,
507  const range_spect &size) override;
508 
509  void add(
510  get_modet mode,
511  const irep_idt &identifier,
512  const range_spect &range_start,
513  const range_spect &range_end) override;
514 };
515 
516 #endif // CPROVER_ANALYSES_GOTO_RW_H
Array constructor from list of elements.
Definition: std_expr.h:1616
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:2022
Real part of the expression describing a complex number.
Definition: std_expr.h:1979
Operator to dereference a pointer.
Definition: pointer_expr.h:834
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.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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
iterator end()
Definition: goto_rw.h:441
iterator begin()
Definition: goto_rw.h:437
The trinary if-then-else operator.
Definition: std_expr.h:2370
Array index operator.
Definition: std_expr.h:1465
Extract member of struct or union.
Definition: std_expr.h:2844
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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
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
friend std::ostream & operator<<(std::ostream &, const range_spect &)
Definition: goto_rw.h:167
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
range_spect & operator-=(const range_spect &other)
Definition: goto_rw.h:148
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
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
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
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:471
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
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:234
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_r_set() const
Definition: goto_rw.h:215
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
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
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:226
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
const objectst & get_w_set() const
Definition: goto_rw.h:220
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
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:1872
The Boolean constant true.
Definition: std_expr.h:3063
Semantic type conversion.
Definition: std_expr.h:2068
The type of an expression, extends irept.
Definition: type.h:29
Concrete Goto Program.
std::ostream & operator<<(std::ostream &os, const range_spect &r)
Definition: goto_rw.h:167
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:867
Guard Data Structure.
guard_exprt guardt
Definition: guard.h:29
static int8_t r
Definition: irep_hash.h:60
BigInt::llong_t llong_t
Definition: mp_arith.cpp:20
get_modet
Definition: object_id.cpp:18
BigInt mp_integer
Definition: smt_terms.h:17
#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