Line data Source code
1 : #include <aws/common/math.h>
2 : #include <aws/common/private/hash_table_impl.h>
3 :
4 : #include <seahorn/seahorn.h>
5 :
6 : #include <hash_table_helper.h>
7 : #include <proof_allocators.h>
8 : #include <utils.h>
9 : #include <nondet.h>
10 :
11 0 : uint64_t nd_hash_fn(const void *key) {
12 0 : (void) key;
13 0 : return nd_uint64_t();
14 0 : }
15 :
16 0 : bool nd_hash_equals_fn(const void *a, const void *b) {
17 0 : return nd_bool();
18 0 : }
19 :
20 0 : void hash_proof_destroy_noop(void *p) {}
21 : void initialize_bounded_aws_hash_table(struct aws_hash_table *map,
22 2300000 : size_t max_table_entries) {
23 2300000 : size_t num_entries = nd_size_t();
24 2300000 : num_entries %= max_table_entries;
25 2300000 : size_t cur_num_entries = num_entries;
26 2300000 : // still aborts if overflow
27 2300000 : assume(aws_round_up_to_power_of_two(cur_num_entries, &num_entries) == AWS_OP_SUCCESS);
28 2300000 :
29 2300000 : size_t required_bytes;
30 2300000 : /* assume setting required_bytes is successful */
31 2300000 : assume(hash_table_state_required_bytes(num_entries, &required_bytes) ==
32 2300000 : AWS_OP_SUCCESS);
33 2300000 : struct hash_table_state *impl = bounded_malloc(required_bytes);
34 2300000 : impl->size = num_entries;
35 2300000 : impl->mask = num_entries - 1;
36 2300000 : impl->max_load_factor = 0.95;
37 2300000 : impl->alloc = sea_allocator();
38 2300000 : impl->hash_fn = &nd_hash_fn;
39 2300000 : impl->equals_fn = &nd_hash_equals_fn;
40 : #ifdef EXPLICIT_HASH_INIT
41 : /** hash_table_state is implicitly initializaed by memhavoc() inside bounded_malloc() */
42 : impl->destroy_key_fn = &hash_proof_destroy_noop;
43 : impl->destroy_value_fn = &hash_proof_destroy_noop;
44 : impl->entry_count = nd_size_t();
45 : impl->max_load = nd_size_t();
46 : #endif
47 :
48 2300000 : map->p_impl = impl;
49 2300000 : }
50 :
51 : void save_byte_from_hash_table(const struct aws_hash_table *map,
52 0 : struct store_byte_from_buffer *storage) {
53 0 : struct hash_table_state *state = map->p_impl;
54 0 : size_t size_in_bytes = nd_size_t();
55 0 : assume(hash_table_state_required_bytes(state->size, &size_in_bytes) ==
56 0 : AWS_OP_SUCCESS);
57 0 : save_byte_from_array((uint8_t *)state, size_in_bytes, storage);
58 0 : }
59 :
60 : void assert_hash_table_unchanged(const struct aws_hash_table *map,
61 0 : const struct store_byte_from_buffer *storage) {
62 0 : struct hash_table_state *state = map->p_impl;
63 0 : uint8_t *byte_array = (uint8_t *)state;
64 0 : assert_byte_from_buffer_matches((uint8_t *)state, storage);
65 0 : }
66 :
67 : bool hash_table_state_has_an_empty_slot(
68 0 : const struct hash_table_state *const state, size_t *const rval) {
69 0 : // assume(state->entry_count > 0);
70 0 : if (state->entry_count == 0) return false;
71 0 : for (size_t i = 0; i < state->size; i++) {
72 0 : const struct hash_table_entry *entry = &state->slots[i];
73 0 : if (entry->hash_code == 0) {
74 0 : return true;
75 0 : }
76 0 : }
77 0 : return false;
78 0 : }
79 :
80 : bool aws_hash_table_has_an_empty_slot(const struct aws_hash_table *const map,
81 0 : size_t *const rval) {
82 0 : return hash_table_state_has_an_empty_slot(map->p_impl, rval);
83 0 : }
84 :
85 0 : size_t aws_hash_table_deep_entry_count(const struct aws_hash_table *const map) {
86 0 : struct hash_table_state *state = map->p_impl;
87 0 : size_t rval = 0;
88 0 : for (size_t i = 0; i < state->size; i++) {
89 0 : struct hash_table_entry *entry = &state->slots[i];
90 0 : if (entry->hash_code){
91 0 : rval++;
92 0 : }
93 0 : }
94 0 : return rval;
95 0 : }
96 :
97 0 : bool aws_hash_table_entry_count_is_valid(const struct aws_hash_table *const map) {
98 0 : return map->p_impl->entry_count == aws_hash_table_deep_entry_count(map);
99 0 : }
100 :
101 0 : bool aws_hash_table_deep_is_empty(const struct aws_hash_table *const map) {
102 0 : struct hash_table_state *state = map->p_impl;
103 0 : bool rval = true;
104 0 : for (size_t i = 0; i < state->size; i++) {
105 0 : struct hash_table_entry *entry = &state->slots[i];
106 0 : rval = rval && (entry->hash_code == 0);
107 0 : }
108 0 : return rval;
109 0 : }
110 :
111 0 : enum aws_hash_iter_status nd_hash_iter_status() {
112 0 : enum aws_hash_iter_status status = nd_int();
113 0 : // status >= AWS_HASH_ITER_STATUS_DONE && status <= AWS_HASH_ITER_STATUS_READY_FOR_USE
114 0 : // assume(status >= AWS_HASH_ITER_STATUS_DONE &&
115 0 : // status <= AWS_HASH_ITER_STATUS_READY_FOR_USE);
116 0 : status %= AWS_HASH_ITER_STATUS_READY_FOR_USE;
117 0 : status = status < AWS_HASH_ITER_STATUS_DONE ? AWS_HASH_ITER_STATUS_DONE : status;
118 0 : return status;
119 0 : }
120 :
121 : void initialize_aws_hash_iter(struct aws_hash_iter *iter,
122 0 : struct aws_hash_table *map) {
123 0 : iter->map = map;
124 0 : iter->element.key = nd_voidp();
125 0 : iter->element.value = nd_voidp();
126 0 : iter->slot = nd_size_t();
127 0 : iter->limit = nd_size_t();
128 0 : // iter->limit <= iter->map->p_impl->size
129 0 : iter->limit %= iter->map->p_impl->size;
130 0 : // iter->slot < iter->limit
131 0 : iter->slot %= (iter->limit - 1);
132 0 : iter->status = nd_hash_iter_status();
133 0 : if (iter->status == AWS_HASH_ITER_STATUS_READY_FOR_USE) {
134 0 : // assume(map->p_impl->slots[iter->slot].hash_code > 0);
135 0 : uint64_t slot_code = map->p_impl->slots[iter->slot].hash_code;
136 0 : map->p_impl->slots[iter->slot].hash_code = slot_code == 0 ? 1 : slot_code;
137 0 : }
138 0 : }
139 :
140 : void mk_valid_aws_hash_iter(struct aws_hash_iter *iter,
141 0 : struct aws_hash_table *map) {
142 0 : initialize_aws_hash_iter(iter, map);
143 0 : assume(aws_hash_iter_is_valid(iter));
144 0 : }
145 :
146 144645 : void ensure_hash_table_has_valid_destroy_functions(struct aws_hash_table *map) {
147 144645 : map->p_impl->destroy_key_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
148 144645 : map->p_impl->destroy_value_fn = nd_bool() ? NULL : hash_proof_destroy_noop;
149 144645 : }
150 :
151 0 : bool uninterpreted_equals(const void *const a, const void *const b) {
152 0 : return nd_bool();
153 0 : }
154 :
155 0 : void uninterpreted_destroy_fn(void *key_or_val) { /** noop **/ }
|
