From e9bb5773ffbff32ba56533ea135281dbb49d96f8 Mon Sep 17 00:00:00 2001 From: Tony Josi Date: Thu, 23 Feb 2023 17:19:09 +0530 Subject: [PATCH] Fix CBMC proofs for DNS (#718) * 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 * 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 Co-authored-by: Mark Tuttle --- source/FreeRTOS_DNS.c | 10 +-- source/FreeRTOS_DNS_Networking.c | 2 +- source/include/FreeRTOS_DNS_Networking.h | 2 +- .../proofs/DNS/DNSclear/DNSclear_harness.c | 2 + test/cbmc/proofs/DNS/DNSclear/Makefile.json | 2 +- .../DNSgetHostByName_harness.c | 87 +++++++++++++++--- .../proofs/DNS/DNSgetHostByName/Makefile.json | 12 ++- .../DNSgetHostByName_a_harness.c | 88 +++++++++++++++++-- .../DNS/DNSgetHostByName_a/Makefile.json | 10 ++- .../DNSgetHostByName_cancel_harness.c | 6 +- test/cbmc/proofs/DNS/DNSlookup/Makefile.json | 3 +- .../ReadNameField/ReadNameField_harness.c | 34 ++++--- test/cbmc/stubs/freertos_api.c | 4 +- 13 files changed, 208 insertions(+), 54 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index d2db8b83a..39c09c917 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -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 ) ) diff --git a/source/FreeRTOS_DNS_Networking.c b/source/FreeRTOS_DNS_Networking.c index 46211cfa3..1406e8ef8 100644 --- a/source/FreeRTOS_DNS_Networking.c +++ b/source/FreeRTOS_DNS_Networking.c @@ -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 ) { diff --git a/source/include/FreeRTOS_DNS_Networking.h b/source/include/FreeRTOS_DNS_Networking.h index 902164389..9b36fdb95 100644 --- a/source/include/FreeRTOS_DNS_Networking.h +++ b/source/include/FreeRTOS_DNS_Networking.h @@ -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 ); diff --git a/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c b/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c index 0e73545dd..440a74fdd 100644 --- a/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c +++ b/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c @@ -7,6 +7,8 @@ #include "FreeRTOS_DNS.h" #include "FreeRTOS_IP_Private.h" +void FreeRTOS_dnsclear( void ); + void harness() { diff --git a/test/cbmc/proofs/DNS/DNSclear/Makefile.json b/test/cbmc/proofs/DNS/DNSclear/Makefile.json index 05be31266..2f5ccf4dd 100644 --- a/test/cbmc/proofs/DNS/DNSclear/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSclear/Makefile.json @@ -11,7 +11,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 6fe871069..fc7237386 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -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 ); + } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 81ef8aacc..79cef356a 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -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}" ] } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c index bc1190458..4ab6d8163 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -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 ); } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index 6d364a58b..421858957 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -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}" ] } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c index b24685dc7..8536a2612 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c @@ -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 ); } diff --git a/test/cbmc/proofs/DNS/DNSlookup/Makefile.json b/test/cbmc/proofs/DNS/DNSlookup/Makefile.json index 103c1ab54..ed8954868 100644 --- a/test/cbmc/proofs/DNS/DNSlookup/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSlookup/Makefile.json @@ -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": diff --git a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c index 253688a13..706679307 100644 --- a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c +++ b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c @@ -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" ); } diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index f52a1573f..a0d7c54c7 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -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;