cprover
fence_shared.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
9 #include "fence_shared.h"
10 
11 #include <iostream>
12 #include <sstream>
13 #include <fstream>
14 #include <list>
15 #include <vector>
16 #include <set>
17 
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 #include <util/message.h>
21 
25 #include <goto-instrument/rw_set.h>
26 // #include <goto-instrument/nondet_volatile.h>
27 
28 #ifdef LOCAL_MAY
30 #endif
31 
32 #define OUTPUT(s, fence, file, line, id, type) \
33  s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'
34 
36 {
37 protected:
41  const namespacet ns;
43 
44  struct
45  {
46  std::list<symbol_exprt> writes;
47  std::list<symbol_exprt> reads;
48  } fenced_edges;
49 
50  virtual void compute()=0;
51 
52  /* prints final results */
53  void print_to_file() const
54  {
55  source_locationt emptyloc;
56 
57  /* removes redundant (due to several call to the same fenced function) */
58  std::set<std::string> non_redundant_display;
59 
60  for(std::list<symbol_exprt>::const_iterator it=fenced_edges.writes.begin();
61  it!=fenced_edges.writes.end();
62  ++it)
63  {
64  std::ostringstream s;
65 
66  if(it->source_location().as_string().empty())
67  continue;
68 
69  OUTPUT(
70  s,
71  "fence",
72  it->source_location().get_file(),
73  it->source_location().get_line(),
74  ns.lookup(it->get_identifier()).base_name,
75  "Write");
76  non_redundant_display.insert(s.str());
77  }
78 
79  for(std::list<symbol_exprt>::const_iterator it=fenced_edges.reads.begin();
80  it!=fenced_edges.reads.end();
81  ++it)
82  {
83  std::ostringstream s;
84 
85  if(it->source_location().as_string().empty())
86  continue;
87 
88  OUTPUT(
89  s,
90  "fence",
91  it->source_location().get_file(),
92  it->source_location().get_line(),
93  ns.lookup(it->get_identifier()).base_name,
94  "Read");
95  non_redundant_display.insert(s.str());
96  }
97 
98  std::ofstream results;
99  results.open("results.txt");
100  for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
101  it!=non_redundant_display.end();
102  ++it)
103  results << *it;
104  results.close();
105  }
106 
107 public:
109  messaget &_message,
110  value_setst &_value_sets,
111  const symbol_tablet &_symbol_table,
112  const goto_functionst &_goto_functions)
113  :message(_message), value_sets(_value_sets), symbol_table(_symbol_table),
114  ns(_symbol_table), goto_functions(_goto_functions)
115  {}
116 
117  virtual ~simple_insertiont() {}
118 
119  void do_it()
120  {
121  compute();
122  print_to_file();
123  }
124 };
125 
126 /* fence insertion for all shared accesses */
128 {
129 protected:
130  void compute();
131 
132 public:
134  messaget &_message,
135  value_setst &_value_sets,
136  const symbol_tablet &_symbol_table,
137  const goto_functionst &_goto_functions)
138  :simple_insertiont(_message, _value_sets, _symbol_table, _goto_functions)
139  {}
140 };
141 
142 /* fence insertion for all shared accesses */
144 {
145 protected:
146  void compute();
147  std::set<irep_idt> visited_functions;
149 #ifdef LOCAL_MAY
150  , local_may_aliast &local_may
151 #endif
152  ); // NOLINT(whitespace/parens)
153 
154 public:
156  messaget &_message,
157  value_setst &_value_sets,
158  const symbol_tablet &_symbol_table,
159  const goto_functionst &_goto_functions)
160  :fence_all_sharedt(_message, _value_sets, _symbol_table, _goto_functions)
161  {}
162 };
163 
164 /* fence insertion for volatile accesses (a la MSVC) */
166 {
167 protected:
168  void compute();
169  bool is_volatile(const typet &src) const;
170 
171 public:
173  messaget &_message,
174  value_setst &_value_sets,
175  const symbol_tablet &_symbol_table,
176  const goto_functionst &_goto_functions)
177  :simple_insertiont(_message, _value_sets, _symbol_table, _goto_functions)
178  {}
179 };
180 
184 bool fence_volatilet::is_volatile(const typet &src) const
185 {
186  if(src.get_bool(ID_C_volatile))
187  return true;
188 
189 // std::cout << "type: " << src << " has sub: "
190 // << src.subtypes().empty() /*src.has_subtypes()*/ << '\n';
191  if(src.id()==ID_symbol)
192  {
193  symbol_tablet::symbolst::const_iterator s_it=
194  symbol_table.symbols.find(to_symbol_type(src).get_identifier());
195  assert(s_it!=symbol_table.symbols.end());
196  return is_volatile(s_it->second.type);
197  }
198  else if(src.has_subtype())
199  {
200  /* if a pointer points to a volatile variable, then any access through this
201  pointer has also to be considered as volatile (conservative) */
202  if(is_volatile(src.subtype()))
203  return true;
204  }
205  else if(src.has_subtypes())
206  {
207  /* if a pointer points to a volatile variable, then any access through this
208  pointer has also to be considered as volatile (conservative) */
209  bool vol=false;
210  for(typet::subtypest::const_iterator it=src.subtypes().begin();
211  it!=src.subtypes().end();
212  ++it)
213  {
214  // std::cout << *it << '\n';
215  vol|=is_volatile(*it);
216  if(vol)
217  break;
218  }
219  return vol;
220  }
221 
222  return false;
223 }
224 
226 {
227  std::cout << "--------\n";
228 
230  {
231  #ifdef LOCAL_MAY
232  local_may_aliast local_may(f_it->second);
233  #endif
234 
235  forall_goto_program_instructions(i_it, f_it->second.body)
236  {
237  rw_set_loct rw_set(ns, value_sets, i_it
238  #ifdef LOCAL_MAY
239  , local_may
240  #endif
241  ); // NOLINT(whitespace/parens)
242  forall_rw_set_w_entries(w_it, rw_set)
243  {
244  if(has_prefix(id2string(w_it->second.object), CPROVER_PREFIX))
245  continue;
246 
247  try
248  {
249  message.debug() << "debug: "
250  << id2string(w_it->second.object) << messaget::eom;
251  const symbolt &var=ns.lookup(w_it->second.object);
252  if(is_volatile(var.type))
253  {
254  message.debug() << "volatile: "
255  << id2string(w_it->second.object) << messaget::eom;
256  fenced_edges.writes.push_front(w_it->second.symbol_expr);
257  }
258  }
259  catch(std::string s)
260  {
261  message.warning() << "failed to find" << s
262  << messaget::eom;
263  continue;
264  }
265  }
266  forall_rw_set_r_entries(r_it, rw_set)
267  {
268  if(has_prefix(id2string(r_it->second.object), CPROVER_PREFIX))
269  continue;
270 
271  try
272  {
273  message.debug() << "debug: "
274  << id2string(r_it->second.object) << messaget::eom;
275  const symbolt &var=ns.lookup(r_it->second.object);
276  #if 0
277  // NOLINTNEXTLINE(readability/braces)
278  if(var.is_volatile && !var.is_thread_local)
279  #endif
280  if(is_volatile(var.type))
281  {
282  message.debug() << "volatile: "
283  << id2string(r_it->second.object) << messaget::eom;
284  fenced_edges.reads.push_front(r_it->second.symbol_expr);
285  }
286  }
287  catch (std::string s)
288  {
289  message.warning() << "failed to find" << s
290  << messaget::eom;
291  continue;
292  }
293  }
294  }
295  }
296 }
297 
299 {
300  std::cout << "--------\n";
301 
303  {
304 #ifdef LOCAL_MAY
305  local_may_aliast local_may(f_it->second);
306 #endif
307 
308  forall_goto_program_instructions(i_it, f_it->second.body)
309  {
310  if(i_it->is_function_call())
311  continue;
312 
313  rw_set_with_trackt rw_set(ns, value_sets, i_it
314 #ifdef LOCAL_MAY
315  , local_may
316 #endif
317  ); // NOLINT(whitespace/parens)
318  forall_rw_set_w_entries(w_it, rw_set)
319  {
320  if(has_prefix(id2string(w_it->second.object), CPROVER_PREFIX))
321  continue;
322 
323  try
324  {
325  const symbolt &var=ns.lookup(w_it->second.object);
326  message.debug() << "debug: "
327  << id2string(w_it->second.object) << " shared: " << var.is_shared()
328  << " loc: " << w_it->second.symbol_expr.source_location()
329  << messaget::eom;
330  if(var.is_shared())
331  {
332  /* this variable has perhaps been discovered after dereferencing
333  a pointer. We want to report this pointer */
334  std::map<const irep_idt, const irep_idt> &ref=
335  rw_set.dereferenced_from;
336  if(ref.find(w_it->second.object)!=ref.end())
337  {
338  const irep_idt from=ref[w_it->second.object];
339  const rw_set_baset::entryt &entry=
340  rw_set.set_reads.find(from)!=rw_set.set_reads.end() ?
341  rw_set.r_entries[from] :
342  rw_set.w_entries[from];
343  message.debug() << "shared: (through "
344  << id2string(w_it->second.object) << ") " << entry.object
345  << messaget::eom;
346  fenced_edges.writes.push_front(entry.symbol_expr);
347  }
348  else
349  {
350  message.debug() << "shared: "
351  << id2string(w_it->second.object) << " -> "
352  << w_it->second.object << messaget::eom;
353  fenced_edges.writes.push_front(w_it->second.symbol_expr);
354  }
355  }
356  }
357  catch(std::string s)
358  {
359  message.warning() << "failed to find" << s
360  << messaget::eom;
361  continue;
362  }
363  }
364  forall_rw_set_r_entries(r_it, rw_set)
365  {
366  if(has_prefix(id2string(r_it->second.object), CPROVER_PREFIX))
367  continue;
368 
369  try
370  {
371  const symbolt &var=ns.lookup(r_it->second.object);
372  message.debug() << "debug: "
373  << id2string(r_it->second.object) << " shared: "
374  << var.is_shared() << " loc: "
375  << r_it->second.symbol_expr.source_location() << messaget::eom;
376  if(var.is_shared())
377  {
378  /* this variable has perhaps been discovered after dereferencing
379  a pointer. We want to report this pointer */
380  std::map<const irep_idt, const irep_idt>&
381  ref=rw_set.dereferenced_from;
382  if(ref.find(r_it->second.object)!=ref.end())
383  {
384  const irep_idt from=ref[r_it->second.object];
385  const rw_set_baset::entryt &entry=
386  rw_set.set_reads.find(from)!=rw_set.set_reads.end() ?
387  rw_set.r_entries[from] :
388  rw_set.w_entries[from];
389 
390  message.debug() << "shared: (through "
391  << id2string(r_it->second.object) << ") " << entry.object
392  << messaget::eom;
393  fenced_edges.reads.push_front(entry.symbol_expr);
394  }
395  else
396  {
397  message.debug() << "shared: "
398  << id2string(r_it->second.object) << " -> "
399  << r_it->second.object << messaget::eom;
400  fenced_edges.reads.push_front(r_it->second.symbol_expr);
401  }
402  }
403  }
404  catch(std::string s)
405  {
406  message.warning() << "failed to find" << s
407  << messaget::eom;
408  continue;
409  }
410  }
411  }
412  }
413 }
414 
416 {
417  message.status() << "--------" << messaget::eom;
418 
421  #ifdef LOCAL_MAY
422  local_may_aliast local_may(main);
423  #endif
424 
426 #ifdef LOCAL_MAY
427  , local_may
428 #endif
429  ); // NOLINT(whitespace/parens)
430 }
431 
433  const goto_programt &code
434 #ifdef LOCAL_MAY
435  , local_may_aliast &local_may
436 #endif
437 )
438 {
440  {
441  if(i_it->is_function_call())
442  {
443  const exprt &fun=to_code_function_call(i_it->code).function();
444 
445  if(fun.id()!=goto_functionst::entry_point())
446  continue;
447 
448  const irep_idt &fun_id=to_symbol_expr(fun).get_identifier();
449 
450  if(visited_functions.find(fun_id)!=visited_functions.end())
451  continue;
452 
453  visited_functions.insert(fun_id);
455  goto_functions.function_map.find(fun_id)->second.body
456 #ifdef LOCAL_MAY
457  , local_may
458 #endif
459  ); // NOLINT(whitespace/parens)
460  visited_functions.erase(fun_id);
461  }
462 
463  rw_set_with_trackt rw_set(ns, value_sets, i_it
464  #ifdef LOCAL_MAY
465  , local_may
466  #endif
467  ); // NOLINT(whitespace/parens)
468  forall_rw_set_w_entries(w_it, rw_set)
469  {
470  if(has_prefix(id2string(w_it->second.object), CPROVER_PREFIX))
471  continue;
472 
473  try
474  {
475  const symbolt &var=ns.lookup(w_it->second.object);
476  message.debug() << "debug: "
477  << id2string(w_it->second.object) << " shared: "
478  << var.is_shared() << " loc: "
479  << w_it->second.symbol_expr.source_location() << messaget::eom;
480  if(var.is_shared())
481  {
482  /* this variable has perhaps been discovered after dereferencing
483  a pointer. We want to report this pointer */
484  std::map<const irep_idt, const irep_idt>&
485  ref=rw_set.dereferenced_from;
486  if(ref.find(w_it->second.object)!=ref.end())
487  {
488  const irep_idt from=ref[w_it->second.object];
489  const rw_set_baset::entryt &entry=
490  rw_set.set_reads.find(from)!=rw_set.set_reads.end() ?
491  rw_set.r_entries[from] :
492  rw_set.w_entries[from];
493 
494  message.debug() << "shared: (through "
495  << id2string(w_it->second.object) << ") " << entry.object
496  << messaget::eom;
497  fenced_edges.writes.push_front(entry.symbol_expr);
498  }
499  else
500  {
501  message.debug() << "shared: "
502  << id2string(w_it->second.object) << " -> "
503  << w_it->second.object << messaget::eom;
504  fenced_edges.writes.push_front(w_it->second.symbol_expr);
505  }
506  }
507  }
508  catch(std::string s)
509  {
510  message.warning() << "failed to find" << s
511  << messaget::eom;
512  continue;
513  }
514  }
515  forall_rw_set_r_entries(r_it, rw_set)
516  {
517  if(has_prefix(id2string(r_it->second.object), CPROVER_PREFIX))
518  continue;
519 
520  try
521  {
522  const symbolt &var=ns.lookup(r_it->second.object);
523  message.debug() << "debug: "
524  << id2string(r_it->second.object) << " shared: "
525  <<var.is_shared() << " loc: "
526  << r_it->second.symbol_expr.source_location() << messaget::eom;
527  if(var.is_shared() && var.type.id()!=ID_code)
528  {
529  /* this variable has perhaps been discovered after dereferencing
530  a pointer. We want to report this pointer */
531  std::map<const irep_idt, const irep_idt>&
532  ref=rw_set.dereferenced_from;
533  if(ref.find(r_it->second.object)!=ref.end())
534  {
535  const irep_idt from=ref[r_it->second.object];
536  const rw_set_baset::entryt &entry=
537  rw_set.set_reads.find(from)!=rw_set.set_reads.end() ?
538  rw_set.r_entries[from] :
539  rw_set.w_entries[from];
540 
541  message.debug() << "shared: (through "
542  << id2string(r_it->second.object) << ") " << entry.object
543  << messaget::eom;
544  fenced_edges.reads.push_front(entry.symbol_expr);
545  }
546  else
547  {
548  message.debug() << "shared: "
549  << id2string(r_it->second.object) << " -> "
550  << r_it->second.object << messaget::eom;
551  fenced_edges.reads.push_front(r_it->second.symbol_expr);
552  }
553  }
554  }
555  catch(std::string s)
556  {
557  message.warning() << "failed to find" << s
558  << messaget::eom;
559  continue;
560  }
561  }
562  }
563 }
564 
566  message_handlert &message_handler,
567  value_setst &value_sets,
568  symbol_tablet &symbol_table,
569  goto_functionst &goto_functions)
570 {
571  messaget message(message_handler);
572  fence_all_sharedt instrumenter(message, value_sets, symbol_table,
573  goto_functions);
574  instrumenter.do_it();
575 }
576 
578  message_handlert &message_handler,
579  value_setst &value_sets,
580  symbol_tablet &symbol_table,
581  goto_functionst &goto_functions)
582 {
583  messaget message(message_handler);
584  fence_all_shared_aegt instrumenter(message, value_sets, symbol_table,
585  goto_functions);
586  instrumenter.do_it();
587 }
588 
590  message_handlert &message_handler,
591  value_setst &value_sets,
592  symbol_tablet &symbol_table,
593  goto_functionst &goto_functions)
594 {
595  messaget message(message_handler);
596  fence_volatilet instrumenter(message, value_sets, symbol_table,
597  goto_functions);
598  instrumenter.do_it();
599 }
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
bool has_subtypes() const
Definition: type.h:70
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
bool is_thread_local
Definition: symbol.h:70
messaget & message
#define CPROVER_PREFIX
bool has_subtype() const
Definition: type.h:77
fence_all_shared_aegt(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
mstreamt & status()
Definition: message.h:238
entriest r_entries
Definition: rw_set.h:57
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
void fence_all_shared_aeg(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:108
subtypest & subtypes()
Definition: type.h:56
std::list< symbol_exprt > reads
std::map< const irep_idt, const irep_idt > dereferenced_from
Definition: rw_set.h:235
void fence_volatile(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
#define OUTPUT(s, fence, file, line, id, type)
const irep_idt & id() const
Definition: irep.h:189
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:104
const symbol_tablet & symbol_table
std::list< symbol_exprt > writes
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
symbolst symbols
Definition: symbol_table.h:57
value_setst & value_sets
Instrumenter.
std::set< irep_idt > visited_functions
The symbol table.
Definition: symbol_table.h:52
irep_idt object
Definition: rw_set.h:48
TO_BE_DOCUMENTED.
Definition: namespace.h:62
int main()
std::set< irep_idt > set_reads
Definition: rw_set.h:238
const namespacet ns
bool is_volatile
Definition: symbol.h:71
simple_insertiont(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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
mstreamt & debug()
Definition: message.h:253
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
symbol_exprt symbol_expr
Definition: rw_set.h:47
bool is_volatile(const typet &src) const
we can determine whether an access is volatile just by looking at the type of the variables involved ...
struct simple_insertiont::@17 fenced_edges
const typet & subtype() const
Definition: type.h:31
Program Transformation.
void print_to_file() const
#define forall_goto_functions(it, functions)
fence_volatilet(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
virtual ~simple_insertiont()
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const goto_functionst & goto_functions
(naive) Fence insertion
void fence_all_shared_aeg_explore(const goto_programt &code)
fence_all_sharedt(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
virtual void compute()=0
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
void fence_all_shared(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Race Detection for Threaded Goto Programs.