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
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,
118 const irep_idt &_function_id,
121 : rw_set_baset(_ns),
126#else
139
140protected:
144
145#ifdef 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,
174};
175
199
200// another producer, this time for entire functions
201
203{
204public:
208 const exprt &function):
210 ns(_goto_model.symbol_table),
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,
244 const irep_idt &_function_id,
249#else
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;
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
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:40
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
instructionst::const_iterator const_targett
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
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