begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/xQueueGenericSend.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 #include "proof/queuecontracts.h"
  25
  26 BaseType_t xQueueGenericSend( QueueHandle_t xQueue,
  27                               const void * const pvItemToQueue,
  28                               TickType_t xTicksToWait,
  29                               const BaseType_t xCopyPosition )
  30 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
  31     [1/2]queuesuspend(xQueue) &*&
  32     chars(pvItemToQueue, M, ?x) &*&
  33     (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/
  34 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  35     [1/2]queuesuspend(xQueue) &*&
  36     chars(pvItemToQueue, M, x);@*/
  37 {
  38     BaseType_t xEntryTimeSet = pdFALSE, xYieldRequired;
  39     TimeOut_t xTimeOut;
  40 #ifdef VERIFAST /*< const pointer declaration */
  41     Queue_t * pxQueue = xQueue;
  42 #else
  43     Queue_t * const pxQueue = xQueue;
  44
  45     configASSERT( pxQueue );
  46     configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) );
  47     configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) );
  48     #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) )
  49         {
  50             configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) );
  51         }
  52     #endif
  53 #endif
  54
  55     /*lint -save -e904 This function relaxes the coding standard somewhat to
  56      * allow return statements within the function itself.  This is done in the
  57      * interest of execution time efficiency. */
  58     for( ; ; )
  59     /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  60         [1/2]queuesuspend(xQueue) &*&
  61         chars(pvItemToQueue, M, x) &*&
  62         u_integer(&xTicksToWait, _) &*&
  63         (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1)) &*&
  64         xTIME_OUT(&xTimeOut);@*/
  65     {
  66         taskENTER_CRITICAL();
  67         {
  68             /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/
  69             /* Is there room on the queue now?  The running task must be the
  70              * highest priority task wanting to access the queue.  If the head item
  71              * in the queue is to be overwritten then it does not matter if the
  72              * queue is full. */
  73             if( ( pxQueue->uxMessagesWaiting < pxQueue->uxLength ) || ( xCopyPosition == queueOVERWRITE ) )
  74             {
  75                 traceQUEUE_SEND( pxQueue );
  76
  77                 /* VeriFast: we do not verify this configuration option */
  78                 #if ( configUSE_QUEUE_SETS == 1 )
  79                     {
  80                         const UBaseType_t uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting;
  81
  82                         xYieldRequired = prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition );
  83
  84                         if( pxQueue->pxQueueSetContainer != NULL )
  85                         {
  86                             if( ( xCopyPosition == queueOVERWRITE ) && ( uxPreviousMessagesWaiting != ( UBaseType_t ) 0 ) )
  87                             {
  88                                 /* Do not notify the queue set as an existing item
  89                                  * was overwritten in the queue so the number of items
  90                                  * in the queue has not changed. */
  91                                 mtCOVERAGE_TEST_MARKER();
  92                             }
  93                             else if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE )
  94                             {
  95                                 /* The queue is a member of a queue set, and posting
  96                                  * to the queue set caused a higher priority task to
  97                                  * unblock. A context switch is required. */
  98                                 queueYIELD_IF_USING_PREEMPTION();
  99                             }
 100                             else
 101                             {
 102                                 mtCOVERAGE_TEST_MARKER();
 103                             }
 104                         }
 105                         else
 106                         {
 107                             /* If there was a task waiting for data to arrive on the
 108                              * queue then unblock it now. */
 109                             if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
 110                             {
 111                                 if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
 112                                 {
 113                                     /* The unblocked task has a priority higher than
 114                                      * our own so yield immediately.  Yes it is ok to
 115                                      * do this from within the critical section - the
 116                                      * kernel takes care of that. */
 117                                     queueYIELD_IF_USING_PREEMPTION();
 118                                 }
 119                                 else
 120                                 {
 121                                     mtCOVERAGE_TEST_MARKER();
 122                                 }
 123                             }
 124                             else if( xYieldRequired != pdFALSE )
 125                             {
 126                                 /* This path is a special case that will only get
 127                                  * executed if the task was holding multiple mutexes
 128                                  * and the mutexes were given back in an order that is
 129                                  * different to that in which they were taken. */
 130                                 queueYIELD_IF_USING_PREEMPTION();
 131                             }
 132                             else
 133                             {
 134                                 mtCOVERAGE_TEST_MARKER();
 135                             }
 136                         }
 137                     }
 138                 #else /* configUSE_QUEUE_SETS */
 139                     {
 140                         /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 141                         xYieldRequired = prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition );
 142
 143                         /* If there was a task waiting for data to arrive on the
 144                          * queue then unblock it now. */
 145                         if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
 146                         {
 147                             if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
 148                             {
 149                                 /* The unblocked task has a priority higher than
 150                                  * our own so yield immediately.  Yes it is ok to do
 151                                  * this from within the critical section - the kernel
 152                                  * takes care of that. */
 153                                 queueYIELD_IF_USING_PREEMPTION();
 154                             }
 155                             else
 156                             {
 157                                 mtCOVERAGE_TEST_MARKER();
 158                             }
 159                         }
 160                         else if( xYieldRequired != pdFALSE )
 161                         {
 162                             /* This path is a special case that will only get
 163                              * executed if the task was holding multiple mutexes and
 164                              * the mutexes were given back in an order that is
 165                              * different to that in which they were taken. */
 166                             queueYIELD_IF_USING_PREEMPTION();
 167                         }
 168                         else
 169                         {
 170                             mtCOVERAGE_TEST_MARKER();
 171                         }
 172                     }
 173                 #endif /* configUSE_QUEUE_SETS */
 174
 175                 /*@
 176                 if (xCopyPosition == queueSEND_TO_BACK)
 177                 {
 178                     close queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x)));
 179                 }
 180                 else if (xCopyPosition == queueSEND_TO_FRONT)
 181                 {
 182                     close queue(pxQueue, Storage, N, M, W, (R == 0 ? (N-1) : (R-1)), (K+1), is_locked, cons(x, abs));
 183                 }
 184                 else if (xCopyPosition == queueOVERWRITE)
 185                 {
 186                     close queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x));
 187                 }
 188                 @*/
 189                 taskEXIT_CRITICAL();
 190                 return pdPASS;
 191             }
 192             else
 193             {
 194                 if( xTicksToWait == ( TickType_t ) 0 )
 195                 {
 196                     /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 197                     /* The queue was full and no block time is specified (or
 198                      * the block time has expired) so leave now. */
 199                     taskEXIT_CRITICAL();
 200
 201                     /* Return to the original privilege level before exiting
 202                      * the function. */
 203                     traceQUEUE_SEND_FAILED( pxQueue );
 204                     return errQUEUE_FULL;
 205                 }
 206                 else if( xEntryTimeSet == pdFALSE )
 207                 {
 208                     /* The queue was full and a block time was specified so
 209                      * configure the timeout structure. */
 210                     vTaskInternalSetTimeOutState( &xTimeOut );
 211                     xEntryTimeSet = pdTRUE;
 212                 }
 213                 else
 214                 {
 215                     /* Entry time was already set. */
 216                     mtCOVERAGE_TEST_MARKER();
 217                 }
 218             }
 219             /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 220         }
 221         taskEXIT_CRITICAL();
 222
 223         /* Interrupts and other tasks can send to and receive from the queue
 224          * now the critical section has been exited. */
 225
 226         /*@close exists(pxQueue);@*/
 227         vTaskSuspendAll();
 228         prvLockQueue( pxQueue );
 229
 230         /* Update the timeout state to see if it has expired yet. */
 231         if( xTaskCheckForTimeOut( &xTimeOut, &xTicksToWait ) == pdFALSE )
 232         {
 233             if( prvIsQueueFull( pxQueue ) != pdFALSE )
 234             {
 235                 traceBLOCKING_ON_QUEUE_SEND( pxQueue );
 236                 /*@open queue_locked_invariant(xQueue)();@*/
 237                 vTaskPlaceOnEventList( &( pxQueue->xTasksWaitingToSend ), xTicksToWait );
 238
 239                 /* Unlocking the queue means queue events can effect the
 240                  * event list.  It is possible that interrupts occurring now
 241                  * remove this task from the event list again - but as the
 242                  * scheduler is suspended the task will go onto the pending
 243                  * ready last instead of the actual ready list. */
 244                 /*@close queue_locked_invariant(xQueue)();@*/
 245                 prvUnlockQueue( pxQueue );
 246
 247                 /* Resuming the scheduler will move tasks from the pending
 248                  * ready list into the ready list - so it is feasible that this
 249                  * task is already in a ready list before it yields - in which
 250                  * case the yield will not cause a context switch unless there
 251                  * is also a higher priority task in the pending ready list. */
 252                 /*@close exists(pxQueue);@*/
 253                 if( xTaskResumeAll() == pdFALSE )
 254                 {
 255                     portYIELD_WITHIN_API();
 256                 }
 257             }
 258             else
 259             {
 260                 /* Try again. */
 261                 prvUnlockQueue( pxQueue );
 262 #ifdef VERIFAST /*< void cast of unused return value */
 263                 /*@close exists(pxQueue);@*/
 264                 xTaskResumeAll();
 265 #else
 266                 ( void ) xTaskResumeAll();
 267 #endif
 268             }
 269         }
 270         else
 271         {
 272             /* The timeout has expired. */
 273             prvUnlockQueue( pxQueue );
 274 #ifdef VERIFAST /*< void cast of unused return value */
 275             /*@close exists(pxQueue);@*/
 276             xTaskResumeAll();
 277 #else
 278             ( void ) xTaskResumeAll();
 279 #endif
 280
 281             traceQUEUE_SEND_FAILED( pxQueue );
 282             return errQUEUE_FULL;
 283         }
 284     } /*lint -restore */
 285 }