cprover
sharing_map.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Sharing map
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_SHARING_MAP_H
13 #define CPROVER_UTIL_SHARING_MAP_H
14 
15 #ifdef SM_DEBUG
16 #include <iostream>
17 #endif
18 
19 #include <functional>
20 #include <map>
21 #include <memory>
22 #include <stack>
23 #include <stdexcept>
24 #include <string>
25 #include <tuple>
26 #include <vector>
27 
28 #include "irep.h"
29 #include "sharing_node.h"
30 #include "threeval.h"
31 
32 #ifdef SM_INTERNAL_CHECKS
33 #define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant")
34 #else
35 #define SM_ASSERT(b)
36 #endif
37 
38 // clang-format off
39 #define SHARING_MAPT(R) \
40  template <class keyT, class valueT, class hashT, class equalT> \
41  R sharing_mapt<keyT, valueT, hashT, equalT>
42 
43 #define SHARING_MAPT2(CV, ST) \
44  template <class keyT, class valueT, class hashT, class equalT> \
45  CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \
46  sharing_mapt<keyT, valueT, hashT, equalT>
47 // clang-format on
48 
49 // Note: Due to a bug in Visual Studio we need to add an additional "const"
50 // qualifier to the return values of insert(), place(), and find(). The type
51 // defined in sharing_mapt already includes the const qualifier, but it is lost
52 // when accessed from outside the class. This is fixed in Visual Studio 15.6.
53 
120 template <class keyT,
121  class valueT,
122  class hashT = std::hash<keyT>,
123  class equalT = std::equal_to<keyT>>
125 {
126 public:
127  friend void sharing_map_interface_test();
128  friend void sharing_map_copy_test();
129  friend void sharing_map_collision_test();
130  friend void sharing_map_view_test();
131 
133  {
134  }
135 
136  typedef keyT key_type;
137  typedef valueT mapped_type;
138  typedef std::pair<const key_type, mapped_type> value_type;
139 
140  typedef hashT hash;
141  typedef equalT key_equal;
142 
143  typedef std::size_t size_type;
144 
149  typedef const std::pair<const mapped_type &, const bool> const_find_type;
150 
155  typedef const std::pair<mapped_type &, const bool> find_type;
156 
157  typedef std::vector<key_type> keyst;
158 
159 protected:
162 
164 
165  typedef typename innert::to_mapt to_mapt;
166  typedef typename innert::leaf_listt leaf_listt;
167 
168 public:
169  // interface
170 
171  size_type erase(const key_type &k, const tvt &key_exists = tvt::unknown());
172 
174  const keyst &ks,
175  const tvt &key_exists = tvt::unknown()); // applies to all keys
176 
177  // return true if element was inserted
179  const key_type &k,
180  const mapped_type &v,
181  const tvt &key_exists=tvt::unknown());
182 
184  const value_type &p,
185  const tvt &key_exists=tvt::unknown());
186 
188  const key_type &k,
189  const mapped_type &v);
190 
192  const value_type &p);
193 
194  find_type find(
195  const key_type &k,
196  const tvt &key_exists=tvt::unknown());
197 
198  const_find_type find(const key_type &k) const;
199 
200  mapped_type &at(
201  const key_type &k,
202  const tvt &key_exists=tvt::unknown());
203 
204  const mapped_type &at(const key_type &k) const;
205 
206  mapped_type &operator[](const key_type &k);
207 
211  void swap(sharing_mapt &other)
212  {
213  map.swap(other.map);
214 
215  std::size_t tmp = num;
216  num=other.num;
217  other.num=tmp;
218  }
219 
223  size_type size() const
224  {
225  return num;
226  }
227 
229  bool empty() const
230  {
231  return num==0;
232  }
233 
235  void clear()
236  {
237  map.clear();
238  num=0;
239  }
240 
246  bool has_key(const key_type &k) const
247  {
248  return get_leaf_node(k)!=nullptr;
249  }
250 
251  // views
252 
253  typedef std::pair<const key_type &, const mapped_type &> view_itemt;
254 
257  typedef std::vector<view_itemt> viewt;
258 
260  {
261  public:
263  const bool in_both,
264  const key_type &k,
265  const mapped_type &m,
266  const mapped_type &other_m) :
267  in_both(in_both),
268  k(k),
269  m(m),
270  other_m(other_m) {}
271 
272  // if true key is in both maps, if false key is only in the map
273  // from which the view was obtained
274  const bool in_both;
275 
276  const key_type &k;
277 
278  const mapped_type &m;
280  };
281 
285  typedef std::vector<delta_view_itemt> delta_viewt;
286 
287  void get_view(viewt &view) const;
288 
289  void get_delta_view(
290  const sharing_mapt &other,
291  delta_viewt &delta_view,
292  const bool only_common = true) const;
293 
294 protected:
295  // helpers
296 
298  const innert *get_container_node(const key_type &k) const;
299 
300  const leaft *get_leaf_node(const key_type &k) const
301  {
302  const innert *cp = get_container_node(k);
303  if(cp == nullptr)
304  return nullptr;
305 
306  const leaft *lp;
307  lp = cp->find_leaf(k);
308 
309  return lp;
310  }
311 
312  void iterate(
313  const baset &n,
314  const unsigned depth,
315  std::function<void(const key_type &k, const mapped_type &m)> f) const;
316 
317  void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view)
318  const;
319 
320  // dummy element returned when no element was found
322 
323  static const std::string not_found_msg;
324 
325  // config
326  static const std::size_t bits;
327  static const std::size_t chunk;
328 
329  // derived config
330  static const std::size_t mask;
331  static const std::size_t steps;
332 
333  // key-value map
335 
336  // number of elements in the map
338 };
339 
340 SHARING_MAPT(void)
341 ::iterate(
342  const baset &n,
343  unsigned depth,
344  std::function<void(const key_type &k, const mapped_type &m)> f) const
345 {
346  typedef std::pair<unsigned, const baset *> stack_itemt;
347 
348  std::stack<stack_itemt> stack;
349  stack.push({depth, &n});
350 
351  do
352  {
353  const stack_itemt &si = stack.top();
354 
355  const unsigned depth = si.first;
356  const baset *bp = si.second;
357 
358  stack.pop();
359 
360  if(depth < steps) // internal
361  {
362  const innert *ip = static_cast<const innert *>(bp);
363  const to_mapt &m = ip->get_to_map();
364  SM_ASSERT(!m.empty());
365 
366  for(const auto &item : m)
367  {
368  const innert *i = &item.second;
369  stack.push({depth + 1, i});
370  }
371  }
372  else // container
373  {
374  SM_ASSERT(depth == steps);
375 
376  const innert *cp = static_cast<const innert *>(bp);
377  const leaf_listt &ll = cp->get_container();
378  SM_ASSERT(!ll.empty());
379 
380  for(const auto &l : ll)
381  {
382  f(l.get_key(), l.get_value());
383  }
384  }
385  }
386  while(!stack.empty());
387 }
388 
398 SHARING_MAPT(void)::get_view(viewt &view) const
399 {
400  SM_ASSERT(view.empty());
401 
402  if(empty())
403  return;
404 
405  auto f = [&view](const key_type &k, const mapped_type &m) {
406  view.push_back(view_itemt(k, m));
407  };
408 
409  iterate(map, 0, f);
410 }
411 
412 SHARING_MAPT(void)
413 ::gather_all(const baset &n, unsigned depth, delta_viewt &delta_view) const
414 {
415  auto f = [&delta_view](const key_type &k, const mapped_type &m) {
416  delta_view.push_back(delta_view_itemt(false, k, m, dummy));
417  };
418 
419  iterate(n, depth, f);
420 }
421 
455 SHARING_MAPT(void)
456 ::get_delta_view(
457  const sharing_mapt &other,
458  delta_viewt &delta_view,
459  const bool only_common) const
460 {
461  SM_ASSERT(delta_view.empty());
462 
463  if(empty())
464  return;
465 
466  if(other.empty())
467  {
468  if(!only_common)
469  {
470  gather_all(map, 0, delta_view);
471  }
472 
473  return;
474  }
475 
476  typedef std::tuple<unsigned, const baset *, const baset *> stack_itemt;
477  std::stack<stack_itemt> stack;
478 
479  // We do a DFS "in lockstep" simultaneously on both maps. For
480  // corresponding nodes we check whether they are shared between the
481  // maps, and if not, we recurse into the corresponding subtrees.
482 
483  // The stack contains the children of already visited nodes that we
484  // still have to visit during the traversal.
485 
486  stack.push(stack_itemt(0, &map, &other.map));
487 
488  do
489  {
490  const stack_itemt &si = stack.top();
491 
492  const unsigned depth = std::get<0>(si);
493  const baset *bp1 = std::get<1>(si);
494  const baset *bp2 = std::get<2>(si);
495 
496  stack.pop();
497 
498  if(depth < steps) // internal
499  {
500  const innert *ip1 = static_cast<const innert *>(bp1);
501  const innert *ip2 = static_cast<const innert *>(bp2);
502 
503  const to_mapt &m = ip1->get_to_map();
504 
505  for(const auto &item : m)
506  {
507  const innert *p;
508 
509  p = ip2->find_child(item.first);
510  if(p==nullptr)
511  {
512  if(!only_common)
513  {
514  gather_all(item.second, depth + 1, delta_view);
515  }
516  }
517  else if(!item.second.shares_with(*p))
518  {
519  stack.push(stack_itemt(depth + 1, &item.second, p));
520  }
521  }
522  }
523  else // container
524  {
525  SM_ASSERT(depth == steps);
526 
527  const innert *cp1 = static_cast<const innert *>(bp1);
528  const innert *cp2 = static_cast<const innert *>(bp2);
529 
530  const leaf_listt &ll1 = cp1->get_container();
531 
532  for(const auto &l1 : ll1)
533  {
534  const key_type &k1=l1.get_key();
535  const leaft *p;
536 
537  p = cp2->find_leaf(k1);
538 
539  if(p != nullptr)
540  {
541  if(!l1.shares_with(*p))
542  {
543  delta_view.push_back({true, k1, l1.get_value(), p->get_value()});
544  }
545  }
546  else if(!only_common)
547  {
548  delta_view.push_back({false, l1.get_key(), l1.get_value(), dummy});
549  }
550  }
551  }
552  }
553  while(!stack.empty());
554 }
555 
556 SHARING_MAPT2(, innert *)::get_container_node(const key_type &k)
557 {
558  std::size_t key = hash()(k);
559  innert *ip = &map;
560 
561  for(std::size_t i = 0; i < steps; i++)
562  {
563  std::size_t bit = key & mask;
564 
565  ip = ip->add_child(bit);
566 
567  key >>= chunk;
568  }
569 
570  return ip;
571 }
572 
573 SHARING_MAPT2(const, innert *)::get_container_node(const key_type &k) const
574 {
575  if(empty())
576  return nullptr;
577 
578  std::size_t key = hash()(k);
579  const innert *ip = &map;
580 
581  for(std::size_t i = 0; i < steps; i++)
582  {
583  std::size_t bit = key & mask;
584 
585  ip = ip->find_child(bit);
586  if(ip == nullptr)
587  return nullptr;
588 
589  key >>= chunk;
590  }
591 
592  return ip;
593 }
594 
604 SHARING_MAPT2(, size_type)::erase(const key_type &k, const tvt &key_exists)
605 {
606  SM_ASSERT(!key_exists.is_false());
607  SM_ASSERT(!key_exists.is_true() || has_key(k));
608 
609  // check if key exists
610  if(key_exists.is_unknown() && !has_key(k))
611  return 0;
612 
613  innert *del = nullptr;
614  std::size_t del_bit = 0;
615  std::size_t del_level = 0;
616 
617  std::size_t key = hash()(k);
618  innert *ip = &map;
619 
620  for(std::size_t i = 0; i < steps; i++)
621  {
622  std::size_t bit = key & mask;
623 
624  const to_mapt &m = as_const(ip)->get_to_map();
625 
626  if(m.size() > 1 || del == nullptr)
627  {
628  del = ip;
629  del_bit=bit;
630  del_level = i;
631  }
632 
633  ip = ip->add_child(bit);
634 
635  key >>= chunk;
636  }
637 
638  const leaf_listt &ll = as_const(ip)->get_container();
639 
640  // forward list has one element
641  if(!ll.empty() && std::next(ll.begin()) == ll.end())
642  {
643  if(del_level < steps - 1)
644  {
645  del->remove_child(del_bit);
646  }
647  else
648  {
649  SM_ASSERT(del_level == steps - 1);
650  del->remove_child(del_bit);
651  }
652 
653  num--;
654  return 1;
655  }
656 
657  SM_ASSERT(!ll.empty());
658 
659  ip->remove_leaf(k);
660  num--;
661 
662  return 1;
663 }
664 
677 ::erase_all(const keyst &ks, const tvt &key_exists)
678 {
679  size_type cnt = 0;
680 
681  for(const key_type &k : ks)
682  {
683  cnt+=erase(k, key_exists);
684  }
685 
686  return cnt;
687 }
688 
701 SHARING_MAPT2(const, const_find_type)
702 ::insert(const key_type &k, const mapped_type &m, const tvt &key_exists)
703 {
704  SM_ASSERT(!key_exists.is_true());
705  SM_ASSERT(!key_exists.is_false() || !has_key(k));
706 
707  if(key_exists.is_unknown())
708  {
709  const leaft *lp = as_const(this)->get_leaf_node(k);
710  if(lp != nullptr)
711  return const_find_type(lp->get_value(), false);
712  }
713 
714  innert *cp = get_container_node(k);
715  SM_ASSERT(cp != nullptr);
716 
717  const leaft *lp = cp->place_leaf(k, m);
718  num++;
719 
720  return const_find_type(lp->get_value(), true);
721 }
722 
723 // Insert element, return const reference
724 SHARING_MAPT2(const, const_find_type)
725 ::insert(const value_type &p, const tvt &key_exists)
726 {
727  return insert(p.first, p.second, key_exists);
728 }
729 
740 SHARING_MAPT2(const, find_type)::place(const key_type &k, const mapped_type &m)
741 {
742  innert *cp = get_container_node(k);
743  SM_ASSERT(cp != nullptr);
744 
745  leaft *lp = cp->find_leaf(k);
746 
747  if(lp != nullptr)
748  return find_type(lp->get_value(), false);
749 
750  lp = cp->place_leaf(k, m);
751  num++;
752 
753  return find_type(lp->get_value(), true);
754 }
755 
757 SHARING_MAPT2(const, find_type)::place(const value_type &p)
758 {
759  return place(p.first, p.second);
760 }
761 
773 SHARING_MAPT2(const, find_type)::find(const key_type &k, const tvt &key_exists)
774 {
775  SM_ASSERT(!key_exists.is_false());
776  SM_ASSERT(!key_exists.is_true() || has_key(k));
777 
778  if(key_exists.is_unknown() && !has_key(k))
779  return find_type(dummy, false);
780 
781  innert *cp = get_container_node(k);
782  SM_ASSERT(cp != nullptr);
783 
784  leaft *lp = cp->find_leaf(k);
785  SM_ASSERT(lp != nullptr);
786 
787  return find_type(lp->get_value(), true);
788 }
789 
799 SHARING_MAPT2(const, const_find_type)::find(const key_type &k) const
800 {
801  const leaft *lp = get_leaf_node(k);
802 
803  if(lp == nullptr)
804  return const_find_type(dummy, false);
805 
806  return const_find_type(lp->get_value(), true);
807 }
808 
821  const key_type &k,
822  const tvt &key_exists)
823 {
824  find_type r=find(k, key_exists);
825 
826  if(!r.second)
827  throw std::out_of_range(not_found_msg);
828 
829  return r.first;
830 }
831 
841 SHARING_MAPT2(const, mapped_type &)::at(const key_type &k) const
842 {
843  const_find_type r=find(k);
844  if(!r.second)
845  throw std::out_of_range(not_found_msg);
846 
847  return r.first;
848 }
849 
858 SHARING_MAPT2(, mapped_type &)::operator[](const key_type &k)
859 {
860  return place(k, mapped_type()).first;
861 }
862 
863 // static constants
864 
865 SHARING_MAPT(const std::string)::not_found_msg="key not found";
866 
867 SHARING_MAPT2(, mapped_type)::dummy;
868 
869 SHARING_MAPT(const std::size_t)::bits = 18;
870 SHARING_MAPT(const std::size_t)::chunk = 3;
871 
872 SHARING_MAPT(const std::size_t)::mask = 0xffff >> (16 - chunk);
873 SHARING_MAPT(const std::size_t)::steps = bits / chunk;
874 
875 #endif
sharing_node_baset baset
Definition: sharing_map.h:163
bool empty() const
Check if map is empty.
Definition: sharing_map.h:229
const T * as_const(T *t)
Definition: sharing_node.h:66
#define SM_ASSERT(b)
Definition: sharing_map.h:35
void swap(sharing_mapt &other)
Swap with other map.
Definition: sharing_map.h:211
static int8_t r
Definition: irep_hash.h:59
void swap(sharing_node_innert &other)
Definition: sharing_node.h:135
sharing_node_innert< key_type, mapped_type > innert
Definition: sharing_map.h:160
friend void sharing_map_collision_test()
void iterate(const baset &n, const unsigned depth, std::function< void(const key_type &k, const mapped_type &m)> f) const
Definition: sharing_map.h:341
find_type place(const key_type &k, const mapped_type &v)
Insert element, return non-const reference.
Definition: sharing_map.h:740
void remove_leaf(const keyT &k)
Definition: sharing_node.h:272
const to_mapt & get_to_map() const
Definition: sharing_node.h:204
friend void sharing_map_interface_test()
leaft * place_leaf(const keyT &k, const valueT &v)
Definition: sharing_node.h:259
valueT mapped_type
Definition: sharing_map.h:137
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:124
delta_view_itemt(const bool in_both, const key_type &k, const mapped_type &m, const mapped_type &other_m)
Definition: sharing_map.h:262
const d_it::innert * find_child(const std::size_t n) const
Definition: sharing_node.h:311
static tvt unknown()
Definition: threeval.h:33
std::vector< key_type > keyst
Definition: sharing_map.h:157
bool has_key(const key_type &k) const
Check if key is in map.
Definition: sharing_map.h:246
mapped_type & at(const key_type &k, const tvt &key_exists=tvt::unknown())
Get element at key.
Definition: sharing_map.h:820
static const std::size_t chunk
Definition: sharing_map.h:327
mapped_type & operator[](const key_type &k)
Get element at key, insert new if non-existent.
Definition: sharing_map.h:858
std::size_t size() const
Definition: small_map.h:576
equalT key_equal
Definition: sharing_map.h:141
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:257
#define SHARING_MAPT(R)
Definition: sharing_map.h:39
size_type size() const
Get number of elements in map.
Definition: sharing_map.h:223
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
unsignedbv_typet size_type()
Definition: c_types.cpp:58
sharing_node_leaft< key_type, mapped_type > leaft
Definition: sharing_map.h:161
STL namespace.
const std::pair< mapped_type &, const bool > find_type
Return type of methods that retrieve a reference to a value.
Definition: sharing_map.h:155
size_type erase(const key_type &k, const tvt &key_exists=tvt::unknown())
Erase element.
Definition: sharing_map.h:604
const valueT & get_value() const
Definition: sharing_node.h:442
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Definition: sharing_map.h:456
static mapped_type dummy
Definition: sharing_map.h:321
find_type find(const key_type &k, const tvt &key_exists=tvt::unknown())
Find element.
Definition: sharing_map.h:773
std::pair< const key_type &, const mapped_type & > view_itemt
Definition: sharing_map.h:253
size_type erase_all(const keyst &ks, const tvt &key_exists=tvt::unknown())
Erase all elements.
Definition: sharing_map.h:677
void clear()
Clear map.
Definition: sharing_map.h:235
friend void sharing_map_view_test()
innert::leaf_listt leaf_listt
Definition: sharing_map.h:166
Definition: threeval.h:19
void get_view(viewt &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Definition: sharing_map.h:398
static const std::size_t steps
Definition: sharing_map.h:331
std::pair< const key_type, mapped_type > value_type
Definition: sharing_map.h:138
static const std::size_t mask
Definition: sharing_map.h:330
std::size_t size_type
Definition: sharing_map.h:143
static const std::string not_found_msg
Definition: sharing_map.h:323
#define SHARING_MAPT2(CV, ST)
Definition: sharing_map.h:43
const_find_type insert(const key_type &k, const mapped_type &v, const tvt &key_exists=tvt::unknown())
Insert element, return const reference.
Definition: sharing_map.h:702
size_type num
Definition: sharing_map.h:337
const mapped_type & other_m
Definition: sharing_map.h:279
void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view) const
Definition: sharing_map.h:413
bool empty() const
Definition: small_map.h:582
Sharing node.
static const std::size_t bits
Definition: sharing_map.h:326
innert::to_mapt to_mapt
Definition: sharing_map.h:165
#define stack(x)
Definition: parser.h:144
const std::pair< const mapped_type &, const bool > const_find_type
Return type of methods that retrieve a const reference to a value.
Definition: sharing_map.h:149
const leaft * get_leaf_node(const key_type &k) const
Definition: sharing_map.h:300
const leaft * find_leaf(const keyT &k) const
Definition: sharing_node.h:226
void remove_child(const std::size_t n)
Definition: sharing_node.h:332
friend void sharing_map_copy_test()
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:285
innert * get_container_node(const key_type &k)
Definition: sharing_map.h:556