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