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 }
event_grapht::com_out
const wmm_grapht::edgest & com_out(event_idt n) const
Definition: event_graph.h:448
abstract_eventt::source_location
source_locationt source_location
Definition: abstract_event.h:36
event_grapht::graph_pensieve_explorert::find_second_event
bool find_second_event(event_idt source)
Definition: pair_collection.cpp:67
abstract_eventt::variable
irep_idt variable
Definition: abstract_event.h:34
event_grapht::graph_explorert::egraph
event_grapht & egraph
Definition: event_graph.h:257
event_grapht::graph_pensieve_explorert::visited_nodes
std::set< event_idt > visited_nodes
Definition: event_graph.h:366
event_graph.h
messaget::eom
static eomt eom
Definition: message.h:297
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:45
OUTPUT
#define OUTPUT(s, fence, file, line, id, type)
Definition: pair_collection.cpp:22
event_idt
wmm_grapht::node_indext event_idt
Definition: event_graph.h:32
event_grapht::graph_pensieve_explorert::naive
bool naive
Definition: event_graph.h:367
event_grapht::po_order
std::list< event_idt > po_order
Definition: event_graph.h:400
abstract_eventt
Definition: abstract_event.h:22
event_grapht::graph_pensieve_explorert::collect_pairs
void collect_pairs()
Definition: pair_collection.cpp:25
event_grapht::message
messaget & message
Definition: event_graph.h:394
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:35
messaget::debug
mstreamt & debug() const
Definition: message.h:429
abstract_eventt::operation
operationt operation
Definition: abstract_event.h:32
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404