CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
sharing_map.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Sharing map
4
5Author: 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 "as_const.h"
20#include "irep.h"
21#include "sharing_node.h"
22#include "threeval.h"
23
24#include <functional>
25#include <map>
26#include <memory>
27#include <optional>
28#include <set>
29#include <stack>
30#include <stdexcept>
31#include <string>
32#include <tuple>
33#include <type_traits>
34#include <vector>
35
36#ifdef SM_INTERNAL_CHECKS
37# define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant")
38#else
39# define SM_ASSERT(b)
40#endif
41
42// clang-format off
43
48#define SHARING_MAPT(type) \
49 template < \
50 typename keyT, \
51 typename valueT, \
52 bool fail_if_equal, \
53 typename hashT, \
54 typename equalT> \
55 type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
56
57#define SHARING_MAPTV(return_type, V) \
58 template < \
59 typename keyT, \
60 typename valueT, \
61 bool fail_if_equal, \
62 typename hashT, \
63 typename equalT> \
64 template <class V> \
65 return_type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
66
72#define SHARING_MAPT2(cv_qualifiers, return_type) \
73 template < \
74 typename keyT, \
75 typename valueT, \
76 bool fail_if_equal, \
77 typename hashT, \
78 typename equalT> \
79 cv_qualifiers typename \
80 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
81 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
82
90#define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type) \
91 template < \
92 typename keyT, \
93 typename valueT, \
94 bool fail_if_equal, \
95 typename hashT, \
96 typename equalT> \
97 template <class template_parameter> \
98 cv_qualifiers typename \
99 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>::return_type \
100 sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
101
107#define SHARING_MAPT4(template_parameter, return_type) \
108 template < \
109 typename keyT, \
110 typename valueT, \
111 bool fail_if_equal, \
112 typename hashT, \
113 typename equalT> \
114 template <class template_parameter> \
115 return_type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>
116// clang-format on
117
183template <
184 typename keyT,
185 typename valueT,
186 bool fail_if_equal = false,
187 typename hashT = std::hash<keyT>,
188 typename equalT = std::equal_to<keyT>>
190{
191public:
193 {
194 }
195
196 typedef keyT key_type;
198
199 typedef hashT hash;
201
202 typedef std::size_t size_type;
203
204 typedef std::vector<key_type> keyst;
205
206protected:
208
209 typedef typename nodet::to_mapt to_mapt;
211
212 struct falset
213 {
214 bool operator()(const mapped_type &lhs, const mapped_type &rhs)
215 {
216 return false;
217 }
218 };
219
220 typedef
221 typename std::conditional<fail_if_equal, std::equal_to<valueT>, falset>::
223
225 {
227 {
228 }
229
231 {
232 return false;
233 }
234 };
235
237 {
243
244 bool operator()(const mapped_type &new_value)
245 {
246 return old_value == new_value;
247 }
248 };
249
250 typedef typename std::conditional<
252 real_value_comparatort,
254
255public:
256 // interface
257
265 void erase(const key_type &k);
266
275 {
276 if(has_key(k))
277 erase(k);
278 }
279
288 template <class valueU>
289 void insert(const key_type &k, valueU &&m);
290
291 template <class valueU>
293 {
294 if(has_key(k))
295 {
296 replace(k, std::forward<valueU>(m));
297 }
298 else
299 {
300 insert(k, std::forward<valueU>(m));
301 }
302 }
303
312 template <class valueU>
313 void replace(const key_type &k, valueU &&m);
314
326 void update(const key_type &k, std::function<void(mapped_type &)> mutator);
327
336 std::optional<std::reference_wrapper<const mapped_type>>
337 find(const key_type &k) const;
338
342 void swap(sharing_mapt &other)
343 {
344 map.swap(other.map);
345
346 std::size_t tmp = num;
347 num = other.num;
348 other.num = tmp;
349 }
350
355 {
356 return num;
357 }
358
360 bool empty() const
361 {
362 return num == 0;
363 }
364
366 void clear()
367 {
368 map.clear();
369 num = 0;
370 }
371
377 bool has_key(const key_type &k) const
378 {
379 return get_leaf_node(k) != nullptr;
380 }
381
382 // views
383
384 typedef std::pair<const key_type &, const mapped_type &> view_itemt;
385
388 typedef std::vector<view_itemt> viewt;
389 typedef std::set<view_itemt> sorted_viewt;
390
392 {
393 v.push_back(vi);
394 }
395
397 {
398 v.insert(vi);
399 }
400
402 {
403 public:
405 const key_type &k,
406 const mapped_type &m,
407 const mapped_type &other_m)
408 : k(k), m(m), other_m(&other_m)
409 {
410 }
411
413 : k(k), m(m), other_m(nullptr)
414 {
415 }
416
417 const key_type &k;
418
420
421 bool is_in_both_maps() const
422 {
423 return other_m != nullptr;
424 }
425
427 {
429 return *other_m;
430 }
431
432 private:
434 };
435
439 typedef std::vector<delta_view_itemt> delta_viewt;
440
450 template <class V>
451 void get_view(V &view) const;
453 {
454 viewt result;
455 get_view(result);
456 return result;
457 }
463 {
464 sorted_viewt result;
465 get_view(result);
466 return result;
467 }
468
503 const sharing_mapt &other,
505 const bool only_common = true) const;
506
508 const sharing_mapt &other,
509 const bool only_common = true) const;
510
514 void
515 iterate(std::function<void(const key_type &k, const mapped_type &m)> f) const
516 {
517 if(empty())
518 return;
519
520 iterate(map, f);
521 }
522
523#if !defined(_MSC_VER)
536 {
537 std::size_t num_nodes = 0;
538 std::size_t num_unique_nodes = 0;
539 std::size_t num_leafs = 0;
540 std::size_t num_unique_leafs = 0;
541 };
542
553 template <class Iterator>
554 static sharing_map_statst get_sharing_stats(
555 Iterator begin,
556 Iterator end,
557 std::function<sharing_mapt &(const Iterator)> f =
558 [](const Iterator it) -> sharing_mapt & { return *it; });
559
569 template <class Iterator>
570 static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end);
571#endif
572
573protected:
574 // helpers
575
577 const nodet *get_leaf_node(const key_type &k) const;
578
597 template <class valueU>
599 const std::size_t starting_level,
600 const std::size_t key_suffix,
601 const std::size_t bit_last,
602 nodet &inner,
603 const key_type &k,
604 valueU &&m);
605
607 const nodet &n,
608 std::function<void(const key_type &k, const mapped_type &m)> f) const;
609
625 const nodet &leaf,
626 const nodet &inner,
627 const std::size_t level,
629 const bool only_common) const;
630
632
634 bool leafs_only,
635 std::set<const void *> &marked,
636 bool mark = true) const;
637
638 static const std::size_t dummy_level;
639
640 // config
641 static const std::size_t bits;
642 static const std::size_t chunk;
643
644 // derived config
645 static const std::size_t mask;
646 static const std::size_t levels;
647
648 // key-value map
650
651 // number of elements in the map
653};
654
655SHARING_MAPT(void)
656::iterate(
657 const nodet &n,
658 std::function<void(const key_type &k, const mapped_type &m)> f) const
659{
660 SM_ASSERT(!n.empty());
661
662 std::stack<const nodet *> stack;
663 stack.push(&n);
664
665 do
666 {
667 const nodet *ip = stack.top();
668 stack.pop();
669
670 SM_ASSERT(!ip->empty());
671
672 if(ip->is_internal())
673 {
674 const to_mapt &m = ip->get_to_map();
675 SM_ASSERT(!m.empty());
676
677 for(const auto item : m)
678 {
679 stack.push(&item.second);
680 }
681 }
682 else if(ip->is_leaf())
683 {
684 f(ip->get_key(), ip->get_value());
685 }
686 else
687 {
689
690 const leaf_listt &ll = ip->get_container();
691 SM_ASSERT(!ll.empty());
692
693 for(const auto &l : ll)
694 {
695 f(l.get_key(), l.get_value());
696 }
697 }
698 } while(!stack.empty());
699}
700
701SHARING_MAPT(std::size_t)
702::count_unmarked_nodes(
704 std::set<const void *> &marked,
705 bool mark) const
706{
707 if(empty())
708 return 0;
709
710 unsigned count = 0;
711
712 std::stack<const nodet *> stack;
713 stack.push(&map);
714
715 do
716 {
717 const nodet *ip = stack.top();
718 SM_ASSERT(!ip->empty());
719 stack.pop();
720
721 const unsigned use_count = ip->use_count();
722
723 const void *raw_ptr =
724 ip->is_internal() ? (const void *)&ip->read_internal()
725 : ip->is_leaf() ? (const void *)&ip->read_leaf()
726 : (const void *)&ip->read_container();
727
728 if(use_count >= 2)
729 {
730 if(marked.find(raw_ptr) != marked.end())
731 {
732 continue;
733 }
734
735 if(mark)
736 {
737 marked.insert(raw_ptr);
738 }
739 }
740
741 if(ip->is_internal())
742 {
743 if(!leafs_only)
744 {
745 count++;
746 }
747
748 const to_mapt &m = ip->get_to_map();
749 SM_ASSERT(!m.empty());
750
751 for(const auto item : m)
752 {
753 stack.push(&item.second);
754 }
755 }
756 else if(ip->is_leaf())
757 {
758 count++;
759 }
760 else
761 {
763
764 if(!leafs_only)
765 {
766 count++;
767 }
768
769 const leaf_listt &ll = ip->get_container();
770 SM_ASSERT(!ll.empty());
771
772 for(const auto &l : ll)
773 {
774 stack.push(&l);
775 }
776 }
777 } while(!stack.empty());
778
779 return count;
780}
781
782#if !defined(_MSC_VER)
783SHARING_MAPT3(Iterator, , sharing_map_statst)
784::get_sharing_stats(
785 Iterator begin,
786 Iterator end,
787 std::function<sharing_mapt &(const Iterator)> f)
788{
789 std::set<const void *> marked;
791
792 // We do a separate pass over the tree for each statistic. This is not very
793 // efficient but the function is intended only for diagnosis purposes anyways.
794
795 // number of nodes
796 for(Iterator it = begin; it != end; it++)
797 {
798 sms.num_nodes += f(it).count_unmarked_nodes(false, marked, false);
799 }
800
801 SM_ASSERT(marked.empty());
802
803 // number of unique nodes
804 for(Iterator it = begin; it != end; it++)
805 {
806 sms.num_unique_nodes += f(it).count_unmarked_nodes(false, marked, true);
807 }
808
809 marked.clear();
810
811 // number of leafs
812 for(Iterator it = begin; it != end; it++)
813 {
814 sms.num_leafs += f(it).count_unmarked_nodes(true, marked, false);
815 }
816
817 SM_ASSERT(marked.empty());
818
819 // number of unique leafs
820 for(Iterator it = begin; it != end; it++)
821 {
822 sms.num_unique_leafs += f(it).count_unmarked_nodes(true, marked, true);
823 }
824
825 return sms;
826}
827
828SHARING_MAPT3(Iterator, , sharing_map_statst)
829::get_sharing_stats_map(Iterator begin, Iterator end)
830{
832 begin, end, [](const Iterator it) -> sharing_mapt & { return it->second; });
833}
834#endif
835
837{
838 SM_ASSERT(view.empty());
839
840 if(empty())
841 return;
842
843 auto f = [&view](const key_type &k, const mapped_type &m) {
844 insert_view_item(view, view_itemt(k, m));
845 };
846
847 iterate(map, f);
848}
849
850SHARING_MAPT(void)
852{
853 auto f = [&delta_view](const key_type &k, const mapped_type &m) {
854 delta_view.push_back(delta_view_itemt(k, m));
855 };
856
857 iterate(n, f);
858}
859
860SHARING_MAPT(void)::add_item_if_not_shared(
861 const nodet &leaf,
863 const std::size_t level,
866{
867 const auto &k = leaf.get_key();
868 std::size_t key = hash()(k);
869
870 key >>= level * chunk;
871
872 const nodet *ip = &inner;
874
875 while(true)
876 {
877 std::size_t bit = key & mask;
878
879 ip = ip->find_child(bit);
880
881 // only in first map
882 if(ip == nullptr)
883 {
884 if(!only_common)
885 {
886 delta_view.push_back({k, leaf.get_value()});
887 }
888
889 return;
890 }
891
892 SM_ASSERT(!ip->empty());
893
894 // potentially in both maps
895 if(ip->is_container())
896 {
897 for(const auto &l2 : ip->get_container())
898 {
899 if(leaf.shares_with(l2))
900 return;
901
902 if(leaf.get_key() == l2.get_key())
903 {
904 delta_view.push_back({k, leaf.get_value(), l2.get_value()});
905 return;
906 }
907 }
908
909 if(!only_common)
910 {
911 delta_view.push_back({k, leaf.get_value()});
912 }
913
914 return;
915 }
916
917 if(ip->is_leaf())
918 {
919 if(ip->shares_with(leaf))
920 return;
921
922 if(equalT()(leaf.get_key(), ip->get_key()))
923 {
924 delta_view.push_back({k, leaf.get_value(), ip->get_value()});
925 }
926 else if(!only_common)
927 {
928 delta_view.push_back({k, leaf.get_value()});
929 }
930
931 return;
932 }
933
934 key >>= chunk;
935 }
936}
937
938SHARING_MAPT(void)
939::get_delta_view(
940 const sharing_mapt &other,
943{
944 SM_ASSERT(delta_view.empty());
945
946 if(empty())
947 return;
948
949 if(other.empty())
950 {
951 if(!only_common)
952 {
953 gather_all(map, delta_view);
954 }
955
956 return;
957 }
958
959 typedef std::pair<const nodet *, const nodet *> stack_itemt;
960 std::stack<stack_itemt> stack;
961
962 std::stack<std::size_t> level_stack;
963
964 // We do a DFS "in lockstep" simultaneously on both maps. For
965 // corresponding nodes we check whether they are shared between the
966 // maps, and if not, we recurse into the corresponding subtrees.
967
968 // The stack contains the children of already visited nodes that we
969 // still have to visit during the traversal.
970
971 if(map.shares_with(other.map))
972 return;
973
974 stack.push(stack_itemt(&map, &other.map));
975 level_stack.push(0);
976
977 do
978 {
979 const stack_itemt &si = stack.top();
980
981 const nodet *ip1 = si.first;
982 const nodet *ip2 = si.second;
983
984 SM_ASSERT(!ip1->shares_with(*ip2));
985
986 stack.pop();
987
988 const std::size_t level = level_stack.top();
989 level_stack.pop();
990
991 SM_ASSERT(!ip1->empty());
992 SM_ASSERT(!ip2->empty());
993
994 if(ip1->is_internal())
995 {
996 SM_ASSERT(!ip2->is_container());
997
998 if(ip2->is_internal())
999 {
1000 for(const auto item : ip1->get_to_map())
1001 {
1002 const nodet &child = item.second;
1003
1004 const nodet *p;
1005 p = ip2->find_child(item.first);
1006
1007 if(p == nullptr)
1008 {
1009 if(!only_common)
1010 {
1011 gather_all(child, delta_view);
1012 }
1013 }
1014 else if(!child.shares_with(*p))
1015 {
1016 stack.push(stack_itemt(&child, p));
1017 level_stack.push(level + 1);
1018 }
1019 }
1020 }
1021 else
1022 {
1023 SM_ASSERT(ip2->is_leaf());
1024
1025 for(const auto item : ip1->get_to_map())
1026 {
1027 const nodet &child = item.second;
1028
1029 if(!child.shares_with(*ip2))
1030 {
1031 stack.push(stack_itemt(&child, ip2));
1032
1033 // The level is not needed when the node of the left map is an
1034 // internal node, and the node of the right map is a leaf node,
1035 // hence we just push a dummy element
1036 level_stack.push(dummy_level);
1037 }
1038 }
1039 }
1040 }
1041 else if(ip1->is_leaf())
1042 {
1043 SM_ASSERT(!ip2->is_container());
1044
1045 if(ip2->is_internal())
1046 {
1047 SM_ASSERT(level != dummy_level);
1048
1049 add_item_if_not_shared(*ip1, *ip2, level, delta_view, only_common);
1050 }
1051 else
1052 {
1053 SM_ASSERT(ip2->is_leaf());
1054
1055 if(equalT()(ip1->get_key(), ip2->get_key()))
1056 {
1057 delta_view.push_back(
1058 {ip1->get_key(), ip1->get_value(), ip2->get_value()});
1059 }
1060 else if(!only_common)
1061 {
1062 delta_view.push_back({ip1->get_key(), ip1->get_value()});
1063 }
1064 }
1065 }
1066 else
1067 {
1068 SM_ASSERT(ip1->is_container());
1069 SM_ASSERT(!ip2->is_internal());
1070
1071 if(ip2->is_leaf())
1072 {
1073 for(const auto &l1 : ip1->get_container())
1074 {
1075 if(l1.shares_with(*ip2))
1076 {
1077 continue;
1078 }
1079
1080 const key_type &k1 = l1.get_key();
1081
1082 if(equalT()(k1, ip2->get_key()))
1083 {
1084 delta_view.push_back({k1, l1.get_value(), ip2->get_value()});
1085 }
1086 else if(!only_common)
1087 {
1088 delta_view.push_back({k1, l1.get_value()});
1089 }
1090 }
1091 }
1092 else
1093 {
1094 SM_ASSERT(ip2->is_container());
1095
1096 for(const auto &l1 : ip1->get_container())
1097 {
1098 const key_type &k1 = l1.get_key();
1099 const nodet *p;
1100
1101 p = ip2->find_leaf(k1);
1102
1103 if(p != nullptr)
1104 {
1105 if(!l1.shares_with(*p))
1106 {
1107 SM_ASSERT(other.has_key(k1));
1108 delta_view.push_back({k1, l1.get_value(), p->get_value()});
1109 }
1110 }
1111 else if(!only_common)
1112 {
1113 SM_ASSERT(!other.has_key(k1));
1114 delta_view.push_back({k1, l1.get_value()});
1115 }
1116 }
1117 }
1118 }
1119 } while(!stack.empty());
1120}
1121
1122SHARING_MAPT2(, delta_viewt)::get_delta_view(
1123 const sharing_mapt &other,
1125{
1127 get_delta_view(other, delta_view, only_common);
1128 return delta_view;
1129}
1130
1131SHARING_MAPT2(, nodet &)::get_leaf_node(const key_type &k)
1132{
1133 SM_ASSERT(has_key(k));
1134
1135 std::size_t key = hash()(k);
1136 nodet *ip = &map;
1138
1139 while(true)
1140 {
1141 std::size_t bit = key & mask;
1142
1143 ip = &ip->add_child(bit);
1144 PRECONDITION(!ip->empty()); // since the key must exist in the map
1145
1146 if(ip->is_internal())
1147 {
1148 key >>= chunk;
1149 continue;
1150 }
1151 else if(ip->is_leaf())
1152 {
1153 return *ip;
1154 }
1155 else
1156 {
1158 return *ip->find_leaf(k);
1159 }
1160 }
1161}
1162
1163SHARING_MAPT2(const, nodet *)::get_leaf_node(const key_type &k) const
1164{
1165 if(empty())
1166 return nullptr;
1167
1168 std::size_t key = hash()(k);
1169 const nodet *ip = &map;
1171
1172 while(true)
1173 {
1174 std::size_t bit = key & mask;
1175
1176 ip = ip->find_child(bit);
1177
1178 if(ip == nullptr)
1179 return nullptr;
1180
1181 SM_ASSERT(!ip->empty());
1182
1183 if(ip->is_internal())
1184 {
1185 key >>= chunk;
1186 continue;
1187 }
1188 else if(ip->is_leaf())
1189 {
1190 return equalT()(ip->get_key(), k) ? ip : nullptr;
1191 }
1192 else
1193 {
1195 return ip->find_leaf(k); // returns nullptr if leaf is not found
1196 }
1197 }
1198
1200 return nullptr;
1201}
1202
1204{
1205 SM_ASSERT(has_key(k));
1206
1207 nodet *del = nullptr;
1208 std::size_t del_bit = 0;
1209
1210 std::size_t key = hash()(k);
1211 nodet *ip = &map;
1212
1213 while(true)
1214 {
1215 std::size_t bit = key & mask;
1216
1217 const to_mapt &m = as_const_ptr(ip)->get_to_map();
1218
1219 if(m.size() > 1 || del == nullptr)
1220 {
1221 del = ip;
1222 del_bit = bit;
1223 }
1224
1225 ip = &ip->add_child(bit);
1226
1227 PRECONDITION(!ip->empty());
1228
1229 if(ip->is_internal())
1230 {
1231 key >>= chunk;
1232 continue;
1233 }
1234 else if(ip->is_leaf())
1235 {
1236 PRECONDITION(equalT()(ip->get_key(), k));
1237 del->remove_child(del_bit);
1238
1239 num--;
1240
1241 return;
1242 }
1243 else
1244 {
1246 const leaf_listt &ll = as_const_ptr(ip)->get_container();
1247 PRECONDITION(!ll.empty());
1248
1249 // forward list has one element
1250 if(std::next(ll.begin()) == ll.end())
1251 {
1252 PRECONDITION(equalT()(ll.front().get_key(), k));
1253 del->remove_child(del_bit);
1254 }
1255 else
1256 {
1257 ip->remove_leaf(k);
1258 }
1259
1260 num--;
1261
1262 return;
1263 }
1264 }
1265
1267}
1268
1269SHARING_MAPT4(valueU, void)
1270::migrate(
1274 nodet &inner,
1275 const key_type &k,
1276 valueU &&m)
1277{
1278 SM_ASSERT(starting_level < levels - 1);
1279 SM_ASSERT(inner.is_defined_internal());
1280
1281 nodet &leaf = inner.add_child(bit_last);
1282 SM_ASSERT(leaf.is_defined_leaf());
1283
1284 std::size_t key_existing = hash()(leaf.get_key());
1285 key_existing >>= chunk * starting_level;
1286
1288 leaf_kept.swap(leaf);
1289
1290 nodet *ip = &leaf;
1291 SM_ASSERT(ip->empty());
1292
1293 // Find place for both elements
1294
1295 std::size_t level = starting_level + 1;
1296 std::size_t key = key_suffix;
1297
1298 key_existing >>= chunk;
1299 key >>= chunk;
1300
1301 SM_ASSERT(level < levels);
1302
1303 do
1304 {
1305 SM_ASSERT(ip->empty());
1306
1307 std::size_t bit_existing = key_existing & mask;
1308 std::size_t bit = key & mask;
1309
1310 if(bit != bit_existing)
1311 {
1312 // Place found
1313
1315 SM_ASSERT(l1.empty());
1316 l1.swap(leaf_kept);
1317
1318 nodet &l2 = ip->add_child(bit);
1319 SM_ASSERT(l2.empty());
1320 l2.make_leaf(k, std::forward<valueU>(m));
1321
1322 return;
1323 }
1324
1326 ip = &ip->add_child(bit);
1327
1328 key >>= chunk;
1329 key_existing >>= chunk;
1330
1331 level++;
1332 } while(level < levels);
1333
1334 // Hash collision, create container and add both elements to it
1335
1336 PRECONDITION(!equalT()(k, leaf_kept.get_key()));
1337
1338 SM_ASSERT(ip->empty());
1339 // Make container and add existing leaf
1340 ip->get_container().push_front(leaf_kept);
1341
1343 // Insert new element in same container
1344 ip->place_leaf(k, std::forward<valueU>(m));
1345}
1346
1347SHARING_MAPT4(valueU, void)
1348::insert(const key_type &k, valueU &&m)
1349{
1350 SM_ASSERT(!has_key(k));
1351
1352 std::size_t key = hash()(k);
1353 nodet *ip = &map;
1354
1355 // The root must be an internal node
1356 SM_ASSERT(ip->is_internal());
1357
1358 std::size_t level = 0;
1359
1360 while(true)
1361 {
1362 std::size_t bit = key & mask;
1363
1364 SM_ASSERT(ip != nullptr);
1365 SM_ASSERT(ip->is_internal());
1366 SM_ASSERT(level == 0 || !ip->empty());
1367
1368 nodet &child = ip->add_child(bit);
1369
1370 // Place is unoccupied
1371 if(child.empty())
1372 {
1373 if(level < levels - 1)
1374 {
1375 // Create leaf
1376 child.make_leaf(k, m);
1377 }
1378 else
1379 {
1380 SM_ASSERT(level == levels - 1);
1381
1382 // Create container and insert leaf
1383 child.place_leaf(k, std::forward<valueU>(m));
1384
1385 SM_ASSERT(child.is_defined_container());
1386 }
1387
1388 num++;
1389
1390 return;
1391 }
1392 else if(child.is_internal())
1393 {
1394 ip = &child;
1395 key >>= chunk;
1396 level++;
1397
1398 continue;
1399 }
1400 else if(child.is_leaf())
1401 {
1402 // migrate leaf downwards
1403 migrate(level, key, bit, *ip, k, std::forward<valueU>(m));
1404
1405 num++;
1406
1407 return;
1408 }
1409 else
1410 {
1411 SM_ASSERT(child.is_defined_container());
1412 SM_ASSERT(level == levels - 1);
1413
1414 // Add to the container
1415 child.place_leaf(k, std::forward<valueU>(m));
1416
1417 num++;
1418
1419 return;
1420 }
1421 }
1422}
1423
1424SHARING_MAPT4(valueU, void)
1426{
1427 nodet &lp = get_leaf_node(k);
1428
1429 INVARIANT(
1430 !value_equalt()(lp.get_value(), m),
1431 "values should not be replaced with equal values to maximize sharing");
1432
1433 lp.set_value(std::forward<valueU>(m));
1434}
1435
1436SHARING_MAPT(void)
1437::update(const key_type &k, std::function<void(mapped_type &)> mutator)
1438{
1439 nodet &lp = get_leaf_node(k);
1440
1441 value_comparatort comparator(lp.get_value());
1442
1443 lp.mutate_value(mutator);
1444
1445 INVARIANT(
1446 !comparator(lp.get_value()),
1447 "sharing_mapt::update should make some change. Consider using read-only "
1448 "method to check if an update is needed beforehand");
1449}
1450
1451SHARING_MAPT2(std::optional<std::reference_wrapper<const, mapped_type>>)::find(
1452 const key_type &k) const
1453{
1454 const nodet *lp = get_leaf_node(k);
1455
1456 if(lp == nullptr)
1457 return std::nullopt;
1458
1459 return std::optional<std::reference_wrapper<const mapped_type>>(
1460 lp->get_value());
1461}
1462
1463// static constants
1464
1465SHARING_MAPT(const std::size_t)::dummy_level = 0xff;
1466
1467SHARING_MAPT(const std::size_t)::bits = 30;
1468SHARING_MAPT(const std::size_t)::chunk = 3;
1469
1470SHARING_MAPT(const std::size_t)::mask = 0xffff >> (16 - chunk);
1471SHARING_MAPT(const std::size_t)::levels = bits / chunk;
1472
1473#endif
const T * as_const_ptr(T *t)
Return a pointer to the same object but ensures the type is pointer to const.
Definition as_const.h:21
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
delta_view_itemt(const key_type &k, const mapped_type &m)
const mapped_type & get_other_map_value() const
const mapped_type * other_m
delta_view_itemt(const key_type &k, const mapped_type &m, const mapped_type &other_m)
A map implemented as a tree where subtrees can be shared between different maps.
void add_item_if_not_shared(const nodet &leaf, const nodet &inner, const std::size_t level, delta_viewt &delta_view, const bool only_common) const
Add a delta item to the delta view if the value in the container (which must only contain a single le...
const nodet * get_leaf_node(const key_type &k) const
sharing_nodet< key_type, mapped_type > nodet
std::size_t count_unmarked_nodes(bool leafs_only, std::set< const void * > &marked, bool mark=true) const
void erase_if_exists(const key_type &k)
Erase element if it exists.
equalT key_equal
std::conditional< fail_if_equal, std::equal_to< valueT >, falset >::type value_equalt
static void insert_view_item(sorted_viewt &v, view_itemt &&vi)
void migrate(const std::size_t starting_level, const std::size_t key_suffix, const std::size_t bit_last, nodet &inner, const key_type &k, valueU &&m)
Move a leaf node further down the tree such as to resolve a collision with another key-value pair.
size_type size() const
Get number of elements in map.
void gather_all(const nodet &n, delta_viewt &delta_view) const
size_type num
std::size_t size_type
static const std::size_t mask
static sharing_map_statst get_sharing_stats(Iterator begin, Iterator end, std::function< sharing_mapt &(const Iterator)> f=[](const Iterator it) -> sharing_mapt &{ return *it;})
Get sharing stats.
std::conditional< fail_if_equal, real_value_comparatort, noop_value_comparatort >::type value_comparatort
void iterate(const nodet &n, std::function< void(const key_type &k, const mapped_type &m)> f) const
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
static void insert_view_item(viewt &v, view_itemt &&vi)
std::vector< key_type > keyst
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
void iterate(std::function< void(const key_type &k, const mapped_type &m)> f) const
Call a function for every key-value pair in the map.
void erase(const key_type &k)
Erase element, element must exist in map.
viewt get_view() const
bool has_key(const key_type &k) const
Check if key is in map.
nodet::to_mapt to_mapt
std::pair< const key_type &, const mapped_type & > view_itemt
nodet & get_leaf_node(const key_type &k)
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end)
Get sharing stats.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
static const std::size_t bits
valueT mapped_type
bool empty() const
Check if map is empty.
void swap(sharing_mapt &other)
Swap with other map.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
void clear()
Clear map.
std::optional< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
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.
static const std::size_t levels
static const std::size_t chunk
std::set< view_itemt > sorted_viewt
nodet::leaf_listt leaf_listt
static const std::size_t dummy_level
void insert_or_replace(const key_type &k, valueU &&m)
delta_viewt get_delta_view(const sharing_mapt &other, const bool only_common=true) const
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
bool is_defined_container() const
bool empty() const
bool is_defined_internal() const
void swap(sharing_nodet &other)
void place_leaf(const keyT &k, valueU &&v)
const leaf_listt & get_container() const
bool is_defined_leaf() const
const valueT & get_value() const
const d_it::innert * find_child(const std::size_t n) const
const d_it & read_internal() const
use_countt use_count() const
const leaft * find_leaf(const keyT &k) const
bool shares_with(const sharing_nodet &other) const
d_it::innert & add_child(const std::size_t n)
bool is_leaf() const
const to_mapt & get_to_map() const
bool is_container() const
const d_ct & read_container() const
void remove_leaf(const keyT &k)
const keyT & get_key() const
bool is_internal() const
const d_lt & read_leaf() const
STL namespace.
#define SHARING_MAPT(type)
Macro to abbreviate the out-of-class definitions of methods and static variables of sharing_mapt.
Definition sharing_map.h:48
#define SHARING_MAPTV(return_type, V)
Definition sharing_map.h:57
#define SHARING_MAPT3(template_parameter, cv_qualifiers, return_type)
Macro to abbreviate the out-of-class definitions of template methods of sharing_mapt with a single te...
Definition sharing_map.h:90
#define SM_ASSERT(b)
Definition sharing_map.h:39
#define SHARING_MAPT4(template_parameter, return_type)
Macro to abbreviate the out-of-class definitions of template methods of sharing_mapt with a single te...
#define SHARING_MAPT2(cv_qualifiers, return_type)
Macro to abbreviate the out-of-class definitions of methods of sharing_mapt with a return type that i...
Definition sharing_map.h:72
Sharing node.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool operator()(const mapped_type &lhs, const mapped_type &rhs)
bool operator()(const mapped_type &)
noop_value_comparatort(const mapped_type &)
bool operator()(const mapped_type &new_value)
real_value_comparatort(const mapped_type &old_value)
Stats about sharing between several sharing map instances.