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 #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 
35 void goto_rw(
36  const irep_idt &function,
38  rw_range_sett &rw_set);
39 
40 void goto_rw(
41  const irep_idt &function,
42  const goto_programt &,
43  rw_range_sett &rw_set);
44 
45 void goto_rw(const goto_functionst &,
46  const irep_idt &function,
47  rw_range_sett &rw_set);
48 
50 {
51 public:
52  range_domain_baset()=default;
53 
56 
59 
60  virtual ~range_domain_baset();
61 
62  virtual void output(const namespacet &ns, std::ostream &out) const=0;
63 };
64 
65 typedef int range_spect;
66 
68 {
69  assert(size.is_long());
70  mp_integer::llong_t ll=size.to_long();
71  assert(ll<=std::numeric_limits<range_spect>::max());
72  assert(ll>=std::numeric_limits<range_spect>::min());
73  return (range_spect)ll;
74 }
75 
76 // each element x represents a range of bits [x.first, x.second.first)
78 {
79  typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
81 
82 public:
83  void output(const namespacet &ns, std::ostream &out) const override;
84 
85  // NOLINTNEXTLINE(readability/identifiers)
86  typedef sub_typet::iterator iterator;
87  // NOLINTNEXTLINE(readability/identifiers)
88  typedef sub_typet::const_iterator const_iterator;
89 
90  iterator begin() { return data.begin(); }
91  const_iterator begin() const { return data.begin(); }
92  const_iterator cbegin() const { return data.begin(); }
93 
94  iterator end() { return data.end(); }
95  const_iterator end() const { return data.end(); }
96  const_iterator cend() const { return data.end(); }
97 
98  void push_back(const sub_typet::value_type &v) { data.push_back(v); }
99  void push_back(sub_typet::value_type &&v) { data.push_back(std::move(v)); }
100 };
101 
102 class array_exprt;
103 class byte_extract_exprt;
104 class dereference_exprt;
105 class if_exprt;
106 class index_exprt;
107 class member_exprt;
108 class shift_exprt;
109 class struct_exprt;
110 class typecast_exprt;
111 
113 {
114 public:
115  #ifdef USE_DSTRING
116  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
117  #else
118  typedef std::unordered_map<
119  irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
120  #endif
121 
122  virtual ~rw_range_sett();
123 
124  explicit rw_range_sett(const namespacet &_ns):
125  ns(_ns)
126  {
127  }
128 
129  const objectst &get_r_set() const
130  {
131  return r_range_set;
132  }
133 
134  const objectst &get_w_set() const
135  {
136  return w_range_set;
137  }
138 
139  const range_domaint &get_ranges(objectst::const_iterator it) const
140  {
141  PRECONDITION(dynamic_cast<range_domaint*>(it->second.get())!=nullptr);
142  return static_cast<const range_domaint &>(*it->second);
143  }
144 
145  enum class get_modet { LHS_W, READ };
146 
147  virtual void get_objects_rec(
148  const irep_idt &,
150  get_modet mode,
151  const exprt &expr)
152  {
153  get_objects_rec(mode, expr);
154  }
155 
156  virtual void get_objects_rec(
157  const irep_idt &,
159  const typet &type)
160  {
161  get_objects_rec(type);
162  }
163 
164  void output(std::ostream &out) const;
165 
166 protected:
167  const namespacet &ns;
168 
170 
171  virtual void get_objects_rec(
172  get_modet mode,
173  const exprt &expr);
174 
175  virtual void get_objects_rec(const typet &type);
176 
177  virtual void get_objects_complex_real(
178  get_modet mode,
179  const complex_real_exprt &expr,
180  const range_spect &range_start,
181  const range_spect &size);
182 
183  virtual void get_objects_complex_imag(
184  get_modet mode,
185  const complex_imag_exprt &expr,
186  const range_spect &range_start,
187  const range_spect &size);
188 
189  virtual void get_objects_if(
190  get_modet mode,
191  const if_exprt &if_expr,
192  const range_spect &range_start,
193  const range_spect &size);
194 
195  // overload to include expressions read/written
196  // through dereferencing
197  virtual void get_objects_dereference(
198  get_modet mode,
199  const dereference_exprt &deref,
200  const range_spect &range_start,
201  const range_spect &size);
202 
203  virtual void get_objects_byte_extract(
204  get_modet mode,
205  const byte_extract_exprt &be,
206  const range_spect &range_start,
207  const range_spect &size);
208 
209  virtual void get_objects_shift(
210  get_modet mode,
211  const shift_exprt &shift,
212  const range_spect &range_start,
213  const range_spect &size);
214 
215  virtual void get_objects_member(
216  get_modet mode,
217  const member_exprt &expr,
218  const range_spect &range_start,
219  const range_spect &size);
220 
221  virtual void get_objects_index(
222  get_modet mode,
223  const index_exprt &expr,
224  const range_spect &range_start,
225  const range_spect &size);
226 
227  virtual void get_objects_array(
228  get_modet mode,
229  const array_exprt &expr,
230  const range_spect &range_start,
231  const range_spect &size);
232 
233  virtual void get_objects_struct(
234  get_modet mode,
235  const struct_exprt &expr,
236  const range_spect &range_start,
237  const range_spect &size);
238 
239  virtual void get_objects_typecast(
240  get_modet mode,
241  const typecast_exprt &tc,
242  const range_spect &range_start,
243  const range_spect &size);
244 
245  virtual void get_objects_address_of(const exprt &object);
246 
247  virtual void get_objects_rec(
248  get_modet mode,
249  const exprt &expr,
250  const range_spect &range_start,
251  const range_spect &size);
252 
253  virtual void add(
254  get_modet mode,
255  const irep_idt &identifier,
256  const range_spect &range_start,
257  const range_spect &range_end);
258 };
259 
260 inline std::ostream &operator << (
261  std::ostream &out,
262  const rw_range_sett &rw_set)
263 {
264  rw_set.output(out);
265  return out;
266 }
267 
268 class value_setst;
269 
271 {
272 public:
274  const namespacet &_ns,
275  value_setst &_value_sets):
276  rw_range_sett(_ns),
277  value_sets(_value_sets)
278  {
279  }
280 
282  const irep_idt &_function,
284  get_modet mode,
285  const exprt &expr) override
286  {
287  function = _function;
288  target=_target;
289 
290  rw_range_sett::get_objects_rec(mode, expr);
291  }
292 
294  const irep_idt &_function,
296  const typet &type) override
297  {
298  function = _function;
299  target = _target;
300 
302  }
303 
304 protected:
306  irep_idt function;
308 
310 
312  get_modet mode,
313  const dereference_exprt &deref,
314  const range_spect &range_start,
315  const range_spect &size) override;
316 };
317 
319 {
320  typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
322 
323 public:
324  virtual void output(const namespacet &ns, std::ostream &out) const override;
325 
326  // NOLINTNEXTLINE(readability/identifiers)
327  typedef sub_typet::iterator iterator;
328  // NOLINTNEXTLINE(readability/identifiers)
329  typedef sub_typet::const_iterator const_iterator;
330 
331  iterator begin() { return data.begin(); }
332  const_iterator begin() const { return data.begin(); }
333  const_iterator cbegin() const { return data.begin(); }
334 
335  iterator end() { return data.end(); }
336  const_iterator end() const { return data.end(); }
337  const_iterator cend() const { return data.end(); }
338 
339  iterator insert(const sub_typet::value_type &v)
340  {
341  return data.insert(v);
342  }
343 
344  iterator insert(sub_typet::value_type &&v)
345  {
346  return data.insert(std::move(v));
347  }
348 };
349 
351 {
352 public:
354  const namespacet &_ns,
355  value_setst &_value_sets,
357  : rw_range_set_value_sett(_ns, _value_sets),
360  {
361  }
362 
363  const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
364  {
365  PRECONDITION(
366  dynamic_cast<guarded_range_domaint*>(it->second.get())!=nullptr);
367  return static_cast<const guarded_range_domaint &>(*it->second);
368  }
369 
371  const irep_idt &_function,
373  get_modet mode,
374  const exprt &expr) override
375  {
377 
378  rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
379  }
380 
382  const irep_idt &function,
384  const typet &type) override
385  {
386  rw_range_sett::get_objects_rec(function, target, type);
387  }
388 
389 protected:
392 
394 
395  void get_objects_if(
396  get_modet mode,
397  const if_exprt &if_expr,
398  const range_spect &range_start,
399  const range_spect &size) override;
400 
401  void add(
402  get_modet mode,
403  const irep_idt &identifier,
404  const range_spect &range_start,
405  const range_spect &range_end) override;
406 };
407 
408 #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:129
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:172
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:329
rw_range_sett::get_objects_address_of
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:428
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:297
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:29
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:293
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
rw_guarded_range_set_value_sett::guard
guardt guard
Definition: goto_rw.h:391
guarded_range_domaint::begin
iterator begin()
Definition: goto_rw.h:331
rw_range_sett::get_modet::LHS_W
@ LHS_W
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
rw_guarded_range_set_value_sett::guard_manager
guard_managert & guard_manager
Definition: goto_rw.h:390
guarded_range_domaint::cbegin
const_iterator cbegin() const
Definition: goto_rw.h:333
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:402
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
guarded_range_domaint::sub_typet
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Definition: goto_rw.h:320
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1740
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:381
guarded_range_domaint::data
sub_typet data
Definition: goto_rw.h:321
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
rw_range_sett::~rw_range_sett
virtual ~rw_range_sett()
Definition: goto_rw.cpp:51
string_hash
Definition: string_hash.h:22
irep_idt
dstringt irep_idt
Definition: irep.h:32
guarded_range_domaint::end
const_iterator end() const
Definition: goto_rw.h:336
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:339
rw_range_set_value_sett
Definition: goto_rw.h:271
range_domaint::output
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:37
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:337
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:218
to_range_spect
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:67
guarded_range_domaint::insert
iterator insert(const sub_typet::value_type &v)
Definition: goto_rw.h:339
range_domaint::end
const_iterator end() const
Definition: goto_rw.h:95
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
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:147
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:370
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:79
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:621
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:147
rw_range_set_value_sett::value_sets
value_setst & value_sets
Definition: goto_rw.h:305
rw_range_sett
Definition: goto_rw.h:113
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:281
rw_range_sett::rw_range_sett
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:124
range_domain_baset
Definition: goto_rw.h:50
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:91
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:705
range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:86
guarded_range_domaint::iterator
sub_typet::iterator iterator
Definition: goto_rw.h:327
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:484
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
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:250
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:98
rw_range_set_value_sett::target
goto_programt::const_targett target
Definition: goto_rw.h:307
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:92
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:80
operator<<
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:260
range_spect
int range_spect
Definition: goto_rw.h:65
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
rw_range_sett::w_range_set
objectst w_range_set
Definition: goto_rw.h:169
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
guarded_range_domaint
Definition: goto_rw.h:319
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2496
value_setst
Definition: value_sets.h:22
rw_range_sett::ns
const namespacet & ns
Definition: goto_rw.h:167
rw_guarded_range_set_value_sett
Definition: goto_rw.h:351
guarded_range_domaint::begin
const_iterator begin() const
Definition: goto_rw.h:332
guarded_range_domaint::end
iterator end()
Definition: goto_rw.h:335
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:273
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1785
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:119
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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:580
guarded_range_domaint::output
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:661
range_domaint::push_back
void push_back(sub_typet::value_type &&v)
Definition: goto_rw.h:99
index_exprt
Array index operator.
Definition: std_expr.h:1293
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
range_domaint::const_iterator
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:88
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
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:679
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
rw_range_sett::get_w_set
const objectst & get_w_set() const
Definition: goto_rw.h:134
rw_range_sett::get_ranges
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:139
range_domaint::begin
iterator begin()
Definition: goto_rw.h:90
rw_range_sett::get_modet::READ
@ READ
rw_range_sett::get_modet
get_modet
Definition: goto_rw.h:145
guarded_range_domaint::insert
iterator insert(sub_typet::value_type &&v)
Definition: goto_rw.h:344
rw_range_sett::r_range_set
objectst r_range_set
Definition: goto_rw.h:169
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:353
range_domaint::end
iterator end()
Definition: goto_rw.h:94
range_domaint
Definition: goto_rw.h:78
range_domaint::cend
const_iterator cend() const
Definition: goto_rw.h:96
rw_guarded_range_set_value_sett::get_ranges
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:363
range_domain_baset::operator=
range_domain_baset & operator=(const range_domain_baset &rhs)=delete