Line data Source code
1 : /*
2 : *
3 : */
4 :
5 : #pragma once
6 :
7 : #include <aws/common/array_list.h>
8 : #include <aws/common/byte_buf.h>
9 :
10 : #include <seahorn/seahorn.h>
11 :
12 : #include <nondet.h>
13 : #include <stddef.h>
14 : #include <stdint.h>
15 :
16 : extern void klee_assume(uintptr_t condition);
17 :
18 : #ifdef __KLEE__ // define macros for KLEE_ASSUME, the assumption for KLEE only
19 : #define KLEE_ASSUME(X) klee_assume(X)
20 : #elif __FUZZ__
21 2290170 : #define KLEE_ASSUME(X) assume(X)
22 : #else
23 : #define KLEE_ASSUME(X)
24 : #endif
25 :
26 : #ifdef __FUZZ__
27 : #define FUZZ_ASSUME(X) assume(X)
28 : #else
29 : #define FUZZ_ASSUME(X)
30 : #endif
31 :
32 : #ifdef __FUZZ__ // set upper bound of X to Y during fuzzing
33 150000 : #define FUZZ_ASSUME_LT(X, Y) X %= Y
34 : #else
35 : #define FUZZ_ASSUME_LT(X, Y)
36 : #endif
37 :
38 : extern __declspec(noalias) void sea_printf(const char *format, ...);
39 :
40 : #define IMPLIES(a, b) (!(a) || (b))
41 :
42 : struct store_byte_from_buffer {
43 : size_t index;
44 : uint8_t byte;
45 : };
46 :
47 : /**
48 : * Asserts whether all bytes from two arrays of same length match.
49 : */
50 : void assert_bytes_match(const uint8_t *const a, const uint8_t *const b,
51 : const size_t len);
52 :
53 : /**
54 : * Asserts whether all bytes from an array are equal to c.
55 : */
56 : void assert_all_bytes_are(const uint8_t *const a, const uint8_t c,
57 : const size_t len);
58 :
59 : /**
60 : * Asserts whether all bytes from an array are equal to 0.
61 : */
62 : void assert_all_zeroes(const uint8_t *const a, const size_t len);
63 :
64 : /**
65 : * Asserts whether the byte in storage correspond to the byte in the same
66 : * position in buffer.
67 : */
68 : void assert_byte_from_buffer_matches(
69 : const uint8_t *const buffer, const struct store_byte_from_buffer *const b);
70 :
71 : /**
72 : * Nondeterministically selects a byte from array and stores it into a
73 : * store_array_list_byte structure. Afterwards, one can prove using the
74 : * assert_array_list_equivalence function whether no byte in the array has
75 : * changed.
76 : */
77 : void save_byte_from_array(const uint8_t *const array, const size_t size,
78 : struct store_byte_from_buffer *const storage);
79 :
80 : /**
81 : * Asserts two aws_array_list structures are equivalent. Prior to using this
82 : * function, it is necessary to select a non-deterministic byte from the rhs
83 : * aws_array_list structure (use save_byte_from_array function), so it can
84 : * properly assert all bytes match.
85 : */
86 : void assert_array_list_equivalence(
87 : const struct aws_array_list *const lhs,
88 : const struct aws_array_list *const rhs,
89 : const struct store_byte_from_buffer *const rhs_byte);
90 :
91 : void assert_byte_buf_equivalence(
92 : const struct aws_byte_buf *const lhs, const struct aws_byte_buf *const rhs,
93 : const struct store_byte_from_buffer *const rhs_byte);
94 :
95 : void assert_byte_cursor_equivalence(
96 : const struct aws_byte_cursor *const lhs,
97 : const struct aws_byte_cursor *const rhs,
98 : const struct store_byte_from_buffer *const rhs_byte);
99 :
100 : /**
101 : * Standard stub function to compare two items.
102 : */
103 : int nondet_compare(const void *const a, const void *const b);
104 :
105 : /**
106 : * Standard stub function to compare two items.
107 : */
108 : int uninterpreted_compare(const void *const a, const void *const b);
109 :
110 : /**
111 : * Standard stub function to compare two items.
112 : */
113 : bool nondet_equals(const void *const a, const void *const b);
114 :
115 : /**
116 : * Standard stub function to compare two items.
117 : * Also enforces uninterpreted_hasher() to be equal for equal values.
118 : */
119 : bool uninterpreted_equals(const void *const a, const void *const b);
120 :
121 : /**
122 : * uninterpreted_equals(), but with an extra assertion that a and b are both
123 : * not null
124 : */
125 : bool uninterpreted_equals_assert_inputs_nonnull(const void *const a,
126 : const void *const b);
127 :
128 : /**
129 : * Standard stub function to hash one item.
130 : */
131 : uint64_t nondet_hasher(const void *a);
132 :
133 : /**
134 : * Standard stub function to hash one item.
135 : */
136 : uint64_t uninterpreted_hasher(const void *a);
137 :
138 : /**
139 : * Standard stub function of a predicate
140 : */
141 : bool uninterpreted_predicate_fn(uint8_t value);
|
