begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/xQueueReceiveFromISR.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 #include "proof/queuecontracts.h"
  29
  30 BaseType_t xQueueReceiveFromISR( QueueHandle_t xQueue,
  31                                  void * const pvBuffer,
  32                                  BaseType_t * const pxHigherPriorityTaskWoken )
  33
  34 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true &*&
  35  *  chars(pvBuffer, M, ?x) &*&
  36  *  pxHigherPriorityTaskWoken == NULL ? true : integer(pxHigherPriorityTaskWoken, _);@*/
  37
  38 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  39  *  (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x)) &*&
  40  *  (pxHigherPriorityTaskWoken == NULL ? true : integer(pxHigherPriorityTaskWoken, _));@*/
  41 {
  42     BaseType_t xReturn;
  43     UBaseType_t uxSavedInterruptStatus;
  44
  45     #ifdef VERIFAST /*< const pointer declaration */
  46         Queue_t * pxQueue = xQueue;
  47     #else
  48         Queue_t * const pxQueue = xQueue;
  49
  50         configASSERT( pxQueue );
  51         configASSERT( !( ( pvBuffer == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) );
  52     #endif
  53
  54     /* RTOS ports that support interrupt nesting have the concept of a maximum
  55      * system call (or maximum API call) interrupt priority.  Interrupts that are
  56      * above the maximum system call priority are kept permanently enabled, even
  57      * when the RTOS kernel is in a critical section, but cannot make any calls to
  58      * FreeRTOS API functions.  If configASSERT() is defined in FreeRTOSConfig.h
  59      * then portASSERT_IF_INTERRUPT_PRIORITY_INVALID() will result in an assertion
  60      * failure if a FreeRTOS API function is called from an interrupt that has been
  61      * assigned a priority above the configured maximum system call priority.
  62      * Only FreeRTOS functions that end in FromISR can be called from interrupts
  63      * that have been assigned a priority at or (logically) below the maximum
  64      * system call interrupt priority.  FreeRTOS maintains a separate interrupt
  65      * safe API to ensure interrupt entry is as fast and as simple as possible.
  66      * More information (albeit Cortex-M specific) is provided on the following
  67      * link: https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html */
  68     portASSERT_IF_INTERRUPT_PRIORITY_INVALID();
  69
  70     uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR();
  71     /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/
  72     {
  73         const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  74
  75         /* Cannot block in an ISR, so check there is data available. */
  76         if( uxMessagesWaiting > ( UBaseType_t ) 0 )
  77         {
  78             const int8_t cRxLock = pxQueue->cRxLock;
  79
  80             traceQUEUE_RECEIVE_FROM_ISR( pxQueue );
  81
  82             /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  83             prvCopyDataFromQueue( pxQueue, pvBuffer );
  84             /*@open queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs);@*/
  85             pxQueue->uxMessagesWaiting = uxMessagesWaiting - ( UBaseType_t ) 1;
  86             /*@assert buffer(Storage, N, M, ?contents);@*/
  87             /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/
  88
  89             /* If the queue is locked the event list will not be modified.
  90              * Instead update the lock count so the task that unlocks the queue
  91              * will know that an ISR has removed data while the queue was
  92              * locked. */
  93             if( cRxLock == queueUNLOCKED )
  94             {
  95                 if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE )
  96                 {
  97                     if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE )
  98                     {
  99                         /* The task waiting has a higher priority than us so
 100                          * force a context switch. */
 101                         if( pxHigherPriorityTaskWoken != NULL )
 102                         {
 103                             *pxHigherPriorityTaskWoken = pdTRUE;
 104                         }
 105                         else
 106                         {
 107                             mtCOVERAGE_TEST_MARKER();
 108                         }
 109                     }
 110                     else
 111                     {
 112                         mtCOVERAGE_TEST_MARKER();
 113                     }
 114                 }
 115                 else
 116                 {
 117                     mtCOVERAGE_TEST_MARKER();
 118                 }
 119             }
 120             else
 121             {
 122                 /* Increment the lock count so the task that unlocks the queue
 123                  * knows that data was removed while it was locked. */
 124                 configASSERT( cRxLock != queueINT8_MAX );
 125
 126                 pxQueue->cRxLock = ( int8_t ) ( cRxLock + 1 );
 127             }
 128
 129             /*@close queue(pxQueue, Storage, N, M, W, (R+1)%N, K-1, is_locked, tail(abs));@*/
 130             /*@assert chars(pvBuffer, M, head(abs));@*/
 131             xReturn = pdPASS;
 132         }
 133         else
 134         {
 135             /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 136             xReturn = pdFAIL;
 137             traceQUEUE_RECEIVE_FROM_ISR_FAILED( pxQueue );
 138         }
 139     }
 140     portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus );
 141
 142     return xReturn;
 143 }