diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/create.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/create.c | 267 |
1 files changed, 267 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/create.c b/FreeRTOS/Test/VeriFast/queue/create.c new file mode 100644 index 000000000..4a7902d3b --- /dev/null +++ b/FreeRTOS/Test/VeriFast/queue/create.c @@ -0,0 +1,267 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +#include "proof/queue.h" + +/* Simplifying assumption: we do not verify queue initialisation in a + * concurrent environment. We assume the queue initialization (including reset) + * happens-before all concurrent send/receives. */ +#ifdef VERIFAST /*< ***xQueueGenericReset happens-before concurrent behavior*** */ + #define taskENTER_CRITICAL() + #define taskEXIT_CRITICAL() +#endif + +/* The following intermediate queue predicates summarise states used by queue + * initialization but not used elsewhere so we confine them to these proofs + * locally. */ +/*@ +predicate queue_init1(QueueHandle_t q;) = + QUEUE_SHAPE(q, _, _, _, _) &*& + queuelists(q) + ; + +predicate queue_init2(QueueHandle_t q, int8_t *Storage, size_t N, size_t M;) = + QUEUE_SHAPE(q, Storage, N, M, _) &*& + queuelists(q) &*& + 0 < N &*& + chars(Storage, (N*M), _) &*& + malloc_block(Storage, N*M) &*& + Storage + N * M <= (int8_t *)UINTPTR_MAX &*& + true + ; +@*/ + +BaseType_t xQueueGenericReset( QueueHandle_t xQueue, + BaseType_t xNewQueue ) +/*@requires queue_init2(xQueue, ?Storage, ?N, ?M);@*/ +/*@ensures 0 == M + ? freertos_mutex(xQueue, Storage, N, 0) + : queue(xQueue, Storage, N, M, 0, (N-1), 0, false, nil) &*& queuelists(xQueue);@*/ +{ +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif + + configASSERT( pxQueue ); + + taskENTER_CRITICAL(); + { + pxQueue->u.xQueue.pcTail = pxQueue->pcHead + ( pxQueue->uxLength * pxQueue->uxItemSize ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ + pxQueue->uxMessagesWaiting = ( UBaseType_t ) 0U; + pxQueue->pcWriteTo = pxQueue->pcHead; + /*@mul_mono_l(0, N-1, M);@*/ + pxQueue->u.xQueue.pcReadFrom = pxQueue->pcHead + ( ( pxQueue->uxLength - 1U ) * pxQueue->uxItemSize ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ + pxQueue->cRxLock = queueUNLOCKED; + pxQueue->cTxLock = queueUNLOCKED; + + if( xNewQueue == pdFALSE ) + { + /* If there are tasks blocked waiting to read from the queue, then + * the tasks will remain blocked as after this function exits the queue + * will still be empty. If there are tasks blocked waiting to write to + * the queue, then one should be unblocked as after this function exits + * it will be possible to write to it. */ + if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE ) + { + if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE ) + { + queueYIELD_IF_USING_PREEMPTION(); + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + } + else + { + /* Ensure the event queues start in the correct state. */ + vListInitialise( &( pxQueue->xTasksWaitingToSend ) ); + vListInitialise( &( pxQueue->xTasksWaitingToReceive ) ); + } + + /*@if (M != 0) { buffer_from_chars(pxQueue->pcHead, N, M); }@*/ + } + taskEXIT_CRITICAL(); + + /* A value is returned for calling semantic consistency with previous + * versions. */ + return pdPASS; +} + +static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, + const UBaseType_t uxItemSize, + uint8_t * pucQueueStorage, + const uint8_t ucQueueType, + Queue_t * pxNewQueue ) + +/*@requires queue_init1(pxNewQueue) &*& + 0 < uxQueueLength &*& 0 < uxItemSize &*& + malloc_block(pucQueueStorage, uxQueueLength * uxItemSize) &*& + pucQueueStorage + uxQueueLength * uxItemSize <= (uint8_t *)UINTPTR_MAX &*& + uchars(pucQueueStorage, uxQueueLength * uxItemSize,_);@*/ +/*@ensures queue(pxNewQueue, ((int8_t *)(void *)pucQueueStorage), uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& + queuelists(pxNewQueue);@*/ +{ +#ifndef VERIFAST /*< void cast of unused var */ + /* Remove compiler warnings about unused parameters should + * configUSE_TRACE_FACILITY not be set to 1. */ + ( void ) ucQueueType; +#endif + + if( uxItemSize == ( UBaseType_t ) 0 ) + { + /* No RAM was allocated for the queue storage area, but PC head cannot + * be set to NULL because NULL is used as a key to say the queue is used as + * a mutex. Therefore just set pcHead to point to the queue as a benign + * value that is known to be within the memory map. */ +#ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pxNewQueue; +#else + pxNewQueue->pcHead = ( int8_t * ) pxNewQueue; +#endif + } + else + { + /* Set the head to the start of the queue storage area. */ +#ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pucQueueStorage; +#else + pxNewQueue->pcHead = ( int8_t * ) pucQueueStorage; +#endif + } + + /* Initialise the queue members as described where the queue type is + * defined. */ + pxNewQueue->uxLength = uxQueueLength; + pxNewQueue->uxItemSize = uxItemSize; + /*@close queue_init2(pxNewQueue, _, uxQueueLength, uxItemSize);@*/ +#ifdef VERIFAST /*< void cast of unused return value */ + xQueueGenericReset( pxNewQueue, pdTRUE ); +#else + ( void ) xQueueGenericReset( pxNewQueue, pdTRUE ); +#endif + + #if ( configUSE_TRACE_FACILITY == 1 ) + { + pxNewQueue->ucQueueType = ucQueueType; + } + #endif /* configUSE_TRACE_FACILITY */ + + #if ( configUSE_QUEUE_SETS == 1 ) + { + pxNewQueue->pxQueueSetContainer = NULL; + } + #endif /* configUSE_QUEUE_SETS */ + + traceQUEUE_CREATE( pxNewQueue ); +} + + + QueueHandle_t xQueueGenericCreate( const UBaseType_t uxQueueLength, + const UBaseType_t uxItemSize, + const uint8_t ucQueueType ) + /*@requires 0 < uxQueueLength &*& + 0 < uxItemSize &*& + 0 < uxQueueLength * uxItemSize &*& + uxQueueLength * uxItemSize <= UINT_MAX;@*/ + /*@ensures result == NULL + ? true + : queue(result, _, uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& + queuelists(result) &*& + result->irqMask |-> _ &*& + result->schedulerSuspend |-> _ &*& + result->locked |-> _;@*/ + { + Queue_t * pxNewQueue; + size_t xQueueSizeInBytes; + uint8_t * pucQueueStorage; + + configASSERT( uxQueueLength > ( UBaseType_t ) 0 ); + + /* Allocate enough space to hold the maximum number of items that + * can be in the queue at any time. It is valid for uxItemSize to be + * zero in the case the queue is used as a semaphore. */ + xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ + + /* Check for multiplication overflow. */ + configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); + +#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) ); +#else + /* Allocate the queue and storage area. Justification for MISRA + * deviation as follows: pvPortMalloc() always ensures returned memory + * blocks are aligned per the requirements of the MCU stack. In this case + * pvPortMalloc() must return a pointer that is guaranteed to meet the + * alignment requirements of the Queue_t structure - which in this case + * is an int8_t *. Therefore, whenever the stack alignment requirements + * are greater than or equal to the pointer to char requirements the cast + * is safe. In other cases alignment requirements are not strict (one or + * two bytes). */ + pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) + xQueueSizeInBytes ); /*lint !e9087 !e9079 see comment above. */ +#endif + + if( pxNewQueue != NULL ) + { +#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + pucQueueStorage = ( uint8_t * ) pvPortMalloc( xQueueSizeInBytes ); + + if( pucQueueStorage == NULL ) + { + vPortFree( pxNewQueue ); + return NULL; + } + + /*@malloc_block_limits(pucQueueStorage);@*/ +#else + /* Jump past the queue structure to find the location of the queue + * storage area. */ + pucQueueStorage = ( uint8_t * ) pxNewQueue; + pucQueueStorage += sizeof( Queue_t ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ +#endif + + #if ( configSUPPORT_STATIC_ALLOCATION == 1 ) + { + /* Queues can be created either statically or dynamically, so + * note this task was created dynamically in case it is later + * deleted. */ + pxNewQueue->ucStaticallyAllocated = pdFALSE; + } + #endif /* configSUPPORT_STATIC_ALLOCATION */ + + prvInitialiseNewQueue( uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue ); + } + else + { + traceQUEUE_CREATE_FAILED( ucQueueType ); + mtCOVERAGE_TEST_MARKER(); + } + + return pxNewQueue; + } |