cprover
reference_counting.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Reference Counting
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_REFERENCE_COUNTING_H
13 #define CPROVER_UTIL_REFERENCE_COUNTING_H
14 
15 #include "invariant.h"
16 
17 template<typename T>
18 // NOLINTNEXTLINE(readability/identifiers)
20 {
21 public:
22  reference_counting():d(nullptr)
23  {
24  }
25 
26  explicit reference_counting(const T &other):d(NULL)
27  {
28  write()=other;
29  }
30 
31  // copy constructor
33  {
34  if(d!=nullptr)
35  {
36  PRECONDITION(d->ref_count != 0);
37  d->ref_count++;
38  #ifdef REFERENCE_COUNTING_DEBUG
39  std::cout << "COPY " << d << " " << d->ref_count << '\n';
40  #endif
41  }
42  }
43 
45  {
46  copy_from(other);
47  return *this;
48  }
49 
51  {
52  remove_ref(d);
53  d=nullptr;
54  }
55 
56  void swap(reference_counting &other)
57  {
58  std::swap(other.d, d);
59  }
60 
61  void clear()
62  {
63  remove_ref(d);
64  d=nullptr;
65  }
66 
67  const T &read() const
68  {
69  if(d==nullptr)
70  return T::blank;
71  return *d;
72  }
73 
74  T &write()
75  {
76  detach();
77  return *d;
78  }
79 
80 protected:
81  class dt:public T
82  {
83  public:
84  unsigned ref_count;
85 
87  {
88  }
89  };
90 
91  dt *d;
92 
93  void remove_ref(dt *old_d);
94 
95  void detach();
96 
97  void copy_from(const reference_counting &other)
98  {
99  PRECONDITION(&other != this); // check if we assign to ourselves
100 
101  #ifdef REFERENCE_COUNTING_DEBUG
102  std::cout << "COPY " << (&other) << "\n";
103  #endif
104 
105  remove_ref(d);
106  d=other.d;
107  if(d!=nullptr)
108  d->ref_count++;
109  }
110 
111 public:
112  dt *get_d() const
113  {
114  return d;
115  }
116 };
117 
118 template<class T>
120 {
121  if(old_d==nullptr)
122  return;
123 
124  PRECONDITION(old_d->ref_count != 0);
125 
126  #ifdef REFERENCE_COUNTING_DEBUG
127  std::cout << "R: " << old_d << " " << old_d->ref_count << '\n';
128  #endif
129 
130  old_d->ref_count--;
131  if(old_d->ref_count==0)
132  {
133  #ifdef REFERENCE_COUNTING_DEBUG
134  std::cout << "DELETING " << old_d << '\n';
135  old_d->clear();
136  std::cout << "DEALLOCATING " << old_d << "\n";
137  #endif
138 
139  delete old_d;
140 
141  #ifdef REFERENCE_COUNTING_DEBUG
142  std::cout << "DONE\n";
143  #endif
144  }
145 }
146 
147 template<class T>
149 {
150  #ifdef REFERENCE_COUNTING_DEBUG
151  std::cout << "DETACH1: " << d << '\n';
152  #endif
153 
154  if(d==nullptr)
155  {
156  d=new dt;
157 
158  #ifdef REFERENCE_COUNTING_DEBUG
159  std::cout << "ALLOCATED " << d << '\n';
160  #endif
161  }
162  else if(d->ref_count>1)
163  {
164  dt *old_d(d);
165  d=new dt(*old_d);
166 
167  #ifdef REFERENCE_COUNTING_DEBUG
168  std::cout << "ALLOCATED " << d << '\n';
169  #endif
170 
171  d->ref_count=1;
172  remove_ref(old_d);
173  }
174 
175  POSTCONDITION(d->ref_count == 1);
176 
177  #ifdef REFERENCE_COUNTING_DEBUG
178  std::cout << "DETACH2: " << d << '\n'
179  #endif
180 }
181 
182 template<class T>
184  const reference_counting<T> &o1,
185  const reference_counting<T> &o2)
186 {
187  if(o1.get_d()==o2.get_d())
188  return true;
189  return o1.read()==o2.read();
190 }
191 
192 template<class T>
193 inline bool operator!=(
194  const reference_counting<T> &i1,
195  const reference_counting<T> &i2)
196 { return !(i1==i2); }
197 
198 #endif // CPROVER_UTIL_REFERENCE_COUNTING_H
void swap(reference_counting &other)
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
reference_counting(const reference_counting &other)
reference_counting & operator=(const reference_counting &other)
reference_counting(const T &other)
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
void remove_ref(dt *old_d)
bool operator!=(const reference_counting< T > &i1, const reference_counting< T > &i2)
const T & read() const
bool operator==(const reference_counting< T > &o1, const reference_counting< T > &o2)
void copy_from(const reference_counting &other)