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