cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
25
void
event_grapht::graph_pensieve_explorert::collect_pairs
()
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
67
bool
event_grapht::graph_pensieve_explorert::find_second_event
(
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
}
abstract_eventt
Definition
abstract_event.h:23
abstract_eventt::source_location
source_locationt source_location
Definition
abstract_event.h:36
abstract_eventt::variable
irep_idt variable
Definition
abstract_event.h:34
abstract_eventt::operation
operationt operation
Definition
abstract_event.h:32
event_grapht::graph_explorert::egraph
event_grapht & egraph
Definition
event_graph.h:257
event_grapht::graph_pensieve_explorert::collect_pairs
void collect_pairs()
Definition
pair_collection.cpp:25
event_grapht::graph_pensieve_explorert::find_second_event
bool find_second_event(event_idt source)
Definition
pair_collection.cpp:67
event_grapht::graph_pensieve_explorert::visited_nodes
std::set< event_idt > visited_nodes
Definition
event_graph.h:366
event_grapht::graph_pensieve_explorert::naive
bool naive
Definition
event_graph.h:367
messaget::eom
static eomt eom
Definition
message.h:289
source_locationt::get_file
const irep_idt & get_file() const
Definition
source_location.h:36
source_locationt::get_line
const irep_idt & get_line() const
Definition
source_location.h:46
event_graph.h
graph of abstract events
event_idt
wmm_grapht::node_indext event_idt
Definition
event_graph.h:32
OUTPUT
#define OUTPUT(s, fence, file, line, id, type)
Definition
pair_collection.cpp:22
message.h
goto-instrument
wmm
pair_collection.cpp
Generated by
1.17.0