CBMC
|
A map implemented as a tree where subtrees can be shared between different maps. More...
#include <sharing_map.h>
Classes | |
class | delta_view_itemt |
struct | falset |
struct | noop_value_comparatort |
struct | real_value_comparatort |
struct | sharing_map_statst |
Stats about sharing between several sharing map instances. More... | |
Public Types | |
typedef keyT | key_type |
typedef valueT | mapped_type |
typedef hashT | hash |
typedef equalT | key_equal |
typedef std::size_t | size_type |
typedef std::vector< key_type > | keyst |
typedef std::pair< const key_type &, const mapped_type & > | view_itemt |
typedef std::vector< view_itemt > | viewt |
View of the key-value pairs in the map. More... | |
typedef std::set< view_itemt > | sorted_viewt |
typedef std::vector< delta_view_itemt > | delta_viewt |
Delta view of the key-value pairs in two maps. More... | |
Public Member Functions | |
~sharing_mapt () | |
void | erase (const key_type &k) |
Erase element, element must exist in map. More... | |
void | erase_if_exists (const key_type &k) |
Erase element if it exists. More... | |
template<class valueU > | |
void | insert (const key_type &k, valueU &&m) |
Insert element, element must not exist in map. More... | |
template<class valueU > | |
void | insert_or_replace (const key_type &k, valueU &&m) |
template<class valueU > | |
void | replace (const key_type &k, valueU &&m) |
Replace element, element must exist in map. More... | |
void | update (const key_type &k, std::function< void(mapped_type &)> mutator) |
Update an element in place; element must exist in map. More... | |
std::optional< std::reference_wrapper< const mapped_type > > | find (const key_type &k) const |
Find element. More... | |
void | swap (sharing_mapt &other) |
Swap with other map. More... | |
size_type | size () const |
Get number of elements in map. More... | |
bool | empty () const |
Check if map is empty. More... | |
void | clear () |
Clear map. More... | |
bool | has_key (const key_type &k) const |
Check if key is in map. More... | |
template<class V > | |
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 references to the keys and values in the map. More... | |
viewt | get_view () const |
sorted_viewt | get_sorted_view () const |
Convenience function to get a sorted view of the map elements. More... | |
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. More... | |
delta_viewt | get_delta_view (const sharing_mapt &other, const bool only_common=true) const |
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. More... | |
template<class view_type > | |
void | get_view (view_type &view) const |
Static Public Member Functions | |
static void | insert_view_item (viewt &v, view_itemt &&vi) |
static void | insert_view_item (sorted_viewt &v, view_itemt &&vi) |
template<class Iterator > | |
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. More... | |
template<class Iterator > | |
static sharing_map_statst | get_sharing_stats_map (Iterator begin, Iterator end) |
Get sharing stats. More... | |
Protected Types | |
typedef sharing_nodet< key_type, mapped_type > | nodet |
typedef nodet::to_mapt | to_mapt |
typedef nodet::leaf_listt | leaf_listt |
typedef std::conditional< fail_if_equal, std::equal_to< valueT >, falset >::type | value_equalt |
typedef std::conditional< fail_if_equal, real_value_comparatort, noop_value_comparatort >::type | value_comparatort |
Protected Member Functions | |
nodet & | get_leaf_node (const key_type &k) |
const nodet * | get_leaf_node (const key_type &k) const |
template<class valueU > | |
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. More... | |
void | iterate (const nodet &n, std::function< void(const key_type &k, const mapped_type &m)> f) const |
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 leaf) is not shared with any of the values in the subtree below inner . More... | |
void | gather_all (const nodet &n, delta_viewt &delta_view) const |
std::size_t | count_unmarked_nodes (bool leafs_only, std::set< const void * > &marked, bool mark=true) const |
Protected Attributes | |
nodet | map |
size_type | num = 0 |
Static Protected Attributes | |
static const std::size_t | dummy_level = 0xff |
static const std::size_t | bits = 30 |
static const std::size_t | chunk = 3 |
static const std::size_t | mask = 0xffff >> (16 - chunk) |
static const std::size_t | levels = bits / chunk |
A map implemented as a tree where subtrees can be shared between different maps.
The map is implemented as a variable-height n-ary trie.
When inserting a key-value pair into the map, first the hash of its key is computed. The bits
number of lower order bits of the hash are deemed significant, and are grouped into bits
/ chunk
chunks. The hash is then treated as a string (with each chunk representing a character) for the purposes of determining the position of the key-value pair in the trie. The actual key-value pairs are stored in the leaf nodes. Collisions (i.e., two different keys yield the same "string"), are handled by chaining the corresponding key-value pairs in a std::forward_list
.
The depth at which a key-value pair will be stored (when calling insert()) depends on the shortest unique prefix of its hash code (treated as a string) with respect to the hash codes of the key-value pairs already in the map.
The use of a trie in combination with hashing has the advantage that the tree is unlikely to degenerate (if the number of hash collisions is low). This makes re-balancing operations unnecessary which do not interact well with sharing. A disadvantage is that the height of the tree is likely greater than if the elements had been stored in a balanced tree.
The nodes in the sharing map are objects of type sharing_nodet. A sharing node has a shared pointer (of type small_shared_n_way_ptrt) which can point to objects of type d_internalt, d_leaft, or d_containert (representing internal nodes, leaf nodes, and container nodes, the latter being used for chaining leafs in a linked list on hash collisions).
Sharing is initially generated when a map is assigned to another map or copied via the copy constructor. Then both maps contain a pointer to the root node of the tree that represents the maps. On subsequent modifications to one of the maps, nodes are copied and sharing is lessened as described in the following.
The replace(), update(), insert(), and erase() operations interact with sharing as follows:
The replace() and update() operations are the only methods where sharing could unnecessarily be broken. This would happen when replacing an old value with a new equal value, or calling update but making no change. The sharing map provides a debug mode to detect such cases. When the template parameter fail_if_equal
is set to true, then the replace() and update() methods yield an invariant violation when the new value is equal to the old value. For this to work, the type of the values stored in the map needs to have a defined equality operator (operator==).
In the descriptions of the methods of the sharing map we also give the complexity of the operations. We use the following symbols:
The first two symbols denote dynamic properties of a given map, whereas the last two symbols are static configuration parameters of the map class.
Definition at line 189 of file sharing_map.h.
typedef std::vector<delta_view_itemt> sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::delta_viewt |
Delta view of the key-value pairs in two maps.
A delta view of two maps is a view of the key-value pairs in the maps that are contained in subtrees that are not shared between them (also see get_delta_view()).
Definition at line 439 of file sharing_map.h.
typedef hashT sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::hash |
Definition at line 199 of file sharing_map.h.
typedef equalT sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::key_equal |
Definition at line 200 of file sharing_map.h.
typedef keyT sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::key_type |
Definition at line 196 of file sharing_map.h.
typedef std::vector<key_type> sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::keyst |
Definition at line 204 of file sharing_map.h.
|
protected |
Definition at line 210 of file sharing_map.h.
typedef valueT sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::mapped_type |
Definition at line 197 of file sharing_map.h.
|
protected |
Definition at line 207 of file sharing_map.h.
typedef std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::size_type |
Definition at line 202 of file sharing_map.h.
typedef std::set<view_itemt> sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sorted_viewt |
Definition at line 389 of file sharing_map.h.
|
protected |
Definition at line 209 of file sharing_map.h.
|
protected |
Definition at line 253 of file sharing_map.h.
|
protected |
Definition at line 222 of file sharing_map.h.
typedef std::pair<const key_type &, const mapped_type &> sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::view_itemt |
Definition at line 384 of file sharing_map.h.
typedef std::vector<view_itemt> sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::viewt |
View of the key-value pairs in the map.
A view is a list of pairs with the components being const references to the keys and values in the map.
Definition at line 388 of file sharing_map.h.
|
inline |
Definition at line 192 of file sharing_map.h.
|
protected |
Add a delta item to the delta view if the value in the container
(which must only contain a single leaf) is not shared with any of the values in the subtree below inner
.
This method is called by get_delta_view()
when a container containing a single leaf is encountered in the first map, and the corresponding node in the second map is an inner node.
leaf | leaf node which is part of the first map in a call map1.get_delta_view(map2, ...) |
inner | inner node which is part of the second map |
level | depth of the nodes in the maps (both leaf and inner must be at the same depth in their respective maps) |
delta_view | delta view to add delta items to |
only_common | flag indicating if only items are added to the delta view for which the keys are in both maps |
Definition at line 860 of file sharing_map.h.
|
inline |
Clear map.
Definition at line 366 of file sharing_map.h.
|
protected |
Definition at line 702 of file sharing_map.h.
|
inline |
Check if map is empty.
Definition at line 360 of file sharing_map.h.
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::erase | ( | const key_type & | k | ) |
Erase element, element must exist in map.
Complexity:
k | The key of the element to erase |
Definition at line 1203 of file sharing_map.h.
|
inline |
Erase element if it exists.
Complexity:
k | The key of the element to erase |
Definition at line 274 of file sharing_map.h.
std::optional< std::reference_wrapper< const typename sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::mapped_type > > sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::find | ( | const key_type & | k | ) | const |
Find element.
Complexity:
k | The key of the element to search |
Definition at line 1451 of file sharing_map.h.
|
protected |
Definition at line 851 of file sharing_map.h.
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::delta_viewt sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::get_delta_view | ( | const sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT > & | other, |
const bool | only_common = true |
||
) | const |
Definition at line 1122 of file sharing_map.h.
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::get_delta_view | ( | const sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT > & | other, |
delta_viewt & | delta_view, | ||
const bool | only_common = true |
||
) | const |
Get a delta view of the elements in the map.
Informally, a delta view of two maps is a view of the key-value pairs in the maps that are contained in subtrees that are not shared between them.
A delta view is represented as a list of structs, with each struct having three members (key
, value1
, value2
). The elements key
, value1
, and value2
are const references to the corresponding elements in the map, with the third being absent if the key only existed in the queried map. The first element is the key, the second element is the mapped value of the first map, and the third element is the mapped value of the second map if present.
Calling A.delta_view(B, ...)
yields a view such that for each element in the view one of two things holds:
When only_common=true
, the first case above holds for every element in the view.
Complexity:
The symbols N1, M1 refer to map A, and symbols N2, M2 refer to map B.
other | other map | |
[out] | delta_view | Empty delta view |
only_common | Indicates if the returned delta view should only contain key-value pairs for keys that exist in both maps |
Definition at line 939 of file sharing_map.h.
|
protected |
Definition at line 1131 of file sharing_map.h.
|
protected |
Definition at line 1163 of file sharing_map.h.
|
static |
Get sharing stats.
Complexity:
begin | begin iterator |
end | end iterator |
f | function applied to the iterator to get a sharing map |
Definition at line 784 of file sharing_map.h.
|
static |
Get sharing stats.
Complexity:
begin | begin iterator of a map |
end | end iterator of a map |
Definition at line 829 of file sharing_map.h.
|
inline |
Convenience function to get a sorted view of the map elements.
A view is a list of pairs with the components being const references to the keys and values in the map.
Definition at line 462 of file sharing_map.h.
|
inline |
Definition at line 452 of file sharing_map.h.
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::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 references to the keys and values in the map.
Complexity:
[out] | view | Empty view |
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::get_view | ( | view_type & | view | ) | const |
Definition at line 836 of file sharing_map.h.
|
inline |
Check if key is in map.
Complexity:
Definition at line 377 of file sharing_map.h.
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::insert | ( | const key_type & | k, |
valueU && | m | ||
) |
Insert element, element must not exist in map.
Complexity:
k | The key of the element to insert |
m | The mapped value to insert |
Definition at line 1348 of file sharing_map.h.
|
inline |
Definition at line 292 of file sharing_map.h.
|
inlinestatic |
Definition at line 396 of file sharing_map.h.
|
inlinestatic |
Definition at line 391 of file sharing_map.h.
|
protected |
Definition at line 656 of file sharing_map.h.
|
inline |
Call a function for every key-value pair in the map.
Complexity: as sharing_mapt::get_view
Definition at line 515 of file sharing_map.h.
|
protected |
Move a leaf node further down the tree such as to resolve a collision with another key-value pair.
This method is called by insert()
to resolve a collision between a key-value pair to be newly inserted, and a key-value pair existing in the map.
starting_level | the depth of the inner node pointing to the leaf existing in the map |
key_suffix | hash code of the existing key in the map, shifted to the right by chunk * starting_level bits (i.e., key_suffix is the rest of the hash code used to determine the position of the key-value pair below level starting_level |
bit_last | last portion of the hash code of the key existing in the map (inner[bit_last] points to the leaf node to move further down the tree) |
inner | inner node of which the child inner[bit_last] is the leaf node to move further down the tree |
k | key of the element to be newly inserted |
m | value of the element to be newly inserted |
Definition at line 1270 of file sharing_map.h.
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::replace | ( | const key_type & | k, |
valueU && | m | ||
) |
Replace element, element must exist in map.
Complexity:
k | The key of the element to insert |
m | The mapped value to replace the old value with |
Definition at line 1425 of file sharing_map.h.
|
inline |
|
inline |
void sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::update | ( | const key_type & | k, |
std::function< void(mapped_type &)> | mutator | ||
) |
Update an element in place; element must exist in map.
Rationale: this avoids copy-out / edit / replace sequences without leaking a non-const reference
Complexity: as sharing_mapt::replace
k | The key of the element to update |
mutator | function to apply to the existing value. Must not store the reference; should make some change to the stored value (if you are unsure if you need to make a change, use find beforehand) |
Definition at line 1437 of file sharing_map.h.
|
staticprotected |
Definition at line 641 of file sharing_map.h.
|
staticprotected |
Definition at line 642 of file sharing_map.h.
|
staticprotected |
Definition at line 638 of file sharing_map.h.
|
staticprotected |
Definition at line 646 of file sharing_map.h.
|
protected |
Definition at line 649 of file sharing_map.h.
|
staticprotected |
Definition at line 645 of file sharing_map.h.
|
protected |
Definition at line 652 of file sharing_map.h.