cprover
graph_visitor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: graph visitor for computing edges involved for fencing
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #include "graph_visitor.h"
13 
14 #include "fence_inserter.h"
15 
16 /* implemented: BTWN1, BTWN4 */
17 #define BTWN1
18 
20  event_grapht &egraph,
21  event_idt next,
22  event_idt end,
23  std::list<event_idt> &old_path,
24  std::set<unsigned> &edges)
25 {
26  if(next==end)
27  {
28  /* inserts all the pos collected from old_path in edges */
29  std::list<event_idt>::const_iterator it=old_path.begin();
30  std::list<event_idt>::const_iterator next_it=it;
31  ++next_it;
32  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
33  {
34  /* it should be a po_s, and not a po_s^+ */
35  assert(egraph.has_po_edge(*it, *next_it));
36  edges.insert(fence_inserter.add_edge(edget(*it, *next_it)));
37  }
38  }
39  else if(egraph.po_out(next).empty())
40  {
41  /* this path is not connecting a to b => return */
42  }
43  else
44  {
45  for(wmm_grapht::edgest::const_iterator
46  next_it=egraph.po_out(next).begin();
47  next_it!=egraph.po_out(next).end();
48  ++next_it)
49  {
50  if(visited_nodes.find(next_it->first)!=visited_nodes.end())
51  continue;
52  visited_nodes.insert(next_it->first);
53 
54  old_path.push_back/*front*/(next_it->first);
55  graph_explore(egraph, next_it->first, end, old_path, edges);
56  old_path.pop_back/*front*/();
57  }
58  }
59 }
60 
62  event_grapht &egraph,
63  event_idt next,
64  event_idt end,
65  std::list<event_idt> &old_path)
66 {
67  if(next==end)
68  {
69  /* inserts all the pos collected from old_path in edges */
70  std::list<event_idt>::const_iterator it=old_path.begin();
71  std::list<event_idt>::const_iterator next_it=it;
72  ++next_it;
73  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
74  {
75  /* it should be a po_s, and not a po_s^+ */
76  assert(egraph.has_po_edge(*it, *next_it));
77  fence_inserter.add_edge(edget(*it, *next_it));
78  }
79  }
80  else if(egraph.po_out(next).empty())
81  {
82  /* this path is not connecting a to b => return */
83  }
84  else
85  {
86  for(wmm_grapht::edgest::const_iterator
87  next_it=egraph.po_out(next).begin();
88  next_it!=egraph.po_out(next).end();
89  ++next_it)
90  {
91  if(visited_nodes.find(next_it->first)!=visited_nodes.end())
92  continue;
93  visited_nodes.insert(next_it->first);
94 
95  old_path.push_back/*front*/(next_it->first);
96  const_graph_explore(egraph, next_it->first, end, old_path);
97  old_path.pop_back/*front*/();
98  }
99  }
100 }
101 
103  event_grapht &egraph,
104  event_idt next,
105  std::list<event_idt> &old_path,
106  std::set<unsigned> &edges,
107  bool porw)
108 {
109  /* TODO: restricts to C_1 U ... U C_n for perf improvement */
110  assert(!old_path.empty());
111 
112  fence_inserter.instrumenter.message.debug() << "(BC) explore "
113  << old_path.front()
114  << " --...--> " << next
115  << messaget::eom;
116 
117  if(visited_nodes.find(next)!=visited_nodes.end())
118  return;
119  visited_nodes.insert(next);
120 
121  /* if all the incoming pos were already visited, add */
122  bool no_other_pos = true;
123  for(wmm_grapht::edgest::const_iterator it=
124  egraph.po_out(next).begin();
125  it!=egraph.po_out(next).end();
126  ++it)
127  if(visited_nodes.find(it->first)==visited_nodes.end())
128  {
129  no_other_pos = false;
130  break;
131  }
132 
133  if(egraph.po_out(next).empty() || no_other_pos)
134  {
135  /* inserts all the pos collected from old_path in edges */
136  std::list<event_idt>::const_iterator it=old_path.begin();
137  std::list<event_idt>::const_iterator next_it=it;
138  ++next_it;
139  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
140  {
141  const abstract_eventt &e1=egraph[*it];
142  const abstract_eventt &e2=egraph[*next_it];
143  if(!porw ||
146  edges.insert(fence_inserter.add_edge(edget(*it, *next_it)));
147  }
148  assert(it!=old_path.end());
149  }
150  else
151  {
152  for(wmm_grapht::edgest::const_iterator
153  next_it=egraph.po_out(next).begin();
154  next_it!=egraph.po_out(next).end();
155  ++next_it)
156  {
157  old_path.push_back/*front*/(next_it->first);
158  graph_explore_BC(egraph, next_it->first, old_path, edges);
159  old_path.pop_back/*front*/();
160  }
161  }
162 }
163 
165  event_grapht &egraph,
166  event_idt next,
167  std::list<event_idt> &old_path)
168 {
169  /* TODO: restricts to C_1 U ... U C_n */
170  assert(old_path.size() > 0);
171 
172  if(visited_nodes.find(next)!=visited_nodes.end())
173  return;
174  visited_nodes.insert(next);
175 
176  /* if all the incoming pos were already visited, add */
177  bool no_other_pos = true;
178  for(wmm_grapht::edgest::const_iterator it=
179  egraph.po_out(next).begin();
180  it!=egraph.po_out(next).end();
181  ++it)
182  if(visited_nodes.find(it->first)==visited_nodes.end())
183  {
184  no_other_pos = false;
185  break;
186  }
187 
188  if(egraph.po_out(next).empty() || no_other_pos)
189  {
190  /* inserts all the pos collected from old_path in edges */
191  std::list<event_idt>::const_iterator it=old_path.begin();
192  std::list<event_idt>::const_iterator next_it=it;
193  ++next_it;
194  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
195  {
196  const abstract_eventt &e1=egraph[*it];
197  const abstract_eventt &e2=egraph[*next_it];
200  fence_inserter.add_edge(edget(*it, *next_it));
201  }
202  // NEW
203  assert(it!=old_path.end());
204  }
205  else
206  {
207  for(wmm_grapht::edgest::const_iterator
208  next_it=egraph.po_out(next).begin();
209  next_it!=egraph.po_out(next).end();
210  ++next_it)
211  {
212  old_path.push_back/*front*/(next_it->first);
213  const_graph_explore_BC(egraph, next_it->first, old_path);
214  old_path.pop_back/*front*/();
215  }
216  }
217 }
218 
220  event_grapht &egraph,
221  event_idt next,
222  std::list<event_idt> &old_path,
223  std::set<unsigned> &edges,
224  bool porw)
225 {
226  /* TODO: restricts to C_1 U ... U C_n */
227  assert(old_path.size() > 0);
228 
229  fence_inserter.instrumenter.message.debug() << "(AC) explore "
230  << old_path.front() << " --...--> " << next << messaget::eom;
231 
232  if(visited_nodes.find(next)!=visited_nodes.end())
233  return;
234  visited_nodes.insert(next);
235 
236  /* if all the incoming pos were already visited, add */
237  bool no_other_pos = true;
238  for(wmm_grapht::edgest::const_iterator it=
239  egraph.po_in(next).begin();
240  it!=egraph.po_in(next).end();
241  ++it)
242  if(visited_nodes.find(it->first)==visited_nodes.end())
243  {
244  no_other_pos = false;
245  break;
246  }
247 
248  if(egraph.po_in(next).empty() || no_other_pos)
249  {
250  /* inserts all the pos collected from old_path in edges */
251  std::list<event_idt>::const_iterator it=old_path.begin();
252  std::list<event_idt>::const_iterator next_it=it;
253  ++next_it;
254  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
255  {
256  const abstract_eventt &e1=egraph[*next_it];
257  const abstract_eventt &e2=egraph[*it];
258  if(!porw ||
261  edges.insert(fence_inserter.add_edge(edget(*next_it, *it)));
262  }
263  assert(it!=old_path.end());
264  }
265  else
266  {
267  for(wmm_grapht::edgest::const_iterator
268  next_it=egraph.po_in(next).begin();
269  next_it!=egraph.po_in(next).end();
270  ++next_it)
271  {
272  old_path.push_back/*front*/(next_it->first);
273  graph_explore_AC(egraph, next_it->first, old_path, edges);
274  old_path.pop_back/*front*/();
275  }
276  }
277 }
278 
280  event_grapht &egraph,
281  event_idt next,
282  std::list<event_idt> &old_path)
283 {
284  /* TODO: restricts to C_1 U ... U C_n */
285  assert(old_path.size() > 0);
286 
287  if(visited_nodes.find(next)!=visited_nodes.end())
288  return;
289  visited_nodes.insert(next);
290 
291  /* if all the incoming pos were already visited, add */
292  bool no_other_pos = true;
293  for(wmm_grapht::edgest::const_iterator it=
294  egraph.po_in(next).begin();
295  it!=egraph.po_in(next).end();
296  ++it)
297  if(visited_nodes.find(it->first)==visited_nodes.end())
298  {
299  no_other_pos = false;
300  break;
301  }
302 
303  /* if beginning of the thread */
304  if(egraph.po_in(next).empty() || no_other_pos)
305  {
306  /* inserts all the pos collected from old_path in edges */
307  std::list<event_idt>::const_iterator it=old_path.begin();
308  std::list<event_idt>::const_iterator next_it=it;
309  ++next_it;
310  for( ; next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
311  {
312  const abstract_eventt &e1=egraph[*next_it];
313  const abstract_eventt &e2=egraph[*it];
316  fence_inserter.add_edge(edget(*next_it, *it));
317  }
318  // NEW
319  assert(it!=old_path.end());
320  }
321  else
322  {
323  for(wmm_grapht::edgest::const_iterator
324  next_it=egraph.po_in(next).begin();
325  next_it!=egraph.po_in(next).end();
326  ++next_it)
327  {
328  old_path.push_back/*front*/(next_it->first);
329  const_graph_explore_AC(egraph, next_it->first, old_path);
330  old_path.pop_back/*front*/();
331  }
332  }
333 }
334 
336  const edget &e,
337  std::set<unsigned> &edges)
338 {
339  visited_nodes.clear();
340 
341 // if(!e.is_po) /* e is in po^+\po */ is_po is a flag set manually, do not
342 // use it for checks!!
343  const wmm_grapht::edgest &list_po_out=
345  if(list_po_out.find(e.second)==list_po_out.end())
346  {
347 #ifdef BTWN1
349 
351  for(wmm_grapht::edgest::const_iterator
352  next_it=egraph.po_out(e.first).begin();
353  next_it!=egraph.po_out(e.first).end();
354  ++next_it)
355  {
356  std::list<event_idt> new_path;
357  new_path.push_back(e.first);
358  new_path.push_back(next_it->first);
359  graph_explore(egraph, next_it->first, e.second, new_path, edges);
360  }
361 #elif defined BTWN4
362  /* all the pos+ intersections inbetween */
363  /* TODO */
364  /* when detecting intersections, add them to a map thread->edges
365  then for BTWN4, enumerates all the edges of the thread of e and
366  check whether e.first-po-> edge.first /\ edge.second-po->e.second,
367  using egraph.are_po_ordered. */
368 #else
369  throw "BTWN definition not selected!"; // NOLINT(readability/throw)
370 #endif
371  }
372  else
373  /* reflexive -- only when in pos */
374  edges.insert(fence_inserter.map_from_e[e]);
375 }
376 
380  const edget &edge,
381  std::set<unsigned> &edges)
382 {
384 
385  /* the edge can be in the reversed order (back-edge) */
386  const abstract_eventt &test_first=egraph[edge.first];
387  const abstract_eventt &test_second=egraph[edge.second];
388  assert(test_first.operation!=test_second.operation);
389 
390  const event_idt first=
392  edge.first:
393  edge.second);
394  const event_idt second=
396  edge.second:
397  edge.first);
398 
399  /* TODO: AC + restricts to C_1 U ... U C_n */
400  visited_nodes.clear();
401 
402  /* if one event only on this thread of the cycle, discard */
403  if(!egraph.po_in(first).empty())
404  {
405  for(wmm_grapht::edgest::const_iterator
406  next_it=egraph.po_in(first).begin();
407  next_it!=egraph.po_in(first).end();
408  ++next_it)
409  {
410  std::list<event_idt> new_path;
411  new_path.push_back(first);
412  new_path.push_back(next_it->first);
413  graph_explore_AC(egraph, next_it->first, new_path, edges);
414  }
415  }
416 
417  if(!egraph.po_out(second).empty())
418  {
419  for(wmm_grapht::edgest::const_iterator
420  next_it=egraph.po_out(second).begin();
421  next_it!=egraph.po_out(second).end();
422  ++next_it)
423  {
424  std::list<event_idt> new_path;
425  new_path.push_back(second);
426  new_path.push_back(next_it->first);
427  graph_explore_BC(egraph, next_it->first, new_path, edges);
428  }
429  }
430 }
431 
435  const edget &edge,
436  std::set<unsigned> &edges)
437 {
439 
440  /* the edge can be in the reversed order (back-edge) */
441  const abstract_eventt &test_first=egraph[edge.first];
442  const abstract_eventt &test_second=egraph[edge.second];
443  assert(test_first.operation!=test_second.operation);
444 
445  const event_idt first=
447  edge.first:
448  edge.second);
449  const event_idt second=
451  edge.second:
452  edge.first);
453 
454  /* TODO: AC + restricts to C_1 U ... U C_n */
455  visited_nodes.clear();
456 
457  if(!egraph.po_in(first).empty())
458  {
459  for(wmm_grapht::edgest::const_iterator
460  next_it=egraph.po_in(first).begin();
461  next_it!=egraph.po_in(first).end();
462  ++next_it)
463  {
464  std::list<event_idt> new_path;
465  new_path.push_back(first);
466  new_path.push_back(next_it->first);
467  graph_explore_AC(egraph, next_it->first, new_path, edges, true);
468  }
469  }
470 
471  if(!egraph.po_out(second).empty())
472  {
473  for(wmm_grapht::edgest::const_iterator
474  next_it=egraph.po_out(second).begin();
475  next_it!=egraph.po_out(second).end();
476  ++next_it)
477  {
478  std::list<event_idt> new_path;
479  new_path.push_back(second);
480  new_path.push_back(next_it->first);
481  graph_explore_BC(egraph, next_it->first, new_path, edges, true);
482  }
483  }
484 }
std::map< edget, unsigned > & map_from_e
messaget & message
Definition: goto2graph.h:280
operationt operation
bool has_po_edge(event_idt i, event_idt j) const
Definition: event_graph.h:380
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void CT_not_powr(const edget &e, std::set< unsigned > &edges)
const wmm_grapht::edgest & po_out(event_idt n) const
Definition: event_graph.h:400
void CT(const edget &e, std::set< unsigned > &edges)
event_grapht::critical_cyclet::delayt edget
Definition: graph_visitor.h:25
fence_insertert & fence_inserter
Definition: graph_visitor.h:27
unsigned add_edge(const edget &e)
const wmm_grapht::edgest & po_in(event_idt n) const
Definition: event_graph.h:395
wmm_grapht::node_indext event_idt
Definition: event_graph.h:32
void graph_explore(event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path, std::set< unsigned > &edges)
void const_graph_explore(event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path)
mstreamt & debug()
Definition: message.h:253
void graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw)
graph visitor for computing edges involved for fencing
ILP construction for all cycles and resolution.
void graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw)
nodet::edgest edgest
Definition: graph.h:136
instrumentert & instrumenter
event_grapht egraph
Definition: goto2graph.h:283
void const_graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
void const_graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
void PT(const edget &e, std::set< unsigned > &edges)
std::set< event_idt > visited_nodes
Definition: graph_visitor.h:28