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 <map>
16 #include <ostream>
17 #include <limits>
18 
19 #include <util/guard.h>
20 
22 
23 #define forall_rw_range_set_r_objects(it, rw_set) \
24  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \
25  it!=(rw_set).get_r_set().end(); ++it)
26 
27 #define forall_rw_range_set_w_objects(it, rw_set) \
28  for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \
29  it!=(rw_set).get_w_set().end(); ++it)
30 
31 class rw_range_sett;
32 class goto_functionst;
33 
35  rw_range_sett &rw_set);
36 
37 void goto_rw(const goto_programt &goto_program,
38  rw_range_sett &rw_set);
39 
40 void goto_rw(const goto_functionst &goto_functions,
41  const irep_idt &function,
42  rw_range_sett &rw_set);
43 
45 {
46 public:
47  virtual ~range_domain_baset();
48 
49  virtual void output(const namespacet &ns, std::ostream &out) const=0;
50 };
51 
52 typedef int range_spect;
53 
55 {
56  assert(size.is_long());
57  mp_integer::llong_t ll=size.to_long();
58  assert(ll<=std::numeric_limits<range_spect>::max());
59  assert(ll>=std::numeric_limits<range_spect>::min());
60  return (range_spect)ll;
61 }
62 
63 // each element x represents a range of bits [x.first, x.second.first)
65  public range_domain_baset,
66  public std::list<std::pair<range_spect, range_spect> >
67 {
68 public:
69  virtual void output(const namespacet &ns, std::ostream &out) const;
70 };
71 
72 class array_exprt;
73 class byte_extract_exprt;
74 class dereference_exprt;
75 class if_exprt;
76 class index_exprt;
77 class member_exprt;
78 class shift_exprt;
79 class struct_exprt;
80 class typecast_exprt;
81 
83 {
84 public:
85  #ifdef USE_DSTRING
86  typedef std::map<irep_idt, range_domain_baset*> objectst;
87  #else
88  typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash>
90  #endif
91 
92  virtual ~rw_range_sett();
93 
94  explicit rw_range_sett(const namespacet &_ns):
95  ns(_ns)
96  {
97  }
98 
99  const objectst &get_r_set() const
100  {
101  return r_range_set;
102  }
103 
104  const objectst &get_w_set() const
105  {
106  return w_range_set;
107  }
108 
109  const range_domaint &get_ranges(objectst::const_iterator it) const
110  {
111  PRECONDITION(dynamic_cast<range_domaint*>(it->second)!=nullptr);
112  return *static_cast<range_domaint*>(it->second);
113  }
114 
115  enum class get_modet { LHS_W, READ };
116 
117  virtual void get_objects_rec(
119  get_modet mode,
120  const exprt &expr)
121  {
122  get_objects_rec(mode, expr);
123  }
124 
125  virtual void get_objects_rec(const typet &type);
126 
127  void output(std::ostream &out) const;
128 
129 protected:
130  const namespacet &ns;
131 
132  objectst r_range_set, w_range_set;
133 
134  virtual void get_objects_rec(
135  get_modet mode,
136  const exprt &expr);
137 
138  virtual void get_objects_complex(
139  get_modet mode,
140  const exprt &expr,
141  const range_spect &range_start,
142  const range_spect &size);
143 
144  virtual void get_objects_if(
145  get_modet mode,
146  const if_exprt &if_expr,
147  const range_spect &range_start,
148  const range_spect &size);
149 
150  // overload to include expressions read/written
151  // through dereferencing
152  virtual void get_objects_dereference(
153  get_modet mode,
154  const dereference_exprt &deref,
155  const range_spect &range_start,
156  const range_spect &size);
157 
158  virtual void get_objects_byte_extract(
159  get_modet mode,
160  const byte_extract_exprt &be,
161  const range_spect &range_start,
162  const range_spect &size);
163 
164  virtual void get_objects_shift(
165  get_modet mode,
166  const shift_exprt &shift,
167  const range_spect &range_start,
168  const range_spect &size);
169 
170  virtual void get_objects_member(
171  get_modet mode,
172  const member_exprt &expr,
173  const range_spect &range_start,
174  const range_spect &size);
175 
176  virtual void get_objects_index(
177  get_modet mode,
178  const index_exprt &expr,
179  const range_spect &range_start,
180  const range_spect &size);
181 
182  virtual void get_objects_array(
183  get_modet mode,
184  const array_exprt &expr,
185  const range_spect &range_start,
186  const range_spect &size);
187 
188  virtual void get_objects_struct(
189  get_modet mode,
190  const struct_exprt &expr,
191  const range_spect &range_start,
192  const range_spect &size);
193 
194  virtual void get_objects_typecast(
195  get_modet mode,
196  const typecast_exprt &tc,
197  const range_spect &range_start,
198  const range_spect &size);
199 
200  virtual void get_objects_address_of(const exprt &object);
201 
202  virtual void get_objects_rec(
203  get_modet mode,
204  const exprt &expr,
205  const range_spect &range_start,
206  const range_spect &size);
207 
208  virtual void add(
209  get_modet mode,
210  const irep_idt &identifier,
211  const range_spect &range_start,
212  const range_spect &range_end);
213 };
214 
215 inline std::ostream &operator << (
216  std::ostream &out,
217  const rw_range_sett &rw_set)
218 {
219  rw_set.output(out);
220  return out;
221 }
222 
223 class value_setst;
224 
226 {
227 public:
229  const namespacet &_ns,
230  value_setst &_value_sets):
231  rw_range_sett(_ns),
232  value_sets(_value_sets)
233  {
234  }
235 
237 
238  virtual void get_objects_rec(
240  get_modet mode,
241  const exprt &expr)
242  {
243  target=_target;
244 
245  rw_range_sett::get_objects_rec(mode, expr);
246  }
247 
248 protected:
250 
252 
253  virtual void get_objects_dereference(
254  get_modet mode,
255  const dereference_exprt &deref,
256  const range_spect &range_start,
257  const range_spect &size);
258 };
259 
261  public range_domain_baset,
262  public std::multimap<range_spect, std::pair<range_spect, exprt> >
263 {
264 public:
265  virtual void output(const namespacet &ns, std::ostream &out) const;
266 };
267 
269 {
270 public:
272  const namespacet &_ns,
273  value_setst &_value_sets):
274  rw_range_set_value_sett(_ns, _value_sets)
275  {
276  }
277 
278  const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
279  {
280  PRECONDITION(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);
281  return *static_cast<guarded_range_domaint*>(it->second);
282  }
283 
284  virtual void get_objects_rec(
286  get_modet mode,
287  const exprt &expr)
288  {
289  guard.make_true();
290 
291  rw_range_set_value_sett::get_objects_rec(_target, mode, expr);
292  }
293 
294 protected:
296 
298 
299  virtual void get_objects_if(
300  get_modet mode,
301  const if_exprt &if_expr,
302  const range_spect &range_start,
303  const range_spect &size);
304 
305  virtual void add(
306  get_modet mode,
307  const irep_idt &identifier,
308  const range_spect &range_start,
309  const range_spect &range_end);
310 };
311 
312 #endif // CPROVER_ANALYSES_GOTO_RW_H
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:117
The type of an expression.
Definition: type.h:20
goto_programt::const_targett target
Definition: goto_rw.h:251
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:278
rw_range_sett(const namespacet &_ns)
Definition: goto_rw.h:94
value_setst & value_sets
Definition: goto_rw.h:249
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Definition: goto_rw.h:215
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:54
int range_spect
Definition: goto_rw.h:52
The trinary if-then-else operator.
Definition: std_expr.h:2771
Definition: guard.h:19
virtual void output(const namespacet &ns, std::ostream &out) const =0
const objectst & get_w_set() const
Definition: goto_rw.h:104
std::unordered_map< irep_idt, range_domain_baset *, string_hash > objectst
Definition: goto_rw.h:89
Extract member of struct or union.
Definition: std_expr.h:3214
void goto_rw(goto_programt::const_targett target, rw_range_sett &rw_set)
Definition: goto_rw.cpp:705
objectst w_range_set
Definition: goto_rw.h:132
instructionst::const_iterator const_targett
void get_objects_rec(get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
Definition: object_id.cpp:16
const namespacet & ns
Definition: goto_rw.h:130
Operator to dereference a pointer.
Definition: std_expr.h:2701
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:271
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
Guard Data Structure.
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Definition: goto_rw.h:228
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
const objectst & get_r_set() const
Definition: goto_rw.h:99
Base class for all expressions.
Definition: expr.h:46
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:284
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:109
virtual ~range_domain_baset()
Definition: goto_rw.cpp:28
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:238
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1464
A base class for shift operators.
Definition: std_expr.h:2227
void output(std::ostream &out) const
Definition: goto_rw.cpp:60
Concrete Goto Program.
array constructor from list of elements
Definition: std_expr.h:1309
array index operator
Definition: std_expr.h:1170