CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
20#ifdef DEBUG
21# include <util/message.h>
22#endif
23
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,
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,
51 it->eq_class));
52 continue;
53 }
54 }
55
56 if(it==data.cend())
57 {
58 ++class_nb;
59 data.insert(
61 data.insert(
63 }
64}
65
67 const abstract_eventt &read,
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
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
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
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 events
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
data_typet data
Definition data_dp.h:54
void dp_merge()
merge in N^3
Definition data_dp.cpp:121
void print(messaget &message)
Definition data_dp.cpp:164
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
Definition data_dp.cpp:76
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Definition data_dp.cpp:66
unsigned class_nb
Definition data_dp.h:55
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
static eomt eom
Definition message.h:289
data dependencies
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition unistd.c:195