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