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 =
468  side_effect_expr_nondett(bool_typet(), source_location);
469 
470  // throw Boolean dice
471  assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
472  assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
473 
474  // Buffers and memory
475  const symbol_exprt buff0_expr=symbol_exprt(vars.w_buff0, vars.type);
476  const symbol_exprt buff1_expr=symbol_exprt(vars.w_buff1, vars.type);
477  const exprt lhs=symbol_exprt(object, vars.type);
478 
479  // Buffer uses
480  const symbol_exprt buff0_used_expr=symbol_exprt(vars.w_buff0_used,
481  bool_typet());
482  const symbol_exprt buff1_used_expr=symbol_exprt(vars.w_buff1_used,
483  bool_typet());
484 
485  // Buffer ownerships
486  const symbol_exprt buff0_thd_expr=
487  symbol_exprt(vars.r_buff0_thds[current_thread], bool_typet());
488  const symbol_exprt buff1_thd_expr=
489  symbol_exprt(vars.r_buff1_thds[current_thread], bool_typet());
490 
491 
492  // Will the write be directly flushed, or is it just a read?
493  assignment(
494  goto_program, target, source_location, vars.flush_delayed, delay_expr);
495  assignment(goto_program, target, source_location, vars.mem_tmp, lhs);
496 
497  // for POWER, only instrumented reads can read from the buffers of other
498  // threads
499  bool instrumented=false;
500 
501  if(!tso_pso_rmo)
502  {
503  if(cycles.find(object)!=cycles.end())
504  {
505  typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
506  std::pair<m_itt, m_itt> ran=cycles_loc.equal_range(object);
507  for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
508  if(ran_it->second==source_location)
509  {
510  instrumented=true;
511  break;
512  }
513  }
514  }
515 
516  // TSO/PSO/RMO
517  if(tso_pso_rmo || !instrumented)
518  {
519  // 7 cases
520 
521  // (1) (3) (4)
522  // if buff0 unused
523  // or buff0 not mine and buff1 unused
524  // or buff0 not mine and buff1 not mine
525  // -> read from memory (and does not modify the buffer in any aspect)
526  const exprt cond_134_expr=
527  or_exprt(
528  not_exprt(buff0_used_expr),
529  or_exprt(
530  and_exprt(
531  not_exprt(buff0_thd_expr),
532  not_exprt(buff1_used_expr)),
533  and_exprt(
534  not_exprt(buff0_thd_expr),
535  not_exprt(buff1_thd_expr))));
536  const exprt val_134_expr=lhs;
537  const exprt buff0_used_134_expr=buff0_used_expr;
538  const exprt buff1_used_134_expr=buff1_used_expr;
539  const exprt buff0_134_expr=buff0_expr;
540  const exprt buff1_134_expr=buff1_expr;
541  const exprt buff0_thd_134_expr=buff0_thd_expr;
542  const exprt buff1_thd_134_expr=buff1_thd_expr;
543 
544  // (2) (6) (7)
545  // if buff0 used and mine
546  // -> read from buff0
547  const exprt cond_267_expr=and_exprt(buff0_used_expr, buff0_thd_expr);
548  const exprt val_267_expr=buff0_expr;
549  const exprt buff0_used_267_expr=false_exprt();
550  const exprt buff1_used_267_expr=false_exprt();
551  const exprt buff0_267_expr=buff0_expr;
552  const exprt buff1_267_expr=buff1_expr;
553  const exprt buff0_thd_267_expr=false_exprt();
554  const exprt buff1_thd_267_expr=false_exprt();
555 
556  // (5)
557  // buff0 and buff1 are used, buff0 is not mine, buff1 is mine
558  // -> read from buff1
559  const exprt cond_5_expr=
560  and_exprt(
561  buff0_used_expr,
562  and_exprt(
563  buff1_used_expr,
564  and_exprt(not_exprt(buff0_thd_expr), buff1_thd_expr)));
565  const exprt val_5_expr=buff1_expr;
566  const exprt buff0_used_5_expr=buff0_used_expr;
567  const exprt buff1_used_5_expr=false_exprt();
568  const exprt buff0_5_expr=buff0_expr;
569  const exprt buff1_5_expr=buff1_expr;
570  const exprt buff0_thd_5_expr=buff0_thd_expr;
571  const exprt buff1_thd_5_expr=false_exprt();
572 
573  // Updates
574  // memory
575  assignment(
576  goto_program,
577  target,
578  source_location,
579  object,
580  if_exprt(
581  cond_134_expr,
582  val_134_expr,
583  if_exprt(
584  cond_267_expr,
585  val_267_expr,
586  val_5_expr)));
587  // buff0
588  assignment(
589  goto_program,
590  target,
591  source_location,
592  vars.w_buff0,
593  if_exprt(
594  delay_expr,
595  buff0_expr,
596  if_exprt(
597  cond_134_expr,
598  buff0_134_expr,
599  if_exprt(
600  cond_267_expr,
601  buff0_267_expr,
602  buff0_5_expr))));
603  // buff1
604  assignment(
605  goto_program,
606  target,
607  source_location,
608  vars.w_buff1,
609  if_exprt(
610  delay_expr,
611  buff1_expr,
612  if_exprt(
613  cond_134_expr,
614  buff1_134_expr,
615  if_exprt(
616  cond_267_expr,
617  buff1_267_expr,
618  buff1_5_expr))));
619  // buff0_used
620  assignment(
621  goto_program,
622  target,
623  source_location,
624  vars.w_buff0_used,
625  if_exprt(
626  delay_expr,
627  buff0_used_expr,
628  if_exprt(
629  cond_134_expr,
630  buff0_used_134_expr,
631  if_exprt(
632  cond_267_expr,
633  buff0_used_267_expr,
634  buff0_used_5_expr))));
635  // buff1_used
636  assignment(
637  goto_program,
638  target,
639  source_location,
640  vars.w_buff1_used,
641  if_exprt(
642  delay_expr,
643  buff1_used_expr,
644  if_exprt(
645  cond_134_expr,
646  buff1_used_134_expr,
647  if_exprt(
648  cond_267_expr,
649  buff1_used_267_expr,
650  buff1_used_5_expr))));
651  // buff0_thd
652  assignment(
653  goto_program,
654  target,
655  source_location,
656  vars.r_buff0_thds[current_thread],
657  if_exprt(
658  delay_expr,
659  buff0_thd_expr,
660  if_exprt(
661  cond_134_expr,
662  buff0_thd_134_expr,
663  if_exprt(
664  cond_267_expr,
665  buff0_thd_267_expr,
666  buff0_thd_5_expr))));
667  // buff1_thd
668  assignment(
669  goto_program,
670  target,
671  source_location,
672  vars.r_buff1_thds[current_thread], if_exprt(
673  delay_expr,
674  buff1_thd_expr,
675  if_exprt(
676  cond_134_expr,
677  buff1_thd_134_expr,
678  if_exprt(
679  cond_267_expr,
680  buff1_thd_267_expr,
681  buff1_thd_5_expr))));
682  }
683  // POWER
684  else
685  {
686  // a thread can read the other threads' buffers
687 
688  // One extra non-deterministic choice needed
689  irep_idt choice1=choice(target->function, "1");
690  const symbol_exprt choice1_expr=symbol_exprt(choice1, bool_typet());
691 
692  // throw Boolean dice
693  assignment(
694  goto_program, target, source_location, choice1, nondet_bool_expr);
695 
696  // 7 cases
697 
698  // (1)
699  // if buff0 unused
700  // -> read from memory (and does not modify the buffer in any aspect)
701  const exprt cond_1_expr=not_exprt(buff0_used_expr);
702  const exprt val_1_expr=lhs;
703  const exprt buff0_used_1_expr=buff0_used_expr;
704  const exprt buff1_used_1_expr=buff1_used_expr;
705  const exprt buff0_1_expr=buff0_expr;
706  const exprt buff1_1_expr=buff1_expr;
707  const exprt buff0_thd_1_expr=buff0_thd_expr;
708  const exprt buff1_thd_1_expr=buff1_thd_expr;
709 
710  // (2) (6) (7)
711  // if buff0 used and mine
712  // -> read from buff0
713  const exprt cond_267_expr=
714  and_exprt(buff0_used_expr, buff0_thd_expr);
715  const exprt val_267_expr=buff0_expr;
716  const exprt buff0_used_267_expr=false_exprt();
717  const exprt buff1_used_267_expr=false_exprt();
718  const exprt buff0_267_expr=buff0_expr;
719  const exprt buff1_267_expr=buff1_expr;
720  const exprt buff0_thd_267_expr=false_exprt();
721  const exprt buff1_thd_267_expr=false_exprt();
722 
723  // (3)
724  // if buff0 used and not mine, and buff1 not used
725  // -> read from buff0 or memory
726  const exprt cond_3_expr=
727  and_exprt(
728  buff0_used_expr,
729  and_exprt(
730  not_exprt(buff0_thd_expr),
731  not_exprt(buff1_used_expr)));
732  const exprt val_3_expr=if_exprt(choice0_expr, buff0_expr, lhs);
733  const exprt buff0_used_3_expr=choice0_expr;
734  const exprt buff1_used_3_expr=false_exprt();
735  const exprt buff0_3_expr=buff0_expr;
736  const exprt buff1_3_expr=buff1_expr;
737  const exprt buff0_thd_3_expr=false_exprt();
738  const exprt buff1_thd_3_expr=false_exprt();
739 
740  // (4)
741  // buff0 and buff1 are both used, and both not mine
742  // -> read from memory or buff0 or buff1
743  const exprt cond_4_expr=
744  and_exprt(
745  and_exprt(buff0_used_expr, not_exprt(buff1_thd_expr)),
746  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
747  const exprt val_4_expr=
748  if_exprt(
749  choice0_expr,
750  lhs,
751  if_exprt(
752  choice1_expr,
753  buff0_expr,
754  buff1_expr));
755  const exprt buff0_used_4_expr=
756  or_exprt(choice0_expr, not_exprt(choice1_expr));
757  const exprt buff1_used_4_expr=choice0_expr;
758  const exprt buff0_4_expr=buff0_expr;
759  const exprt buff1_4_expr=buff1_expr;
760  const exprt buff0_thd_4_expr=buff0_thd_expr;
761  const exprt buff1_thd_4_expr=
762  if_exprt(choice0_expr, buff1_thd_expr, false_exprt());
763 
764  // (5)
765  // buff0 and buff1 are both used, and buff0 not mine, and buff1 mine
766  // -> read buff1 or buff0
767  const exprt cond_5_expr=
768  and_exprt(
769  and_exprt(buff0_used_expr, buff1_thd_expr),
770  and_exprt(buff1_used_expr, not_exprt(buff0_thd_expr)));
771  const exprt val_5_expr=
772  if_exprt(
773  choice0_expr,
774  buff1_expr,
775  buff0_expr);
776  const exprt buff0_used_5_expr=choice0_expr;
777  const exprt buff1_used_5_expr=false_exprt();
778  const exprt buff0_5_expr=buff0_expr;
779  const exprt buff1_5_expr=buff1_expr;
780  const exprt buff0_thd_5_expr=false_exprt();
781  const exprt buff1_thd_5_expr=false_exprt();
782 
783  // Updates
784  // memory
785  assignment(
786  goto_program,
787  target,
788  source_location,
789  object,
790  if_exprt(
791  cond_1_expr,
792  val_1_expr,
793  if_exprt(
794  cond_267_expr,
795  val_267_expr,
796  if_exprt(
797  cond_4_expr,
798  val_4_expr,
799  if_exprt(
800  cond_5_expr,
801  val_5_expr,
802  val_3_expr)))));
803  // buff0
804  assignment(
805  goto_program,
806  target,
807  source_location,
808  vars.w_buff0,
809  if_exprt(
810  delay_expr,
811  buff0_expr,
812  if_exprt(
813  cond_1_expr,
814  buff0_1_expr,
815  if_exprt(
816  cond_267_expr,
817  buff0_267_expr,
818  if_exprt(
819  cond_4_expr,
820  buff0_4_expr,
821  if_exprt(
822  cond_5_expr,
823  buff0_5_expr,
824  buff0_3_expr))))));
825  // buff1
826  assignment(
827  goto_program,
828  target,
829  source_location,
830  vars.w_buff1,
831  if_exprt(
832  delay_expr,
833  buff1_expr,
834  if_exprt(
835  cond_1_expr,
836  buff1_1_expr,
837  if_exprt(
838  cond_267_expr,
839  buff1_267_expr,
840  if_exprt(
841  cond_4_expr,
842  buff1_4_expr,
843  if_exprt(
844  cond_5_expr,
845  buff1_5_expr,
846  buff1_3_expr))))));
847  // buff0_used
848  assignment(
849  goto_program,
850  target,
851  source_location,
852  vars.w_buff0_used,
853  if_exprt(
854  delay_expr,
855  buff0_used_expr,
856  if_exprt(
857  cond_1_expr,
858  buff0_used_1_expr,
859  if_exprt(
860  cond_267_expr,
861  buff0_used_267_expr,
862  if_exprt(
863  cond_4_expr,
864  buff0_used_4_expr,
865  if_exprt(
866  cond_5_expr,
867  buff0_used_5_expr,
868  buff0_used_3_expr))))));
869  // buff1_used
870  assignment(
871  goto_program,
872  target,
873  source_location,
874  vars.w_buff1_used,
875  if_exprt(
876  delay_expr,
877  buff1_used_expr,
878  if_exprt(
879  cond_1_expr,
880  buff1_used_1_expr,
881  if_exprt(
882  cond_267_expr,
883  buff1_used_267_expr,
884  if_exprt(
885  cond_4_expr,
886  buff1_used_4_expr,
887  if_exprt(
888  cond_5_expr,
889  buff1_used_5_expr,
890  buff1_used_3_expr))))));
891  // buff0_thd
892  assignment(
893  goto_program,
894  target,
895  source_location,
896  vars.r_buff0_thds[current_thread],
897  if_exprt(
898  delay_expr,
899  buff0_thd_expr,
900  if_exprt(
901  cond_1_expr,
902  buff0_thd_1_expr,
903  if_exprt(
904  cond_267_expr,
905  buff0_thd_267_expr,
906  if_exprt(
907  cond_4_expr,
908  buff0_thd_4_expr,
909  if_exprt(
910  cond_5_expr,
911  buff0_thd_5_expr,
912  buff0_thd_3_expr))))));
913  // buff1_thd
914  assignment(
915  goto_program,
916  target,
917  source_location,
918  vars.r_buff1_thds[current_thread],
919  if_exprt(
920  delay_expr,
921  buff1_thd_expr,
922  if_exprt(
923  cond_1_expr,
924  buff1_thd_1_expr,
925  if_exprt(
926  cond_267_expr,
927  buff1_thd_267_expr,
928  if_exprt(
929  cond_4_expr,
930  buff1_thd_4_expr,
931  if_exprt(
932  cond_5_expr,
933  buff1_thd_5_expr,
934  buff1_thd_3_expr))))));
935  }
936  }
937  catch(const std::string &s)
938  {
939  message.warning() << s << messaget::eom;
940  }
941 }
942 
944  const namespacet &ns,
945  const symbol_exprt &symbol_expr,
946  bool is_write
947  // are we asking for the variable (false), or for the variable and
948  // the source_location in the code (true)
949 )
950 {
951  const irep_idt &identifier=symbol_expr.get_identifier();
952 
953  if(identifier==CPROVER_PREFIX "alloc" ||
954  identifier==CPROVER_PREFIX "alloc_size" ||
955  identifier=="stdin" ||
956  identifier=="stdout" ||
957  identifier=="stderr" ||
958  identifier=="sys_nerr" ||
959  has_prefix(id2string(identifier), "__unbuffered_") ||
960  has_prefix(id2string(identifier), "__CPROVER"))
961  return false; // not buffered
962 
963  const symbolt &symbol=ns.lookup(identifier);
964 
965  if(!symbol.is_static_lifetime)
966  return false; // these are local
967 
968  if(symbol.is_thread_local)
969  return false; // these are local
970 
971  if(instrumentations.find(identifier)!=instrumentations.end())
972  return false; // these are instrumentations
973 
974  return is_buffered_in_general(symbol_expr, is_write);
975 }
976 
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(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 =
1189  side_effect_expr_nondett(bool_typet(), source_location);
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:40
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:3228
messaget & message
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:4518
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:3359
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
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
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:4486
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:3282
#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:1340
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
The boolean constant false.
Definition: std_expr.h:4497
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:404
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:878
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:315
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
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:136
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36
Race Detection for Threaded Goto Programs.