1 /**
2  * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3  * SPDX-License-Identifier: Apache-2.0.
4  */
5 
6 #include <aws/common/byte_buf.h>
7 #include <aws/common/ring_buffer.h>
8 #include <proof_helpers/make_common_data_structures.h>
9 #include <proof_helpers/ring_buffer_abstract_states.h>
10 
aws_ring_buffer_release_harness()11 void aws_ring_buffer_release_harness() {
12     /* parameters */
13     struct aws_byte_buf buf;
14     struct aws_ring_buffer ring_buf;
15 
16     size_t ring_buf_size;
17 
18     /* assumptions */
19     ensure_ring_buffer_has_allocated_members(&ring_buf, ring_buf_size);
20     __CPROVER_assume(!aws_ring_buffer_is_empty(&ring_buf));
21     __CPROVER_assume(aws_ring_buffer_is_valid(&ring_buf));
22     ensure_byte_buf_has_allocated_buffer_member_in_ring_buf(&buf, &ring_buf);
23     __CPROVER_assume(aws_byte_buf_is_valid(&buf));
24 
25     /* copy of state before call */
26     struct aws_ring_buffer ring_buf_old = ring_buf;
27     struct aws_byte_buf buf_old = buf;
28 
29     aws_ring_buffer_release(&ring_buf, &buf);
30 
31     /* assertions */
32     uint8_t *old_head = aws_atomic_load_ptr(&ring_buf_old.head);
33     uint8_t *old_tail = aws_atomic_load_ptr(&ring_buf_old.tail);
34     uint8_t *new_head = aws_atomic_load_ptr(&ring_buf.head);
35     uint8_t *new_tail = aws_atomic_load_ptr(&ring_buf.tail);
36     assert(aws_ring_buffer_is_valid(&ring_buf));
37     assert(ring_buf.allocator == ring_buf_old.allocator);
38     assert(ring_buf.allocation == ring_buf_old.allocation);
39     assert(new_head == old_head);
40     assert(new_tail == buf_old.buffer + buf_old.capacity);
41     assert(ring_buf.allocation_end == ring_buf_old.allocation_end);
42     assert(buf.allocator == NULL);
43     assert(buf.buffer == NULL);
44     assert(buf.len == 0);
45     assert(buf.capacity == 0);
46     assert(IMPLIES(is_front_valid_state(&ring_buf_old), is_empty_state(&ring_buf) || is_middle_valid_state(&ring_buf)));
47     assert(IMPLIES(
48         is_middle_valid_state(&ring_buf_old),
49         is_empty_state(&ring_buf) || is_middle_valid_state(&ring_buf) || is_ends_valid_state(&ring_buf)));
50     assert(IMPLIES(
51         is_ends_valid_state(&ring_buf_old),
52         is_empty_state(&ring_buf) || is_middle_valid_state(&ring_buf) || is_ends_valid_state(&ring_buf)));
53 }
54