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/std_expr.h>
22 
24 
25 #ifdef LOCAL_MAY
27 #endif
28 
29 class namespacet;
30 class value_setst;
31 
32 // a container for read/write sets
33 
35 {
36 public:
37  explicit rw_set_baset(const namespacet &_ns)
38  :ns(_ns)
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;
101 };
102 
103 inline std::ostream &operator<<(
104  std::ostream &out, const rw_set_baset &rw_set)
105 {
106  rw_set.output(out);
107  return out;
108 }
109 
110 // a producer of read/write sets
111 
113 {
114 public:
115 #ifdef LOCAL_MAY
116  _rw_set_loct(
117  const namespacet &_ns,
118  value_setst &_value_sets,
119  const irep_idt &_function_id,
121  local_may_aliast &may)
122  : rw_set_baset(_ns),
123  value_sets(_value_sets),
124  function_id(_function_id),
125  target(_target),
126  local_may(may)
127 #else
129  const namespacet &_ns,
130  value_setst &_value_sets,
131  const irep_idt &_function_id,
133  : rw_set_baset(_ns),
134  value_sets(_value_sets),
135  function_id(_function_id),
136  target(_target)
137 #endif
138  {
139  }
140 
141 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, "", exprt::operandst());
153  }
154 
155  void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
156  {
157  read_write_rec(expr, true, false, "", guard_conjuncts);
158  }
159 
160  void write(const exprt &expr)
161  {
162  read_write_rec(expr, false, true, "", exprt::operandst());
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,
172  bool w,
173  const std::string &suffix,
174  const exprt::operandst &guard_conjuncts);
175 };
176 
178 {
179 public:
180 #ifdef LOCAL_MAY
181  rw_set_loct(
182  const namespacet &_ns,
183  value_setst &_value_sets,
184  const irep_idt &_function_id,
186  local_may_aliast &may)
187  : _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
188 #else
190  const namespacet &_ns,
191  value_setst &_value_sets,
192  const irep_idt &_function_id,
194  : _rw_set_loct(_ns, _value_sets, _function_id, _target)
195 #endif
196  {
197  compute();
198  }
199 };
200 
201 // another producer, this time for entire functions
202 
204 {
205 public:
207  value_setst &_value_sets,
208  const goto_modelt &_goto_model,
209  const exprt &function):
210  rw_set_baset(ns),
211  ns(_goto_model.symbol_table),
212  value_sets(_value_sets),
213  goto_functions(_goto_model.goto_functions)
214  {
215  compute_rec(function);
216  }
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,
245  const irep_idt &_function_id,
247  local_may_aliast &may)
248  : _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
249  dereferencing(false)
250 #else
252  const namespacet &_ns,
253  value_setst &_value_sets,
254  const irep_idt &_function_id,
255  goto_programt::const_targett _target)
256  : _rw_set_loct(_ns, _value_sets, _function_id, _target),
257  dereferencing(false)
258 #endif
259  {
260  compute();
261  }
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_with_trackt::set_track_deref
void set_track_deref()
Definition: rw_set.h:281
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
rw_set_functiont::rw_set_functiont
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
Definition: rw_set.h:206
rw_set_with_trackt::dereferenced
std::vector< entryt > dereferenced
Definition: rw_set.h:266
rw_set_functiont::goto_functions
const goto_functionst & goto_functions
Definition: rw_set.h:221
rw_set_baset::entryt
Definition: rw_set.h:45
rw_set_baset::rw_set_baset
rw_set_baset(const namespacet &_ns)
Definition: rw_set.h:37
rw_set_loct::rw_set_loct
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
Definition: rw_set.h:189
rw_set_baset::entryt::guard
exprt guard
Definition: rw_set.h:48
_rw_set_loct::assign
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:80
_rw_set_loct::target
const goto_programt::const_targett target
Definition: rw_set.h:144
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
rw_set_functiont::compute_rec
void compute_rec(const exprt &function)
Definition: rw_set.cpp:200
rw_set_baset::ns
const namespacet & ns
Definition: rw_set.h:100
_rw_set_loct::read
void read(const exprt &expr)
Definition: rw_set.h:150
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
rw_set_baset::~rw_set_baset
virtual ~rw_set_baset()=default
operator<<
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition: rw_set.h:103
rw_set_baset::reset_track_deref
virtual void reset_track_deref()
Definition: rw_set.h:98
rw_set_baset::r_entries
entriest r_entries
Definition: rw_set.h:60
local_may_aliast
Definition: local_may_alias.h:26
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
rw_set_with_trackt::track_deref
void track_deref(const entryt &entry, bool read)
Definition: rw_set.h:268
rw_set_with_trackt::dereferencing
bool dereferencing
Definition: rw_set.h:265
rw_set_with_trackt::rw_set_with_trackt
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
Definition: rw_set.h:251
_rw_set_loct::function_id
const irep_idt function_id
Definition: rw_set.h:143
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
rw_set_baset::empty
bool empty() const
Definition: rw_set.h:75
_rw_set_loct::_rw_set_loct
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
Definition: rw_set.h:128
rw_set_baset::swap
void swap(rw_set_baset &other)
Definition: rw_set.h:62
rw_set_with_trackt::reset_track_deref
void reset_track_deref()
Definition: rw_set.h:286
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
rw_set_baset::w_entries
entriest w_entries
Definition: rw_set.h:60
_rw_set_loct::value_sets
value_setst & value_sets
Definition: rw_set.h:142
rw_set_baset::track_deref
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:93
rw_set_with_trackt
Definition: rw_set.h:229
rw_set_baset::entryt::entryt
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)
Definition: rw_set.h:50
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
rw_set_baset::has_w_entry
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:80
value_setst
Definition: value_sets.h:22
rw_set_loct
Definition: rw_set.h:178
rw_set_functiont::value_sets
value_setst & value_sets
Definition: rw_set.h:220
_rw_set_loct::read_write_rec
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition: rw_set.cpp:86
rw_set_with_trackt::dereferenced_from
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:236
rw_set_baset
Definition: rw_set.h:35
_rw_set_loct::write
void write(const exprt &expr)
Definition: rw_set.h:160
_rw_set_loct
Definition: rw_set.h:113
rw_set_baset::entryt::object
irep_idt object
Definition: rw_set.h:47
rw_set_baset::entriest
std::unordered_map< irep_idt, entryt > entriest
Definition: rw_set.h:59
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
rw_set_functiont::ns
const namespacet ns
Definition: rw_set.h:219
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
rw_set_baset::operator+=
rw_set_baset & operator+=(const rw_set_baset &other)
Definition: rw_set.h:68
rw_set_baset::has_r_entry
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:85
r
static int8_t r
Definition: irep_hash.h:59
rw_set_baset::entryt::symbol_expr
symbol_exprt symbol_expr
Definition: rw_set.h:46
_rw_set_loct::compute
void compute()
Definition: rw_set.cpp:48
_rw_set_loct::read
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
Definition: rw_set.h:155
std_expr.h
API to expression classes.
rw_set_with_trackt::set_reads
std::set< irep_idt > set_reads
Definition: rw_set.h:239
rw_set_functiont
Definition: rw_set.h:204
rw_set_baset::output
void output(std::ostream &out) const
Definition: rw_set.cpp:25
rw_set_baset::set_track_deref
virtual void set_track_deref()
Definition: rw_set.h:97