cprover
Loading...
Searching...
No Matches
rw_set.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Race Detection for Threaded Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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
29class value_setst;
30
31// a container for read/write sets
32
34{
35public:
36 explicit rw_set_baset(const namespacet &_ns)
37 :ns(_ns)
38 {
39 }
40
41 virtual ~rw_set_baset() = default;
42
43 struct entryt
44 {
48
50 const symbol_exprt &_symbol_expr,
51 const irep_idt &_object,
52 const exprt &_guard)
53 : symbol_expr(_symbol_expr), object(_object), guard(_guard)
54 {
55 }
56 };
57
58 typedef std::unordered_map<irep_idt, entryt> entriest;
60
61 void swap(rw_set_baset &other)
62 {
63 std::swap(other.r_entries, r_entries);
64 std::swap(other.w_entries, w_entries);
65 }
66
68 {
69 r_entries.insert(other.r_entries.begin(), other.r_entries.end());
70 w_entries.insert(other.w_entries.begin(), other.w_entries.end());
71 return *this;
72 }
73
74 bool empty() const
75 {
76 return r_entries.empty() && w_entries.empty();
77 }
78
79 bool has_w_entry(irep_idt object) const
80 {
81 return w_entries.find(object)!=w_entries.end();
82 }
83
84 bool has_r_entry(irep_idt object) const
85 {
86 return r_entries.find(object)!=r_entries.end();
87 }
88
89 void output(std::ostream &out) const;
90
91protected:
92 virtual void track_deref(const entryt &, bool read)
93 {
94 (void)read; // unused parameter
95 }
96 virtual void set_track_deref() {}
97 virtual void reset_track_deref() {}
98
99 const namespacet &ns;
100};
101
102inline std::ostream &operator<<(
103 std::ostream &out, const rw_set_baset &rw_set)
104{
105 rw_set.output(out);
106 return out;
107}
108
109// a producer of read/write sets
110
112{
113public:
114#ifdef LOCAL_MAY
116 const namespacet &_ns,
117 value_setst &_value_sets,
118 const irep_idt &_function_id,
120 local_may_aliast &may)
121 : rw_set_baset(_ns),
122 value_sets(_value_sets),
123 function_id(_function_id),
124 target(_target),
125 local_may(may)
126#else
128 const namespacet &_ns,
129 value_setst &_value_sets,
130 const irep_idt &_function_id,
132 : rw_set_baset(_ns),
133 value_sets(_value_sets),
134 function_id(_function_id),
135 target(_target)
136#endif
137 {
138 }
139
140protected:
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, "", exprt::operandst());
152 }
153
154 void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
155 {
156 read_write_rec(expr, true, false, "", guard_conjuncts);
157 }
158
159 void write(const exprt &expr)
160 {
161 read_write_rec(expr, false, true, "", exprt::operandst());
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,
171 bool w,
172 const std::string &suffix,
173 const exprt::operandst &guard_conjuncts);
174};
175
177{
178public:
179#ifdef LOCAL_MAY
181 const namespacet &_ns,
182 value_setst &_value_sets,
183 const irep_idt &_function_id,
185 local_may_aliast &may)
186 : _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
187#else
189 const namespacet &_ns,
190 value_setst &_value_sets,
191 const irep_idt &_function_id,
193 : _rw_set_loct(_ns, _value_sets, _function_id, _target)
194#endif
195 {
196 compute();
197 }
198};
199
200// another producer, this time for entire functions
201
203{
204public:
206 value_setst &_value_sets,
207 const goto_modelt &_goto_model,
208 const exprt &function):
210 ns(_goto_model.symbol_table),
211 value_sets(_value_sets),
212 goto_functions(_goto_model.goto_functions)
213 {
214 compute_rec(function);
215 }
216
217protected:
221
222 void compute_rec(const exprt &function);
223};
224
225/* rw_set_loc keeping track of the dereference path */
226
228{
229public:
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,
244 const irep_idt &_function_id,
246 local_may_aliast &may)
247 : _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
248 dereferencing(false)
249#else
251 const namespacet &_ns,
252 value_setst &_value_sets,
253 const irep_idt &_function_id,
254 goto_programt::const_targett _target)
255 : _rw_set_loct(_ns, _value_sets, _function_id, _target),
256 dereferencing(false)
257#endif
258 {
259 compute();
260 }
261
262protected:
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
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:74
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition: rw_set.cpp:80
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
Definition: rw_set.h:154
const irep_idt function_id
Definition: rw_set.h:142
void read(const exprt &expr)
Definition: rw_set.h:149
value_setst & value_sets
Definition: rw_set.h:141
void compute()
Definition: rw_set.cpp:46
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
Definition: rw_set.h:127
void write(const exprt &expr)
Definition: rw_set.h:159
const goto_programt::const_targett target
Definition: rw_set.h:143
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
entriest r_entries
Definition: rw_set.h:59
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:79
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:84
bool empty() const
Definition: rw_set.h:74
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:92
rw_set_baset(const namespacet &_ns)
Definition: rw_set.h:36
std::unordered_map< irep_idt, entryt > entriest
Definition: rw_set.h:58
virtual void reset_track_deref()
Definition: rw_set.h:97
void swap(rw_set_baset &other)
Definition: rw_set.h:61
entriest w_entries
Definition: rw_set.h:59
void output(std::ostream &out) const
Definition: rw_set.cpp:23
rw_set_baset & operator+=(const rw_set_baset &other)
Definition: rw_set.h:67
const namespacet & ns
Definition: rw_set.h:99
virtual void set_track_deref()
Definition: rw_set.h:96
virtual ~rw_set_baset()=default
const goto_functionst & goto_functions
Definition: rw_set.h:220
void compute_rec(const exprt &function)
Definition: rw_set.cpp:194
const namespacet ns
Definition: rw_set.h:218
value_setst & value_sets
Definition: rw_set.h:219
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
Definition: rw_set.h:205
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
Definition: rw_set.h:188
void reset_track_deref()
Definition: rw_set.h:285
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:235
std::vector< entryt > dereferenced
Definition: rw_set.h:265
bool dereferencing
Definition: rw_set.h:264
void set_track_deref()
Definition: rw_set.h:280
void track_deref(const entryt &entry, bool read)
Definition: rw_set.h:267
std::set< irep_idt > set_reads
Definition: rw_set.h:238
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol Table + CFG.
static int8_t r
Definition: irep_hash.h:60
Field-insensitive, location-sensitive may-alias analysis.
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition: rw_set.h:102
API to expression classes.
irep_idt object
Definition: rw_set.h:46
symbol_exprt symbol_expr
Definition: rw_set.h:45
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)
Definition: rw_set.h:49