diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/include/proof/queue.h')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/include/proof/queue.h | 550 |
1 files changed, 550 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/include/proof/queue.h b/FreeRTOS/Test/VeriFast/include/proof/queue.h new file mode 100644 index 000000000..610bc03d9 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/queue.h @@ -0,0 +1,550 @@ +/* + * 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. + */ + +#ifndef QUEUE_H +#define QUEUE_H + +#define VERIFAST +#include <stdlib.h> +#include <stdint.h> +#include <string.h> +#include <threading.h> +/*@#include "common.gh"@*/ + +typedef size_t TickType_t; +typedef size_t UBaseType_t; +typedef ssize_t BaseType_t; + +/* Empty/no-op macros */ +/* Tracing */ +#define traceBLOCKING_ON_QUEUE_PEEK(x) +#define traceBLOCKING_ON_QUEUE_RECEIVE(x) +#define traceBLOCKING_ON_QUEUE_SEND(x) +#define traceQUEUE_CREATE(x) +#define traceQUEUE_CREATE_FAILED(x) +#define traceQUEUE_DELETE(x) +#define traceQUEUE_PEEK(x) +#define traceQUEUE_PEEK_FAILED(x) +#define traceQUEUE_PEEK_FROM_ISR(x) +#define traceQUEUE_PEEK_FROM_ISR_FAILED(x) +#define traceQUEUE_RECEIVE(x) +#define traceQUEUE_RECEIVE_FAILED(x) +#define traceQUEUE_RECEIVE_FROM_ISR(x) +#define traceQUEUE_RECEIVE_FROM_ISR_FAILED(x) +#define traceQUEUE_SEND(x) +#define traceQUEUE_SEND_FAILED(x) +#define traceQUEUE_SEND_FROM_ISR(x) +#define traceQUEUE_SEND_FROM_ISR_FAILED(x) +/* Coverage */ +#define mtCOVERAGE_TEST_MARKER() +/* Asserts */ +#define configASSERT(x) +#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID() + +/* Map portable memory management functions */ +#define pvPortMalloc malloc +#define vPortFree free + +#define queueSEND_TO_BACK ( ( BaseType_t ) 0 ) +#define queueSEND_TO_FRONT ( ( BaseType_t ) 1 ) +#define queueOVERWRITE ( ( BaseType_t ) 2 ) + +#define pdTRUE 1 +#define pdFALSE 0 + +#define pdPASS pdTRUE +#define pdFAIL pdFALSE +#define errQUEUE_FULL 0 +#define errQUEUE_EMPTY 0 + +/* Constants used with the cRxLock and cTxLock structure members. */ +#define queueUNLOCKED ( ( int8_t ) -1 ) +#define queueLOCKED_UNMODIFIED ( ( int8_t ) 0 ) +#define queueINT8_MAX ( ( int8_t ) 127 ) + +typedef struct QueuePointers +{ + int8_t * pcTail; /*< Points to the byte at the end of the queue storage area. Once more byte is allocated than necessary to store the queue items, this is used as a marker. */ + int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */ +} QueuePointers_t; + +typedef struct SemaphoreData +{ +#ifdef VERIFAST /*< do not model xMutexHolder */ + void *xMutexHolder; +#else + TaskHandle_t xMutexHolder; /*< The handle of the task that holds the mutex. */ +#endif + UBaseType_t uxRecursiveCallCount; /*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */ +} SemaphoreData_t; + +/* VeriFast does not support unions so we replace with a struct */ +struct fake_union_t { + QueuePointers_t xQueue; + SemaphoreData_t xSemaphore; +}; + +typedef struct xLIST { + UBaseType_t uxNumberOfItems; +#ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */ + struct xLIST_ITEM *pxIndex; + MiniListItem_t xListEnd; +#endif +} List_t; + +typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */ +{ + int8_t * pcHead; /*< Points to the beginning of the queue storage area. */ + int8_t * pcWriteTo; /*< Points to the free next place in the storage area. */ + +#ifdef VERIFAST /*< VeriFast does not model unions */ + struct fake_union_t u; +#else + union + { + QueuePointers_t xQueue; /*< Data required exclusively when this structure is used as a queue. */ + SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */ + } u; +#endif + + List_t xTasksWaitingToSend; /*< List of tasks that are blocked waiting to post onto this queue. Stored in priority order. */ + List_t xTasksWaitingToReceive; /*< List of tasks that are blocked waiting to read from this queue. Stored in priority order. */ + + volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */ + UBaseType_t uxLength; /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */ + UBaseType_t uxItemSize; /*< The size of each items that the queue will hold. */ + + volatile int8_t cRxLock; /*< Stores the number of items received from the queue (removed from the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + volatile int8_t cTxLock; /*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + + #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) ) + uint8_t ucStaticallyAllocated; /*< Set to pdTRUE if the memory used by the queue was statically allocated to ensure no attempt is made to free the memory. */ + #endif + + #if ( configUSE_QUEUE_SETS == 1 ) + struct QueueDefinition * pxQueueSetContainer; + #endif + + #if ( configUSE_TRACE_FACILITY == 1 ) + UBaseType_t uxQueueNumber; + uint8_t ucQueueType; + #endif + + /*@struct mutex *irqMask;@*/ /*< Ghost mutex simulates the effect of irq masking */ + /*@struct mutex *schedulerSuspend;@*/ /*< Ghost mutex simulates the effect of scheduler suspension */ + /*@struct mutex *locked;@*/ /*< Ghost mutex simulates the effect of queue locking */ +} xQUEUE; + +typedef xQUEUE Queue_t; + +typedef struct QueueDefinition * QueueHandle_t; + +/*@ +#define QUEUE_SHAPE(q, Storage, N, M, K) \ + malloc_block_QueueDefinition(q) &*& \ + q->pcHead |-> Storage &*& \ + q->pcWriteTo |-> ?WPtr &*& \ + q->u.xQueue.pcTail |-> ?End &*& \ + q->u.xQueue.pcReadFrom |-> ?RPtr &*& \ + q->uxItemSize |-> M &*& \ + q->uxLength |-> N &*& \ + q->uxMessagesWaiting |-> K &*& \ + q->cRxLock |-> ?rxLock &*& \ + q->cTxLock |-> ?txLock &*& \ + struct_QueuePointers_padding(&q->u.xQueue) &*& \ + struct_SemaphoreData_padding(&q->u.xSemaphore) &*& \ + struct_fake_union_t_padding(&q->u) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToSend) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \ + q->u.xSemaphore.xMutexHolder |-> _ &*& \ + q->u.xSemaphore.uxRecursiveCallCount |-> _ &*& \ + true + +predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + 1 + K) % N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left((R+1)%N, contents)) &*& + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* A buffer allows us to interpret a flat character array of `N*M` bytes as a +list of `N` elements where each element is `M` bytes */ +/*@ +predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) = + N == 0 + ? elements == nil + : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs); + +lemma void buffer_length(char *buffer, size_t N, size_t M) +requires buffer(buffer, N, M, ?elements); +ensures buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + open buffer(buffer, N, M, elements); + close buffer(buffer, N, M, elements); + } else { + open buffer(buffer, N, M, elements); + buffer_length(buffer+M, N-1, M); + } +} +@*/ + +/* +There is no need in the queue proofs to preserve a relationship between `cs` +and `elements` (i.e., `flatten(elements) == cs`) because we only move in one +direction from `cs` to `elements` during queue creation when the contents is +fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from +elements back to cs then this would require a stronger lemma. +*/ +/*@ +lemma void buffer_from_chars(char *buffer, size_t N, size_t M) +requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M; +ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + close exists(nil); + } else { + int i = 0; + while (i < N) + invariant 0 <= i &*& i <= N &*& + chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*& + buffer(buffer + (N-i)*M, i, M, ?ys); + decreases N-i; + { + mul_mono_l(0, N-i-1, M); + chars_split(buffer, (N-i-1)*M); + mul_mono_l(i, N, M); + mul_mono_l(N-i, N, M); + take_take((N-i-1)*M, (N-i)*M, cs); + i++; + } + close exists(ys); + buffer_length(buffer, N, M); + } +} + +lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M) +requires + buffer(buffer, N1, M, ?elements1) &*& + buffer(buffer + N1 * M, N2, M, ?elements2) &*& + 0 <= N1 &*& 0 <= N2; +ensures buffer(buffer, N1+N2, M, append(elements1, elements2)); +{ + if (N1 == 0) { + open buffer(buffer, 0, M, _); + } else if (N2 == 0) { + open buffer(buffer + N1 * M, 0, M, _); + } else { + open buffer(buffer, N1, M, elements1); + append_buffer(buffer + M, N1-1, N2, M); + close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2))); + } +} + +lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i) +requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N; +ensures + buffer(buffer, i, M, take(i, elements)) &*& + chars(buffer + i * M, M, nth(i, elements)) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements)); +{ + if (i == 0) { + // straightforward + } else { + buffer_length(buffer, N, M); + int j = 0; + while (j < i) + invariant 0 <= j &*& j <= i &*& + buffer(buffer, j, M, take(j, elements)) &*& + buffer(buffer + j * M, N-j, M, drop(j, elements)); + decreases i-j; + { + drop_drop(1, j, elements); + nth_drop2(elements, j); + open buffer(buffer + j * M, N-j, M, drop(j, elements)); + assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements); + close buffer(buffer + j * M, 1, M, singleton(x)); + append_buffer(buffer, j, 1, M); + take_plus_one(j, elements); + j++; + } + drop_drop(1, j, elements); + nth_drop2(elements, i); + open buffer(buffer + (i+1) * M, (N-1-i), M, _); + } +} + +lemma void join_element(char *buffer, size_t N, size_t M, size_t i) +requires + 0 <= i &*& i < N &*& + buffer(buffer, i, M, ?prefix) &*& + chars(buffer + i * M, M, ?element) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix); +ensures buffer(buffer, N, M, append(prefix, cons(element, suffix))); +{ + if (i == 0) { + open buffer(buffer, i, M, prefix); + assert prefix == nil; + close buffer(buffer, N, M, cons(element, suffix)); + } else { + close buffer(buffer + i * M, N-i, M, cons(element, suffix)); + append_buffer(buffer, i, N-i, M); + } +} + +predicate list(List_t *l;) = + l->uxNumberOfItems |-> _; + +predicate queuelists(QueueHandle_t q;) = + list(&q->xTasksWaitingToSend) &*& + list(&q->xTasksWaitingToReceive); +@*/ + +/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the +queue predicate above does not hold as a postcondition. If the caller +subsequently decrements K then the queue predicate can be reinstated. */ +/*@ +predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + K) % N &*& //< Differs from queue predicate + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* Can't be called `mutex` as this clashes with VeriFast's predicate */ +/*@ +predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) = + QUEUE_SHAPE(q, Storage, N, 0, K) &*& + queuelists(q) &*& + 0 < N &*& + 0 <= K &*& K <= N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + WPtr == Storage &*& + RPtr == Storage &*& + End == Storage &*& + malloc_block(Storage, 0) &*& + chars(Storage, 0, _) &*& + true + ; +@*/ + +/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost +`irqMask` gives access to the core queue resources. The permissions granted +after masking interrupts depends on the caller: +- A task has access to the queue and the queuelists +- An ISR has access to the queue and, if the queue is unlocked, the queuelists */ +/*@ +predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) = + q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr)); + +predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() = + queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_isr && is_locked ? true : queuelists(queue)); +@*/ + +/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */ +/*@ +predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() = + queue->locked |-> ?m &*& + mutex(m, queue_locked_invariant(queue)); + +predicate queuesuspend(QueueHandle_t q;) = + q->schedulerSuspend |-> ?m &*& + mutex(m, scheduler_suspended_invariant(q)); +@*/ + +/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */ +/*@ +predicate queuelock(QueueHandle_t q;) = + q->locked |-> ?m &*& + mutex(m, queue_locked_invariant(q)); + +predicate_ctor queue_locked_invariant(QueueHandle_t queue)() = + queuelists(queue); +@*/ + +BaseType_t vListInitialise(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +BaseType_t listLIST_IS_EMPTY(List_t *list); +/*@requires list->uxNumberOfItems |-> ?len;@*/ +/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/ + +typedef struct xTIME_OUT +{ + BaseType_t xOverflowCount; + TickType_t xTimeOnEntering; +} TimeOut_t; + +/*@ +predicate xTIME_OUT(struct xTIME_OUT *to;) = + to->xOverflowCount |-> _ &*& + to->xTimeOnEntering |-> _ &*& + struct_xTIME_OUT_padding(to); +@*/ + +void vTaskInternalSetTimeOutState( TimeOut_t * x); +/*@requires xTIME_OUT(x);@*/ +/*@ensures xTIME_OUT(x);@*/ + +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ); +/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ +/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ + +BaseType_t xTaskRemoveFromEventList(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait ); +/*@requires list(pxEventList);@*/ +/*@ensures list(pxEventList);@*/ + +void vTaskMissedYield(); +/*@requires true;@*/ +/*@ensures true;@*/ + +void vTaskSuspendAll(); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ + +BaseType_t xTaskResumeAll( void ); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ + +void prvLockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuelock(xQueue); @*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ + +void prvUnlockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuelock(xQueue);@*/ + +void setInterruptMask(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + queuelists(xQueue);@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ +} + +void clearInterruptMask(QueueHandle_t xQueue) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*& + queuelists(xQueue);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, false)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, false);@*/ +} + +#define taskENTER_CRITICAL() setInterruptMask(xQueue) +#define taskEXIT_CRITICAL() clearInterruptMask(xQueue) +#define portYIELD_WITHIN_API() +#define queueYIELD_IF_USING_PREEMPTION() + +UBaseType_t setInterruptMaskFromISR(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_locked ? true : queuelists(xQueue));@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ + return 0; +} + +void clearInterruptMaskFromISR(QueueHandle_t xQueue, UBaseType_t uxSavedInterruptStatus) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*& + (is_locked ? true : queuelists(xQueue));@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, true)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, true);@*/ +} + +#define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR(xQueue) +#define portCLEAR_INTERRUPT_MASK_FROM_ISR(uxSavedInterruptStatus) clearInterruptMaskFromISR(xQueue, uxSavedInterruptStatus) + +#endif /* QUEUE_H */ |