CBMC
rw_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Race Detection for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: February 2006
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_RW_SET_H
15 #define CPROVER_GOTO_INSTRUMENT_RW_SET_H
16 
17 #include <iosfwd>
18 #include <vector>
19 #include <set>
20 
21 #include <util/std_expr.h>
22 
24 
25 #ifdef LOCAL_MAY
27 #endif
28 
29 class message_handlert;
30 class value_setst;
31 
32 // a container for read/write sets
33 
35 {
36 public:
39  {
40  }
41 
42  virtual ~rw_set_baset() = default;
43 
44  struct entryt
45  {
49 
51  const symbol_exprt &_symbol_expr,
52  const irep_idt &_object,
53  const exprt &_guard)
54  : symbol_expr(_symbol_expr), object(_object), guard(_guard)
55  {
56  }
57  };
58 
59  typedef std::unordered_map<irep_idt, entryt> entriest;
61 
62  void swap(rw_set_baset &other)
63  {
64  std::swap(other.r_entries, r_entries);
65  std::swap(other.w_entries, w_entries);
66  }
67 
69  {
70  r_entries.insert(other.r_entries.begin(), other.r_entries.end());
71  w_entries.insert(other.w_entries.begin(), other.w_entries.end());
72  return *this;
73  }
74 
75  bool empty() const
76  {
77  return r_entries.empty() && w_entries.empty();
78  }
79 
80  bool has_w_entry(irep_idt object) const
81  {
82  return w_entries.find(object)!=w_entries.end();
83  }
84 
85  bool has_r_entry(irep_idt object) const
86  {
87  return r_entries.find(object)!=r_entries.end();
88  }
89 
90  void output(std::ostream &out) const;
91 
92 protected:
93  virtual void track_deref(const entryt &, bool read)
94  {
95  (void)read; // unused parameter
96  }
97  virtual void set_track_deref() {}
98  virtual void reset_track_deref() {}
99 
100  const namespacet &ns;
102 };
103 
104 inline std::ostream &operator<<(
105  std::ostream &out, const rw_set_baset &rw_set)
106 {
107  rw_set.output(out);
108  return out;
109 }
110 
111 // a producer of read/write sets
112 
114 {
115 public:
116 #ifdef LOCAL_MAY
117  _rw_set_loct(
118  const namespacet &_ns,
119  value_setst &_value_sets,
120  const irep_idt &_function_id,
122  local_may_aliast &may,
125  value_sets(_value_sets),
126  function_id(_function_id),
127  target(_target),
128  local_may(may)
129 #else
131  const namespacet &_ns,
132  value_setst &_value_sets,
133  const irep_idt &_function_id,
137  value_sets(_value_sets),
138  function_id(_function_id),
139  target(_target)
140 #endif
141  {
142  }
143 
144 protected:
148 
149 #ifdef LOCAL_MAY
150  local_may_aliast &local_may;
151 #endif
152 
153  void read(const exprt &expr)
154  {
155  read_write_rec(expr, true, false, "", exprt::operandst());
156  }
157 
158  void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
159  {
160  read_write_rec(expr, true, false, "", guard_conjuncts);
161  }
162 
163  void write(const exprt &expr)
164  {
165  read_write_rec(expr, false, true, "", exprt::operandst());
166  }
167 
168  void compute();
169 
170  void assign(const exprt &lhs, const exprt &rhs);
171 
172  void read_write_rec(
173  const exprt &expr,
174  bool r,
175  bool w,
176  const std::string &suffix,
177  const exprt::operandst &guard_conjuncts);
178 };
179 
181 {
182 public:
183 #ifdef LOCAL_MAY
184  rw_set_loct(
185  const namespacet &_ns,
186  value_setst &_value_sets,
187  const irep_idt &_function_id,
189  local_may_aliast &may,
191  : _rw_set_loct(
192  _ns,
193  _value_sets,
194  _function_id,
195  _target,
196  may,
198 #else
200  const namespacet &_ns,
201  value_setst &_value_sets,
202  const irep_idt &_function_id,
205  : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler)
206 #endif
207  {
208  compute();
209  }
210 };
211 
212 // another producer, this time for entire functions
213 
215 {
216 public:
218  value_setst &_value_sets,
219  const goto_modelt &_goto_model,
220  const exprt &function,
223  ns(_goto_model.symbol_table),
224  value_sets(_value_sets),
225  goto_functions(_goto_model.goto_functions)
226  {
227  compute_rec(function);
228  }
229 
230 protected:
231  const namespacet ns;
234 
235  void compute_rec(const exprt &function);
236 };
237 
238 /* rw_set_loc keeping track of the dereference path */
239 
241 {
242 public:
243  // NOTE: combine this with entriest to avoid double copy
244  /* keeps track of who is dereferenced from who.
245  E.g., y=&z; x=*y;
246  reads(x=*y;)={y,z}
247  dereferenced_from={z|->y} */
248  std::map<const irep_idt, const irep_idt> dereferenced_from;
249 
250  /* is var a read or write */
251  std::set<irep_idt> set_reads;
252 
253 #ifdef LOCAL_MAY
255  const namespacet &_ns,
256  value_setst &_value_sets,
257  const irep_idt &_function_id,
259  local_may_aliast &may,
261  : _rw_set_loct(
262  _ns,
263  _value_sets,
264  _function_id,
265  _target,
266  may,
268  dereferencing(false)
269 #else
271  const namespacet &_ns,
272  value_setst &_value_sets,
273  const irep_idt &_function_id,
274  goto_programt::const_targett _target,
276  : _rw_set_loct(_ns, _value_sets, _function_id, _target, message_handler),
277  dereferencing(false)
278 #endif
279  {
280  compute();
281  }
282 
283 protected:
284  /* flag and variable in the expression, from which we dereference */
286  std::vector<entryt> dereferenced;
287 
288  void track_deref(const entryt &entry, bool read)
289  {
290  if(dereferencing && dereferenced.empty())
291  {
292  dereferenced.insert(dereferenced.begin(), entry);
293  if(read)
294  set_reads.insert(entry.object);
295  }
296  else if(dereferencing && !dereferenced.empty())
297  dereferenced_from.insert(
298  std::make_pair(entry.object, dereferenced.front().object));
299  }
300 
302  {
303  dereferencing=true;
304  }
305 
307  {
308  dereferencing=false;
309  dereferenced.clear();
310  }
311 };
312 
313 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:73
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition: rw_set.cpp:79
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Definition: rw_set.h:130
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
Definition: rw_set.h:158
const irep_idt function_id
Definition: rw_set.h:146
void read(const exprt &expr)
Definition: rw_set.h:153
value_setst & value_sets
Definition: rw_set.h:145
void compute()
Definition: rw_set.cpp:45
void write(const exprt &expr)
Definition: rw_set.h:163
const goto_programt::const_targett target
Definition: rw_set.h:147
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
entriest r_entries
Definition: rw_set.h:60
rw_set_baset & operator+=(const rw_set_baset &other)
Definition: rw_set.h:68
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:80
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:85
bool empty() const
Definition: rw_set.h:75
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:93
std::unordered_map< irep_idt, entryt > entriest
Definition: rw_set.h:59
virtual void reset_track_deref()
Definition: rw_set.h:98
rw_set_baset(const namespacet &_ns, message_handlert &message_handler)
Definition: rw_set.h:37
void swap(rw_set_baset &other)
Definition: rw_set.h:62
entriest w_entries
Definition: rw_set.h:60
void output(std::ostream &out) const
Definition: rw_set.cpp:22
const namespacet & ns
Definition: rw_set.h:100
virtual void set_track_deref()
Definition: rw_set.h:97
message_handlert & message_handler
Definition: rw_set.h:101
virtual ~rw_set_baset()=default
const goto_functionst & goto_functions
Definition: rw_set.h:233
void compute_rec(const exprt &function)
Definition: rw_set.cpp:193
const namespacet ns
Definition: rw_set.h:231
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function, message_handlert &message_handler)
Definition: rw_set.h:217
value_setst & value_sets
Definition: rw_set.h:232
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Definition: rw_set.h:199
void reset_track_deref()
Definition: rw_set.h:306
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:248
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Definition: rw_set.h:270
std::vector< entryt > dereferenced
Definition: rw_set.h:286
bool dereferencing
Definition: rw_set.h:285
void set_track_deref()
Definition: rw_set.h:301
void track_deref(const entryt &entry, bool read)
Definition: rw_set.h:288
std::set< irep_idt > set_reads
Definition: rw_set.h:251
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol Table + CFG.
static int8_t r
Definition: irep_hash.h:60
int __CPROVER_ID java::java io InputStream read
Definition: java.io.c:5
Field-insensitive, location-sensitive may-alias analysis.
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition: rw_set.h:104
API to expression classes.
irep_idt object
Definition: rw_set.h:47
symbol_exprt symbol_expr
Definition: rw_set.h:46
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)
Definition: rw_set.h:50