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