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_nonconst() = code_assignt(symbol, value);
180  t->code_nonconst().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,
300  target,
301  source_location,
302  vars.w_buff0,
303  original_instruction.get_code().op1());
304 
305  // We update the used flags
306  assignment(
307  goto_program,
308  target,
309  source_location,
310  vars.w_buff1_used,
311  vars.w_buff0_used);
312  assignment(
313  goto_program,
314  target,
315  source_location,
316  vars.w_buff0_used,
317  true_exprt());
318 
319  // We should not exceed the buffer size -- inserts assertion for dynamically
320  // checking this
321  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
322  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
323  const exprt cond_expr=
324  not_exprt(and_exprt(buff1_used_expr, buff0_used_expr));
325 
326  target = goto_program.insert_before(
327  target, goto_programt::make_assertion(cond_expr, source_location));
328  target++;
329 
330  // We update writers ownership of the values in the buffer
331  for(unsigned cnt=0; cnt<nb_threads; cnt++)
332  assignment(goto_program, target, source_location, vars.r_buff1_thds[cnt],
333  vars.r_buff0_thds[cnt]);
334 
335  // We update the lucky new author of this value in the buffer
336  assignment(
337  goto_program,
338  target,
339  source_location,
340  vars.r_buff0_thds[current_thread],
341  true_exprt());
342 }
343 
346  goto_programt &goto_program,
347  goto_programt::targett &target,
348  const source_locationt &source_location,
349  const irep_idt &object,
350  const unsigned current_thread)
351 {
352  const std::string identifier=id2string(object);
353 
354  // mostly for instrumenting the fences. A thread only flushes the values it
355  // wrote in the buffer.
356  message.debug() << "det flush: " << messaget::eom;
357  const varst &vars=(*this)(object);
358 
359  // current value in the memory
360  const exprt lhs=symbol_exprt(object, vars.type);
361 
362  // if buff0 from this thread, uses it to update the memory (the most recent
363  // value, or last write by -ws-> ); if not, if buff1 from this thread, uses
364  // it; if not, keeps the current memory value
365  const exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
366  const exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
367 
368  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
369  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
370 
371  const exprt buff0_mine_expr=symbol_exprt(vars.r_buff0_thds[current_thread],
372  bool_typet());
373  const exprt buff1_mine_expr=symbol_exprt(vars.r_buff1_thds[current_thread],
374  bool_typet());
375 
376  const exprt buff0_used_and_mine_expr=and_exprt(buff0_used_expr,
377  buff0_mine_expr);
378  const exprt buff1_used_and_mine_expr=and_exprt(buff1_used_expr,
379  buff1_mine_expr);
380 
381  const exprt new_value_expr=
382  if_exprt(
383  buff0_used_and_mine_expr,
384  buff0_expr,
385  if_exprt(
386  buff1_used_and_mine_expr,
387  buff1_expr,
388  lhs));
389 
390  // We update (or not) the value in the memory
391  assignment(goto_program, target, source_location, object, new_value_expr);
392 
393  // We update the flags of the buffer
394  // if buff0 used and mine, then it is no more used, as we flushed the last
395  // write and -ws-> imposes not to have other writes in the buffer
396  assignment(
397  goto_program,
398  target,
399  source_location,
400  vars.w_buff0_used,
401  if_exprt(
402  buff0_used_and_mine_expr,
403  false_exprt(),
404  buff0_used_expr));
405 
406  // buff1 used and mine & not buff0 used and mine, then it no more used
407  // if buff0 is used and mine, then, by ws, buff1 is no more used
408  // otherwise, remains as it is
409  const exprt buff0_or_buff1_used_and_mine_expr=
410  or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
411 
412  assignment(
413  goto_program,
414  target,
415  source_location,
416  vars.w_buff1_used,
417  if_exprt(
418  buff0_or_buff1_used_and_mine_expr,
419  false_exprt(),
420  buff1_used_expr));
421 
422  // We update the ownerships
423  // if buff0 mine and used, flushed, so belongs to nobody
424  const exprt buff0_thd_expr=
425  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
426 
427  assignment(
428  goto_program,
429  target,
430  source_location,
431  vars.r_buff0_thds[current_thread],
432  if_exprt(buff0_used_and_mine_expr, false_exprt(), buff0_thd_expr));
433 
434  // if buff1 used and mine, or if buff0 used and mine, then buff1 flushed and
435  // doesn't belong to anybody
436  const exprt buff1_thd_expr=
437  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
438 
439  assignment(
440  goto_program,
441  target,
442  source_location,
443  vars.r_buff1_thds[current_thread],
444  if_exprt(
445  buff0_or_buff1_used_and_mine_expr,
446  false_exprt(),
447  buff1_thd_expr));
448 }
449 
452  const irep_idt &function_id,
453  goto_programt &goto_program,
454  goto_programt::targett &target,
455  const source_locationt &source_location,
456  const irep_idt &object,
457  const unsigned current_thread,
458  const bool tso_pso_rmo) // true: tso/pso/rmo; false: power
459 {
460  const std::string identifier=id2string(object);
461 
462  message.debug() << "nondet flush: " << object << messaget::eom;
463 
464  try
465  {
466  const varst &vars=(*this)(object);
467 
468  // Non deterministic choice
469  irep_idt choice0 = choice(function_id, "0");
470  irep_idt choice2 = choice(function_id, "2"); // delays the write flush
471 
472  const symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
473  const symbol_exprt delay_expr=symbol_exprt(choice2, bool_typet());
474  const exprt nondet_bool_expr =
475  side_effect_expr_nondett(bool_typet(), source_location);
476 
477  // throw Boolean dice
478  assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
479  assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
480 
481  // Buffers and memory
482  const symbol_exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
483  const symbol_exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
484  const exprt lhs=symbol_exprt(object, vars.type);
485 
486  // Buffer uses
487  const symbol_exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used,
488  bool_typet());
489  const symbol_exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used,
490  bool_typet());
491 
492  // Buffer ownerships
493  const symbol_exprt buff0_thd_expr=
494  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
495  const symbol_exprt buff1_thd_expr=
496  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
497 
498 
499  // Will the write be directly flushed, or is it just a read?
500  assignment(
501  goto_program, target, source_location, vars.flush_delayed, delay_expr);
502  assignment(goto_program, target, source_location, vars.mem_tmp, lhs);
503 
504  // for POWER, only instrumented reads can read from the buffers of other
505  // threads
506  bool instrumented=false;
507 
508  if(!tso_pso_rmo)
509  {
510  if(cycles.find(object)!=cycles.end())
511  {
512  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
513  std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(object);
514  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
515  if(ran_it->second==source_location)
516  {
517  instrumented=true;
518  break;
519  }
520  }
521  }
522 
523  // TSO/PSO/RMO
524  if(tso_pso_rmo || !instrumented)
525  {
526  // 7 cases
527 
528  // (1) (3) (4)
529  // if buff0 unused
530  // or buff0 not mine and buff1 unused
531  // or buff0 not mine and buff1 not mine
532  // -> read from memory (and does not modify the buffer in any aspect)
533  const exprt cond_134_expr=
534  or_exprt(
535  not_exprt(buff0_used_expr),
536  or_exprt(
537  and_exprt(
538  not_exprt(buff0_thd_expr),
539  not_exprt(buff1_used_expr)),
540  and_exprt(
541  not_exprt(buff0_thd_expr),
542  not_exprt(buff1_thd_expr))));
543  const exprt val_134_expr=lhs;
544  const exprt buff0_used_134_expr=buff0_used_expr;
545  const exprt buff1_used_134_expr=buff1_used_expr;
546  const exprt buff0_134_expr=buff0_expr;
547  const exprt buff1_134_expr=buff1_expr;
548  const exprt buff0_thd_134_expr=buff0_thd_expr;
549  const exprt buff1_thd_134_expr=buff1_thd_expr;
550 
551  // (2) (6) (7)
552  // if buff0 used and mine
553  // -> read from buff0
554  const exprt cond_267_expr=and_exprt(buff0_used_expr, buff0_thd_expr);
555  const exprt val_267_expr=buff0_expr;
556  const exprt buff0_used_267_expr=false_exprt();
557  const exprt buff1_used_267_expr=false_exprt();
558  const exprt buff0_267_expr=buff0_expr;
559  const exprt buff1_267_expr=buff1_expr;
560  const exprt buff0_thd_267_expr=false_exprt();
561  const exprt buff1_thd_267_expr=false_exprt();
562 
563  // (5)
564  // buff0 and buff1 are used, buff0 is not mine, buff1 is mine
565  // -> read from buff1
566  const exprt cond_5_expr=
567  and_exprt(
568  buff0_used_expr,
569  and_exprt(
570  buff1_used_expr,
571  and_exprt(not_exprt(buff0_thd_expr), buff1_thd_expr)));
572  const exprt val_5_expr=buff1_expr;
573  const exprt buff0_used_5_expr=buff0_used_expr;
574  const exprt buff1_used_5_expr=false_exprt();
575  const exprt buff0_5_expr=buff0_expr;
576  const exprt buff1_5_expr=buff1_expr;
577  const exprt buff0_thd_5_expr=buff0_thd_expr;
578  const exprt buff1_thd_5_expr=false_exprt();
579 
580  // Updates
581  // memory
582  assignment(
583  goto_program,
584  target,
585  source_location,
586  object,
587  if_exprt(
588  cond_134_expr,
589  val_134_expr,
590  if_exprt(
591  cond_267_expr,
592  val_267_expr,
593  val_5_expr)));
594  // buff0
595  assignment(
596  goto_program,
597  target,
598  source_location,
599  vars.w_buff0,
600  if_exprt(
601  delay_expr,
602  buff0_expr,
603  if_exprt(
604  cond_134_expr,
605  buff0_134_expr,
606  if_exprt(
607  cond_267_expr,
608  buff0_267_expr,
609  buff0_5_expr))));
610  // buff1
611  assignment(
612  goto_program,
613  target,
614  source_location,
615  vars.w_buff1,
616  if_exprt(
617  delay_expr,
618  buff1_expr,
619  if_exprt(
620  cond_134_expr,
621  buff1_134_expr,
622  if_exprt(
623  cond_267_expr,
624  buff1_267_expr,
625  buff1_5_expr))));
626  // buff0_used
627  assignment(
628  goto_program,
629  target,
630  source_location,
631  vars.w_buff0_used,
632  if_exprt(
633  delay_expr,
634  buff0_used_expr,
635  if_exprt(
636  cond_134_expr,
637  buff0_used_134_expr,
638  if_exprt(
639  cond_267_expr,
640  buff0_used_267_expr,
641  buff0_used_5_expr))));
642  // buff1_used
643  assignment(
644  goto_program,
645  target,
646  source_location,
647  vars.w_buff1_used,
648  if_exprt(
649  delay_expr,
650  buff1_used_expr,
651  if_exprt(
652  cond_134_expr,
653  buff1_used_134_expr,
654  if_exprt(
655  cond_267_expr,
656  buff1_used_267_expr,
657  buff1_used_5_expr))));
658  // buff0_thd
659  assignment(
660  goto_program,
661  target,
662  source_location,
663  vars.r_buff0_thds[current_thread],
664  if_exprt(
665  delay_expr,
666  buff0_thd_expr,
667  if_exprt(
668  cond_134_expr,
669  buff0_thd_134_expr,
670  if_exprt(
671  cond_267_expr,
672  buff0_thd_267_expr,
673  buff0_thd_5_expr))));
674  // buff1_thd
675  assignment(
676  goto_program,
677  target,
678  source_location,
679  vars.r_buff1_thds[current_thread], if_exprt(
680  delay_expr,
681  buff1_thd_expr,
682  if_exprt(
683  cond_134_expr,
684  buff1_thd_134_expr,
685  if_exprt(
686  cond_267_expr,
687  buff1_thd_267_expr,
688  buff1_thd_5_expr))));
689  }
690  // POWER
691  else
692  {
693  // a thread can read the other threads' buffers
694 
695  // One extra non-deterministic choice needed
696  irep_idt choice1 = choice(function_id, "1");
697  const symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
698 
699  // throw Boolean dice
700  assignment(
701  goto_program, target, source_location, choice1, nondet_bool_expr);
702 
703  // 7 cases
704 
705  // (1)
706  // if buff0 unused
707  // -> read from memory (and does not modify the buffer in any aspect)
708  const exprt cond_1_expr=not_exprt(buff0_used_expr);
709  const exprt val_1_expr=lhs;
710  const exprt buff0_used_1_expr=buff0_used_expr;
711  const exprt buff1_used_1_expr=buff1_used_expr;
712  const exprt buff0_1_expr=buff0_expr;
713  const exprt buff1_1_expr=buff1_expr;
714  const exprt buff0_thd_1_expr=buff0_thd_expr;
715  const exprt buff1_thd_1_expr=buff1_thd_expr;
716 
717  // (2) (6) (7)
718  // if buff0 used and mine
719  // -> read from buff0
720  const exprt cond_267_expr=
721  and_exprt(buff0_used_expr, buff0_thd_expr);
722  const exprt val_267_expr=buff0_expr;
723  const exprt buff0_used_267_expr=false_exprt();
724  const exprt buff1_used_267_expr=false_exprt();
725  const exprt buff0_267_expr=buff0_expr;
726  const exprt buff1_267_expr=buff1_expr;
727  const exprt buff0_thd_267_expr=false_exprt();
728  const exprt buff1_thd_267_expr=false_exprt();
729 
730  // (3)
731  // if buff0 used and not mine, and buff1 not used
732  // -> read from buff0 or memory
733  const exprt cond_3_expr=
734  and_exprt(
735  buff0_used_expr,
736  and_exprt(
737  not_exprt(buff0_thd_expr),
738  not_exprt(buff1_used_expr)));
739  const exprt val_3_expr=if_exprt(choice0_expr, buff0_expr, lhs);
740  const exprt buff0_used_3_expr=choice0_expr;
741  const exprt buff1_used_3_expr=false_exprt();
742  const exprt buff0_3_expr=buff0_expr;
743  const exprt buff1_3_expr=buff1_expr;
744  const exprt buff0_thd_3_expr=false_exprt();
745  const exprt buff1_thd_3_expr=false_exprt();
746 
747  // (4)
748  // buff0 and buff1 are both used, and both not mine
749  // -> read from memory or buff0 or buff1
750  const exprt cond_4_expr=
751  and_exprt(
752  and_exprt(buff0_used_expr, not_exprt(buff1_thd_expr)),
753  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
754  const exprt val_4_expr=
755  if_exprt(
756  choice0_expr,
757  lhs,
758  if_exprt(
759  choice1_expr,
760  buff0_expr,
761  buff1_expr));
762  const exprt buff0_used_4_expr=
763  or_exprt(choice0_expr, not_exprt(choice1_expr));
764  const exprt buff1_used_4_expr=choice0_expr;
765  const exprt buff0_4_expr=buff0_expr;
766  const exprt buff1_4_expr=buff1_expr;
767  const exprt buff0_thd_4_expr=buff0_thd_expr;
768  const exprt buff1_thd_4_expr=
769  if_exprt(choice0_expr, buff1_thd_expr, false_exprt());
770 
771  // (5)
772  // buff0 and buff1 are both used, and buff0 not mine, and buff1 mine
773  // -> read buff1 or buff0
774  const exprt cond_5_expr=
775  and_exprt(
776  and_exprt(buff0_used_expr, buff1_thd_expr),
777  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
778  const exprt val_5_expr=
779  if_exprt(
780  choice0_expr,
781  buff1_expr,
782  buff0_expr);
783  const exprt buff0_used_5_expr=choice0_expr;
784  const exprt buff1_used_5_expr=false_exprt();
785  const exprt buff0_5_expr=buff0_expr;
786  const exprt buff1_5_expr=buff1_expr;
787  const exprt buff0_thd_5_expr=false_exprt();
788  const exprt buff1_thd_5_expr=false_exprt();
789 
790  // Updates
791  // memory
792  assignment(
793  goto_program,
794  target,
795  source_location,
796  object,
797  if_exprt(
798  cond_1_expr,
799  val_1_expr,
800  if_exprt(
801  cond_267_expr,
802  val_267_expr,
803  if_exprt(
804  cond_4_expr,
805  val_4_expr,
806  if_exprt(
807  cond_5_expr,
808  val_5_expr,
809  val_3_expr)))));
810  // buff0
811  assignment(
812  goto_program,
813  target,
814  source_location,
815  vars.w_buff0,
816  if_exprt(
817  delay_expr,
818  buff0_expr,
819  if_exprt(
820  cond_1_expr,
821  buff0_1_expr,
822  if_exprt(
823  cond_267_expr,
824  buff0_267_expr,
825  if_exprt(
826  cond_4_expr,
827  buff0_4_expr,
828  if_exprt(
829  cond_5_expr,
830  buff0_5_expr,
831  buff0_3_expr))))));
832  // buff1
833  assignment(
834  goto_program,
835  target,
836  source_location,
837  vars.w_buff1,
838  if_exprt(
839  delay_expr,
840  buff1_expr,
841  if_exprt(
842  cond_1_expr,
843  buff1_1_expr,
844  if_exprt(
845  cond_267_expr,
846  buff1_267_expr,
847  if_exprt(
848  cond_4_expr,
849  buff1_4_expr,
850  if_exprt(
851  cond_5_expr,
852  buff1_5_expr,
853  buff1_3_expr))))));
854  // buff0_used
855  assignment(
856  goto_program,
857  target,
858  source_location,
859  vars.w_buff0_used,
860  if_exprt(
861  delay_expr,
862  buff0_used_expr,
863  if_exprt(
864  cond_1_expr,
865  buff0_used_1_expr,
866  if_exprt(
867  cond_267_expr,
868  buff0_used_267_expr,
869  if_exprt(
870  cond_4_expr,
871  buff0_used_4_expr,
872  if_exprt(
873  cond_5_expr,
874  buff0_used_5_expr,
875  buff0_used_3_expr))))));
876  // buff1_used
877  assignment(
878  goto_program,
879  target,
880  source_location,
881  vars.w_buff1_used,
882  if_exprt(
883  delay_expr,
884  buff1_used_expr,
885  if_exprt(
886  cond_1_expr,
887  buff1_used_1_expr,
888  if_exprt(
889  cond_267_expr,
890  buff1_used_267_expr,
891  if_exprt(
892  cond_4_expr,
893  buff1_used_4_expr,
894  if_exprt(
895  cond_5_expr,
896  buff1_used_5_expr,
897  buff1_used_3_expr))))));
898  // buff0_thd
899  assignment(
900  goto_program,
901  target,
902  source_location,
903  vars.r_buff0_thds[current_thread],
904  if_exprt(
905  delay_expr,
906  buff0_thd_expr,
907  if_exprt(
908  cond_1_expr,
909  buff0_thd_1_expr,
910  if_exprt(
911  cond_267_expr,
912  buff0_thd_267_expr,
913  if_exprt(
914  cond_4_expr,
915  buff0_thd_4_expr,
916  if_exprt(
917  cond_5_expr,
918  buff0_thd_5_expr,
919  buff0_thd_3_expr))))));
920  // buff1_thd
921  assignment(
922  goto_program,
923  target,
924  source_location,
925  vars.r_buff1_thds[current_thread],
926  if_exprt(
927  delay_expr,
928  buff1_thd_expr,
929  if_exprt(
930  cond_1_expr,
931  buff1_thd_1_expr,
932  if_exprt(
933  cond_267_expr,
934  buff1_thd_267_expr,
935  if_exprt(
936  cond_4_expr,
937  buff1_thd_4_expr,
938  if_exprt(
939  cond_5_expr,
940  buff1_thd_5_expr,
941  buff1_thd_3_expr))))));
942  }
943  }
944  catch(const std::string &s)
945  {
946  message.warning() << s << messaget::eom;
947  }
948 }
949 
951  const namespacet &ns,
952  const symbol_exprt &symbol_expr,
953  bool is_write
954  // are we asking for the variable (false), or for the variable and
955  // the source_location in the code (true)
956 )
957 {
958  const irep_idt &identifier=symbol_expr.get_identifier();
959 
960  if(identifier==CPROVER_PREFIX "alloc" ||
961  identifier==CPROVER_PREFIX "alloc_size" ||
962  identifier=="stdin" ||
963  identifier=="stdout" ||
964  identifier=="stderr" ||
965  identifier=="sys_nerr" ||
966  has_prefix(id2string(identifier), "__unbuffered_") ||
967  has_prefix(id2string(identifier), "__CPROVER"))
968  return false; // not buffered
969 
970  const symbolt &symbol=ns.lookup(identifier);
971 
972  if(!symbol.is_static_lifetime)
973  return false; // these are local
974 
975  if(symbol.is_thread_local)
976  return false; // these are local
977 
978  if(instrumentations.find(identifier)!=instrumentations.end())
979  return false; // these are instrumentations
980 
981  return is_buffered_in_general(symbol_expr, is_write);
982 }
983 
985  const symbol_exprt &symbol_expr,
986  bool is_write
987  // are we asking for the variable (false), or for the variable and the
988  // source_location in the code? (true)
989 )
990 {
991  if(cav11)
992  return true;
993 
994  const irep_idt &identifier=symbol_expr.get_identifier();
995  const source_locationt &source_location=symbol_expr.source_location();
996 
997  if(cycles.find(identifier)==cycles.end())
998  return false; // not to instrument
999 
1000  if(!is_write)
1001  {
1002  // to be uncommented only when we are sure all the cycles
1003  // are detected (before detection of the pairs -- no hack)
1004  // WARNING: on the FULL cycle, not reduced by PO
1005  /*typedef std::multimap<irep_idt,source_locationt>::iterator m_itt;
1006  std::pair<m_itt,m_itt> ran=cycles_r_loc.equal_range(identifier);
1007  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1008  if(ran_it->second==source_location)*/
1009  return true;
1010  }
1011  else
1012  {
1013  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1014  std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(identifier);
1015  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1016  if(ran_it->second==source_location)
1017  return true; // not to instrument
1018  }
1019 
1020  return false;
1021 }
1022 
1027  value_setst &value_sets,
1028  goto_functionst &goto_functions)
1029 {
1031 
1032  for(auto &gf_entry : goto_functions.function_map)
1033  {
1034 #ifdef LOCAL_MAY
1035  local_may_aliast local_may(gf_entry.second);
1036 #endif
1037 
1038  Forall_goto_program_instructions(i_it, gf_entry.second.body)
1039  {
1040  rw_set_loct rw_set(
1041  ns,
1042  value_sets,
1043  gf_entry.first,
1044  i_it
1045 #ifdef LOCAL_MAY
1046  ,
1047  local_may
1048 #endif
1049  ); // NOLINT(whitespace/parens)
1050  for(const auto &w_entry : rw_set.w_entries)
1051  {
1052  for(const auto &r_entry : rw_set.r_entries)
1053  {
1054  message.debug() << "debug: " << id2string(w_entry.second.object)
1055  << " reads from " << id2string(r_entry.second.object)
1056  << messaget::eom;
1057  if(is_buffered_in_general(r_entry.second.symbol_expr, true))
1058  {
1059  // shouldn't it be true? false => overapprox
1060  affected_by_delay_set.insert(w_entry.second.object);
1061  }
1062  }
1063  }
1064  }
1065  }
1066 }
1067 
1070  value_setst &value_sets,
1071  const irep_idt &function_id,
1072  memory_modelt model)
1073 {
1075  << "visit function " << function_id << messaget::eom;
1076  if(function_id == INITIALIZE_FUNCTION)
1077  return;
1078 
1080  goto_programt &goto_program = goto_functions.function_map[function_id].body;
1081 
1082 #ifdef LOCAL_MAY
1083  local_may_aliast local_may(goto_functions.function_map[function_id]);
1084 #endif
1085 
1086  Forall_goto_program_instructions(i_it, goto_program)
1087  {
1088  goto_programt::instructiont &instruction=*i_it;
1089 
1090  shared_buffers.message.debug() << "instruction "<<instruction.type
1091  << messaget::eom;
1092 
1093  /* thread marking */
1094  if(instruction.is_start_thread())
1095  {
1099  }
1100  else if(instruction.is_end_thread())
1102 
1103  if(instruction.is_assign())
1104  {
1105  try
1106  {
1107  rw_set_loct rw_set(
1108  ns,
1109  value_sets,
1110  function_id,
1111  i_it
1112 #ifdef LOCAL_MAY
1113  ,
1114  local_may
1115 #endif
1116  ); // NOLINT(whitespace/parens)
1117 
1118  if(rw_set.empty())
1119  continue;
1120 
1121  // add all the written values (which are not instrumentations)
1122  // in a set
1123  for(const auto &w_entry : rw_set.w_entries)
1124  {
1125  if(shared_buffers.is_buffered(ns, w_entry.second.symbol_expr, false))
1126  past_writes.insert(w_entry.second.object);
1127  }
1128 
1129  goto_programt::instructiont original_instruction;
1130  original_instruction.swap(instruction);
1131  const source_locationt &source_location=
1132  original_instruction.source_location;
1133 
1134  // ATOMIC_BEGIN: we make the whole thing atomic
1135  instruction = goto_programt::make_atomic_begin(source_location);
1136  i_it++;
1137 
1138  // we first perform (non-deterministically) up to 2 writes for
1139  // stuff that is potentially read
1140  for(const auto &r_entry : rw_set.r_entries)
1141  {
1142  // flush read -- do nothing in this implementation
1144  goto_program, i_it, source_location, r_entry.second.object);
1145 
1146  if(shared_buffers.is_buffered(ns, r_entry.second.symbol_expr, false))
1148  function_id,
1149  goto_program,
1150  i_it,
1151  source_location,
1152  r_entry.second.object,
1154  (model == TSO || model == PSO || model == RMO));
1155  }
1156 
1157  // Now perform the write(s).
1158  for(const auto &w_entry : rw_set.w_entries)
1159  {
1160  // if one of the previous read was to buffer, then delays the read
1161  if(model==RMO || model==Power)
1162  {
1163  for(const auto &r_entry : rw_set.r_entries)
1164  {
1166  ns, r_entry.second.symbol_expr, true))
1167  {
1169  goto_program,
1170  i_it,
1171  source_location,
1172  r_entry.second.object,
1173  w_entry.second.object);
1174  }
1175  }
1176  }
1177 
1178  if(shared_buffers.is_buffered(ns, w_entry.second.symbol_expr, true))
1179  {
1181  goto_program,
1182  i_it,
1183  source_location,
1184  w_entry.second.object,
1185  original_instruction,
1186  current_thread);
1187  }
1188  else
1189  {
1190  // unbuffered
1191  if(model==RMO || model==Power)
1192  {
1193  for(const auto &r_entry : rw_set.r_entries)
1194  {
1195  if(
1197  r_entry.second.object) !=
1199  {
1201  << "second: " << r_entry.second.object << messaget::eom;
1202  const varst &vars = (shared_buffers)(r_entry.second.object);
1203 
1205  << "writer " << w_entry.second.object << " reads "
1206  << r_entry.second.object << messaget::eom;
1207 
1208  // TO FIX: how to deal with rhs including calls?
1209  // if a read is delayed, use its alias instead of itself
1210  // -- or not
1211  symbol_exprt to_replace_expr =
1212  symbol_exprt(r_entry.second.object, vars.type);
1213  symbol_exprt new_read_expr=symbol_exprt(
1214  vars.read_delayed_var,
1215  pointer_type(vars.type));
1216  symbol_exprt read_delayed_expr=symbol_exprt(
1217  vars.read_delayed, bool_typet());
1218 
1219  // One extra non-deterministic choice needed
1220  irep_idt choice1 = shared_buffers.choice(function_id, "1");
1221  const symbol_exprt choice1_expr=symbol_exprt(choice1,
1222  bool_typet());
1223  const exprt nondet_bool_expr =
1224  side_effect_expr_nondett(bool_typet(), source_location);
1225 
1226  // throw Boolean dice
1228  goto_program,
1229  i_it,
1230  source_location,
1231  choice1,
1232  nondet_bool_expr);
1233 
1234  const if_exprt rhs(
1235  read_delayed_expr,
1236  if_exprt(
1237  choice1_expr,
1238  dereference_exprt{new_read_expr},
1239  to_replace_expr),
1240  to_replace_expr); // original_instruction.get_code().op1());
1241 
1243  goto_program,
1244  i_it,
1245  source_location,
1246  r_entry.second.object,
1247  rhs);
1248  }
1249  }
1250  }
1251 
1252  // normal assignment
1254  goto_program,
1255  i_it,
1256  source_location,
1257  w_entry.second.object,
1258  original_instruction.get_code().op1());
1259  }
1260  }
1261 
1262  // if last writes was flushed to make the lhs reads the buffer but
1263  // without affecting the memory, restore the previous memory value
1264  // (buffer flush delay)
1265  for(const auto &r_entry : rw_set.r_entries)
1266  {
1267  if(shared_buffers.is_buffered(ns, r_entry.second.symbol_expr, false))
1268  {
1270  << "flush restore: " << r_entry.second.object << messaget::eom;
1271  const varst vars = (shared_buffers)(r_entry.second.object);
1272  const exprt delayed_expr=symbol_exprt(vars.flush_delayed,
1273  bool_typet());
1274  const symbol_exprt mem_value_expr=symbol_exprt(vars.mem_tmp,
1275  vars.type);
1276  const exprt cond_expr = if_exprt(
1277  delayed_expr, mem_value_expr, r_entry.second.symbol_expr);
1278 
1280  goto_program,
1281  i_it,
1282  source_location,
1283  r_entry.second.object,
1284  cond_expr);
1286  goto_program, i_it, source_location,
1287  vars.flush_delayed, false_exprt());
1288  }
1289  }
1290 
1291  // ATOMIC_END
1292  i_it = goto_program.insert_before(
1293  i_it, goto_programt::make_atomic_end(source_location));
1294  i_it++;
1295 
1296  i_it--; // the for loop already counts us up
1297  }
1298  catch (...)
1299  {
1300  shared_buffers.message.warning() << "Identifier not found"
1301  << messaget::eom;
1302  }
1303  }
1304  else if(
1305  is_fence(instruction, ns) ||
1306  (instruction.is_other() &&
1307  instruction.get_code().get_statement() == ID_fence &&
1308  (instruction.get_code().get_bool("WRfence") ||
1309  instruction.get_code().get_bool("WWfence") ||
1310  instruction.get_code().get_bool("RWfence") ||
1311  instruction.get_code().get_bool("RRfence"))))
1312  {
1313  goto_programt::instructiont original_instruction;
1314  original_instruction.swap(instruction);
1315  const source_locationt &source_location=
1316  original_instruction.source_location;
1317 
1318  // ATOMIC_BEGIN
1319  instruction = goto_programt::make_atomic_begin(source_location);
1320  i_it++;
1321 
1322  // does it for all the previous statements
1323  for(std::set<irep_idt>::iterator s_it=past_writes.begin();
1324  s_it!=past_writes.end(); s_it++)
1325  {
1327  goto_program, i_it, source_location, *s_it,
1328  current_thread);
1329  }
1330 
1331  // ATOMIC_END
1332  i_it = goto_program.insert_before(
1333  i_it, goto_programt::make_atomic_end(source_location));
1334  i_it++;
1335 
1336  i_it--; // the for loop already counts us up
1337  }
1338  else if(is_lwfence(instruction, ns))
1339  {
1340  // po -- remove the lwfence
1341  *i_it = goto_programt::make_skip(i_it->source_location);
1342  }
1343  else if(instruction.is_function_call())
1344  {
1345  const exprt &fun = instruction.get_function_call().function();
1346  weak_memory(value_sets, to_symbol_expr(fun).get_identifier(), model);
1347  }
1348  }
1349 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
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:34
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:347
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:345
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:984
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:450
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:494
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:386
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:350
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:1834
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:36
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:458
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: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:155
equal_exprt
Equality.
Definition: std_expr.h:1139
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
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
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:950
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:141
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:623
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:877
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:1942
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
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::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:835
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:109
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
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:319
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:1069
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:189
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:919
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
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:451
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
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:444
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:330
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:457
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
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:445
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:238
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:1026
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:563
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:930
not_exprt
Boolean negation.
Definition: std_expr.h:2041