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:
41
42 std::list<irep_idt> w_guards;
43
44 const symbolt &get_guard_symbol(const irep_idt &object);
45
47 {
48 return get_guard_symbol(object).symbol_expr();
49 }
50
52 {
53 return get_guard_symbol_expr(entry.object);
54 }
55
57 {
59 }
60
61 void add_initialization(goto_programt &goto_program) const;
62
63protected:
65};
66
68{
69 const irep_idt identifier=id2string(object)+"$w_guard";
70
71 const symbol_table_baset::symbolst::const_iterator it =
72 symbol_table.symbols.find(identifier);
73
74 if(it!=symbol_table.symbols.end())
75 return it->second;
76
77 w_guards.push_back(identifier);
78
79 symbolt new_symbol{
80 identifier, bool_typet(), symbol_table.lookup_ref(object).mode};
81 new_symbol.base_name=identifier;
82 new_symbol.is_static_lifetime=true;
83 new_symbol.value=false_exprt();
84
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_table_baset &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
177 {
178 goto_programt::instructiont &instruction=*i_it;
179
180 if(instruction.is_assign())
181 {
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
189 original_instruction.swap(instruction);
190
191 instruction =
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_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 }
208
209 // insert original statement here
210 {
211 goto_programt::targett t=goto_program.insert_before(i_it);
213 }
214
215 // now add assignments for what is written -- reset
216 for(const auto &w_entry : rw_set.w_entries)
217 {
218 if(!is_shared(ns, w_entry.second.symbol_expr))
219 continue;
220
221 goto_program.insert_before(
222 i_it,
224 w_guards.get_w_guard_expr(w_entry.second),
225 false_exprt(),
226 original_instruction.source_location()));
227 }
228
229 // now add assertions for what is read and written
230 for(const auto &r_entry : rw_set.r_entries)
231 {
232 if(!is_shared(ns, r_entry.second.symbol_expr))
233 continue;
234
236 original_instruction.source_location();
237 annotated_location.set_comment(comment(r_entry.second, false));
238 goto_program.insert_before(
239 i_it,
241 w_guards.get_assertion(r_entry.second), annotated_location));
242 }
243
244 for(const auto &w_entry : rw_set.w_entries)
245 {
246 if(!is_shared(ns, w_entry.second.symbol_expr))
247 continue;
248
250 original_instruction.source_location();
251 annotated_location.set_comment(comment(w_entry.second, true));
252 goto_program.insert_before(
253 i_it,
255 w_guards.get_assertion(w_entry.second), annotated_location));
256 }
257
258 i_it--; // the for loop already counts us up
259 }
260 }
261
262 remove_skip(goto_program);
263}
264
266 value_setst &value_sets,
267 symbol_table_baset &symbol_table,
268 const irep_idt &function_id,
270 const goto_functionst::goto_functiont &goto_function,
271#endif
272 goto_programt &goto_program)
273{
274 w_guardst w_guards(symbol_table);
275
277 value_sets,
278 symbol_table,
279 function_id,
280 L_M_ARG(goto_function) goto_program,
281 w_guards);
282
283 w_guards.add_initialization(goto_program);
284 goto_program.update();
285}
286
288 value_setst &value_sets,
289 goto_modelt &goto_model)
290{
291 w_guardst w_guards(goto_model.symbol_table);
292
293 for(auto &gf_entry : goto_model.goto_functions.function_map)
294 {
295 if(
298 {
300 value_sets,
301 goto_model.symbol_table,
302 gf_entry.first,
303 L_M_ARG(gf_entry.second) gf_entry.second.body,
304 w_guards);
305 }
306 }
307
308 // get "main"
309 goto_functionst::function_mapt::iterator
310 m_it=goto_model.goto_functions.function_map.find(
311 goto_model.goto_functions.entry_point());
312
313 if(m_it==goto_model.goto_functions.function_map.end())
314 throw "race check instrumentation needs an entry point";
315
316 goto_programt &main=m_it->second.body;
317 w_guards.add_initialization(main);
318 goto_model.goto_functions.update();
319}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3017
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:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
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())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
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().
Boolean negation.
Definition std_expr.h:2278
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
The symbol table base class interface.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
bool is_shared() const
Definition symbol.h:101
std::list< irep_idt > w_guards
const symbolt & get_guard_symbol(const irep_idt &object)
const exprt get_assertion(const rw_set_baset::entryt &entry)
void add_initialization(goto_programt &goto_program) const
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
symbol_table_baset & symbol_table
const exprt get_guard_symbol_expr(const irep_idt &object)
w_guardst(symbol_table_baset &_symbol_table)
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)
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
#define L_M_ARG(x)
static void race_check(value_setst &value_sets, symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
#define L_M_LAST_ARG(x)
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
Program Transformation.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
irep_idt object
Definition rw_set.h:46