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 
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 &entry, bool read) {}
91  virtual void set_track_deref() {}
92  virtual void reset_track_deref() {}
93 
94  const namespacet &ns;
95 };
96 
97 inline std::ostream &operator<<(
98  std::ostream &out, const rw_set_baset &rw_set)
99 {
100  rw_set.output(out);
101  return out;
102 }
103 
104 #define forall_rw_set_r_entries(it, rw_set) \
105  for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \
106  it!=(rw_set).r_entries.end(); it++)
107 
108 #define forall_rw_set_w_entries(it, rw_set) \
109  for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \
110  it!=(rw_set).w_entries.end(); it++)
111 
112 // a producer of read/write sets
113 
115 {
116 public:
117 #ifdef LOCAL_MAY
118  _rw_set_loct(
119  const namespacet &_ns,
120  value_setst &_value_sets,
122  local_may_aliast &may):
123  rw_set_baset(_ns),
124  value_sets(_value_sets),
125  target(_target),
126  local_may(may)
127 #else
129  const namespacet &_ns,
130  value_setst &_value_sets,
132  rw_set_baset(_ns),
133  value_sets(_value_sets),
134  target(_target)
135 #endif
136  {
137  }
138 
140 
141 protected:
144 
145 #ifdef LOCAL_MAY
146  local_may_aliast &local_may;
147 #endif
148 
149  void read(const exprt &expr)
150  {
151  read_write_rec(expr, true, false, "", guardt());
152  }
153 
154  void read(const exprt &expr, const guardt &guard)
155  {
156  read_write_rec(expr, true, false, "", guard);
157  }
158 
159  void write(const exprt &expr)
160  {
161  read_write_rec(expr, false, true, "", guardt());
162  }
163 
164  void compute();
165 
166  void assign(const exprt &lhs, const exprt &rhs);
167 
168  void read_write_rec(
169  const exprt &expr,
170  bool r, bool w,
171  const std::string &suffix,
172  const guardt &guard);
173 };
174 
176 {
177 public:
178 #ifdef LOCAL_MAY
179  rw_set_loct(
180  const namespacet &_ns,
181  value_setst &_value_sets,
183  local_may_aliast &may):
184  _rw_set_loct(_ns, _value_sets, _target, may)
185 #else
187  const namespacet &_ns,
188  value_setst &_value_sets,
190  _rw_set_loct(_ns, _value_sets, _target)
191 #endif
192  {
193  compute();
194  }
195 
197 };
198 
199 // another producer, this time for entire functions
200 
202 {
203 public:
205  value_setst &_value_sets,
206  const goto_modelt &_goto_model,
207  const exprt &function):
208  rw_set_baset(ns),
209  ns(_goto_model.symbol_table),
210  value_sets(_value_sets),
211  goto_functions(_goto_model.goto_functions)
212  {
213  compute_rec(function);
214  }
215 
217 
218 protected:
219  const namespacet ns;
222 
223  void compute_rec(const exprt &function);
224 };
225 
226 /* rw_set_loc keeping track of the dereference path */
227 
229 {
230 public:
231  // NOTE: combine this with entriest to avoid double copy
232  /* keeps track of who is dereferenced from who.
233  E.g., y=&z; x=*y;
234  reads(x=*y;)={y,z}
235  dereferenced_from={z|->y} */
236  std::map<const irep_idt, const irep_idt> dereferenced_from;
237 
238  /* is var a read or write */
239  std::set<irep_idt> set_reads;
240 
241 #ifdef LOCAL_MAY
243  const namespacet &_ns,
244  value_setst &_value_sets,
246  local_may_aliast &may):
247  _rw_set_loct(_ns, _value_sets, _target, may),
248  dereferencing(false)
249 #else
251  const namespacet &_ns,
252  value_setst &_value_sets,
253  goto_programt::const_targett _target):
254  _rw_set_loct(_ns, _value_sets, _target),
255  dereferencing(false)
256 #endif
257  {
258  compute();
259  }
260 
262 
263 protected:
264  /* flag and variable in the expression, from which we dereference */
266  std::vector<entryt> dereferenced;
267 
268  void track_deref(const entryt &entry, bool read)
269  {
270  if(dereferencing && dereferenced.empty())
271  {
272  dereferenced.insert(dereferenced.begin(), entry);
273  if(read)
274  set_reads.insert(entry.object);
275  }
276  else if(dereferencing && !dereferenced.empty())
277  dereferenced_from.insert(
278  std::make_pair(entry.object, dereferenced.front().object));
279  }
280 
282  {
283  dereferencing=true;
284  }
285 
287  {
288  dereferencing=false;
289  dereferenced.clear();
290  }
291 };
292 
293 #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:128
virtual void track_deref(const entryt &entry, bool read)
Definition: rw_set.h:90
void compute()
Definition: rw_set.cpp:47
static int8_t r
Definition: irep_hash.h:59
void reset_track_deref()
Definition: rw_set.h:286
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:250
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:97
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
Definition: rw_set.h:204
entriest r_entries
Definition: rw_set.h:57
~rw_set_loct()
Definition: rw_set.h:196
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:236
Definition: guard.h:19
virtual void reset_track_deref()
Definition: rw_set.h:92
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:142
void set_track_deref()
Definition: rw_set.h:281
Symbol Table + CFG.
The boolean constant true.
Definition: std_expr.h:4488
const namespacet & ns
Definition: rw_set.h:94
~_rw_set_loct()
Definition: rw_set.h:139
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
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
irep_idt object
Definition: rw_set.h:48
TO_BE_DOCUMENTED.
Definition: namespace.h:74
~rw_set_baset()
Definition: rw_set.h:43
const goto_programt::const_targett target
Definition: rw_set.h:143
Guard Data Structure.
std::set< irep_idt > set_reads
Definition: rw_set.h:239
const goto_functionst & goto_functions
Definition: rw_set.h:221
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
entriest w_entries
Definition: rw_set.h:57
std::vector< entryt > dereferenced
Definition: rw_set.h:266
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:268
value_setst & value_sets
Definition: rw_set.h:220
rw_set_baset(const namespacet &_ns)
Definition: rw_set.h:38
Base class for all expressions.
Definition: expr.h:42
symbol_exprt symbol_expr
Definition: rw_set.h:47
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::unordered_map< irep_idt, entryt > entriest
Definition: rw_set.h:56
bool dereferencing
Definition: rw_set.h:265
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:79
void write(const exprt &expr)
Definition: rw_set.h:159
virtual void set_track_deref()
Definition: rw_set.h:91
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
Definition: rw_set.h:186
void read(const exprt &expr, const guardt &guard)
Definition: rw_set.h:154
void read(const exprt &expr)
Definition: rw_set.h:149
const namespacet ns
Definition: rw_set.h:219
Field-insensitive, location-sensitive may-alias analysis.