diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/include/queue_init.h')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/include/queue_init.h | 141 |
1 files changed, 141 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/include/queue_init.h b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h new file mode 100644 index 000000000..f05d18830 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/queue_init.h @@ -0,0 +1,141 @@ +#include "FreeRTOS.h" +#include "queue.h" +#include "queue_datastructure.h" + +#ifndef CBMC_OBJECT_BITS +#define CBMC_OBJECT_BITS 7 +#endif + +#ifndef CBMC_OBJECT_MAX_SIZE +#define CBMC_OBJECT_MAX_SIZE (UINT32_MAX>>(CBMC_OBJECT_BITS+1)) +#endif + +/* Using prvCopyDataToQueue together with prvNotifyQueueSetContainer + leads to a problem space explosion. Therefore, we use this stub + and a sepearted proof on prvCopyDataToQueue to deal with it. + As prvNotifyQueueSetContainer is disabled if configUSE_QUEUE_SETS != 1, + in other cases the original implementation should be used. */ +#if( configUSE_QUEUE_SETS == 1 ) + BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) + { + if(pxQueue->uxItemSize > ( UBaseType_t ) 0) + { + __CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable"); + if(xPosition == queueSEND_TO_BACK){ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable"); + }else{ + __CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable"); + } + return pdFALSE; + }else + { + return nondet_BaseType_t(); + } + } +#endif + +/* xQueueCreateSet is compiled out if configUSE_QUEUE_SETS != 1.*/ +#if( configUSE_QUEUE_SETS == 1 ) + QueueSetHandle_t xUnconstrainedQueueSet() + { + UBaseType_t uxEventQueueLength = 2; + QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength); + if( xSet ) + { + xSet->cTxLock = nondet_int8_t(); + xSet->cRxLock = nondet_int8_t(); + xSet->uxMessagesWaiting = nondet_UBaseType_t(); + xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength); + xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + } + return xSet; + } +#endif + +/* Create a mostly unconstrained Queue but bound the max item size. + This is required for performance reasons in CBMC at the moment. */ +QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound ) { + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + __CPROVER_assume(uxQueueLength > 0); + __CPROVER_assume(uxItemSize < uxItemSizeBound); + + // QueueGenericCreate method does not check for multiplication overflow + size_t uxQueueStorageSize; + __CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE); + __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} + +/* Create a mostly unconstrained Queue */ +QueueHandle_t xUnconstrainedQueue( void ) { + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; + + __CPROVER_assume(uxQueueLength > 0); + + // QueueGenericCreate method does not check for multiplication overflow + size_t uxQueueStorageSize; + __CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE); + __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + + QueueHandle_t xQueue = + xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType); + + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} + +/* Create a mostly unconstrained Mutex */ +QueueHandle_t xUnconstrainedMutex( void ) { + uint8_t ucQueueType; + QueueHandle_t xQueue = + xQueueCreateMutex(ucQueueType); + if(xQueue){ + xQueue->cTxLock = nondet_int8_t(); + xQueue->cRxLock = nondet_int8_t(); + xQueue->uxMessagesWaiting = nondet_UBaseType_t(); + /* This is an invariant checked with a couple of asserts in the code base. + If it is false from the beginning, the CBMC proofs are not able to succeed*/ + __CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength); + xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t(); + xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t(); + #if( configUSE_QUEUE_SETS == 1) + xQueueAddToSet(xQueue, xUnconstrainedQueueSet()); + #endif + } + return xQueue; +} |