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,
1102  memory_modelt model) const
1103 {
1104  std::string cycle;
1105  for(const_iterator it=reduced.begin(); it!=reduced.end(); ++it)
1106  {
1107  const abstract_eventt &it_evt=egraph[*it];
1108  const std::string var_name=id2string(it_evt.variable)
1109  + " (" + it_evt.source_location.as_string() + ")";
1110  if(map_var2id.find(var_name)!=map_var2id.end())
1111  {
1112  cycle += "t" + std::to_string(it_evt.thread) + " (";
1113  cycle += map_var2id[var_name] + ") ";
1114  }
1115  else
1116  {
1117  const std::string new_id="var@" + std::to_string(map_var2id.size());
1118  map_var2id[var_name]=new_id;
1119  map_id2var[new_id]=var_name;
1120  cycle += "t" + std::to_string(it_evt.thread) + " (";
1121  cycle += new_id + ") ";
1122  }
1123  }
1124  return cycle;
1125 }
1126 
1128  memory_modelt model,
1129  std::map<std::string, std::string> &map_id2var,
1130  std::map<std::string, std::string> &map_var2id,
1131  bool hide_internals) const
1132 {
1133  std::string cycle;
1134 
1135  assert(size() > 2);
1136 
1137  /* removes all the internal events */
1138  if(hide_internals)
1139  {
1140  critical_cyclet reduced(egraph, id);
1141  this->hide_internals(reduced);
1142  assert(reduced.size() > 0);
1143  cycle+=print_detail(reduced, map_id2var, map_var2id, model);
1144  cycle+=": ";
1145  cycle+=print_name(reduced, model);
1146  }
1147  else
1148  {
1149  cycle+=print_detail(*this, map_id2var, map_var2id, model);
1150  cycle+=": ";
1151  cycle+=print_name(*this, model);
1152  }
1153 
1154  return cycle;
1155 }
1156 
1158  critical_cyclet &reduced) const
1159 {
1160  std::set<event_idt> reduced_evts;
1161  const_iterator first_it, prev_it=end();
1162 
1163  /* finds an element first of its thread */
1164  for(first_it=begin(); first_it!=end(); ++first_it)
1165  {
1166  const abstract_eventt &first=egraph[*first_it];
1167  if(prev_it!=end() && egraph[*prev_it].thread!=first.thread
1168  && !first.is_fence())
1169  break;
1170  prev_it=first_it;
1171  }
1172  assert(first_it!=end());
1173  reduced.push_back(*first_it);
1174  reduced_evts.insert(*first_it);
1175 
1176  /* conserves only the extrema of threads */
1177  for(const_iterator cur_it=first_it; cur_it!=end(); ++cur_it)
1178  {
1179  const abstract_eventt &cur=egraph[*cur_it];
1180  if(cur.is_fence())
1181  continue;
1182 
1183  const_iterator next_it=cur_it;
1184  ++next_it;
1185  if(next_it==end())
1186  next_it=begin();
1187 
1188  if(cur.thread!=egraph[*next_it].thread)
1189  {
1190  if(reduced_evts.find(*cur_it)==reduced_evts.end())
1191  {
1192  reduced.push_back(*cur_it);
1193  reduced_evts.insert(*cur_it);
1194  }
1195  for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1196  assert(next_it!=end());
1197  if(reduced_evts.find(*next_it)==reduced_evts.end())
1198  {
1199  reduced.push_back(*next_it);
1200  reduced_evts.insert(*next_it);
1201  }
1202  }
1203  }
1204 
1205  for(const_iterator cur_it=begin(); cur_it!=first_it; ++cur_it)
1206  {
1207  const abstract_eventt &cur=egraph[*cur_it];
1208  if(cur.is_fence())
1209  continue;
1210 
1211  const_iterator next_it=cur_it;
1212  ++next_it;
1213  assert(next_it!=end());
1214 
1215  if(cur.thread!=egraph[*next_it].thread)
1216  {
1217  if(reduced_evts.find(*cur_it)==reduced_evts.end())
1218  {
1219  reduced.push_back(*cur_it);
1220  reduced_evts.insert(*cur_it);
1221  }
1222  for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {}
1223  assert(next_it!=end());
1224  if(reduced_evts.find(*next_it)==reduced_evts.end())
1225  {
1226  reduced.push_back(*next_it);
1227  reduced_evts.insert(*next_it);
1228  }
1229  }
1230  }
1231 }
1232 
1234  const critical_cyclet &reduced,
1235  memory_modelt model) const
1236 {
1237  assert(reduced.size()>=2);
1238  unsigned extra_fence_count=0;
1239 
1240  std::string name;
1241  const_iterator prev_it=reduced.end();
1242  bool first_done=false;
1243  for(const_iterator cur_it=reduced.begin(); cur_it!=reduced.end(); ++cur_it)
1244  {
1245  const abstract_eventt &cur=egraph[*cur_it];
1246 
1247  if(prev_it!=reduced.end())
1248  {
1249  const abstract_eventt &prev=egraph[*prev_it];
1250 
1254  {
1255  ++extra_fence_count;
1256  // nothing to do
1257  }
1258 
1260  {
1261  const_iterator n_it=cur_it;
1262  bool wraparound=false;
1263  while(true)
1264  {
1265  ++n_it;
1266  if(n_it==reduced.end())
1267  {
1268  assert(!wraparound);
1269  wraparound=true;
1270  first_done=true;
1271  ++extra_fence_count;
1272  n_it=reduced.begin();
1273  }
1274  const abstract_eventt &cand=egraph[*n_it];
1278  break;
1279  if(!wraparound)
1280  ++cur_it;
1281  if(!wraparound)
1282  ++extra_fence_count;
1283  }
1284  const abstract_eventt &succ=egraph[*n_it];
1287  name += (model==Power?" Sync":" MFence");
1288  name += (prev.variable==succ.variable?"s":"d")
1289  + prev.get_operation() + succ.get_operation();
1290  }
1291 
1293  {
1294  std::string cand_name=" LwSync";
1295  const_iterator n_it=cur_it;
1296  bool wraparound=false;
1297  while(true)
1298  {
1299  ++n_it;
1300  if(n_it==reduced.end())
1301  {
1302  assert(!wraparound);
1303  wraparound=true;
1304  first_done=true;
1305  ++extra_fence_count;
1306  n_it=reduced.begin();
1307  }
1308  const abstract_eventt &cand=egraph[*n_it];
1312  break;
1315  cand.fence_value()&1))
1316  cand_name=(model==Power?" Sync":" MFence");
1317  if(!wraparound)
1318  ++cur_it;
1319  if(!wraparound)
1320  ++extra_fence_count;
1321  }
1322  const abstract_eventt &succ=egraph[*n_it];
1325  name += cand_name;
1326  name += (prev.variable==succ.variable?"s":"d")
1327  + prev.get_operation() + succ.get_operation();
1328  }
1329 
1331  {
1332  std::string cand_name;
1333  if(cur.fence_value()&1)
1334  cand_name=(model==Power?" Sync":" MFence");
1335  else
1336  cand_name=" LwSync";
1337  const_iterator n_it=cur_it;
1338  bool wraparound=false;
1339  while(true)
1340  {
1341  ++n_it;
1342  if(n_it==reduced.end())
1343  {
1344  assert(!wraparound);
1345  wraparound=true;
1346  first_done=true;
1347  ++extra_fence_count;
1348  n_it=reduced.begin();
1349  }
1350  const abstract_eventt &cand=egraph[*n_it];
1354  break;
1357  cand.fence_value()&1))
1358  cand_name=(model==Power?" Sync":" MFence");
1359  if(!wraparound)
1360  ++cur_it;
1361  if(!wraparound)
1362  ++extra_fence_count;
1363  }
1364  const abstract_eventt &succ=egraph[*n_it];
1367  name += cand_name;
1368  name += (prev.variable==succ.variable?"s":"d")
1369  + prev.get_operation() + succ.get_operation();
1370  }
1371 
1372  else if(prev.variable==cur.variable
1375  {
1376  name += " Rf";
1377  name += (prev.thread==cur.thread?"i":"e");
1378  }
1379 
1380  else if(prev.variable==cur.variable
1383  && (prev.thread!=cur.thread || *prev_it > *cur_it))
1384  {
1385  name += " Fr";
1386  name += (prev.thread==cur.thread?"i":"e");
1387  }
1388 
1389  else if(prev.variable==cur.variable &&
1392  (prev.thread!=cur.thread || *prev_it > *cur_it))
1393  {
1394  /* we prefer to write Po rather than Wsi */
1395  name += " Ws";
1396  name += (prev.thread==cur.thread?"i":"e");
1397  }
1398 
1399  else if(prev.thread==cur.thread
1403  {
1404  const data_dpt &dep=egraph.map_data_dp[cur.thread];
1405 
1407  dep.dp(prev, cur))
1408  {
1409  name += " DpData";
1410  name += (prev.variable==cur.variable?"s":"d")
1411  + cur.get_operation();
1412  }
1413  else
1414  {
1415  name += " Po";
1416  name += (prev.variable==cur.variable?"s":"d") + prev.get_operation()
1417  + cur.get_operation();
1418  }
1419  }
1420 
1421  else if(cur.variable!=ID_unknown && prev.variable!=ID_unknown)
1422  assert(false);
1423  }
1424 
1425  prev_it=cur_it;
1426  }
1427 
1428  if(first_done)
1429  {
1430  auto n_events=extra_fence_count;
1431  for(std::string::const_iterator it=name.begin();
1432  it!=name.end();
1433  ++it)
1434  if(*it==' ')
1435  ++n_events;
1436  assert(n_events==reduced.size());
1437 
1438  return name;
1439  }
1440 
1441  const abstract_eventt &first=egraph[reduced.front()];
1442  const abstract_eventt &last=egraph[reduced.back()];
1443 
1447 
1451  {
1452  std::string cand_name=" LwSync";
1453  const_iterator it=reduced.begin();
1454  for( ; it!=reduced.end(); ++it)
1455  {
1456  const abstract_eventt &cand=egraph[*it];
1457 
1461  break;
1464  cand.fence_value()&1))
1465  cand_name=(model==Power?" Sync":" MFence");
1466  }
1467  assert(it!=reduced.begin() && it!=reduced.end());
1468  const abstract_eventt &succ=egraph[*it];
1469  assert(succ.operation==abstract_eventt::operationt::Read ||
1470  succ.operation==abstract_eventt::operationt::Write);
1471  name += cand_name;
1472  name += (last.variable==succ.variable?"s":"d")
1473  + last.get_operation() + succ.get_operation();
1474  }
1475 
1476  else if(last.variable==first.variable
1479  {
1480  name += " Rf";
1481  name += (last.thread==first.thread?"i":"e");
1482  }
1483 
1484  else if(last.variable==first.variable
1487  && (last.thread!=first.thread || reduced.back() > reduced.front()))
1488  {
1489  name += " Fr";
1490  name += (last.thread==first.thread?"i":"e");
1491  }
1492 
1493  else if(last.variable==first.variable &&
1496  (last.thread!=first.thread || reduced.back() > reduced.front()))
1497  {
1498  /* we prefer to write Po rather than Wsi */
1499  name += " Ws";
1500  name += (last.thread==first.thread?"i":"e");
1501  }
1502 
1503  else if(last.thread==first.thread)
1504  {
1505  const data_dpt &dep=egraph.map_data_dp[last.thread];
1506 
1508  dep.dp(last, first))
1509  {
1510  name += " DpData";
1511  name += (last.variable==first.variable?"s":"d")
1512  + first.get_operation();
1513  }
1514  else
1515  {
1516  name += " Po";
1517  name += (last.variable==first.variable?"s":"d") + last.get_operation()
1518  + first.get_operation();
1519  }
1520  }
1521 
1522  else if(last.variable!=ID_unknown && first.variable!=ID_unknown)
1523  assert(false);
1524 
1525 #if 0
1526  critical_cyclet::size_type n_events=extra_fence_count;
1527  for(std::string::const_iterator it=name.begin();
1528  it!=name.end();
1529  ++it)
1530  if(*it==' ')
1531  ++n_events;
1532  assert(n_events==reduced.size());
1533 #endif
1534 
1535  return name;
1536 }
1537 
1539  std::ostream &str,
1540  unsigned colour,
1541  memory_modelt model) const
1542 {
1543  /* print vertices */
1544  for(const_iterator it=begin(); it!=end(); ++it)
1545  {
1546  const abstract_eventt &ev=egraph[*it];
1547 
1548  /* id of the cycle in comments */
1549  str << "/* " << id << " */\n";
1550 
1551  /* vertex */
1552  str << ev.id << "[label=\"\\\\lb {" << ev.id << "}" << ev.get_operation();
1553  str << "{" << ev.variable << "} {} @thread" << ev.thread << "\"];\n";
1554  }
1555 
1556  /* print edges */
1557  const_iterator prev_it=end();
1558  for(const_iterator cur_it=begin(); cur_it!=end(); ++cur_it)
1559  {
1560  const abstract_eventt &cur=egraph[*cur_it];
1561 
1562  /* id of the cycle in comments */
1563  str << "/* " << id << " */\n";
1564 
1565  /* edge */
1566  if(prev_it!=end())
1567  {
1568  const abstract_eventt &prev=egraph[*prev_it];
1569 
1570  str << prev.id << "->";
1572  {
1573  const_iterator n_it=cur_it;
1574  ++n_it;
1575  const abstract_eventt &succ=
1576  n_it!=end() ? egraph[*n_it] : egraph[front()];
1577  str << succ.id << "[label=\"";
1578  str << (model==Power?"Sync":"MFence");
1579  str << (prev.variable==cur.variable?"s":"d");
1580  str << prev.get_operation() << succ.get_operation();
1581  }
1583  {
1584  const_iterator n_it=cur_it;
1585  ++n_it;
1586  const abstract_eventt &succ=
1587  n_it!=end() ? egraph[*n_it] : egraph[front()];
1588  str << succ.id << "[label=\"";
1589  str << "LwSync" << (prev.variable==cur.variable?"s":"d");
1590  str <<prev.get_operation() << succ.get_operation();
1591  }
1592  else if(prev.variable==cur.variable
1595  {
1596  str << cur.id << "[label=\"";
1597  str << "Rf" << (prev.thread==cur.thread?"i":"e");
1598  }
1599  else if(prev.variable==cur.variable
1602  {
1603  str << cur.id << "[label=\"";
1604  str << "Fr" << (prev.thread==cur.thread?"i":"e");
1605  }
1606  else if(prev.variable==cur.variable &&
1609  prev.thread!=cur.thread)
1610  {
1611  /* we prefer to write Po rather than Wsi */
1612  str << cur.id << "[label=\"";
1613  str << "Ws" << (prev.thread==cur.thread?"i":"e");
1614  }
1615  else if(prev.thread==cur.thread &&
1617  {
1618  str << cur.id << "[label=\"";
1619  str << "Po" << (prev.variable==cur.variable?"s":"d")
1620  + prev.get_operation() + cur.get_operation();
1621  }
1622  else
1623  str << cur.id << "[label=\"?";
1624 
1625  str << "\",color=" << print_colour(colour) << "];\n";
1626  }
1627 
1628  prev_it=cur_it;
1629  }
1630 
1631  const abstract_eventt &first=egraph[front()];
1632  const abstract_eventt &last=egraph[back()];
1633 
1634  /* id of the cycle in comments */
1635  str << "/* " << id << " */\n";
1636 
1637  /* edge */
1638  str << last.id << "->";
1640  {
1641  const_iterator next=begin();
1642  ++next;
1643  const abstract_eventt &succ=egraph[*next];
1644  str << succ.id << "[label=\"";
1645  str << (model==Power?"Sync":"MFence");
1646  str << (last.variable==first.variable?"s":"d");
1647  str << last.get_operation() << succ.get_operation();
1648  }
1650  {
1651  const_iterator next=begin();
1652  ++next;
1653  const abstract_eventt &succ=egraph[*next];
1654  str << succ.id << "[label=\"";
1655  str << "LwSync" << (last.variable==first.variable?"s":"d");
1656  str << last.get_operation() << succ.get_operation();
1657  }
1658  else if(last.variable==first.variable &&
1661  {
1662  str << first.id << "[label=\"";
1663  str << "Rf" << (last.thread==first.thread?"i":"e");
1664  }
1665  else if(last.variable==first.variable &&
1668  {
1669  str << first.id << "[label=\"";
1670  str << "Fr" << (last.thread==first.thread?"i":"e");
1671  }
1672  else if(last.variable==first.variable &&
1675  last.thread!=first.thread)
1676  {
1677  /* we prefer to write Po rather than Wsi */
1678  str << first.id << "[label=\"";
1679  str << "Ws" << (last.thread==first.thread?"i":"e");
1680  }
1681  else if(last.thread==first.thread &&
1683  {
1684  str << first.id << "[label=\"";
1685  str << "Po" << (last.variable==first.variable?"s":"d");
1686  str << last.get_operation() << first.get_operation();
1687  }
1688  else
1689  str << first.id << "[label=\"?";
1690 
1691  str << "\", color=" << print_colour(colour) << "];\n";
1692 }
std::list< event_idt > po_order
Definition: event_graph.h:402
grapht< abstract_eventt >::nodet & operator[](event_idt n)
Definition: event_graph.h:415
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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:407
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:420
void hide_internals(critical_cyclet &reduced) const
void add_po_edge(event_idt a, event_idt b)
Definition: event_graph.h:455
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:72
std::size_t size() const
Definition: event_graph.h:430
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:440
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:396
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:450
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:425
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:475
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
std::string print_detail(const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, memory_modelt model) const
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:513
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