cprover
sharing_node.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Sharing node
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_SHARING_NODE_H
13 #define CPROVER_UTIL_SHARING_NODE_H
14 
15 #ifdef SN_DEBUG
16 #include <iostream>
17 #endif
18 
19 #include <forward_list>
20 #include <type_traits>
21 
22 #ifndef SN_SMALL_MAP
23 #define SN_SMALL_MAP 1
24 #endif
25 
26 #ifndef SN_SHARE_KEYS
27 #define SN_SHARE_KEYS 0
28 #endif
29 
30 #if SN_SMALL_MAP == 1
31 #include "small_map.h"
32 #else
33 #include <map>
34 #endif
35 
36 #include "invariant.h"
37 #include "make_unique.h"
38 #include "small_shared_ptr.h"
40 
41 #ifdef SN_INTERNAL_CHECKS
42 #define SN_ASSERT(b) INVARIANT(b, "Sharing node internal invariant")
43 #define SN_ASSERT_USE(v, b) SN_ASSERT(b)
44 #else
45 #define SN_ASSERT(b)
46 #define SN_ASSERT_USE(v, b) static_cast<void>(v);
47 #endif
48 
49 // clang-format off
50 #define SN_TYPE_PAR_DECL \
51  template <typename keyT, \
52  typename valueT, \
53  typename equalT = std::equal_to<keyT>>
54 
55 #define SN_TYPE_PAR_DEF \
56  template <typename keyT, typename valueT, typename equalT>
57 // clang-format on
58 
59 #define SN_TYPE_ARGS keyT, valueT, equalT
60 
61 #define SN_PTR_TYPE_ARGS d_internalt<SN_TYPE_ARGS>, d_containert<SN_TYPE_ARGS>
62 
63 #define SN_PTR_TYPE_ARG d_leaft<SN_TYPE_ARGS>
64 
65 template <class T>
66 const T *as_const(T *t)
67 {
68  return t;
69 }
70 
71 // Inner nodes (internal nodes or container nodes)
72 
74 
76 
78 {
79 public:
81 #if SN_SMALL_MAP == 1
83 #else
84  typedef std::map<std::size_t, innert> to_mapt;
85 #endif
86 
88 };
89 
91 
93 {
94 public:
96  typedef std::forward_list<leaft> leaf_listt;
97 
99 };
100 
102 {
103 };
104 
106 {
107 public:
110 
111  typedef typename d_it::to_mapt to_mapt;
112 
113  typedef typename d_ct::leaft leaft;
114  typedef typename d_ct::leaf_listt leaf_listt;
115 
117  {
118  }
119 
120  bool empty() const
121  {
122  return data == empty_data;
123  }
124 
125  void clear()
126  {
127  data = empty_data;
128  }
129 
130  bool shares_with(const sharing_node_innert &other) const
131  {
132  return data == other.data;
133  }
134 
136  {
137  data.swap(other.data);
138  }
139 
140  // Types
141 
142  bool is_internal() const
143  {
144  return data.is_derived_u();
145  }
146 
147  bool is_container() const
148  {
149  return data.is_derived_v();
150  }
151 
153  {
154  SN_ASSERT(data.use_count() > 0);
155 
156  if(data == empty_data)
157  {
158  data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
159  }
160  else if(data.use_count() > 1)
161  {
162  data = make_shared_derived_u<SN_PTR_TYPE_ARGS>(*data.get_derived_u());
163  }
164 
165  SN_ASSERT(data.use_count() == 1);
166 
167  return *data.get_derived_u();
168  }
169 
170  const d_it &read_internal() const
171  {
172  SN_ASSERT(!empty());
173 
174  return *data.get_derived_u();
175  }
176 
178  {
179  SN_ASSERT(data.use_count() > 0);
180 
181  if(data == empty_data)
182  {
183  data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
184  }
185  else if(data.use_count() > 1)
186  {
187  data = make_shared_derived_v<SN_PTR_TYPE_ARGS>(*data.get_derived_v());
188  }
189 
190  SN_ASSERT(data.use_count() == 1);
191 
192  return *data.get_derived_v();
193  }
194 
195  const d_ct &read_container() const
196  {
197  SN_ASSERT(!empty());
198 
199  return *data.get_derived_v();
200  }
201 
202  // Accessors
203 
204  const to_mapt &get_to_map() const
205  {
206  return read_internal().m;
207  }
208 
210  {
211  return write_internal().m;
212  }
213 
214  const leaf_listt &get_container() const
215  {
216  return read_container().con;
217  }
218 
220  {
221  return write_container().con;
222  }
223 
224  // Containers
225 
226  const leaft *find_leaf(const keyT &k) const
227  {
229 
230  const leaf_listt &c = get_container();
231 
232  for(const auto &n : c)
233  {
234  if(equalT()(n.get_key(), k))
235  return &n;
236  }
237 
238  return nullptr;
239  }
240 
241  leaft *find_leaf(const keyT &k)
242  {
244 
245  leaf_listt &c = get_container();
246 
247  for(auto &n : c)
248  {
249  if(equalT()(n.get_key(), k))
250  return &n;
251  }
252 
253  // If we return nullptr the call must be followed by a call to
254  // place_leaf(k, ...)
255  return nullptr;
256  }
257 
258  // add leaf, key must not exist yet
259  leaft *place_leaf(const keyT &k, const valueT &v)
260  {
262 
263  SN_ASSERT(as_const(this)->find_leaf(k) == nullptr);
264 
265  leaf_listt &c = get_container();
266  c.push_front(leaft(k, v));
267 
268  return &c.front();
269  }
270 
271  // remove leaf, key must exist
272  void remove_leaf(const keyT &k)
273  {
275 
276  leaf_listt &c = get_container();
277 
278  SN_ASSERT(!c.empty());
279 
280  const leaft &first = c.front();
281 
282  if(equalT()(first.get_key(), k))
283  {
284  c.pop_front();
285  return;
286  }
287 
288  typename leaf_listt::const_iterator last_it = c.begin();
289 
290  typename leaf_listt::const_iterator it = c.begin();
291  it++;
292 
293  for(; it != c.end(); it++)
294  {
295  const leaft &leaf = *it;
296 
297  if(equalT()(leaf.get_key(), k))
298  {
299  c.erase_after(last_it);
300  return;
301  }
302 
303  last_it = it;
304  }
305 
306  UNREACHABLE;
307  }
308 
309  // Handle children
310 
311  const typename d_it::innert *find_child(const std::size_t n) const
312  {
314 
315  const to_mapt &m = get_to_map();
316  typename to_mapt::const_iterator it = m.find(n);
317 
318  if(it != m.end())
319  return &it->second;
320 
321  return nullptr;
322  }
323 
324  typename d_it::innert *add_child(const std::size_t n)
325  {
327 
328  to_mapt &m = get_to_map();
329  return &m[n];
330  }
331 
332  void remove_child(const std::size_t n)
333  {
335 
336  to_mapt &m = get_to_map();
337  std::size_t r = m.erase(n);
338 
339  SN_ASSERT_USE(r, r == 1);
340  }
341 
344 };
345 
349 
350 // Leafs
351 
353 {
354 public:
355 #if SN_SHARE_KEYS == 1
356  std::shared_ptr<keyT> k;
357 #else
358  keyT k;
359 #endif
360  valueT v;
361 };
362 
364 {
365 public:
367 
368  sharing_node_leaft(const keyT &k, const valueT &v) : data(empty_data)
369  {
370  SN_ASSERT(empty());
371 
372  auto &d = write();
373 
374 // Copy key
375 #if SN_SHARE_KEYS == 1
376  SN_ASSERT(d.k == nullptr);
377  d.k = std::make_shared<keyT>(k);
378 #else
379  d.k = k;
380 #endif
381 
382  // Copy value
383  d.v = v;
384  }
385 
386  bool empty() const
387  {
388  return data == empty_data;
389  }
390 
391  void clear()
392  {
393  data = empty_data;
394  }
395 
396  bool shares_with(const sharing_node_leaft &other) const
397  {
398  return data == other.data;
399  }
400 
402  {
403  data.swap(other.data);
404  }
405 
407  {
408  SN_ASSERT(data.use_count() > 0);
409 
410  if(data == empty_data)
411  {
412  data = make_small_shared_ptr<d_lt>();
413  }
414  else if(data.use_count() > 1)
415  {
416  data = make_small_shared_ptr<d_lt>(*data);
417  }
418 
419  SN_ASSERT(data.use_count() == 1);
420 
421  return *data;
422  }
423 
424  const d_lt &read() const
425  {
426  return *data;
427  }
428 
429  // Accessors
430 
431  const keyT &get_key() const
432  {
433  SN_ASSERT(!empty());
434 
435 #if SN_SHARE_KEYS == 1
436  return *read().k;
437 #else
438  return read().k;
439 #endif
440  }
441 
442  const valueT &get_value() const
443  {
444  SN_ASSERT(!empty());
445 
446  return read().v;
447  }
448 
449  valueT &get_value()
450  {
451  SN_ASSERT(!empty());
452 
453  return write().v;
454  }
455 
458 };
459 
462  make_small_shared_ptr<SN_PTR_TYPE_ARG>();
463 
464 #endif
const T * as_const(T *t)
Definition: sharing_node.h:66
#define SN_TYPE_PAR_DECL
Definition: sharing_node.h:50
static int8_t r
Definition: irep_hash.h:59
sharing_node_leaft(const keyT &k, const valueT &v)
Definition: sharing_node.h:368
void swap(sharing_node_innert &other)
Definition: sharing_node.h:135
static small_shared_ptrt< d_leaft< keyT, valueT, equalT > > empty_data
Definition: sharing_node.h:457
bool empty() const
Definition: sharing_node.h:386
bool shares_with(const sharing_node_leaft &other) const
Definition: sharing_node.h:396
void remove_leaf(const keyT &k)
Definition: sharing_node.h:272
const to_mapt & get_to_map() const
Definition: sharing_node.h:204
A helper class to store use-counts of objects held by small shared pointers.
#define SN_ASSERT_USE(v, b)
Definition: sharing_node.h:46
leaf_listt con
Definition: sharing_node.h:98
leaft * place_leaf(const keyT &k, const valueT &v)
Definition: sharing_node.h:259
const d_it::innert * find_child(const std::size_t n) const
Definition: sharing_node.h:311
sharing_node_leaft< keyT, valueT, equalT > leaft
Definition: sharing_node.h:95
to_mapt m
Definition: sharing_node.h:87
d_it::innert * add_child(const std::size_t n)
Definition: sharing_node.h:324
const leaf_listt & get_container() const
Definition: sharing_node.h:214
Small map.
std::forward_list< leaft > leaf_listt
Definition: sharing_node.h:96
bool is_container() const
Definition: sharing_node.h:147
const valueT & get_value() const
Definition: sharing_node.h:442
valueT & get_value()
Definition: sharing_node.h:449
This class is really similar to boost&#39;s intrusive_pointer, but can be a bit simpler seeing as we&#39;re o...
const_iterator end() const
Definition: small_map.h:373
const_iterator find(std::size_t idx) const
Definition: small_map.h:464
d_ct & write_container()
Definition: sharing_node.h:177
std::size_t erase(std::size_t idx)
Definition: small_map.h:478
bool is_internal() const
Definition: sharing_node.h:142
bool empty() const
Definition: sharing_node.h:120
to_mapt & get_to_map()
Definition: sharing_node.h:209
small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > data
Definition: sharing_node.h:342
const d_ct & read_container() const
Definition: sharing_node.h:195
const d_lt & read() const
Definition: sharing_node.h:424
d_containert< keyT, valueT, equalT > d_ct
Definition: sharing_node.h:109
leaf_listt & get_container()
Definition: sharing_node.h:219
d_internalt< keyT, valueT, equalT > d_it
Definition: sharing_node.h:108
d_ct::leaf_listt leaf_listt
Definition: sharing_node.h:114
d_leaft< keyT, valueT, equalT > d_lt
Definition: sharing_node.h:366
leaft * find_leaf(const keyT &k)
Definition: sharing_node.h:241
#define SN_ASSERT(b)
Definition: sharing_node.h:45
bool shares_with(const sharing_node_innert &other) const
Definition: sharing_node.h:130
valueT v
Definition: sharing_node.h:360
void swap(sharing_node_leaft &other)
Definition: sharing_node.h:401
#define UNREACHABLE
Definition: invariant.h:250
static small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > empty_data
Definition: sharing_node.h:343
const d_it & read_internal() const
Definition: sharing_node.h:170
d_it::to_mapt to_mapt
Definition: sharing_node.h:111
const keyT & get_key() const
Definition: sharing_node.h:431
small_shared_two_way_pointeet< unsigned > d_baset
Definition: sharing_node.h:73
This class is similar to small_shared_ptrt and boost&#39;s intrusive_ptr.
sharing_node_innert< keyT, valueT, equalT > innert
Definition: sharing_node.h:80
small_shared_ptrt< d_leaft< keyT, valueT, equalT > > data
Definition: sharing_node.h:456
small_mapt< innert > to_mapt
Definition: sharing_node.h:82
const leaft * find_leaf(const keyT &k) const
Definition: sharing_node.h:226
Definition: kdev_t.h:24
void remove_child(const std::size_t n)
Definition: sharing_node.h:332
#define SN_TYPE_PAR_DEF
Definition: sharing_node.h:55