cprover
Loading...
Searching...
No Matches
rw_set.cpp
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#include "rw_set.h"
15
16#include <util/pointer_expr.h>
17#include <util/std_code.h>
18
20
22
23void rw_set_baset::output(std::ostream &out) const
24{
25 out << "READ:\n";
26 for(entriest::const_iterator it=r_entries.begin();
27 it!=r_entries.end();
28 it++)
29 {
30 out << it->second.object << " if "
31 << from_expr(ns, it->second.object, it->second.guard) << '\n';
32 }
33
34 out << '\n';
35
36 out << "WRITE:\n";
37 for(entriest::const_iterator it=w_entries.begin();
38 it!=w_entries.end();
39 it++)
40 {
41 out << it->second.object << " if "
42 << from_expr(ns, it->second.object, it->second.guard) << '\n';
43 }
44}
45
47{
48 if(target->is_assign())
49 {
50 assign(target->assign_lhs(), target->assign_rhs());
51 }
52 else if(target->is_goto() ||
53 target->is_assume() ||
54 target->is_assert())
55 {
56 read(target->get_condition());
57 }
58 else if(target->is_function_call())
59 {
60 read(target->call_function());
61
62 // do operands
63 for(code_function_callt::argumentst::const_iterator it =
64 target->call_arguments().begin();
65 it != target->call_arguments().end();
66 it++)
67 read(*it);
68
69 if(target->call_lhs().is_not_nil())
70 write(target->call_lhs());
71 }
72}
73
74void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
75{
76 read(rhs);
77 read_write_rec(lhs, false, true, "", exprt::operandst());
78}
79
81 const exprt &expr,
82 bool r,
83 bool w,
84 const std::string &suffix,
86{
87 if(expr.id()==ID_symbol)
88 {
89 const symbol_exprt &symbol_expr=to_symbol_expr(expr);
90
91 irep_idt object=id2string(symbol_expr.get_identifier())+suffix;
92
93 if(r)
94 {
95 const auto &entry = r_entries.emplace(
96 object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
97
98 track_deref(entry.first->second, true);
99 }
100
101 if(w)
102 {
103 const auto &entry = w_entries.emplace(
104 object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
105
106 track_deref(entry.first->second, false);
107 }
108 }
109 else if(expr.id()==ID_member)
110 {
111 const auto &member_expr = to_member_expr(expr);
112 const std::string &component_name =
113 id2string(member_expr.get_component_name());
115 member_expr.compound(),
116 r,
117 w,
118 "." + component_name + suffix,
120 }
121 else if(expr.id()==ID_index)
122 {
123 // we don't distinguish the array elements for now
124 const auto &index_expr = to_index_expr(expr);
125 read_write_rec(index_expr.array(), r, w, "[]" + suffix, guard_conjuncts);
127 }
128 else if(expr.id()==ID_dereference)
129 {
131 read(to_dereference_expr(expr).pointer(), guard_conjuncts);
132
133 exprt tmp=expr;
134 #ifdef LOCAL_MAY
135 const std::set<exprt> aliases=local_may.get(target, expr);
136 for(std::set<exprt>::const_iterator it=aliases.begin();
137 it!=aliases.end();
138 ++it)
139 {
140 #ifndef LOCAL_MAY_SOUND
141 if(it->id()==ID_unknown)
142 {
143 /* as an under-approximation */
144 // std::cout << "Sorry, LOCAL_MAY too imprecise. "
145 // << Omitting some variables.\n";
146 irep_idt object=ID_unknown;
147
148 entryt &entry=r_entries[object];
149 entry.object=object;
151 entry.guard = conjunction(guard_conjuncts); // should 'OR'
152
153 continue;
154 }
155 #endif
156 read_write_rec(*it, r, w, suffix, guard_conjuncts);
157 }
158 #else
160
162#endif
163
165 }
166 else if(expr.id()==ID_typecast)
167 {
168 read_write_rec(to_typecast_expr(expr).op(), r, w, suffix, guard_conjuncts);
169 }
170 else if(expr.id()==ID_address_of)
171 {
172 assert(expr.operands().size()==1);
173 }
174 else if(expr.id()==ID_if)
175 {
176 const auto &if_expr = to_if_expr(expr);
178
180 true_guard.push_back(if_expr.cond());
181 read_write_rec(if_expr.true_case(), r, w, suffix, true_guard);
182
184 false_guard.push_back(not_exprt(if_expr.cond()));
185 read_write_rec(if_expr.false_case(), r, w, suffix, false_guard);
186 }
187 else
188 {
189 forall_operands(it, expr)
190 read_write_rec(*it, r, w, suffix, guard_conjuncts);
191 }
192}
193
195{
196 if(function.id()==ID_symbol)
197 {
198 const irep_idt &function_id = to_symbol_expr(function).get_identifier();
199
200 goto_functionst::function_mapt::const_iterator f_it =
201 goto_functions.function_map.find(function_id);
202
204 {
205 const goto_programt &body=f_it->second.body;
206
207#ifdef LOCAL_MAY
209#if 0
210 for(goto_functionst::function_mapt::const_iterator
213 local_may(g_it->second);
214#endif
215#endif
216
218 {
219 *this += rw_set_loct(
220 ns,
222 function_id,
223 i_it
225 ,
227#endif
228 ); // NOLINT(whitespace/parens)
229 }
230 }
231 }
232 else if(function.id()==ID_if)
233 {
234 compute_rec(to_if_expr(function).true_case());
235 compute_rec(to_if_expr(function).false_case());
236 }
237}
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
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
void write(const exprt &expr)
Definition rw_set.h:159
const goto_programt::const_targett target
Definition rw_set.h:143
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
operandst & operands()
Definition expr.h:92
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & id() const
Definition irep.h:396
Boolean negation.
Definition std_expr.h:2181
entriest r_entries
Definition rw_set.h:59
virtual void track_deref(const entryt &, bool read)
Definition rw_set.h:92
virtual void reset_track_deref()
Definition rw_set.h:97
entriest w_entries
Definition rw_set.h:59
void output(std::ostream &out) const
Definition rw_set.cpp:23
const namespacet & ns
Definition rw_set.h:99
virtual void set_track_deref()
Definition rw_set.h:96
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
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
#define forall_operands(it, expr)
Definition expr.h:18
#define forall_goto_program_instructions(it, program)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Race Detection for Threaded Goto Programs.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:34
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
irep_idt object
Definition rw_set.h:46
symbol_exprt symbol_expr
Definition rw_set.h:45