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;