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 "guard.h"
21 
23 
24 class rw_range_sett;
25 class goto_modelt;
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 array_exprt;
95 class byte_extract_exprt;
96 class dereference_exprt;
97 class if_exprt;
98 class index_exprt;
99 class member_exprt;
100 class shift_exprt;
101 class struct_exprt;
102 class typecast_exprt;
103 
105 {
106 public:
107  #ifdef USE_DSTRING
108  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
109  #else
110  typedef std::unordered_map<
111  irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
112  #endif
113 
114  virtual ~rw_range_sett();
115 
116  explicit rw_range_sett(const namespacet &_ns):
117  ns(_ns)
118  {
119  }
120 
121  const objectst &get_r_set() const
122  {
123  return r_range_set;
124  }
125 
126  const objectst &get_w_set() const
127  {
128  return w_range_set;
129  }
130 
131  const range_domaint &
132  get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
133  {
134  PRECONDITION(dynamic_cast<range_domaint *>(ranges.get()) != nullptr);
135  return static_cast<const range_domaint &>(*ranges);
136  }
137 
138  enum class get_modet { LHS_W, READ };
139 
140  virtual void get_objects_rec(
141  const irep_idt &,
143  get_modet mode,
144  const exprt &expr)
145  {
146  get_objects_rec(mode, expr);
147  }
148 
149  virtual void get_objects_rec(
150  const irep_idt &,
152  const typet &type)
153  {
154  get_objects_rec(type);
155  }
156 
157  void output(std::ostream &out) const;
158 
159 protected:
160  const namespacet &ns;
161 
163 
164  virtual void get_objects_rec(
165  get_modet mode,
166  const exprt &expr);
167 
168  virtual void get_objects_rec(const typet &type);
169 
170  virtual void get_objects_complex_real(
171  get_modet mode,
172  const complex_real_exprt &expr,
173  const range_spect &range_start,
174  const range_spect &size);
175 
176  virtual void get_objects_complex_imag(
177  get_modet mode,
178  const complex_imag_exprt &expr,
179  const range_spect &range_start,
180  const range_spect &size);
181 
182  virtual void get_objects_if(
183  get_modet mode,
184  const if_exprt &if_expr,
185  const range_spect &range_start,
186  const range_spect &size);
187 
188  // overload to include expressions read/written
189  // through dereferencing
190  virtual void get_objects_dereference(
191  get_modet mode,
192  const dereference_exprt &deref,
193  const range_spect &range_start,
194  const range_spect &size);
195 
196  virtual void get_objects_byte_extract(
197  get_modet mode,
198  const byte_extract_exprt &be,
199  const range_spect &range_start,
200  const range_spect &size);
201 
202  virtual void get_objects_shift(
203  get_modet mode,
204  const shift_exprt &shift,
205  const range_spect &range_start,
206  const range_spect &size);
207 
208  virtual void get_objects_member(
209  get_modet mode,
210  const member_exprt &expr,
211  const range_spect &range_start,
212  const range_spect &size);
213 
214  virtual void get_objects_index(
215  get_modet mode,
216  const index_exprt &expr,
217  const range_spect &range_start,
218  const range_spect &size);
219 
220  virtual void get_objects_array(
221  get_modet mode,
222  const array_exprt &expr,
223  const range_spect &range_start,
224  const range_spect &size);
225 
226  virtual void get_objects_struct(
227  get_modet mode,
228  const struct_exprt &expr,
229  const range_spect &range_start,
230  const range_spect &size);
231 
232  virtual void get_objects_typecast(
233  get_modet mode,
234  const typecast_exprt &tc,
235  const range_spect &range_start,
236  const range_spect &size);
237 
238  virtual void get_objects_address_of(const exprt &object);
239 
240  virtual void get_objects_rec(
241  get_modet mode,
242  const exprt &expr,
243  const range_spect &range_start,
244  const range_spect &size);
245 
246  virtual void add(
247  get_modet mode,
248  const irep_idt &identifier,
249  const range_spect &range_start,
250  const range_spect &range_end);
251 };
252 
253 inline std::ostream &operator << (
254  std::ostream &out,
255  const rw_range_sett &rw_set)
256 {
257  rw_set.output(out);
258  return out;
259 }
260 
261 class value_setst;
262 
264 {
265 public:
267  const namespacet &_ns,
268  value_setst &_value_sets):
269  rw_range_sett(_ns),
270  value_sets(_value_sets)
271  {
272  }
273 
275  const irep_idt &_function,
277  get_modet mode,
278  const exprt &expr) override
279  {
280  function = _function;
281  target=_target;
282 
283  rw_range_sett::get_objects_rec(mode, expr);
284  }
285 
287  const irep_idt &_function,
289  const typet &type) override
290  {
291  function = _function;
292  target = _target;
293 
295  }
296 
297 protected:
299  irep_idt function;
301 
303 
305  get_modet mode,
306  const dereference_exprt &deref,
307  const range_spect &range_start,
308  const range_spect &size) override;
309 };
310 
312 {
313  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
315 
316 public:
317  virtual void output(const namespacet &ns, std::ostream &out) const override;
318 
319  // NOLINTNEXTLINE(readability/identifiers)
320  typedef sub_typet::iterator iterator;
321  // NOLINTNEXTLINE(readability/identifiers)
322  typedef sub_typet::const_iterator const_iterator;
323 
324  iterator begin() { return data.begin(); }
325  const_iterator begin() const { return data.begin(); }
326  const_iterator cbegin() const { return data.begin(); }
327 
328  iterator end() { return data.end(); }
329  const_iterator end() const { return data.end(); }
330  const_iterator cend() const { return data.end(); }
331 
332  iterator insert(const sub_typet::value_type &v)
333  {
334  return data.insert(v);
335  }
336 
337  iterator insert(sub_typet::value_type &&v)
338  {
339  return data.insert(std::move(v));
340  }
341 };
342 
344 {
345 public:
347  const namespacet &_ns,
348  value_setst &_value_sets,
350  : rw_range_set_value_sett(_ns, _value_sets),
353  {
354  }
355 
356  const guarded_range_domaint &
357  get_ranges(const std::unique_ptr<range_domain_baset> &ranges) const
358  {
359  PRECONDITION(
360  dynamic_cast<guarded_range_domaint *>(ranges.get()) != nullptr);
361  return static_cast<const guarded_range_domaint &>(*ranges);
362  }
363 
365  const irep_idt &_function,
367  get_modet mode,
368  const exprt &expr) override
369  {
371 
372  rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
373  }
374 
376  const irep_idt &function,
378  const typet &type) override
379  {
380  rw_range_sett::get_objects_rec(function, target, type);
381  }
382 
383 protected:
386 
388 
389  void get_objects_if(
390  get_modet mode,
391  const if_exprt &if_expr,
392  const range_spect &range_start,
393  const range_spect &size) override;
394 
395  void add(
396  get_modet mode,
397  const irep_idt &identifier,
398  const range_spect &range_start,
399  const range_spect &range_end) override;
400 };
401 
402 #endif // CPROVER_ANALYSES_GOTO_RW_H
guard_exprt
Definition: guard_expr.h:27
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
rw_range_sett::get_r_set
const objectst & get_r_set() const
Definition: goto_rw.h:121
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:116
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:174
goto_rw
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:755
guarded_range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:322
rw_range_sett::get_objects_address_of
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:430
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:147
typet
The type of an expression, extends irept.
Definition: type.h:28
rw_range_set_value_sett::get_objects_rec
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
Definition: goto_rw.h:286
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:135
rw_range_sett::get_ranges
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:132
rw_guarded_range_set_value_sett::guard
guardt guard
Definition: goto_rw.h:385
guarded_range_domaint::begin
iterator begin()
Definition: goto_rw.h:324
rw_range_sett::get_modet::LHS_W
@ LHS_W
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
rw_guarded_range_set_value_sett::guard_manager
guard_managert & guard_manager
Definition: goto_rw.h:384
guarded_range_domaint::cbegin
const_iterator cbegin() const
Definition: goto_rw.h:326
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:404
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
guarded_range_domaint::sub_typet
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition: goto_rw.h:313
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1689
rw_guarded_range_set_value_sett::get_objects_rec
void get_objects_rec(const irep_idt &function, goto_programt::const_targett target, const typet &type) override
Definition: goto_rw.h:375
guarded_range_domaint::data
sub_typet data
Definition: goto_rw.h:314
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
rw_range_sett::~rw_range_sett
virtual ~rw_range_sett()
Definition: goto_rw.cpp:53
string_hash
Definition: string_hash.h:22
irep_idt
dstringt irep_idt
Definition: irep.h:37
guarded_range_domaint::end
const_iterator end() const
Definition: goto_rw.h:329
guardt
guard_exprt guardt
Definition: guard.h:27
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:341
rw_range_set_value_sett
Definition: goto_rw.h:264
range_domaint::output
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:39
range_domain_baset::operator=
range_domain_baset & operator=(range_domain_baset &&rhs)=delete
guarded_range_domaint::cend
const_iterator cend() const
Definition: goto_rw.h:330
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:220
to_range_spect
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:59
rw_guarded_range_set_value_sett::get_ranges
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:357
guarded_range_domaint::insert
iterator insert(const sub_typet::value_type &v)
Definition: goto_rw.h:332
range_domaint::end
const_iterator end() const
Definition: goto_rw.h:87
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1582
rw_range_set_value_sett::get_objects_rec
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:140
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard.h
Guard Data Structure.
rw_guarded_range_set_value_sett::get_objects_rec
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:364
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
range_domaint::sub_typet
std::list< std::pair< range_spect, range_spect > > sub_typet
Definition: goto_rw.h:71
rw_range_set_value_sett::get_objects_dereference
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:619
rw_range_sett::get_objects_rec
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:140
rw_range_set_value_sett::value_sets
value_setst & value_sets
Definition: goto_rw.h:298
rw_range_sett
Definition: goto_rw.h:105
range_domain_baset::range_domain_baset
range_domain_baset()=default
rw_range_set_value_sett::get_objects_rec
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
Definition: goto_rw.h:274
rw_range_sett::rw_range_sett
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:116
range_domain_baset
Definition: goto_rw.h:42
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:83
rw_guarded_range_set_value_sett::add
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
Definition: goto_rw.cpp:703
range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:78
guarded_range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:320
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:482
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:96
range_domain_baset::range_domain_baset
range_domain_baset(const range_domain_baset &rhs)=delete
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:35
range_domaint::push_back
void push_back(const sub_typet::value_type &v)
Definition: goto_rw.h:90
rw_range_set_value_sett::target
goto_programt::const_targett target
Definition: goto_rw.h:300
range_domain_baset::range_domain_baset
range_domain_baset(range_domain_baset &&rhs)=delete
range_domaint::cbegin
const_iterator cbegin() const
Definition: goto_rw.h:84
rw_range_sett::output
void output(std::ostream &out) const
Definition: goto_rw.cpp:66
range_domaint::data
sub_typet data
Definition: goto_rw.h:72
operator<<
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:253
range_spect
int range_spect
Definition: goto_rw.h:57
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
rw_range_sett::w_range_set
objectst w_range_set
Definition: goto_rw.h:162
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
guarded_range_domaint
Definition: goto_rw.h:312
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
value_setst
Definition: value_sets.h:22
rw_range_sett::ns
const namespacet & ns
Definition: goto_rw.h:160
rw_guarded_range_set_value_sett
Definition: goto_rw.h:344
guarded_range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:325
guarded_range_domaint::end
iterator end()
Definition: goto_rw.h:328
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:266
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1734
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
rw_range_sett::objectst
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
Definition: goto_rw.h:111
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
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:87
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
guarded_range_domaint::output
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:659
range_domaint::push_back
void push_back(sub_typet::value_type &&v)
Definition: goto_rw.h:91
index_exprt
Array index operator.
Definition: std_expr.h:1242
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:80
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
rw_guarded_range_set_value_sett::get_objects_if
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:677
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
rw_range_sett::get_w_set
const objectst & get_w_set() const
Definition: goto_rw.h:126
range_domaint::begin
iterator begin()
Definition: goto_rw.h:82
rw_range_sett::get_modet::READ
@ READ
rw_range_sett::get_modet
get_modet
Definition: goto_rw.h:138
guarded_range_domaint::insert
iterator insert(sub_typet::value_type &&v)
Definition: goto_rw.h:337
rw_range_sett::r_range_set
objectst r_range_set
Definition: goto_rw.h:162
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, guard_managert &guard_manager)
Definition: goto_rw.h:346
range_domaint::end
iterator end()
Definition: goto_rw.h:86
range_domaint
Definition: goto_rw.h:70
range_domaint::cend
const_iterator cend() const
Definition: goto_rw.h:88
range_domain_baset::operator=
range_domain_baset & operator=(const range_domain_baset &rhs)=delete