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 
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,
36  (local_write?source_locationt():write.loc),
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,
46  (local_read?source_locationt():read.loc),
47  it->eq_class));
48  continue;
49  }
50  }
51 
52  if(it==data.cend())
53  {
54  ++class_nb;
55  data.insert(
56  datat(read.id, (local_read?source_locationt():read.loc), class_nb));
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 {
66  datat d_read(read.variable, read.source_location);
67  datat d_write(write.variable, write.source_location);
68  dp_analysis(d_read, read.local, d_write, write.local);
69 }
70 
72 bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
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 
160 void data_dpt::print(messaget &message)
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 }
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:117
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
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:160
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:72
abstract_eventt
Definition: abstract_event.h:23
source_locationt
Definition: source_location.h:19
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:62
abstract_eventt::local
bool local
Definition: abstract_event.h:38
messaget::debug
mstreamt & debug() const
Definition: message.h:429
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423