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 <util/invariant.h>
16 
17 #include <cstdint>
18 #include <limits>
19 #include <unordered_set>
20 #include <vector>
21 
24 {
25 public:
26  template <typename T>
27  constexpr T &&operator()(T &&t) const
28  {
29  return std::forward<T>(t);
30  }
31 };
32 
53 template <class K, class V, class KeyToDenseInteger = identity_functort>
55 {
56 public:
58  typedef std::vector<K> possible_keyst;
59 
60 private:
61  // Offset between keys resulting from KeyToDenseInteger{}(key) and indices
62  // into map.
63  int64_t offset;
64 
65  typedef std::vector<std::pair<K, V>> backing_storet;
66 
67  // Main store: contains <key, value> pairs, where entries at positions with
68  // no corresponding key are default-initialized and entries with a
69  // corresponding key but no value set yet have the correct key but a default-
70  // initialized value. Both of these are skipped by this type's iterators.
72 
73  // Indicates whether a given position in \ref map's value has been set, and
74  // therefore whether our iterators should stop at a given location. We use
75  // this auxiliary structure rather than `pair<K, std::optional<V>>` in
76  // \ref map because this way we can more easily return a std::map-like
77  // std::pair<const K, V> & from the iterator.
78  std::vector<bool> value_set;
79 
80  // Population count (number of '1's) in value_set, i.e., number of keys whose
81  // values have been set.
82  std::size_t n_values_set;
83 
84  // "Allowed" keys passed to \ref setup_for_keys. Attempting to use keys not
85  // included in this vector may result in an invariant failure, but can
86  // sometimes silently succeed
88 
89  // Convert a key into an index into \ref map
90  std::size_t key_to_index(const K &key) const
91  {
92  auto key_integer = KeyToDenseInteger{}(key);
93  INVARIANT(((int64_t)key_integer) >= offset, "index should be in range");
94  auto ret = (std::size_t)key_integer - (std::size_t)offset;
95  INVARIANT(ret < map.size(), "index should be in range");
96  return ret;
97  }
98 
99  // Note that \ref map entry at offset \ref index has been set.
100  void mark_index_set(std::size_t index)
101  {
102  if(!value_set[index])
103  {
104  ++n_values_set;
105  value_set[index] = true;
106  }
107  }
108 
109  // Has the \ref map entry at offset \ref index been set?
110  bool index_is_set(std::size_t index) const
111  {
112  return value_set[index];
113  }
114 
115  // Support class used to implement both const and non-const iterators
116  // This is just a std::vector iterator pointing into \ref map, but with an
117  // operator++ that skips unset values.
118  template <class UnderlyingIterator, class UnderlyingValue>
120  {
121  // Type of this template instantiation
123  // Type of our containing \ref dense_integer_mapt
125 
126  public:
127  // These types are defined such that the class is compatible with being
128  // treated as an STL iterator. For this to work, they must not be renamed.
129  using iterator_category = std::forward_iterator_tag;
130  using value_type = UnderlyingValue;
131  using difference_type = std::ptrdiff_t;
132  using pointer = UnderlyingValue *;
133  using reference = UnderlyingValue &;
134 
135  iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
137  {
138  it = skip_unset_values(it);
139  }
140 
144  typename backing_storet::const_iterator,
145  const typename backing_storet::value_type>() const
146  {
148  }
149 
151  {
152  self_typet i = *this;
154  return i;
155  }
157  {
159  return *this;
160  }
162  {
163  return *underlying_iterator;
164  }
166  {
167  return &*underlying_iterator;
168  }
169  bool operator==(const self_typet &rhs) const
170  {
172  }
173  bool operator!=(const self_typet &rhs) const
174  {
176  }
177 
178  private:
179  // Advance \ref it to the next map entry with an initialized value
180  UnderlyingIterator advance(UnderlyingIterator it)
181  {
182  return skip_unset_values(std::next(it));
183  }
184 
185  // Return the next iterator >= it with its value set
186  UnderlyingIterator skip_unset_values(UnderlyingIterator it)
187  {
188  auto iterator_pos = (std::size_t)std::distance(
189  underlying_map.map.begin(),
190  (typename backing_storet::const_iterator)it);
191  while((std::size_t)iterator_pos < underlying_map.map.size() &&
192  !underlying_map.value_set.at(iterator_pos))
193  {
194  ++iterator_pos;
195  ++it;
196  }
197  return it;
198  }
199 
200  // Wrapped std::vector iterator
201  UnderlyingIterator underlying_iterator;
203  };
204 
205 public:
208  typedef iterator_templatet<
209  typename backing_storet::iterator,
210  typename backing_storet::value_type>
212 
215  typedef iterator_templatet<
216  typename backing_storet::const_iterator,
217  const typename backing_storet::value_type>
219 
221  {
222  }
223 
231  template <typename Iter>
232  void setup_for_keys(Iter first, Iter last)
233  {
234  INVARIANT(
235  size() == 0,
236  "setup_for_keys must only be called on a newly-constructed container");
237 
238  int64_t highest_key = std::numeric_limits<int64_t>::min();
239  int64_t lowest_key = std::numeric_limits<int64_t>::max();
240  std::unordered_set<int64_t> seen_keys;
241  for(Iter it = first; it != last; ++it)
242  {
243  int64_t integer_key = (int64_t)KeyToDenseInteger{}(*it);
244  highest_key = std::max(integer_key, highest_key);
245  lowest_key = std::min(integer_key, lowest_key);
246  INVARIANT(
247  seen_keys.insert(integer_key).second,
248  "keys for use in dense_integer_mapt must be unique");
249  }
250 
251  if(highest_key < lowest_key)
252  {
253  offset = 0;
254  }
255  else
256  {
257  std::size_t map_size = (std::size_t)((highest_key - lowest_key) + 1);
258  INVARIANT(
259  map_size > 0, // overflowed?
260  "dense_integer_mapt size should fit in std::size_t");
261  INVARIANT(
262  map_size <= std::numeric_limits<std::size_t>::max(),
263  "dense_integer_mapt size should fit in std::size_t");
264  offset = lowest_key;
265  map.resize(map_size);
266  for(Iter it = first; it != last; ++it)
267  map.at(key_to_index(*it)).first = *it;
268  value_set.resize(map_size);
269  }
270 
271  possible_keys_vector.insert(possible_keys_vector.end(), first, last);
272  }
273 
274  const V &at(const K &key) const
275  {
276  std::size_t index = key_to_index(key);
277  INVARIANT(index_is_set(index), "map value should be set");
278  return map.at(index).second;
279  }
280  V &at(const K &key)
281  {
282  std::size_t index = key_to_index(key);
283  INVARIANT(index_is_set(index), "map value should be set");
284  return map.at(index).second;
285  }
286 
287  V &operator[](const K &key)
288  {
289  std::size_t index = key_to_index(key);
290  mark_index_set(index);
291  return map.at(index).second;
292  }
293 
294  std::pair<iterator, bool> insert(const std::pair<const K, V> &pair)
295  {
296  auto index = key_to_index(pair.first);
297  auto signed_index =
298  static_cast<typename backing_storet::iterator::difference_type>(index);
299  iterator it{std::next(map.begin(), signed_index), *this};
300 
301  if(index_is_set(index))
302  return {it, false};
303  else
304  {
305  mark_index_set(index);
306  map.at(index).second = pair.second;
307  return {it, true};
308  }
309  }
310 
311  std::size_t count(const K &key) const
312  {
313  return index_is_set(key_to_index(key));
314  }
315 
316  std::size_t size() const
317  {
318  return n_values_set;
319  }
320 
322  {
323  return possible_keys_vector;
324  }
325 
327  {
328  return iterator{map.begin(), *this};
329  }
330 
332  {
333  return iterator{map.end(), *this};
334  }
335 
337  {
338  return const_iterator{map.begin(), *this};
339  }
340 
342  {
343  return const_iterator{map.end(), *this};
344  }
345 
347  {
348  return begin();
349  }
350 
352  {
353  return end();
354  }
355 };
356 
357 #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