cprover
abstract_event.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: abstract events
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
16 
17 #include <util/source_location.h>
18 #include <util/graph.h>
19 
20 #include "wmm.h"
21 
22 class abstract_eventt:public graph_nodet<empty_edget>
23 {
24 protected:
26  memory_modelt model, bool lwsync_met) const;
27 
28 public:
29  /* for now, both fence functions and asm fences accepted */
30  enum class operationt { Write, Read, Fence, Lwfence, ASMfence };
31 
33  unsigned thread;
35  unsigned id;
37  bool local;
38 
39  // for ASMfence
40  bool WRfence;
41  bool WWfence;
42  bool RRfence;
43  bool RWfence;
44  bool WWcumul;
45  bool RWcumul;
46  bool RRcumul;
47 
49  operation(operationt::Write),
50  thread(0),
51  id(0),
52  local(false),
53  WRfence(false),
54  WWfence(false),
55  RRfence(false),
56  RWfence(false),
57  WWcumul(false),
58  RWcumul(false),
59  RRcumul(false)
60  {
61  }
62 
64  operationt _op, unsigned _th, irep_idt _var,
65  unsigned _id, source_locationt _loc, bool _local)
66  :operation(_op), thread(_th), variable(_var), id(_id),
67  source_location(_loc), local(_local)
68  {
69  }
70 
72  operationt _op,
73  unsigned _th,
74  irep_idt _var,
75  unsigned _id,
76  source_locationt _loc,
77  bool _local,
78  bool WRf,
79  bool WWf,
80  bool RRf,
81  bool RWf,
82  bool WWc,
83  bool RWc,
84  bool RRc):
85  operation(_op),
86  thread(_th),
87  variable(_var),
88  id(_id),
89  source_location(_loc),
90  local(_local),
91  WRfence(RWf),
92  WWfence(WWf),
93  RRfence(RRf),
94  RWfence(WRf),
95  WWcumul(WWc),
96  RWcumul(RWc),
97  RRcumul(RRc)
98  {
99  }
100 
101  /* post declaration (through graph) -- doesn't copy */
102  void operator()(const abstract_eventt &other)
103  {
104  operation=other.operation;
105  thread=other.thread;
106  variable=other.variable;
107  id=other.id;
109  local=other.local;
110  }
111 
112  bool operator==(const abstract_eventt &other) const
113  {
114  return (id == other.id);
115  }
116 
117  bool operator<(const abstract_eventt &other) const
118  {
119  return (id < other.id);
120  }
121 
122  bool is_fence() const
123  {
124  return operation==operationt::Fence ||
127  }
128 
129  /* checks the safety of the pair locally (i.e., w/o taking fences
130  or dependencies into account -- use is_unsafe on the whole
131  critical cycle for this) */
132  bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
133  {
134  return unsafe_pair_lwfence_param(next, model, false);
135  }
136 
138  const abstract_eventt &next,
139  memory_modelt model) const
140  {
141  return unsafe_pair_lwfence_param(next, model, true);
142  }
143 
144  bool unsafe_pair_asm(
145  const abstract_eventt &next,
146  memory_modelt model,
147  unsigned char met) const;
148 
149  std::string get_operation() const
150  {
151  switch(operation)
152  {
153  case operationt::Write: return "W";
154  case operationt::Read: return "R";
155  case operationt::Fence: return "F";
156  case operationt::Lwfence: return "f";
157  case operationt::ASMfence: return "asm:";
158  }
159  assert(false);
160  return "?";
161  }
162 
164  const abstract_eventt &second) const
165  {
166  return
167  (WRfence &&
168  first.operation==operationt::Write &&
169  second.operation==operationt::Read) ||
170  ((WWfence || WWcumul) &&
171  first.operation==operationt::Write &&
172  second.operation==operationt::Write) ||
173  ((RWfence || RWcumul) &&
174  first.operation==operationt::Read &&
175  second.operation==operationt::Write) ||
176  ((RRfence || RRcumul) &&
177  first.operation==operationt::Read &&
178  second.operation==operationt::Read);
179  }
180 
181  bool is_direct() const { return WWfence || WRfence || RRfence || RWfence; }
182  bool is_cumul() const { return WWcumul || RWcumul || RRcumul; }
183 
184  unsigned char fence_value() const
185  {
186  return uc(WRfence) + 2u * uc(WWfence) + 4u * uc(RRfence) +
187  8u * uc(RWfence) + 16u * uc(WWcumul) + 32u * uc(RWcumul) +
188  64u * uc(RRcumul);
189  }
190 
191 private:
192  static unsigned char uc(bool truth_value)
193  {
194  return truth_value ? 1u : 0u;
195  }
196 };
197 
198 inline std::ostream &operator<<(
199  std::ostream &s,
200  const abstract_eventt &e)
201 {
202  return s << e.get_operation() << e.variable;
203 }
204 
205 #endif // CPROVER_GOTO_INSTRUMENT_WMM_ABSTRACT_EVENT_H
memory models
bool unsafe_pair_lwfence_param(const abstract_eventt &next, memory_modelt model, bool lwsync_met) const
bool operator<(const abstract_eventt &other) const
bool unsafe_pair_asm(const abstract_eventt &next, memory_modelt model, unsigned char met) const
operationt operation
bool is_fence() const
bool is_cumul() const
bool unsafe_pair(const abstract_eventt &next, memory_modelt model) const
unsigned char fence_value() const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local, bool WRf, bool WWf, bool RRf, bool RWf, bool WWc, bool RWc, bool RRc)
memory_modelt
Definition: wmm.h:17
void operator()(const abstract_eventt &other)
bool is_corresponding_fence(const abstract_eventt &first, const abstract_eventt &second) const
bool unsafe_pair_lwfence(const abstract_eventt &next, memory_modelt model) const
abstract_eventt(operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local)
std::string get_operation() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool operator==(const abstract_eventt &other) const
A Template Class for Graphs.
static unsigned char uc(bool truth_value)
bool is_direct() const
source_locationt source_location
This class represents a node in a directed graph.
Definition: graph.h:35
std::ostream & operator<<(std::ostream &s, const abstract_eventt &e)