cprover
shared_buffers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "shared_buffers.h"
10 
11 #include <util/c_types.h>
12 #include <util/fresh_symbol.h>
13 
15 
16 #include <goto-instrument/rw_set.h>
17 
18 #include "fence.h"
19 
21 std::string shared_bufferst::unique(void)
22 {
24  return "$fresh#"+std::to_string(uniq++);
25 }
26 
29  const irep_idt &object)
30 {
31  var_mapt::const_iterator it=var_map.find(object);
32  if(it!=var_map.end())
33  return it->second;
34 
35  varst &vars=var_map[object];
36 
38  const symbolt &symbol=ns.lookup(object);
39 
40  vars.type=symbol.type;
41 
42  vars.w_buff0=add(object, symbol.base_name, "$w_buff0", symbol.type);
43  vars.w_buff1=add(object, symbol.base_name, "$w_buff1", symbol.type);
44 
45  vars.w_buff0_used=add(object, symbol.base_name, "$w_buff0_used",
46  bool_typet());
47  vars.w_buff1_used=add(object, symbol.base_name, "$w_buff1_used",
48  bool_typet());
49 
50  vars.mem_tmp=add(object, symbol.base_name, "$mem_tmp", symbol.type);
51  vars.flush_delayed=add(object, symbol.base_name, "$flush_delayed",
52  bool_typet());
53 
54  vars.read_delayed=
55  add(object, symbol.base_name, "$read_delayed", bool_typet());
56  vars.read_delayed_var=
57  add(
58  object,
59  symbol.base_name,
60  "$read_delayed_var",
61  pointer_type(symbol.type));
62 
63  for(unsigned cnt=0; cnt<nb_threads; cnt++)
64  {
65  vars.r_buff0_thds.push_back(
67  object,
68  symbol.base_name,
69  "$r_buff0_thd"+std::to_string(cnt),
70  bool_typet()));
71  vars.r_buff1_thds.push_back(
73  object,
74  symbol.base_name,
75  "$r_buff1_thd"+std::to_string(cnt),
76  bool_typet()));
77  }
78 
79  return vars;
80 }
81 
86  const irep_idt &object,
87  const irep_idt &base_name,
88  const std::string &suffix,
89  const typet &type,
90  bool instrument)
91 {
92  const namespacet ns(symbol_table);
93 
94  symbolt &new_symbol = get_fresh_aux_symbol(
95  type,
96  id2string(object) + suffix,
97  id2string(base_name) + suffix,
98  ns.lookup(object).location,
99  ns.lookup(object).mode,
100  symbol_table);
101  new_symbol.is_static_lifetime=true;
102  new_symbol.value.make_nil();
103 
104  if(instrument)
105  instrumentations.insert(new_symbol.name);
106 
107  return new_symbol.name;
108 }
109 
111 {
112  goto_programt::targett t=goto_program.instructions.begin();
113  const namespacet ns(symbol_table);
114 
115  for(const auto &vars : var_map)
116  {
117  source_locationt source_location;
118  source_location.make_nil();
119 
120  assignment(goto_program, t, source_location, vars.second.w_buff0_used,
121  false_exprt());
122  assignment(goto_program, t, source_location, vars.second.w_buff1_used,
123  false_exprt());
124  assignment(goto_program, t, source_location, vars.second.flush_delayed,
125  false_exprt());
126  assignment(goto_program, t, source_location, vars.second.read_delayed,
127  false_exprt());
128  assignment(goto_program, t, source_location, vars.second.read_delayed_var,
129  null_pointer_exprt(pointer_type(vars.second.type)));
130 
131  for(const auto &id : vars.second.r_buff0_thds)
132  assignment(goto_program, t, source_location, id, false_exprt());
133 
134  for(const auto &id : vars.second.r_buff1_thds)
135  assignment(goto_program, t, source_location, id, false_exprt());
136  }
137 }
138 
140  goto_functionst &goto_functions)
141 {
142  // get "main"
143  goto_functionst::function_mapt::iterator
144  m_it=goto_functions.function_map.find(goto_functions.entry_point());
145 
146  if(m_it==goto_functions.function_map.end())
147  throw "weak memory instrumentation needs an entry point";
148 
149  goto_programt &main=m_it->second.body;
151 }
152 
155  goto_programt &goto_program,
157  const source_locationt &source_location,
158  const irep_idt &id_lhs,
159  const exprt &value)
160 {
161  const namespacet ns(symbol_table);
162  std::string identifier=id2string(id_lhs);
163 
164  const size_t pos=identifier.find("[]");
165 
166  if(pos!=std::string::npos)
167  {
168  /* we don't distinguish the members of an array for the moment */
169  identifier.erase(pos);
170  }
171 
172  try
173  {
174  const exprt symbol=ns.lookup(identifier).symbol_expr();
175 
176  t=goto_program.insert_before(t);
177  t->type=ASSIGN;
178  t->code=code_assignt(symbol, value);
179  t->code.add_source_location()=source_location;
180  t->source_location=source_location;
181 
182  // instrumentations.insert((const irep_idt) (t->code.id()));
183 
184  t++;
185  }
186  catch(const std::string &s)
187  {
188  message.warning() << s << messaget::eom;
189  }
190 }
191 
194  goto_programt &goto_program,
195  goto_programt::targett &target,
196  const source_locationt &source_location,
197  const irep_idt &read_object,
198  const irep_idt &write_object)
199 {
200 /* option 1: */
201 /* trick using an additional variable whose value is to be defined later */
202 
203 #if 0
204  assignment(goto_program, target, source_location, vars.read_delayed,
205  true_exprt());
206  assignment(goto_program, target, source_location, vars.read_delayed_var,
207  read_object);
208 
209  const irep_idt &new_var=add_fresh_var(write_object, unique(), vars.type);
210 
211  assignment(goto_program, target, source_location, vars.read_new_var, new_var);
212 
213  // initial write, but from the new variable now
214  assignment(goto_program, target, source_location, write_object, new_var);
215 #endif
216 
217 /* option 2 */
218 /* pointer */
219 
220  const std::string identifier=id2string(write_object);
221 
222  message.debug()<<"delay_read: " << messaget::eom;
223  const varst &vars=(*this)(write_object);
224 
225  const symbol_exprt read_object_expr=symbol_exprt(read_object, vars.type);
226 
227  assignment(
228  goto_program,
229  target,
230  source_location,
231  vars.read_delayed,
232  true_exprt());
233  assignment(
234  goto_program,
235  target,
236  source_location,
237  vars.read_delayed_var,
238  address_of_exprt(read_object_expr));
239 }
240 
243  goto_programt &goto_program,
244  goto_programt::targett &target,
245  const source_locationt &source_location,
246  const irep_idt &write_object)
247 {
248 #if 0
249  // option 1
250  const varst &vars=(*this)(write_object);
251 
252  const symbol_exprt fresh_var_expr=symbol_exprt(vars.read_new_var, vars.type);
253  const symbol_exprt var_expr=symbol_exprt(vars.read_delayed_var, vars.type);
254  const exprt eq_expr=equal_exprt(var_expr, fresh_var_expr);
255 
256  const symbol_exprt cond_delayed_expr=symbol_exprt(vars.read_delayed,
257  bool_typet());
258  const exprt if_expr=if_exprt(cond_delayed_expr, eq_expr, true_exprt());
259 
260  target=goto_program.insert_before(target);
261  target->type=ASSUME;
262  target->guard=if_expr;
263  target->guard.source_location()=source_location;
264  target->source_location=source_location;
265 
266  target++;
267 
268  assignment(goto_program, target, source_location, vars.read_delayed,
269  false_exprt());
270 #else
271  // option 2: do nothing
272  // unused parameters
273  (void)goto_program;
274  (void)target;
275  (void)target;
276  (void)source_location;
277  (void)write_object;
278 #endif
279 }
280 
283  goto_programt &goto_program,
284  goto_programt::targett &target,
285  const source_locationt &source_location,
286  const irep_idt &object,
287  goto_programt::instructiont &original_instruction,
288  const unsigned current_thread)
289 {
290  const std::string identifier=id2string(object);
291 
292  message.debug() << "write: " << object << messaget::eom;
293  const varst &vars=(*this)(object);
294 
295  // We rotate the write buffers for anything that is written.
296  assignment(goto_program, target, source_location, vars.w_buff1, vars.w_buff0);
297  assignment(
298  goto_program, target, source_location, vars.w_buff0,
299  original_instruction.code.op1());
300 
301  // We update the used flags
302  assignment(
303  goto_program,
304  target,
305  source_location,
306  vars.w_buff1_used,
307  vars.w_buff0_used);
308  assignment(
309  goto_program,
310  target,
311  source_location,
312  vars.w_buff0_used,
313  true_exprt());
314 
315  // We should not exceed the buffer size -- inserts assertion for dynamically
316  // checking this
317  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
318  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
319  const exprt cond_expr=
320  not_exprt(and_exprt(buff1_used_expr, buff0_used_expr));
321 
322  target = goto_program.insert_before(
323  target, goto_programt::make_assertion(cond_expr, source_location));
324  target++;
325 
326  // We update writers ownership of the values in the buffer
327  for(unsigned cnt=0; cnt<nb_threads; cnt++)
328  assignment(goto_program, target, source_location, vars.r_buff1_thds[cnt],
329  vars.r_buff0_thds[cnt]);
330 
331  // We update the lucky new author of this value in the buffer
332  assignment(
333  goto_program,
334  target,
335  source_location,
336  vars.r_buff0_thds[current_thread],
337  true_exprt());
338 }
339 
342  goto_programt &goto_program,
343  goto_programt::targett &target,
344  const source_locationt &source_location,
345  const irep_idt &object,
346  const unsigned current_thread)
347 {
348  const std::string identifier=id2string(object);
349 
350  // mostly for instrumenting the fences. A thread only flushes the values it
351  // wrote in the buffer.
352  message.debug() << "det flush: " << messaget::eom;
353  const varst &vars=(*this)(object);
354 
355  // current value in the memory
356  const exprt lhs=symbol_exprt(object, vars.type);
357 
358  // if buff0 from this thread, uses it to update the memory (the most recent
359  // value, or last write by -ws-> ); if not, if buff1 from this thread, uses
360  // it; if not, keeps the current memory value
361  const exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
362  const exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
363 
364  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
365  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
366 
367  const exprt buff0_mine_expr=symbol_exprt(vars.r_buff0_thds[current_thread],
368  bool_typet());
369  const exprt buff1_mine_expr=symbol_exprt(vars.r_buff1_thds[current_thread],
370  bool_typet());
371 
372  const exprt buff0_used_and_mine_expr=and_exprt(buff0_used_expr,
373  buff0_mine_expr);
374  const exprt buff1_used_and_mine_expr=and_exprt(buff1_used_expr,
375  buff1_mine_expr);
376 
377  const exprt new_value_expr=
378  if_exprt(
379  buff0_used_and_mine_expr,
380  buff0_expr,
381  if_exprt(
382  buff1_used_and_mine_expr,
383  buff1_expr,
384  lhs));
385 
386  // We update (or not) the value in the memory
387  assignment(goto_program, target, source_location, object, new_value_expr);
388 
389  // We update the flags of the buffer
390  // if buff0 used and mine, then it is no more used, as we flushed the last
391  // write and -ws-> imposes not to have other writes in the buffer
392  assignment(
393  goto_program,
394  target,
395  source_location,
396  vars.w_buff0_used,
397  if_exprt(
398  buff0_used_and_mine_expr,
399  false_exprt(),
400  buff0_used_expr));
401 
402  // buff1 used and mine & not buff0 used and mine, then it no more used
403  // if buff0 is used and mine, then, by ws, buff1 is no more used
404  // otherwise, remains as it is
405  const exprt buff0_or_buff1_used_and_mine_expr=
406  or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
407 
408  assignment(
409  goto_program,
410  target,
411  source_location,
412  vars.w_buff1_used,
413  if_exprt(
414  buff0_or_buff1_used_and_mine_expr,
415  false_exprt(),
416  buff1_used_expr));
417 
418  // We update the ownerships
419  // if buff0 mine and used, flushed, so belongs to nobody
420  const exprt buff0_thd_expr=
421  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
422 
423  assignment(
424  goto_program,
425  target,
426  source_location,
427  vars.r_buff0_thds[current_thread],
428  if_exprt(buff0_used_and_mine_expr, false_exprt(), buff0_thd_expr));
429 
430  // if buff1 used and mine, or if buff0 used and mine, then buff1 flushed and
431  // doesn't belong to anybody
432  const exprt buff1_thd_expr=
433  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
434 
435  assignment(
436  goto_program,
437  target,
438  source_location,
439  vars.r_buff1_thds[current_thread],
440  if_exprt(
441  buff0_or_buff1_used_and_mine_expr,
442  false_exprt(),
443  buff1_thd_expr));
444 }
445 
448  const irep_idt &function_id,
449  goto_programt &goto_program,
450  goto_programt::targett &target,
451  const source_locationt &source_location,
452  const irep_idt &object,
453  const unsigned current_thread,
454  const bool tso_pso_rmo) // true: tso/pso/rmo; false: power
455 {
456  const std::string identifier=id2string(object);
457 
458  message.debug() << "nondet flush: " << object << messaget::eom;
459 
460  try
461  {
462  const varst &vars=(*this)(object);
463 
464  // Non deterministic choice
465  irep_idt choice0 = choice(function_id, "0");
466  irep_idt choice2 = choice(function_id, "2"); // delays the write flush
467 
468  const symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
469  const symbol_exprt delay_expr=symbol_exprt(choice2, bool_typet());
470  const exprt nondet_bool_expr =
471  side_effect_expr_nondett(bool_typet(), source_location);
472 
473  // throw Boolean dice
474  assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
475  assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
476 
477  // Buffers and memory
478  const symbol_exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
479  const symbol_exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
480  const exprt lhs=symbol_exprt(object, vars.type);
481 
482  // Buffer uses
483  const symbol_exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used,
484  bool_typet());
485  const symbol_exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used,
486  bool_typet());
487 
488  // Buffer ownerships
489  const symbol_exprt buff0_thd_expr=
490  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
491  const symbol_exprt buff1_thd_expr=
492  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
493 
494 
495  // Will the write be directly flushed, or is it just a read?
496  assignment(
497  goto_program, target, source_location, vars.flush_delayed, delay_expr);
498  assignment(goto_program, target, source_location, vars.mem_tmp, lhs);
499 
500  // for POWER, only instrumented reads can read from the buffers of other
501  // threads
502  bool instrumented=false;
503 
504  if(!tso_pso_rmo)
505  {
506  if(cycles.find(object)!=cycles.end())
507  {
508  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
509  std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(object);
510  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
511  if(ran_it->second==source_location)
512  {
513  instrumented=true;
514  break;
515  }
516  }
517  }
518 
519  // TSO/PSO/RMO
520  if(tso_pso_rmo || !instrumented)
521  {
522  // 7 cases
523 
524  // (1) (3) (4)
525  // if buff0 unused
526  // or buff0 not mine and buff1 unused
527  // or buff0 not mine and buff1 not mine
528  // -> read from memory (and does not modify the buffer in any aspect)
529  const exprt cond_134_expr=
530  or_exprt(
531  not_exprt(buff0_used_expr),
532  or_exprt(
533  and_exprt(
534  not_exprt(buff0_thd_expr),
535  not_exprt(buff1_used_expr)),
536  and_exprt(
537  not_exprt(buff0_thd_expr),
538  not_exprt(buff1_thd_expr))));
539  const exprt val_134_expr=lhs;
540  const exprt buff0_used_134_expr=buff0_used_expr;
541  const exprt buff1_used_134_expr=buff1_used_expr;
542  const exprt buff0_134_expr=buff0_expr;
543  const exprt buff1_134_expr=buff1_expr;
544  const exprt buff0_thd_134_expr=buff0_thd_expr;
545  const exprt buff1_thd_134_expr=buff1_thd_expr;
546 
547  // (2) (6) (7)
548  // if buff0 used and mine
549  // -> read from buff0
550  const exprt cond_267_expr=and_exprt(buff0_used_expr, buff0_thd_expr);
551  const exprt val_267_expr=buff0_expr;
552  const exprt buff0_used_267_expr=false_exprt();
553  const exprt buff1_used_267_expr=false_exprt();
554  const exprt buff0_267_expr=buff0_expr;
555  const exprt buff1_267_expr=buff1_expr;
556  const exprt buff0_thd_267_expr=false_exprt();
557  const exprt buff1_thd_267_expr=false_exprt();
558 
559  // (5)
560  // buff0 and buff1 are used, buff0 is not mine, buff1 is mine
561  // -> read from buff1
562  const exprt cond_5_expr=
563  and_exprt(
564  buff0_used_expr,
565  and_exprt(
566  buff1_used_expr,
567  and_exprt(not_exprt(buff0_thd_expr), buff1_thd_expr)));
568  const exprt val_5_expr=buff1_expr;
569  const exprt buff0_used_5_expr=buff0_used_expr;
570  const exprt buff1_used_5_expr=false_exprt();
571  const exprt buff0_5_expr=buff0_expr;
572  const exprt buff1_5_expr=buff1_expr;
573  const exprt buff0_thd_5_expr=buff0_thd_expr;
574  const exprt buff1_thd_5_expr=false_exprt();
575 
576  // Updates
577  // memory
578  assignment(
579  goto_program,
580  target,
581  source_location,
582  object,
583  if_exprt(
584  cond_134_expr,
585  val_134_expr,
586  if_exprt(
587  cond_267_expr,
588  val_267_expr,
589  val_5_expr)));
590  // buff0
591  assignment(
592  goto_program,
593  target,
594  source_location,
595  vars.w_buff0,
596  if_exprt(
597  delay_expr,
598  buff0_expr,
599  if_exprt(
600  cond_134_expr,
601  buff0_134_expr,
602  if_exprt(
603  cond_267_expr,
604  buff0_267_expr,
605  buff0_5_expr))));
606  // buff1
607  assignment(
608  goto_program,
609  target,
610  source_location,
611  vars.w_buff1,
612  if_exprt(
613  delay_expr,
614  buff1_expr,
615  if_exprt(
616  cond_134_expr,
617  buff1_134_expr,
618  if_exprt(
619  cond_267_expr,
620  buff1_267_expr,
621  buff1_5_expr))));
622  // buff0_used
623  assignment(
624  goto_program,
625  target,
626  source_location,
627  vars.w_buff0_used,
628  if_exprt(
629  delay_expr,
630  buff0_used_expr,
631  if_exprt(
632  cond_134_expr,
633  buff0_used_134_expr,
634  if_exprt(
635  cond_267_expr,
636  buff0_used_267_expr,
637  buff0_used_5_expr))));
638  // buff1_used
639  assignment(
640  goto_program,
641  target,
642  source_location,
643  vars.w_buff1_used,
644  if_exprt(
645  delay_expr,
646  buff1_used_expr,
647  if_exprt(
648  cond_134_expr,
649  buff1_used_134_expr,
650  if_exprt(
651  cond_267_expr,
652  buff1_used_267_expr,
653  buff1_used_5_expr))));
654  // buff0_thd
655  assignment(
656  goto_program,
657  target,
658  source_location,
659  vars.r_buff0_thds[current_thread],
660  if_exprt(
661  delay_expr,
662  buff0_thd_expr,
663  if_exprt(
664  cond_134_expr,
665  buff0_thd_134_expr,
666  if_exprt(
667  cond_267_expr,
668  buff0_thd_267_expr,
669  buff0_thd_5_expr))));
670  // buff1_thd
671  assignment(
672  goto_program,
673  target,
674  source_location,
675  vars.r_buff1_thds[current_thread], if_exprt(
676  delay_expr,
677  buff1_thd_expr,
678  if_exprt(
679  cond_134_expr,
680  buff1_thd_134_expr,
681  if_exprt(
682  cond_267_expr,
683  buff1_thd_267_expr,
684  buff1_thd_5_expr))));
685  }
686  // POWER
687  else
688  {
689  // a thread can read the other threads' buffers
690 
691  // One extra non-deterministic choice needed
692  irep_idt choice1 = choice(function_id, "1");
693  const symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
694 
695  // throw Boolean dice
696  assignment(
697  goto_program, target, source_location, choice1, nondet_bool_expr);
698 
699  // 7 cases
700 
701  // (1)
702  // if buff0 unused
703  // -> read from memory (and does not modify the buffer in any aspect)
704  const exprt cond_1_expr=not_exprt(buff0_used_expr);
705  const exprt val_1_expr=lhs;
706  const exprt buff0_used_1_expr=buff0_used_expr;
707  const exprt buff1_used_1_expr=buff1_used_expr;
708  const exprt buff0_1_expr=buff0_expr;
709  const exprt buff1_1_expr=buff1_expr;
710  const exprt buff0_thd_1_expr=buff0_thd_expr;
711  const exprt buff1_thd_1_expr=buff1_thd_expr;
712 
713  // (2) (6) (7)
714  // if buff0 used and mine
715  // -> read from buff0
716  const exprt cond_267_expr=
717  and_exprt(buff0_used_expr, buff0_thd_expr);
718  const exprt val_267_expr=buff0_expr;
719  const exprt buff0_used_267_expr=false_exprt();
720  const exprt buff1_used_267_expr=false_exprt();
721  const exprt buff0_267_expr=buff0_expr;
722  const exprt buff1_267_expr=buff1_expr;
723  const exprt buff0_thd_267_expr=false_exprt();
724  const exprt buff1_thd_267_expr=false_exprt();
725 
726  // (3)
727  // if buff0 used and not mine, and buff1 not used
728  // -> read from buff0 or memory
729  const exprt cond_3_expr=
730  and_exprt(
731  buff0_used_expr,
732  and_exprt(
733  not_exprt(buff0_thd_expr),
734  not_exprt(buff1_used_expr)));
735  const exprt val_3_expr=if_exprt(choice0_expr, buff0_expr, lhs);
736  const exprt buff0_used_3_expr=choice0_expr;
737  const exprt buff1_used_3_expr=false_exprt();
738  const exprt buff0_3_expr=buff0_expr;
739  const exprt buff1_3_expr=buff1_expr;
740  const exprt buff0_thd_3_expr=false_exprt();
741  const exprt buff1_thd_3_expr=false_exprt();
742 
743  // (4)
744  // buff0 and buff1 are both used, and both not mine
745  // -> read from memory or buff0 or buff1
746  const exprt cond_4_expr=
747  and_exprt(
748  and_exprt(buff0_used_expr, not_exprt(buff1_thd_expr)),
749  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
750  const exprt val_4_expr=
751  if_exprt(
752  choice0_expr,
753  lhs,
754  if_exprt(
755  choice1_expr,
756  buff0_expr,
757  buff1_expr));
758  const exprt buff0_used_4_expr=
759  or_exprt(choice0_expr, not_exprt(choice1_expr));
760  const exprt buff1_used_4_expr=choice0_expr;
761  const exprt buff0_4_expr=buff0_expr;
762  const exprt buff1_4_expr=buff1_expr;
763  const exprt buff0_thd_4_expr=buff0_thd_expr;
764  const exprt buff1_thd_4_expr=
765  if_exprt(choice0_expr, buff1_thd_expr, false_exprt());
766 
767  // (5)
768  // buff0 and buff1 are both used, and buff0 not mine, and buff1 mine
769  // -> read buff1 or buff0
770  const exprt cond_5_expr=
771  and_exprt(
772  and_exprt(buff0_used_expr, buff1_thd_expr),
773  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
774  const exprt val_5_expr=
775  if_exprt(
776  choice0_expr,
777  buff1_expr,
778  buff0_expr);
779  const exprt buff0_used_5_expr=choice0_expr;
780  const exprt buff1_used_5_expr=false_exprt();
781  const exprt buff0_5_expr=buff0_expr;
782  const exprt buff1_5_expr=buff1_expr;
783  const exprt buff0_thd_5_expr=false_exprt();
784  const exprt buff1_thd_5_expr=false_exprt();
785 
786  // Updates
787  // memory
788  assignment(
789  goto_program,
790  target,
791  source_location,
792  object,
793  if_exprt(
794  cond_1_expr,
795  val_1_expr,
796  if_exprt(
797  cond_267_expr,
798  val_267_expr,
799  if_exprt(
800  cond_4_expr,
801  val_4_expr,
802  if_exprt(
803  cond_5_expr,
804  val_5_expr,
805  val_3_expr)))));
806  // buff0
807  assignment(
808  goto_program,
809  target,
810  source_location,
811  vars.w_buff0,
812  if_exprt(
813  delay_expr,
814  buff0_expr,
815  if_exprt(
816  cond_1_expr,
817  buff0_1_expr,
818  if_exprt(
819  cond_267_expr,
820  buff0_267_expr,
821  if_exprt(
822  cond_4_expr,
823  buff0_4_expr,
824  if_exprt(
825  cond_5_expr,
826  buff0_5_expr,
827  buff0_3_expr))))));
828  // buff1
829  assignment(
830  goto_program,
831  target,
832  source_location,
833  vars.w_buff1,
834  if_exprt(
835  delay_expr,
836  buff1_expr,
837  if_exprt(
838  cond_1_expr,
839  buff1_1_expr,
840  if_exprt(
841  cond_267_expr,
842  buff1_267_expr,
843  if_exprt(
844  cond_4_expr,
845  buff1_4_expr,
846  if_exprt(
847  cond_5_expr,
848  buff1_5_expr,
849  buff1_3_expr))))));
850  // buff0_used
851  assignment(
852  goto_program,
853  target,
854  source_location,
855  vars.w_buff0_used,
856  if_exprt(
857  delay_expr,
858  buff0_used_expr,
859  if_exprt(
860  cond_1_expr,
861  buff0_used_1_expr,
862  if_exprt(
863  cond_267_expr,
864  buff0_used_267_expr,
865  if_exprt(
866  cond_4_expr,
867  buff0_used_4_expr,
868  if_exprt(
869  cond_5_expr,
870  buff0_used_5_expr,
871  buff0_used_3_expr))))));
872  // buff1_used
873  assignment(
874  goto_program,
875  target,
876  source_location,
877  vars.w_buff1_used,
878  if_exprt(
879  delay_expr,
880  buff1_used_expr,
881  if_exprt(
882  cond_1_expr,
883  buff1_used_1_expr,
884  if_exprt(
885  cond_267_expr,
886  buff1_used_267_expr,
887  if_exprt(
888  cond_4_expr,
889  buff1_used_4_expr,
890  if_exprt(
891  cond_5_expr,
892  buff1_used_5_expr,
893  buff1_used_3_expr))))));
894  // buff0_thd
895  assignment(
896  goto_program,
897  target,
898  source_location,
899  vars.r_buff0_thds[current_thread],
900  if_exprt(
901  delay_expr,
902  buff0_thd_expr,
903  if_exprt(
904  cond_1_expr,
905  buff0_thd_1_expr,
906  if_exprt(
907  cond_267_expr,
908  buff0_thd_267_expr,
909  if_exprt(
910  cond_4_expr,
911  buff0_thd_4_expr,
912  if_exprt(
913  cond_5_expr,
914  buff0_thd_5_expr,
915  buff0_thd_3_expr))))));
916  // buff1_thd
917  assignment(
918  goto_program,
919  target,
920  source_location,
921  vars.r_buff1_thds[current_thread],
922  if_exprt(
923  delay_expr,
924  buff1_thd_expr,
925  if_exprt(
926  cond_1_expr,
927  buff1_thd_1_expr,
928  if_exprt(
929  cond_267_expr,
930  buff1_thd_267_expr,
931  if_exprt(
932  cond_4_expr,
933  buff1_thd_4_expr,
934  if_exprt(
935  cond_5_expr,
936  buff1_thd_5_expr,
937  buff1_thd_3_expr))))));
938  }
939  }
940  catch(const std::string &s)
941  {
942  message.warning() << s << messaget::eom;
943  }
944 }
945 
947  const namespacet &ns,
948  const symbol_exprt &symbol_expr,
949  bool is_write
950  // are we asking for the variable (false), or for the variable and
951  // the source_location in the code (true)
952 )
953 {
954  const irep_idt &identifier=symbol_expr.get_identifier();
955 
956  if(identifier==CPROVER_PREFIX "alloc" ||
957  identifier==CPROVER_PREFIX "alloc_size" ||
958  identifier=="stdin" ||
959  identifier=="stdout" ||
960  identifier=="stderr" ||
961  identifier=="sys_nerr" ||
962  has_prefix(id2string(identifier), "__unbuffered_") ||
963  has_prefix(id2string(identifier), "__CPROVER"))
964  return false; // not buffered
965 
966  const symbolt &symbol=ns.lookup(identifier);
967 
968  if(!symbol.is_static_lifetime)
969  return false; // these are local
970 
971  if(symbol.is_thread_local)
972  return false; // these are local
973 
974  if(instrumentations.find(identifier)!=instrumentations.end())
975  return false; // these are instrumentations
976 
977  return is_buffered_in_general(symbol_expr, is_write);
978 }
979 
981  const symbol_exprt &symbol_expr,
982  bool is_write
983  // are we asking for the variable (false), or for the variable and the
984  // source_location in the code? (true)
985 )
986 {
987  if(cav11)
988  return true;
989 
990  const irep_idt &identifier=symbol_expr.get_identifier();
991  const source_locationt &source_location=symbol_expr.source_location();
992 
993  if(cycles.find(identifier)==cycles.end())
994  return false; // not to instrument
995 
996  if(!is_write)
997  {
998  // to be uncommented only when we are sure all the cycles
999  // are detected (before detection of the pairs -- no hack)
1000  // WARNING: on the FULL cycle, not reduced by PO
1001  /*typedef std::multimap<irep_idt,source_locationt>::iterator m_itt;
1002  std::pair<m_itt,m_itt> ran=cycles_r_loc.equal_range(identifier);
1003  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1004  if(ran_it->second==source_location)*/
1005  return true;
1006  }
1007  else
1008  {
1009  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1010  std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(identifier);
1011  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1012  if(ran_it->second==source_location)
1013  return true; // not to instrument
1014  }
1015 
1016  return false;
1017 }
1018 
1023  value_setst &value_sets,
1024  goto_functionst &goto_functions)
1025 {
1027 
1028  Forall_goto_functions(f_it, goto_functions)
1029  {
1030 #ifdef LOCAL_MAY
1031  local_may_aliast local_may(f_it->second);
1032 #endif
1033 
1034  Forall_goto_program_instructions(i_it, f_it->second.body)
1035  {
1036  rw_set_loct rw_set(
1037  ns,
1038  value_sets,
1039  f_it->first,
1040  i_it
1041 #ifdef LOCAL_MAY
1042  ,
1043  local_may
1044 #endif
1045  ); // NOLINT(whitespace/parens)
1046  forall_rw_set_w_entries(w_it, rw_set)
1047  forall_rw_set_r_entries(r_it, rw_set)
1048  {
1049  message.debug() <<"debug: "<<id2string(w_it->second.object)
1050  <<" reads from "<<id2string(r_it->second.object)
1051  <<messaget::eom;
1052  if(is_buffered_in_general(r_it->second.symbol_expr, true))
1053  // shouldn't it be true? false => overapprox
1054  affected_by_delay_set.insert(w_it->second.object);
1055  }
1056  }
1057  }
1058 }
1059 
1062  value_setst &value_sets,
1063  const irep_idt &function_id,
1064  memory_modelt model)
1065 {
1067  << "visit function " << function_id << messaget::eom;
1068  if(function_id == INITIALIZE_FUNCTION)
1069  return;
1070 
1072  goto_programt &goto_program = goto_functions.function_map[function_id].body;
1073 
1074 #ifdef LOCAL_MAY
1075  local_may_aliast local_may(goto_functions.function_map[function_id]);
1076 #endif
1077 
1078  Forall_goto_program_instructions(i_it, goto_program)
1079  {
1080  goto_programt::instructiont &instruction=*i_it;
1081 
1082  shared_buffers.message.debug() << "instruction "<<instruction.type
1083  << messaget::eom;
1084 
1085  /* thread marking */
1086  if(instruction.is_start_thread())
1087  {
1091  }
1092  else if(instruction.is_end_thread())
1094 
1095  if(instruction.is_assign())
1096  {
1097  try
1098  {
1099  rw_set_loct rw_set(
1100  ns,
1101  value_sets,
1102  function_id,
1103  i_it
1104 #ifdef LOCAL_MAY
1105  ,
1106  local_may
1107 #endif
1108  ); // NOLINT(whitespace/parens)
1109 
1110  if(rw_set.empty())
1111  continue;
1112 
1113  // add all the written values (which are not instrumentations)
1114  // in a set
1115  forall_rw_set_w_entries(w_it, rw_set)
1116  if(shared_buffers.is_buffered(ns, w_it->second.symbol_expr, false))
1117  past_writes.insert(w_it->second.object);
1118 
1119  goto_programt::instructiont original_instruction;
1120  original_instruction.swap(instruction);
1121  const source_locationt &source_location=
1122  original_instruction.source_location;
1123 
1124  // ATOMIC_BEGIN: we make the whole thing atomic
1125  instruction = goto_programt::make_atomic_begin(source_location);
1126  i_it++;
1127 
1128  // we first perform (non-deterministically) up to 2 writes for
1129  // stuff that is potentially read
1130  forall_rw_set_r_entries(e_it, rw_set)
1131  {
1132  // flush read -- do nothing in this implementation
1134  goto_program, i_it, source_location, e_it->second.object);
1135 
1136  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, false))
1138  function_id,
1139  goto_program,
1140  i_it,
1141  source_location,
1142  e_it->second.object,
1144  (model == TSO || model == PSO || model == RMO));
1145  }
1146 
1147  // Now perform the write(s).
1148  forall_rw_set_w_entries(e_it, rw_set)
1149  {
1150  // if one of the previous read was to buffer, then delays the read
1151  if(model==RMO || model==Power)
1152  {
1153  forall_rw_set_r_entries(r_it, rw_set)
1154  if(shared_buffers.is_buffered(ns, r_it->second.symbol_expr, true))
1155  {
1157  goto_program, i_it, source_location, r_it->second.object,
1158  e_it->second.object);
1159  }
1160  }
1161 
1162  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, true))
1163  {
1165  goto_program, i_it, source_location,
1166  e_it->second.object, original_instruction,
1167  current_thread);
1168  }
1169  else
1170  {
1171  // unbuffered
1172  if(model==RMO || model==Power)
1173  {
1174  forall_rw_set_r_entries(r_it, rw_set)
1176  r_it->second.object)!=
1178  {
1179  shared_buffers.message.debug() << "second: "
1180  << r_it->second.object << messaget::eom;
1181  const varst &vars=(shared_buffers)(r_it->second.object);
1182 
1183  shared_buffers.message.debug() << "writer "
1184  <<e_it->second.object
1185  <<" reads "<<r_it->second.object<< messaget::eom;
1186 
1187  // TO FIX: how to deal with rhs including calls?
1188  // if a read is delayed, use its alias instead of itself
1189  // -- or not
1190  symbol_exprt to_replace_expr=symbol_exprt(
1191  r_it->second.object, vars.type);
1192  symbol_exprt new_read_expr=symbol_exprt(
1193  vars.read_delayed_var,
1194  pointer_type(vars.type));
1195  symbol_exprt read_delayed_expr=symbol_exprt(
1196  vars.read_delayed, bool_typet());
1197 
1198  // One extra non-deterministic choice needed
1199  irep_idt choice1 = shared_buffers.choice(function_id, "1");
1200  const symbol_exprt choice1_expr=symbol_exprt(choice1,
1201  bool_typet());
1202  const exprt nondet_bool_expr =
1203  side_effect_expr_nondett(bool_typet(), source_location);
1204 
1205  // throw Boolean dice
1207  goto_program,
1208  i_it,
1209  source_location,
1210  choice1,
1211  nondet_bool_expr);
1212 
1213  const if_exprt rhs(
1214  read_delayed_expr,
1215  if_exprt(
1216  choice1_expr,
1217  dereference_exprt{new_read_expr},
1218  to_replace_expr),
1219  to_replace_expr); // original_instruction.code.op1());
1220 
1222  goto_program, i_it, source_location,
1223  r_it->second.object, rhs);
1224  }
1225  }
1226 
1227  // normal assignment
1229  goto_program, i_it, source_location,
1230  e_it->second.object, original_instruction.code.op1());
1231  }
1232  }
1233 
1234  // if last writes was flushed to make the lhs reads the buffer but
1235  // without affecting the memory, restore the previous memory value
1236  // (buffer flush delay)
1237  forall_rw_set_r_entries(e_it, rw_set)
1238  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, false))
1239  {
1240  shared_buffers.message.debug() << "flush restore: "
1241  << e_it->second.object << messaget::eom;
1242  const varst vars= (shared_buffers)(e_it->second.object);
1243  const exprt delayed_expr=symbol_exprt(vars.flush_delayed,
1244  bool_typet());
1245  const symbol_exprt mem_value_expr=symbol_exprt(vars.mem_tmp,
1246  vars.type);
1247  const exprt cond_expr=if_exprt(delayed_expr, mem_value_expr,
1248  e_it->second.symbol_expr);
1249 
1251  goto_program, i_it, source_location,
1252  e_it->second.object, cond_expr);
1254  goto_program, i_it, source_location,
1255  vars.flush_delayed, false_exprt());
1256  }
1257 
1258  // ATOMIC_END
1259  i_it = goto_program.insert_before(
1260  i_it, goto_programt::make_atomic_end(source_location));
1261  i_it++;
1262 
1263  i_it--; // the for loop already counts us up
1264  }
1265  catch (...)
1266  {
1267  shared_buffers.message.warning() << "Identifier not found"
1268  << messaget::eom;
1269  }
1270  }
1271  else if(is_fence(instruction, ns) ||
1272  (instruction.is_other() &&
1273  instruction.code.get_statement()==ID_fence &&
1274  (instruction.code.get_bool("WRfence") ||
1275  instruction.code.get_bool("WWfence") ||
1276  instruction.code.get_bool("RWfence") ||
1277  instruction.code.get_bool("RRfence"))))
1278  {
1279  goto_programt::instructiont original_instruction;
1280  original_instruction.swap(instruction);
1281  const source_locationt &source_location=
1282  original_instruction.source_location;
1283 
1284  // ATOMIC_BEGIN
1285  instruction = goto_programt::make_atomic_begin(source_location);
1286  i_it++;
1287 
1288  // does it for all the previous statements
1289  for(std::set<irep_idt>::iterator s_it=past_writes.begin();
1290  s_it!=past_writes.end(); s_it++)
1291  {
1293  goto_program, i_it, source_location, *s_it,
1294  current_thread);
1295  }
1296 
1297  // ATOMIC_END
1298  i_it = goto_program.insert_before(
1299  i_it, goto_programt::make_atomic_end(source_location));
1300  i_it++;
1301 
1302  i_it--; // the for loop already counts us up
1303  }
1304  else if(is_lwfence(instruction, ns))
1305  {
1306  // po -- remove the lwfence
1307  *i_it = goto_programt::make_skip(i_it->source_location);
1308  }
1309  else if(instruction.is_function_call())
1310  {
1311  const exprt &fun=to_code_function_call(instruction.code).function();
1312  weak_memory(value_sets, to_symbol_expr(fun).get_identifier(), model);
1313  }
1314  }
1315 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
shared_bufferst::write
void write(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)
instruments write
Definition: shared_buffers.cpp:282
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
shared_bufferst::cfg_visitort::symbol_table
symbol_tablet & symbol_table
Definition: shared_buffers.h:195
TSO
@ TSO
Definition: wmm.h:20
is_lwfence
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36
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
shared_bufferst::det_flush
void det_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)
flush buffers (instruments fence)
Definition: shared_buffers.cpp:341
shared_bufferst::varst::w_buff1_used
irep_idt w_buff1_used
Definition: shared_buffers.h:57
shared_bufferst::is_buffered_in_general
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
Definition: shared_buffers.cpp:980
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:466
RMO
@ RMO
Definition: wmm.h:22
pos
literalt pos(literalt a)
Definition: literal.h:194
irept::make_nil
void make_nil()
Definition: irep.h:475
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:510
typet
The type of an expression, extends irept.
Definition: type.h:29
shared_bufferst::varst::read_delayed
irep_idt read_delayed
Definition: shared_buffers.h:70
fresh_symbol.h
Fresh auxiliary symbol creation.
shared_bufferst::varst::r_buff0_thds
std::vector< irep_idt > r_buff0_thds
Definition: shared_buffers.h:67
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
shared_bufferst::cfg_visitort::goto_functions
goto_functionst & goto_functions
Definition: shared_buffers.h:196
PSO
@ PSO
Definition: wmm.h:21
and_exprt
Boolean AND.
Definition: std_expr.h:2137
shared_bufferst::symbol_table
class symbol_tablet & symbol_table
Definition: shared_buffers.h:224
exprt
Base class for all expressions.
Definition: expr.h:53
shared_bufferst::cfg_visitort::max_thread
unsigned max_thread
Definition: shared_buffers.h:201
Power
@ Power
Definition: wmm.h:23
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool_typet
The Boolean type.
Definition: std_types.h:37
shared_bufferst::cycles_loc
std::multimap< irep_idt, source_locationt > cycles_loc
Definition: shared_buffers.h:83
shared_bufferst::add
irep_idt add(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
Definition: shared_buffers.cpp:85
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
shared_bufferst::add_initialization_code
void add_initialization_code(goto_functionst &goto_functions)
Definition: shared_buffers.cpp:139
shared_bufferst::cfg_visitort::current_thread
unsigned current_thread
Definition: shared_buffers.h:199
shared_bufferst::add_fresh_var
irep_idt add_fresh_var(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
Definition: shared_buffers.h:264
goto_programt::instructiont::is_end_thread
bool is_end_thread() const
Definition: goto_program.h:474
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:82
shared_bufferst::assignment
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)
add an assignment in the goto-program
Definition: shared_buffers.cpp:154
equal_exprt
Equality.
Definition: std_expr.h:1190
local_may_aliast
Definition: local_may_alias.h:26
shared_bufferst::varst::flush_delayed
irep_idt flush_delayed
Definition: shared_buffers.h:64
shared_bufferst::choice
irep_idt choice(const irep_idt &function_id, const std::string &suffix)
Definition: shared_buffers.h:160
shared_bufferst::var_map
var_mapt var_map
Definition: shared_buffers.h:77
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
is_fence
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
shared_bufferst::is_buffered
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
Definition: shared_buffers.cpp:946
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
shared_bufferst::message
messaget & message
Definition: shared_buffers.h:245
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
or_exprt
Boolean OR.
Definition: std_expr.h:2245
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
shared_bufferst::varst::w_buff1
irep_idt w_buff1
Definition: shared_buffers.h:54
shared_bufferst::cav11
bool cav11
Definition: shared_buffers.h:242
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
rw_set_baset::empty
bool empty() const
Definition: rw_set.h:75
shared_bufferst::varst::w_buff0_used
irep_idt w_buff0_used
Definition: shared_buffers.h:57
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
forall_rw_set_r_entries
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:110
shared_bufferst::affected_by_delay_set
std::set< irep_idt > affected_by_delay_set
Definition: shared_buffers.h:234
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
shared_bufferst::cfg_visitort::weak_memory
void weak_memory(value_setst &value_sets, const irep_idt &function_id, memory_modelt model)
instruments the program for the pairs detected through the CFG
Definition: shared_buffers.cpp:1061
shared_bufferst::unique
std::string unique()
returns a unique id (for fresh variables)
Definition: shared_buffers.cpp:21
shared_buffers.h
shared_bufferst::cycles
std::set< irep_idt > cycles
Definition: shared_buffers.h:81
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:935
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
shared_bufferst::cfg_visitort::past_writes
std::set< irep_idt > past_writes
Definition: shared_buffers.h:204
memory_modelt
memory_modelt
Definition: wmm.h:18
main
int main(int argc, char *argv[])
Definition: file_converter.cpp:41
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
shared_bufferst::delay_read
void delay_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)
delays a read (POWER)
Definition: shared_buffers.cpp:193
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
shared_bufferst::cfg_visitort::shared_buffers
shared_bufferst & shared_buffers
Definition: shared_buffers.h:194
shared_bufferst::nondet_flush
void nondet_flush(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)
instruments read
Definition: shared_buffers.cpp:447
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
shared_bufferst::instrumentations
std::set< irep_idt > instrumentations
Definition: shared_buffers.h:230
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
value_setst
Definition: value_sets.h:22
rw_set_loct
Definition: rw_set.h:186
shared_bufferst::cfg_visitort::coming_from
unsigned coming_from
Definition: shared_buffers.h:200
shared_bufferst::varst::type
typet type
Definition: shared_buffers.h:73
symbolt
Symbol table entry.
Definition: symbol.h:28
rw_set.h
Race Detection for Threaded Goto Programs.
ASSUME
@ ASSUME
Definition: goto_program.h:35
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
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:73
shared_bufferst::varst::w_buff0
irep_idt w_buff0
Definition: shared_buffers.h:54
shared_bufferst::varst::r_buff1_thds
std::vector< irep_idt > r_buff1_thds
Definition: shared_buffers.h:67
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
shared_bufferst::flush_read
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
Definition: shared_buffers.cpp:242
messaget::debug
mstreamt & debug() const
Definition: message.h:429
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
codet::op1
exprt & op1()
Definition: expr.h:105
shared_bufferst::operator()
const varst & operator()(const irep_idt &object)
instruments the variable
Definition: shared_buffers.cpp:28
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
fence.h
Fences for instrumentation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:473
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
shared_bufferst::uniq
unsigned uniq
Definition: shared_buffers.h:238
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
messaget::warning
mstreamt & warning() const
Definition: message.h:404
shared_bufferst::varst::read_delayed_var
irep_idt read_delayed_var
Definition: shared_buffers.h:71
shared_bufferst::varst::mem_tmp
irep_idt mem_tmp
Definition: shared_buffers.h:63
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
shared_bufferst::varst
Definition: shared_buffers.h:50
c_types.h
shared_bufferst::nb_threads
unsigned nb_threads
Definition: shared_buffers.h:227
shared_bufferst::affected_by_delay
void affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
Definition: shared_buffers.cpp:1022
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
shared_bufferst::add_initialization
void add_initialization(goto_programt &goto_program)
Definition: shared_buffers.cpp:110
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:946
not_exprt
Boolean negation.
Definition: std_expr.h:2843