From 063a5a758b489b0be0b65900118391a79c914176 Mon Sep 17 00:00:00 2001 From: "Mark R. Tuttle" Date: Thu, 1 Oct 2020 20:35:28 +0000 Subject: [PATCH] Modify CBMC proofs to make assumptions about malloc explicit. Some proofs assume that some pointers returned by malloc are not NULL. This patch modifies those proofs to make these assumptions explicit with `__CPROVER_assume(pointer != NULL)` for all such pointers. --- .../proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c | 4 ++++ .../ARPGenerateRequestPacket_harness.c | 1 + .../OutputARPRequest_harness.c | 2 ++ .../OutputARPRequest_harness.c | 6 +++++- .../OutputARPRequest_harness.c | 5 ++++- test/cbmc/proofs/CheckOptions/CheckOptions_harness.c | 1 + .../CheckOptionsInner/CheckOptionsInner_harness.c | 6 ++++++ .../vSocketBind_harness.c | 2 ++ .../TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c | 2 ++ .../ProcessIPPacket/ProcessIPPacket_harness.c | 7 +++++++ test/cbmc/stubs/freertos_api.c | 12 ++++++++++-- 11 files changed, 44 insertions(+), 4 deletions(-) diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c index 05f31d926..3e9e2ded2 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c +++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -14,7 +14,11 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS { NetworkBufferDescriptor_t *pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) ); + __CPROVER_assume( pxNetworkBuffer != NULL ); + pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; return pxNetworkBuffer; } diff --git a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c index d35641318..8ce128eec 100644 --- a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c +++ b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -18,6 +18,7 @@ void harness() __CPROVER_assume( ucBUFFER_SIZE >= sizeof( ARPPacket_t ) && ucBUFFER_SIZE < 2 * sizeof( ARPPacket_t ) ); void *xBuffer = malloc( ucBUFFER_SIZE ); + __CPROVER_assume( xBuffer != NULL ); NetworkBufferDescriptor_t xNetworkBuffer2; xNetworkBuffer2.pucEthernetBuffer = xBuffer; diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c index 8bc882566..7f8456ce7 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -66,6 +66,8 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS __CPROVER_assume( malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes ); xNetworkBuffer.pucEthernetBuffer = malloc( malloc_size ); #endif + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); + xNetworkBuffer.xDataLength = xRequestedSizeBytes; return &xNetworkBuffer; } diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c index 2923e6f83..c12e1e57f 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -33,6 +33,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB #else current->pucEthernetBuffer = malloc( sizeof( ARPPacket_t ) ); #endif + __CPROVER_assume( current->pucEthernetBuffer != NULL ); current->xDataLength = sizeof( ARPPacket_t ); } } @@ -47,7 +48,10 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB safety point of view. */ void * pvPortMalloc( size_t xWantedSize ) { - return malloc( xWantedSize ); +void *ptr = malloc( xWantedSize ); + + __CPROVER_assume( ptr != NULL ); + return ptr; } /* diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c index e5dd072fa..76e743c6a 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -25,7 +25,10 @@ void * pvPortMalloc( size_t xWantedSize ) { - return malloc( xWantedSize ); +void *ptr = malloc( xWantedSize ); + + __CPROVER_assume( ptr != NULL ); + return ptr; } diff --git a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c index 67439b07e..523aa1d60 100644 --- a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c +++ b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c @@ -81,6 +81,7 @@ void harness() /* pxNetworkBuffer can be any buffer descriptor with any buffer */ NetworkBufferDescriptor_t pxNetworkBuffer; pxNetworkBuffer.pucEthernetBuffer = malloc( buffer_size ); + __CPROVER_assume( pxNetworkBuffer.pucEthernetBuffer != NULL ); pxNetworkBuffer.xDataLength = buffer_size; /**************************************************************** diff --git a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c index 3d17373d1..6a3403275 100644 --- a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c +++ b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -38,19 +38,24 @@ void harness() size_t buffer_size; uint8_t * pucPtr = malloc( buffer_size ); + __CPROVER_assume( pucPtr != NULL ); + /* uxIndex in an index into the buffer */ size_t uxIndex; /* pxSocket can be any socket with some initialized values */ FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + __CPROVER_assume( pxSocket != NULL ); pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL ); vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); if( nondet_bool() ) { TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume( segment != NULL ); listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue, &segment->xQueueItem ); } @@ -60,6 +65,7 @@ void harness() if( nondet_bool() ) { TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume( segment != NULL ); vListInitialiseItem( &segment->xSegmentItem ); listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xTxSegments, &segment->xQueueItem ); diff --git a/test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c b/test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c index 60f59c865..190fc94c5 100644 --- a/test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c +++ b/test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c @@ -54,6 +54,8 @@ FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); /* malloc instead of safeMalloc since we do not allow socket without binding. */ struct freertos_sockaddr * pxBindAddress = malloc( sizeof( struct freertos_sockaddr ) ); + __CPROVER_assume( pxBindAddress != NULL ); + /* uxAddressLength is not used in this implementation. */ size_t uxAddressLength; diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index 982f2324d..c574e0b60 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -55,6 +55,7 @@ size_t bufferSize = sizeof( NetworkBufferDescriptor_t ); /* The code does not expect pucEthernetBuffer to be equal to NULL if pxBuffer is not NULL. */ pxBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes ); + __CPROVER_assume( pxBuffer->pucEthernetBuffer != NULL ); pxBuffer->xDataLength = xRequestedSizeBytes; } @@ -75,6 +76,7 @@ size_t bufferSize = sizeof( TCPPacket_t ); /* The code does not expect pucEthernetBuffer to be equal to NULL if pxNetworkBuffer is not NULL. */ pxNetworkBuffer->pucEthernetBuffer = malloc( bufferSize ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); } UBaseType_t uxOptionsLength; diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c index a93812e45..e601ad41b 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -30,10 +30,17 @@ void harness() { NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc( sizeof( NetworkBufferDescriptor_t ) ); + __CPROVER_assume( pxNetworkBuffer != NULL ); + /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ pxNetworkBuffer->pucEthernetBuffer = malloc( ipTOTAL_ETHERNET_FRAME_SIZE ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ __CPROVER_assume( pxNetworkBuffer->xDataLength >= sizeof( IPPacket_t ) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE ); + IPPacket_t * const pxIPPacket = malloc( sizeof( IPPacket_t ) ); + __CPROVER_assume( pxIPPacket != NULL ); + publicProcessIPPacket( pxIPPacket, pxNetworkBuffer ); } diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index 114e51ee2..19eace3eb 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -37,8 +37,16 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol ) { - return nondet_bool() ? - FREERTOS_INVALID_SOCKET : malloc( sizeof( Socket_t ) ); + if( nondet_bool() ) + { + return FREERTOS_INVALID_SOCKET; + } + else + { + void *ptr = malloc( sizeof( Socket_t ) ); + __CPROVER_assume( ptr != NULL ); + return ptr; + } } /****************************************************************