Skip to content

Commit

Permalink
Revert unnecessary change
Browse files Browse the repository at this point in the history
  • Loading branch information
@ActoryOu
ActoryOu committed Jul 16, 2024
1 parent 6071476 commit f211db9
Show file tree
Hide file tree
Showing 6 changed files with 153 additions and 134 deletions.
7 changes: 2 additions & 5 deletions source/FreeRTOS_IP.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1042,11 +1042,8 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void const * pvBuffer )
NetworkBufferDescriptor_t * pxBuffer;

pxBuffer = pxUDPPayloadBuffer_to_NetworkBuffer( pvBuffer );

if( pxBuffer != NULL )
{
vReleaseNetworkBufferAndDescriptor( pxBuffer );
}
configASSERT( pxBuffer != NULL );
vReleaseNetworkBufferAndDescriptor( pxBuffer );
}
/*-----------------------------------------------------------*/

Expand Down
34 changes: 17 additions & 17 deletions source/FreeRTOS_IP_Utils.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -747,32 +747,32 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
* for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */
ucIPType = pucIPType[ 0 ] & 0xf0U;

/* To help the translation from a UDP payload pointer to a networkBuffer,
* a byte was stored at a certain negative offset (-48 bytes).
* It must have a value of either 0x4x or 0x6x. */
configASSERT( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) );

switch( ucIPType ) /* LCOV_EXCL_BR_LINE */
{
/* For Rx path, it's possible to receive packets that is disabled. We should be able to get the network
* descriptor to free that network buffer correctly. */
case ipTYPE_IPv6:
uxOffset = sizeof( UDPPacket_IPv6_t );
break;
#if ( ipconfigUSE_IPv6 != 0 )
case ipTYPE_IPv6:
uxOffset = sizeof( UDPPacket_IPv6_t );
break;
#endif /* ( ipconfigUSE_IPv6 != 0 ) */

case ipTYPE_IPv4:
uxOffset = sizeof( UDPPacket_t );
break;
#if ( ipconfigUSE_IPv4 != 0 )
case ipTYPE_IPv4:
uxOffset = sizeof( UDPPacket_t );
break;
#endif /* ( ipconfigUSE_IPv4 != 0 ) */

default:
FreeRTOS_debug_printf( ( "pxUDPPayloadBuffer_to_NetworkBuffer: Undefined ucIPType \n" ) );
uxOffset = 0;
uxOffset = sizeof( UDPPacket_t );
break;
}

if( uxOffset != 0 )
{
pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
}
else
{
pxResult = NULL;
}
pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
}

return pxResult;
Expand Down
129 changes: 75 additions & 54 deletions test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
#include "NetworkBufferManagement.h"
#include "NetworkInterface.h"

/* CBMC includes. */
#include "cbmc.h"

uint32_t FreeRTOS_dnslookup( const char * pcHostName );
Expand All @@ -37,6 +38,7 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
const char * pcHostName,
TickType_t uxIdentifier,
UBaseType_t uxHostType );
uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer );

/****************************************************************
* We abstract:
Expand All @@ -56,6 +58,54 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
* bound the iterations of strcmp.
****************************************************************/

/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
TickType_t xBlockTimeTicks )
{
NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );

if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );

if( pxNetworkBuffer->pucEthernetBuffer == NULL )
{
free( pxNetworkBuffer );
pxNetworkBuffer = NULL;
}
else
{
pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
}
}

return pxNetworkBuffer;
}

/*
* In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
* stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
*/
void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer != NULL,
"Precondition: pxNetworkBuffer != NULL" );

free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET );
free( pxNetworkBuffer );
}

/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
* is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
* memory */
void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
{
__CPROVER_assert( pvBuffer != NULL,
"FreeRTOS precondition: pvBuffer != NULL" );
}

/****************************************************************
* Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply.
*
Expand Down Expand Up @@ -122,20 +172,39 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxDNSBuf )
{
BaseType_t ret;
int len;
uintptr_t uxTypeOffset;
const uint8_t * pucIPType;
uint8_t ucIPType;
NetworkBufferDescriptor_t * pxNetworkEndPoints;

__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) );
__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) );

pxDNSBuf->pucPayloadBuffer = malloc( len );
pxNetworkEndPoints = pxGetNetworkBufferWithDescriptor( len, 0 );
__CPROVER_assume( pxNetworkEndPoints != NULL );
__CPROVER_assume( pxNetworkEndPoints->pucEthernetBuffer != NULL );

pxDNSBuf->pucPayloadBuffer = pxNetworkEndPoints->pucEthernetBuffer;
pxDNSBuf->uxPayloadLength = len;

__CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );

__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );

return ret;
/* When IPv6 is supported, find out the type of the packet.
* It is stored 48 bytes before the payload buffer as 0x40 or 0x60. */
uxTypeOffset = __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( pxDNSBuf->pucPayloadBuffer );
uxTypeOffset -= ipUDP_PAYLOAD_IP_TYPE_OFFSET;
pucIPType = ( const uint8_t * ) uxTypeOffset;

/* For an IPv4 packet, pucIPType points to 6 bytes before the pucEthernetBuffer,
* for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */
ucIPType = pucIPType[ 0 ] & 0xf0U;

/* To help the translation from a UDP payload pointer to a networkBuffer,
* a byte was stored at a certain negative offset (-48 bytes).
* It must have a value of either 0x4x or 0x6x. */
__CPROVER_assume( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) );

return nondet_basetype();
}


Expand Down Expand Up @@ -193,54 +262,6 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
return size;
}

/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
TickType_t xBlockTimeTicks )
{
NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );

if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );

if( pxNetworkBuffer->pucEthernetBuffer == NULL )
{
free( pxNetworkBuffer );
pxNetworkBuffer = NULL;
}
else
{
pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
}
}

return pxNetworkBuffer;
}

/*
* In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
* stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
*/
void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer != NULL,
"Precondition: pxNetworkBuffer != NULL" );

free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET );
free( pxNetworkBuffer );
}

/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
* is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
* memory */
void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
{
__CPROVER_assert( pvBuffer != NULL,
"FreeRTOS precondition: pvBuffer != NULL" );
}

uint32_t Prepare_CacheLookup( const char * pcHostName,
BaseType_t xFamily,
struct freertos_addrinfo ** ppxAddressInfo )
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
"OBJS":
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
Expand Down
114 changes: 58 additions & 56 deletions test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,11 @@
#include "NetworkBufferManagement.h"
#include "NetworkInterface.h"

/* CBMC includes. */
#include "cbmc.h"

uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer );

/****************************************************************
* We abstract:
*
Expand All @@ -37,6 +40,54 @@
* bound the iterations of strcmp.
****************************************************************/

/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
TickType_t xBlockTimeTicks )
{
NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );

if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET );

if( pxNetworkBuffer->pucEthernetBuffer == NULL )
{
free( pxNetworkBuffer );
pxNetworkBuffer = NULL;
}
else
{
pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
}
}

return pxNetworkBuffer;
}

/*
* In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
* stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
*/
void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer != NULL,
"Precondition: pxNetworkBuffer != NULL" );

free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) );
free( pxNetworkBuffer );
}

/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
* is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
* memory */
void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
{
__CPROVER_assert( pvBuffer != NULL,
"FreeRTOS precondition: pvBuffer != NULL" );
}

/****************************************************************
* Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply.
*
Expand Down Expand Up @@ -111,45 +162,6 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
return ret;
}

/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
TickType_t xBlockTimeTicks )
{
NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );

if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET );

if( pxNetworkBuffer->pucEthernetBuffer == NULL )
{
free( pxNetworkBuffer );
pxNetworkBuffer = NULL;
}
else
{
pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
}
}

return pxNetworkBuffer;
}

/*
* In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
* stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
*/
void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer != NULL,
"Precondition: pxNetworkBuffer != NULL" );

free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) );
free( pxNetworkBuffer );
}

Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
{
Socket_t xSock = safeMalloc( sizeof( struct xSOCKET ) );
Expand Down Expand Up @@ -207,31 +219,21 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxDNSBuf )
{
BaseType_t ret;
int len;
NetworkBufferDescriptor_t * pxNetworkBuffer;

__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) );

if( nondet_bool() )
{
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 );
__CPROVER_assume( pxNetworkBuffer != NULL );
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 );
__CPROVER_assume( pxNetworkBuffer != NULL );
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );

pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer;
pxDNSBuf->uxPayloadLength = len;
__CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer;
pxDNSBuf->uxPayloadLength = len;

__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );

ret = len;
}
else
{
__CPROVER_assume( ret < 0 );
}

return ret;
return nondet_basetype();
}

/* Function xDNSSetCallBack is proven to be correct separately. */
Expand Down
Loading

0 comments on commit f211db9

Please sign in to comment.