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