cprover
Loading...
Searching...
No Matches
race_check.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 "race_check.h"
15
16#include <util/prefix.h>
17
19
22
23#include "rw_set.h"
24
25#ifdef LOCAL_MAY
27#define L_M_ARG(x) x,
28#define L_M_LAST_ARG(x) , x
29#else
30#define L_M_ARG(x)
31#define L_M_LAST_ARG(x)
32#endif
33
35{
36public:
37 explicit w_guardst(symbol_tablet &_symbol_table):symbol_table(_symbol_table)
38 {
39 }
40
41 std::list<irep_idt> w_guards;
42
43 const symbolt &get_guard_symbol(const irep_idt &object);
44
46 {
47 return get_guard_symbol(object).symbol_expr();
48 }
49
51 {
52 return get_guard_symbol_expr(entry.object);
53 }
54
56 {
58 }
59
60 void add_initialization(goto_programt &goto_program) const;
61
62protected:
64};
65
67{
68 const irep_idt identifier=id2string(object)+"$w_guard";
69
70 const symbol_tablet::symbolst::const_iterator it=
71 symbol_table.symbols.find(identifier);
72
73 if(it!=symbol_table.symbols.end())
74 return it->second;
75
76 w_guards.push_back(identifier);
77
78 symbolt new_symbol;
79 new_symbol.name=identifier;
80 new_symbol.base_name=identifier;
81 new_symbol.type=bool_typet();
82 new_symbol.is_static_lifetime=true;
83 new_symbol.value=false_exprt();
84
85 symbolt *symbol_ptr;
86 symbol_table.move(new_symbol, symbol_ptr);
87 return *symbol_ptr;
88}
89
91{
92 goto_programt::targett t=goto_program.instructions.begin();
93 const namespacet ns(symbol_table);
94
95 for(std::list<irep_idt>::const_iterator
96 it=w_guards.begin();
97 it!=w_guards.end();
98 it++)
99 {
100 exprt symbol=ns.lookup(*it).symbol_expr();
101
102 t = goto_program.insert_before(
104
105 t++;
106 }
107}
108
109static std::string comment(const rw_set_baset::entryt &entry, bool write)
110{
111 std::string result;
112 if(write)
113 result="W/W";
114 else
115 result="R/W";
116
117 result+=" data race on ";
118 result+=id2string(entry.object);
119 return result;
120}
121
122static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
123{
124 const irep_idt &identifier=symbol_expr.get_identifier();
125
126 if(
127 identifier == CPROVER_PREFIX "alloc" ||
128 identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" ||
129 identifier == "stdout" || identifier == "stderr" ||
130 identifier == "sys_nerr" ||
131 has_prefix(id2string(identifier), "symex::invalid_object") ||
132 has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
133 return false; // no race check
134
135 const symbolt &symbol=ns.lookup(identifier);
136 return symbol.is_shared();
137}
138
139static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
140{
141 for(rw_set_baset::entriest::const_iterator
142 it=rw_set.r_entries.begin();
143 it!=rw_set.r_entries.end();
144 it++)
145 if(is_shared(ns, it->second.symbol_expr))
146 return true;
147
148 for(rw_set_baset::entriest::const_iterator
149 it=rw_set.w_entries.begin();
150 it!=rw_set.w_entries.end();
151 it++)
152 if(is_shared(ns, it->second.symbol_expr))
153 return true;
154
155 return false;
156}
157
158// clang-format off
159// clang-format is confused by the L_M_ARG macro and wants to indent the line
160// after
161static void race_check(
162 value_setst &value_sets,
163 symbol_tablet &symbol_table,
164 const irep_idt &function_id,
165 L_M_ARG(const goto_functionst::goto_functiont &goto_function)
166 goto_programt &goto_program,
167 w_guardst &w_guards)
168// clang-format on
169{
170 namespacet ns(symbol_table);
171
172#ifdef LOCAL_MAY
173 local_may_aliast local_may(goto_function);
174#endif
175
176 Forall_goto_program_instructions(i_it, goto_program)
177 {
178 goto_programt::instructiont &instruction=*i_it;
179
180 if(instruction.is_assign())
181 {
182 rw_set_loct rw_set(
183 ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may));
184
185 if(!has_shared_entries(ns, rw_set))
186 continue;
187
188 goto_programt::instructiont original_instruction;
189 original_instruction.swap(instruction);
190
191 instruction =
192 goto_programt::make_skip(original_instruction.source_location());
193 i_it++;
194
195 // now add assignments for what is written -- set
196 for(const auto &w_entry : rw_set.w_entries)
197 {
198 if(!is_shared(ns, w_entry.second.symbol_expr))
199 continue;
200
201 goto_programt::targett t = goto_program.insert_before(
202 i_it,
204 w_guards.get_w_guard_expr(w_entry.second),
205 w_entry.second.guard,
206 original_instruction.source_location()));
207 i_it=++t;
208 }
209
210 // insert original statement here
211 {
212 goto_programt::targett t=goto_program.insert_before(i_it);
213 *t=original_instruction;
214 i_it=++t;
215 }
216
217 // now add assignments for what is written -- reset
218 for(const auto &w_entry : rw_set.w_entries)
219 {
220 if(!is_shared(ns, w_entry.second.symbol_expr))
221 continue;
222
223 goto_programt::targett t = goto_program.insert_before(
224 i_it,
226 w_guards.get_w_guard_expr(w_entry.second),
227 false_exprt(),
228 original_instruction.source_location()));
229 i_it = std::next(t);
230 }
231
232 // now add assertions for what is read and written
233 for(const auto &r_entry : rw_set.r_entries)
234 {
235 if(!is_shared(ns, r_entry.second.symbol_expr))
236 continue;
237
238 goto_programt::targett t = goto_program.insert_before(
239 i_it,
241 w_guards.get_assertion(r_entry.second),
242 original_instruction.source_location()));
243 t->source_location_nonconst().set_comment(
244 comment(r_entry.second, false));
245 i_it=++t;
246 }
247
248 for(const auto &w_entry : rw_set.w_entries)
249 {
250 if(!is_shared(ns, w_entry.second.symbol_expr))
251 continue;
252
253 goto_programt::targett t = goto_program.insert_before(
254 i_it,
256 w_guards.get_assertion(w_entry.second),
257 original_instruction.source_location()));
258 t->source_location_nonconst().set_comment(
259 comment(w_entry.second, true));
260 i_it=++t;
261 }
262
263 i_it--; // the for loop already counts us up
264 }
265 }
266
267 remove_skip(goto_program);
268}
269
271 value_setst &value_sets,
272 symbol_tablet &symbol_table,
273 const irep_idt &function_id,
274#ifdef LOCAL_MAY
275 const goto_functionst::goto_functiont &goto_function,
276#endif
277 goto_programt &goto_program)
278{
279 w_guardst w_guards(symbol_table);
280
282 value_sets,
283 symbol_table,
284 function_id,
285 L_M_ARG(goto_function) goto_program,
286 w_guards);
287
288 w_guards.add_initialization(goto_program);
289 goto_program.update();
290}
291
293 value_setst &value_sets,
294 goto_modelt &goto_model)
295{
296 w_guardst w_guards(goto_model.symbol_table);
297
298 for(auto &gf_entry : goto_model.goto_functions.function_map)
299 {
300 if(
301 gf_entry.first != goto_functionst::entry_point() &&
302 gf_entry.first != INITIALIZE_FUNCTION)
303 {
305 value_sets,
306 goto_model.symbol_table,
307 gf_entry.first,
308 L_M_ARG(gf_entry.second) gf_entry.second.body,
309 w_guards);
310 }
311 }
312
313 // get "main"
314 goto_functionst::function_mapt::iterator
315 m_it=goto_model.goto_functions.function_map.find(
316 goto_model.goto_functions.entry_point());
317
318 if(m_it==goto_model.goto_functions.function_map.end())
319 throw "race check instrumentation needs an entry point";
320
321 goto_programt &main=m_it->second.body;
322 w_guards.add_initialization(main);
323 goto_model.goto_functions.update();
324}
The Boolean type.
Definition: std_types.h:36
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
The Boolean constant false.
Definition: std_expr.h:2865
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:522
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::iterator targett
Definition: goto_program.h:592
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
entriest r_entries
Definition: rw_set.h:59
entriest w_entries
Definition: rw_set.h:59
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_shared() const
Definition: symbol.h:95
exprt value
Initial value of symbol.
Definition: symbol.h:34
std::list< irep_idt > w_guards
Definition: race_check.cpp:41
const symbolt & get_guard_symbol(const irep_idt &object)
Definition: race_check.cpp:66
const exprt get_assertion(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:55
w_guardst(symbol_tablet &_symbol_table)
Definition: race_check.cpp:37
void add_initialization(goto_programt &goto_program) const
Definition: race_check.cpp:90
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:50
const exprt get_guard_symbol_expr(const irep_idt &object)
Definition: race_check.cpp:45
symbol_tablet & symbol_table
Definition: race_check.cpp:63
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
int main()
Definition: example.cpp:18
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Field-insensitive, location-sensitive may-alias analysis.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
static void race_check(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:161
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
Definition: race_check.cpp:139
#define L_M_ARG(x)
Definition: race_check.cpp:30
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:122
#define L_M_LAST_ARG(x)
Definition: race_check.cpp:31
Race Detection for Threaded Goto Programs.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
irep_idt object
Definition: rw_set.h:46