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  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 
139 protected:
142 
143 #ifdef LOCAL_MAY
144  local_may_aliast &local_may;
145 #endif
146 
147  void read(const exprt &expr)
148  {
149  read_write_rec(expr, true, false, "", guardt());
150  }
151 
152  void read(const exprt &expr, const guardt &guard)
153  {
154  read_write_rec(expr, true, false, "", guard);
155  }
156 
157  void write(const exprt &expr)
158  {
159  read_write_rec(expr, false, true, "", guardt());
160  }
161 
162  void compute();
163 
164  void assign(const exprt &lhs, const exprt &rhs);
165 
166  void read_write_rec(
167  const exprt &expr,
168  bool r, bool w,
169  const std::string &suffix,
170  const guardt &guard);
171 };
172 
174 {
175 public:
176 #ifdef LOCAL_MAY
177  rw_set_loct(
178  const namespacet &_ns,
179  value_setst &_value_sets,
181  local_may_aliast &may):
182  _rw_set_loct(_ns, _value_sets, _target, may)
183 #else
185  const namespacet &_ns,
186  value_setst &_value_sets,
188  _rw_set_loct(_ns, _value_sets, _target)
189 #endif
190  {
191  compute();
192  }
193 };
194 
195 // another producer, this time for entire functions
196 
198 {
199 public:
201  value_setst &_value_sets,
202  const goto_modelt &_goto_model,
203  const exprt &function):
204  rw_set_baset(ns),
205  ns(_goto_model.symbol_table),
206  value_sets(_value_sets),
207  goto_functions(_goto_model.goto_functions)
208  {
209  compute_rec(function);
210  }
211 
212 protected:
213  const namespacet ns;
216 
217  void compute_rec(const exprt &function);
218 };
219 
220 /* rw_set_loc keeping track of the dereference path */
221 
223 {
224 public:
225  // NOTE: combine this with entriest to avoid double copy
226  /* keeps track of who is dereferenced from who.
227  E.g., y=&z; x=*y;
228  reads(x=*y;)={y,z}
229  dereferenced_from={z|->y} */
230  std::map<const irep_idt, const irep_idt> dereferenced_from;
231 
232  /* is var a read or write */
233  std::set<irep_idt> set_reads;
234 
235 #ifdef LOCAL_MAY
237  const namespacet &_ns,
238  value_setst &_value_sets,
240  local_may_aliast &may):
241  _rw_set_loct(_ns, _value_sets, _target, may),
242  dereferencing(false)
243 #else
245  const namespacet &_ns,
246  value_setst &_value_sets,
247  goto_programt::const_targett _target):
248  _rw_set_loct(_ns, _value_sets, _target),
249  dereferencing(false)
250 #endif
251  {
252  compute();
253  }
254 
255 protected:
256  /* flag and variable in the expression, from which we dereference */
258  std::vector<entryt> dereferenced;
259 
260  void track_deref(const entryt &entry, bool read)
261  {
262  if(dereferencing && dereferenced.empty())
263  {
264  dereferenced.insert(dereferenced.begin(), entry);
265  if(read)
266  set_reads.insert(entry.object);
267  }
268  else if(dereferencing && !dereferenced.empty())
269  dereferenced_from.insert(
270  std::make_pair(entry.object, dereferenced.front().object));
271  }
272 
274  {
275  dereferencing=true;
276  }
277 
279  {
280  dereferencing=false;
281  dereferenced.clear();
282  }
283 };
284 
285 #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
void compute()
Definition: rw_set.cpp:47
static int8_t r
Definition: irep_hash.h:59
void reset_track_deref()
Definition: rw_set.h:278
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:244
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:200
entriest r_entries
Definition: rw_set.h:57
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:230
Definition: guard.h:19
virtual ~rw_set_baset()=default
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:140
void set_track_deref()
Definition: rw_set.h:273
Symbol Table + CFG.
The boolean constant true.
Definition: std_expr.h:4486
const namespacet & ns
Definition: rw_set.h:94
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:398
irep_idt object
Definition: rw_set.h:48
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const goto_programt::const_targett target
Definition: rw_set.h:141
Guard Data Structure.
std::set< irep_idt > set_reads
Definition: rw_set.h:233
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const goto_functionst & goto_functions
Definition: rw_set.h:215
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:258
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:260
value_setst & value_sets
Definition: rw_set.h:214
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:257
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:79
void write(const exprt &expr)
Definition: rw_set.h:157
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:184
void read(const exprt &expr, const guardt &guard)
Definition: rw_set.h:152
void read(const exprt &expr)
Definition: rw_set.h:147
const namespacet ns
Definition: rw_set.h:213
Field-insensitive, location-sensitive may-alias analysis.