CBMC
dense_integer_map.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dense integer map
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
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 
23 {
24 public:
25  template <typename T>
26  constexpr T &&operator()(T &&t) const
27  {
28  return std::forward<T>(t);
29  }
30 };
31 
52 template <class K, class V, class KeyToDenseInteger = identity_functort>
54 {
55 public:
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-initialized and entries with a
68  // corresponding key but no value set yet have the correct key but a default-
69  // initialized value. Both of these are skipped by this type's iterators.
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, std::optional<V>>` in
75  // \ref map 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
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 - (std::size_t)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>
119  {
120  // Type of this template instantiation
122  // Type of our containing \ref dense_integer_mapt
124 
125  public:
126  // These types are defined such that the class is compatible with being
127  // treated as an STL iterator. For this to work, they must not be renamed.
128  using iterator_category = std::forward_iterator_tag;
129  using value_type = UnderlyingValue;
130  using difference_type = std::ptrdiff_t;
131  using pointer = UnderlyingValue *;
132  using reference = UnderlyingValue &;
133 
134  iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
136  {
137  it = skip_unset_values(it);
138  }
139 
143  typename backing_storet::const_iterator,
144  const typename backing_storet::value_type>() const
145  {
147  }
148 
150  {
151  self_typet i = *this;
153  return i;
154  }
156  {
158  return *this;
159  }
161  {
162  return *underlying_iterator;
163  }
165  {
166  return &*underlying_iterator;
167  }
168  bool operator==(const self_typet &rhs) const
169  {
171  }
172  bool operator!=(const self_typet &rhs) const
173  {
175  }
176 
177  private:
178  // Advance \ref it to the next map entry with an initialized value
179  UnderlyingIterator advance(UnderlyingIterator it)
180  {
181  return skip_unset_values(std::next(it));
182  }
183 
184  // Return the next iterator >= it with its value set
185  UnderlyingIterator skip_unset_values(UnderlyingIterator it)
186  {
187  auto iterator_pos = (std::size_t)std::distance(
188  underlying_map.map.begin(),
189  (typename backing_storet::const_iterator)it);
190  while((std::size_t)iterator_pos < underlying_map.map.size() &&
191  !underlying_map.value_set.at(iterator_pos))
192  {
193  ++iterator_pos;
194  ++it;
195  }
196  return it;
197  }
198 
199  // Wrapped std::vector iterator
200  UnderlyingIterator underlying_iterator;
202  };
203 
204 public:
207  typedef iterator_templatet<
208  typename backing_storet::iterator,
209  typename backing_storet::value_type>
211 
214  typedef iterator_templatet<
215  typename backing_storet::const_iterator,
216  const typename backing_storet::value_type>
218 
220  {
221  }
222 
230  template <typename Iter>
231  void setup_for_keys(Iter first, Iter last)
232  {
233  INVARIANT(
234  size() == 0,
235  "setup_for_keys must only be called on a newly-constructed container");
236 
237  int64_t highest_key = std::numeric_limits<int64_t>::min();
238  int64_t lowest_key = std::numeric_limits<int64_t>::max();
239  std::unordered_set<int64_t> seen_keys;
240  for(Iter it = first; it != last; ++it)
241  {
242  int64_t integer_key = (int64_t)KeyToDenseInteger{}(*it);
243  highest_key = std::max(integer_key, highest_key);
244  lowest_key = std::min(integer_key, lowest_key);
245  INVARIANT(
246  seen_keys.insert(integer_key).second,
247  "keys for use in dense_integer_mapt must be unique");
248  }
249 
250  if(highest_key < lowest_key)
251  {
252  offset = 0;
253  }
254  else
255  {
256  std::size_t map_size = (std::size_t)((highest_key - lowest_key) + 1);
257  INVARIANT(
258  map_size > 0, // overflowed?
259  "dense_integer_mapt size should fit in std::size_t");
260  INVARIANT(
261  map_size <= std::numeric_limits<std::size_t>::max(),
262  "dense_integer_mapt size should fit in std::size_t");
263  offset = lowest_key;
264  map.resize(map_size);
265  for(Iter it = first; it != last; ++it)
266  map.at(key_to_index(*it)).first = *it;
267  value_set.resize(map_size);
268  }
269 
270  possible_keys_vector.insert(possible_keys_vector.end(), first, last);
271  }
272 
273  const V &at(const K &key) const
274  {
275  std::size_t index = key_to_index(key);
276  INVARIANT(index_is_set(index), "map value should be set");
277  return map.at(index).second;
278  }
279  V &at(const K &key)
280  {
281  std::size_t index = key_to_index(key);
282  INVARIANT(index_is_set(index), "map value should be set");
283  return map.at(index).second;
284  }
285 
286  V &operator[](const K &key)
287  {
288  std::size_t index = key_to_index(key);
289  mark_index_set(index);
290  return map.at(index).second;
291  }
292 
293  std::pair<iterator, bool> insert(const std::pair<const K, V> &pair)
294  {
295  auto index = key_to_index(pair.first);
296  auto signed_index =
297  static_cast<typename backing_storet::iterator::difference_type>(index);
298  iterator it{std::next(map.begin(), signed_index), *this};
299 
300  if(index_is_set(index))
301  return {it, false};
302  else
303  {
304  mark_index_set(index);
305  map.at(index).second = pair.second;
306  return {it, true};
307  }
308  }
309 
310  std::size_t count(const K &key) const
311  {
312  return index_is_set(key_to_index(key));
313  }
314 
315  std::size_t size() const
316  {
317  return n_values_set;
318  }
319 
321  {
322  return possible_keys_vector;
323  }
324 
326  {
327  return iterator{map.begin(), *this};
328  }
329 
331  {
332  return iterator{map.end(), *this};
333  }
334 
336  {
337  return const_iterator{map.begin(), *this};
338  }
339 
341  {
342  return const_iterator{map.end(), *this};
343  }
344 
346  {
347  return begin();
348  }
349 
351  {
352  return end();
353  }
354 };
355 
356 #endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H
std::forward_iterator_tag iterator_category
iterator_templatet< UnderlyingIterator, UnderlyingValue > self_typet
iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
bool operator==(const self_typet &rhs) const
bool operator!=(const self_typet &rhs) const
dense_integer_mapt< K, V, KeyToDenseInteger > map_typet
UnderlyingIterator skip_unset_values(UnderlyingIterator it)
UnderlyingIterator advance(UnderlyingIterator it)
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be ...
void setup_for_keys(Iter first, Iter last)
Set the keys that are allowed to be used in this container.
const_iterator cbegin() const
void mark_index_set(std::size_t index)
std::vector< K > possible_keyst
Type of the container returned by possible_keys.
iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type > const_iterator
const iterator.
const possible_keyst & possible_keys() const
possible_keyst possible_keys_vector
V & operator[](const K &key)
std::size_t count(const K &key) const
std::pair< iterator, bool > insert(const std::pair< const K, V > &pair)
iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type > iterator
iterator.
bool index_is_set(std::size_t index) const
const_iterator cend() const
std::size_t key_to_index(const K &key) const
std::vector< std::pair< K, V > > backing_storet
const_iterator end() const
backing_storet map
std::size_t n_values_set
V & at(const K &key)
std::size_t size() const
const V & at(const K &key) const
const_iterator begin() const
std::vector< bool > value_set
Identity functor. When we use C++20 this can be replaced with std::identity.
constexpr T && operator()(T &&t) const