CBMC
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 
21 
22 #include "rw_set.h"
23 
24 #ifdef LOCAL_MAY
26 #define L_M_ARG(x) x,
27 #define L_M_LAST_ARG(x) , x
28 #else
29 #define L_M_ARG(x)
30 #define L_M_LAST_ARG(x)
31 #endif
32 
33 class w_guardst
34 {
35 public:
36  explicit w_guardst(symbol_table_baset &_symbol_table)
37  : 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_table_baset::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  identifier, bool_typet(), symbol_table.lookup_ref(object).mode};
80  new_symbol.base_name=identifier;
81  new_symbol.is_static_lifetime=true;
82  new_symbol.value=false_exprt();
83 
84  symbolt *symbol_ptr;
85  symbol_table.move(new_symbol, symbol_ptr);
86  return *symbol_ptr;
87 }
88 
90 {
91  goto_programt::targett t=goto_program.instructions.begin();
92  const namespacet ns(symbol_table);
93 
94  for(std::list<irep_idt>::const_iterator
95  it=w_guards.begin();
96  it!=w_guards.end();
97  it++)
98  {
99  exprt symbol=ns.lookup(*it).symbol_expr();
100 
101  t = goto_program.insert_before(
103 
104  t++;
105  }
106 }
107 
108 static std::string comment(const rw_set_baset::entryt &entry, bool write)
109 {
110  std::string result;
111  if(write)
112  result="W/W";
113  else
114  result="R/W";
115 
116  result+=" data race on ";
117  result+=id2string(entry.object);
118  return result;
119 }
120 
121 static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
122 {
123  const irep_idt &identifier=symbol_expr.get_identifier();
124 
125  if(
126  identifier == CPROVER_PREFIX "alloc" ||
127  identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" ||
128  identifier == "stdout" || identifier == "stderr" ||
129  identifier == "sys_nerr" ||
130  identifier.starts_with("symex::invalid_object") ||
131  identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
132  return false; // no race check
133 
134  const symbolt &symbol=ns.lookup(identifier);
135  return symbol.is_shared();
136 }
137 
138 static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
139 {
140  for(rw_set_baset::entriest::const_iterator
141  it=rw_set.r_entries.begin();
142  it!=rw_set.r_entries.end();
143  it++)
144  if(is_shared(ns, it->second.symbol_expr))
145  return true;
146 
147  for(rw_set_baset::entriest::const_iterator
148  it=rw_set.w_entries.begin();
149  it!=rw_set.w_entries.end();
150  it++)
151  if(is_shared(ns, it->second.symbol_expr))
152  return true;
153 
154  return false;
155 }
156 
157 // clang-format off
158 // clang-format is confused by the L_M_ARG macro and wants to indent the line
159 // after
160 static void race_check(
161  value_setst &value_sets,
162  symbol_table_baset &symbol_table,
163  const irep_idt &function_id,
164  L_M_ARG(const goto_functionst::goto_functiont &goto_function)
165  goto_programt &goto_program,
166  w_guardst &w_guards,
167  message_handlert &message_handler)
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,
184  value_sets,
185  function_id,
186  i_it L_M_LAST_ARG(local_may),
187  message_handler);
188 
189  if(!has_shared_entries(ns, rw_set))
190  continue;
191 
192  goto_programt::instructiont original_instruction;
193  original_instruction.swap(instruction);
194 
195  instruction =
196  goto_programt::make_skip(original_instruction.source_location());
197  i_it++;
198 
199  // now add assignments for what is written -- set
200  for(const auto &w_entry : rw_set.w_entries)
201  {
202  if(!is_shared(ns, w_entry.second.symbol_expr))
203  continue;
204 
205  goto_program.insert_before(
206  i_it,
208  w_guards.get_w_guard_expr(w_entry.second),
209  w_entry.second.guard,
210  original_instruction.source_location()));
211  }
212 
213  // insert original statement here
214  {
215  goto_programt::targett t=goto_program.insert_before(i_it);
216  *t=original_instruction;
217  }
218 
219  // now add assignments for what is written -- reset
220  for(const auto &w_entry : rw_set.w_entries)
221  {
222  if(!is_shared(ns, w_entry.second.symbol_expr))
223  continue;
224 
225  goto_program.insert_before(
226  i_it,
228  w_guards.get_w_guard_expr(w_entry.second),
229  false_exprt(),
230  original_instruction.source_location()));
231  }
232 
233  // now add assertions for what is read and written
234  for(const auto &r_entry : rw_set.r_entries)
235  {
236  if(!is_shared(ns, r_entry.second.symbol_expr))
237  continue;
238 
239  source_locationt annotated_location =
240  original_instruction.source_location();
241  annotated_location.set_comment(comment(r_entry.second, false));
242  goto_program.insert_before(
243  i_it,
245  w_guards.get_assertion(r_entry.second), annotated_location));
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  source_locationt annotated_location =
254  original_instruction.source_location();
255  annotated_location.set_comment(comment(w_entry.second, true));
256  goto_program.insert_before(
257  i_it,
259  w_guards.get_assertion(w_entry.second), annotated_location));
260  }
261 
262  i_it--; // the for loop already counts us up
263  }
264  }
265 
266  remove_skip(goto_program);
267 }
268 
270  value_setst &value_sets,
271  symbol_table_baset &symbol_table,
272  const irep_idt &function_id,
273 #ifdef LOCAL_MAY
274  const goto_functionst::goto_functiont &goto_function,
275 #endif
276  goto_programt &goto_program,
277  message_handlert &message_handler)
278 {
279  w_guardst w_guards(symbol_table);
280 
281  race_check(
282  value_sets,
283  symbol_table,
284  function_id,
285  L_M_ARG(goto_function) goto_program,
286  w_guards,
287  message_handler);
288 
289  w_guards.add_initialization(goto_program);
290  goto_program.update();
291 }
292 
294  value_setst &value_sets,
295  goto_modelt &goto_model,
296  message_handlert &message_handler)
297 {
298  w_guardst w_guards(goto_model.symbol_table);
299 
300  for(auto &gf_entry : goto_model.goto_functions.function_map)
301  {
302  if(
303  gf_entry.first != goto_functionst::entry_point() &&
304  gf_entry.first != INITIALIZE_FUNCTION)
305  {
306  race_check(
307  value_sets,
308  goto_model.symbol_table,
309  gf_entry.first,
310  L_M_ARG(gf_entry.second) gf_entry.second.body,
311  w_guards,
312  message_handler);
313  }
314  }
315 
316  // get "main"
317  goto_functionst::function_mapt::iterator
318  m_it=goto_model.goto_functions.function_map.find(
319  goto_model.goto_functions.entry_point());
320 
321  if(m_it==goto_model.goto_functions.function_map.end())
322  throw "race check instrumentation needs an entry point";
323 
324  goto_programt &main=m_it->second.body;
325  w_guards.add_initialization(main);
326  goto_model.goto_functions.update();
327 }
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
Base class for all expressions.
Definition: expr.h:56
The Boolean constant false.
Definition: std_expr.h:3072
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.
Definition: goto_program.h:181
const source_locationt & source_location() const
Definition: goto_program.h:333
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:541
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:622
instructionst::iterator targett
Definition: goto_program.h:614
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:891
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:692
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Boolean negation.
Definition: std_expr.h:2327
entriest r_entries
Definition: rw_set.h:60
entriest w_entries
Definition: rw_set.h:60
void set_comment(const irep_idt &comment)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
bool is_shared() const
Definition: symbol.h:101
irep_idt mode
Language mode.
Definition: symbol.h:49
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
void add_initialization(goto_programt &goto_program) const
Definition: race_check.cpp:89
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
Definition: race_check.cpp:50
symbol_table_baset & symbol_table
Definition: race_check.cpp:63
const exprt get_guard_symbol_expr(const irep_idt &object)
Definition: race_check.cpp:45
w_guardst(symbol_table_baset &_symbol_table)
Definition: race_check.cpp:36
#define CPROVER_PREFIX
int main(int argc, char *argv[])
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Field-insensitive, location-sensitive may-alias analysis.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
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, message_handlert &message_handler)
Definition: race_check.cpp:160
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
Definition: race_check.cpp:138
#define L_M_ARG(x)
Definition: race_check.cpp:29
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Definition: race_check.cpp:121
#define L_M_LAST_ARG(x)
Definition: race_check.cpp:30
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:87
Program Transformation.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
irep_idt object
Definition: rw_set.h:47
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:195