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

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