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 #include <util/optional.h>
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 
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, 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
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  : 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>
124  // Type of this template instantiation
126  // Type of our containing \ref dense_integer_mapt
128 
129  public:
130  iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
132  {
133  it = skip_unset_values(it);
134  }
135 
138  operator iterator_templatet<
139  typename backing_storet::const_iterator,
140  const typename backing_storet::value_type>() const
141  {
143  }
144 
146  {
147  self_typet i = *this;
149  return i;
150  }
152  {
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  {
167  }
168  bool operator!=(const self_typet &rhs) const
169  {
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::size_t)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;
198  };
199 
200 public:
203  typedef iterator_templatet<
204  typename backing_storet::iterator,
205  typename backing_storet::value_type>
207 
210  typedef iterator_templatet<
211  typename backing_storet::const_iterator,
212  const typename backing_storet::value_type>
214 
216  {
217  }
218 
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 = (int64_t)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  std::size_t map_size = (std::size_t)((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  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(map_size);
261  for(Iter it = first; it != last; ++it)
262  map.at(key_to_index(*it)).first = *it;
263  value_set.resize(map_size);
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  auto index = key_to_index(pair.first);
292  auto signed_index =
293  static_cast<typename backing_storet::iterator::difference_type>(index);
294  iterator it{std::next(map.begin(), signed_index), *this};
295 
296  if(index_is_set(index))
297  return {it, false};
298  else
299  {
300  mark_index_set(index);
301  map.at(index).second = pair.second;
302  return {it, true};
303  }
304  }
305 
306  std::size_t count(const K &key) const
307  {
308  return index_is_set(key_to_index(key));
309  }
310 
311  std::size_t size() const
312  {
313  return n_values_set;
314  }
315 
317  {
318  return possible_keys_vector;
319  }
320 
322  {
323  return iterator{map.begin(), *this};
324  }
325 
327  {
328  return iterator{map.end(), *this};
329  }
330 
332  {
333  return const_iterator{map.begin(), *this};
334  }
335 
337  {
338  return const_iterator{map.end(), *this};
339  }
340 
342  {
343  return begin();
344  }
345 
347  {
348  return end();
349  }
350 };
351 
352 #endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H
dense_integer_mapt::possible_keys_vector
possible_keyst possible_keys_vector
Definition: dense_integer_map.h:86
dense_integer_mapt::at
V & at(const K &key)
Definition: dense_integer_map.h:275
dense_integer_mapt::setup_for_keys
void setup_for_keys(Iter first, Iter last)
Set the keys that are allowed to be used in this container.
Definition: dense_integer_map.h:227
dense_integer_mapt::iterator_templatet::iterator_templatet
iterator_templatet(UnderlyingIterator it, const map_typet &underlying_map)
Definition: dense_integer_map.h:130
dense_integer_mapt::const_iterator
iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type > const_iterator
const iterator.
Definition: dense_integer_map.h:213
identity_functort::operator()
constexpr T && operator()(T &&t) const
Definition: dense_integer_map.h:27
dense_integer_mapt::iterator_templatet::advance
UnderlyingIterator advance(UnderlyingIterator it)
Definition: dense_integer_map.h:175
dense_integer_mapt::operator[]
V & operator[](const K &key)
Definition: dense_integer_map.h:282
optional.h
dense_integer_mapt::value_set
std::vector< bool > value_set
Definition: dense_integer_map.h:77
dense_integer_mapt::backing_storet
std::vector< std::pair< K, V > > backing_storet
Definition: dense_integer_map.h:64
dense_integer_mapt::insert
std::pair< iterator, bool > insert(const std::pair< const K, V > &pair)
Definition: dense_integer_map.h:289
dense_integer_mapt::begin
const_iterator begin() const
Definition: dense_integer_map.h:331
invariant.h
dense_integer_mapt::n_values_set
std::size_t n_values_set
Definition: dense_integer_map.h:81
dense_integer_mapt::at
const V & at(const K &key) const
Definition: dense_integer_map.h:269
dense_integer_mapt::mark_index_set
void mark_index_set(std::size_t index)
Definition: dense_integer_map.h:99
dense_integer_mapt::size
std::size_t size() const
Definition: dense_integer_map.h:311
dense_integer_mapt::iterator_templatet::underlying_map
const map_typet & underlying_map
Definition: dense_integer_map.h:197
dense_integer_mapt::possible_keys
const possible_keyst & possible_keys() const
Definition: dense_integer_map.h:316
dense_integer_mapt::iterator_templatet::map_typet
dense_integer_mapt< K, V, KeyToDenseInteger > map_typet
Definition: dense_integer_map.h:127
dense_integer_mapt::iterator_templatet::operator++
self_typet operator++()
Definition: dense_integer_map.h:145
dense_integer_mapt::iterator_templatet::operator!=
bool operator!=(const self_typet &rhs) const
Definition: dense_integer_map.h:168
dense_integer_mapt::possible_keyst
std::vector< K > possible_keyst
Type of the container returned by possible_keys.
Definition: dense_integer_map.h:57
dense_integer_mapt::iterator_templatet::self_typet
iterator_templatet< UnderlyingIterator, UnderlyingValue > self_typet
Definition: dense_integer_map.h:125
dense_integer_mapt::iterator_templatet::operator->
base_typet::pointer operator->() const
Definition: dense_integer_map.h:160
identity_functort
Identity functor. When we use C++20 this can be replaced with std::identity.
Definition: dense_integer_map.h:23
dense_integer_mapt::offset
int64_t offset
Definition: dense_integer_map.h:62
dense_integer_mapt::end
iterator end()
Definition: dense_integer_map.h:326
dense_integer_mapt::cbegin
const_iterator cbegin() const
Definition: dense_integer_map.h:341
dense_integer_mapt::iterator_templatet::operator*
base_typet::reference operator*() const
Definition: dense_integer_map.h:156
dense_integer_mapt::map
backing_storet map
Definition: dense_integer_map.h:70
dense_integer_mapt::key_to_index
std::size_t key_to_index(const K &key) const
Definition: dense_integer_map.h:89
dense_integer_mapt::iterator_templatet::skip_unset_values
UnderlyingIterator skip_unset_values(UnderlyingIterator it)
Definition: dense_integer_map.h:181
dense_integer_mapt::end
const_iterator end() const
Definition: dense_integer_map.h:336
dense_integer_mapt::iterator_templatet::underlying_iterator
UnderlyingIterator underlying_iterator
Definition: dense_integer_map.h:196
dense_integer_mapt::iterator
iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type > iterator
iterator.
Definition: dense_integer_map.h:206
dense_integer_mapt::count
std::size_t count(const K &key) const
Definition: dense_integer_map.h:306
dense_integer_mapt::iterator_templatet::operator++
self_typet operator++(int junk)
Definition: dense_integer_map.h:151
dense_integer_mapt::dense_integer_mapt
dense_integer_mapt()
Definition: dense_integer_map.h:215
dense_integer_mapt::iterator_templatet::base_typet
std::iterator< std::forward_iterator_tag, UnderlyingValue > base_typet
Definition: dense_integer_map.h:123
dense_integer_mapt::begin
iterator begin()
Definition: dense_integer_map.h:321
dense_integer_mapt::cend
const_iterator cend() const
Definition: dense_integer_map.h:346
dense_integer_mapt::index_is_set
bool index_is_set(std::size_t index) const
Definition: dense_integer_map.h:109
dense_integer_mapt::iterator_templatet
Definition: dense_integer_map.h:118
dense_integer_mapt::iterator_templatet::operator==
bool operator==(const self_typet &rhs) const
Definition: dense_integer_map.h:164
validation_modet::INVARIANT
@ INVARIANT
dense_integer_mapt
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be ...
Definition: dense_integer_map.h:53