CBMC
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
30class value_setst;
31
32// a container for read/write sets
33
35{
36public:
41
42 virtual ~rw_set_baset() = default;
43
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
92protected:
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
102};
103
104inline std::ostream &operator<<(
105 std::ostream &out, const rw_set_baset &rw_set)
106{
107 rw_set.output(out);
108 return out;
109}
110
111// a producer of read/write sets
112
114{
115public:
116#ifdef LOCAL_MAY
118 const namespacet &_ns,
120 const irep_idt &_function_id,
129#else
143
144protected:
148
149#ifdef LOCAL_MAY
151#endif
152
153 void read(const exprt &expr)
154 {
155 read_write_rec(expr, true, false, "", exprt::operandst());
156 }
157
158 void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
159 {
160 read_write_rec(expr, true, false, "", guard_conjuncts);
161 }
162
163 void write(const exprt &expr)
164 {
165 read_write_rec(expr, false, true, "", exprt::operandst());
166 }
167
168 void compute();
169
170 void assign(const exprt &lhs, const exprt &rhs);
171
172 void read_write_rec(
173 const exprt &expr,
174 bool r,
175 bool w,
176 const std::string &suffix,
178};
179
211
212// another producer, this time for entire functions
213
215{
216public:
229
230protected:
234
235 void compute_rec(const exprt &function);
236};
237
238/* rw_set_loc keeping track of the dereference path */
239
241{
242public:
243 // NOTE: combine this with entriest to avoid double copy
244 /* keeps track of who is dereferenced from who.
245 E.g., y=&z; x=*y;
246 reads(x=*y;)={y,z}
247 dereferenced_from={z|->y} */
248 std::map<const irep_idt, const irep_idt> dereferenced_from;
249
250 /* is var a read or write */
251 std::set<irep_idt> set_reads;
252
253#ifdef LOCAL_MAY
255 const namespacet &_ns,
257 const irep_idt &_function_id,
261 : _rw_set_loct(
262 _ns,
265 _target,
266 may,
269#else
282
283protected:
284 /* flag and variable in the expression, from which we dereference */
286 std::vector<entryt> dereferenced;
287
288 void track_deref(const entryt &entry, bool read)
289 {
290 if(dereferencing && dereferenced.empty())
291 {
292 dereferenced.insert(dereferenced.begin(), entry);
293 if(read)
294 set_reads.insert(entry.object);
295 }
296 else if(dereferencing && !dereferenced.empty())
297 dereferenced_from.insert(
298 std::make_pair(entry.object, dereferenced.front().object));
299 }
300
302 {
303 dereferencing=true;
304 }
305
307 {
308 dereferencing=false;
310 }
311};
312
313#endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H
void assign(const exprt &lhs, const exprt &rhs)
Definition rw_set.cpp:73
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition rw_set.cpp:79
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Definition rw_set.h:130
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
Definition rw_set.h:158
const irep_idt function_id
Definition rw_set.h:146
void read(const exprt &expr)
Definition rw_set.h:153
value_setst & value_sets
Definition rw_set.h:145
void compute()
Definition rw_set.cpp:45
void write(const exprt &expr)
Definition rw_set.h:163
const goto_programt::const_targett target
Definition rw_set.h:147
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:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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:60
bool has_w_entry(irep_idt object) const
Definition rw_set.h:80
bool has_r_entry(irep_idt object) const
Definition rw_set.h:85
bool empty() const
Definition rw_set.h:75
virtual void track_deref(const entryt &, bool read)
Definition rw_set.h:93
std::unordered_map< irep_idt, entryt > entriest
Definition rw_set.h:59
virtual void reset_track_deref()
Definition rw_set.h:98
rw_set_baset(const namespacet &_ns, message_handlert &message_handler)
Definition rw_set.h:37
void swap(rw_set_baset &other)
Definition rw_set.h:62
entriest w_entries
Definition rw_set.h:60
void output(std::ostream &out) const
Definition rw_set.cpp:22
rw_set_baset & operator+=(const rw_set_baset &other)
Definition rw_set.h:68
const namespacet & ns
Definition rw_set.h:100
virtual void set_track_deref()
Definition rw_set.h:97
message_handlert & message_handler
Definition rw_set.h:101
virtual ~rw_set_baset()=default
const goto_functionst & goto_functions
Definition rw_set.h:233
void compute_rec(const exprt &function)
Definition rw_set.cpp:193
const namespacet ns
Definition rw_set.h:231
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function, message_handlert &message_handler)
Definition rw_set.h:217
value_setst & value_sets
Definition rw_set.h:232
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Definition rw_set.h:199
void reset_track_deref()
Definition rw_set.h:306
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition rw_set.h:248
std::vector< entryt > dereferenced
Definition rw_set.h:286
void set_track_deref()
Definition rw_set.h:301
void track_deref(const entryt &entry, bool read)
Definition rw_set.h:288
std::set< irep_idt > set_reads
Definition rw_set.h:251
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol Table + CFG.
static int8_t r
Definition irep_hash.h:60
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
Field-insensitive, location-sensitive may-alias analysis.
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Definition rw_set.h:104
API to expression classes.
irep_idt object
Definition rw_set.h:47
symbol_exprt symbol_expr
Definition rw_set.h:46
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)
Definition rw_set.h:50