CBMC
pair_collection.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: collection of pairs (for Pensieve's static delay-set
4  analysis) in graph of abstract events
5 
6 Author:
7 
8 Date: 2013
9 
10 \*******************************************************************/
11 
15 
16 #include "event_graph.h"
17 
18 #include <fstream>
19 
20 #include <util/message.h>
21 
22 #define OUTPUT(s, fence, file, line, id, type) \
23  s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'
24 
26 {
27  std::ofstream res;
28  res.open("results.txt");
29 
30  for(std::list<event_idt>::const_iterator st_it=egraph.po_order.begin();
31  st_it!=egraph.po_order.end(); ++st_it)
32  {
33  /* pick X */
34  event_idt first=*st_it;
35  egraph.message.debug() << "first: " << egraph[first].id << messaget::eom;
36 
37  if(visited_nodes.find(first)!=visited_nodes.end())
38  continue;
39 
40  /* by rules (1) + (3), we must have X --cmp-- A */
41  if(egraph.com_out(first).empty() && !naive)
42  continue;
43 
44  /* find Y s.t. X --po-- Y and Y --cmp-- B, by rules (2) + (4) */
45  if(find_second_event(first))
46  {
47  const abstract_eventt &first_event=egraph[first];
48 
49  try
50  {
51  /* directly outputs */
52  OUTPUT(res, "fence", first_event.source_location.get_file(),
53  first_event.source_location.get_line(), first_event.variable,
54  static_cast<int>(first_event.operation));
55  }
56  catch(const std::string &s)
57  {
58  egraph.message.warning() << "failed to find" << s << messaget::eom;
59  continue;
60  }
61  }
62  }
63 
64  res.close();
65 }
66 
68  event_idt current)
69 {
70  if(visited_nodes.find(current)!=visited_nodes.end())
71  return false;
72 
73  visited_nodes.insert(current);
74 
75  for(wmm_grapht::edgest::const_iterator
76  it=egraph.po_out(current).begin();
77  it!=egraph.po_out(current).end(); ++it)
78  {
79  if(naive || !egraph.com_out(it->first).empty())
80  return true;
81 
82  if(find_second_event(it->first))
83  return true;
84  }
85 
86  return false;
87 }
source_locationt source_location
operationt operation
std::set< event_idt > visited_nodes
Definition: event_graph.h:366
std::list< event_idt > po_order
Definition: event_graph.h:400
const wmm_grapht::edgest & com_out(event_idt n) const
Definition: event_graph.h:448
messaget & message
Definition: event_graph.h:394
mstreamt & warning() const
Definition: message.h:396
mstreamt & debug() const
Definition: message.h:421
static eomt eom
Definition: message.h:289
const irep_idt & get_line() const
const irep_idt & get_file() const
graph of abstract events
wmm_grapht::node_indext event_idt
Definition: event_graph.h:32
#define OUTPUT(s, fence, file, line, id, type)