diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/include')
6 files changed, 268 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/include/README.md b/FreeRTOS-Plus/Test/CBMC/include/README.md new file mode 100644 index 000000000..fa317dc04 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/README.md @@ -0,0 +1,2 @@ +This directory contains include files used by the CBMC proofs: +* cbmc.h defines some macros used in the proof test harnesses diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h new file mode 100644 index 000000000..22434a91c --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h @@ -0,0 +1,3 @@ +eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer ) { + prvProcessIPPacket(pxIPPacket, pxNetworkBuffer); +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h new file mode 100644 index 000000000..01075d2ba --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h @@ -0,0 +1,12 @@ +int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ) { + prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength ); +} + +BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ) { + prvTCPHandleState(pxSocket, ppxNetworkBuffer); +} + +void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer, + uint32_t ulLen, BaseType_t xReleaseAfterSend ) { + prvTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/cbmc.h b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h new file mode 100644 index 000000000..c30063bae --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h @@ -0,0 +1,100 @@ +/* Standard includes. */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" + +/* + * CBMC models a pointer as an object id and an offset into that + * object. The top bits of a pointer encode the object id and the + * remaining bits encode the offset. This means there is a bound on + * the maximum offset into an object in CBMC, and hence a bound on the + * size of objects in CBMC. + */ +#define CBMC_BITS 7 +#define CBMC_MAX_OBJECT_SIZE ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) ) + +#define IMPLIES( a, b ) ( !( a ) || ( b ) ) + +BaseType_t nondet_basetype(); +UBaseType_t nondet_ubasetype(); +TickType_t nondet_ticktype(); +int32_t nondet_int32(); +uint32_t nondet_uint32(); +size_t nondet_sizet(); + +#define nondet_BaseType() nondet_basetype() + +void * safeMalloc( size_t size ); + + +enum CBMC_LOOP_CONDITION +{ + CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN +}; + +/* CBMC specification: capture old value for precondition and */ +/* postcondition checking */ + +#define OLDVAL( var ) _old_ ## var +#define SAVE_OLDVAL( var, typ ) const typ OLDVAL( var ) = var + +/* CBMC specification: capture old value for values passed by */ +/* reference in function abstractions */ + +#define OBJ( var ) ( * var ) +#define OLDOBJ( var ) _oldobj_ ## var +#define SAVE_OLDOBJ( var, typ ) const typ OLDOBJ( var ) = OBJ( var ) + +/* CBMC debugging: printfs for expressions */ + +#define __CPROVER_printf( var ) { uint32_t ValueOf_ ## var = ( uint32_t ) var; } +#define __CPROVER_printf2( str, exp ) { uint32_t ValueOf_ ## str = ( uint32_t ) ( exp ); } + +/* CBMC debugging: printfs for pointer expressions */ + +#define __CPROVER_printf_ptr( var ) { uint8_t * ValueOf_ ## var = ( uint8_t * ) var; } +#define __CPROVER_printf2_ptr( str, exp ) { uint8_t * ValueOf_ ## str = ( uint8_t * ) ( exp ); } + +/* + * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes. + * This assertion is used in some of the TaskPool proofs. + */ +#define __CPROVER_assert_zero_allocation() \ + __CPROVER_assert( pvPortMalloc( 0 ) == NULL, \ + "pvPortMalloc allows zero-allocated memory." ) + +/* + * A stub for pvPortMalloc that nondeterministically chooses to return + * either NULL or an allocation of the requested space. The stub is + * guaranteed to return NULL when asked to allocate 0 bytes. + * This stub is used in some of the TaskPool proofs. + */ +void * pvPortMalloc( size_t xWantedSize ) +{ + if( xWantedSize == 0 ) + { + return NULL; + } + + return nondet_bool() ? malloc( xWantedSize ) : NULL; +} + +void vPortFree( void * pv ) +{ + ( void ) pv; + free( pv ); +} 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; +} diff --git a/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h new file mode 100644 index 000000000..a0dd6de4a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h @@ -0,0 +1,10 @@ +#ifndef INC_TASK_STUBS_H +#define INC_TASK_STUBS_H + +#include "FreeRTOS.h" +#include "task.h" + +BaseType_t xState; +void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit); + +#endif /* INC_TASK_STUBS_H */ |