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  SN_ASSERT(data && other.data);
133 
134  return data == other.data;
135  }
136 
138  {
139  data.swap(other.data);
140  }
141 
142  // Types
143 
144  bool is_internal() const
145  {
146  return data.is_derived_u();
147  }
148 
149  bool is_container() const
150  {
151  return data.is_derived_v();
152  }
153 
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  if(data == empty_data)
180  {
181  data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
182  }
183  else if(data.use_count() > 1)
184  {
185  data = make_shared_derived_v<SN_PTR_TYPE_ARGS>(*data.get_derived_v());
186  }
187 
188  SN_ASSERT(data.use_count() == 1);
189 
190  return *data.get_derived_v();
191  }
192 
193  const d_ct &read_container() const
194  {
195  SN_ASSERT(!empty());
196 
197  return *data.get_derived_v();
198  }
199 
200  // Accessors
201 
202  const to_mapt &get_to_map() const
203  {
204  return read_internal().m;
205  }
206 
208  {
209  return write_internal().m;
210  }
211 
212  const leaf_listt &get_container() const
213  {
214  return read_container().con;
215  }
216 
218  {
219  return write_container().con;
220  }
221 
222  // Containers
223 
224  const leaft *find_leaf(const keyT &k) const
225  {
227 
228  const leaf_listt &c = get_container();
229 
230  for(const auto &n : c)
231  {
232  if(equalT()(n.get_key(), k))
233  return &n;
234  }
235 
236  return nullptr;
237  }
238 
239  leaft *find_leaf(const keyT &k)
240  {
242 
243  leaf_listt &c = get_container();
244 
245  for(auto &n : c)
246  {
247  if(equalT()(n.get_key(), k))
248  return &n;
249  }
250 
251  // If we return nullptr the call must be followed by a call to
252  // place_leaf(k, ...)
253  return nullptr;
254  }
255 
256  // add leaf, key must not exist yet
257  leaft *place_leaf(const keyT &k, const valueT &v)
258  {
260  // we need to check empty() first as the const version of find_leaf() must
261  // not be called on an empty node
262  SN_ASSERT(empty() || as_const(this)->find_leaf(k) == nullptr);
263 
264  leaf_listt &c = get_container();
265  c.push_front(leaft(k, v));
266 
267  return &c.front();
268  }
269 
270  // remove leaf, key must exist
271  void remove_leaf(const keyT &k)
272  {
274 
275  leaf_listt &c = get_container();
276 
277  SN_ASSERT(!c.empty());
278 
279  const leaft &first = c.front();
280 
281  if(equalT()(first.get_key(), k))
282  {
283  c.pop_front();
284  return;
285  }
286 
287  typename leaf_listt::const_iterator last_it = c.begin();
288 
289  typename leaf_listt::const_iterator it = c.begin();
290  it++;
291 
292  for(; it != c.end(); it++)
293  {
294  const leaft &leaf = *it;
295 
296  if(equalT()(leaf.get_key(), k))
297  {
298  c.erase_after(last_it);
299  return;
300  }
301 
302  last_it = it;
303  }
304 
305  UNREACHABLE;
306  }
307 
308  // Handle children
309 
310  const typename d_it::innert *find_child(const std::size_t n) const
311  {
313 
314  const to_mapt &m = get_to_map();
315  typename to_mapt::const_iterator it = m.find(n);
316 
317  if(it != m.end())
318  return &it->second;
319 
320  return nullptr;
321  }
322 
323  typename d_it::innert *add_child(const std::size_t n)
324  {
326 
327  to_mapt &m = get_to_map();
328  return &m[n];
329  }
330 
331  void remove_child(const std::size_t n)
332  {
334 
335  to_mapt &m = get_to_map();
336  std::size_t r = m.erase(n);
337 
338  SN_ASSERT_USE(r, r == 1);
339  }
340 
343 };
344 
348 
349 // Leafs
350 
352 {
353 public:
354 #if SN_SHARE_KEYS == 1
355  std::shared_ptr<keyT> k;
356 #else
357  keyT k;
358 #endif
359  valueT v;
360 };
361 
363 {
364 public:
366 
367  sharing_node_leaft(const keyT &k, const valueT &v) : data(empty_data)
368  {
369  SN_ASSERT(empty());
370 
371  auto &d = write();
372 
373 // Copy key
374 #if SN_SHARE_KEYS == 1
375  SN_ASSERT(d.k == nullptr);
376  d.k = std::make_shared<keyT>(k);
377 #else
378  d.k = k;
379 #endif
380 
381  // Copy value
382  d.v = v;
383  }
384 
385  bool empty() const
386  {
387  return data == empty_data;
388  }
389 
390  void clear()
391  {
392  data = empty_data;
393  }
394 
395  bool shares_with(const sharing_node_leaft &other) const
396  {
397  return data == other.data;
398  }
399 
401  {
402  data.swap(other.data);
403  }
404 
406  {
407  SN_ASSERT(data.use_count() > 0);
408 
409  if(data == empty_data)
410  {
411  data = make_small_shared_ptr<d_lt>();
412  }
413  else if(data.use_count() > 1)
414  {
415  data = make_small_shared_ptr<d_lt>(*data);
416  }
417 
418  SN_ASSERT(data.use_count() == 1);
419 
420  return *data;
421  }
422 
423  const d_lt &read() const
424  {
425  return *data;
426  }
427 
428  // Accessors
429 
430  const keyT &get_key() const
431  {
432  SN_ASSERT(!empty());
433 
434 #if SN_SHARE_KEYS == 1
435  return *read().k;
436 #else
437  return read().k;
438 #endif
439  }
440 
441  const valueT &get_value() const
442  {
443  SN_ASSERT(!empty());
444 
445  return read().v;
446  }
447 
448  valueT &get_value()
449  {
450  SN_ASSERT(!empty());
451 
452  return write().v;
453  }
454 
457 };
458 
461  make_small_shared_ptr<SN_PTR_TYPE_ARG>();
462 
463 #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:367
void swap(sharing_node_innert &other)
Definition: sharing_node.h:137
static small_shared_ptrt< d_leaft< keyT, valueT, equalT > > empty_data
Definition: sharing_node.h:456
bool empty() const
Definition: sharing_node.h:385
bool shares_with(const sharing_node_leaft &other) const
Definition: sharing_node.h:395
void remove_leaf(const keyT &k)
Definition: sharing_node.h:271
const to_mapt & get_to_map() const
Definition: sharing_node.h:202
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:257
const d_it::innert * find_child(const std::size_t n) const
Definition: sharing_node.h:310
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:323
const leaf_listt & get_container() const
Definition: sharing_node.h:212
Small map.
std::forward_list< leaft > leaf_listt
Definition: sharing_node.h:96
bool is_container() const
Definition: sharing_node.h:149
const valueT & get_value() const
Definition: sharing_node.h:441
valueT & get_value()
Definition: sharing_node.h:448
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:144
bool empty() const
Definition: sharing_node.h:120
to_mapt & get_to_map()
Definition: sharing_node.h:207
small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > data
Definition: sharing_node.h:341
const d_ct & read_container() const
Definition: sharing_node.h:193
const d_lt & read() const
Definition: sharing_node.h:423
d_containert< keyT, valueT, equalT > d_ct
Definition: sharing_node.h:109
leaf_listt & get_container()
Definition: sharing_node.h:217
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:365
leaft * find_leaf(const keyT &k)
Definition: sharing_node.h:239
#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:359
void swap(sharing_node_leaft &other)
Definition: sharing_node.h:400
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
static small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > empty_data
Definition: sharing_node.h:342
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:430
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:455
small_mapt< innert > to_mapt
Definition: sharing_node.h:82
const leaft * find_leaf(const keyT &k) const
Definition: sharing_node.h:224
Definition: kdev_t.h:24
void remove_child(const std::size_t n)
Definition: sharing_node.h:331
#define SN_TYPE_PAR_DEF
Definition: sharing_node.h:55