Line data Source code
1 : /*
2 : *
3 : */
4 :
5 : #include <stdlib.h> // for exit()
6 :
7 : #include <aws/common/private/hash_table_impl.h>
8 : #include <bounds.h>
9 : #include <proof_allocators.h>
10 : #include <seahorn/seahorn.h>
11 : #include <utils.h>
12 :
13 : void assert_bytes_match(const uint8_t *const a, const uint8_t *const b,
14 2140836 : const size_t len) {
15 2140836 : sassert(len == 0 || !a == !b);
16 2140836 : if (len > 0 && a != NULL && b != NULL) {
17 1846975 : size_t i = nd_size_t();
18 1846975 : /* prevent spurious pointer overflows */
19 1846975 : assume(i < len && len < MAX_MALLOC);
20 1846975 : sassert(a[i] == b[i]);
21 1846975 : }
22 2140836 : }
23 :
24 : void assert_all_bytes_are(const uint8_t *const a, const uint8_t c,
25 406283 : const size_t len) {
26 406283 : if (len > 0 && a != NULL) {
27 405649 : size_t i = nd_size_t();
28 405649 : assume(i < len);
29 405649 : sassert(a[i] == c);
30 405649 : }
31 406283 : }
32 :
33 333057 : void assert_all_zeroes(const uint8_t *const a, const size_t len) {
34 333057 : assert_all_bytes_are(a, 0, len);
35 333057 : }
36 :
37 : void assert_byte_from_buffer_matches(
38 684631 : const uint8_t *const buffer, const struct store_byte_from_buffer *const b) {
39 684631 : if (buffer && b) {
40 684631 : sassert(*(buffer + b->index) == b->byte);
41 684631 : }
42 684631 : }
43 :
44 : void save_byte_from_array(const uint8_t *const array, const size_t size,
45 8124379 : struct store_byte_from_buffer *const storage) {
46 8124379 : storage->index = nd_size_t();
47 8124379 : if (size > 0 && array && storage) {
48 5521667 : assume(storage->index < size);
49 5521667 : storage->byte = array[storage->index];
50 5587835 : } else {
51 2602712 : storage->byte = nd_uint8_t();
52 2602712 : }
53 8124379 : }
54 :
55 : void assert_array_list_equivalence(
56 : const struct aws_array_list *const lhs,
57 : const struct aws_array_list *const rhs,
58 504080 : const struct store_byte_from_buffer *const rhs_byte) {
59 504080 : /* In order to be equivalent, either both are NULL or both are non-NULL */
60 504080 : if (lhs == rhs) {
61 0 : return;
62 504080 : } else {
63 504080 : sassert(lhs && rhs); /* if only one is null, they differ */
64 504080 : }
65 504080 : sassert(lhs->alloc == rhs->alloc);
66 504080 : sassert(lhs->current_size == rhs->current_size);
67 504080 : sassert(lhs->length == rhs->length);
68 504080 : sassert(lhs->item_size == rhs->item_size);
69 504080 : if (lhs->current_size > 0) {
70 177329 : assert_byte_from_buffer_matches((uint8_t *)lhs->data, rhs_byte);
71 177329 : }
72 504080 : }
73 :
74 : void assert_byte_buf_equivalence(
75 : const struct aws_byte_buf *const lhs, const struct aws_byte_buf *const rhs,
76 618722 : const struct store_byte_from_buffer *const rhs_byte) {
77 618722 : /* In order to be equivalent, either both are NULL or both are non-NULL */
78 618722 : if (lhs == rhs) {
79 0 : return;
80 618722 : } else {
81 618722 : sassert(lhs && rhs); /* if only one is null, they differ */
82 618722 : }
83 618722 : sassert(lhs->len == rhs->len);
84 618722 : sassert(lhs->capacity == rhs->capacity);
85 618722 : sassert(lhs->allocator == rhs->allocator);
86 618722 : if (lhs->len > 0) {
87 153396 : assert_byte_from_buffer_matches(lhs->buffer, rhs_byte);
88 153396 : }
89 618722 : }
90 :
91 : void assert_byte_cursor_equivalence(
92 : const struct aws_byte_cursor *const lhs,
93 : const struct aws_byte_cursor *const rhs,
94 24375 : const struct store_byte_from_buffer *const rhs_byte) {
95 24375 : sassert(!lhs == !rhs);
96 24375 : if (lhs && rhs) {
97 24375 : sassert(lhs->len == rhs->len);
98 24375 : if (lhs->len > 0) {
99 9665 : assert_byte_from_buffer_matches(lhs->ptr, rhs_byte);
100 9665 : }
101 24375 : }
102 24375 : }
103 :
104 : bool uninterpreted_predicate_fn(uint8_t value);
105 :
106 0 : bool nondet_equals(const void *const a, const void *const b) {
107 0 : sassert(a != NULL);
108 0 : sassert(b != NULL);
109 0 : return a == b ? true : nd_bool();
110 0 : }
111 :
112 0 : uint64_t uninterpreted_hasher(const void *a) { return nd_uint64_t(); }
|