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