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 #define forall_rw_set_r_entries(it, rw_set) \
111  for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \
112  it!=(rw_set).r_entries.end(); it++)
113 
114 #define forall_rw_set_w_entries(it, rw_set) \
115  for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \
116  it!=(rw_set).w_entries.end(); it++)
117 
118 // a producer of read/write sets
119 
121 {
122 public:
123 #ifdef LOCAL_MAY
124  _rw_set_loct(
125  const namespacet &_ns,
126  value_setst &_value_sets,
127  const irep_idt &_function_id,
129  local_may_aliast &may)
130  : rw_set_baset(_ns),
131  value_sets(_value_sets),
132  function_id(_function_id),
133  target(_target),
134  local_may(may)
135 #else
137  const namespacet &_ns,
138  value_setst &_value_sets,
139  const irep_idt &_function_id,
141  : rw_set_baset(_ns),
142  value_sets(_value_sets),
143  function_id(_function_id),
144  target(_target)
145 #endif
146  {
147  }
148 
149 protected:
153 
154 #ifdef LOCAL_MAY
155  local_may_aliast &local_may;
156 #endif
157 
158  void read(const exprt &expr)
159  {
160  read_write_rec(expr, true, false, "", exprt::operandst());
161  }
162 
163  void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
164  {
165  read_write_rec(expr, true, false, "", guard_conjuncts);
166  }
167 
168  void write(const exprt &expr)
169  {
170  read_write_rec(expr, false, true, "", exprt::operandst());
171  }
172 
173  void compute();
174 
175  void assign(const exprt &lhs, const exprt &rhs);
176 
177  void read_write_rec(
178  const exprt &expr,
179  bool r,
180  bool w,
181  const std::string &suffix,
182  const exprt::operandst &guard_conjuncts);
183 };
184 
186 {
187 public:
188 #ifdef LOCAL_MAY
189  rw_set_loct(
190  const namespacet &_ns,
191  value_setst &_value_sets,
192  const irep_idt &_function_id,
194  local_may_aliast &may)
195  : _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
196 #else
198  const namespacet &_ns,
199  value_setst &_value_sets,
200  const irep_idt &_function_id,
202  : _rw_set_loct(_ns, _value_sets, _function_id, _target)
203 #endif
204  {
205  compute();
206  }
207 };
208 
209 // another producer, this time for entire functions
210 
212 {
213 public:
215  value_setst &_value_sets,
216  const goto_modelt &_goto_model,
217  const exprt &function):
218  rw_set_baset(ns),
219  ns(_goto_model.symbol_table),
220  value_sets(_value_sets),
221  goto_functions(_goto_model.goto_functions)
222  {
223  compute_rec(function);
224  }
225 
226 protected:
227  const namespacet ns;
230 
231  void compute_rec(const exprt &function);
232 };
233 
234 /* rw_set_loc keeping track of the dereference path */
235 
237 {
238 public:
239  // NOTE: combine this with entriest to avoid double copy
240  /* keeps track of who is dereferenced from who.
241  E.g., y=&z; x=*y;
242  reads(x=*y;)={y,z}
243  dereferenced_from={z|->y} */
244  std::map<const irep_idt, const irep_idt> dereferenced_from;
245 
246  /* is var a read or write */
247  std::set<irep_idt> set_reads;
248 
249 #ifdef LOCAL_MAY
251  const namespacet &_ns,
252  value_setst &_value_sets,
253  const irep_idt &_function_id,
255  local_may_aliast &may)
256  : _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
257  dereferencing(false)
258 #else
260  const namespacet &_ns,
261  value_setst &_value_sets,
262  const irep_idt &_function_id,
263  goto_programt::const_targett _target)
264  : _rw_set_loct(_ns, _value_sets, _function_id, _target),
265  dereferencing(false)
266 #endif
267  {
268  compute();
269  }
270 
271 protected:
272  /* flag and variable in the expression, from which we dereference */
274  std::vector<entryt> dereferenced;
275 
276  void track_deref(const entryt &entry, bool read)
277  {
278  if(dereferencing && dereferenced.empty())
279  {
280  dereferenced.insert(dereferenced.begin(), entry);
281  if(read)
282  set_reads.insert(entry.object);
283  }
284  else if(dereferencing && !dereferenced.empty())
285  dereferenced_from.insert(
286  std::make_pair(entry.object, dereferenced.front().object));
287  }
288 
290  {
291  dereferencing=true;
292  }
293 
295  {
296  dereferencing=false;
297  dereferenced.clear();
298  }
299 };
300 
301 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H
rw_set_with_trackt::set_track_deref
void set_track_deref()
Definition: rw_set.h:289
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:214
rw_set_with_trackt::dereferenced
std::vector< entryt > dereferenced
Definition: rw_set.h:274
rw_set_functiont::goto_functions
const goto_functionst & goto_functions
Definition: rw_set.h:229
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:197
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:79
_rw_set_loct::target
const goto_programt::const_targett target
Definition: rw_set.h:152
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
rw_set_functiont::compute_rec
void compute_rec(const exprt &function)
Definition: rw_set.cpp:199
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:158
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:276
rw_set_with_trackt::dereferencing
bool dereferencing
Definition: rw_set.h:273
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:259
_rw_set_loct::function_id
const irep_idt function_id
Definition: rw_set.h:151
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:136
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:294
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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:150
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:237
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:186
rw_set_functiont::value_sets
value_setst & value_sets
Definition: rw_set.h:228
_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:85
rw_set_with_trackt::dereferenced_from
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:244
rw_set_baset
Definition: rw_set.h:35
_rw_set_loct::write
void write(const exprt &expr)
Definition: rw_set.h:168
_rw_set_loct
Definition: rw_set.h:121
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:73
rw_set_functiont::ns
const namespacet ns
Definition: rw_set.h:227
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:47
_rw_set_loct::read
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
Definition: rw_set.h:163
std_expr.h
API to expression classes.
rw_set_with_trackt::set_reads
std::set< irep_idt > set_reads
Definition: rw_set.h:247
rw_set_functiont
Definition: rw_set.h:212
rw_set_baset::output
void output(std::ostream &out) const
Definition: rw_set.cpp:24
rw_set_baset::set_track_deref
virtual void set_track_deref()
Definition: rw_set.h:97