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/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 
34 class w_guardst
35 {
36 public:
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 
45  const exprt get_guard_symbol_expr(const irep_idt &object)
46  {
47  return get_guard_symbol(object).symbol_expr();
48  }
49 
51  {
52  return get_guard_symbol_expr(entry.object);
53  }
54 
56  {
57  return not_exprt(get_guard_symbol_expr(entry.object));
58  }
59 
60  void add_initialization(goto_programt &goto_program) const;
61 
62 protected:
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 
109 static 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 
122 static 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 
139 static 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
161 static 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  forall_rw_set_w_entries(e_it, rw_set)
197  {
198  if(!is_shared(ns, e_it->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(e_it->second),
205  e_it->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  forall_rw_set_w_entries(e_it, rw_set)
219  {
220  if(!is_shared(ns, e_it->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(e_it->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  forall_rw_set_r_entries(e_it, rw_set)
234  {
235  if(!is_shared(ns, e_it->second.symbol_expr))
236  continue;
237 
238  goto_programt::targett t = goto_program.insert_before(
239  i_it,
241  w_guards.get_assertion(e_it->second),
242  original_instruction.source_location));
243  t->source_location.set_comment(comment(e_it->second, false));
244  i_it=++t;
245  }
246 
247  forall_rw_set_w_entries(e_it, rw_set)
248  {
249  if(!is_shared(ns, e_it->second.symbol_expr))
250  continue;
251 
252  goto_programt::targett t = goto_program.insert_before(
253  i_it,
255  w_guards.get_assertion(e_it->second),
256  original_instruction.source_location));
257  t->source_location.set_comment(comment(e_it->second, true));
258  i_it=++t;
259  }
260 
261  i_it--; // the for loop already counts us up
262  }
263  }
264 
265  remove_skip(goto_program);
266 }
267 
269  value_setst &value_sets,
270  symbol_tablet &symbol_table,
271  const irep_idt &function_id,
272 #ifdef LOCAL_MAY
273  const goto_functionst::goto_functiont &goto_function,
274 #endif
275  goto_programt &goto_program)
276 {
277  w_guardst w_guards(symbol_table);
278 
279  race_check(
280  value_sets,
281  symbol_table,
282  function_id,
283  L_M_ARG(goto_function) goto_program,
284  w_guards);
285 
286  w_guards.add_initialization(goto_program);
287  goto_program.update();
288 }
289 
291  value_setst &value_sets,
292  goto_modelt &goto_model)
293 {
294  w_guardst w_guards(goto_model.symbol_table);
295 
296  Forall_goto_functions(f_it, goto_model.goto_functions)
297  if(f_it->first!=goto_functionst::entry_point() &&
298  f_it->first != INITIALIZE_FUNCTION)
299  race_check(
300  value_sets,
301  goto_model.symbol_table,
302  f_it->first,
303  L_M_ARG(f_it->second) f_it->second.body,
304  w_guards);
305 
306  // get "main"
307  goto_functionst::function_mapt::iterator
308  m_it=goto_model.goto_functions.function_map.find(
309  goto_model.goto_functions.entry_point());
310 
311  if(m_it==goto_model.goto_functions.function_map.end())
312  throw "race check instrumentation needs an entry point";
313 
314  goto_programt &main=m_it->second.body;
315  w_guards.add_initialization(main);
316  goto_model.goto_functions.update();
317 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
forall_rw_set_w_entries
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:114
rw_set_baset::entryt
Definition: rw_set.h:44
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:510
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
L_M_LAST_ARG
#define L_M_LAST_ARG(x)
Definition: race_check.cpp:31
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
pointer_predicates.h
prefix.h
w_guardst::w_guards
std::list< irep_idt > w_guards
Definition: race_check.cpp:41
race_check
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
exprt
Base class for all expressions.
Definition: expr.h:52
goto_modelt
Definition: goto_model.h:25
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool_typet
The Boolean type.
Definition: std_types.h:36
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:88
race_check.h
w_guardst::get_assertion
const exprt get_assertion(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:55
rw_set_baset::r_entries
entriest r_entries
Definition: rw_set.h:60
local_may_aliast
Definition: local_may_alias.h:25
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
is_shared
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:122
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
local_may_alias.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
w_guardst::get_guard_symbol
const symbolt & get_guard_symbol(const irep_idt &object)
Definition: race_check.cpp:66
SYMEX_DYNAMIC_PREFIX
#define SYMEX_DYNAMIC_PREFIX
Definition: pointer_predicates.h:17
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:118
forall_rw_set_r_entries
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:110
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
w_guardst::get_w_guard_expr
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:50
symbolt::is_shared
bool is_shared() const
Definition: symbol.h:95
false_exprt
The Boolean constant false.
Definition: std_expr.h:4153
rw_set_baset::w_entries
entriest w_entries
Definition: rw_set.h:60
w_guardst::symbol_table
symbol_tablet & symbol_table
Definition: race_check.cpp:63
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
L_M_ARG
#define L_M_ARG(x)
Definition: race_check.cpp:30
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
value_setst
Definition: value_sets.h:21
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
rw_set_loct
Definition: rw_set.h:185
symbolt
Symbol table entry.
Definition: symbol.h:27
rw_set.h
rw_set_baset
Definition: rw_set.h:34
w_guardst
Definition: race_check.cpp:34
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
rw_set_baset::entryt::object
irep_idt object
Definition: rw_set.h:47
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
has_shared_entries
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
Definition: race_check.cpp:139
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
w_guardst::add_initialization
void add_initialization(goto_programt &goto_program) const
Definition: race_check.cpp:90
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
remove_skip.h
main
int main()
Definition: file_converter.cpp:15
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
w_guardst::w_guardst
w_guardst(symbol_tablet &_symbol_table)
Definition: race_check.cpp:37
w_guardst::get_guard_symbol_expr
const exprt get_guard_symbol_expr(const irep_idt &object)
Definition: race_check.cpp:45
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
not_exprt
Boolean negation.
Definition: std_expr.h:2995