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()11void 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