Skip to content

Commit b867245

Browse files
committed
Add dense_integer_mapt type
This gives a map-like interface but vector-like lookup cost, ideal for mapping keys that have a bijection with densely packed integers, such as the location numbers of a well-formed goto_modelt or goto_programt.
1 parent aba7e75 commit b867245

File tree

1 file changed

+350
-0
lines changed

1 file changed

+350
-0
lines changed

src/util/dense_integer_map.h

Lines changed: 350 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,350 @@
1+
/*******************************************************************\
2+
3+
Module: Dense integer map
4+
5+
Author: Diffblue Ltd
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Dense integer map
11+
12+
#ifndef CPROVER_UTIL_DENSE_INTEGER_MAP_H
13+
#define CPROVER_UTIL_DENSE_INTEGER_MAP_H
14+
15+
#include <limits>
16+
#include <unordered_set>
17+
#include <vector>
18+
19+
#include <util/invariant.h>
20+
#include <util/optional.h>
21+
22+
/// Identity functor. When we use C++20 this can be replaced with std::identity.
23+
class identity_functort
24+
{
25+
public:
26+
template <typename T>
27+
constexpr T &&operator()(T &&t) const
28+
{
29+
return std::forward<T>(t);
30+
}
31+
};
32+
33+
/// A map type that is backed by a vector, which relies on the ability to (a)
34+
/// see the keys that might be used in advance of their usage, and (b) map those
35+
/// keys onto a dense range of integers. You should specialise
36+
/// key_to_dense_integer for your key type before using. If it maps your keys
37+
/// onto too sparse a range, considerable memory will be wasted, as well as time
38+
/// spent skipping over the unused indices while iterating.
39+
///
40+
/// Value type V must be default constructible.
41+
///
42+
/// The type is optimised for fast lookups at the expense of flexibility.
43+
/// It makes one compromise on the iterface of std::map / unordered_map: the
44+
/// iterator refers to a pair<key, optionalt<value>>, where the value optional
45+
/// will always be defined. This is because the backing store uses optionalt
46+
/// this way and we don't want to impose the price of copying the key and value
47+
/// each time we move the iterator just so we have a <const K, V> & to give out.
48+
///
49+
/// Undocumented functions with matching names have the same semantics as
50+
/// std::map equivalents (including perfect iterator stability, with ordering
51+
/// according to the given KeyToDenseInteger function)
52+
template <class K, class V, class KeyToDenseInteger = identity_functort>
53+
class dense_integer_mapt
54+
{
55+
public:
56+
/// Type of the container returned by \ref possible_keys
57+
typedef std::vector<K> possible_keyst;
58+
59+
private:
60+
// Offset between keys resulting from KeyToDenseInteger{}(key) and indices
61+
// into map.
62+
int64_t offset;
63+
64+
typedef std::vector<std::pair<K, V>> backing_storet;
65+
66+
// Main store: contains <key, value> pairs, where entries at positions with
67+
// no corresponding key are default-initialised and entries with a
68+
// corresponding key but no value set yet have the correct key but a default-
69+
// initialized key. Both of these are skipped by this type's iterators.
70+
backing_storet map;
71+
72+
// Indicates whether a given position in \ref map's value has been set, and
73+
// therefore whether our iterators should stop at a given location. We use
74+
// this auxiliary structure rather than `pair<K, optionalt<V>>` in \ref map
75+
// because this way we can more easily return a std::map-like
76+
// std::pair<const K, V> & from the iterator.
77+
std::vector<bool> value_set;
78+
79+
// Population count (number of '1's) in value_set, i.e., number of keys whose
80+
// values have been set.
81+
std::size_t n_values_set;
82+
83+
// "Allowed" keys passed to \ref setup_for_keys. Attempting to use keys not
84+
// included in this vector may result in an invariant failure, but can
85+
// sometimes silently succeed
86+
possible_keyst possible_keys_vector;
87+
88+
// Convert a key into an index into \ref map
89+
std::size_t key_to_index(const K &key) const
90+
{
91+
auto key_integer = KeyToDenseInteger{}(key);
92+
INVARIANT(((int64_t)key_integer) >= offset, "index should be in range");
93+
auto ret = (std::size_t)key_integer - offset;
94+
INVARIANT(ret < map.size(), "index should be in range");
95+
return ret;
96+
}
97+
98+
// Note that \ref map entry at offset \ref index has been set.
99+
void mark_index_set(std::size_t index)
100+
{
101+
if(!value_set[index])
102+
{
103+
++n_values_set;
104+
value_set[index] = true;
105+
}
106+
}
107+
108+
// Has the \ref map entry at offset \ref index been set?
109+
bool index_is_set(std::size_t index) const
110+
{
111+
return value_set[index];
112+
}
113+
114+
// Support class used to implement both const and non-const iterators
115+
// This is just a std::vector iterator pointing into \ref map, but with an
116+
// operator++ that skips unset values.
117+
template <class UnderlyingIterator, class UnderlyingValue>
118+
class iterator_templatet
119+
: public std::iterator<std::forward_iterator_tag, UnderlyingValue>
120+
{
121+
// Type of the std::iterator support class we inherit
122+
typedef std::iterator<std::forward_iterator_tag, UnderlyingValue>
123+
base_typet;
124+
// Type of this template instantiation
125+
typedef iterator_templatet<UnderlyingIterator, UnderlyingValue> self_typet;
126+
// Type of our containing \ref dense_integer_mapt
127+
typedef dense_integer_mapt<K, V, KeyToDenseInteger> map_typet;
128+
129+
public:
130+
iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
131+
: underlying_iterator(it), underlying_map(underlying_map)
132+
{
133+
it = skip_unset_values(it);
134+
}
135+
136+
/// Convert iterator to const_iterator
137+
/// (redundant when defined in the const_iterator itself)
138+
operator iterator_templatet<
139+
typename backing_storet::const_iterator,
140+
const typename backing_storet::value_type>() const
141+
{
142+
return {underlying_iterator, underlying_map};
143+
}
144+
145+
self_typet operator++()
146+
{
147+
self_typet i = *this;
148+
underlying_iterator = advance(underlying_iterator);
149+
return i;
150+
}
151+
self_typet operator++(int junk)
152+
{
153+
underlying_iterator = advance(underlying_iterator);
154+
return *this;
155+
}
156+
typename base_typet::reference operator*() const
157+
{
158+
return *underlying_iterator;
159+
}
160+
typename base_typet::pointer operator->() const
161+
{
162+
return &*underlying_iterator;
163+
}
164+
bool operator==(const self_typet &rhs) const
165+
{
166+
return underlying_iterator == rhs.underlying_iterator;
167+
}
168+
bool operator!=(const self_typet &rhs) const
169+
{
170+
return underlying_iterator != rhs.underlying_iterator;
171+
}
172+
173+
private:
174+
// Advance \ref it to the next map entry with an initialized value
175+
UnderlyingIterator advance(UnderlyingIterator it)
176+
{
177+
return skip_unset_values(std::next(it));
178+
}
179+
180+
// Return the next iterator >= it with its value set
181+
UnderlyingIterator skip_unset_values(UnderlyingIterator it)
182+
{
183+
auto iterator_pos = std::distance(
184+
underlying_map.map.begin(),
185+
(typename backing_storet::const_iterator)it);
186+
while((std::size_t)iterator_pos < underlying_map.map.size() &&
187+
!underlying_map.value_set.at(iterator_pos))
188+
{
189+
++iterator_pos;
190+
++it;
191+
}
192+
return it;
193+
}
194+
195+
// Wrapped std::vector iterator
196+
UnderlyingIterator underlying_iterator;
197+
const map_typet &underlying_map;
198+
};
199+
200+
public:
201+
/// iterator. Stable with respect to all operations on this type once
202+
/// setup_for_keys has been called.
203+
typedef iterator_templatet<
204+
typename backing_storet::iterator,
205+
typename backing_storet::value_type>
206+
iterator;
207+
208+
/// const iterator. Stable with respect to all operations on this type once
209+
/// setup_for_keys has been called.
210+
typedef iterator_templatet<
211+
typename backing_storet::const_iterator,
212+
const typename backing_storet::value_type>
213+
const_iterator;
214+
215+
dense_integer_mapt() : offset(0), n_values_set(0)
216+
{
217+
}
218+
219+
/// Set the keys that are allowed to be used in this container. Checks that
220+
/// the integers produced for each key by \ref KeyToDenseInteger are unique
221+
/// and fall within a std::size_t's range (the integers are allowed to be
222+
/// negative so long as max(integers) - min(integers) <= max-size_t).
223+
/// This should be called before the container is used and not called again.
224+
/// Using keys not provided to this function with operator[], insert, at(...)
225+
/// etc may cause an invariant failure or undefined behaviour.
226+
template <typename Iter>
227+
void setup_for_keys(Iter first, Iter last)
228+
{
229+
INVARIANT(
230+
size() == 0,
231+
"setup_for_keys must only be called on a newly-constructed container");
232+
233+
int64_t highest_key = std::numeric_limits<int64_t>::min();
234+
int64_t lowest_key = std::numeric_limits<int64_t>::max();
235+
std::unordered_set<int64_t> seen_keys;
236+
for(Iter it = first; it != last; ++it)
237+
{
238+
int64_t integer_key = KeyToDenseInteger{}(*it);
239+
highest_key = std::max(integer_key, highest_key);
240+
lowest_key = std::min(integer_key, lowest_key);
241+
INVARIANT(
242+
seen_keys.insert(integer_key).second,
243+
"keys for use in dense_integer_mapt must be unique");
244+
}
245+
246+
if(highest_key < lowest_key)
247+
{
248+
offset = 0;
249+
}
250+
else
251+
{
252+
auto map_size = (highest_key - lowest_key) + 1;
253+
INVARIANT(
254+
map_size > 0, // overflowed?
255+
"dense_integer_mapt size should fit in std::size_t");
256+
INVARIANT(
257+
((std::size_t)map_size) <= std::numeric_limits<std::size_t>::max(),
258+
"dense_integer_mapt size should fit in std::size_t");
259+
offset = lowest_key;
260+
map.resize((highest_key - lowest_key) + 1);
261+
for(Iter it = first; it != last; ++it)
262+
map.at(key_to_index(*it)).first = *it;
263+
value_set.resize((highest_key - lowest_key) + 1);
264+
}
265+
266+
possible_keys_vector.insert(possible_keys_vector.end(), first, last);
267+
}
268+
269+
const V &at(const K &key) const
270+
{
271+
std::size_t index = key_to_index(key);
272+
INVARIANT(index_is_set(index), "map value should be set");
273+
return map.at(index).second;
274+
}
275+
V &at(const K &key)
276+
{
277+
std::size_t index = key_to_index(key);
278+
INVARIANT(index_is_set(index), "map value should be set");
279+
return map.at(index).second;
280+
}
281+
282+
V &operator[](const K &key)
283+
{
284+
std::size_t index = key_to_index(key);
285+
mark_index_set(index);
286+
return map.at(index).second;
287+
}
288+
289+
std::pair<iterator, bool> insert(const std::pair<const K, V> &pair)
290+
{
291+
std::size_t index = key_to_index(pair.first);
292+
iterator it{std::next(map.begin(), index), *this};
293+
294+
if(index_is_set(index))
295+
return {it, false};
296+
else
297+
{
298+
mark_index_set(index);
299+
map.at(index).second = pair.second;
300+
return {it, true};
301+
}
302+
}
303+
304+
std::size_t count(const K &key) const
305+
{
306+
return index_is_set(key_to_index(key));
307+
}
308+
309+
std::size_t size() const
310+
{
311+
return n_values_set;
312+
}
313+
314+
const possible_keyst &possible_keys() const
315+
{
316+
return possible_keys_vector;
317+
}
318+
319+
iterator begin()
320+
{
321+
return iterator{map.begin(), *this};
322+
}
323+
324+
iterator end()
325+
{
326+
return iterator{map.end(), *this};
327+
}
328+
329+
const_iterator begin() const
330+
{
331+
return const_iterator{map.begin(), *this};
332+
}
333+
334+
const_iterator end() const
335+
{
336+
return const_iterator{map.end(), *this};
337+
}
338+
339+
const_iterator cbegin() const
340+
{
341+
return begin();
342+
}
343+
344+
const_iterator cend() const
345+
{
346+
return end();
347+
}
348+
};
349+
350+
#endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H

0 commit comments

Comments
 (0)