cprover
race_check.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Race Detection for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: February 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "race_check.h"
15 
16 #include <util/std_expr.h>
17 #include <util/guard.h>
18 #include <util/symbol_table.h>
19 #include <util/prefix.h>
20 #include <util/cprover_prefix.h>
21 
24 
27 
28 #include "rw_set.h"
29 
30 #ifdef LOCAL_MAY
32 #define L_M_ARG(x) x,
33 #define L_M_LAST_ARG(x) , x
34 #else
35 #define L_M_ARG(x)
36 #define L_M_LAST_ARG(x)
37 #endif
38 
39 class w_guardst
40 {
41 public:
42  explicit w_guardst(symbol_tablet &_symbol_table):symbol_table(_symbol_table)
43  {
44  }
45 
46  std::list<irep_idt> w_guards;
47 
48  const symbolt &get_guard_symbol(const irep_idt &object);
49 
50  const exprt get_guard_symbol_expr(const irep_idt &object)
51  {
52  return get_guard_symbol(object).symbol_expr();
53  }
54 
56  {
57  return get_guard_symbol_expr(entry.object);
58  }
59 
61  {
62  return not_exprt(get_guard_symbol_expr(entry.object));
63  }
64 
65  void add_initialization(goto_programt &goto_program) const;
66 
67 protected:
69 };
70 
72 {
73  const irep_idt identifier=id2string(object)+"$w_guard";
74 
75  const symbol_tablet::symbolst::const_iterator it=
76  symbol_table.symbols.find(identifier);
77 
78  if(it!=symbol_table.symbols.end())
79  return it->second;
80 
81  w_guards.push_back(identifier);
82 
83  symbolt new_symbol;
84  new_symbol.name=identifier;
85  new_symbol.base_name=identifier;
86  new_symbol.type=bool_typet();
87  new_symbol.is_static_lifetime=true;
88  new_symbol.value=false_exprt();
89 
90  symbolt *symbol_ptr;
91  symbol_table.move(new_symbol, symbol_ptr);
92  return *symbol_ptr;
93 }
94 
96 {
97  goto_programt::targett t=goto_program.instructions.begin();
98  const namespacet ns(symbol_table);
99 
100  for(std::list<irep_idt>::const_iterator
101  it=w_guards.begin();
102  it!=w_guards.end();
103  it++)
104  {
105  exprt symbol=ns.lookup(*it).symbol_expr();
106 
107  t=goto_program.insert_before(t);
108  t->type=ASSIGN;
109  t->code=code_assignt(symbol, false_exprt());
110 
111  t++;
112  }
113 }
114 
115 std::string comment(const rw_set_baset::entryt &entry, bool write)
116 {
117  std::string result;
118  if(write)
119  result="W/W";
120  else
121  result="R/W";
122 
123  result+=" data race on ";
124  result+=id2string(entry.object);
125  return result;
126 }
127 
129  const namespacet &ns,
130  const symbol_exprt &symbol_expr)
131 {
132  const irep_idt &identifier=symbol_expr.get_identifier();
133 
134  if(identifier==CPROVER_PREFIX "alloc" ||
135  identifier==CPROVER_PREFIX "alloc_size" ||
136  identifier=="stdin" ||
137  identifier=="stdout" ||
138  identifier=="stderr" ||
139  identifier=="sys_nerr" ||
140  has_prefix(id2string(identifier), "symex::invalid_object") ||
141  has_prefix(id2string(identifier), "symex_dynamic::dynamic_object"))
142  return false; // no race check
143 
144  const symbolt &symbol=ns.lookup(identifier);
145  return symbol.is_shared();
146 }
147 
149  const namespacet &ns,
150  const rw_set_baset &rw_set)
151 {
152  for(rw_set_baset::entriest::const_iterator
153  it=rw_set.r_entries.begin();
154  it!=rw_set.r_entries.end();
155  it++)
156  if(is_shared(ns, it->second.symbol_expr))
157  return true;
158 
159  for(rw_set_baset::entriest::const_iterator
160  it=rw_set.w_entries.begin();
161  it!=rw_set.w_entries.end();
162  it++)
163  if(is_shared(ns, it->second.symbol_expr))
164  return true;
165 
166  return false;
167 }
168 
170  value_setst &value_sets,
171  symbol_tablet &symbol_table,
172  L_M_ARG(const goto_functionst::goto_functiont &goto_function)
173  goto_programt &goto_program,
174  w_guardst &w_guards)
175 {
176  namespacet ns(symbol_table);
177 
178 #ifdef LOCAL_MAY
179  local_may_aliast local_may(goto_function);
180 #endif
181 
182  Forall_goto_program_instructions(i_it, goto_program)
183  {
184  goto_programt::instructiont &instruction=*i_it;
185 
186  if(instruction.is_assign())
187  {
188  rw_set_loct rw_set(ns, value_sets, i_it L_M_LAST_ARG(local_may));
189 
190  if(!has_shared_entries(ns, rw_set))
191  continue;
192 
193  goto_programt::instructiont original_instruction;
194  original_instruction.swap(instruction);
195 
196  instruction.make_skip();
197  i_it++;
198 
199  // now add assignments for what is written -- set
200  forall_rw_set_w_entries(e_it, rw_set)
201  {
202  if(!is_shared(ns, e_it->second.symbol_expr))
203  continue;
204 
205  goto_programt::targett t=goto_program.insert_before(i_it);
206 
207  t->type=ASSIGN;
208  t->code=code_assignt(
209  w_guards.get_w_guard_expr(e_it->second),
210  e_it->second.guard);
211 
212  t->source_location=original_instruction.source_location;
213  i_it=++t;
214  }
215 
216  // insert original statement here
217  {
218  goto_programt::targett t=goto_program.insert_before(i_it);
219  *t=original_instruction;
220  i_it=++t;
221  }
222 
223  // now add assignments for what is written -- reset
224  forall_rw_set_w_entries(e_it, rw_set)
225  {
226  if(!is_shared(ns, e_it->second.symbol_expr))
227  continue;
228 
229  goto_programt::targett t=goto_program.insert_before(i_it);
230 
231  t->type=ASSIGN;
232  t->code=code_assignt(
233  w_guards.get_w_guard_expr(e_it->second),
234  false_exprt());
235 
236  t->source_location=original_instruction.source_location;
237  i_it=++t;
238  }
239 
240  // now add assertions for what is read and written
241  forall_rw_set_r_entries(e_it, rw_set)
242  {
243  if(!is_shared(ns, e_it->second.symbol_expr))
244  continue;
245 
246  goto_programt::targett t=goto_program.insert_before(i_it);
247 
248  t->make_assertion(w_guards.get_assertion(e_it->second));
249  t->source_location=original_instruction.source_location;
250  t->source_location.set_comment(comment(e_it->second, false));
251  i_it=++t;
252  }
253 
254  forall_rw_set_w_entries(e_it, rw_set)
255  {
256  if(!is_shared(ns, e_it->second.symbol_expr))
257  continue;
258 
259  goto_programt::targett t=goto_program.insert_before(i_it);
260 
261  t->make_assertion(w_guards.get_assertion(e_it->second));
262  t->source_location=original_instruction.source_location;
263  t->source_location.set_comment(comment(e_it->second, true));
264  i_it=++t;
265  }
266 
267  i_it--; // the for loop already counts us up
268  }
269  }
270 
271  remove_skip(goto_program);
272 }
273 
275  value_setst &value_sets,
276  symbol_tablet &symbol_table,
277 #ifdef LOCAL_MAY
278  const goto_functionst::goto_functiont &goto_function,
279 #endif
280  goto_programt &goto_program)
281 {
282  w_guardst w_guards(symbol_table);
283 
284  race_check(
285  value_sets,
286  symbol_table,
287  L_M_ARG(goto_function)
288  goto_program,
289  w_guards);
290 
291  w_guards.add_initialization(goto_program);
292  goto_program.update();
293 }
294 
296  value_setst &value_sets,
297  symbol_tablet &symbol_table,
298  goto_functionst &goto_functions)
299 {
300  w_guardst w_guards(symbol_table);
301 
302  Forall_goto_functions(f_it, goto_functions)
303  if(f_it->first!=goto_functionst::entry_point() &&
304  f_it->first!=CPROVER_PREFIX "initialize")
305  race_check(
306  value_sets,
307  symbol_table,
308  L_M_ARG(f_it->second)
309  f_it->second.body,
310  w_guards);
311 
312  // get "main"
313  goto_functionst::function_mapt::iterator
314  m_it=goto_functions.function_map.find(goto_functions.entry_point());
315 
316  if(m_it==goto_functions.function_map.end())
317  throw "race check instrumentation needs an entry point";
318 
319  goto_programt &main=m_it->second.body;
320  w_guards.add_initialization(main);
321  goto_functions.update();
322 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
Boolean negation.
Definition: std_expr.h:2648
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
bool is_shared() const
Definition: symbol.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
instructionst instructions
The list of instructions in the goto program.
entriest r_entries
Definition: rw_set.h:57
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:108
#define L_M_LAST_ARG(x)
Definition: race_check.cpp:36
exprt value
Initial value of symbol.
Definition: symbol.h:40
const exprt get_guard_symbol_expr(const irep_idt &object)
Definition: race_check.cpp:50
Race Detection for Threaded Goto Programs.
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:104
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
symbolst symbols
Definition: symbol_table.h:57
Value Set Propagation.
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
irep_idt object
Definition: rw_set.h:48
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void add_initialization(goto_programt &goto_program) const
Definition: race_check.cpp:95
int main()
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:128
Guard Data Structure.
goto_function_templatet< goto_programt > goto_functiont
Symbol table.
#define L_M_ARG(x)
Definition: race_check.cpp:35
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
The boolean constant false.
Definition: std_expr.h:3753
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
entriest w_entries
Definition: rw_set.h:57
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
w_guardst(symbol_tablet &_symbol_table)
Definition: race_check.cpp:42
Base class for all expressions.
Definition: expr.h:46
const symbolt & get_guard_symbol(const irep_idt &object)
Definition: race_check.cpp:71
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:142
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:55
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:169
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::list< irep_idt > w_guards
Definition: race_check.cpp:46
symbol_tablet & symbol_table
Definition: race_check.cpp:68
bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
Definition: race_check.cpp:148
Program Transformation.
Concrete Goto Program.
Assignment.
Definition: std_code.h:144
const exprt get_assertion(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:60
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.