cprover
data_dp.h
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 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
16 
17 #include <set>
18 
19 #include <util/source_location.h>
20 
21 class abstract_eventt;
22 class messaget;
23 
24 struct datat
25 {
28  mutable unsigned eq_class;
29 
30  datat(irep_idt _id, source_locationt _loc, unsigned _eq_class)
31  : id(_id), loc(_loc), eq_class(_eq_class)
32  {
33  }
34 
36  : id(_id), loc(_loc), eq_class(0)
37  {
38  }
39 
40  bool operator==(const datat &d) const
41  {
42  return id==d.id && loc==d.loc;
43  }
44 
45  bool operator<(const datat &d2) const
46  {
47  return id<d2.id || (id==d2.id && loc<d2.loc);
48  }
49 };
50 
51 class data_dpt:public std::set<datat>
52 {
53 public:
54  unsigned class_nb;
55 
56  /* add this dependency in the structure */
57  void dp_analysis(const abstract_eventt &read, const abstract_eventt &write);
58  void dp_analysis(
59  const datat &read,
60  bool local_read,
61  const datat &write,
62  bool local_write);
63 
64  /* are these two events with a data dependency ? */
65  bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const;
66 
67  /* routine to maintain partitioning */
68  void dp_merge();
69 
70  /* printing */
71  void print(messaget &message);
72 };
73 
74 #endif // CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
irep_idt id
Definition: data_dp.h:26
unsigned eq_class
Definition: data_dp.h:28
void print(messaget &message)
Definition: data_dp.cpp:160
bool operator==(const datat &d) const
Definition: data_dp.h:40
bool operator<(const datat &d2) const
Definition: data_dp.h:45
datat(irep_idt _id, source_locationt _loc, unsigned _eq_class)
Definition: data_dp.h:30
void dp_merge()
merge in N^3
Definition: data_dp.cpp:117
Definition: data_dp.h:24
source_locationt loc
Definition: data_dp.h:27
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Definition: data_dp.cpp:62
datat(irep_idt _id, source_locationt _loc)
Definition: data_dp.h:35
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
Definition: data_dp.cpp:72
unsigned class_nb
Definition: data_dp.h:54