cprover
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 
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 
57 typedef 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 
74 public:
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 
94 class byte_extract_exprt;
95 class dereference_exprt;
96 class shift_exprt;
97 
99 {
100 public:
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 
153 protected:
154  const namespacet &ns;
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 
247 inline 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 
255 class value_setst;
256 
258 {
259 public:
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 
277  rw_range_sett::get_objects_rec(mode, expr);
278  }
279 
281  const irep_idt &_function,
283  const typet &type) override
284  {
285  function = _function;
286  target = _target;
287 
289  }
290 
291 protected:
293  irep_idt function;
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 
310 public:
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 {
339 public:
341  const namespacet &_ns,
342  value_setst &_value_sets,
344  : rw_range_set_value_sett(_ns, _value_sets),
347  {
348  }
349 
350  const guarded_range_domaint &
351  get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
352  {
353  PRECONDITION(
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  {
374  rw_range_sett::get_objects_rec(function, target, type);
375  }
376 
377 protected:
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:1467
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:1820
Real part of the expression describing a complex number.
Definition: std_expr.h:1775
Operator to dereference a pointer.
Definition: pointer_expr.h:628
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:71
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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:656
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:2172
Array index operator.
Definition: std_expr.h:1328
Extract member of struct or union.
Definition: std_expr.h:2613
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
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:674
guard_managert & guard_manager
Definition: goto_rw.h:378
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:351
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition: goto_rw.cpp:700
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:616
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
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:134
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:132
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_r_set() const
Definition: goto_rw.h:115
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:171
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:249
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:338
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:113
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:427
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
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:126
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:217
const namespacet & ns
Definition: goto_rw.h:154
const objectst & get_w_set() const
Definition: goto_rw.h:120
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:479
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:401
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition: goto_rw.h:105
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:296
A base class for shift and rotate operators.
Struct constructor from list of elements.
Definition: std_expr.h:1668
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
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:754
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::llong_t llong_t
Definition: mp_arith.cpp:20
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