From f30e18524c8824ccc808d1ce09c152e52596806f Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 13 Jan 2023 17:42:24 +0000 Subject: [PATCH 01/26] 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 --- test/cbmc/proofs/Makefile.template | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 375c15c120..094fd560c1 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -119,8 +119,8 @@ goto: # Ignore the return code for CBMC, so that we can still generate the # report if the proof failed. If the proof failed, we separately fail # the entire job using the check-cbmc-result rule. -cbmc.txt: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 +cbmc.xml: $(ENTRY).goto + -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 @@ -128,29 +128,27 @@ property.xml: $(ENTRY).goto coverage.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 -cbmc: cbmc.txt +cbmc: cbmc.xml property: property.xml coverage: coverage.xml -report: cbmc.txt property.xml coverage.xml +report: cbmc.xml property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS_PLUS_TCP) \ - --blddir $(FREERTOS_PLUS_TCP) \ - --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ - --result cbmc.txt \ + --reportdir report \ + --result cbmc.xml \ --property property.xml \ - --block coverage.xml + --coverage coverage.xml -# This rule depends only on cbmc.txt and has no dependents, so it will +# This rule depends only on cbmc.xml and has no dependents, so it will # not block the report from being generated if it fails. This rule is # intended to fail if and only if the CBMC safety check that emits -# cbmc.txt yielded a proof failure. -check-cbmc-result: cbmc.txt - grep -e "^VERIFICATION SUCCESSFUL" $^ +# cbmc.xml yielded a proof failure. +check-cbmc-result: cbmc.xml + grep 'SUCCESS' $^ # ____________________________________________________________________ # Rules @@ -160,7 +158,7 @@ check-cbmc-result: cbmc.txt clean: @RM@ $(OBJS) $(ENTRY).goto @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt - @RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* + @RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-* @RM@ *~ \#* @RM@ queue_datastructure.h From e703699345a4df57cb68586660b0df73f4869dea Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 Feb 2023 11:49:28 +0000 Subject: [PATCH 02/26] wip --- source/FreeRTOS_DNS.c | 177 +++++++++--------- test/cbmc/patches/FreeRTOSConfig.h | 2 +- .../DNSgetHostByName_harness.c | 41 +++- .../proofs/DNS/DNSgetHostByName/Makefile.json | 3 + 4 files changed, 127 insertions(+), 96 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index e1d6f1458d..3b49811063 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -621,7 +621,7 @@ if( ulIPAddress != 0UL ) { #if ( ipconfigUSE_IPv6 != 0 ) - if( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) + if( ( ppxAddressInfo != NULL) && ( *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 ) ); @@ -729,27 +729,30 @@ */ static void prvIncreaseDNS4Index( NetworkEndPoint_t * pxEndPoint ) { - uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex; - uint8_t ucInitialIndex = ucIndex; - - for( ; ; ) + if ( pxEndPoint != NULL) { - ucIndex++; + uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex; + uint8_t ucInitialIndex = ucIndex; - if( ucIndex >= ( uint8_t ) ipconfigENDPOINT_DNS_ADDRESS_COUNT ) + for( ; ; ) { - ucIndex = 0U; - } + ucIndex++; - if( ( pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ] != 0U ) || - ( ucInitialIndex == ucIndex ) ) - { - break; + if( ucIndex >= ( uint8_t ) ipconfigENDPOINT_DNS_ADDRESS_COUNT ) + { + ucIndex = 0U; + } + + if( ( pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ] != 0U ) || + ( ucInitialIndex == ucIndex ) ) + { + break; + } } - } - FreeRTOS_printf( ( "prvIncreaseDNS4Index: from %d to %d\n", ( int ) ucInitialIndex, ( int ) ucIndex ) ); - pxEndPoint->ipv4_settings.ucDNSIndex = ucIndex; + FreeRTOS_printf( ( "prvIncreaseDNS4Index: from %d to %d\n", ( int ) ucInitialIndex, ( int ) ucIndex ) ); + pxEndPoint->ipv4_settings.ucDNSIndex = ucIndex; + } } /*-----------------------------------------------------------*/ @@ -950,10 +953,10 @@ if( ( xDNS_IP_Preference == xPreferenceIPv6 ) && ENDPOINT_IS_IPv6( pxEndPoint ) ) { uint8_t ucIndex = pxEndPoint->ipv6_settings.ucDNSIndex; - uint8_t * ucBytes = pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes; + uint8_t * ucBytes = &(pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes); /* Test if the DNS entry is in used. */ - if( ( ucBytes[ 0 ] != 0U ) && ( ucBytes[ 1 ] != 0U ) ) + if( ( ucBytes ) && ( ucBytes[ 0 ] != 0U ) && ( ucBytes[ 1 ] != 0U ) ) { pxAddress->sin_family = FREERTOS_AF_INET6; pxAddress->sin_len = ( uint8_t ) sizeof( struct freertos_sockaddr ); @@ -1171,78 +1174,78 @@ pxEndPoint = prvFillSockAddress( &xAddress, pcHostName ); - if( pxEndPoint != NULL ) + if( pxEndPoint != NULL && xDNSSocket != NULL) { do { - if( xDNSSocket->usLocalPort == 0U ) - { - /* Bind the client socket to a random port number. */ - uint16_t usPort = 0U; - #if ( ipconfigUSE_MDNS == 1 ) - if( xAddress.sin_port == FreeRTOS_htons( ipMDNS_PORT ) ) - { - /* For a mDNS lookup, bind to the mDNS port 5353. */ - usPort = FreeRTOS_htons( ipMDNS_PORT ); - } - #endif - - if( DNS_BindSocket( xDNSSocket, usPort ) != 0 ) - { - FreeRTOS_printf( ( "DNS bind to %u failed\n", FreeRTOS_ntohs( usPort ) ) ); - break; - } - } - - uxReturn = prvSendBuffer( pcHostName, - uxIdentifier, - xDNSSocket, - xFamily, - &xAddress ); - - if( uxReturn == pdFAIL ) - { - break; - } - - /* Create the message in the obtained buffer. */ - - /* receive a dns reply message */ - xBytes = DNS_ReadReply( xDNSSocket, - &xRecvAddress, - &xReceiveBuffer ); - - if( ( uxReadTimeOut_ticks > 0 ) && - ( pxEndPoint != NULL ) && - ( ( xBytes == -pdFREERTOS_ERRNO_EWOULDBLOCK ) || - ( xBytes == 0 ) ) ) - { - /* This search timed out, next time try with a different DNS. */ - #if ( ipconfigUSE_IPv6 != 0 ) - if( xAddress.sin_family == FREERTOS_AF_INET6 ) - { - prvIncreaseDNS6Index( pxEndPoint ); - } - else - #endif - { - prvIncreaseDNS4Index( pxEndPoint ); - } - } - - if( xReceiveBuffer.pucPayloadBuffer != NULL ) - { - if( xBytes > 0 ) - { - xReceiveBuffer.uxPayloadLength = xBytes; - ulIPAddress = prvDNSReply( &xReceiveBuffer, ppxAddressInfo, uxIdentifier, xRecvAddress.sin_port ); - } - - /* Finished with the buffer. The zero copy interface - * is being used, so the buffer must be freed by the - * task. */ - FreeRTOS_ReleaseUDPPayloadBuffer( xReceiveBuffer.pucPayloadBuffer ); - } + // if( xDNSSocket->usLocalPort == 0U ) + // { + // /* Bind the client socket to a random port number. */ + // uint16_t usPort = 0U; + // #if ( ipconfigUSE_MDNS == 1 ) + // if( xAddress.sin_port == FreeRTOS_htons( ipMDNS_PORT ) ) + // { + // /* For a mDNS lookup, bind to the mDNS port 5353. */ + // usPort = FreeRTOS_htons( ipMDNS_PORT ); + // } + // #endif + + // if( DNS_BindSocket( xDNSSocket, usPort ) != 0 ) + // { + // FreeRTOS_printf( ( "DNS bind to %u failed\n", FreeRTOS_ntohs( usPort ) ) ); + // break; + // } + // } + + // uxReturn = prvSendBuffer( pcHostName, + // uxIdentifier, + // xDNSSocket, + // xFamily, + // &xAddress ); + + // if( uxReturn == pdFAIL ) + // { + // break; + // } + + // /* Create the message in the obtained buffer. */ + + // /* receive a dns reply message */ + // xBytes = DNS_ReadReply( xDNSSocket, + // &xRecvAddress, + // &xReceiveBuffer ); + + // if( ( uxReadTimeOut_ticks > 0 ) && + // ( pxEndPoint != NULL ) && + // ( ( xBytes == -pdFREERTOS_ERRNO_EWOULDBLOCK ) || + // ( xBytes == 0 ) ) ) + // { + // /* This search timed out, next time try with a different DNS. */ + // #if ( ipconfigUSE_IPv6 != 0 ) + // if( xAddress.sin_family == FREERTOS_AF_INET6 ) + // { + // prvIncreaseDNS6Index( pxEndPoint ); + // } + // else + // #endif + // { + // prvIncreaseDNS4Index( pxEndPoint ); + // } + // } + + // if( xReceiveBuffer.pucPayloadBuffer != NULL ) + // { + // if( xBytes > 0 ) + // { + // xReceiveBuffer.uxPayloadLength = xBytes; + // ulIPAddress = prvDNSReply( &xReceiveBuffer, ppxAddressInfo, uxIdentifier, xRecvAddress.sin_port ); + // } + + // /* Finished with the buffer. The zero copy interface + // * is being used, so the buffer must be freed by the + // * task. */ + // FreeRTOS_ReleaseUDPPayloadBuffer( xReceiveBuffer.pucPayloadBuffer ); + // } } while( ipFALSE_BOOL ); } else diff --git a/test/cbmc/patches/FreeRTOSConfig.h b/test/cbmc/patches/FreeRTOSConfig.h index e3ed1f8ad5..7e61af32f1 100644 --- a/test/cbmc/patches/FreeRTOSConfig.h +++ b/test/cbmc/patches/FreeRTOSConfig.h @@ -127,7 +127,7 @@ * is set to 2 so the formatting functions are included without the stdio.h being * included in tasks.c. That is because this project defines its own sprintf() * functions. */ -#define configUSE_STATS_FORMATTING_FUNCTIONS 1 +#define configUSE_STATS_FORMATTING_FUNCTIONS 0 /* Assert call defined for debug builds. */ extern void vAssertCalled( const char * pcFile, diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 6fe8710696..95cc678ab2 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( const 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,10 +98,11 @@ 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( const ConstSocket_t xDNSSocket, struct freertos_sockaddr * xAddress, struct xDNSBuffer * pxDNSBuf ) { + BaseType_t ret; int len; pxDNSBuf->pucPayloadBuffer = safeMalloc( len ); @@ -107,7 +112,9 @@ void DNS_ReadReply( Socket_t xDNSSocket, __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; } @@ -132,6 +139,13 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName ) return ret; } +BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, + NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + BaseType_t ret; + return ret; +} /**************************************************************** * Abstract prvCreateDNSMessage @@ -144,7 +158,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; @@ -160,6 +175,16 @@ void harness() { size_t len; + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + __CPROVER_assume( 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 ); diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 55c199a8d4..949a26dfa5 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -13,6 +13,7 @@ "CBMCFLAGS": [ "--unwind 1", + "--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" @@ -23,12 +24,14 @@ "$(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" ], "DEF": [ + "ipconfigUSE_IPv6=1", "ipconfigDNS_USE_CALLBACKS={callback}", "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" ] From ba95154bd54264ba50247d9b6ed038516fdef694 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 Feb 2023 16:30:52 +0000 Subject: [PATCH 03/26] wip DNSgetHostByName --- .../DNSgetHostByName_cancel_harness.c | 6 +++-- .../ReadNameField/ReadNameField_harness.c | 27 +++++++++---------- 2 files changed, 16 insertions(+), 17 deletions(-) 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 b24685dc73..8536a2612e 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/ReadNameField/ReadNameField_harness.c b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c index 253688a13a..ec236625e8 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,10 +39,8 @@ 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 ); { return 0; } @@ -69,9 +65,10 @@ void harness() size_t uxRemainingBytes; size_t uxDestLen; + ParseSet_t pxSet; - uint8_t * pucByte = malloc( uxRemainingBytes ); - char * pcName = malloc( uxDestLen ); + pxSet.pucByte = malloc( uxRemainingBytes ); + //pxSet.pcRequestedName = malloc( uxDestLen ); /* Preconditions */ @@ -81,8 +78,8 @@ void harness() __CPROVER_assume( uxRemainingBytes <= NETWORK_BUFFER_SIZE ); __CPROVER_assume( uxDestLen <= NAME_SIZE ); - __CPROVER_assume( pucByte != NULL ); - __CPROVER_assume( pcName != NULL ); + __CPROVER_assume( pxSet.pucByte != NULL ); + //__CPROVER_assume( pxSet.pcRequestedName != NULL ); /* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */ /*__CPROVER_assume(uxRemainingBytes > 0); */ @@ -90,9 +87,9 @@ 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 */ From 7d09c1e317d7024331ae41e833e2d30da6ec3bd3 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 9 Feb 2023 09:53:17 +0000 Subject: [PATCH 04/26] wip DNSgetHostByName --- .../DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 8 +++++++- test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 95cc678ab2..2021916432 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -124,9 +124,12 @@ void DNS_CloseSocket( Socket_t xDNSSocket ) Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { - Socket_t sock; + + Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); + __CPROVER_assume(sock != NULL); //TODO: _TJ_: can we assume socket creation always succeed like this? return sock; + } uint32_t FreeRTOS_dnslookup( const char * pcHostName ) @@ -177,6 +180,8 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); + __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? + __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); /* Interface init. */ @@ -193,4 +198,5 @@ void harness() 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 949a26dfa5..068834162b 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -13,6 +13,7 @@ "CBMCFLAGS": [ "--unwind 1", + "--unwindset strchr.0:{HOSTNAME_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}", From c243eee5c4240766d9ec77f81ea82acd0108104f Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 9 Feb 2023 17:08:47 +0000 Subject: [PATCH 05/26] fixed cbmc proof for DNS_ReadNameField --- .../cbmc/proofs/ReadNameField/ReadNameField_harness.c | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c index ec236625e8..e50d6fde30 100644 --- a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c +++ b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c @@ -63,23 +63,20 @@ void harness() "NAME_SIZE >= 4 required for good coverage." ); - size_t uxRemainingBytes; size_t uxDestLen; ParseSet_t pxSet; - pxSet.pucByte = malloc( uxRemainingBytes ); - //pxSet.pcRequestedName = 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( pxSet.pucByte != NULL ); - //__CPROVER_assume( pxSet.pcRequestedName != NULL ); /* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */ /*__CPROVER_assume(uxRemainingBytes > 0); */ @@ -94,6 +91,6 @@ void harness() /* Postconditions */ - __CPROVER_assert( index <= uxDestLen + 1 && index <= uxRemainingBytes, + __CPROVER_assert( index <= uxDestLen + 1 && index <= pxSet.uxSourceBytesRemaining, "DNS_ReadNameField : index <= uxDestLen+1" ); } From ae10fc02e8e51c80e0d8f2e1925dee722c16cd01 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 9 Feb 2023 17:42:12 +0000 Subject: [PATCH 06/26] wip DNSgetHostByName_a_harness --- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 9 ++++++--- test/cbmc/stubs/freertos_api.c | 5 +++-- 2 files changed, 9 insertions(+), 5 deletions(-) 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 bc11904588..1c466e1d2f 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" ); diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index c4e3281e61..7cf227c1b7 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -211,8 +211,9 @@ 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; From f07501f5c5cb8c64ae4c31807a2d53a60bff5189 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 10 Feb 2023 07:31:15 +0000 Subject: [PATCH 07/26] Fix CBMC prooff for DNSgetHostByName --- source/FreeRTOS_DNS.c | 177 +++++++++--------- .../DNSgetHostByName_harness.c | 19 +- .../proofs/DNS/DNSgetHostByName/Makefile.json | 3 +- 3 files changed, 107 insertions(+), 92 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 3b49811063..e881f1aed8 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -621,7 +621,7 @@ if( ulIPAddress != 0UL ) { #if ( ipconfigUSE_IPv6 != 0 ) - if( ( ppxAddressInfo != NULL) && ( *ppxAddressInfo != NULL) && ( *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 ) ); @@ -729,30 +729,27 @@ */ static void prvIncreaseDNS4Index( NetworkEndPoint_t * pxEndPoint ) { - if ( pxEndPoint != NULL) + uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex; + uint8_t ucInitialIndex = ucIndex; + + for( ; ; ) { - uint8_t ucIndex = pxEndPoint->ipv4_settings.ucDNSIndex; - uint8_t ucInitialIndex = ucIndex; + ucIndex++; - for( ; ; ) + if( ucIndex >= ( uint8_t ) ipconfigENDPOINT_DNS_ADDRESS_COUNT ) { - ucIndex++; - - if( ucIndex >= ( uint8_t ) ipconfigENDPOINT_DNS_ADDRESS_COUNT ) - { - ucIndex = 0U; - } - - if( ( pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ] != 0U ) || - ( ucInitialIndex == ucIndex ) ) - { - break; - } + ucIndex = 0U; } - FreeRTOS_printf( ( "prvIncreaseDNS4Index: from %d to %d\n", ( int ) ucInitialIndex, ( int ) ucIndex ) ); - pxEndPoint->ipv4_settings.ucDNSIndex = ucIndex; + if( ( pxEndPoint->ipv4_settings.ulDNSServerAddresses[ ucIndex ] != 0U ) || + ( ucInitialIndex == ucIndex ) ) + { + break; + } } + + FreeRTOS_printf( ( "prvIncreaseDNS4Index: from %d to %d\n", ( int ) ucInitialIndex, ( int ) ucIndex ) ); + pxEndPoint->ipv4_settings.ucDNSIndex = ucIndex; } /*-----------------------------------------------------------*/ @@ -953,10 +950,10 @@ if( ( xDNS_IP_Preference == xPreferenceIPv6 ) && ENDPOINT_IS_IPv6( pxEndPoint ) ) { uint8_t ucIndex = pxEndPoint->ipv6_settings.ucDNSIndex; - uint8_t * ucBytes = &(pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes); + uint8_t * ucBytes = pxEndPoint->ipv6_settings.xDNSServerAddresses[ ucIndex ].ucBytes; /* Test if the DNS entry is in used. */ - if( ( ucBytes ) && ( ucBytes[ 0 ] != 0U ) && ( ucBytes[ 1 ] != 0U ) ) + if( ( ucBytes[ 0 ] != 0U ) && ( ucBytes[ 1 ] != 0U ) ) { pxAddress->sin_family = FREERTOS_AF_INET6; pxAddress->sin_len = ( uint8_t ) sizeof( struct freertos_sockaddr ); @@ -1174,78 +1171,78 @@ pxEndPoint = prvFillSockAddress( &xAddress, pcHostName ); - if( pxEndPoint != NULL && xDNSSocket != NULL) + if( pxEndPoint != NULL ) { do { - // if( xDNSSocket->usLocalPort == 0U ) - // { - // /* Bind the client socket to a random port number. */ - // uint16_t usPort = 0U; - // #if ( ipconfigUSE_MDNS == 1 ) - // if( xAddress.sin_port == FreeRTOS_htons( ipMDNS_PORT ) ) - // { - // /* For a mDNS lookup, bind to the mDNS port 5353. */ - // usPort = FreeRTOS_htons( ipMDNS_PORT ); - // } - // #endif - - // if( DNS_BindSocket( xDNSSocket, usPort ) != 0 ) - // { - // FreeRTOS_printf( ( "DNS bind to %u failed\n", FreeRTOS_ntohs( usPort ) ) ); - // break; - // } - // } - - // uxReturn = prvSendBuffer( pcHostName, - // uxIdentifier, - // xDNSSocket, - // xFamily, - // &xAddress ); - - // if( uxReturn == pdFAIL ) - // { - // break; - // } - - // /* Create the message in the obtained buffer. */ - - // /* receive a dns reply message */ - // xBytes = DNS_ReadReply( xDNSSocket, - // &xRecvAddress, - // &xReceiveBuffer ); - - // if( ( uxReadTimeOut_ticks > 0 ) && - // ( pxEndPoint != NULL ) && - // ( ( xBytes == -pdFREERTOS_ERRNO_EWOULDBLOCK ) || - // ( xBytes == 0 ) ) ) - // { - // /* This search timed out, next time try with a different DNS. */ - // #if ( ipconfigUSE_IPv6 != 0 ) - // if( xAddress.sin_family == FREERTOS_AF_INET6 ) - // { - // prvIncreaseDNS6Index( pxEndPoint ); - // } - // else - // #endif - // { - // prvIncreaseDNS4Index( pxEndPoint ); - // } - // } - - // if( xReceiveBuffer.pucPayloadBuffer != NULL ) - // { - // if( xBytes > 0 ) - // { - // xReceiveBuffer.uxPayloadLength = xBytes; - // ulIPAddress = prvDNSReply( &xReceiveBuffer, ppxAddressInfo, uxIdentifier, xRecvAddress.sin_port ); - // } - - // /* Finished with the buffer. The zero copy interface - // * is being used, so the buffer must be freed by the - // * task. */ - // FreeRTOS_ReleaseUDPPayloadBuffer( xReceiveBuffer.pucPayloadBuffer ); - // } + if( xDNSSocket->usLocalPort == 0U ) + { + /* Bind the client socket to a random port number. */ + uint16_t usPort = 0U; + #if ( ipconfigUSE_MDNS == 1 ) + if( xAddress.sin_port == FreeRTOS_htons( ipMDNS_PORT ) ) + { + /* For a mDNS lookup, bind to the mDNS port 5353. */ + usPort = FreeRTOS_htons( ipMDNS_PORT ); + } + #endif + + if( DNS_BindSocket( xDNSSocket, usPort ) != 0 ) + { + FreeRTOS_printf( ( "DNS bind to %u failed\n", FreeRTOS_ntohs( usPort ) ) ); + break; + } + } + + uxReturn = prvSendBuffer( pcHostName, + uxIdentifier, + xDNSSocket, + xFamily, + &xAddress ); + + if( uxReturn == pdFAIL ) + { + break; + } + + /* Create the message in the obtained buffer. */ + + /* receive a dns reply message */ + xBytes = DNS_ReadReply( xDNSSocket, + &xRecvAddress, + &xReceiveBuffer ); + + if( ( uxReadTimeOut_ticks > 0 ) && + ( pxEndPoint != NULL ) && + ( ( xBytes == -pdFREERTOS_ERRNO_EWOULDBLOCK ) || + ( xBytes == 0 ) ) ) + { + /* This search timed out, next time try with a different DNS. */ + #if ( ipconfigUSE_IPv6 != 0 ) + if( xAddress.sin_family == FREERTOS_AF_INET6 ) + { + prvIncreaseDNS6Index( pxEndPoint ); + } + else + #endif + { + prvIncreaseDNS4Index( pxEndPoint ); + } + } + + if( xReceiveBuffer.pucPayloadBuffer != NULL ) + { + if( xBytes > 0 ) + { + xReceiveBuffer.uxPayloadLength = xBytes; + ulIPAddress = prvDNSReply( &xReceiveBuffer, ppxAddressInfo, uxIdentifier, xRecvAddress.sin_port ); + } + + /* Finished with the buffer. The zero copy interface + * is being used, so the buffer must be freed by the + * task. */ + FreeRTOS_ReleaseUDPPayloadBuffer( xReceiveBuffer.pucPayloadBuffer ); + } } while( ipFALSE_BOOL ); } else diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 2021916432..95dc37df26 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -105,11 +105,12 @@ BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket, BaseType_t ret; int len; + __CPROVER_assume( len > sizeof(DNSMessage_t) && len < CBMC_MAX_OBJECT_SIZE ); + pxDNSBuf->pucPayloadBuffer = safeMalloc( len ); pxDNSBuf->uxPayloadLength = len; - __CPROVER_assume( len < CBMC_MAX_OBJECT_SIZE ); __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL ); __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength ); @@ -170,6 +171,22 @@ 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 ) ); + + __CPROVER_assume( pxNetworkBuffer != NULL ); + + pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + /**************************************************************** * The proof for FreeRTOS_gethostbyname. ****************************************************************/ diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 068834162b..f7dfe746c6 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -14,6 +14,8 @@ [ "--unwind 1", "--unwindset strchr.0:{HOSTNAME_UNWIND}", + "--unwindset prvIncreaseDNS4Index.0:6", + "--unwindset prvIncreaseDNS6Index.0:6", "--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}", @@ -24,7 +26,6 @@ [ "$(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" From fd1690e34c101dc98dc54160fca0460c7bcaef13 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Sun, 12 Feb 2023 10:41:01 +0000 Subject: [PATCH 08/26] wip fix DNSgetHostByName_a CBMC proof --- .../DNSgetHostByName_a_harness.c | 60 ++++++++++++++++++- .../DNS/DNSgetHostByName_a/Makefile.json | 6 +- 2 files changed, 63 insertions(+), 3 deletions(-) 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 1c466e1d2f..578a0a9fd4 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -89,8 +89,52 @@ size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer, void func( const char * pcHostName, void * pvSearchID, - uint32_t ulIPAddress ) + struct freertos_addrinfo * pxAddressInfo ) { + +} + +BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, + NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + 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 ) ); + + __CPROVER_assume( pxNetworkBuffer != NULL ); + + pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) +{ + + Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); + __CPROVER_assume(sock != NULL); //TODO: _TJ_: can we assume socket creation always succeed like this? + + return sock; + +} + +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 ); } /**************************************************************** @@ -101,6 +145,18 @@ void harness() { size_t len; + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? + __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? + __CPROVER_assume( 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 ); @@ -108,7 +164,7 @@ void harness() __CPROVER_assume( pcHostName != NULL ); pcHostName[ len - 1 ] = NULL; - FOnDNSEvent pCallback = func; + FOnDNSEvent pCallback = &func; TickType_t xTimeout; void * pvSearchID; diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index 6d364a58b2..365d407592 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -9,6 +9,10 @@ "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 +20,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" From 241535fc7423af0657ed42fda9f2bfa618f7183e Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 06:42:08 +0000 Subject: [PATCH 09/26] fixed cbmc target func not called issue in DNSclear --- test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c | 2 ++ test/cbmc/proofs/DNS/DNSclear/Makefile.json | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c b/test/cbmc/proofs/DNS/DNSclear/DNSclear_harness.c index 0e73545dd3..440a74fdda 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 05be312667..2f5ccf4ddb 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": [ From 8dac64dd25bb60b9e3d5fb8c22cea2a2b9e88f85 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 07:07:13 +0000 Subject: [PATCH 10/26] fixed cbmc target func not called issue in DNSlookup --- test/cbmc/proofs/DNS/DNSlookup/Makefile.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DNS/DNSlookup/Makefile.json b/test/cbmc/proofs/DNS/DNSlookup/Makefile.json index 103c1ab544..ed8954868c 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": From 88f699f26efc64ab094022c16c67d6794d75013f Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 09:50:20 +0000 Subject: [PATCH 11/26] fix DNSgetHostByName_a CBMC proof --- source/FreeRTOS_DNS.c | 4 ---- 1 file changed, 4 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 5a4aee0727..372c4f9a9c 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; } /*-----------------------------------------------------------*/ From 07e208af5e55ea51f9d3405148fe633ee563fff1 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 16:46:40 +0000 Subject: [PATCH 12/26] update comments --- .../proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 6 +++--- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 7 +++---- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 95dc37df26..a68452a497 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -127,7 +127,7 @@ Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); - __CPROVER_assume(sock != NULL); //TODO: _TJ_: can we assume socket creation always succeed like this? + __CPROVER_assume(sock != NULL); return sock; @@ -197,8 +197,8 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? - __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? + __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy + __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); /* Interface init. */ 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 578a0a9fd4..444eb982a3 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -122,8 +122,7 @@ Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); - __CPROVER_assume(sock != NULL); //TODO: _TJ_: can we assume socket creation always succeed like this? - + __CPROVER_assume(sock != NULL); return sock; } @@ -147,8 +146,8 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? - __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: how to validate this in src? + __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy + __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); /* Interface init. */ From e3d4b4c7dcb940c8f1f56c005f4a74ea591fa439 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 00:31:15 +0530 Subject: [PATCH 13/26] more asserts --- .../cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 2 ++ .../proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 2 ++ 2 files changed, 4 insertions(+) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index a68452a497..1f9ee39cbc 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -147,6 +147,8 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes 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." ); BaseType_t ret; return ret; } 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 444eb982a3..c6d462f8c6 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -98,6 +98,8 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes 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." ); BaseType_t ret; return ret; } From 22e6eb6911ce6c10b5084a4d84c3bf91f5910b56 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 15:28:42 +0530 Subject: [PATCH 14/26] fixing formatting --- source/FreeRTOS_DNS.c | 2 +- .../proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 372c4f9a9c..1129a125ca 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -617,7 +617,7 @@ if( ulIPAddress != 0UL ) { #if ( ipconfigUSE_IPv6 != 0 ) - if( ( ppxAddressInfo != NULL) && ( *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 ) ); diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 1f9ee39cbc..ac50639934 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -105,7 +105,7 @@ BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket, BaseType_t ret; int len; - __CPROVER_assume( len > sizeof(DNSMessage_t) && len < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) ); pxDNSBuf->pucPayloadBuffer = safeMalloc( len ); @@ -127,7 +127,7 @@ Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); - __CPROVER_assume(sock != NULL); + __CPROVER_assume( sock != NULL ); return sock; From 3a9405d90e50ce24b9df990de95db36e19b9c205 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 15:51:00 +0530 Subject: [PATCH 15/26] updating as per review comments --- .../DNSgetHostByName_harness.c | 21 ++++++++++----- .../DNSgetHostByName_a_harness.c | 26 ++++++++++++------- 2 files changed, 32 insertions(+), 15 deletions(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index ac50639934..b0a3d448aa 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -180,12 +180,21 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS { NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) ); - __CPROVER_assume( pxNetworkBuffer != NULL ); - - pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + 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; } 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 c6d462f8c6..c1dbc6a41f 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -111,21 +111,29 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS { NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) ); - __CPROVER_assume( pxNetworkBuffer != NULL ); - - pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + 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 sock = safeMalloc( sizeof(struct xSOCKET) ); - __CPROVER_assume(sock != NULL); - return sock; + Socket_t xSock = safeMalloc( sizeof(struct xSOCKET) ); + return xSock; } From 6e229f98d395ff1e747ee863ba9b1e1d092b3052 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 09:59:11 +0530 Subject: [PATCH 16/26] fix dns after review comments --- .../proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 3 +-- .../proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 3 +++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index b0a3d448aa..42996e5c57 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -127,8 +127,6 @@ Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); - __CPROVER_assume( sock != NULL ); - return sock; } @@ -149,6 +147,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes { __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; } 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 c1dbc6a41f..b3e169f43c 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -100,6 +100,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes { __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; } @@ -144,6 +145,8 @@ uint32_t Prepare_CacheLookup( const char * pcHostName, ( * ppxAddressInfo ) = ( struct freertos_addrinfo * ) malloc( sizeof( struct freertos_addrinfo ) ); __CPROVER_assume( ( * ppxAddressInfo ) != NULL ); __CPROVER_assume( ( * ppxAddressInfo )->ai_next == NULL ); + uint32_t ulRet; + return ulRet; } /**************************************************************** From 45910b34b2624e6fce67d61c442da25920a209a4 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 10:02:53 +0530 Subject: [PATCH 17/26] adding more asserts --- test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 1 + 1 file changed, 1 insertion(+) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 42996e5c57..24a078c2a6 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -121,6 +121,7 @@ BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket, void DNS_CloseSocket( Socket_t xDNSSocket ) { + __CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." ); } Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) From cb85b0cec12a01298e5eedb95fe2c5d42b4445a8 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 10:36:53 +0530 Subject: [PATCH 18/26] adds more asserts --- source/FreeRTOS_DNS.c | 2 ++ .../DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 7 +++++-- test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 9 ++++++--- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 3 +++ test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json | 4 +++- 5 files changed, 19 insertions(+), 6 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 1129a125ca..c330157831 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -946,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. */ @@ -963,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/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 24a078c2a6..71b59d4ce2 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -208,8 +208,11 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy - __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy + + /* 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. */ diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index f7dfe746c6..af4adf29de 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -8,14 +8,16 @@ "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:6", - "--unwindset prvIncreaseDNS6Index.0:6", + "--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}", @@ -35,6 +37,7 @@ [ "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 b3e169f43c..d96a3fb580 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -159,6 +159,9 @@ void harness() 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 ); //TODO: _TJ_: verfiy __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index 365d407592..421858957c 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -5,6 +5,7 @@ # 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": [ @@ -30,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}" ] } From 653c089aeab1cf9a5606f504c66c26abd12b9528 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 15:41:42 +0530 Subject: [PATCH 19/26] minor fix --- test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index af4adf29de..fa786e16b6 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -10,7 +10,7 @@ "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" + "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", "CBMCFLAGS": [ From 3680cacd14c289269c784ce34c2fadbb857b1cbc Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Sat, 18 Feb 2023 00:01:39 +0530 Subject: [PATCH 20/26] fixing comments --- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 d96a3fb580..bfc65c0c55 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -162,8 +162,8 @@ void harness() /* 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 ); //TODO: _TJ_: verfiy - __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); //TODO: _TJ_: verfiy + __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. */ From 93b9c21feff5101772fa9cda414e02693ae9e06e Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Sat, 18 Feb 2023 00:04:16 +0530 Subject: [PATCH 21/26] fixing comments --- test/cbmc/proofs/ReadNameField/ReadNameField_harness.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c index e50d6fde30..706679307c 100644 --- a/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c +++ b/test/cbmc/proofs/ReadNameField/ReadNameField_harness.c @@ -42,6 +42,8 @@ size_t DNS_ReadNameField( ParseSet_t * pxSet, size_t DNS_ReadNameField( ParseSet_t * pxSet, size_t uxDestLen ); { + __CPROVER_assert( pxSet != NULL, + "pxSet shouldnt be NULL" ); return 0; } From d6ebdab0e441da2c6963e881ccba126a2e0b076e Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Sat, 18 Feb 2023 00:10:28 +0530 Subject: [PATCH 22/26] fixing minor issue --- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 bfc65c0c55..562155b971 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -91,7 +91,10 @@ void func( const char * pcHostName, void * pvSearchID, struct freertos_addrinfo * pxAddressInfo ) { - + __CPROVER_assert( pcHostName != NULL, + "Precondition: pcHostName != NULL" ); + __CPROVER_assert( pvSearchID != NULL, + "Precondition: pvSearchID != NULL" ); } BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, @@ -182,6 +185,7 @@ void harness() FOnDNSEvent pCallback = &func; TickType_t xTimeout; void * pvSearchID; + __CPROVER_assume( pvSearchID != NULL ); FreeRTOS_gethostbyname_a( pcHostName, pCallback, pvSearchID, xTimeout ); } From 89955c6c3140a0731f3ba0e2bff22951fb007c16 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 21 Feb 2023 16:08:19 +0530 Subject: [PATCH 23/26] fixing DNS_ReadReply() signature --- source/FreeRTOS_DNS_Networking.c | 2 +- source/include/FreeRTOS_DNS_Networking.h | 2 +- .../proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/source/FreeRTOS_DNS_Networking.c b/source/FreeRTOS_DNS_Networking.c index d99b7c5a58..cbebf718e5 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 902164389b..9b36fdb957 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/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 71b59d4ce2..2c44dff3aa 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -22,7 +22,7 @@ uint32_t FreeRTOS_dnslookup( const char * pcHostName ); Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ); void DNS_CloseSocket( Socket_t xDNSSocket ); -BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket, +BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, struct freertos_sockaddr * xAddress, struct xDNSBuffer * pxDNSBuf ); uint32_t DNS_SendRequest( Socket_t xDNSSocket, @@ -98,7 +98,7 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket, * We stub out this function which returned a dns_buffer filled with random data * ****************************************************************/ -BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket, +BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, struct freertos_sockaddr * xAddress, struct xDNSBuffer * pxDNSBuf ) { From 5661ba2103573722b0b06faccc8143ae138a5f21 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 21 Feb 2023 16:14:58 +0530 Subject: [PATCH 24/26] making code more consistant --- .../proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 2c44dff3aa..8191fc3213 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -122,6 +122,7 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, 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 ) @@ -206,17 +207,17 @@ void harness() { size_t len; - pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( 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 ); + pxNetworkEndPoints->pxNext = NULL; /* Interface init. */ - pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); + pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub; From ff8c4483a5ccda8e6332845c5cf25bfc09e92d0d Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 21 Feb 2023 17:06:43 +0530 Subject: [PATCH 25/26] adding more asserts --- source/FreeRTOS_DNS.c | 2 +- .../DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 239b545e8c..39c09c917d 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -659,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 ) ); 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 562155b971..4ab6d81634 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -95,6 +95,8 @@ void func( const char * pcHostName, "Precondition: pcHostName != NULL" ); __CPROVER_assert( pvSearchID != NULL, "Precondition: pvSearchID != NULL" ); + __CPROVER_assert( pxAddressInfo != NULL, + "Precondition: pxAddressInfo != NULL" ); } BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, @@ -173,8 +175,6 @@ void harness() 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 ); From 7d454ec3f5bf73801c55aa23d732dd8960dfdcd2 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 22 Feb 2023 09:10:43 +0530 Subject: [PATCH 26/26] making code more consistent --- .../DNS/DNSgetHostByName/DNSgetHostByName_harness.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index 8191fc3213..fc72373867 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -107,7 +107,7 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) ); - pxDNSBuf->pucPayloadBuffer = safeMalloc( len ); + pxDNSBuf->pucPayloadBuffer = malloc( len ); pxDNSBuf->uxPayloadLength = len; @@ -128,7 +128,7 @@ void DNS_CloseSocket( Socket_t xDNSSocket ) Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { - Socket_t sock = safeMalloc( sizeof(struct xSOCKET) ); + Socket_t sock = malloc( sizeof(struct xSOCKET) ); return sock; } @@ -207,7 +207,7 @@ void harness() { size_t len; - pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); /* Asserts are added in the src code to make sure ucDNSIndex @@ -217,13 +217,13 @@ void harness() pxNetworkEndPoints->pxNext = NULL; /* Interface init. */ - pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); + 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 );