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 
14 
15 #include <goto-instrument/rw_set.h>
16 
17 #include "fence.h"
18 
20 std::string shared_bufferst::unique(void)
21 {
23  return "$fresh#"+std::to_string(uniq++);
24 }
25 
28  const irep_idt &object)
29 {
30  var_mapt::const_iterator it=var_map.find(object);
31  if(it!=var_map.end())
32  return it->second;
33 
34  varst &vars=var_map[object];
35 
37  const symbolt &symbol=ns.lookup(object);
38 
39  vars.type=symbol.type;
40 
41  vars.w_buff0=add(object, symbol.base_name, "$w_buff0", symbol.type);
42  vars.w_buff1=add(object, symbol.base_name, "$w_buff1", symbol.type);
43 
44  vars.w_buff0_used=add(object, symbol.base_name, "$w_buff0_used",
45  bool_typet());
46  vars.w_buff1_used=add(object, symbol.base_name, "$w_buff1_used",
47  bool_typet());
48 
49  vars.mem_tmp=add(object, symbol.base_name, "$mem_tmp", symbol.type);
50  vars.flush_delayed=add(object, symbol.base_name, "$flush_delayed",
51  bool_typet());
52 
53  vars.read_delayed=
54  add(object, symbol.base_name, "$read_delayed", bool_typet());
55  vars.read_delayed_var=
56  add(
57  object,
58  symbol.base_name,
59  "$read_delayed_var",
60  pointer_type(symbol.type));
61 
62  for(unsigned cnt=0; cnt<nb_threads; cnt++)
63  {
64  vars.r_buff0_thds.push_back(
66  object,
67  symbol.base_name,
68  "$r_buff0_thd"+std::to_string(cnt),
69  bool_typet()));
70  vars.r_buff1_thds.push_back(
72  object,
73  symbol.base_name,
74  "$r_buff1_thd"+std::to_string(cnt),
75  bool_typet()));
76  }
77 
78  return vars;
79 }
80 
85  const irep_idt &object,
86  const irep_idt &base_name,
87  const std::string &suffix,
88  const typet &type,
89  bool instrument)
90 {
91  const irep_idt identifier=id2string(object)+suffix;
92 
93  symbolt new_symbol;
94  new_symbol.name=identifier;
95  new_symbol.base_name=id2string(base_name)+suffix;
96  new_symbol.type=type;
97  new_symbol.is_static_lifetime=true;
98  new_symbol.value.make_nil();
99 
100  if(instrument)
101  instrumentations.insert(identifier);
102 
103  symbolt *symbol_ptr;
104  symbol_table.move(new_symbol, symbol_ptr);
105  return identifier;
106 }
107 
109 {
110  goto_programt::targett t=goto_program.instructions.begin();
111  const namespacet ns(symbol_table);
112 
113  for(const auto &vars : var_map)
114  {
115  source_locationt source_location;
116  source_location.make_nil();
117 
118  assignment(goto_program, t, source_location, vars.second.w_buff0_used,
119  false_exprt());
120  assignment(goto_program, t, source_location, vars.second.w_buff1_used,
121  false_exprt());
122  assignment(goto_program, t, source_location, vars.second.flush_delayed,
123  false_exprt());
124  assignment(goto_program, t, source_location, vars.second.read_delayed,
125  false_exprt());
126  assignment(goto_program, t, source_location, vars.second.read_delayed_var,
127  null_pointer_exprt(pointer_type(vars.second.type)));
128 
129  for(const auto &id : vars.second.r_buff0_thds)
130  assignment(goto_program, t, source_location, id, false_exprt());
131 
132  for(const auto &id : vars.second.r_buff1_thds)
133  assignment(goto_program, t, source_location, id, false_exprt());
134  }
135 }
136 
138  goto_functionst &goto_functions)
139 {
140  // get "main"
141  goto_functionst::function_mapt::iterator
142  m_it=goto_functions.function_map.find(goto_functions.entry_point());
143 
144  if(m_it==goto_functions.function_map.end())
145  throw "weak memory instrumentation needs an entry point";
146 
147  goto_programt &main=m_it->second.body;
149 }
150 
153  goto_programt &goto_program,
155  const source_locationt &source_location,
156  const irep_idt &id_lhs,
157  const exprt &value)
158 {
159  const namespacet ns(symbol_table);
160  std::string identifier=id2string(id_lhs);
161 
162  const size_t pos=identifier.find("[]");
163 
164  if(pos!=std::string::npos)
165  {
166  /* we don't distinguish the members of an array for the moment */
167  identifier.erase(pos);
168  }
169 
170  try
171  {
172  const exprt symbol=ns.lookup(identifier).symbol_expr();
173 
174  t=goto_program.insert_before(t);
175  t->type=ASSIGN;
176  t->code=code_assignt(symbol, value);
177  t->code.add_source_location()=source_location;
178  t->source_location=source_location;
179 
180  // instrumentations.insert((const irep_idt) (t->code.id()));
181 
182  t++;
183  }
184  catch(const std::string &s)
185  {
186  message.warning() << s << messaget::eom;
187  }
188 }
189 
192  goto_programt &goto_program,
193  goto_programt::targett &target,
194  const source_locationt &source_location,
195  const irep_idt &read_object,
196  const irep_idt &write_object)
197 {
198 /* option 1: */
199 /* trick using an additional variable whose value is to be defined later */
200 
201 #if 0
202  assignment(goto_program, target, source_location, vars.read_delayed,
203  true_exprt());
204  assignment(goto_program, target, source_location, vars.read_delayed_var,
205  read_object);
206 
207  const irep_idt &new_var=add_fresh_var(write_object, unique(), vars.type);
208 
209  assignment(goto_program, target, source_location, vars.read_new_var, new_var);
210 
211  // initial write, but from the new variable now
212  assignment(goto_program, target, source_location, write_object, new_var);
213 #endif
214 
215 /* option 2 */
216 /* pointer */
217 
218  const std::string identifier=id2string(write_object);
219 
220  message.debug()<<"delay_read: " << messaget::eom;
221  const varst &vars=(*this)(write_object);
222 
223  const symbol_exprt read_object_expr=symbol_exprt(read_object, vars.type);
224 
225  assignment(
226  goto_program,
227  target,
228  source_location,
229  vars.read_delayed,
230  true_exprt());
231  assignment(
232  goto_program,
233  target,
234  source_location,
235  vars.read_delayed_var,
236  address_of_exprt(read_object_expr));
237 }
238 
241  goto_programt &goto_program,
242  goto_programt::targett &target,
243  const source_locationt &source_location,
244  const irep_idt &write_object)
245 {
246 #if 0
247  // option 1
248  const varst &vars=(*this)(write_object);
249 
250  const symbol_exprt fresh_var_expr=symbol_exprt(vars.read_new_var, vars.type);
251  const symbol_exprt var_expr=symbol_exprt(vars.read_delayed_var, vars.type);
252  const exprt eq_expr=equal_exprt(var_expr, fresh_var_expr);
253 
254  const symbol_exprt cond_delayed_expr=symbol_exprt(vars.read_delayed,
255  bool_typet());
256  const exprt if_expr=if_exprt(cond_delayed_expr, eq_expr, true_exprt());
257 
258  target=goto_program.insert_before(target);
259  target->type=ASSUME;
260  target->guard=if_expr;
261  target->guard.source_location()=source_location;
262  target->source_location=source_location;
263 
264  target++;
265 
266  assignment(goto_program, target, source_location, vars.read_delayed,
267  false_exprt());
268 #else
269  // option 2: do nothing
270  // unused parameters
271  (void)goto_program;
272  (void)target;
273  (void)target;
274  (void)source_location;
275  (void)write_object;
276 #endif
277 }
278 
281  goto_programt &goto_program,
282  goto_programt::targett &target,
283  const source_locationt &source_location,
284  const irep_idt &object,
285  goto_programt::instructiont &original_instruction,
286  const unsigned current_thread)
287 {
288  const std::string identifier=id2string(object);
289 
290  message.debug() << "write: " << object << messaget::eom;
291  const varst &vars=(*this)(object);
292 
293  // We rotate the write buffers for anything that is written.
294  assignment(goto_program, target, source_location, vars.w_buff1, vars.w_buff0);
295  assignment(
296  goto_program, target, source_location, vars.w_buff0,
297  original_instruction.code.op1());
298 
299  // We update the used flags
300  assignment(
301  goto_program,
302  target,
303  source_location,
304  vars.w_buff1_used,
305  vars.w_buff0_used);
306  assignment(
307  goto_program,
308  target,
309  source_location,
310  vars.w_buff0_used,
311  true_exprt());
312 
313  // We should not exceed the buffer size -- inserts assertion for dynamically
314  // checking this
315  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
316  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
317  const exprt cond_expr=
318  not_exprt(and_exprt(buff1_used_expr, buff0_used_expr));
319 
320  target=goto_program.insert_before(target);
321  target->guard=cond_expr;
322  target->type=ASSERT;
323  target->code=code_assertt();
324  target->code.add_source_location()=source_location;
325  target->source_location=source_location;
326  target++;
327 
328  // We update writers ownership of the values in the buffer
329  for(unsigned cnt=0; cnt<nb_threads; cnt++)
330  assignment(goto_program, target, source_location, vars.r_buff1_thds[cnt],
331  vars.r_buff0_thds[cnt]);
332 
333  // We update the lucky new author of this value in the buffer
334  assignment(
335  goto_program,
336  target,
337  source_location,
338  vars.r_buff0_thds[current_thread],
339  true_exprt());
340 }
341 
344  goto_programt &goto_program,
345  goto_programt::targett &target,
346  const source_locationt &source_location,
347  const irep_idt &object,
348  const unsigned current_thread)
349 {
350  const std::string identifier=id2string(object);
351 
352  // mostly for instrumenting the fences. A thread only flushes the values it
353  // wrote in the buffer.
354  message.debug() << "det flush: " << messaget::eom;
355  const varst &vars=(*this)(object);
356 
357  // current value in the memory
358  const exprt lhs=symbol_exprt(object, vars.type);
359 
360  // if buff0 from this thread, uses it to update the memory (the most recent
361  // value, or last write by -ws-> ); if not, if buff1 from this thread, uses
362  // it; if not, keeps the current memory value
363  const exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
364  const exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
365 
366  const exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used, bool_typet());
367  const exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used, bool_typet());
368 
369  const exprt buff0_mine_expr=symbol_exprt(vars.r_buff0_thds[current_thread],
370  bool_typet());
371  const exprt buff1_mine_expr=symbol_exprt(vars.r_buff1_thds[current_thread],
372  bool_typet());
373 
374  const exprt buff0_used_and_mine_expr=and_exprt(buff0_used_expr,
375  buff0_mine_expr);
376  const exprt buff1_used_and_mine_expr=and_exprt(buff1_used_expr,
377  buff1_mine_expr);
378 
379  const exprt new_value_expr=
380  if_exprt(
381  buff0_used_and_mine_expr,
382  buff0_expr,
383  if_exprt(
384  buff1_used_and_mine_expr,
385  buff1_expr,
386  lhs));
387 
388  // We update (or not) the value in the memory
389  assignment(goto_program, target, source_location, object, new_value_expr);
390 
391  // We update the flags of the buffer
392  // if buff0 used and mine, then it is no more used, as we flushed the last
393  // write and -ws-> imposes not to have other writes in the buffer
394  assignment(
395  goto_program,
396  target,
397  source_location,
398  vars.w_buff0_used,
399  if_exprt(
400  buff0_used_and_mine_expr,
401  false_exprt(),
402  buff0_used_expr));
403 
404  // buff1 used and mine & not buff0 used and mine, then it no more used
405  // if buff0 is used and mine, then, by ws, buff1 is no more used
406  // otherwise, remains as it is
407  const exprt buff0_or_buff1_used_and_mine_expr=
408  or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
409 
410  assignment(
411  goto_program,
412  target,
413  source_location,
414  vars.w_buff1_used,
415  if_exprt(
416  buff0_or_buff1_used_and_mine_expr,
417  false_exprt(),
418  buff1_used_expr));
419 
420  // We update the ownerships
421  // if buff0 mine and used, flushed, so belongs to nobody
422  const exprt buff0_thd_expr=
423  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
424 
425  assignment(
426  goto_program,
427  target,
428  source_location,
429  vars.r_buff0_thds[current_thread],
430  if_exprt(buff0_used_and_mine_expr, false_exprt(), buff0_thd_expr));
431 
432  // if buff1 used and mine, or if buff0 used and mine, then buff1 flushed and
433  // doesn't belong to anybody
434  const exprt buff1_thd_expr=
435  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
436 
437  assignment(
438  goto_program,
439  target,
440  source_location,
441  vars.r_buff1_thds[current_thread],
442  if_exprt(
443  buff0_or_buff1_used_and_mine_expr,
444  false_exprt(),
445  buff1_thd_expr));
446 }
447 
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(target->function, "0");
467  irep_idt choice2=choice(target->function, "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(target->function, "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  Forall_goto_functions(f_it, goto_functions)
1030  {
1031 #ifdef LOCAL_MAY
1032  local_may_aliast local_may(f_it->second);
1033 #endif
1034 
1035  Forall_goto_program_instructions(i_it, f_it->second.body)
1036  {
1037  rw_set_loct rw_set(ns, value_sets, i_it
1038 #ifdef LOCAL_MAY
1039  , local_may
1040 #endif
1041  ); // NOLINT(whitespace/parens)
1042  forall_rw_set_w_entries(w_it, rw_set)
1043  forall_rw_set_r_entries(r_it, rw_set)
1044  {
1045  message.debug() <<"debug: "<<id2string(w_it->second.object)
1046  <<" reads from "<<id2string(r_it->second.object)
1047  <<messaget::eom;
1048  if(is_buffered_in_general(r_it->second.symbol_expr, true))
1049  // shouldn't it be true? false => overapprox
1050  affected_by_delay_set.insert(w_it->second.object);
1051  }
1052  }
1053  }
1054 }
1055 
1058  value_setst &value_sets,
1059  const irep_idt &function,
1060  memory_modelt model)
1061 {
1062  shared_buffers.message.debug() << "visit function "<< function
1063  << messaget::eom;
1064  if(function == INITIALIZE_FUNCTION)
1065  return;
1066 
1068  goto_programt &goto_program=goto_functions.function_map[function].body;
1069 
1070 #ifdef LOCAL_MAY
1071  local_may_aliast local_may(goto_functions.function_map[function]);
1072 #endif
1073 
1074  Forall_goto_program_instructions(i_it, goto_program)
1075  {
1076  goto_programt::instructiont &instruction=*i_it;
1077 
1078  shared_buffers.message.debug() << "instruction "<<instruction.type
1079  << messaget::eom;
1080 
1081  /* thread marking */
1082  if(instruction.is_start_thread())
1083  {
1087  }
1088  else if(instruction.is_end_thread())
1090 
1091  if(instruction.is_assign())
1092  {
1093  try
1094  {
1095  rw_set_loct rw_set(ns, value_sets, i_it
1096 #ifdef LOCAL_MAY
1097  , local_may
1098 #endif
1099  ); // NOLINT(whitespace/parens)
1100 
1101  if(rw_set.empty())
1102  continue;
1103 
1104  // add all the written values (which are not instrumentations)
1105  // in a set
1106  forall_rw_set_w_entries(w_it, rw_set)
1107  if(shared_buffers.is_buffered(ns, w_it->second.symbol_expr, false))
1108  past_writes.insert(w_it->second.object);
1109 
1110  goto_programt::instructiont original_instruction;
1111  original_instruction.swap(instruction);
1112  const source_locationt &source_location=
1113  original_instruction.source_location;
1114 
1115  // ATOMIC_BEGIN: we make the whole thing atomic
1116  instruction.make_atomic_begin();
1117  instruction.source_location=source_location;
1118  i_it++;
1119 
1120  // we first perform (non-deterministically) up to 2 writes for
1121  // stuff that is potentially read
1122  forall_rw_set_r_entries(e_it, rw_set)
1123  {
1124  // flush read -- do nothing in this implementation
1126  goto_program, i_it, source_location, e_it->second.object);
1127 
1128  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, false))
1130  goto_program, i_it, source_location, e_it->second.object,
1132  (model==TSO || model==PSO || model==RMO));
1133  }
1134 
1135  // Now perform the write(s).
1136  forall_rw_set_w_entries(e_it, rw_set)
1137  {
1138  // if one of the previous read was to buffer, then delays the read
1139  if(model==RMO || model==Power)
1140  {
1141  forall_rw_set_r_entries(r_it, rw_set)
1142  if(shared_buffers.is_buffered(ns, r_it->second.symbol_expr, true))
1143  {
1145  goto_program, i_it, source_location, r_it->second.object,
1146  e_it->second.object);
1147  }
1148  }
1149 
1150  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, true))
1151  {
1153  goto_program, i_it, source_location,
1154  e_it->second.object, original_instruction,
1155  current_thread);
1156  }
1157  else
1158  {
1159  // unbuffered
1160  if(model==RMO || model==Power)
1161  {
1162  forall_rw_set_r_entries(r_it, rw_set)
1164  r_it->second.object)!=
1166  {
1167  shared_buffers.message.debug() << "second: "
1168  << r_it->second.object << messaget::eom;
1169  const varst &vars=(shared_buffers)(r_it->second.object);
1170 
1171  shared_buffers.message.debug() << "writer "
1172  <<e_it->second.object
1173  <<" reads "<<r_it->second.object<< messaget::eom;
1174 
1175  // TO FIX: how to deal with rhs including calls?
1176  // if a read is delayed, use its alias instead of itself
1177  // -- or not
1178  symbol_exprt to_replace_expr=symbol_exprt(
1179  r_it->second.object, vars.type);
1180  symbol_exprt new_read_expr=symbol_exprt(
1181  vars.read_delayed_var,
1182  pointer_type(vars.type));
1183  symbol_exprt read_delayed_expr=symbol_exprt(
1184  vars.read_delayed, bool_typet());
1185 
1186  // One extra non-deterministic choice needed
1187  irep_idt choice1=shared_buffers.choice(
1188  instruction.function, "1");
1189  const symbol_exprt choice1_expr=symbol_exprt(choice1,
1190  bool_typet());
1191  const exprt nondet_bool_expr =
1192  side_effect_expr_nondett(bool_typet(), source_location);
1193 
1194  // throw Boolean dice
1196  goto_program,
1197  i_it,
1198  source_location,
1199  choice1,
1200  nondet_bool_expr);
1201 
1202  const if_exprt rhs(
1203  read_delayed_expr,
1204  if_exprt(
1205  choice1_expr,
1206  dereference_exprt(new_read_expr, vars.type),
1207  to_replace_expr),
1208  to_replace_expr); // original_instruction.code.op1());
1209 
1211  goto_program, i_it, source_location,
1212  r_it->second.object, rhs);
1213  }
1214  }
1215 
1216  // normal assignment
1218  goto_program, i_it, source_location,
1219  e_it->second.object, original_instruction.code.op1());
1220  }
1221  }
1222 
1223  // if last writes was flushed to make the lhs reads the buffer but
1224  // without affecting the memory, restore the previous memory value
1225  // (buffer flush delay)
1226  forall_rw_set_r_entries(e_it, rw_set)
1227  if(shared_buffers.is_buffered(ns, e_it->second.symbol_expr, false))
1228  {
1229  shared_buffers.message.debug() << "flush restore: "
1230  << e_it->second.object << messaget::eom;
1231  const varst vars= (shared_buffers)(e_it->second.object);
1232  const exprt delayed_expr=symbol_exprt(vars.flush_delayed,
1233  bool_typet());
1234  const symbol_exprt mem_value_expr=symbol_exprt(vars.mem_tmp,
1235  vars.type);
1236  const exprt cond_expr=if_exprt(delayed_expr, mem_value_expr,
1237  e_it->second.symbol_expr);
1238 
1240  goto_program, i_it, source_location,
1241  e_it->second.object, cond_expr);
1243  goto_program, i_it, source_location,
1244  vars.flush_delayed, false_exprt());
1245  }
1246 
1247  // ATOMIC_END
1248  i_it=goto_program.insert_before(i_it);
1249  i_it->make_atomic_end();
1250  i_it->source_location=source_location;
1251  i_it++;
1252 
1253  i_it--; // the for loop already counts us up
1254  }
1255  catch (...)
1256  {
1257  shared_buffers.message.warning() << "Identifier not found"
1258  << messaget::eom;
1259  }
1260  }
1261  else if(is_fence(instruction, ns) ||
1262  (instruction.is_other() &&
1263  instruction.code.get_statement()==ID_fence &&
1264  (instruction.code.get_bool("WRfence") ||
1265  instruction.code.get_bool("WWfence") ||
1266  instruction.code.get_bool("RWfence") ||
1267  instruction.code.get_bool("RRfence"))))
1268  {
1269  goto_programt::instructiont original_instruction;
1270  original_instruction.swap(instruction);
1271  const source_locationt &source_location=
1272  original_instruction.source_location;
1273 
1274  // ATOMIC_BEGIN
1275  instruction.make_atomic_begin();
1276  instruction.source_location=source_location;
1277  i_it++;
1278 
1279  // does it for all the previous statements
1280  for(std::set<irep_idt>::iterator s_it=past_writes.begin();
1281  s_it!=past_writes.end(); s_it++)
1282  {
1284  goto_program, i_it, source_location, *s_it,
1285  current_thread);
1286  }
1287 
1288  // ATOMIC_END
1289  i_it=goto_program.insert_before(i_it);
1290  i_it->make_atomic_end();
1291  i_it->source_location=source_location;
1292  i_it++;
1293 
1294  i_it--; // the for loop already counts us up
1295  }
1296  else if(is_lwfence(instruction, ns))
1297  {
1298  // po -- remove the lwfence
1299  i_it->make_skip();
1300  }
1301  else if(instruction.is_function_call())
1302  {
1303  const exprt &fun=to_code_function_call(instruction.code).function();
1304  weak_memory(value_sets, to_symbol_expr(fun).get_identifier(), model);
1305  }
1306  }
1307 }
const irep_idt & get_statement() const
Definition: std_code.h:56
void add_initialization_code(goto_functionst &goto_functions)
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
Boolean negation.
Definition: std_expr.h:3308
messaget & message
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:65
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
Boolean OR.
Definition: std_expr.h:2531
#define CPROVER_PREFIX
bool empty() const
Definition: rw_set.h:72
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
Definition: wmm.h:23
const irep_idt & get_identifier() const
Definition: std_expr.h:176
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:111
The null pointer constant.
Definition: std_expr.h:4471
literalt pos(literalt a)
Definition: literal.h:193
exprt value
Initial value of symbol.
Definition: symbol.h:34
The trinary if-then-else operator.
Definition: std_expr.h:3427
Definition: wmm.h:22
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
void add_initialization(goto_programt &goto_program)
The Boolean type.
Definition: std_types.h:28
irep_idt choice(const irep_idt &function, const std::string &suffix)
Symbol table entry.
Definition: symbol.h:27
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
std::string unique()
returns a unique id (for fresh variables)
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...
bool is_static_lifetime
Definition: symbol.h:65
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
mstreamt & warning() const
Definition: message.h:391
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
Equality.
Definition: std_expr.h:1484
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std::set< irep_idt > instrumentations
goto_functionst & goto_functions
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:107
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
The Boolean constant true.
Definition: std_expr.h:4443
memory_modelt
Definition: wmm.h:17
instructionst::iterator targett
Definition: goto_program.h:414
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
std::set< irep_idt > past_writes
Operator to dereference a pointer.
Definition: std_expr.h:3355
#define INITIALIZE_FUNCTION
Boolean AND.
Definition: std_expr.h:2409
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
exprt & op1()
Definition: expr.h:87
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
shared_bufferst & shared_buffers
Definition: wmm.h:21
std::vector< irep_idt > r_buff1_thds
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const varst & operator()(const irep_idt &object)
instruments the variable
int main()
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irep_idt add_fresh_var(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
The Boolean constant false.
Definition: std_expr.h:4452
std::multimap< irep_idt, source_locationt > cycles_loc
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
std::vector< irep_idt > r_buff0_thds
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:548
static eomt eom
Definition: message.h:284
typet type
Type of symbol.
Definition: symbol.h:31
void nondet_flush(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
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
exprt & function()
Definition: std_code.h:1099
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
Fences for instrumentation.
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
Definition: wmm.h:20
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)
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
std::set< irep_idt > cycles
void make_nil()
Definition: irep.h:315
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
class symbol_tablet & symbol_table
std::set< irep_idt > affected_by_delay_set
mstreamt & debug() const
Definition: message.h:416
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)
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36
Race Detection for Threaded Goto Programs.