FreeRTOS/FreeRTOS-Plus-TCP
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Plus-TCP synced 2025-10-24 03:32:36 +08:00
Code Issues Releases Wiki Activity

Fix CBMC proofs for DNS (#718)

Browse Source 
* Use CBMC XML output to enable VSCode debugger (#673)

Prior to this commit, CBMC would emit logging information in plain text
format, which does not contain information required for the CBMC VSCode
debugger. This commit makes CBMC use XML instead of plain text.

Co-authored-by: Mark Tuttle <tuttle@acm.org>

* wip

* wip DNSgetHostByName

* wip DNSgetHostByName

* fixed cbmc proof for DNS_ReadNameField

* wip DNSgetHostByName_a_harness

* Fix CBMC prooff for DNSgetHostByName

* wip fix DNSgetHostByName_a CBMC proof

* fixed cbmc target func not called issue in DNSclear

* fixed cbmc target func not called issue in DNSlookup

* fix DNSgetHostByName_a CBMC proof

* update comments

* more asserts

* fixing formatting

* updating as per review comments

* fix dns after review comments

* adding more asserts

* adds more asserts

* minor fix

* fixing comments

* fixing comments

* fixing minor issue

* fixing DNS_ReadReply() signature

* making code more consistant

* adding more  asserts

* making code more consistent

---------

Co-authored-by: Kareem Khazem <karkhaz@amazon.com>
Co-authored-by: Mark Tuttle <tuttle@acm.org>
This commit is contained in:
Tony Josi
2023-02-23 17:19:09 +05:30
committed by GitHub
parent ff11a1484a
commit e9bb5773ff
13 changed files with 208 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
source/FreeRTOS_DNS.c
View File

@@ -157,8 +157,6 @@
/* TODO: Fix IPv6 DNS query in Windows Simulator. */
IPPreference_t xDNS_IP_Preference = xPreferenceIPv4;
/** @brief Used for additional error checking when asserts are enabled. */
_static struct freertos_addrinfo * pxLastInfo = NULL;
/*-----------------------------------------------------------*/
/**
@@ -315,7 +313,6 @@
if( pxInfo != NULL )
{
configASSERT( pxLastInfo != pxInfo );
while( pxIterator != NULL )
{
@@ -325,7 +322,6 @@
}
}
pxLastInfo = NULL;
}
/*-----------------------------------------------------------*/
@@ -621,7 +617,7 @@
if( ulIPAddress != 0UL )
{
#if ( ipconfigUSE_IPv6 != 0 )
if( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )
if( ( ppxAddressInfo != NULL ) && ( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) )
{
FreeRTOS_printf( ( "prvPrepareLookup: found '%s' in cache: %pip\n",
pcHostName, ( *ppxAddressInfo )->xPrivateStorage.sockaddr.sin_address.xIP_IPv6.ucBytes ) );
@@ -663,7 +659,7 @@
( xFamily == FREERTOS_AF_INET6 ) ? pdTRUE : pdFALSE );
}
}
else if( ppxAddressInfo != NULL )
else if( ( ppxAddressInfo != NULL ) && ( *( ppxAddressInfo ) != NULL ) )
{
/* The IP address is known, do the call-back now. */
pCallbackFunction( pcHostName, pvSearchID, *( ppxAddressInfo ) );
@@ -950,6 +946,7 @@
if( ( xDNS_IP_Preference == xPreferenceIPv6 ) && ENDPOINT_IS_IPv6( pxEndPoint ) )
{
uint8_t ucIndex = pxEndPoint->ipv6_settings.ucDNSIndex;
configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
uint8_t * ucBytes = pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes;
/* Test if the DNS entry is in used. */
@@ -967,6 +964,7 @@
#endif /* if ( ipconfigUSE_IPv6 != 0 ) */
{
uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex;
configASSERT(ucIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT);
uint32_t ulIPAddress = pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ];
if( ( ulIPAddress != 0U ) && ( ulIPAddress != ipBROADCAST_IP_ADDRESS ) )

2
source/FreeRTOS_DNS_Networking.c
View File

@@ -136,7 +136,7 @@
* @param xAddress address to read from
* @param pxReceiveBuffer buffer to fill with received data
*/
BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxReceiveBuffer )
{

2
source/include/FreeRTOS_DNS_Networking.h
View File

@@ -46,7 +46,7 @@
const struct freertos_sockaddr * xAddress,
const struct xDNSBuffer * pxDNSBuf );
BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxReceiveBuffer );

2
test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c
View File

@@ -7,6 +7,8 @@
#include "FreeRTOS_DNS.h"
#include "FreeRTOS_IP_Private.h"
void FreeRTOS_dnsclear( void );
void harness()
{

2
test/cbmc/proofs/DNS/DNSclear/Makefile.json
View File

@@ -11,7 +11,7 @@
"OBJS":
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto"
],
"DEF":
[

87
test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
View File

@@ -22,15 +22,17 @@
uint32_t FreeRTOS_dnslookup( const char * pcHostName );
Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks );
void DNS_CloseSocket( Socket_t xDNSSocket );
void DNS_ReadReply( Socket_t xDNSSocket,
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxDNSBuf );
uint32_t DNS_SendRequest( Socket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxDNSBuf );
uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t xBufferLength,
BaseType_t xExpected );
size_t uxBufferLength,
struct freertos_addrinfo ** ppxAddressInfo,
BaseType_t xExpected,
uint16_t usPort );
/****************************************************************
* We abstract:
@@ -61,8 +63,10 @@ uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
****************************************************************/
uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t xBufferLength,
BaseType_t xExpected )
size_t uxBufferLength,
struct freertos_addrinfo ** ppxAddressInfo,
BaseType_t xExpected,
uint16_t usPort )
{
uint32_t size;
@@ -94,32 +98,39 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket,
* We stub out this function which returned a dns_buffer filled with random data
*
****************************************************************/
void DNS_ReadReply( Socket_t xDNSSocket,
BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
struct freertos_sockaddr * xAddress,
struct xDNSBuffer * pxDNSBuf )
{
BaseType_t ret;
int len;
pxDNSBuf->pucPayloadBuffer = safeMalloc( len );
__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) );
pxDNSBuf->pucPayloadBuffer = malloc( len );
pxDNSBuf->uxPayloadLength = len;
__CPROVER_assume( len < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadSize );
__CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
return ret;
}
void DNS_CloseSocket( Socket_t xDNSSocket )
{
__CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." );
free( xDNSSocket );
}
Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
{
Socket_t sock;
Socket_t sock = malloc( sizeof(struct xSOCKET) );
return sock;
}
uint32_t FreeRTOS_dnslookup( const char * pcHostName )
@@ -132,6 +143,16 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
return ret;
}
BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
NetworkBufferDescriptor_t * const pxNetworkBuffer,
BaseType_t xReleaseAfterSend )
{
__CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
__CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
BaseType_t ret;
return ret;
}
/****************************************************************
* Abstract prvCreateDNSMessage
@@ -144,7 +165,8 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName )
size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
const char * pcHostName,
TickType_t uxIdentifier )
TickType_t uxIdentifier,
UBaseType_t uxHostType )
{
__CPROVER_havoc_object( pucUDPPayloadBuffer );
size_t size;
@@ -152,6 +174,31 @@ size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
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 * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = malloc( 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;
}
/****************************************************************
* The proof for FreeRTOS_gethostbyname.
****************************************************************/
@@ -160,12 +207,28 @@ void harness()
{
size_t len;
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
__CPROVER_assume( pxNetworkEndPoints != NULL );
/* Asserts are added in the src code to make sure ucDNSIndex
will be less than ipconfigENDPOINT_DNS_ADDRESS_COUNT */
__CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
__CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
pxNetworkEndPoints->pxNext = NULL;
/* Interface init. */
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
__CPROVER_assume( len <= MAX_HOSTNAME_LEN );
char * pcHostName = safeMalloc( len );
char * pcHostName = malloc( len );
__CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */
__CPROVER_assume( pcHostName != NULL );
pcHostName[ len - 1 ] = NULL;
FreeRTOS_gethostbyname( pcHostName );
}

12
test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
View File

@@ -8,11 +8,17 @@
"callback": 0,
"MAX_HOSTNAME_LEN": 10,
"ENDPOINT_DNS_ADDRESS_COUNT": 5,
"HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
"ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
"CBMCFLAGS":
[
"--unwind 1",
"--unwindset strchr.0:{HOSTNAME_UNWIND}",
"--unwindset prvIncreaseDNS4Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
"--unwindset prvIncreaseDNS6Index.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
"--unwindset prvFillSockAddress.0:2,prvFillSockAddress.1:2",
"--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}",
"--unwindset prvGetHostByNameOp_WithRetry.0:{HOSTNAME_UNWIND}",
"--nondet-static"
@@ -22,7 +28,7 @@
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
@@ -30,7 +36,9 @@
"DEF":
[
"ipconfigUSE_IPv6=1",
"ipconfigDNS_USE_CALLBACKS={callback}",
"MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}"
"MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
"ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
]
}

88
test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
View File

@@ -48,8 +48,10 @@
****************************************************************/
uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t xBufferLength,
BaseType_t xExpected )
size_t uxBufferLength,
struct freertos_addrinfo ** ppxAddressInfo,
BaseType_t xExpected,
uint16_t usPort )
{
__CPROVER_assert( pucUDPPayloadBuffer != NULL,
"Precondition: pucUDPPayloadBuffer != NULL" );
@@ -69,7 +71,8 @@ uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
const char * pcHostName,
TickType_t uxIdentifier )
TickType_t uxIdentifier,
UBaseType_t uxHostType )
{
__CPROVER_assert( pucUDPPayloadBuffer != NULL,
"Precondition: pucUDPPayloadBuffer != NULL" );
@@ -86,8 +89,69 @@ size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
void func( const char * pcHostName,
void * pvSearchID,
uint32_t ulIPAddress )
struct freertos_addrinfo * pxAddressInfo )
{
__CPROVER_assert( pcHostName != NULL,
"Precondition: pcHostName != NULL" );
__CPROVER_assert( pvSearchID != NULL,
"Precondition: pvSearchID != NULL" );
__CPROVER_assert( pxAddressInfo != NULL,
"Precondition: pxAddressInfo != NULL" );
}
BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
NetworkBufferDescriptor_t * const pxNetworkBuffer,
BaseType_t xReleaseAfterSend )
{
__CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
__CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
BaseType_t ret;
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 * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = malloc( 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;
}
Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
{
Socket_t xSock = safeMalloc( sizeof(struct xSOCKET) );
return xSock;
}
uint32_t Prepare_CacheLookup( const char * pcHostName,
BaseType_t xFamily,
struct freertos_addrinfo ** ppxAddressInfo )
{
( * ppxAddressInfo ) = ( struct freertos_addrinfo * ) malloc( sizeof( struct freertos_addrinfo ) );
__CPROVER_assume( ( * ppxAddressInfo ) != NULL );
__CPROVER_assume( ( * ppxAddressInfo )->ai_next == NULL );
uint32_t ulRet;
return ulRet;
}
/****************************************************************
@@ -98,6 +162,19 @@ void harness()
{
size_t len;
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
__CPROVER_assume( pxNetworkEndPoints != NULL );
/* Asserts are added in the src code to make sure ucDNSIndex
will be less than ipconfigENDPOINT_DNS_ADDRESS_COUNT */
__CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
__CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT );
__CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
/* Interface init. */
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
__CPROVER_assume( len <= MAX_HOSTNAME_LEN );
char * pcHostName = safeMalloc( len );
@@ -105,9 +182,10 @@ void harness()
__CPROVER_assume( pcHostName != NULL );
pcHostName[ len - 1 ] = NULL;
FOnDNSEvent pCallback = func;
FOnDNSEvent pCallback = &func;
TickType_t xTimeout;
void * pvSearchID;
__CPROVER_assume( pvSearchID != NULL );
FreeRTOS_gethostbyname_a( pcHostName, pCallback, pvSearchID, xTimeout );
}

10
test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
View File

@@ -5,10 +5,15 @@
# According to the specification MAX_HOST_NAME is upto 255.
"callback": 1,
"MAX_HOSTNAME_LEN": 10,
"ENDPOINT_DNS_ADDRESS_COUNT": 5,
"HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
"CBMCFLAGS":
[
"--unwind 1",
"--unwindset prvFillSockAddress.0:2,prvFillSockAddress.1:2",
"--unwindset FreeRTOS_freeaddrinfo.0:2",
"--unwindset strchr.0:{HOSTNAME_UNWIND}",
"--unwindset strncpy.0:255",
"--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}",
"--nondet-static"
],
@@ -16,7 +21,7 @@
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
"$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
@@ -26,6 +31,7 @@
"ipconfigDNS_USE_CALLBACKS={callback}",
"MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
# This value is defined only when ipconfigUSE_DNS_CACHE==1
"ipconfigDNS_CACHE_NAME_LENGTH=254"
"ipconfigDNS_CACHE_NAME_LENGTH=254",
"ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
]
}

6
test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
View File

@@ -17,7 +17,8 @@ void vDNSSetCallBack( const char * pcHostName,
void * pvSearchID,
FOnDNSEvent pCallbackFunction,
TickType_t xTimeout,
TickType_t xIdentifier );
TickType_t xIdentifier,
BaseType_t xIsIPv6 );
void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
{
@@ -56,6 +57,7 @@ void harness()
FOnDNSEvent pCallback = func;
TickType_t xTimeout;
TickType_t xIdentifier;
BaseType_t xIsIPv6;
size_t len;
__CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
@@ -66,6 +68,6 @@ void harness()
pcHostName[ len - 1 ] = NULL;
}
vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier ); /* Add an item to be able to check the cancel function if the list is non-empty. */
vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier, xIsIPv6 ); /* Add an item to be able to check the cancel function if the list is non-empty. */
FreeRTOS_gethostbyname_cancel( &pvSearchID );
}

3
test/cbmc/proofs/DNS/DNSlookup/Makefile.json
View File

@@ -8,13 +8,14 @@
"CBMCFLAGS":
[
"--unwind 1",
"--unwindset prvFindEntryIndex.0:3",
"--unwindset prvProcessDNSCache.0:5,strcmp.0:{HOSTNAME_UNWIND}",
"--nondet-static"
],
"OBJS":
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto",
"$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
],
"DEF":

34
test/cbmc/proofs/ReadNameField/ReadNameField_harness.c
View File

@@ -24,10 +24,8 @@
* Signature of function under test
****************************************************************/
size_t DNS_ReadNameField( const uint8_t * pucByte,
size_t uxRemainingBytes,
char * pcName,
size_t uxDestLen );
size_t DNS_ReadNameField( ParseSet_t * pxSet,
size_t uxDestLen );
/****************************************************************
* The function under test is not defined in all configurations
@@ -41,11 +39,11 @@ size_t DNS_ReadNameField( const uint8_t * pucByte,
/* DNS_ReadNameField is not defined in this configuration, stub it. */
size_t DNS_ReadNameField( const uint8_t * pucByte,
size_t uxRemainingBytes,
char * pcName,
size_t uxDestLen )
size_t DNS_ReadNameField( ParseSet_t * pxSet,
size_t uxDestLen );
{
__CPROVER_assert( pxSet != NULL,
"pxSet shouldnt be NULL" );
return 0;
}
@@ -67,22 +65,20 @@ void harness()
"NAME_SIZE >= 4 required for good coverage." );
size_t uxRemainingBytes;
size_t uxDestLen;
ParseSet_t pxSet;
uint8_t * pucByte = malloc( uxRemainingBytes );
char * pcName = malloc( uxDestLen );
pxSet.pucByte = malloc( pxSet.uxSourceBytesRemaining );
/* Preconditions */
__CPROVER_assume( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( pxSet.uxSourceBytesRemaining < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( uxDestLen < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( uxRemainingBytes <= NETWORK_BUFFER_SIZE );
__CPROVER_assume( pxSet.uxSourceBytesRemaining <= NETWORK_BUFFER_SIZE );
__CPROVER_assume( uxDestLen <= NAME_SIZE );
__CPROVER_assume( pucByte != NULL );
__CPROVER_assume( pcName != NULL );
__CPROVER_assume( pxSet.pucByte != NULL );
/* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */
/*__CPROVER_assume(uxRemainingBytes > 0); */
@@ -90,13 +86,13 @@ void harness()
/* Avoid overflow on uxDestLen - 1U */
__CPROVER_assume( uxDestLen > 0 );
size_t index = DNS_ReadNameField( pucByte,
uxRemainingBytes,
pcName,
size_t index = DNS_ReadNameField( &pxSet,
uxDestLen );
/* Postconditions */
__CPROVER_assert( index <= uxDestLen + 1 && index <= uxRemainingBytes,
__CPROVER_assert( index <= uxDestLen + 1 && index <= pxSet.uxSourceBytesRemaining,
"DNS_ReadNameField : index <= uxDestLen+1" );
}

4
test/cbmc/stubs/freertos_api.c
View File

@@ -211,8 +211,8 @@ int32_t FreeRTOS_sendto( Socket_t xSocket,
* pointer to the buffer (or NULL).
****************************************************************/
void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes,
TickType_t xBlockTimeTicks,
void * FreeRTOS_GetUDPPayloadBuffer( size_t uxRequestedSizeBytes,
TickType_t uxBlockTimeTicks,
uint8_t ucIPType )
{
size_t size;