cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
data_dp.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: data dependencies
4
5
Author: Vincent Nimal
6
7
Date: 2012
8
9
\*******************************************************************/
10
13
14
#include "
data_dp.h
"
15
16
#include <
util/invariant.h
>
17
18
#include "
abstract_event.h
"
19
20
#ifdef DEBUG
21
# include <
util/message.h
>
22
#endif
23
25
void
data_dpt::dp_analysis
(
26
const
datat
&read,
27
bool
local_read,
28
const
datat
&write,
29
bool
local_write)
30
{
31
data_typet::const_iterator it;
32
33
for
(it=
data
.cbegin(); it!=
data
.cend(); ++it)
34
{
35
if
(local_read && it->id==read.
id
)
36
{
37
data
.insert(
38
datat
(
39
write.
id
,
40
(local_write?
source_locationt
():write.
loc
),
41
it->eq_class));
42
continue
;
43
}
44
45
if
(local_write && it->id==write.
id
)
46
{
47
data
.insert(
48
datat
(
49
read.
id
,
50
(local_read?
source_locationt
():read.
loc
),
51
it->eq_class));
52
continue
;
53
}
54
}
55
56
if
(it==
data
.cend())
57
{
58
++
class_nb
;
59
data
.insert(
60
datat
(read.
id
, (local_read?
source_locationt
():read.
loc
),
class_nb
));
61
data
.insert(
62
datat
(write.
id
, (local_write?
source_locationt
():write.
loc
),
class_nb
));
63
}
64
}
65
66
void
data_dpt::dp_analysis
(
67
const
abstract_eventt
&read,
68
const
abstract_eventt
&write)
69
{
70
datat
d_read(read.
variable
, read.
source_location
);
71
datat
d_write(write.
variable
, write.
source_location
);
72
dp_analysis
(d_read, read.
local
, d_write, write.
local
);
73
}
74
76
bool
data_dpt::dp
(
const
abstract_eventt
&e1,
const
abstract_eventt
&e2)
const
77
{
78
for
(
auto
it1=
data
.cbegin(); it1!=
data
.cend(); ++it1)
79
{
80
auto
it2=it1;
81
++it2;
82
if
(it2==
data
.cend())
83
break
;
84
85
if
(e1.
local
)
86
{
87
if
(it1->id != e1.
variable
)
88
continue
;
89
}
90
else
91
{
92
if
(it1->id!=e1.
variable
|| it1->loc!=e1.
source_location
)
93
continue
;
94
}
95
96
for
(; it2!=
data
.cend(); ++it2)
97
{
98
if
(e2.
local
)
99
{
100
if
(it2->id!=e2.
variable
)
101
continue
;
102
}
103
else
104
{
105
if
(it2->id!=e2.
variable
|| it2->loc!=e2.
source_location
)
106
continue
;
107
}
108
/* or else, same class */
109
if
(it1->eq_class==it2->eq_class)
110
{
111
// message.debug() << e1<<"-dp->"<<e2 << messaget::eom;
112
return
true
;
113
}
114
}
115
}
116
// message.debug() << e1<<"-x->"<<e2 << messaget::eom;
117
return
false
;
118
}
119
121
void
data_dpt::dp_merge
()
122
{
123
if
(
data
.size()<2)
124
return
;
125
126
unsigned
initial_size=
data
.size();
127
128
unsigned
from=0;
129
unsigned
to=0;
130
131
/* look for similar elements */
132
for
(
auto
it1=
data
.cbegin(); it1!=
data
.cend(); ++it1)
133
{
134
auto
it2=it1;
135
++it2;
136
/* all ok -- ends */
137
if
(it2==
data
.cend())
138
return
;
139
140
for
(; it2!=
data
.cend(); ++it2)
141
{
142
if
(it1 == it2)
143
{
144
from=it2->eq_class;
145
to=it1->eq_class;
146
data
.erase(it2);
147
break
;
148
}
149
}
150
}
151
152
/* merge */
153
for
(
auto
it3=
data
.begin(); it3!=
data
.end(); ++it3)
154
if
(it3->eq_class==from)
155
it3->eq_class=to;
156
157
/* strictly monotonous => converges */
158
INVARIANT
(initial_size>
data
.size(),
"strictly monotonous => converges"
);
159
160
/* repeat until classes are disjunct */
161
dp_merge
();
162
}
163
164
void
data_dpt::print
(
messaget
&message)
165
{
166
#ifdef DEBUG
167
data_typet::const_iterator it;
168
std::map<unsigned, std::set<source_locationt> > classed;
169
170
for
(it=
data
.cbegin(); it!=
data
.cend(); ++it)
171
{
172
if
(classed.find(it->eq_class)==classed.end())
173
{
174
std::set<source_locationt> s;
175
s.insert(it->loc);
176
classed[it->eq_class]=s;
177
}
178
else
179
classed[it->eq_class].insert(it->loc);
180
}
181
182
for
(std::map<
unsigned
, std::set<source_locationt> >::const_iterator
183
m_it=classed.begin();
184
m_it!=classed.end(); ++m_it)
185
{
186
message.
debug
() <<
"class #"
<<m_it->first <<
messaget::eom
;
187
std::set<source_locationt>::const_iterator l_it;
188
for
(l_it=m_it->second.begin(); l_it!=m_it->second.end(); ++l_it)
189
message.
debug
()<<
"loc: "
<<*l_it <<
messaget::eom
;
190
}
191
#else
192
(void)message;
// unused parameter
193
#endif
194
}
abstract_event.h
abstract events
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::local
bool local
Definition
abstract_event.h:38
data_dpt::data
data_typet data
Definition
data_dp.h:54
data_dpt::dp_merge
void dp_merge()
merge in N^3
Definition
data_dp.cpp:121
data_dpt::print
void print(messaget &message)
Definition
data_dp.cpp:164
data_dpt::dp
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
Definition
data_dp.cpp:76
data_dpt::dp_analysis
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Definition
data_dp.cpp:66
data_dpt::class_nb
unsigned class_nb
Definition
data_dp.h:55
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::debug
mstreamt & debug() const
Definition
message.h:421
messaget::eom
static eomt eom
Definition
message.h:289
source_locationt
Definition
source_location.h:20
data_dp.h
data dependencies
invariant.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
message.h
datat
Definition
data_dp.h:25
datat::id
irep_idt id
Definition
data_dp.h:26
datat::loc
source_locationt loc
Definition
data_dp.h:27
goto-instrument
wmm
data_dp.cpp
Generated by
1.17.0