|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Unit tests for dense_integer_map |
| 4 | +
|
| 5 | +Author: Diffblue Ltd |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include <testing-utils/use_catch.h> |
| 10 | + |
| 11 | +#include <util/dense_integer_map.h> |
| 12 | + |
| 13 | +TEST_CASE("no keys", "[core][util][dense_integer_map]") |
| 14 | +{ |
| 15 | + dense_integer_mapt<int, int> map; |
| 16 | + std::vector<int> empty; |
| 17 | + map.setup_for_keys(empty.begin(), empty.end()); |
| 18 | + |
| 19 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 20 | + |
| 21 | + REQUIRE_THROWS_AS(map.at(0), invariant_failedt); |
| 22 | + REQUIRE_THROWS_AS(map[0], invariant_failedt); |
| 23 | + REQUIRE_THROWS_AS(map.insert({0, 0}), invariant_failedt); |
| 24 | +} |
| 25 | + |
| 26 | +TEST_CASE("one key", "[core][util][dense_integer_map]") |
| 27 | +{ |
| 28 | + dense_integer_mapt<int, int> map; |
| 29 | + std::vector<int> allowed_keys = {1}; |
| 30 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 31 | + |
| 32 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 33 | + |
| 34 | + REQUIRE(map.size() == 0); |
| 35 | + |
| 36 | + REQUIRE_THROWS_AS(map.at(1), invariant_failedt); |
| 37 | + REQUIRE(!map.count(1)); |
| 38 | + REQUIRE(map[1] == 0); |
| 39 | + |
| 40 | + REQUIRE(map.size() == 1); |
| 41 | + REQUIRE(map.count(1)); |
| 42 | + |
| 43 | + map[1] = 2; |
| 44 | + REQUIRE(map.at(1) == 2); |
| 45 | + REQUIRE(map[1] == 2); |
| 46 | + |
| 47 | + auto insert_result = map.insert({1, 5}); |
| 48 | + REQUIRE(!insert_result.second); |
| 49 | + REQUIRE(insert_result.first == map.begin()); |
| 50 | + |
| 51 | + REQUIRE_THROWS_AS(map.at(0), invariant_failedt); |
| 52 | + REQUIRE_THROWS_AS(map[0], invariant_failedt); |
| 53 | + REQUIRE_THROWS_AS(map.insert({0, 0}), invariant_failedt); |
| 54 | +} |
| 55 | + |
| 56 | +TEST_CASE("insert fresh key", "[core][util][dense_integer_map]") |
| 57 | +{ |
| 58 | + dense_integer_mapt<int, int> map; |
| 59 | + std::vector<int> allowed_keys = {1}; |
| 60 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 61 | + |
| 62 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 63 | + |
| 64 | + auto insert_result = map.insert({1, 5}); |
| 65 | + REQUIRE(insert_result.second); |
| 66 | + REQUIRE(insert_result.first == map.begin()); |
| 67 | + |
| 68 | + REQUIRE(map.at(1) == 5); |
| 69 | + REQUIRE(map[1] == 5); |
| 70 | +} |
| 71 | + |
| 72 | +TEST_CASE("multiple, sparse keys", "[core][util][dense_integer_map]") |
| 73 | +{ |
| 74 | + dense_integer_mapt<int, int> map; |
| 75 | + std::vector<int> allowed_keys = {1, 10}; |
| 76 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 77 | + |
| 78 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 79 | + |
| 80 | + REQUIRE(map.size() == 0); |
| 81 | + |
| 82 | + map.insert({1, 2}); |
| 83 | + REQUIRE(map.size() == 1); |
| 84 | + auto second_insert_result = map.insert({10, 11}); |
| 85 | + REQUIRE(second_insert_result.second); |
| 86 | + REQUIRE(second_insert_result.first == std::next(map.begin())); |
| 87 | + |
| 88 | + REQUIRE_THROWS_AS(map[0], invariant_failedt); |
| 89 | + REQUIRE(map[1] == 2); |
| 90 | + // Keys in the gap are silently accepted, though this is bad practice: |
| 91 | + // REQUIRE_THROWS_AS(map[2], invariant_failedt); |
| 92 | + // REQUIRE_THROWS_AS(map[3], invariant_failedt); |
| 93 | + // REQUIRE_THROWS_AS(map[4], invariant_failedt); |
| 94 | + // REQUIRE_THROWS_AS(map[5], invariant_failedt); |
| 95 | + // REQUIRE_THROWS_AS(map[6], invariant_failedt); |
| 96 | + // REQUIRE_THROWS_AS(map[7], invariant_failedt); |
| 97 | + // REQUIRE_THROWS_AS(map[8], invariant_failedt); |
| 98 | + // REQUIRE_THROWS_AS(map[9], invariant_failedt); |
| 99 | + REQUIRE(map[10] == 11); |
| 100 | + REQUIRE_THROWS_AS(map[11], invariant_failedt); |
| 101 | +} |
| 102 | + |
| 103 | +TEST_CASE("iterators", "[core][util][dense_integer_map]") |
| 104 | +{ |
| 105 | + dense_integer_mapt<int, int> map; |
| 106 | + std::vector<int> allowed_keys = {1, 10}; |
| 107 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 108 | + |
| 109 | + map.insert({1, 5}); |
| 110 | + map.insert({10, 11}); |
| 111 | + |
| 112 | + std::vector<std::pair<int, int>> iterator_result{map.begin(), map.end()}; |
| 113 | + REQUIRE( |
| 114 | + iterator_result == std::vector<std::pair<int, int>>{{1, 5}, {10, 11}}); |
| 115 | + |
| 116 | + int acc = 0; |
| 117 | + for(auto &key_value : map) |
| 118 | + key_value.second = ++acc; |
| 119 | + |
| 120 | + iterator_result = std::vector<std::pair<int, int>>{map.begin(), map.end()}; |
| 121 | + REQUIRE(iterator_result == std::vector<std::pair<int, int>>{{1, 1}, {10, 2}}); |
| 122 | + |
| 123 | + REQUIRE(map.begin() != map.end()); |
| 124 | + REQUIRE(map.begin() != std::next(map.begin())); |
| 125 | + REQUIRE(map.begin() == map.begin()); |
| 126 | + REQUIRE(map.size() == 2); |
| 127 | + REQUIRE(std::distance(map.begin(), map.end()) == map.size()); |
| 128 | + |
| 129 | + { |
| 130 | + const auto &const_map = map; |
| 131 | + |
| 132 | + iterator_result = |
| 133 | + std::vector<std::pair<int, int>>{const_map.begin(), const_map.end()}; |
| 134 | + REQUIRE( |
| 135 | + iterator_result == std::vector<std::pair<int, int>>{{1, 1}, {10, 2}}); |
| 136 | + |
| 137 | + auto non_const_iterator = map.begin(); |
| 138 | + auto converted_non_const_iterator = |
| 139 | + (decltype(map)::const_iterator)non_const_iterator; |
| 140 | + auto const_iterator = const_map.begin(); |
| 141 | + auto other_const_iterator = const_map.begin(); |
| 142 | + |
| 143 | + REQUIRE(converted_non_const_iterator == const_iterator); |
| 144 | + REQUIRE(converted_non_const_iterator == other_const_iterator); |
| 145 | + } |
| 146 | +} |
| 147 | + |
| 148 | +TEST_CASE("keys must be unique", "[core][util][dense_integer_map]") |
| 149 | +{ |
| 150 | + dense_integer_mapt<int, int> map; |
| 151 | + std::vector<int> allowed_keys = {1, 1}; |
| 152 | + |
| 153 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 154 | + |
| 155 | + REQUIRE_THROWS_AS( |
| 156 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()), |
| 157 | + invariant_failedt); |
| 158 | + |
| 159 | + allowed_keys = {1, 2, 1}; |
| 160 | + REQUIRE_THROWS_AS( |
| 161 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()), |
| 162 | + invariant_failedt); |
| 163 | + |
| 164 | + allowed_keys = {1, 2}; |
| 165 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 166 | +} |
| 167 | + |
| 168 | +class reverse_orderingt |
| 169 | +{ |
| 170 | +public: |
| 171 | + int operator()(int x) |
| 172 | + { |
| 173 | + return 10 - x; |
| 174 | + } |
| 175 | +}; |
| 176 | + |
| 177 | +TEST_CASE( |
| 178 | + "ordering by custom key-to-integer function", |
| 179 | + "[core][util][dense_integer_map]") |
| 180 | +{ |
| 181 | + dense_integer_mapt<int, int, reverse_orderingt> map; |
| 182 | + std::vector<int> allowed_keys = {-20, 0, 20}; |
| 183 | + |
| 184 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 185 | + map.insert({0, 1}); |
| 186 | + map.insert({-20, 2}); |
| 187 | + map.insert({20, 3}); |
| 188 | + |
| 189 | + std::vector<std::pair<int, int>> iterator_result{map.begin(), map.end()}; |
| 190 | + |
| 191 | + REQUIRE( |
| 192 | + iterator_result == |
| 193 | + std::vector<std::pair<int, int>>{{20, 3}, {0, 1}, {-20, 2}}); |
| 194 | +} |
| 195 | + |
| 196 | +class index_is_mod2t |
| 197 | +{ |
| 198 | +public: |
| 199 | + int operator()(int x) |
| 200 | + { |
| 201 | + return x % 2; |
| 202 | + } |
| 203 | +}; |
| 204 | + |
| 205 | +TEST_CASE("indices must be unique", "[core][util][dense_integer_map]") |
| 206 | +{ |
| 207 | + dense_integer_mapt<int, int, index_is_mod2t> map; |
| 208 | + |
| 209 | + cbmc_invariants_should_throwt invariants_throw_in_this_scope; |
| 210 | + |
| 211 | + // Illegal keys (are equal mod 2) |
| 212 | + std::vector<int> allowed_keys = {2, 4}; |
| 213 | + REQUIRE_THROWS_AS( |
| 214 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()), |
| 215 | + invariant_failedt); |
| 216 | + |
| 217 | + // Legal keys (not equal mod 2) |
| 218 | + allowed_keys = {2, 3}; |
| 219 | + map.setup_for_keys(allowed_keys.begin(), allowed_keys.end()); |
| 220 | +} |
0 commit comments