CBMC
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 
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 
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 
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 events
source_locationt source_location
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
Definition: data_dp.h:25
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:195