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/hash_table.h> 7 #include <aws/common/private/hash_table_impl.h> 8 #include <proof_helpers/make_common_data_structures.h> 9 #include <proof_helpers/utils.h> 10 // Currently takes 4m40s 11 aws_hash_table_put_harness()12void aws_hash_table_put_harness() { 13 struct aws_hash_table map; 14 ensure_allocated_hash_table(&map, MAX_TABLE_SIZE); 15 __CPROVER_assume(aws_hash_table_is_valid(&map)); 16 map.p_impl->destroy_key_fn = nondet_bool() ? NULL : hash_proof_destroy_noop; 17 map.p_impl->destroy_value_fn = nondet_bool() ? NULL : hash_proof_destroy_noop; 18 map.p_impl->equals_fn = uninterpreted_equals_assert_inputs_nonnull; 19 map.p_impl->hash_fn = uninterpreted_hasher; 20 map.p_impl->alloc = aws_default_allocator(); 21 22 size_t empty_slot_idx; 23 __CPROVER_assume(aws_hash_table_has_an_empty_slot(&map, &empty_slot_idx)); 24 25 void *key; 26 void *value; 27 bool track_was_created; 28 int was_created; 29 struct hash_table_state old_state = *map.p_impl; 30 31 int rval = aws_hash_table_put(&map, key, value, track_was_created ? &was_created : NULL); 32 if (rval == AWS_OP_SUCCESS) { 33 if (track_was_created) { 34 assert(map.p_impl->entry_count == old_state.entry_count + was_created); 35 } else { 36 assert( 37 map.p_impl->entry_count == old_state.entry_count || 38 map.p_impl->entry_count == old_state.entry_count + 1); 39 } 40 } else { 41 assert(map.p_impl->entry_count == old_state.entry_count); 42 } 43 assert(aws_hash_table_is_valid(&map)); 44 } 45