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