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_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 
270  virtual void get_objects_rec(
272  get_modet mode,
273  const exprt &expr)
274  {
275  target=_target;
276 
277  rw_range_sett::get_objects_rec(mode, expr);
278  }
279 
280 protected:
282 
284 
285  virtual void get_objects_dereference(
286  get_modet mode,
287  const dereference_exprt &deref,
288  const range_spect &range_start,
289  const range_spect &size);
290 };
291 
293 {
294  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
296 
297 public:
298  virtual void output(const namespacet &ns, std::ostream &out) const override;
299 
300  // NOLINTNEXTLINE(readability/identifiers)
301  typedef sub_typet::iterator iterator;
302  // NOLINTNEXTLINE(readability/identifiers)
303  typedef sub_typet::const_iterator const_iterator;
304 
305  iterator begin() { return data.begin(); }
306  const_iterator begin() const { return data.begin(); }
307  const_iterator cbegin() const { return data.begin(); }
308 
309  iterator end() { return data.end(); }
310  const_iterator end() const { return data.end(); }
311  const_iterator cend() const { return data.end(); }
312 
313  iterator insert(const sub_typet::value_type &v)
314  {
315  return data.insert(v);
316  }
317 
318  iterator insert(sub_typet::value_type &&v)
319  {
320  return data.insert(std::move(v));
321  }
322 };
323 
325 {
326 public:
328  const namespacet &_ns,
329  value_setst &_value_sets):
330  rw_range_set_value_sett(_ns, _value_sets)
331  {
332  }
333 
334  const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
335  {
336  PRECONDITION(
337  dynamic_cast<guarded_range_domaint*>(it->second.get())!=nullptr);
338  return static_cast<const guarded_range_domaint &>(*it->second);
339  }
340 
341  virtual void get_objects_rec(
343  get_modet mode,
344  const exprt &expr)
345  {
346  guard = true_exprt();
347 
348  rw_range_set_value_sett::get_objects_rec(_target, mode, expr);
349  }
350 
351 protected:
353 
355 
356  virtual void get_objects_if(
357  get_modet mode,
358  const if_exprt &if_expr,
359  const range_spect &range_start,
360  const range_spect &size);
361 
362  virtual void add(
363  get_modet mode,
364  const irep_idt &identifier,
365  const range_spect &range_start,
366  const range_spect &range_end);
367 };
368 
369 #endif // CPROVER_ANALYSES_GOTO_RW_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
rw_range_sett::get_r_set
const objectst & get_r_set() const
Definition: goto_rw.h:125
rw_range_set_value_sett::get_objects_dereference
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:618
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
rw_range_sett::get_objects_if
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
rw_range_sett::get_objects_shift
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:173
guarded_range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:303
rw_range_sett::get_objects_address_of
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:431
rw_range_sett::get_objects_array
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:299
rw_range_sett::get_objects_byte_extract
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
typet
The type of an expression, extends irept.
Definition: type.h:27
rw_range_sett::get_objects_dereference
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
goto_rw
void goto_rw(goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:749
rw_guarded_range_set_value_sett::guard
guardt guard
Definition: goto_rw.h:352
guarded_range_domaint::begin
iterator begin()
Definition: goto_rw.h:305
rw_range_sett::get_modet::LHS_W
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
guarded_range_domaint::cbegin
const_iterator cbegin() const
Definition: goto_rw.h:307
data
Definition: kdev_t.h:24
rw_range_sett::get_objects_typecast
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:405
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
guarded_range_domaint::sub_typet
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition: goto_rw.h:294
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:2040
guarded_range_domaint::data
sub_typet data
Definition: goto_rw.h:295
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
rw_range_sett::~rw_range_sett
virtual ~rw_range_sett()
Definition: goto_rw.cpp:51
string_hash
Definition: string_hash.h:21
irep_idt
dstringt irep_idt
Definition: irep.h:32
guarded_range_domaint::end
const_iterator end() const
Definition: goto_rw.h:310
rw_range_sett::get_objects_struct
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:342
rw_range_set_value_sett
Definition: goto_rw.h:257
range_domaint::output
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:37
guarded_range_domaint::cend
const_iterator cend() const
Definition: goto_rw.h:311
rw_range_sett::get_objects_member
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:219
to_range_spect
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:63
guarded_range_domaint::insert
iterator insert(const sub_typet::value_type &v)
Definition: goto_rw.h:313
rw_guarded_range_set_value_sett::add
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:702
range_domaint::end
const_iterator end() const
Definition: goto_rw.h:91
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
guard.h
range_domaint::sub_typet
std::list< std::pair< range_spect, range_spect > > sub_typet
Definition: goto_rw.h:75
guardt
Definition: guard.h:19
rw_range_sett::get_objects_rec
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:143
rw_range_set_value_sett::value_sets
value_setst & value_sets
Definition: goto_rw.h:281
rw_range_sett
Definition: goto_rw.h:108
range_domain_baset::range_domain_baset
range_domain_baset()=default
rw_range_sett::rw_range_sett
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:120
range_domain_baset
Definition: goto_rw.h:45
range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:87
range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:82
rw_guarded_range_set_value_sett::get_objects_if
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:676
guarded_range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:301
rw_range_sett::add
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:481
llong_t
BigInt::llong_t llong_t
Definition: mp_arith.cpp:23
rw_range_sett::get_objects_complex_imag
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:94
rw_range_sett::get_objects_index
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:252
range_domain_baset::~range_domain_baset
virtual ~range_domain_baset()
Definition: goto_rw.cpp:33
range_domaint::push_back
void push_back(const sub_typet::value_type &v)
Definition: goto_rw.h:94
rw_range_set_value_sett::target
goto_programt::const_targett target
Definition: goto_rw.h:283
range_domaint::cbegin
const_iterator cbegin() const
Definition: goto_rw.h:88
rw_range_sett::output
void output(std::ostream &out) const
Definition: goto_rw.cpp:64
range_domaint::data
sub_typet data
Definition: goto_rw.h:76
operator<<
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:247
rw_guarded_range_set_value_sett::get_objects_rec
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:341
range_spect
int range_spect
Definition: goto_rw.h:61
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
rw_range_sett::w_range_set
objectst w_range_set
Definition: goto_rw.h:158
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
guarded_range_domaint
Definition: goto_rw.h:292
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2866
value_setst
Definition: value_sets.h:21
rw_range_set_value_sett::get_objects_rec
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:270
rw_range_sett::ns
const namespacet & ns
Definition: goto_rw.h:156
rw_guarded_range_set_value_sett
Definition: goto_rw.h:324
guarded_range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:306
guarded_range_domaint::end
iterator end()
Definition: goto_rw.h:309
rw_guarded_range_set_value_sett::rw_guarded_range_set_value_sett
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:327
rw_range_set_value_sett::rw_range_set_value_sett
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:260
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2087
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
rw_range_sett::objectst
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition: goto_rw.h:115
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
range_domain_baset::output
virtual void output(const namespacet &ns, std::ostream &out) const =0
rw_range_sett::get_objects_complex_real
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:85
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
guarded_range_domaint::output
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:658
range_domaint::push_back
void push_back(sub_typet::value_type &&v)
Definition: goto_rw.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1595
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:84
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
rw_range_sett::get_w_set
const objectst & get_w_set() const
Definition: goto_rw.h:130
rw_range_sett::get_ranges
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:135
range_domaint::begin
iterator begin()
Definition: goto_rw.h:86
rw_range_sett::get_modet::READ
rw_range_sett::get_modet
get_modet
Definition: goto_rw.h:141
guarded_range_domaint::insert
iterator insert(sub_typet::value_type &&v)
Definition: goto_rw.h:318
rw_range_sett::r_range_set
objectst r_range_set
Definition: goto_rw.h:158
range_domaint::end
iterator end()
Definition: goto_rw.h:90
range_domaint
Definition: goto_rw.h:73
range_domaint::cend
const_iterator cend() const
Definition: goto_rw.h:92
rw_guarded_range_set_value_sett::get_ranges
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:334
range_domain_baset::operator=
range_domain_baset & operator=(const range_domain_baset &rhs)=delete