Merge pull request #14 from FreeRTOS/malloc

Modify CBMC proofs to make assumptions about malloc explicit.
FreeRTOS · Oct 2, 2020 · 2314ca5 · 2314ca5
2 parents e104bca + 063a5a7
commit 2314ca5
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;
+	}
 }
 
 /****************************************************************