Skip to content

Commit 4e97880

Browse files
committed
Use small intrusive pointer in irep
1 parent 9749321 commit 4e97880

File tree

4 files changed

+507
-297
lines changed

4 files changed

+507
-297
lines changed

src/util/cow.h

+235
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
/*******************************************************************\
2+
3+
Module: Copy on write class
4+
5+
Author: Reuben Thomas, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_COW_H
10+
#define CPROVER_UTIL_COW_H
11+
12+
#include "util/small_shared_ptr.h"
13+
#include "util/invariant.h"
14+
15+
#include <limits>
16+
17+
template <typename T>
18+
class copy_on_writet final
19+
{
20+
public:
21+
// Note that this *is* the default constructor. An invariant of a
22+
// copy-on-write object is that it is never null.
23+
template <typename... Ts>
24+
explicit copy_on_writet(Ts &&... ts)
25+
: t_(make_small_shared_ptr<T>(std::forward<Ts>(ts)...))
26+
{
27+
INVARIANT(
28+
pointee_is_shareable(*t_),
29+
"newly-constructed COW pointers must be shareable");
30+
}
31+
32+
copy_on_writet(const copy_on_writet &rhs)
33+
: t_(
34+
pointee_is_shareable(*rhs.t_) ? rhs.t_
35+
: make_small_shared_ptr<T>(*rhs.t_))
36+
{
37+
INVARIANT(
38+
pointee_is_shareable(*t_),
39+
"newly-constructed COW pointers must be shareable");
40+
}
41+
42+
copy_on_writet &operator=(const copy_on_writet &rhs)
43+
{
44+
auto copy(rhs);
45+
swap(copy);
46+
return *this;
47+
}
48+
49+
copy_on_writet(copy_on_writet &&rhs)
50+
{
51+
swap(rhs);
52+
}
53+
54+
copy_on_writet &operator=(copy_on_writet &&rhs)
55+
{
56+
swap(rhs);
57+
return *this;
58+
}
59+
60+
~copy_on_writet() = default; // delete if the refcount is 1, like usual
61+
62+
void swap(copy_on_writet &rhs)
63+
{
64+
std::swap(t_, rhs.t_);
65+
}
66+
67+
const T &read() const
68+
{
69+
return *t_;
70+
}
71+
72+
T &write(bool mark_shareable)
73+
{
74+
if(pointee_use_count(*t_) != 1)
75+
{
76+
t_ = make_small_shared_ptr<T>(*t_);
77+
}
78+
INVARIANT(
79+
pointee_use_count(*t_) == 1,
80+
"mutable references to a COW pointer must be unique");
81+
pointee_set_shareable(*t_, mark_shareable);
82+
INVARIANT(
83+
pointee_is_shareable(*t_) == mark_shareable,
84+
"sharing flag must have expected value after obtaining mutable ref");
85+
return *t_;
86+
}
87+
88+
// Ideally these would be non-members, but they depend on private member t_
89+
90+
template <typename U>
91+
bool operator==(const copy_on_writet<U> &rhs) const
92+
{
93+
return t_ == rhs.t_;
94+
}
95+
96+
template <typename U>
97+
bool operator!=(const copy_on_writet<U> &rhs) const
98+
{
99+
return t_ != rhs.t_;
100+
}
101+
102+
template <typename U>
103+
bool operator<(const copy_on_writet<U> &rhs) const
104+
{
105+
return t_ < rhs.t_;
106+
}
107+
108+
template <typename U>
109+
bool operator>(const copy_on_writet<U> &rhs) const
110+
{
111+
return t_ > rhs.t_;
112+
}
113+
114+
template <typename U>
115+
bool operator<=(const copy_on_writet<U> &rhs) const
116+
{
117+
return t_ <= rhs.t_;
118+
}
119+
120+
template <typename U>
121+
bool operator>=(const copy_on_writet<U> &rhs) const
122+
{
123+
return t_ >= rhs.t_;
124+
}
125+
126+
private:
127+
small_shared_ptrt<T> t_;
128+
};
129+
130+
////////////////////////////////////////////////////////////////////////////////
131+
132+
template <typename Num>
133+
class copy_on_write_pointeet
134+
{
135+
public:
136+
copy_on_write_pointeet() = default;
137+
138+
copy_on_write_pointeet(const copy_on_write_pointeet &)
139+
{
140+
}
141+
142+
copy_on_write_pointeet &operator=(const copy_on_write_pointeet &)
143+
{
144+
return *this;
145+
}
146+
147+
copy_on_write_pointeet(copy_on_write_pointeet &&)
148+
{
149+
}
150+
151+
copy_on_write_pointeet &operator=(copy_on_write_pointeet &&)
152+
{
153+
return *this;
154+
}
155+
156+
void increment_use_count()
157+
{
158+
INVARIANT(
159+
is_shareable(),
160+
"cannot increment the use count of a non-shareable reference");
161+
use_count_ += 1;
162+
}
163+
164+
void decrement_use_count()
165+
{
166+
INVARIANT(
167+
is_shareable(),
168+
"cannot decrement the use count of a non-shareable reference");
169+
use_count_ -= 1;
170+
}
171+
172+
Num use_count() const
173+
{
174+
return is_shareable() ? use_count_ : 1;
175+
}
176+
177+
void set_shareable(bool u)
178+
{
179+
use_count_ = u ? 1 : unshareable;
180+
}
181+
182+
bool is_shareable() const
183+
{
184+
return use_count_ != unshareable;
185+
}
186+
187+
protected:
188+
~copy_on_write_pointeet() = default;
189+
190+
private:
191+
static const Num unshareable;
192+
Num use_count_ = 0;
193+
};
194+
195+
template <typename Num>
196+
const Num copy_on_write_pointeet<Num>::unshareable =
197+
(std::numeric_limits<Num>::max)(); // suppress macro expansion on windows
198+
199+
template <typename Num>
200+
inline void pointee_increment_use_count(copy_on_write_pointeet<Num> &p)
201+
{
202+
p.increment_use_count();
203+
}
204+
205+
template <typename Num>
206+
inline void pointee_decrement_use_count(copy_on_write_pointeet<Num> &p)
207+
{
208+
p.decrement_use_count();
209+
}
210+
211+
template <typename Num>
212+
inline Num pointee_use_count(const copy_on_write_pointeet<Num> &p)
213+
{
214+
return p.use_count();
215+
}
216+
217+
template <typename Num, typename T>
218+
inline void pointee_set_use_count(copy_on_write_pointeet<Num> &p, T count)
219+
{
220+
p.set_use_count(count);
221+
}
222+
223+
template <typename Num>
224+
inline void pointee_set_shareable(copy_on_write_pointeet<Num> &p, bool u)
225+
{
226+
p.set_shareable(u);
227+
}
228+
229+
template <typename Num>
230+
inline bool pointee_is_shareable(const copy_on_write_pointeet<Num> &p)
231+
{
232+
return p.is_shareable();
233+
}
234+
235+
#endif

0 commit comments

Comments
 (0)