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_code.h>
23 #include <util/namespace.h>
24 #include <util/std_expr.h>
25 
28 
29 #ifdef LOCAL_MAY
31 #endif
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, irep_id_hash> 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 namespacet &_ns,
207  const goto_functionst &_goto_functions,
208  const exprt &function):
209  rw_set_baset(_ns),
210  value_sets(_value_sets),
211  goto_functions(_goto_functions)
212  {
213  compute_rec(function);
214  }
215 
217 
218 protected:
221 
222  void compute_rec(const exprt &function);
223 };
224 
225 /* rw_set_loc keeping track of the dereference path */
226 
228 {
229 public:
230  // NOTE: combine this with entriest to avoid double copy
231  /* keeps track of who is dereferenced from who.
232  E.g., y=&z; x=*y;
233  reads(x=*y;)={y,z}
234  dereferenced_from={z|->y} */
235  std::map<const irep_idt, const irep_idt> dereferenced_from;
236 
237  /* is var a read or write */
238  std::set<irep_idt> set_reads;
239 
240 #ifdef LOCAL_MAY
242  const namespacet &_ns,
243  value_setst &_value_sets,
245  local_may_aliast &may):
246  _rw_set_loct(_ns, _value_sets, _target, may),
247  dereferencing(false)
248 #else
250  const namespacet &_ns,
251  value_setst &_value_sets,
252  goto_programt::const_targett _target):
253  _rw_set_loct(_ns, _value_sets, _target),
254  dereferencing(false)
255 #endif
256  {
257  compute();
258  }
259 
261 
262 protected:
263  /* flag and variable in the expression, from which we dereference */
265  std::vector<entryt> dereferenced;
266 
267  void track_deref(const entryt &entry, bool read)
268  {
269  if(dereferencing && dereferenced.empty())
270  {
271  dereferenced.insert(dereferenced.begin(), entry);
272  if(read)
273  set_reads.insert(entry.object);
274  }
275  else if(dereferencing && !dereferenced.empty())
276  dereferenced_from.insert(
277  std::make_pair(entry.object, dereferenced.front().object));
278  }
279 
281  {
282  dereferencing=true;
283  }
284 
286  {
287  dereferencing=false;
288  dereferenced.clear();
289  }
290 };
291 
292 #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:285
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:249
bool empty() const
Definition: rw_set.h:72
void output(std::ostream &out) const
Definition: rw_set.cpp:24
rw_set_functiont(value_setst &_value_sets, const namespacet &_ns, const goto_functionst &_goto_functions, const exprt &function)
Definition: rw_set.h:204
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition: rw_set.h:97
entriest r_entries
Definition: rw_set.h:57
Goto Programs with Functions.
~rw_set_loct()
Definition: rw_set.h:196
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:235
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:280
instructionst::const_iterator const_targett
The boolean constant true.
Definition: std_expr.h:3742
const namespacet & ns
Definition: rw_set.h:94
Value Set Propagation.
~_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
std::unordered_map< irep_idt, entryt, irep_id_hash > entriest
Definition: rw_set.h:56
API to expression classes.
irep_idt object
Definition: rw_set.h:48
TO_BE_DOCUMENTED.
Definition: namespace.h:62
~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:238
const goto_functionst & goto_functions
Definition: rw_set.h:220
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
entriest w_entries
Definition: rw_set.h:57
std::vector< entryt > dereferenced
Definition: rw_set.h:265
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:267
value_setst & value_sets
Definition: rw_set.h:219
rw_set_baset(const namespacet &_ns)
Definition: rw_set.h:38
Base class for all expressions.
Definition: expr.h:46
symbol_exprt symbol_expr
Definition: rw_set.h:47
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool dereferencing
Definition: rw_set.h:264
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
Field-insensitive, location-sensitive may-alias analysis.