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