cprover
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/guard.h>
22 #include <util/std_expr.h>
23 
25 
26 #ifdef LOCAL_MAY
28 #endif
29 
30 class namespacet;
31 class value_setst;
32 
33 // a container for read/write sets
34 
36 {
37 public:
38  explicit rw_set_baset(const namespacet &_ns)
39  :ns(_ns)
40  {
41  }
42 
43  virtual ~rw_set_baset() = default;
44 
45  struct entryt
46  {
50 
52  {
53  }
54  };
55 
56  typedef std::unordered_map<irep_idt, entryt> entriest;
58 
59  void swap(rw_set_baset &other)
60  {
61  std::swap(other.r_entries, r_entries);
62  std::swap(other.w_entries, w_entries);
63  }
64 
66  {
67  r_entries.insert(other.r_entries.begin(), other.r_entries.end());
68  w_entries.insert(other.w_entries.begin(), other.w_entries.end());
69  return *this;
70  }
71 
72  bool empty() const
73  {
74  return r_entries.empty() && w_entries.empty();
75  }
76 
77  bool has_w_entry(irep_idt object) const
78  {
79  return w_entries.find(object)!=w_entries.end();
80  }
81 
82  bool has_r_entry(irep_idt object) const
83  {
84  return r_entries.find(object)!=r_entries.end();
85  }
86 
87  void output(std::ostream &out) const;
88 
89 protected:
90  virtual void track_deref(const entryt &, bool read)
91  {
92  (void)read; // unused parameter
93  }
94  virtual void set_track_deref() {}
95  virtual void reset_track_deref() {}
96 
97  const namespacet &ns;
98 };
99 
100 inline std::ostream &operator<<(
101  std::ostream &out, const rw_set_baset &rw_set)
102 {
103  rw_set.output(out);
104  return out;
105 }
106 
107 #define forall_rw_set_r_entries(it, rw_set) \
108  for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \
109  it!=(rw_set).r_entries.end(); it++)
110 
111 #define forall_rw_set_w_entries(it, rw_set) \
112  for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \
113  it!=(rw_set).w_entries.end(); it++)
114 
115 // a producer of read/write sets
116 
118 {
119 public:
120 #ifdef LOCAL_MAY
121  _rw_set_loct(
122  const namespacet &_ns,
123  value_setst &_value_sets,
125  local_may_aliast &may):
126  rw_set_baset(_ns),
127  value_sets(_value_sets),
128  target(_target),
129  local_may(may)
130 #else
132  const namespacet &_ns,
133  value_setst &_value_sets,
135  rw_set_baset(_ns),
136  value_sets(_value_sets),
137  target(_target)
138 #endif
139  {
140  }
141 
142 protected:
145 
146 #ifdef LOCAL_MAY
147  local_may_aliast &local_may;
148 #endif
149 
150  void read(const exprt &expr)
151  {
152  read_write_rec(expr, true, false, "", guardt());
153  }
154 
155  void read(const exprt &expr, const guardt &guard)
156  {
157  read_write_rec(expr, true, false, "", guard);
158  }
159 
160  void write(const exprt &expr)
161  {
162  read_write_rec(expr, false, true, "", guardt());
163  }
164 
165  void compute();
166 
167  void assign(const exprt &lhs, const exprt &rhs);
168 
169  void read_write_rec(
170  const exprt &expr,
171  bool r, bool w,
172  const std::string &suffix,
173  const guardt &guard);
174 };
175 
177 {
178 public:
179 #ifdef LOCAL_MAY
180  rw_set_loct(
181  const namespacet &_ns,
182  value_setst &_value_sets,
184  local_may_aliast &may):
185  _rw_set_loct(_ns, _value_sets, _target, may)
186 #else
188  const namespacet &_ns,
189  value_setst &_value_sets,
191  _rw_set_loct(_ns, _value_sets, _target)
192 #endif
193  {
194  compute();
195  }
196 };
197 
198 // another producer, this time for entire functions
199 
201 {
202 public:
204  value_setst &_value_sets,
205  const goto_modelt &_goto_model,
206  const exprt &function):
207  rw_set_baset(ns),
208  ns(_goto_model.symbol_table),
209  value_sets(_value_sets),
210  goto_functions(_goto_model.goto_functions)
211  {
212  compute_rec(function);
213  }
214 
215 protected:
216  const namespacet ns;
219 
220  void compute_rec(const exprt &function);
221 };
222 
223 /* rw_set_loc keeping track of the dereference path */
224 
226 {
227 public:
228  // NOTE: combine this with entriest to avoid double copy
229  /* keeps track of who is dereferenced from who.
230  E.g., y=&z; x=*y;
231  reads(x=*y;)={y,z}
232  dereferenced_from={z|->y} */
233  std::map<const irep_idt, const irep_idt> dereferenced_from;
234 
235  /* is var a read or write */
236  std::set<irep_idt> set_reads;
237 
238 #ifdef LOCAL_MAY
240  const namespacet &_ns,
241  value_setst &_value_sets,
243  local_may_aliast &may):
244  _rw_set_loct(_ns, _value_sets, _target, may),
245  dereferencing(false)
246 #else
248  const namespacet &_ns,
249  value_setst &_value_sets,
250  goto_programt::const_targett _target):
251  _rw_set_loct(_ns, _value_sets, _target),
252  dereferencing(false)
253 #endif
254  {
255  compute();
256  }
257 
258 protected:
259  /* flag and variable in the expression, from which we dereference */
261  std::vector<entryt> dereferenced;
262 
263  void track_deref(const entryt &entry, bool read)
264  {
265  if(dereferencing && dereferenced.empty())
266  {
267  dereferenced.insert(dereferenced.begin(), entry);
268  if(read)
269  set_reads.insert(entry.object);
270  }
271  else if(dereferencing && !dereferenced.empty())
272  dereferenced_from.insert(
273  std::make_pair(entry.object, dereferenced.front().object));
274  }
275 
277  {
278  dereferencing=true;
279  }
280 
282  {
283  dereferencing=false;
284  dereferenced.clear();
285  }
286 };
287 
288 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
Definition: rw_set.h:131
void compute()
Definition: rw_set.cpp:47
static int8_t r
Definition: irep_hash.h:59
void reset_track_deref()
Definition: rw_set.h:281
void swap(rw_set_baset &other)
Definition: rw_set.h:59
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
Definition: rw_set.h:247
bool empty() const
Definition: rw_set.h:72
void output(std::ostream &out) const
Definition: rw_set.cpp:24
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition: rw_set.h:100
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
Definition: rw_set.h:203
entriest r_entries
Definition: rw_set.h:57
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:233
Definition: guard.h:19
virtual ~rw_set_baset()=default
virtual void reset_track_deref()
Definition: rw_set.h:95
rw_set_baset & operator+=(const rw_set_baset &other)
Definition: rw_set.h:65
void compute_rec(const exprt &function)
Definition: rw_set.cpp:198
value_setst & value_sets
Definition: rw_set.h:143
void set_track_deref()
Definition: rw_set.h:276
Symbol Table + CFG.
The Boolean constant true.
Definition: std_expr.h:4443
const namespacet & ns
Definition: rw_set.h:97
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:82
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:77
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:90
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:415
irep_idt object
Definition: rw_set.h:48
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const goto_programt::const_targett target
Definition: rw_set.h:144
Guard Data Structure.
A collection of goto functions.
std::set< irep_idt > set_reads
Definition: rw_set.h:236
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const goto_functionst & goto_functions
Definition: rw_set.h:218
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
entriest w_entries
Definition: rw_set.h:57
std::vector< entryt > dereferenced
Definition: rw_set.h:261
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)
Definition: rw_set.cpp:85
void track_deref(const entryt &entry, bool read)
Definition: rw_set.h:263
value_setst & value_sets
Definition: rw_set.h:217
rw_set_baset(const namespacet &_ns)
Definition: rw_set.h:38
Base class for all expressions.
Definition: expr.h:54
symbol_exprt symbol_expr
Definition: rw_set.h:47
Expression to hold a symbol (variable)
Definition: std_expr.h:143
std::unordered_map< irep_idt, entryt > entriest
Definition: rw_set.h:56
bool dereferencing
Definition: rw_set.h:260
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:79
void write(const exprt &expr)
Definition: rw_set.h:160
virtual void set_track_deref()
Definition: rw_set.h:94
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
Definition: rw_set.h:187
void read(const exprt &expr, const guardt &guard)
Definition: rw_set.h:155
void read(const exprt &expr)
Definition: rw_set.h:150
const namespacet ns
Definition: rw_set.h:216
Field-insensitive, location-sensitive may-alias analysis.