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