1 /**
2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3 * SPDX-License-Identifier: Apache-2.0.
4 */
5
6 #include <aws/common/private/hash_table_impl.h>
7 #include <proof_helpers/nondet.h>
8
9 /********************************************************************************
10 * This module represents a hash-table that is not backed by any actual memory
11 * It just takes non-det actions when given inputs. We know this is safe because
12 * we've already proven the c-common hash-table memory safe under these
13 * pre/post conditions.
14 *
15 * Since we're making almost everything nondet, the only externally visible property
16 * of the hash-table is the entry_count.
17 */
18
19 /**
20 * As noted above the only externally visible property of the hash-table is the [entry_count]. And it can vary between
21 * 0-SIZE_MAX. So there is really nothing to assert here */
aws_hash_table_is_valid(const struct aws_hash_table * map)22 bool aws_hash_table_is_valid(const struct aws_hash_table *map) {
23 return map && map->p_impl;
24 }
25
26 /**
27 * Given a pointer to a hash_iter, checks that it is well-formed, with all data-structure invariants.
28 */
aws_hash_iter_is_valid(const struct aws_hash_iter * iter)29 bool aws_hash_iter_is_valid(const struct aws_hash_iter *iter) {
30 if (!iter) {
31 return false;
32 }
33 if (!iter->map) {
34 return false;
35 }
36 if (!aws_hash_table_is_valid(iter->map)) {
37 return false;
38 }
39 if (iter->limit != iter->map->p_impl->entry_count) {
40 return false;
41 }
42
43 switch (iter->status) {
44 case AWS_HASH_ITER_STATUS_DONE:
45 /* Done iff slot == limit */
46 return iter->slot == iter->limit;
47 case AWS_HASH_ITER_STATUS_DELETE_CALLED:
48 /* iter->slot can underflow to SIZE_MAX after a delete
49 * see the comments for aws_hash_iter_delete() */
50 return iter->slot <= iter->limit;
51 case AWS_HASH_ITER_STATUS_READY_FOR_USE:
52 /* A slot must point to a valid location (i.e. hash_code != 0) */
53 return iter->slot < iter->limit;
54 }
55 /* Invalid status code */
56 return false;
57 }
58
59 /**
60 * Allocate a hash_table_state with no memory for the slots.
61 * Since CBMC runs with memory safety assertions on,
62 * CBMC will detect any attempt to use the slots.
63 * This ensures that no code will ever accidentally use the values
64 * in the slots, ensuring maximal nondeterminism.
65 */
make_hash_table_with_no_backing_store(struct aws_hash_table * map,size_t max_table_entries)66 void make_hash_table_with_no_backing_store(struct aws_hash_table *map, size_t max_table_entries) {
67 if (map != NULL) {
68 map->p_impl = malloc(sizeof(struct hash_table_state));
69 __CPROVER_assume(map->p_impl != NULL);
70 __CPROVER_assume(map->p_impl->entry_count <= max_table_entries);
71 }
72 }
73 /**
74 * Nondet clear. Since the only externally visible property of this
75 * table is the entry_count, just set it to 0
76 */
aws_hash_table_clear(struct aws_hash_table * map)77 void aws_hash_table_clear(struct aws_hash_table *map) {
78 AWS_PRECONDITION(aws_hash_table_is_valid(map));
79 struct hash_table_state *state = map->p_impl;
80 state->entry_count = 0;
81 AWS_POSTCONDITION(aws_hash_table_is_valid(map));
82 }
83
84 /**
85 * Nondet put. Since there is no backing store, we just non-determinstically either add it or don't.
86 */
aws_hash_table_put(struct aws_hash_table * map,const void * key,void * value,int * was_created)87 int aws_hash_table_put(struct aws_hash_table *map, const void *key, void *value, int *was_created) {
88 AWS_PRECONDITION(aws_hash_table_is_valid(map));
89
90 int track_was_created;
91 if (was_created) {
92 *was_created = track_was_created;
93 }
94
95 int rval;
96
97 struct hash_table_state *state = map->p_impl;
98
99 /* Avoid overflow */
100 if (state->entry_count == SIZE_MAX) {
101 return track_was_created ? AWS_OP_ERR : rval;
102 }
103
104 if (rval == AWS_OP_SUCCESS) {
105 state->entry_count++;
106 }
107 AWS_POSTCONDITION(aws_hash_table_is_valid(map));
108 return rval;
109 }
110
111 /**
112 * Not yet implemented
113 */
114 int aws_hash_table_remove_element(struct aws_hash_table *map, struct aws_hash_element *p_value);
115
116 /**
117 * Not yet implemented
118 */
119 int aws_hash_table_remove(
120 struct aws_hash_table *map,
121 const void *key,
122 struct aws_hash_element *p_value,
123 int *was_present);
124
125 /**
126 * Not yet implemented
127 */
128 int aws_hash_table_create(
129 struct aws_hash_table *map,
130 const void *key,
131 struct aws_hash_element **p_elem,
132 int *was_created);
133
134 /**
135 * Implements a version of aws_hash_table_find() that non-determinstially either:
136 * 1. Return NULL, indicating that the element didn't exist
137 * 2. Returns a newly created element. By default, just create a totally non-determinstic element.
138 * However, if the consumer of the stub uses the element, this may be insufficient. Use the same
139 * style of generator as the hash_iterator stubs, except with a different signature due to the different
140 * calling context.
141 *
142 * To declare a genarator:
143 * -DHASH_TABLE_FIND_ELEMENT_GENERATOR=the_generator_fn, where the_generator_fn has signature:
144 * the_generator_fnconst struct aws_hash_table *map, const void *key, struct aws_hash_element *p_elem).
145 *
146 * NOTE: If you want a version of aws_hash_table_find() that that ensures that the table actually has the found value
147 * when find returns success, that can be found in aws_hash_table_find_override.c
148 */
149 #ifdef HASH_TABLE_FIND_ELEMENT_GENERATOR
150 void HASH_TABLE_FIND_ELEMENT_GENERATOR(
151 const struct aws_hash_table *map,
152 const void *key,
153 struct aws_hash_element *p_elem);
154 #endif
155
aws_hash_table_find(const struct aws_hash_table * map,const void * key,struct aws_hash_element ** p_elem)156 int aws_hash_table_find(const struct aws_hash_table *map, const void *key, struct aws_hash_element **p_elem) {
157 AWS_PRECONDITION(aws_hash_table_is_valid(map), "Input hash_table [map] must be valid.");
158 AWS_PRECONDITION(AWS_OBJECT_PTR_IS_WRITABLE(p_elem), "Input pointer [p_elem] must be writable.");
159 const struct hash_table_state *const state = map->p_impl;
160 if (nondet_bool()) {
161 *p_elem = NULL;
162 } else {
163 *p_elem = malloc(sizeof(struct aws_hash_element));
164 #ifdef HASH_TABLE_FIND_ELEMENT_GENERATOR
165 HASH_TABLE_FIND_ELEMENT_GENERATOR(map, key, *p_elem);
166 #endif
167 }
168 AWS_POSTCONDITION(aws_hash_table_is_valid(map), "Output hash_table [map] must be valid.");
169 return AWS_OP_SUCCESS;
170 }
171
172 #ifdef HASH_ITER_ELEMENT_GENERATOR
173 void HASH_ITER_ELEMENT_GENERATOR(struct aws_hash_iter *new_iter, const struct aws_hash_iter *old_iter);
174 #endif
175
176 /* Simple map for what the iterator does: it just chugs along, returns a nondet value, until its gone at most
177 * map->entry_count times */
aws_hash_iter_begin(const struct aws_hash_table * map)178 struct aws_hash_iter aws_hash_iter_begin(const struct aws_hash_table *map) {
179 /* Leave it as non-det as possible */
180 AWS_PRECONDITION(aws_hash_table_is_valid(map));
181
182 /* Build a nondet iterator, set the required fields, and return it */
183 struct aws_hash_iter rval;
184 rval.map = map;
185 rval.limit = map->p_impl->entry_count;
186 rval.slot = 0;
187 rval.status = (rval.slot == rval.limit) ? AWS_HASH_ITER_STATUS_DONE : AWS_HASH_ITER_STATUS_READY_FOR_USE;
188 #ifdef HASH_ITER_ELEMENT_GENERATOR
189 HASH_ITER_ELEMENT_GENERATOR(&rval, NULL);
190 #endif
191 return rval;
192 }
193
aws_hash_iter_done(const struct aws_hash_iter * iter)194 bool aws_hash_iter_done(const struct aws_hash_iter *iter) {
195 AWS_PRECONDITION(aws_hash_iter_is_valid(iter));
196 AWS_PRECONDITION(
197 iter->status == AWS_HASH_ITER_STATUS_DONE || iter->status == AWS_HASH_ITER_STATUS_READY_FOR_USE,
198 "Input aws_hash_iter [iter] status should either be done or ready to use.");
199 bool rval = iter->slot == iter->limit;
200 assert(rval == (iter->status == AWS_HASH_ITER_STATUS_DONE));
201 return rval;
202 }
203
aws_hash_iter_next(struct aws_hash_iter * iter)204 void aws_hash_iter_next(struct aws_hash_iter *iter) {
205 AWS_PRECONDITION(aws_hash_iter_is_valid(iter));
206
207 if (iter->slot == iter->limit) {
208 iter->status = AWS_HASH_ITER_STATUS_DONE;
209 return;
210 }
211
212 /* Build a nondet iterator, set the required fields, and copy it over */
213 struct aws_hash_iter rval;
214 rval.map = iter->map;
215 rval.limit = iter->limit;
216 rval.slot = iter->slot + 1;
217 rval.status = (rval.slot == rval.limit) ? AWS_HASH_ITER_STATUS_DONE : AWS_HASH_ITER_STATUS_READY_FOR_USE;
218 #ifdef HASH_ITER_ELEMENT_GENERATOR
219 HASH_ITER_ELEMENT_GENERATOR(&rval, iter);
220 #endif
221
222 *iter = rval;
223 }
224
225 /* delete always leaves the element unusable, so we'll just leave the element totally nondet */
aws_hash_iter_delete(struct aws_hash_iter * iter,bool destroy_contents)226 void aws_hash_iter_delete(struct aws_hash_iter *iter, bool destroy_contents) {
227 AWS_PRECONDITION(aws_hash_iter_is_valid(iter));
228 AWS_PRECONDITION(
229 iter->status == AWS_HASH_ITER_STATUS_READY_FOR_USE, "Input aws_hash_iter [iter] must be ready for use.");
230 AWS_PRECONDITION(aws_hash_iter_is_valid(iter));
231 AWS_PRECONDITION(
232 iter->map->p_impl->entry_count > 0,
233 "The hash_table_state pointed by input [iter] must contain at least one entry.");
234
235 /* reduce the size of the underlying map */
236 iter->map->p_impl->entry_count--;
237
238 /* Build a nondet iterator, set the required fields, and copy it over */
239 struct aws_hash_iter rval;
240 rval.map = iter->map;
241 rval.slot = iter->slot;
242 rval.limit = iter->limit - 1;
243 rval.status = AWS_HASH_ITER_STATUS_DELETE_CALLED;
244 *iter = rval;
245 }
246