cprover
event_graph.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: graph of abstract events
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "event_graph.h"
15 
16 #include <util/message.h>
17 
18 #include <fstream>
19 
20 
21 #define NB_COLOURS 14
22 static const char *colour_map[NB_COLOURS]=
23  {"red", "blue", "black", "green", "yellow",
24  "orange", "blueviolet", "cyan", "cadetblue", "magenta", "palegreen",
25  "deeppink", "indigo", "olivedrab"};
26 #define print_colour(u) colour_map[u%NB_COLOURS]
27 
28 void event_grapht::print_rec_graph(std::ofstream &file, event_idt node_id,
29  std::set<event_idt> &visited)
30 {
31  const abstract_eventt &node=operator[](node_id);
32  file << node_id << "[label=\"" << node << ", " << node.source_location <<
33  "\"];\n";
34  visited.insert(node_id);
35 
36  for(wmm_grapht::edgest::const_iterator
37  it=po_out(node_id).begin();
38  it!=po_out(node_id).end(); ++it)
39  {
40  file << node_id << "->" << it->first << "[]\n";
41  file << "{rank=same; " << node_id << "; " << it->first << "}\n";
42  if(visited.find(it->first)==visited.end())
43  print_rec_graph(file, it->first, visited);
44  }
45 
46  for(wmm_grapht::edgest::const_iterator
47  it=com_out(node_id).begin();
48  it!=com_out(node_id).end(); ++it)
49  {
50  file << node_id << "->" << it->first << "[style=\"dotted\"]\n";
51  if(visited.find(it->first)==visited.end())
52  print_rec_graph(file, it->first, visited);
53  }
54 }
55 
57 {
58  assert(!po_order.empty());
59  std::set<event_idt> visited;
60  event_idt root=po_order.front();
61  std::ofstream file;
62  file.open("graph.dot");
63  file << "digraph G {\n";
64  file << "rankdir=LR;\n";
65  print_rec_graph(file, root, visited);
66  file << "}\n";
67 }
68 
72 void event_grapht::explore_copy_segment(std::set<event_idt> &explored,
73  event_idt begin, event_idt end) const
74 {
75  // std::cout << "explores " << begin << " against " << end << '\n';
76  if(explored.find(begin)!=explored.end())
77  return;
78 
79  explored.insert(begin);
80 
81  if(begin==end)
82  return;
83 
84  for(wmm_grapht::edgest::const_iterator it=po_out(begin).begin();
85  it!=po_out(begin).end();
86  ++it)
87  explore_copy_segment(explored, it->first, end);
88 }
89 
91 {
92  const abstract_eventt &begin_event=operator[](begin);
93  const abstract_eventt &end_event=operator[](end);
94 
95  /* not sure -- we should allow cross function cycles */
96  if(begin_event.source_location.get_file()!=end_event.source_location
97  .get_file()
98  || begin_event.source_location.get_function()!=end_event.source_location
99  .get_function())
100  return end;
101 
102  if(duplicated_bodies.find(std::make_pair(begin_event, end_event))
103  !=duplicated_bodies.end())
104  return end;
105 
106  duplicated_bodies.insert(std::make_pair(begin_event, end_event));
107 
108  message.status() << "tries to duplicate between "
109  << begin_event.source_location
110  << " and " << end_event.source_location << messaget::eom;
111  std::set<event_idt> covered;
112 
113  /* collects the nodes of the subgraph */
114  explore_copy_segment(covered, begin, end);
115 
116  if(covered.empty())
117  return end;
118 
119 // for(std::set<event_idt>::const_iterator it=covered.begin();
120 // it!=covered.end(); ++it)
121 // std::cout << "covered: " << *it << '\n';
122 
123  std::map<event_idt, event_idt> orig2copy;
124 
125  /* duplicates nodes */
126  for(std::set<event_idt>::const_iterator it=covered.begin();
127  it!=covered.end();
128  ++it)
129  {
130  const event_idt new_node=add_node();
131  operator[](new_node)(operator[](*it));
132  orig2copy[*it]=new_node;
133  }
134 
135  /* nested loops -- replicates the po_s back-edges */
136  // actually not necessary, as they have been treated before
137  // (working on back-edges...)
138 
139  /* replicates the po_s forward-edges -- O(#E^2) */
140  for(std::set<event_idt>::const_iterator it_i=covered.begin();
141  it_i!=covered.end();
142  ++it_i)
143  {
144  for(std::set<event_idt>::const_iterator it_j=covered.begin();
145  it_j!=covered.end();
146  ++it_j)
147  {
148  /* skips potential back-edges */
149  if(*it_j >= *it_i)
150  continue;
151 
152  if(has_po_edge(*it_j, *it_i))
153  add_po_edge(orig2copy[*it_j], orig2copy[*it_i]);
154  }
155  }
156 
157  /* appends the copy to the original, and returns the end of the copy */
158  add_po_edge(end, orig2copy[begin]);
159 
160  // TODO: to move to goto2graph, after po_s construction
161  /* replicates the cmp-edges -- O(#E x #G) */
162  for(std::set<event_idt>::const_iterator it_i=covered.begin();
163  it_i!=covered.end();
164  ++it_i)
165  {
166  for(event_idt it_j=0;
167  it_j<size();
168  ++it_j)
169  {
170  /* skips potential back-edges */
171  if(it_j >= *it_i)
172  continue;
173 
174  if(has_com_edge(it_j, *it_i))
175  {
176  add_com_edge(it_j, orig2copy[*it_i]);
177  add_com_edge(orig2copy[*it_i], it_j);
178  }
179  }
180  }
181  // end
182 
183  return orig2copy[end];
184 }
185 
187  const_iterator s_it,
188  const abstract_eventt &first,
189  const abstract_eventt &second) const
190 {
191  bool AC=false;
192  const_iterator AC_it=s_it;
193  ++AC_it;
194  for(; AC_it!=end(); ++AC_it)
195  {
196  const abstract_eventt &AC_evt=egraph[*AC_it];
198  {
199  AC=true;
200  break;
201  }
202  if(AC_evt.thread!=second.thread)
203  break;
204  }
205 
206  if(AC)
207  return true;
208 
209  if(AC_it==end() && egraph[front()].thread==second.thread)
210  {
211  for(AC_it=begin(); ; ++AC_it)
212  {
213  const abstract_eventt &AC_evt=egraph[*AC_it];
215  {
216  AC=true;
217  break;
218  }
219  if(AC_evt==first || AC_evt.thread!=second.thread)
220  break;
221  }
222  }
223 
224  return AC;
225 }
226 
228  const_iterator it,
229  const abstract_eventt &first,
230  const abstract_eventt &second) const
231 {
232  bool BC=false;
233  /* no fence before the first element? (BC) */
234  const_iterator BC_it;
235  if(it==begin())
236  {
237  BC_it=end();
238  --BC_it;
239  }
240  else
241  {
242  BC_it=it;
243  --BC_it;
244  }
245  for(; BC_it!=begin(); --BC_it)
246  {
247  const abstract_eventt &BC_evt=egraph[*BC_it];
249  {
250  BC=true;
251  break;
252  }
253  if(BC_evt.thread!=first.thread)
254  break;
255  }
256 
257  if(BC)
258  return true;
259 
260  if(BC_it==begin() && egraph[back()].thread==first.thread)
261  {
262  BC_it=end();
263  --BC_it;
264  for(; ; --BC_it)
265  {
266  const abstract_eventt &BC_evt=egraph[*BC_it];
268  {
269  BC=true;
270  break;
271  }
272  if(BC_evt==second || BC_evt.thread!=first.thread)
273  break;
274  }
275  }
276 
277  return BC;
278 }
279 
281 {
282  egraph.message.debug() << "cycle is safe?" << messaget::eom;
283  bool unsafe_met=false;
284 
285  /* critical cycles contain at least 4 events */
286  if(size()<4)
287  return false;
288 
289  /* critical cycles contain at least 2 threads */
290  unsigned thread=egraph[*begin()].thread;
291  const_iterator th_it;
292  for(th_it=begin();
293  th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
294  thread=egraph[*th_it].thread;
295  if(th_it==end())
296  return false;
297 
298  /* selects the first element of the pair */
299  const_iterator it=begin();
300  const_iterator next=it;
301  ++next;
302  for(; it!=end() && next!=end(); ++next, ++it)
303  {
304  const abstract_eventt &it_evt=egraph[*it];
305  const abstract_eventt &next_evt=egraph[*next];
306 
307  /* strong fence -- this pair is safe */
309  continue;
310 
312  continue;
313 
314  /* first element is a weak fence */
316  continue;
317 
318  /* selects the next event which is not a weak fence */
319  const_iterator s_it=next;
320 
321  for(; s_it!=end() &&
322  egraph[*s_it].operation==abstract_eventt::operationt::Lwfence;
323  ++s_it)
324  {
325  }
326 
327  if(s_it==end())
328  continue;
329 
330  const abstract_eventt &s_evt=egraph[*s_it];
331 
333  continue;
334 
335  /* if the whole cycle has been explored */
336  if(it==s_it)
337  continue;
338 
339  const abstract_eventt &first=it_evt;
340  const abstract_eventt &second=s_evt;
341  const data_dpt &data_dp=egraph.map_data_dp[first.thread];
342 
343  /* if data dp between linking the pair, safe */
344  if(first.thread==second.thread && data_dp.dp(first, second))
345  continue;
346 
347  /* AC and BC conditions */
348  if(first.thread!=second.thread && model==Power)
349  {
350  if(check_AC(s_it, first, second))
351  continue;
352 
353  if(check_BC(it, first, second))
354  continue;
355  }
356 
357  const_iterator n_it=it;
358  ++n_it;
359  if(s_it==n_it)
360  {
361  /* there is no lwfence between the pair */
362  if(first.unsafe_pair(second, model)
363  && (first.thread!=second.thread || egraph.are_po_ordered(*it, *s_it)))
364  {
365  const_iterator before_first;
366  const_iterator after_second;
367 
368  if(it==begin())
369  before_first=end();
370  else
371  before_first=it;
372  --before_first;
373 
374  n_it=s_it;
375  ++n_it;
376  if(n_it==end())
377  after_second=begin();
378  else
379  after_second=s_it;
380 
381  if(first.variable==second.variable
382  && first.thread==second.thread
383  && egraph[*before_first].thread!=first.thread
384  && egraph[*after_second].thread!=second.thread)
385  {
386  /* not unsafe */
387  }
388  else
389  {
390  if(fast)
391  return true;
392  else
393  {
394  const delayt delay(*it, *s_it, (first.thread==second.thread));
395  unsafe_pairs.insert(delay);
396  unsafe_met=true;
397  }
398  }
399  }
400  }
401  else
402  {
403  /* one (or more) lwfence between the pair */
404  if(first.unsafe_pair_lwfence(second, model)
405  && (first.thread!=second.thread || egraph.are_po_ordered(*it, *s_it)))
406  {
407  const_iterator before_first;
408  const_iterator after_second;
409 
410  if(it==begin())
411  before_first=end();
412  else
413  before_first=it;
414  --before_first;
415 
416  n_it=s_it;
417  ++n_it;
418  if(n_it==end())
419  after_second=begin();
420  else
421  after_second=s_it;
422 
423  if(first.variable==second.variable
424  && first.thread==second.thread
425  && egraph[*before_first].thread!=first.thread
426  && egraph[*after_second].thread!=second.thread)
427  {
428  /* not unsafe */
429  }
430  else
431  {
432  if(fast)
433  return true;
434  else
435  {
436  const delayt delay(*it, *s_it, (first.thread==second.thread));
437  unsafe_pairs.insert(delay);
438  unsafe_met=true;
439  }
440  }
441  }
442  }
443  }
444 
445  /* strong fence -- this pair is safe */
446  if(egraph[back()].operation==abstract_eventt::operationt::Fence
447  || egraph[front()].operation==abstract_eventt::operationt::Fence)
448  return unsafe_met;
449 
450  /* first element is a weak fence */
451  if(egraph[back()].operation==abstract_eventt::operationt::Lwfence)
452  return unsafe_met;
453 
454  /* selects the next event which is not a weak fence */
455  const_iterator s_it;
456  for(s_it=begin();
457  s_it!=end() &&
458  egraph[*s_it].operation==abstract_eventt::operationt::Lwfence;
459  s_it++)
460  {
461  }
462 
463  /* if the whole cycle has been explored */
464  if(s_it==end())
465  return unsafe_met;
466 
467  if(egraph[*s_it].operation==abstract_eventt::operationt::Fence)
468  return unsafe_met;
469 
470  const abstract_eventt &first=egraph[back()];
471  const abstract_eventt &second=egraph[*s_it];
472 
473  const data_dpt &data_dp=egraph.map_data_dp[first.thread];
474 
475  /* if data dp between linking the pair, safe */
476  if(first.thread==second.thread && data_dp.dp(first, second))
477  return unsafe_met;
478 
479  /* AC and BC conditions */
480  if(first.thread!=second.thread && model==Power)
481  {
482  if(check_AC(s_it, first, second))
483  return unsafe_met;
484 
485  if(check_BC(begin(), first, second))
486  return unsafe_met;
487  }
488 
489  if(s_it==begin())
490  {
491  /* no lwfence between the pair */
492  if(first.unsafe_pair(second, model)
493  && (first.thread!=second.thread || egraph.are_po_ordered(back(), *s_it)))
494  {
495  std::list<event_idt>::const_iterator before_first;
496  std::list<event_idt>::const_iterator after_second;
497 
498  before_first=end();
499  --before_first;
500  --before_first;
501 
502  after_second=s_it;
503  ++after_second;
504 
505  if(first.variable==second.variable
506  && first.thread==second.thread
507  && egraph[*before_first].thread!=first.thread
508  && egraph[*after_second].thread!=second.thread)
509  {
510  /* not unsafe */
511  }
512  else
513  {
514  if(!fast)
515  {
516  const delayt delay(back(), *s_it, (first.thread==second.thread));
517  unsafe_pairs.insert(delay);
518  }
519  return true;
520  }
521  }
522  }
523  else
524  {
525  /* one (or more) lwfence between the pair */
526  if(first.unsafe_pair_lwfence(second, model)
527  && (first.thread!=second.thread || egraph.are_po_ordered(back(), *s_it)))
528  {
529  std::list<event_idt>::const_iterator before_first;
530  std::list<event_idt>::const_iterator after_second;
531 
532  before_first=end();
533  --before_first;
534  --before_first;
535 
536  after_second=s_it;
537  ++after_second;
538 
539  if(first.variable==second.variable
540  && first.thread==second.thread
541  && egraph[*before_first].thread!=first.thread
542  && egraph[*after_second].thread!=second.thread)
543  {
544  /* not unsafe */
545  }
546  else
547  {
548  if(!fast)
549  {
550  const delayt delay(back(), *s_it, (first.thread==second.thread));
551  unsafe_pairs.insert(delay);
552  }
553  return true;
554  }
555  }
556  }
557 
558  return unsafe_met;
559 }
560 
563  memory_modelt model,
564  bool fast)
565 {
566  egraph.message.debug() << "cycle is safe?" << messaget::eom;
567  bool unsafe_met=false;
568  unsigned char fences_met=0;
569 
570  /* critical cycles contain at least 4 events */
571  if(size()<4)
572  return false;
573 
574  /* critical cycles contain at least 2 threads */
575  unsigned thread=egraph[*begin()].thread;
576  const_iterator th_it;
577  for(th_it=begin();
578  th_it!=end() && thread==egraph[*th_it].thread; ++th_it)
579  thread=egraph[*th_it].thread;
580  if(th_it==end())
581  return false;
582 
583  /* selects the first element of the pair */
584  for(const_iterator it=begin(); it!=end() && ++it!=end(); it++)
585  {
586  --it;
587  fences_met=0;
588 
589  /* fence -- this pair is safe */
590  if(egraph[*it].operation==abstract_eventt::operationt::ASMfence)
591  continue;
592 
593  if(egraph[*(++it)].operation==abstract_eventt::operationt::ASMfence)
594  {
595  --it;
596  continue;
597  }
598 
599  --it;
600 
601  /* selects the next event which is not a weak fence */
602  const_iterator s_it=++it;
603  --it;
604 
605  for(;
606  s_it!=end() &&
607  egraph[*s_it].operation==abstract_eventt::operationt::ASMfence;
608  s_it++)
609  fences_met |= egraph[*s_it].fence_value();
610 
611  if(s_it==end())
612  continue;
613 
614  if(egraph[*s_it].operation==abstract_eventt::operationt::ASMfence)
615  continue;
616 
617  /* if the whole cycle has been explored */
618  if(it==s_it)
619  continue;
620 
621  const abstract_eventt &first=egraph[*it];
622  const abstract_eventt &second=egraph[*s_it];
623 
624  const data_dpt &data_dp=egraph.map_data_dp[first.thread];
625 
626  /* if data dp between linking the pair, safe */
627  if(first.thread==second.thread && data_dp.dp(first, second))
628  continue;
629 
630  /* AC and BC conditions */
631  if(first.thread!=second.thread && model==Power)
632  {
633  bool AC=false;
634  bool BC=false;
635 
636  /* no fence after the second element? (AC) */
637  const_iterator AC_it=++s_it;
638  --s_it;
639  for(;
640  AC_it!=end() && egraph[*AC_it].thread==second.thread;
641  AC_it++)
642  if(egraph[*AC_it].operation==abstract_eventt::operationt::ASMfence
643  && egraph[*AC_it].is_cumul()
644  && egraph[*AC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
645  {
646  AC=true;
647  break;
648  }
649 
650  if(AC)
651  continue;
652 
653  if(AC_it==end() && egraph[front()].thread==second.thread)
654  {
655  for(AC_it=begin();
656  !(egraph[*AC_it]==first) && egraph[*AC_it].thread==second.thread;
657  AC_it++)
658  if(egraph[*AC_it].operation==abstract_eventt::operationt::ASMfence &&
659  egraph[*AC_it].is_cumul() &&
660  egraph[*AC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
661  {
662  AC=true;
663  break;
664  }
665  }
666 
667  if(AC)
668  continue;
669 
670  /* no fence before the first element? (BC) */
671  const_iterator BC_it;
672  if(it==begin())
673  {
674  BC_it=end();
675  BC_it--;
676  }
677  else
678  {
679  BC_it=--it;
680  ++it;
681  }
682  for( ;
683  BC_it!=begin() && egraph[*BC_it].thread==first.thread;
684  BC_it--)
685  {
686  if(egraph[*BC_it].operation==abstract_eventt::operationt::ASMfence &&
687  egraph[*BC_it].is_cumul() &&
688  egraph[*BC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
689  {
690  BC=true;
691  break;
692  }
693  }
694 
695  if(BC)
696  continue;
697 
698  if(BC_it==begin() && egraph[back()].thread==first.thread)
699  {
700  for(BC_it=end();
701  !(egraph[*BC_it]==second) && egraph[*BC_it].thread==first.thread;
702  BC_it--)
703  if(egraph[*BC_it].operation==abstract_eventt::operationt::ASMfence &&
704  egraph[*BC_it].is_cumul() &&
705  egraph[*BC_it].is_corresponding_fence(egraph[*it], egraph[*s_it]))
706  {
707  BC=true;
708  break;
709  }
710  }
711 
712  if(BC)
713  continue;
714  }
715 
716  if(s_it==++it)
717  {
718  --it;
719 
720  /* no lwfence between the pair */
721  if(first.unsafe_pair(second, model)
722  && (first.thread!=second.thread || egraph.are_po_ordered(*it, *s_it)))
723  {
724  if(fast)
725  return true;
726  else
727  {
728  const delayt delay(*it, *s_it, (first.thread==second.thread));
729  unsafe_pairs.insert(delay);
730  unsafe_met=true;
731  }
732  }
733  }
734  else
735  {
736  --it;
737 
738  /* one (or more) lwfence between the pair */
739  if(first.unsafe_pair_asm(second, model, fences_met)
740  && (first.thread!=second.thread || egraph.are_po_ordered(*it, *s_it)))
741  {
742  if(fast)
743  return true;
744  else
745  {
746  const delayt delay(*it, *s_it, (first.thread==second.thread));
747  unsafe_pairs.insert(delay);
748  unsafe_met=true;
749  }
750  }
751  }
752  }
753 
754  /* strong fence -- this pair is safe */
755  if(egraph[back()].operation==abstract_eventt::operationt::ASMfence
756  || egraph[front()].operation==abstract_eventt::operationt::ASMfence)
757  return unsafe_met;
758 
759  fences_met=0;
760 
761  /* selects the next event which is not a weak fence */
762  const_iterator s_it;
763  for(s_it=begin();
764  s_it!=end() &&
765  egraph[*s_it].operation==abstract_eventt::operationt::ASMfence;
766  s_it++)
767  fences_met |= egraph[*s_it].fence_value();
768 
769  /* if the whole cycle has been explored */
770  if(s_it==end())
771  return unsafe_met;
772 
773  if(egraph[*s_it].operation==abstract_eventt::operationt::ASMfence)
774  return unsafe_met;
775 
776  const abstract_eventt &first=egraph[back()];
777  const abstract_eventt &second=egraph[*s_it];
778 
779  const data_dpt &data_dp=egraph.map_data_dp[first.thread];
780 
781  /* if data dp between linking the pair, safe */
782  if(first.thread==second.thread && data_dp.dp(first, second))
783  return unsafe_met;
784 
785  /* AC and BC conditions */
786  if(first.thread!=second.thread && model==Power)
787  {
788  bool AC=false;
789  bool BC=false;
790 
791  /* no fence after the second element? (AC) */
792  const_iterator AC_it=++s_it;
793  --s_it;
794  for(;
795  AC_it!=end() && egraph[*AC_it].thread==second.thread;
796  AC_it++)
797  if(egraph[*AC_it].operation==abstract_eventt::operationt::ASMfence
798  && egraph[*AC_it].is_cumul()
799  && egraph[*AC_it].is_corresponding_fence(first, second))
800  {
801  AC=true;
802  break;
803  }
804 
805  if(AC)
806  return unsafe_met;
807 
808  if(AC_it==end() && egraph[front()].thread==second.thread)
809  {
810  for(AC_it=begin();
811  !(egraph[*AC_it]==first) && egraph[*AC_it].thread==second.thread;
812  AC_it++)
813  if(egraph[*AC_it].operation==abstract_eventt::operationt::ASMfence &&
814  egraph[*AC_it].is_cumul() &&
815  egraph[*AC_it].is_corresponding_fence(first, second))
816  {
817  AC=true;
818  break;
819  }
820  }
821 
822  if(AC)
823  return unsafe_met;
824 
825  /* no fence before the first element? (BC) */
826  const_iterator BC_it=end();
827  --BC_it;
828 
829  for(;
830  BC_it!=begin() && egraph[*BC_it].thread==first.thread;
831  BC_it--)
832  if(egraph[*BC_it].operation==abstract_eventt::operationt::ASMfence
833  && egraph[*BC_it].is_cumul()
834  && egraph[*BC_it].is_corresponding_fence(first, second))
835  {
836  BC=true;
837  break;
838  }
839 
840  if(BC)
841  return unsafe_met;
842 
843  if(BC_it==begin() && egraph[back()].thread==first.thread)
844  {
845  BC_it=end();
846  BC_it--;
847  for(;
848  !(egraph[*BC_it]==second) && egraph[*BC_it].thread==first.thread;
849  BC_it--)
850  if(egraph[*BC_it].operation==abstract_eventt::operationt::ASMfence
851  && egraph[*BC_it].is_cumul()
852  && egraph[*BC_it].is_corresponding_fence(first, second))
853  {
854  BC=true;
855  break;
856  }
857  }
858 
859  if(BC)
860  return unsafe_met;
861  }
862 
863  if(s_it==begin())
864  {
865  /* no lwfence between the pair */
866  if(first.unsafe_pair(second, model)
867  && (first.thread!=second.thread || egraph.are_po_ordered(back(), *s_it)))
868  {
869  if(!fast)
870  {
871  const delayt delay(back(), *s_it, (first.thread==second.thread));
872  unsafe_pairs.insert(delay);
873  }
874  return true;
875  }
876  }
877  else
878  {
879  /* one (or more) lwfence between the pair */
880  if(first.unsafe_pair_asm(second, model, fences_met)
881  && (first.thread!=second.thread || egraph.are_po_ordered(back(), *s_it)))
882  {
883  if(!fast)
884  {
885  const delayt delay(back(), *s_it, (first.thread==second.thread));
886  unsafe_pairs.insert(delay);
887  }
888  return true;
889  }
890  }
891 
892  return unsafe_met;
893 }
894 
896 {
897  const_iterator it=begin();
898 
899  /* find the first non-fence event */
900  for(; it!=end(); ++it)
901  {
902  const abstract_eventt &it_evt=egraph[*it];
906  break;
907  }
908 
909  /* if only fences, uniproc */
910  if(it==end())
911  return false;
912 
913  const irep_idt &var=egraph[*it].variable;
914 
915  /* if it is an array access, by over-approximation, we don't have
916  uniproc in the cycle (tab[]) */
917  if(!egraph.ignore_arrays && id2string(var).find("[]")!=std::string::npos)
918  return true;
919 
920  for(; it!=end(); ++it)
921  {
922  const abstract_eventt &it_evt=egraph[*it];
923  if(it_evt.variable!=var
927  break;
928  }
929 
930  return (it!=end());
931 }
932 
934 {
935  const_iterator it=begin();
936 
937  /* find the first non-fence event */
938  for(; it!=end(); it++)
939  {
940  const abstract_eventt &it_evt=egraph[*it];
944  break;
945  }
946 
947  /* if only fences, uniproc */
948  if(it==end())
949  return false;
950 
951  const irep_idt &var=egraph[*it].variable;
952 
953  const_iterator prev=it;
954  for(; it!=end(); prev=it, ++it)
955  {
956  const abstract_eventt &it_evt=egraph[*it];
957  if(
958  !(it_evt.variable==var
959  &&(it==begin() || it_evt.operation!=abstract_eventt::operationt::Read
960  || egraph[*prev].operation!=abstract_eventt::operationt::Read))
964  break;
965  }
966 
967  return (it!=end());
968 }
969 
971 {
972  // assert(size()>2);
973  if(size()<=2)
974  return false;
975 
976  for(const_iterator it=begin(); it!=end(); ++it)
977  {
978  const_iterator n_it=it;
979  ++n_it;
980 
981  if(n_it==end())
982  break;
983 
984  const abstract_eventt &current=egraph[*it];
985  const abstract_eventt &next=egraph[*n_it];
986 
987  /* rf */
990  continue;
991 
992  /* data dependencies */
993  const data_dpt &dep=egraph.map_data_dp[current.thread];
994 
995  if(dep.dp(current, next))
996  continue;
997 
998  return true;
999  }
1000 
1001  const abstract_eventt &current=egraph[back()];
1002  const abstract_eventt &next=egraph[front()];
1003 
1004  /* rf */
1007  return false;
1008 
1009  /* data dependencies */
1010  const data_dpt &dep=egraph.map_data_dp[current.thread];
1011 
1012  if(dep.dp(current, next))
1013  return false;
1014 
1015  return true;
1016 }
1017 
1019 {
1020  std::string cycle="Cycle: ";
1021  for(const_iterator it=begin(); it!=end(); ++it)
1022  cycle += std::to_string(egraph[*it].id) + "; ";
1023  return cycle + " End of cycle.";
1024 }
1025 
1027 {
1028  std::string name="Unsafe pairs: ";
1029  for(std::set<delayt>::const_iterator it=unsafe_pairs.begin();
1030  it!=unsafe_pairs.end();
1031  ++it)
1032  {
1033  const abstract_eventt &first=egraph[it->second];
1034  const abstract_eventt &last=egraph[it->first];
1035 
1036  if(last.variable==first.variable
1039  {
1040  name += " Rf";
1041  name += (last.thread==first.thread?"i":"e");
1042  }
1043 
1044  else if(last.variable==first.variable &&
1047  (last.thread!=first.thread || it->first > it->second))
1048  {
1049  name += " Fr";
1050  name += (last.thread==first.thread?"i":"e");
1051  }
1052  else if(last.variable==first.variable &&
1055  (last.thread!=first.thread || it->first > it->second))
1056  {
1057  /* we prefer to write Po rather than Wsi */
1058  name += " Ws";
1059  name += (last.thread==first.thread?"i":"e");
1060  }
1061  else if(last.thread==first.thread &&
1063  {
1064  name += " Po";
1065  name += (last.variable==first.variable?"s":"d") + last.get_operation()
1066  + first.get_operation();
1067  }
1068  }
1069 
1070  return name;
1071 }
1072 
1074 {
1075  std::string cycle="Cycle: ";
1076  for(const_iterator it=begin(); it!=end(); ++it)
1077  {
1078  const abstract_eventt &it_evt=egraph[*it];
1079  cycle += it_evt.get_operation() + id2string(it_evt.variable)
1080  + "; ";
1081  }
1082  return cycle+" End of cycle.";
1083 }
1084 
1086 {
1087  std::string cycle;
1088  for(const_iterator it=begin(); it!=end(); ++it)
1089  {
1090  const abstract_eventt &it_evt=egraph[*it];
1091  cycle += id2string(it_evt.variable) + " (";
1092  cycle += it_evt.source_location.as_string();
1093  cycle += " thread " + std::to_string(it_evt.thread) + ") ";
1094  }
1095  return cycle;
1096 }
1097 
1099  const critical_cyclet &reduced,
1100  std::map<std::string, std::string> &map_id2var,
1101  std::map<std::string, std::string> &map_var2id) const
1102 {
1103  std::string cycle;
1104  for(const_iterator it=reduced.begin(); it!=reduced.end(); ++it)
1105  {
1106  const abstract_eventt &it_evt=egraph[*it];
1107  const std::string var_name=id2string(it_evt.variable)
1108  + " (" + it_evt.source_location.as_string() + ")";
1109  if(map_var2id.find(var_name)!=map_var2id.end())
1110  {
1111  cycle += "t" + std::to_string(it_evt.thread) + " (";
1112  cycle += map_var2id[var_name] + ") ";
1113  }
1114  else
1115  {
1116  const std::string new_id="var@" + std::to_string(map_var2id.size());
1117  map_var2id[var_name]=new_id;
1118  map_id2var[new_id]=var_name;
1119  cycle += "t" + std::to_string(it_evt.thread) + " (";
1120  cycle += new_id + ") ";
1121  }
1122  }
1123  return cycle;
1124 }
1125 
1127  memory_modelt model,
1128  std::map<std::string, std::string> &map_id2var,
1129  std::map<std::string, std::string> &map_var2id,
1130  bool hide_internals) const
1131 {
1132  std::string cycle;
1133 
1134  assert(size() > 2);
1135 
1136  /* removes all the internal events */
1137  if(hide_internals)
1138  {
1139  critical_cyclet reduced(egraph, id);
1140  this->hide_internals(reduced);
1141  assert(reduced.size() > 0);
1142  cycle+=print_detail(reduced, map_id2var, map_var2id);
1143  cycle+=": ";
1144  cycle+=print_name(reduced, model);
1145  }
1146  else
1147  {
1148  cycle+=print_detail(*this, map_id2var, map_var2id);
1149  cycle+=": ";
1150  cycle+=print_name(*this, model);
1151  }
1152 
1153  return cycle;
1154 }
1155 
1157  critical_cyclet &reduced) const
1158 {
1159  std::set<event_idt> reduced_evts;
1160  const_iterator first_it, prev_it=end();
1161 
1162  /* finds an element first of its thread */
1163  for(first_it=begin(); first_it!=end(); ++first_it)
1164  {
1165  const abstract_eventt &first=egraph[*first_it];
1166  if(prev_it!=end() && egraph[*prev_it].thread!=first.thread
1167  && !first.is_fence())
1168  break;
1169  prev_it=first_it;
1170  }
1171  assert(first_it!=end());
1172  reduced.push_back(*first_it);
1173  reduced_evts.insert(*first_it);
1174 
1175  /* conserves only the extrema of threads */
1176  for(const_iterator cur_it=first_it; cur_it!=end(); ++cur_it)
1177  {
1178  const abstract_eventt &cur=egraph[*cur_it];
1179  if(cur.is_fence())
1180  continue;
1181 
1182  const_iterator next_it=cur_it;
1183  ++next_it;
1184  if(next_it==end())
1185  next_it=begin();
1186 
1187  if(cur.thread!=egraph[*next_it].thread)
1188  {
1189  if(reduced_evts.find(*cur_it)==reduced_evts.end())
1190  {
1191  reduced.push_back(*cur_it);
1192  reduced_evts.insert(*cur_it);
1193  }
1194  for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1195  assert(next_it!=end());
1196  if(reduced_evts.find(*next_it)==reduced_evts.end())
1197  {
1198  reduced.push_back(*next_it);
1199  reduced_evts.insert(*next_it);
1200  }
1201  }
1202  }
1203 
1204  for(const_iterator cur_it=begin(); cur_it!=first_it; ++cur_it)
1205  {
1206  const abstract_eventt &cur=egraph[*cur_it];
1207  if(cur.is_fence())
1208  continue;
1209 
1210  const_iterator next_it=cur_it;
1211  ++next_it;
1212  assert(next_it!=end());
1213 
1214  if(cur.thread!=egraph[*next_it].thread)
1215  {
1216  if(reduced_evts.find(*cur_it)==reduced_evts.end())
1217  {
1218  reduced.push_back(*cur_it);
1219  reduced_evts.insert(*cur_it);
1220  }
1221  for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1222  assert(next_it!=end());
1223  if(reduced_evts.find(*next_it)==reduced_evts.end())
1224  {
1225  reduced.push_back(*next_it);
1226  reduced_evts.insert(*next_it);
1227  }
1228  }
1229  }
1230 }
1231 
1233  const critical_cyclet &reduced,
1234  memory_modelt model) const
1235 {
1236  assert(reduced.size()>=2);
1237  unsigned extra_fence_count=0;
1238 
1239  std::string name;
1240  const_iterator prev_it=reduced.end();
1241  bool first_done=false;
1242  for(const_iterator cur_it=reduced.begin(); cur_it!=reduced.end(); ++cur_it)
1243  {
1244  const abstract_eventt &cur=egraph[*cur_it];
1245 
1246  if(prev_it!=reduced.end())
1247  {
1248  const abstract_eventt &prev=egraph[*prev_it];
1249 
1253  {
1254  ++extra_fence_count;
1255  // nothing to do
1256  }
1257 
1259  {
1260  const_iterator n_it=cur_it;
1261  bool wraparound=false;
1262  while(true)
1263  {
1264  ++n_it;
1265  if(n_it==reduced.end())
1266  {
1267  assert(!wraparound);
1268  wraparound=true;
1269  first_done=true;
1270  ++extra_fence_count;
1271  n_it=reduced.begin();
1272  }
1273  const abstract_eventt &cand=egraph[*n_it];
1277  break;
1278  if(!wraparound)
1279  ++cur_it;
1280  if(!wraparound)
1281  ++extra_fence_count;
1282  }
1283  const abstract_eventt &succ=egraph[*n_it];
1286  name += (model==Power?" Sync":" MFence");
1287  name += (prev.variable==succ.variable?"s":"d")
1288  + prev.get_operation() + succ.get_operation();
1289  }
1290 
1292  {
1293  std::string cand_name=" LwSync";
1294  const_iterator n_it=cur_it;
1295  bool wraparound=false;
1296  while(true)
1297  {
1298  ++n_it;
1299  if(n_it==reduced.end())
1300  {
1301  assert(!wraparound);
1302  wraparound=true;
1303  first_done=true;
1304  ++extra_fence_count;
1305  n_it=reduced.begin();
1306  }
1307  const abstract_eventt &cand=egraph[*n_it];
1311  break;
1314  cand.fence_value()&1))
1315  cand_name=(model==Power?" Sync":" MFence");
1316  if(!wraparound)
1317  ++cur_it;
1318  if(!wraparound)
1319  ++extra_fence_count;
1320  }
1321  const abstract_eventt &succ=egraph[*n_it];
1324  name += cand_name;
1325  name += (prev.variable==succ.variable?"s":"d")
1326  + prev.get_operation() + succ.get_operation();
1327  }
1328 
1330  {
1331  std::string cand_name;
1332  if(cur.fence_value()&1)
1333  cand_name=(model==Power?" Sync":" MFence");
1334  else
1335  cand_name=" LwSync";
1336  const_iterator n_it=cur_it;
1337  bool wraparound=false;
1338  while(true)
1339  {
1340  ++n_it;
1341  if(n_it==reduced.end())
1342  {
1343  assert(!wraparound);
1344  wraparound=true;
1345  first_done=true;
1346  ++extra_fence_count;
1347  n_it=reduced.begin();
1348  }
1349  const abstract_eventt &cand=egraph[*n_it];
1353  break;
1356  cand.fence_value()&1))
1357  cand_name=(model==Power?" Sync":" MFence");
1358  if(!wraparound)
1359  ++cur_it;
1360  if(!wraparound)
1361  ++extra_fence_count;
1362  }
1363  const abstract_eventt &succ=egraph[*n_it];
1366  name += cand_name;
1367  name += (prev.variable==succ.variable?"s":"d")
1368  + prev.get_operation() + succ.get_operation();
1369  }
1370 
1371  else if(prev.variable==cur.variable
1374  {
1375  name += " Rf";
1376  name += (prev.thread==cur.thread?"i":"e");
1377  }
1378 
1379  else if(prev.variable==cur.variable
1382  && (prev.thread!=cur.thread || *prev_it > *cur_it))
1383  {
1384  name += " Fr";
1385  name += (prev.thread==cur.thread?"i":"e");
1386  }
1387 
1388  else if(prev.variable==cur.variable &&
1391  (prev.thread!=cur.thread || *prev_it > *cur_it))
1392  {
1393  /* we prefer to write Po rather than Wsi */
1394  name += " Ws";
1395  name += (prev.thread==cur.thread?"i":"e");
1396  }
1397 
1398  else if(prev.thread==cur.thread
1402  {
1403  const data_dpt &dep=egraph.map_data_dp[cur.thread];
1404 
1406  dep.dp(prev, cur))
1407  {
1408  name += " DpData";
1409  name += (prev.variable==cur.variable?"s":"d")
1410  + cur.get_operation();
1411  }
1412  else
1413  {
1414  name += " Po";
1415  name += (prev.variable==cur.variable?"s":"d") + prev.get_operation()
1416  + cur.get_operation();
1417  }
1418  }
1419 
1420  else if(cur.variable!=ID_unknown && prev.variable!=ID_unknown)
1421  assert(false);
1422  }
1423 
1424  prev_it=cur_it;
1425  }
1426 
1427  if(first_done)
1428  {
1429  auto n_events=extra_fence_count;
1430  for(std::string::const_iterator it=name.begin();
1431  it!=name.end();
1432  ++it)
1433  if(*it==' ')
1434  ++n_events;
1435  assert(n_events==reduced.size());
1436 
1437  return name;
1438  }
1439 
1440  const abstract_eventt &first=egraph[reduced.front()];
1441  const abstract_eventt &last=egraph[reduced.back()];
1442 
1446 
1450  {
1451  std::string cand_name=" LwSync";
1452  const_iterator it=reduced.begin();
1453  for( ; it!=reduced.end(); ++it)
1454  {
1455  const abstract_eventt &cand=egraph[*it];
1456 
1460  break;
1463  cand.fence_value()&1))
1464  cand_name=(model==Power?" Sync":" MFence");
1465  }
1466  assert(it!=reduced.begin() && it!=reduced.end());
1467  const abstract_eventt &succ=egraph[*it];
1468  assert(succ.operation==abstract_eventt::operationt::Read ||
1469  succ.operation==abstract_eventt::operationt::Write);
1470  name += cand_name;
1471  name += (last.variable==succ.variable?"s":"d")
1472  + last.get_operation() + succ.get_operation();
1473  }
1474 
1475  else if(last.variable==first.variable
1478  {
1479  name += " Rf";
1480  name += (last.thread==first.thread?"i":"e");
1481  }
1482 
1483  else if(last.variable==first.variable
1486  && (last.thread!=first.thread || reduced.back() > reduced.front()))
1487  {
1488  name += " Fr";
1489  name += (last.thread==first.thread?"i":"e");
1490  }
1491 
1492  else if(last.variable==first.variable &&
1495  (last.thread!=first.thread || reduced.back() > reduced.front()))
1496  {
1497  /* we prefer to write Po rather than Wsi */
1498  name += " Ws";
1499  name += (last.thread==first.thread?"i":"e");
1500  }
1501 
1502  else if(last.thread==first.thread)
1503  {
1504  const data_dpt &dep=egraph.map_data_dp[last.thread];
1505 
1507  dep.dp(last, first))
1508  {
1509  name += " DpData";
1510  name += (last.variable==first.variable?"s":"d")
1511  + first.get_operation();
1512  }
1513  else
1514  {
1515  name += " Po";
1516  name += (last.variable==first.variable?"s":"d") + last.get_operation()
1517  + first.get_operation();
1518  }
1519  }
1520 
1521  else if(last.variable!=ID_unknown && first.variable!=ID_unknown)
1522  assert(false);
1523 
1524 #if 0
1525  critical_cyclet::size_type n_events=extra_fence_count;
1526  for(std::string::const_iterator it=name.begin();
1527  it!=name.end();
1528  ++it)
1529  if(*it==' ')
1530  ++n_events;
1531  assert(n_events==reduced.size());
1532 #endif
1533 
1534  return name;
1535 }
1536 
1538  std::ostream &str,
1539  unsigned colour,
1540  memory_modelt model) const
1541 {
1542  /* print vertices */
1543  for(const_iterator it=begin(); it!=end(); ++it)
1544  {
1545  const abstract_eventt &ev=egraph[*it];
1546 
1547  /* id of the cycle in comments */
1548  str << "/* " << id << " */\n";
1549 
1550  /* vertex */
1551  str << ev.id << "[label=\"\\\\lb {" << ev.id << "}" << ev.get_operation();
1552  str << "{" << ev.variable << "} {} @thread" << ev.thread << "\"];\n";
1553  }
1554 
1555  /* print edges */
1556  const_iterator prev_it=end();
1557  for(const_iterator cur_it=begin(); cur_it!=end(); ++cur_it)
1558  {
1559  const abstract_eventt &cur=egraph[*cur_it];
1560 
1561  /* id of the cycle in comments */
1562  str << "/* " << id << " */\n";
1563 
1564  /* edge */
1565  if(prev_it!=end())
1566  {
1567  const abstract_eventt &prev=egraph[*prev_it];
1568 
1569  str << prev.id << "->";
1571  {
1572  const_iterator n_it=cur_it;
1573  ++n_it;
1574  const abstract_eventt &succ=
1575  n_it!=end() ? egraph[*n_it] : egraph[front()];
1576  str << succ.id << "[label=\"";
1577  str << (model==Power?"Sync":"MFence");
1578  str << (prev.variable==cur.variable?"s":"d");
1579  str << prev.get_operation() << succ.get_operation();
1580  }
1582  {
1583  const_iterator n_it=cur_it;
1584  ++n_it;
1585  const abstract_eventt &succ=
1586  n_it!=end() ? egraph[*n_it] : egraph[front()];
1587  str << succ.id << "[label=\"";
1588  str << "LwSync" << (prev.variable==cur.variable?"s":"d");
1589  str <<prev.get_operation() << succ.get_operation();
1590  }
1591  else if(prev.variable==cur.variable
1594  {
1595  str << cur.id << "[label=\"";
1596  str << "Rf" << (prev.thread==cur.thread?"i":"e");
1597  }
1598  else if(prev.variable==cur.variable
1601  {
1602  str << cur.id << "[label=\"";
1603  str << "Fr" << (prev.thread==cur.thread?"i":"e");
1604  }
1605  else if(prev.variable==cur.variable &&
1608  prev.thread!=cur.thread)
1609  {
1610  /* we prefer to write Po rather than Wsi */
1611  str << cur.id << "[label=\"";
1612  str << "Ws" << (prev.thread==cur.thread?"i":"e");
1613  }
1614  else if(prev.thread==cur.thread &&
1616  {
1617  str << cur.id << "[label=\"";
1618  str << "Po" << (prev.variable==cur.variable?"s":"d")
1619  + prev.get_operation() + cur.get_operation();
1620  }
1621  else
1622  str << cur.id << "[label=\"?";
1623 
1624  str << "\",color=" << print_colour(colour) << "];\n";
1625  }
1626 
1627  prev_it=cur_it;
1628  }
1629 
1630  const abstract_eventt &first=egraph[front()];
1631  const abstract_eventt &last=egraph[back()];
1632 
1633  /* id of the cycle in comments */
1634  str << "/* " << id << " */\n";
1635 
1636  /* edge */
1637  str << last.id << "->";
1639  {
1640  const_iterator next=begin();
1641  ++next;
1642  const abstract_eventt &succ=egraph[*next];
1643  str << succ.id << "[label=\"";
1644  str << (model==Power?"Sync":"MFence");
1645  str << (last.variable==first.variable?"s":"d");
1646  str << last.get_operation() << succ.get_operation();
1647  }
1649  {
1650  const_iterator next=begin();
1651  ++next;
1652  const abstract_eventt &succ=egraph[*next];
1653  str << succ.id << "[label=\"";
1654  str << "LwSync" << (last.variable==first.variable?"s":"d");
1655  str << last.get_operation() << succ.get_operation();
1656  }
1657  else if(last.variable==first.variable &&
1660  {
1661  str << first.id << "[label=\"";
1662  str << "Rf" << (last.thread==first.thread?"i":"e");
1663  }
1664  else if(last.variable==first.variable &&
1667  {
1668  str << first.id << "[label=\"";
1669  str << "Fr" << (last.thread==first.thread?"i":"e");
1670  }
1671  else if(last.variable==first.variable &&
1674  last.thread!=first.thread)
1675  {
1676  /* we prefer to write Po rather than Wsi */
1677  str << first.id << "[label=\"";
1678  str << "Ws" << (last.thread==first.thread?"i":"e");
1679  }
1680  else if(last.thread==first.thread &&
1682  {
1683  str << first.id << "[label=\"";
1684  str << "Po" << (last.variable==first.variable?"s":"d");
1685  str << last.get_operation() << first.get_operation();
1686  }
1687  else
1688  str << first.id << "[label=\"?";
1689 
1690  str << "\", color=" << print_colour(colour) << "];\n";
1691 }
std::list< event_idt > po_order
Definition: event_graph.h:401
grapht< abstract_eventt >::nodet & operator[](event_idt n)
Definition: event_graph.h:414
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string print_name(const critical_cyclet &redyced, memory_modelt model) const
#define NB_COLOURS
Definition: event_graph.cpp:21
event_idt add_node()
Definition: event_graph.h:406
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
operationt operation
bool is_fence() const
Definition: wmm.h:23
const irep_idt & get_function() const
std::string as_string() const
void print_dot(std::ostream &str, unsigned colour, memory_modelt model) const
graph of abstract events
bool has_po_edge(event_idt i, event_idt j) const
Definition: event_graph.h:419
void hide_internals(critical_cyclet &reduced) const
void add_po_edge(event_idt a, event_idt b)
Definition: event_graph.h:454
unsignedbv_typet size_type()
Definition: c_types.cpp:58
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
unsigned char fence_value() const
data_typet::const_iterator const_iterator
Definition: event_graph.h:71
std::size_t size() const
Definition: event_graph.h:429
bool is_unsafe_asm(memory_modelt model, bool fast=false)
same as is_unsafe, but with ASM fences
std::string print_all(memory_modelt model, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, bool hide_internals) const
#define print_colour(u)
Definition: event_graph.cpp:26
const wmm_grapht::edgest & po_out(event_idt n) const
Definition: event_graph.h:439
memory_modelt
Definition: wmm.h:17
void print_graph()
Definition: event_graph.cpp:56
std::string print_output() const
bool unsafe_pair_lwfence(const abstract_eventt &next, memory_modelt model) const
messaget & message
Definition: event_graph.h:395
event_idt copy_segment(event_idt begin, event_idt end)
Definition: event_graph.cpp:90
std::string get_operation() const
const wmm_grapht::edgest & com_out(event_idt n) const
Definition: event_graph.h:449
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::string print_detail(const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id) const
wmm_grapht::node_indext event_idt
Definition: event_graph.h:33
bool has_com_edge(event_idt i, event_idt j) const
Definition: event_graph.h:424
bool is_unsafe(memory_modelt model, bool fast=false)
checks whether there is at least one pair which is unsafe (takes fences and dependencies into account...
const irep_idt & get_file() const
void print_rec_graph(std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)
Definition: event_graph.cpp:28
mstreamt & status() const
Definition: message.h:317
void add_com_edge(event_idt a, event_idt b)
Definition: event_graph.h:474
bool check_AC(data_typet::const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
static const char * colour_map[14]
Definition: event_graph.cpp:22
std::string print_unsafes() const
source_locationt source_location
bool check_BC(data_typet::const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
Definition: data_dp.cpp:73
std::string print_events() const
std::set< std::pair< const abstract_eventt &, const abstract_eventt & > > duplicated_bodies
Definition: event_graph.h:512
void explore_copy_segment(std::set< event_idt > &explored, event_idt begin, event_idt end) const
copies the segment
Definition: event_graph.cpp:72
Definition: kdev_t.h:19