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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
/**
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
* SPDX-License-Identifier: Apache-2.0.
*/
#include <aws/common/private/hash_table_impl.h>
#include <proof_helpers/utils.h>
void assert_bytes_match(const uint8_t *const a, const uint8_t *const b, const size_t len) {
assert(len == 0 || !a == !b);
if (len > 0 && a != NULL && b != NULL) {
size_t i;
__CPROVER_assume(i < len && len < MAX_MALLOC); /* prevent spurious pointer overflows */
assert(a[i] == b[i]);
}
}
void assert_all_bytes_are(const uint8_t *const a, const uint8_t c, const size_t len) {
if (len > 0 && a != NULL) {
size_t i;
__CPROVER_assume(i < len);
assert(a[i] == c);
}
}
void assert_all_zeroes(const uint8_t *const a, const size_t len) {
assert_all_bytes_are(a, 0, len);
}
void assert_byte_from_buffer_matches(const uint8_t *const buffer, const struct store_byte_from_buffer *const b) {
if (buffer && b) {
assert(*(buffer + b->index) == b->byte);
}
}
void save_byte_from_array(const uint8_t *const array, const size_t size, struct store_byte_from_buffer *const storage) {
if (size > 0 && array && storage) {
storage->index = nondet_size_t();
__CPROVER_assume(storage->index < size);
storage->byte = array[storage->index];
}
}
void assert_array_list_equivalence(
const struct aws_array_list *const lhs,
const struct aws_array_list *const rhs,
const struct store_byte_from_buffer *const rhs_byte) {
/* In order to be equivalent, either both are NULL or both are non-NULL */
if (lhs == rhs) {
return;
} else {
assert(lhs && rhs); /* if only one is null, they differ */
}
assert(lhs->alloc == rhs->alloc);
assert(lhs->current_size == rhs->current_size);
assert(lhs->length == rhs->length);
assert(lhs->item_size == rhs->item_size);
if (lhs->current_size > 0) {
assert_byte_from_buffer_matches((uint8_t *)lhs->data, rhs_byte);
}
}
void assert_byte_buf_equivalence(
const struct aws_byte_buf *const lhs,
const struct aws_byte_buf *const rhs,
const struct store_byte_from_buffer *const rhs_byte) {
/* In order to be equivalent, either both are NULL or both are non-NULL */
if (lhs == rhs) {
return;
} else {
assert(lhs && rhs); /* if only one is null, they differ */
}
assert(lhs->len == rhs->len);
assert(lhs->capacity == rhs->capacity);
assert(lhs->allocator == rhs->allocator);
if (lhs->len > 0) {
assert_byte_from_buffer_matches(lhs->buffer, rhs_byte);
}
}
void assert_byte_cursor_equivalence(
const struct aws_byte_cursor *const lhs,
const struct aws_byte_cursor *const rhs,
const struct store_byte_from_buffer *const rhs_byte) {
assert(!lhs == !rhs);
if (lhs && rhs) {
assert(lhs->len == rhs->len);
if (lhs->len > 0) {
assert_byte_from_buffer_matches(lhs->ptr, rhs_byte);
}
}
}
void save_byte_from_hash_table(const struct aws_hash_table *map, struct store_byte_from_buffer *storage) {
struct hash_table_state *state = map->p_impl;
size_t size_in_bytes;
__CPROVER_assume(hash_table_state_required_bytes(state->size, &size_in_bytes) == AWS_OP_SUCCESS);
save_byte_from_array((uint8_t *)state, size_in_bytes, storage);
}
void check_hash_table_unchanged(const struct aws_hash_table *map, const struct store_byte_from_buffer *storage) {
struct hash_table_state *state = map->p_impl;
uint8_t *byte_array = (uint8_t *)state;
assert(byte_array[storage->index] == storage->byte);
}
int nondet_compare(const void *const a, const void *const b) {
assert(a != NULL);
assert(b != NULL);
return nondet_int();
}
int __CPROVER_uninterpreted_compare(const void *const a, const void *const b);
int uninterpreted_compare(const void *const a, const void *const b) {
assert(a != NULL);
assert(b != NULL);
int rval = __CPROVER_uninterpreted_compare(a, b);
/* Compare is reflexive */
__CPROVER_assume(IMPLIES(a == b, rval == 0));
/* Compare is anti-symmetric*/
__CPROVER_assume(__CPROVER_uninterpreted_compare(b, a) == -rval);
/* If two things are equal, their hashes are also equal */
if (rval == 0) {
__CPROVER_assume(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b));
}
return rval;
}
bool nondet_equals(const void *const a, const void *const b) {
assert(a != NULL);
assert(b != NULL);
return nondet_bool();
}
bool __CPROVER_uninterpreted_equals(const void *const a, const void *const b);
uint64_t __CPROVER_uninterpreted_hasher(const void *const a);
/**
* Add assumptions that equality is reflexive and symmetric. Don't bother with
* transitivity because it doesn't cause any spurious proof failures on hash-table
*/
bool uninterpreted_equals(const void *const a, const void *const b) {
bool rval = __CPROVER_uninterpreted_equals(a, b);
/* Equals is reflexive */
__CPROVER_assume(IMPLIES(a == b, rval));
/* Equals is symmetric */
__CPROVER_assume(__CPROVER_uninterpreted_equals(b, a) == rval);
/* If two things are equal, their hashes are also equal */
if (rval) {
__CPROVER_assume(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b));
}
return rval;
}
bool uninterpreted_equals_assert_inputs_nonnull(const void *const a, const void *const b) {
assert(a != NULL);
assert(b != NULL);
return uninterpreted_equals(a, b);
}
uint64_t nondet_hasher(const void *a) {
assert(a != NULL);
return nondet_uint64_t();
}
/**
* Standard stub function to hash one item.
*/
uint64_t uninterpreted_hasher(const void *a) {
assert(a != NULL);
return __CPROVER_uninterpreted_hasher(a);
}
bool uninterpreted_predicate_fn(uint8_t value);
|
