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 <limits>
17 #include <map>
18 #include <memory> // unique_ptr
19 
20 #include <util/guard.h>
21 
23 
24 #define forall_rw_range_set_r_objects(it, rw_set) \
25  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \
26  it!=(rw_set).get_r_set().end(); ++it)
27 
28 #define forall_rw_range_set_w_objects(it, rw_set) \
29  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \
30  it!=(rw_set).get_w_set().end(); ++it)
31 
32 class rw_range_sett;
33 class goto_modelt;
34 
36  rw_range_sett &rw_set);
37 
38 void goto_rw(const goto_programt &,
39  rw_range_sett &rw_set);
40 
41 void goto_rw(const goto_functionst &,
42  const irep_idt &function,
43  rw_range_sett &rw_set);
44 
46 {
47 public:
48  range_domain_baset()=default;
49 
50  range_domain_baset(const range_domain_baset &rhs)=delete;
52 
55 
56  virtual ~range_domain_baset();
57 
58  virtual void output(const namespacet &ns, std::ostream &out) const=0;
59 };
60 
61 typedef int range_spect;
62 
64 {
65  assert(size.is_long());
66  mp_integer::llong_t ll=size.to_long();
67  assert(ll<=std::numeric_limits<range_spect>::max());
68  assert(ll>=std::numeric_limits<range_spect>::min());
69  return (range_spect)ll;
70 }
71 
72 // each element x represents a range of bits [x.first, x.second.first)
74 {
75  typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
77 
78 public:
79  void output(const namespacet &ns, std::ostream &out) const override;
80 
81  // NOLINTNEXTLINE(readability/identifiers)
82  typedef sub_typet::iterator iterator;
83  // NOLINTNEXTLINE(readability/identifiers)
84  typedef sub_typet::const_iterator const_iterator;
85 
86  iterator begin() { return data.begin(); }
87  const_iterator begin() const { return data.begin(); }
88  const_iterator cbegin() const { return data.begin(); }
89 
90  iterator end() { return data.end(); }
91  const_iterator end() const { return data.end(); }
92  const_iterator cend() const { return data.end(); }
93 
94  void push_back(const sub_typet::value_type &v) { data.push_back(v); }
95  void push_back(sub_typet::value_type &&v) { data.push_back(std::move(v)); }
96 };
97 
98 class array_exprt;
99 class byte_extract_exprt;
100 class dereference_exprt;
101 class if_exprt;
102 class index_exprt;
103 class member_exprt;
104 class shift_exprt;
105 class struct_exprt;
106 class typecast_exprt;
107 
109 {
110 public:
111  #ifdef USE_DSTRING
112  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
113  #else
114  typedef std::unordered_map<
115  irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
116  #endif
117 
118  virtual ~rw_range_sett();
119 
120  explicit rw_range_sett(const namespacet &_ns):
121  ns(_ns)
122  {
123  }
124 
125  const objectst &get_r_set() const
126  {
127  return r_range_set;
128  }
129 
130  const objectst &get_w_set() const
131  {
132  return w_range_set;
133  }
134 
135  const range_domaint &get_ranges(objectst::const_iterator it) const
136  {
137  PRECONDITION(dynamic_cast<range_domaint*>(it->second.get())!=nullptr);
138  return static_cast<const range_domaint &>(*it->second);
139  }
140 
141  enum class get_modet { LHS_W, READ };
142 
143  virtual void get_objects_rec(
145  get_modet mode,
146  const exprt &expr)
147  {
148  get_objects_rec(mode, expr);
149  }
150 
151  virtual void get_objects_rec(const typet &type);
152 
153  void output(std::ostream &out) const;
154 
155 protected:
156  const namespacet &ns;
157 
159 
160  virtual void get_objects_rec(
161  get_modet mode,
162  const exprt &expr);
163 
164  virtual void get_objects_complex(
165  get_modet mode,
166  const exprt &expr,
167  const range_spect &range_start,
168  const range_spect &size);
169 
170  virtual void get_objects_if(
171  get_modet mode,
172  const if_exprt &if_expr,
173  const range_spect &range_start,
174  const range_spect &size);
175 
176  // overload to include expressions read/written
177  // through dereferencing
178  virtual void get_objects_dereference(
179  get_modet mode,
180  const dereference_exprt &deref,
181  const range_spect &range_start,
182  const range_spect &size);
183 
184  virtual void get_objects_byte_extract(
185  get_modet mode,
186  const byte_extract_exprt &be,
187  const range_spect &range_start,
188  const range_spect &size);
189 
190  virtual void get_objects_shift(
191  get_modet mode,
192  const shift_exprt &shift,
193  const range_spect &range_start,
194  const range_spect &size);
195 
196  virtual void get_objects_member(
197  get_modet mode,
198  const member_exprt &expr,
199  const range_spect &range_start,
200  const range_spect &size);
201 
202  virtual void get_objects_index(
203  get_modet mode,
204  const index_exprt &expr,
205  const range_spect &range_start,
206  const range_spect &size);
207 
208  virtual void get_objects_array(
209  get_modet mode,
210  const array_exprt &expr,
211  const range_spect &range_start,
212  const range_spect &size);
213 
214  virtual void get_objects_struct(
215  get_modet mode,
216  const struct_exprt &expr,
217  const range_spect &range_start,
218  const range_spect &size);
219 
220  virtual void get_objects_typecast(
221  get_modet mode,
222  const typecast_exprt &tc,
223  const range_spect &range_start,
224  const range_spect &size);
225 
226  virtual void get_objects_address_of(const exprt &object);
227 
228  virtual void get_objects_rec(
229  get_modet mode,
230  const exprt &expr,
231  const range_spect &range_start,
232  const range_spect &size);
233 
234  virtual void add(
235  get_modet mode,
236  const irep_idt &identifier,
237  const range_spect &range_start,
238  const range_spect &range_end);
239 };
240 
241 inline std::ostream &operator << (
242  std::ostream &out,
243  const rw_range_sett &rw_set)
244 {
245  rw_set.output(out);
246  return out;
247 }
248 
249 class value_setst;
250 
252 {
253 public:
255  const namespacet &_ns,
256  value_setst &_value_sets):
257  rw_range_sett(_ns),
258  value_sets(_value_sets)
259  {
260  }
261 
263 
264  virtual void get_objects_rec(
266  get_modet mode,
267  const exprt &expr)
268  {
269  target=_target;
270 
271  rw_range_sett::get_objects_rec(mode, expr);
272  }
273 
274 protected:
276 
278 
279  virtual void get_objects_dereference(
280  get_modet mode,
281  const dereference_exprt &deref,
282  const range_spect &range_start,
283  const range_spect &size);
284 };
285 
287 {
288  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
290 
291 public:
292  virtual void output(const namespacet &ns, std::ostream &out) const override;
293 
294  // NOLINTNEXTLINE(readability/identifiers)
295  typedef sub_typet::iterator iterator;
296  // NOLINTNEXTLINE(readability/identifiers)
297  typedef sub_typet::const_iterator const_iterator;
298 
299  iterator begin() { return data.begin(); }
300  const_iterator begin() const { return data.begin(); }
301  const_iterator cbegin() const { return data.begin(); }
302 
303  iterator end() { return data.end(); }
304  const_iterator end() const { return data.end(); }
305  const_iterator cend() const { return data.end(); }
306 
307  iterator insert(const sub_typet::value_type &v)
308  {
309  return data.insert(v);
310  }
311 
312  iterator insert(sub_typet::value_type &&v)
313  {
314  return data.insert(std::move(v));
315  }
316 };
317 
319 {
320 public:
322  const namespacet &_ns,
323  value_setst &_value_sets):
324  rw_range_set_value_sett(_ns, _value_sets)
325  {
326  }
327 
328  const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
329  {
330  PRECONDITION(
331  dynamic_cast<guarded_range_domaint*>(it->second.get())!=nullptr);
332  return static_cast<const guarded_range_domaint &>(*it->second);
333  }
334 
335  virtual void get_objects_rec(
337  get_modet mode,
338  const exprt &expr)
339  {
340  guard.make_true();
341 
342  rw_range_set_value_sett::get_objects_rec(_target, mode, expr);
343  }
344 
345 protected:
347 
349 
350  virtual void get_objects_if(
351  get_modet mode,
352  const if_exprt &if_expr,
353  const range_spect &range_start,
354  const range_spect &size);
355 
356  virtual void add(
357  get_modet mode,
358  const irep_idt &identifier,
359  const range_spect &range_start,
360  const range_spect &range_end);
361 };
362 
363 #endif // CPROVER_ANALYSES_GOTO_RW_H
The type of an expression.
Definition: type.h:22
goto_programt::const_targett target
Definition: goto_rw.h:277
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:84
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:328
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:120
iterator begin()
Definition: goto_rw.h:299
const_iterator cbegin() const
Definition: goto_rw.h:301
value_setst & value_sets
Definition: goto_rw.h:275
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:297
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:241
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:63
virtual ~rw_range_sett()
Definition: goto_rw.cpp:51
int range_spect
Definition: goto_rw.h:61
const_iterator end() const
Definition: goto_rw.h:91
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:592
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:209
The trinary if-then-else operator.
Definition: std_expr.h:3359
const_iterator end() const
Definition: goto_rw.h:304
std::list< std::pair< range_spect, range_spect > > sub_typet
Definition: goto_rw.h:75
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:239
Definition: guard.h:19
virtual void get_objects_complex(get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:85
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition: goto_rw.h:288
const_iterator cend() const
Definition: goto_rw.h:305
virtual void output(const namespacet &ns, std::ostream &out) const =0
const objectst & get_w_set() const
Definition: goto_rw.h:130
const_iterator cbegin() const
Definition: goto_rw.h:88
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:329
objectst r_range_set
Definition: goto_rw.h:158
iterator end()
Definition: goto_rw.h:90
Extract member of struct or union.
Definition: std_expr.h:3869
void make_true()
Definition: expr.cpp:144
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:37
void goto_rw(goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:715
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:642
objectst w_range_set
Definition: goto_rw.h:158
Symbol Table + CFG.
iterator insert(const sub_typet::value_type &v)
Definition: goto_rw.h:307
const namespacet & ns
Definition: goto_rw.h:156
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:414
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:464
Operator to dereference a pointer.
Definition: std_expr.h:3282
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:321
sub_typet data
Definition: goto_rw.h:76
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:134
sub_typet::iterator iterator
Definition: goto_rw.h:295
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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:103
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const_iterator cend() const
Definition: goto_rw.h:92
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:143
Guard Data Structure.
BigInt::llong_t llong_t
Definition: mp_arith.cpp:23
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:161
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:668
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:254
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:289
void push_back(const sub_typet::value_type &v)
Definition: goto_rw.h:94
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
const objectst & get_r_set() const
Definition: goto_rw.h:125
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:389
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:122
const_iterator begin() const
Definition: goto_rw.h:300
iterator end()
Definition: goto_rw.h:303
Base class for all expressions.
Definition: expr.h:42
const_iterator begin() const
Definition: goto_rw.h:87
void push_back(sub_typet::value_type &&v)
Definition: goto_rw.h:95
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:624
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:335
range_domain_baset & operator=(const range_domain_baset &rhs)=delete
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:135
dstringt irep_idt
Definition: irep.h:32
sub_typet::iterator iterator
Definition: goto_rw.h:82
virtual ~range_domain_baset()
Definition: goto_rw.cpp:33
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:264
range_domain_baset()=default
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1815
iterator insert(sub_typet::value_type &&v)
Definition: goto_rw.h:312
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition: goto_rw.h:115
A base class for shift operators.
Definition: std_expr.h:2765
void output(std::ostream &out) const
Definition: goto_rw.cpp:64
array constructor from list of elements
Definition: std_expr.h:1617
Definition: kdev_t.h:24
iterator begin()
Definition: goto_rw.h:86
array index operator
Definition: std_expr.h:1462