begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/create.c

   1 /*
   2  * FreeRTOS V202104.00
   3  * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
   6  * this software and associated documentation files (the "Software"), to deal in
   7  * the Software without restriction, including without limitation the rights to
   8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
   9  * the Software, and to permit persons to whom the Software is furnished to do so,
  10  * subject to the following conditions:
  11  *
  12  * The above copyright notice and this permission notice shall be included in all
  13  * copies or substantial portions of the Software.
  14  *
  15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
  17  * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
  18  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  21  */
  22
  23 #include "proof/queue.h"
  24
  25 /* Simplifying assumption: we do not verify queue initialisation in a
  26  * concurrent environment. We assume the queue initialization (including reset)
  27  * happens-before all concurrent send/receives. */
  28 #ifdef VERIFAST /*< ***xQueueGenericReset happens-before concurrent behavior*** */
  29     #define taskENTER_CRITICAL()
  30     #define taskEXIT_CRITICAL()
  31 #endif
  32
  33 /* The following intermediate queue predicates summarise states used by queue
  34  * initialization but not used elsewhere so we confine them to these proofs
  35  * locally. */
  36 /*@
  37 predicate queue_init1(QueueHandle_t q;) =
  38     QUEUE_SHAPE(q, _, _, _, _) &*&
  39     queuelists(q)
  40     ;
  41
  42 predicate queue_init2(QueueHandle_t q, int8_t *Storage, size_t N, size_t M;) =
  43     QUEUE_SHAPE(q, Storage, N, M, _) &*&
  44     queuelists(q) &*&
  45     0 < N &*&
  46     chars(Storage, (N*M), _) &*&
  47     malloc_block(Storage, N*M) &*&
  48     Storage + N * M <= (int8_t *)UINTPTR_MAX &*&
  49     true
  50     ;
  51 @*/
  52
  53 BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
  54                                BaseType_t xNewQueue )
  55 /*@requires queue_init2(xQueue, ?Storage, ?N, ?M);@*/
  56 /*@ensures 0 == M
  57     ? freertos_mutex(xQueue, Storage, N, 0)
  58     : queue(xQueue, Storage, N, M, 0, (N-1), 0, false, nil) &*& queuelists(xQueue);@*/
  59 {
  60 #ifdef VERIFAST /*< const pointer declaration */
  61     Queue_t * pxQueue = xQueue;
  62 #else
  63     Queue_t * const pxQueue = xQueue;
  64 #endif
  65
  66     configASSERT( pxQueue );
  67
  68     taskENTER_CRITICAL();
  69     {
  70         pxQueue->u.xQueue.pcTail = pxQueue->pcHead + ( pxQueue->uxLength * pxQueue->uxItemSize ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */
  71         pxQueue->uxMessagesWaiting = ( UBaseType_t ) 0U;
  72         pxQueue->pcWriteTo = pxQueue->pcHead;
  73         /*@mul_mono_l(0, N-1, M);@*/
  74         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. */
  75         pxQueue->cRxLock = queueUNLOCKED;
  76         pxQueue->cTxLock = queueUNLOCKED;
  77
  78         if( xNewQueue == pdFALSE )
  79         {
  80             /* If there are tasks blocked waiting to read from the queue, then
  81              * the tasks will remain blocked as after this function exits the queue
  82              * will still be empty.  If there are tasks blocked waiting to write to
  83              * the queue, then one should be unblocked as after this function exits
  84              * it will be possible to write to it. */
  85             if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE )
  86             {
  87                 if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE )
  88                 {
  89                     queueYIELD_IF_USING_PREEMPTION();
  90                 }
  91                 else
  92                 {
  93                     mtCOVERAGE_TEST_MARKER();
  94                 }
  95             }
  96             else
  97             {
  98                 mtCOVERAGE_TEST_MARKER();
  99             }
 100         }
 101         else
 102         {
 103             /* Ensure the event queues start in the correct state. */
 104             vListInitialise( &( pxQueue->xTasksWaitingToSend ) );
 105             vListInitialise( &( pxQueue->xTasksWaitingToReceive ) );
 106         }
 107
 108         /*@if (M != 0) { buffer_from_chars(pxQueue->pcHead, N, M); }@*/
 109     }
 110     taskEXIT_CRITICAL();
 111
 112     /* A value is returned for calling semantic consistency with previous
 113      * versions. */
 114     return pdPASS;
 115 }
 116
 117 static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength,
 118                                    const UBaseType_t uxItemSize,
 119                                    uint8_t * pucQueueStorage,
 120                                    const uint8_t ucQueueType,
 121                                    Queue_t * pxNewQueue )
 122
 123 /*@requires queue_init1(pxNewQueue) &*&
 124     0 < uxQueueLength &*& 0 < uxItemSize &*&
 125     malloc_block(pucQueueStorage, uxQueueLength * uxItemSize) &*&
 126     pucQueueStorage + uxQueueLength * uxItemSize <= (uint8_t *)UINTPTR_MAX &*&
 127     uchars(pucQueueStorage, uxQueueLength * uxItemSize,_);@*/
 128 /*@ensures queue(pxNewQueue, ((int8_t *)(void *)pucQueueStorage), uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*&
 129     queuelists(pxNewQueue);@*/
 130 {
 131 #ifndef VERIFAST /*< void cast of unused var */
 132     /* Remove compiler warnings about unused parameters should
 133      * configUSE_TRACE_FACILITY not be set to 1. */
 134     ( void ) ucQueueType;
 135 #endif
 136
 137     if( uxItemSize == ( UBaseType_t ) 0 )
 138     {
 139         /* No RAM was allocated for the queue storage area, but PC head cannot
 140          * be set to NULL because NULL is used as a key to say the queue is used as
 141          * a mutex.  Therefore just set pcHead to point to the queue as a benign
 142          * value that is known to be within the memory map. */
 143 #ifdef VERIFAST /*< stricter casting */
 144         pxNewQueue->pcHead = ( int8_t * ) ( void * ) pxNewQueue;
 145 #else
 146         pxNewQueue->pcHead = ( int8_t * ) pxNewQueue;
 147 #endif
 148     }
 149     else
 150     {
 151         /* Set the head to the start of the queue storage area. */
 152 #ifdef VERIFAST /*< stricter casting */
 153         pxNewQueue->pcHead = ( int8_t * ) ( void * ) pucQueueStorage;
 154 #else
 155         pxNewQueue->pcHead = ( int8_t * ) pucQueueStorage;
 156 #endif
 157     }
 158
 159     /* Initialise the queue members as described where the queue type is
 160      * defined. */
 161     pxNewQueue->uxLength = uxQueueLength;
 162     pxNewQueue->uxItemSize = uxItemSize;
 163     /*@close queue_init2(pxNewQueue, _, uxQueueLength, uxItemSize);@*/
 164 #ifdef VERIFAST /*< void cast of unused return value */
 165     xQueueGenericReset( pxNewQueue, pdTRUE );
 166 #else
 167     ( void ) xQueueGenericReset( pxNewQueue, pdTRUE );
 168 #endif
 169
 170     #if ( configUSE_TRACE_FACILITY == 1 )
 171         {
 172             pxNewQueue->ucQueueType = ucQueueType;
 173         }
 174     #endif /* configUSE_TRACE_FACILITY */
 175
 176     #if ( configUSE_QUEUE_SETS == 1 )
 177         {
 178             pxNewQueue->pxQueueSetContainer = NULL;
 179         }
 180     #endif /* configUSE_QUEUE_SETS */
 181
 182     traceQUEUE_CREATE( pxNewQueue );
 183 }
 184
 185
 186     QueueHandle_t xQueueGenericCreate( const UBaseType_t uxQueueLength,
 187                                        const UBaseType_t uxItemSize,
 188                                        const uint8_t ucQueueType )
 189     /*@requires 0 < uxQueueLength &*&
 190         0 < uxItemSize &*&
 191         0 < uxQueueLength * uxItemSize &*&
 192         uxQueueLength * uxItemSize <= UINT_MAX;@*/
 193     /*@ensures result == NULL
 194         ? true
 195         : queue(result, _, uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*&
 196             queuelists(result) &*&
 197             result->irqMask |-> _ &*&
 198             result->schedulerSuspend |-> _ &*&
 199             result->locked |-> _;@*/
 200     {
 201         Queue_t * pxNewQueue;
 202         size_t xQueueSizeInBytes;
 203         uint8_t * pucQueueStorage;
 204
 205         configASSERT( uxQueueLength > ( UBaseType_t ) 0 );
 206
 207         /* Allocate enough space to hold the maximum number of items that
 208          * can be in the queue at any time.  It is valid for uxItemSize to be
 209          * zero in the case the queue is used as a semaphore. */
 210         xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */
 211
 212         /* Check for multiplication overflow. */
 213         configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
 214
 215 #ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */
 216         pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) );
 217 #else
 218         /* Allocate the queue and storage area.  Justification for MISRA
 219          * deviation as follows:  pvPortMalloc() always ensures returned memory
 220          * blocks are aligned per the requirements of the MCU stack.  In this case
 221          * pvPortMalloc() must return a pointer that is guaranteed to meet the
 222          * alignment requirements of the Queue_t structure - which in this case
 223          * is an int8_t *.  Therefore, whenever the stack alignment requirements
 224          * are greater than or equal to the pointer to char requirements the cast
 225          * is safe.  In other cases alignment requirements are not strict (one or
 226          * two bytes). */
 227         pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) + xQueueSizeInBytes ); /*lint !e9087 !e9079 see comment above. */
 228 #endif
 229
 230         if( pxNewQueue != NULL )
 231         {
 232 #ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */
 233             pucQueueStorage = ( uint8_t * ) pvPortMalloc( xQueueSizeInBytes );
 234
 235             if( pucQueueStorage == NULL )
 236             {
 237                 vPortFree( pxNewQueue );
 238                 return NULL;
 239             }
 240
 241             /*@malloc_block_limits(pucQueueStorage);@*/
 242 #else
 243             /* Jump past the queue structure to find the location of the queue
 244              * storage area. */
 245             pucQueueStorage = ( uint8_t * ) pxNewQueue;
 246             pucQueueStorage += sizeof( Queue_t ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */
 247 #endif
 248
 249             #if ( configSUPPORT_STATIC_ALLOCATION == 1 )
 250                 {
 251                     /* Queues can be created either statically or dynamically, so
 252                      * note this task was created dynamically in case it is later
 253                      * deleted. */
 254                     pxNewQueue->ucStaticallyAllocated = pdFALSE;
 255                 }
 256             #endif /* configSUPPORT_STATIC_ALLOCATION */
 257
 258             prvInitialiseNewQueue( uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue );
 259         }
 260         else
 261         {
 262             traceQUEUE_CREATE_FAILED( ucQueueType );
 263             mtCOVERAGE_TEST_MARKER();
 264         }
 265
 266         return pxNewQueue;
 267     }