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.
FreeRTOS · Oct 1, 2020 · 063a5a7 · 063a5a7
1 parent 54faf1c
commit 063a5a7
Show file tree

Hide file tree

Showing 11 changed files with 44 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/.../cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c b/.../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
@@ -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
@@ -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
@@ -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;
+	}
 }
 
 /****************************************************************