1 /** 2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. 3 * SPDX-License-Identifier: Apache-2.0. 4 */ 5 6 #pragma once 7 8 #include <aws/common/array_list.h> 9 #include <aws/common/byte_buf.h> 10 #include <aws/common/common.h> 11 #include <aws/common/linked_list.h> 12 #include <aws/common/priority_queue.h> 13 #include <aws/common/private/hash_table_impl.h> 14 #include <aws/common/ring_buffer.h> 15 #include <aws/common/string.h> 16 #include <proof_helpers/nondet.h> 17 #include <proof_helpers/utils.h> 18 19 #include <stdlib.h> 20 21 /* Assume valid memory for ptr, if count > 0 and count < MAX_MALLOC. */ 22 #define ASSUME_VALID_MEMORY_COUNT(ptr, count) \ 23 do { \ 24 ptr = malloc(sizeof(*(ptr)) * (count)); \ 25 __CPROVER_assume(ptr != NULL); \ 26 } while (0) 27 28 #define ASSUME_VALID_MEMORY(ptr) ASSUME_VALID_MEMORY_COUNT(ptr, sizeof(*(ptr))) 29 30 #define ASSUME_DEFAULT_ALLOCATOR(allocator) allocator = aws_default_allocator() 31 32 /* 33 * Checks whether aws_byte_buf is bounded by max_size 34 */ 35 bool aws_byte_buf_is_bounded(const struct aws_byte_buf *const buf, const size_t max_size); 36 37 /* 38 * Checks whether aws_byte_buf has the correct allocator 39 */ 40 bool aws_byte_buf_has_allocator(const struct aws_byte_buf *const buf); 41 42 /* 43 * Ensures aws_byte_buf has a proper allocated buffer member 44 */ 45 void ensure_byte_buf_has_allocated_buffer_member(struct aws_byte_buf *const buf); 46 47 /* 48 * Ensures aws_ring_buffer has proper allocated members 49 */ 50 void ensure_ring_buffer_has_allocated_members(struct aws_ring_buffer *ring_buf, const size_t size); 51 /* 52 * Checks whether aws_byte_cursor is bounded by max_size 53 */ 54 bool aws_byte_cursor_is_bounded(const struct aws_byte_cursor *const cursor, const size_t max_size); 55 56 /* 57 * Ensure a byte_buf is allocated within a ring_buf (a relational invariant) 58 */ 59 void ensure_byte_buf_has_allocated_buffer_member_in_ring_buf( 60 struct aws_byte_buf *buf, 61 struct aws_ring_buffer *ring_buf); 62 63 /* 64 * Ensures aws_byte_cursor has a proper allocated buffer member 65 */ 66 void ensure_byte_cursor_has_allocated_buffer_member(struct aws_byte_cursor *const cursor); 67 68 /* 69 * Checks whether aws_array_list is bounded by max_initial_item_allocation and max_item_size 70 */ 71 bool aws_array_list_is_bounded( 72 const struct aws_array_list *const list, 73 const size_t max_initial_item_allocation, 74 const size_t max_item_size); 75 76 /** 77 * Ensures the data member of an aws_array_list structure is correctly allocated 78 */ 79 void ensure_array_list_has_allocated_data_member(struct aws_array_list *const list); 80 81 /** 82 * Ensures that the aws_linked_list [list] is correctly allocated 83 */ 84 void ensure_linked_list_is_allocated(struct aws_linked_list *list, size_t max_length); 85 86 /* 87 * Checks whether aws_priority_queue is bounded by max_initial_item_allocation and max_item_size 88 */ 89 bool aws_priority_queue_is_bounded( 90 const struct aws_priority_queue *const queue, 91 const size_t max_initial_item_allocation, 92 const size_t max_item_size); 93 94 /** 95 * Ensures members of an aws_priority_queue structure are correctly 96 * allocated. 97 */ 98 void ensure_priority_queue_has_allocated_members(struct aws_priority_queue *const queue); 99 100 /* 101 * Ensures aws_hash_table has a proper allocated p_impl member 102 */ 103 void ensure_allocated_hash_table(struct aws_hash_table *map, size_t max_table_entries); 104 105 /* 106 * Ensures aws_hash_table has destroy function pointers that are enther null or valid 107 */ 108 void ensure_hash_table_has_valid_destroy_functions(struct aws_hash_table *map); 109 110 /** 111 * A correct hash table has max_load < size. This means that there is always one slot empty. 112 * These functions are useful for assuming that there is some (nondet) slot which is empty 113 * which is necessary to prove termination for hash-table deletion code. Should only be used inside 114 * an assume because of the way it does nondet. 115 */ 116 bool aws_hash_table_has_an_empty_slot(const struct aws_hash_table *const map, size_t *const rval); 117 bool hash_table_state_has_an_empty_slot(const struct hash_table_state *const state, size_t *const rval); 118 119 /** 120 * A correct implementation of the hash_destroy function should never have a memory 121 * error on valid input. There is the question of whether the destroy functions themselves 122 * are correctly called (i.e. only on valid input, no double free, etc.). Testing this would 123 * require a stronger function here. 124 */ 125 void hash_proof_destroy_noop(void *p); 126 127 /** 128 * Ensures a valid string is allocated, with as much nondet as possible 129 */ 130 struct aws_string *ensure_string_is_allocated_nondet_length(); 131 132 /** 133 * Ensures a valid string is allocated, with as much nondet as possible, but len < max 134 */ 135 struct aws_string *nondet_allocate_string_bounded_length(size_t max_size); 136 137 /** 138 * Ensures a valid string is allocated, with as much nondet as possible, but fixed defined len 139 */ 140 struct aws_string *ensure_string_is_allocated(size_t size); 141 142 /** 143 * Ensures a valid const string is allocated, with as much nondet as possible, len < max_size 144 */ 145 const char *ensure_c_str_is_allocated(size_t max_size); 146