From a29a5d303379675b8b06ddc11a15cbc327fcabf4 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 13 Jan 2023 17:42:24 +0000 Subject: [PATCH 01/21] 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 6dd6f278455454dfd6ed74f4d5c1681dcf7d4c36 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 Feb 2023 06:54:59 +0000 Subject: [PATCH 02/21] wip --- test/cbmc/patches/FreeRTOSConfig.h | 2 +- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 9 +++++++-- test/cbmc/stubs/freertos_api.c | 3 ++- 3 files changed, 10 insertions(+), 4 deletions(-) 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/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index cd628ff0be..90f252a931 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -75,7 +75,12 @@ BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) void harness() { BaseType_t xReset; - eDHCPState_t eExpectedState; + //eDHCPState_t eExpectedState; + + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); + //pxNetworkEndPoint_Temp->xDHCPData.eExpectedState = eExpectedState; /**************************************************************** * Initialize the counter used to bound the number of times @@ -100,5 +105,5 @@ void harness() __CPROVER_assume( xDHCPSocket != NULL ); } - vDHCPProcess( xReset, eExpectedState ); + vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index c4e3281e61..cf453f6211 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -212,7 +212,8 @@ int32_t FreeRTOS_sendto( Socket_t xSocket, ****************************************************************/ void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks ) + TickType_t xBlockTimeTicks, + uint8_t ucIPType ) { size_t size; From d31cf246be5256dbd6c8005671c9d1509656e3de Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 10 Feb 2023 16:58:44 +0000 Subject: [PATCH 03/21] wip DHCPProcess --- source/FreeRTOS_DHCP.c | 4 ++-- .../proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 14 +++++++++++++- .../cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 1 + 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index b40b026f4c..ff056d9be5 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -128,7 +128,7 @@ */ static void prvCloseDHCPSocket( NetworkEndPoint_t * pxEndPoint ); - static void vDHCPProcessEndPoint( BaseType_t xReset, + void vDHCPProcessEndPoint( BaseType_t xReset, BaseType_t xDoCheck, NetworkEndPoint_t * pxEndPoint ); @@ -650,7 +650,7 @@ * @param[in] pxEndPoint: The end-point for which the DHCP state machine should * make one cycle. */ - static void vDHCPProcessEndPoint( BaseType_t xReset, + void vDHCPProcessEndPoint( BaseType_t xReset, BaseType_t xDoCheck, NetworkEndPoint_t * pxEndPoint ) { diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 90f252a931..3abb57162f 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -75,8 +75,17 @@ BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) void harness() { BaseType_t xReset; + BaseType_t xDoCheck; //eDHCPState_t eExpectedState; + 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 ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); @@ -105,5 +114,8 @@ void harness() __CPROVER_assume( xDHCPSocket != NULL ); } - vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); + //vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); + + vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 55c199a8d4..81ef8aacc2 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -24,6 +24,7 @@ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], From 1afeb4ab99c140d35364d7c51e1100696f3083c8 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Sat, 11 Feb 2023 05:33:19 +0000 Subject: [PATCH 04/21] wip dhcp process --- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 4 ++-- test/cbmc/proofs/MakefileCommon.json | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 3abb57162f..74baadd6eb 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -114,8 +114,8 @@ void harness() __CPROVER_assume( xDHCPSocket != NULL ); } - //vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); + vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); - vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + //vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json index ace4a5c352..7bc6bc03dd 100644 --- a/test/cbmc/proofs/MakefileCommon.json +++ b/test/cbmc/proofs/MakefileCommon.json @@ -31,7 +31,7 @@ ], "CBMCFLAGS ": [ - "--object-bits 7", + "--object-bits 9", "--32", "--bounds-check", "--pointer-check" From 8c930df6e56eb71c59f165434240864531e5c815 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 04:28:57 +0000 Subject: [PATCH 05/21] wip --- source/FreeRTOS_DHCP.c | 22 +- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 414 +++++++++++++++++- .../proofs/DHCP/DHCPProcess/Makefile.json | 1 - 3 files changed, 422 insertions(+), 15 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index ff056d9be5..b4351306d8 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -286,7 +286,7 @@ /* PAss the address of a pointer pucUDPPayload, because zero-copy is used. */ lBytes = FreeRTOS_recvfrom( xDHCPv4Socket, &( pucUDPPayload ), 0, FREERTOS_ZERO_COPY, NULL, NULL ); - if( lBytes > 0 ) + if( lBytes > 0 && pucUDPPayload != NULL ) { /* Remove it now, destination not found. */ FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); @@ -1316,8 +1316,10 @@ } } } - - FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); + if (pucUDPPayload != NULL) + { + FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); + } } /* if( lBytes > 0 ) */ return xReturn; @@ -1478,7 +1480,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( pucUDPPayloadBuffer != NULL ) + if( xDHCPv4Socket != FREERTOS_INVALID_SOCKET && xDHCPv4Socket != NULL && pucUDPPayloadBuffer != NULL ) { /* Copy in the IP address being requested. */ @@ -1505,7 +1507,10 @@ { /* The packet was not successfully queued for sending and must be * returned to the stack. */ - FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); + if (pucUDPPayloadBuffer != NULL) + { + FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); + } } else { @@ -1547,7 +1552,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( pucUDPPayloadBuffer != NULL ) + if( xDHCPv4Socket != FREERTOS_INVALID_SOCKET && xDHCPv4Socket != NULL && pucUDPPayloadBuffer != NULL ) { const void * pvCopySource; void * pvCopyDest; @@ -1587,7 +1592,10 @@ { /* The packet was not successfully queued for sending and must be * returned to the stack. */ - FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); + if (pucUDPPayloadBuffer != NULL) + { + FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); + } } else { diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 74baadd6eb..c3d648d0cd 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -42,15 +42,414 @@ #include "FreeRTOS_DHCP.h" #include "FreeRTOS_ARP.h" +#include "NetworkBufferManagement.h" + +#include "cbmc.h" + /* Static members defined in FreeRTOS_DHCP.c */ extern DHCPData_t xDHCPData; -extern Socket_t xDHCPSocket; -void prvCreateDHCPSocket(); +extern Socket_t xDHCPv4Socket; +void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint ); /* Static member defined in freertos_api.c */ #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND extern uint32_t GetNetworkBuffer_failure_count; #endif + + + + + + + + + + + + + + + +/**************************************************************** +* This is a collection of abstractions of methods in the FreeRTOS TCP +* API. The abstractions simply perform minimal validation of +* function arguments, and return unconstrained values of the +* appropriate type. +****************************************************************/ + +/**************************************************************** +* Abstract FreeRTOS_socket. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/socket.html +* +* We stub out this function to do nothing but allocate space for a +* socket containing unconstrained data or return an error. +****************************************************************/ + +Socket_t FreeRTOS_socket( BaseType_t xDomain, + BaseType_t xType, + BaseType_t xProtocol ) +{ + // if( nondet_bool() ) + // { + // return FREERTOS_INVALID_SOCKET; + // } + // else + // { + void * ptr = malloc( sizeof( struct xSOCKET ) ); + __CPROVER_assume( ptr != NULL ); + return ptr; + // } +} + +/**************************************************************** +* Abstract FreeRTOS_setsockopt. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html +****************************************************************/ + +BaseType_t FreeRTOS_setsockopt( Socket_t xSocket, + int32_t lLevel, + int32_t lOptionName, + const void * pvOptionValue, + size_t uxOptionLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pvOptionValue != NULL, + "FreeRTOS precondition: pvOptionValue != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** +* Abstract FreeRTOS_closesocket. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/close.html +****************************************************************/ + +BaseType_t FreeRTOS_closesocket( Socket_t xSocket ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** +* Abstract FreeRTOS_bind. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/bind.html +****************************************************************/ + +BaseType_t FreeRTOS_bind( Socket_t xSocket, + struct freertos_sockaddr * pxAddress, + socklen_t xAddressLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pxAddress != NULL, + "FreeRTOS precondition: pxAddress != NULL" ); + return nondet_BaseType(); +} + +/**************************************************************** +* Abstract FreeRTOS_inet_addr. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/inet_addr.html +****************************************************************/ + +uint32_t FreeRTOS_inet_addr( const char * pcIPAddress ) +{ + __CPROVER_assert( pcIPAddress != NULL, + "FreeRTOS precondition: pcIPAddress != NULL" ); + return nondet_uint32(); +} + +/**************************************************************** +* Abstract FreeRTOS_recvfrom. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/recvfrom.html +* +* We stub out this function to do nothing but allocate a buffer of +* unconstrained size containing unconstrained data and return the +* size (or return the size 0 if the allocation fails). +****************************************************************/ + +int32_t FreeRTOS_recvfrom( Socket_t xSocket, + void * pvBuffer, + size_t uxBufferLength, + BaseType_t xFlags, + struct freertos_sockaddr * pxSourceAddress, + socklen_t * pxSourceAddressLength ) + +{ + /**************************************************************** + * "If the zero copy calling semantics are used (the ulFlags + * parameter does not have the FREERTOS_ZERO_COPY bit set) then + * pvBuffer does not point to a buffer and xBufferLength is not + * used." This is from the documentation. + ****************************************************************/ + __CPROVER_assert( xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY" ); + + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + + /**************************************************************** + * TODO: We need to check this out. + * + * The code calls recvfrom with these parameters NULL, it is not + * clear from the documentation that this is allowed. + ****************************************************************/ + #if 0 + __CPROVER_assert( pxSourceAddress != NULL, + "FreeRTOS precondition: pxSourceAddress != NULL" ); + __CPROVER_assert( pxSourceAddressLength != NULL, + "FreeRTOS precondition: pxSourceAddress != NULL" ); + #endif + + size_t payload_size; + __CPROVER_assume( payload_size + sizeof( UDPPacket_t ) + < CBMC_MAX_OBJECT_SIZE ); + + /**************************************************************** + * TODO: We need to make this lower bound explicit in the Makefile.json + * + * DNSMessage_t is a typedef in FreeRTOS_DNS.c + * sizeof(DNSMessage_t) = 6 * sizeof(uint16_t) + ****************************************************************/ + __CPROVER_assume( payload_size >= 6 * sizeof( uint16_t ) ); + + #ifdef CBMC_FREERTOS_RECVFROM_BUFFER_BOUND + __CPROVER_assume( payload_size <= CBMC_FREERTOS_RECVFROM_BUFFER_BOUND ); + #endif + + uint32_t buffer_size = payload_size + sizeof( UDPPacket_t ); + uint8_t * buffer = safeMalloc( buffer_size ); + + if( buffer == NULL ) + { + buffer_size = 0; + } + else + { + buffer = buffer + sizeof( UDPPacket_t ); + buffer_size = buffer_size - sizeof( UDPPacket_t ); + } + + *( ( uint8_t ** ) pvBuffer ) = buffer; + return buffer_size; +} + +/**************************************************************** +* Abstract FreeRTOS_recvfrom. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/sendto.html +****************************************************************/ + +int32_t FreeRTOS_sendto( Socket_t xSocket, + const void * pvBuffer, + size_t uxTotalDataLength, + BaseType_t xFlags, + const struct freertos_sockaddr * pxDestinationAddress, + socklen_t xDestinationAddressLength ) +{ + __CPROVER_assert( xSocket != NULL, + "FreeRTOS precondition: xSocket != NULL" ); + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + __CPROVER_assert( pxDestinationAddress != NULL, + "FreeRTOS precondition: pxDestinationAddress != NULL" ); + return nondet_int32(); +} + +/**************************************************************** +* Abstract FreeRTOS_GetUDPPayloadBuffer +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/FreeRTOS_GetUDPPayloadBuffer.html +* +* We stub out this function to do nothing but allocate a buffer of +* unconstrained size containing unconstrained data and return a +* pointer to the buffer (or NULL). +****************************************************************/ + +void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, + TickType_t xBlockTimeTicks, + uint8_t ucIPType ) +{ + size_t size; + + __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( size >= sizeof( UDPPacket_t ) ); + + uint8_t * buffer = safeMalloc( size ); + + return buffer == NULL ? buffer : buffer + sizeof( UDPPacket_t ); +} + +/**************************************************************** +* Abstract FreeRTOS_GetUDPPayloadBuffer +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html +****************************************************************/ + +void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); + __CPROVER_assert( __CPROVER_POINTER_OFFSET( pvBuffer ) + == sizeof( UDPPacket_t ), + "FreeRTOS precondition: pvBuffer offset" ); + + free( pvBuffer - sizeof( UDPPacket_t ) ); +} + +/*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 = ( malloc( ( ( uint8_t * ) xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipIP_TYPE_OFFSET ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +/**************************************************************** +* Abstract pxGetNetworkBufferWithDescriptor. +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vReleaseNetworkBufferAndDescriptor.html +****************************************************************/ + +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + if( pxNetworkBuffer->pucEthernetBuffer != NULL ) + { + free( pxNetworkBuffer->pucEthernetBuffer ); + } + + free( pxNetworkBuffer ); +} + +/**************************************************************** +* Abstract FreeRTOS_GetAddressConfiguration +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_GetAddressConfiguration.html +****************************************************************/ + +void FreeRTOS_GetAddressConfiguration( uint32_t * pulIPAddress, + uint32_t * pulNetMask, + uint32_t * pulGatewayAddress, + uint32_t * pulDNSServerAddress ) +{ + if( pulIPAddress != NULL ) + { + *pulIPAddress = nondet_unint32(); + } + + if( pulNetMask != NULL ) + { + *pulNetMask = nondet_unint32(); + } + + if( pulGatewayAddress != NULL ) + { + *pulGatewayAddress = nondet_unint32(); + } + + if( pulDNSServerAddress != NULL ) + { + *pulDNSServerAddress = nondet_unint32(); + } +} + +/****************************************************************/ + +/**************************************************************** +* This is a collection of methods that are defined by the user +* application but are invoked by the FreeRTOS API. +****************************************************************/ + +/**************************************************************** +* Abstract FreeRTOS_GetAddressConfiguration +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vApplicationIPNetworkEventHook.html +****************************************************************/ + +void vApplicationIPNetworkEventHook( eIPCallbackEvent_t eNetworkEvent ) +{ +} + +/**************************************************************** +* Abstract pcApplicationHostnameHook +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html +****************************************************************/ + +const char * pcApplicationHostnameHook( void ) +{ + return "hostname"; +} + +/****************************************************************/ + + +/**************************************************************** +* Abstract xNetworkInterfaceOutput +* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html#xNetworkInterfaceOutput +****************************************************************/ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t bReleaseAfterSend ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "The networkbuffer cannot be NULL" ); + + BaseType_t xReturn; + + /* Return some random value. */ + return xReturn; +} + +/****************************************************************/ + +/** + * @brief Internal version of bind() that should not be called directly. + * 'xInternal' is used for TCP sockets only: it allows to have several + * (connected) child sockets bound to the same server port. + * + * @param[in] pxSocket: The socket is to be bound. + * @param[in] pxBindAddress: The port to which this socket should be bound. + * @param[in] uxAddressLength: The address length. + * @param[in] xInternal: pdTRUE is calling internally, else pdFALSE. + * + * @return If the socket was bound to a port successfully, then a 0 is returned. + * Or else, an error code is returned. + */ +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + + BaseType_t ret; + __CPROVER_assume( ret == 0 ); + return ret; + +} + + + + + + + + + + + + + + + + + + + + + + /**************************************************************** * The signature of the function under test. @@ -107,15 +506,16 @@ void harness() * xReset==True resets the state to eWaitingSendFirstDiscover. ****************************************************************/ - if( !( ( xDHCPData.eDHCPState == eInitialWait ) || + if( !( ( pxNetworkEndPoint_Temp->xDHCPData.eDHCPState == eInitialWait ) || ( xReset != pdFALSE ) ) ) { - prvCreateDHCPSocket(); - __CPROVER_assume( xDHCPSocket != NULL ); + prvCreateDHCPSocket( pxNetworkEndPoint_Temp ); + } - vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); + __CPROVER_assume( xDHCPv4Socket != NULL ); + //vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); - //vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 5fcd044318..e36f447401 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -41,7 +41,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_DHCP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" From df8661ad3a8eee4979dcb0120587953db5ac0326 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 05:54:40 +0000 Subject: [PATCH 06/21] fix CBMC ProcessDHCPReplies proofs --- test/cbmc/proofs/ProcessDHCPReplies/Makefile.json | 2 ++ .../ProcessDHCPReplies/ProcessDHCPReplies_harness.c | 9 +++++++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json index 1fa2aa6888..694fe02e7d 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json +++ b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json @@ -26,6 +26,8 @@ "CBMCFLAGS": [ # "--nondet-static", "--unwind 1", + "--unwindset vProcessHandleOption.0:6", + "--unwindset vProcessHandleOption.1:6", "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" ], diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c index 99e94dd3fd..4eee6a5370 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c +++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -19,7 +19,8 @@ * Signature of function under test ****************************************************************/ -BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ); +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + NetworkEndPoint_t * pxEndPoint ); /**************************************************************** * The proof for FreeRTOS_gethostbyname. @@ -33,5 +34,9 @@ void harness() BaseType_t xExpectedMessageType; - prvProcessDHCPReplies( xExpectedMessageType ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); + + prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); } From 76bdc7cb6b885e004ebec361e7353f05db786f14 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 18:06:51 +0000 Subject: [PATCH 07/21] wip DHCPProcess --- source/FreeRTOS_DHCP.c | 4 +- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 406 +----------------- .../proofs/DHCP/DHCPProcess/Makefile.json | 1 + test/cbmc/stubs/freertos_api.c | 2 +- 4 files changed, 19 insertions(+), 394 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index b4351306d8..1625447028 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -94,7 +94,7 @@ /* * Interpret message received on the DHCP socket. */ - static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ); /* @@ -1224,7 +1224,7 @@ * * @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise. */ - static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ) { uint8_t * pucUDPPayload; diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index c3d648d0cd..5de249b9ee 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -59,414 +59,35 @@ void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint ); - - - - - - - - - - - -/**************************************************************** -* This is a collection of abstractions of methods in the FreeRTOS TCP -* API. The abstractions simply perform minimal validation of -* function arguments, and return unconstrained values of the -* appropriate type. -****************************************************************/ - -/**************************************************************** -* Abstract FreeRTOS_socket. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/socket.html -* -* We stub out this function to do nothing but allocate space for a -* socket containing unconstrained data or return an error. -****************************************************************/ - -Socket_t FreeRTOS_socket( BaseType_t xDomain, - BaseType_t xType, - BaseType_t xProtocol ) -{ - // if( nondet_bool() ) - // { - // return FREERTOS_INVALID_SOCKET; - // } - // else - // { - void * ptr = malloc( sizeof( struct xSOCKET ) ); - __CPROVER_assume( ptr != NULL ); - return ptr; - // } -} - -/**************************************************************** -* Abstract FreeRTOS_setsockopt. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html -****************************************************************/ - -BaseType_t FreeRTOS_setsockopt( Socket_t xSocket, - int32_t lLevel, - int32_t lOptionName, - const void * pvOptionValue, - size_t uxOptionLength ) -{ - __CPROVER_assert( xSocket != NULL, - "FreeRTOS precondition: xSocket != NULL" ); - __CPROVER_assert( pvOptionValue != NULL, - "FreeRTOS precondition: pvOptionValue != NULL" ); - return nondet_BaseType(); -} - /**************************************************************** -* Abstract FreeRTOS_closesocket. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/close.html +* The signature of the function under test. ****************************************************************/ -BaseType_t FreeRTOS_closesocket( Socket_t xSocket ) -{ - __CPROVER_assert( xSocket != NULL, - "FreeRTOS precondition: xSocket != NULL" ); - return nondet_BaseType(); -} +void vDHCPProcess( BaseType_t xReset, + struct xNetworkEndPoint * pxEndPoint ); /**************************************************************** -* Abstract FreeRTOS_bind. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/bind.html +* Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies. ****************************************************************/ -BaseType_t FreeRTOS_bind( Socket_t xSocket, - struct freertos_sockaddr * pxAddress, - socklen_t xAddressLength ) +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + NetworkEndPoint_t * pxEndPoint ) { - __CPROVER_assert( xSocket != NULL, - "FreeRTOS precondition: xSocket != NULL" ); - __CPROVER_assert( pxAddress != NULL, - "FreeRTOS precondition: pxAddress != NULL" ); return nondet_BaseType(); } -/**************************************************************** -* Abstract FreeRTOS_inet_addr. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/inet_addr.html -****************************************************************/ - -uint32_t FreeRTOS_inet_addr( const char * pcIPAddress ) -{ - __CPROVER_assert( pcIPAddress != NULL, - "FreeRTOS precondition: pcIPAddress != NULL" ); - return nondet_uint32(); -} - -/**************************************************************** -* Abstract FreeRTOS_recvfrom. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/recvfrom.html -* -* We stub out this function to do nothing but allocate a buffer of -* unconstrained size containing unconstrained data and return the -* size (or return the size 0 if the allocation fails). -****************************************************************/ - -int32_t FreeRTOS_recvfrom( Socket_t xSocket, - void * pvBuffer, - size_t uxBufferLength, - BaseType_t xFlags, - struct freertos_sockaddr * pxSourceAddress, - socklen_t * pxSourceAddressLength ) - -{ - /**************************************************************** - * "If the zero copy calling semantics are used (the ulFlags - * parameter does not have the FREERTOS_ZERO_COPY bit set) then - * pvBuffer does not point to a buffer and xBufferLength is not - * used." This is from the documentation. - ****************************************************************/ - __CPROVER_assert( xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY" ); - - __CPROVER_assert( pvBuffer != NULL, - "FreeRTOS precondition: pvBuffer != NULL" ); - - /**************************************************************** - * TODO: We need to check this out. - * - * The code calls recvfrom with these parameters NULL, it is not - * clear from the documentation that this is allowed. - ****************************************************************/ - #if 0 - __CPROVER_assert( pxSourceAddress != NULL, - "FreeRTOS precondition: pxSourceAddress != NULL" ); - __CPROVER_assert( pxSourceAddressLength != NULL, - "FreeRTOS precondition: pxSourceAddress != NULL" ); - #endif - - size_t payload_size; - __CPROVER_assume( payload_size + sizeof( UDPPacket_t ) - < CBMC_MAX_OBJECT_SIZE ); - - /**************************************************************** - * TODO: We need to make this lower bound explicit in the Makefile.json - * - * DNSMessage_t is a typedef in FreeRTOS_DNS.c - * sizeof(DNSMessage_t) = 6 * sizeof(uint16_t) - ****************************************************************/ - __CPROVER_assume( payload_size >= 6 * sizeof( uint16_t ) ); - - #ifdef CBMC_FREERTOS_RECVFROM_BUFFER_BOUND - __CPROVER_assume( payload_size <= CBMC_FREERTOS_RECVFROM_BUFFER_BOUND ); - #endif - - uint32_t buffer_size = payload_size + sizeof( UDPPacket_t ); - uint8_t * buffer = safeMalloc( buffer_size ); - - if( buffer == NULL ) - { - buffer_size = 0; - } - else - { - buffer = buffer + sizeof( UDPPacket_t ); - buffer_size = buffer_size - sizeof( UDPPacket_t ); - } - - *( ( uint8_t ** ) pvBuffer ) = buffer; - return buffer_size; -} - -/**************************************************************** -* Abstract FreeRTOS_recvfrom. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/sendto.html -****************************************************************/ - -int32_t FreeRTOS_sendto( Socket_t xSocket, - const void * pvBuffer, - size_t uxTotalDataLength, - BaseType_t xFlags, - const struct freertos_sockaddr * pxDestinationAddress, - socklen_t xDestinationAddressLength ) -{ - __CPROVER_assert( xSocket != NULL, - "FreeRTOS precondition: xSocket != NULL" ); - __CPROVER_assert( pvBuffer != NULL, - "FreeRTOS precondition: pvBuffer != NULL" ); - __CPROVER_assert( pxDestinationAddress != NULL, - "FreeRTOS precondition: pxDestinationAddress != NULL" ); - return nondet_int32(); -} - -/**************************************************************** -* Abstract FreeRTOS_GetUDPPayloadBuffer -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/FreeRTOS_GetUDPPayloadBuffer.html -* -* We stub out this function to do nothing but allocate a buffer of -* unconstrained size containing unconstrained data and return a -* pointer to the buffer (or NULL). -****************************************************************/ - -void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks, - uint8_t ucIPType ) -{ - size_t size; - - __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); - __CPROVER_assume( size >= sizeof( UDPPacket_t ) ); - - uint8_t * buffer = safeMalloc( size ); - - return buffer == NULL ? buffer : buffer + sizeof( UDPPacket_t ); -} - -/**************************************************************** -* Abstract FreeRTOS_GetUDPPayloadBuffer -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html -****************************************************************/ - -void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) -{ - __CPROVER_assert( pvBuffer != NULL, - "FreeRTOS precondition: pvBuffer != NULL" ); - __CPROVER_assert( __CPROVER_POINTER_OFFSET( pvBuffer ) - == sizeof( UDPPacket_t ), - "FreeRTOS precondition: pvBuffer offset" ); - - free( pvBuffer - sizeof( UDPPacket_t ) ); -} - -/*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 = ( malloc( ( ( uint8_t * ) xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipIP_TYPE_OFFSET ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; - return pxNetworkBuffer; -} - -/**************************************************************** -* Abstract pxGetNetworkBufferWithDescriptor. -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vReleaseNetworkBufferAndDescriptor.html -****************************************************************/ - -void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) -{ - __CPROVER_assert( pxNetworkBuffer != NULL, - "Precondition: pxNetworkBuffer != NULL" ); - - if( pxNetworkBuffer->pucEthernetBuffer != NULL ) - { - free( pxNetworkBuffer->pucEthernetBuffer ); - } - - free( pxNetworkBuffer ); -} - -/**************************************************************** -* Abstract FreeRTOS_GetAddressConfiguration -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_GetAddressConfiguration.html -****************************************************************/ - -void FreeRTOS_GetAddressConfiguration( uint32_t * pulIPAddress, - uint32_t * pulNetMask, - uint32_t * pulGatewayAddress, - uint32_t * pulDNSServerAddress ) -{ - if( pulIPAddress != NULL ) - { - *pulIPAddress = nondet_unint32(); - } - - if( pulNetMask != NULL ) - { - *pulNetMask = nondet_unint32(); - } - - if( pulGatewayAddress != NULL ) - { - *pulGatewayAddress = nondet_unint32(); - } - - if( pulDNSServerAddress != NULL ) - { - *pulDNSServerAddress = nondet_unint32(); - } -} - -/****************************************************************/ - -/**************************************************************** -* This is a collection of methods that are defined by the user -* application but are invoked by the FreeRTOS API. -****************************************************************/ - -/**************************************************************** -* Abstract FreeRTOS_GetAddressConfiguration -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vApplicationIPNetworkEventHook.html -****************************************************************/ - -void vApplicationIPNetworkEventHook( eIPCallbackEvent_t eNetworkEvent ) -{ -} - -/**************************************************************** -* Abstract pcApplicationHostnameHook -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html -****************************************************************/ - -const char * pcApplicationHostnameHook( void ) +BaseType_t xSocketValid( const ConstSocket_t xSocket ) { - return "hostname"; + return pdTRUE; } -/****************************************************************/ - - -/**************************************************************** -* Abstract xNetworkInterfaceOutput -* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html#xNetworkInterfaceOutput -****************************************************************/ -BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkBuffer, - BaseType_t bReleaseAfterSend ) -{ - __CPROVER_assert( pxNetworkBuffer != NULL, "The networkbuffer cannot be NULL" ); - - BaseType_t xReturn; - - /* Return some random value. */ - return xReturn; -} - -/****************************************************************/ - -/** - * @brief Internal version of bind() that should not be called directly. - * 'xInternal' is used for TCP sockets only: it allows to have several - * (connected) child sockets bound to the same server port. - * - * @param[in] pxSocket: The socket is to be bound. - * @param[in] pxBindAddress: The port to which this socket should be bound. - * @param[in] uxAddressLength: The address length. - * @param[in] xInternal: pdTRUE is calling internally, else pdFALSE. - * - * @return If the socket was bound to a port successfully, then a 0 is returned. - * Or else, an error code is returned. - */ BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, struct freertos_sockaddr * pxBindAddress, size_t uxAddressLength, - BaseType_t xInternal ) + BaseType_t xInternal ) { - - BaseType_t ret; - __CPROVER_assume( ret == 0 ); - return ret; - + return 0; } - - - - - - - - - - - - - - - - - - - - - - - -/**************************************************************** -* The signature of the function under test. -****************************************************************/ - -void vDHCPProcess( BaseType_t xReset, - eDHCPState_t eExpectedState ); - -/**************************************************************** -* Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies. -****************************************************************/ - -BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) -{ - return nondet_BaseType(); -} - /**************************************************************** * The proof of vDHCPProcess ****************************************************************/ @@ -514,8 +135,11 @@ void harness() } __CPROVER_assume( xDHCPv4Socket != NULL ); - //vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); - vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + xDHCPv4Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP ); + + vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); + + //vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index e36f447401..5fcd044318 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -41,6 +41,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_DHCP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index cf453f6211..9290a0e024 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -43,7 +43,7 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, } else { - void * ptr = malloc( sizeof( Socket_t ) ); + void * ptr = malloc( sizeof( struct xSOCKET ) ); __CPROVER_assume( ptr != NULL ); return ptr; } From 73260076abfc379e9eaccc4ef9e769083a0d190d Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 09:40:13 +0000 Subject: [PATCH 08/21] fix DHCPProcess CBMC proof --- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 38 +++++++++++++++++-- 1 file changed, 35 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 5de249b9ee..61c746ca91 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -88,6 +88,40 @@ BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, { return 0; } + + +/*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 ); + __CPROVER_assume( xRequestedSizeBytes > (dhcpFIRST_OPTION_BYTE_OFFSET + sizeof( MACAddress_t ) + ipIP_TYPE_OFFSET) ); + + pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ( ipIP_TYPE_OFFSET) )) + ipIP_TYPE_OFFSET; + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); +} + +/* CALLED BY FREERTOS + * Hook to return a human-readable name */ +const char * pcApplicationHostnameHook( void ) +{ + const char * name; + + name = "hostname"; + return name; +} /**************************************************************** * The proof of vDHCPProcess ****************************************************************/ @@ -138,8 +172,6 @@ void harness() xDHCPv4Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP ); - vDHCPProcess( xReset, pxNetworkEndPoint_Temp ); - - //vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); } From 973ce0ca2fb82b346fd7705796118f062632d830 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 09:45:25 +0000 Subject: [PATCH 09/21] fix DHCPProcess CBMC proof --- test/cbmc/proofs/MakefileCommon.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json index 7bc6bc03dd..7ada3e1dca 100644 --- a/test/cbmc/proofs/MakefileCommon.json +++ b/test/cbmc/proofs/MakefileCommon.json @@ -31,7 +31,7 @@ ], "CBMCFLAGS ": [ - "--object-bits 9", + "--object-bits 8", "--32", "--bounds-check", "--pointer-check" From ea47d730230a4dbb5717290ce238d873a9a282b9 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 16:38:00 +0000 Subject: [PATCH 10/21] added multiple end point --- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 61c746ca91..3d8606b083 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -134,11 +134,16 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); + pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); + __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL ); /* Interface init. */ pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); + pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface; + __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); From 1b25fbf068fabf92272b23a5a8da7e017ab0519e Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 18:27:11 +0000 Subject: [PATCH 11/21] fix ProcessDHCPReplies --- source/FreeRTOS_DHCP.c | 4 ++-- test/cbmc/proofs/ProcessDHCPReplies/Makefile.json | 11 +++++++---- .../ProcessDHCPReplies/ProcessDHCPReplies_harness.c | 4 ++-- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index 1625447028..b4351306d8 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -94,7 +94,7 @@ /* * Interpret message received on the DHCP socket. */ - _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ); /* @@ -1224,7 +1224,7 @@ * * @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise. */ - _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, + static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ) { uint8_t * pucUDPPayload; diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json index 694fe02e7d..7ad6132c43 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json +++ b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json @@ -26,11 +26,14 @@ "CBMCFLAGS": [ # "--nondet-static", "--unwind 1", - "--unwindset vProcessHandleOption.0:6", - "--unwindset vProcessHandleOption.1:6", - "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:6", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:6", + "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + ], + "OPT": + [ + "--export-file-local-symbols" ], - "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c index 4eee6a5370..7cb0f992df 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c +++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -19,7 +19,7 @@ * Signature of function under test ****************************************************************/ -BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, +BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ); /**************************************************************** @@ -38,5 +38,5 @@ void harness() __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); - prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); + __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); } From 5458be3aa1d67bee81b554a93f8fd006773929f6 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 15 Feb 2023 15:02:50 +0530 Subject: [PATCH 12/21] fix function sign. --- source/FreeRTOS_DHCP.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index 1b9b69b2e5..4397508359 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -128,7 +128,7 @@ */ static void prvCloseDHCPSocket( NetworkEndPoint_t * pxEndPoint ); - void vDHCPProcessEndPoint( BaseType_t xReset, + static void vDHCPProcessEndPoint( BaseType_t xReset, BaseType_t xDoCheck, NetworkEndPoint_t * pxEndPoint ); @@ -651,7 +651,7 @@ * @param[in] pxEndPoint: The end-point for which the DHCP state machine should * make one cycle. */ - void vDHCPProcessEndPoint( BaseType_t xReset, + static void vDHCPProcessEndPoint( BaseType_t xReset, BaseType_t xDoCheck, NetworkEndPoint_t * pxEndPoint ) { From 1b0e67ced5dae26cf2b4f1a834949a7997f57610 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 15 Feb 2023 16:40:39 +0530 Subject: [PATCH 13/21] fix DHCP CBMC proofs --- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 9 +++++---- test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 17 +++++++++++++++-- .../proofs/ProcessDHCPReplies/Makefile.json | 11 +++++++---- 3 files changed, 27 insertions(+), 10 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 3d8606b083..5c71c04129 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -63,14 +63,15 @@ void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint ); * The signature of the function under test. ****************************************************************/ -void vDHCPProcess( BaseType_t xReset, - struct xNetworkEndPoint * pxEndPoint ); +void __CPROVER_file_local_FreeRTOS_DHCP_c_vDHCPProcessEndPoint( BaseType_t xReset, + BaseType_t xDoCheck, + NetworkEndPoint_t * pxEndPoint ); /**************************************************************** * Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies. ****************************************************************/ -BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType, +BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType, NetworkEndPoint_t * pxEndPoint ) { return nondet_BaseType(); @@ -177,6 +178,6 @@ void harness() xDHCPv4Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP ); - vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); + __CPROVER_file_local_FreeRTOS_DHCP_c_vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 5fcd044318..813c4bfc98 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -31,12 +31,24 @@ # Minimal buffer size for maximum coverage, see harness for details. "BUFFER_SIZE": 299, + "ENDPOINT_DNS_ADDRESS_COUNT": 5, # The number of times GetNetworkBufferWithDescriptor can be allowed to fail # (plus 1). "FAILURE_BOUND": 2, + "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", - "CBMCFLAGS": "--unwind 4 --unwindset strlen.0:11,memcmp.0:7,prvProcessDHCPReplies.0:8,prvCreatePartDHCPMessage.0:{FAILURE_BOUND} --nondet-static --flush", + "CBMCFLAGS": [ + "--unwind 4", + "--unwindset strlen.0:11,memcmp.0:7", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--nondet-static --flush" + ], + "OPT": + [ + "--export-file-local-symbols" + ], "OBJS": [ "$(ENTRY)_harness.goto", @@ -51,6 +63,7 @@ [ "BUFFER_SIZE={BUFFER_SIZE}", "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", - "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}", + "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ] } diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json index 7ad6132c43..09d5c8d4e5 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json +++ b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json @@ -10,6 +10,7 @@ # Buffer header: sizeof(DHCPMessage_t) = 241 # Buffer header: sizeof(DHCPMessage_IPv4_t) = 240 "BUFFER_HEADER": 240, + "ENDPOINT_DNS_ADDRESS_COUNT": 5, ################################################################ # Buffer size @@ -20,19 +21,20 @@ ################################################################ # Buffer payload "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 1", + "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", ################################################################ "CBMCFLAGS": [ # "--nondet-static", "--unwind 1", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:6", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:6", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" ], "OPT": [ - "--export-file-local-symbols" + "--export-file-local-symbols" ], "OBJS": [ @@ -48,6 +50,7 @@ "DEF": [ "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}", - "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}" + "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}", + "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ] } From 02c374cb58b506fe2f75cf5170c3a7feb432f6e3 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 00:24:21 +0530 Subject: [PATCH 14/21] NULL assume to assignment --- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 4 ++-- .../proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 5c71c04129..bbc7694516 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -137,7 +137,7 @@ void harness() __CPROVER_assume( pxNetworkEndPoints != NULL ); pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); - __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL ); + pxNetworkEndPoints->pxNext->pxNext = NULL; /* Interface init. */ pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); @@ -148,7 +148,7 @@ void harness() NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); - __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); + pxNetworkEndPoint_Temp->pxNext = NULL; //pxNetworkEndPoint_Temp->xDHCPData.eExpectedState = eExpectedState; /**************************************************************** diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c index 7cb0f992df..9ad18e06aa 100644 --- a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c +++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -36,7 +36,7 @@ void harness() NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); - __CPROVER_assume( pxNetworkEndPoint_Temp->pxNext == NULL ); + pxNetworkEndPoint_Temp->pxNext = NULL; __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); } From 0090dc92dfb82fefd49b41b350327a3abde27695 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 09:29:35 +0530 Subject: [PATCH 15/21] updating with changes wrt review comments --- source/FreeRTOS_DHCP.c | 12 ++++++------ .../proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 10 +++++++++- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index 4397508359..d67b8b89e5 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -287,7 +287,7 @@ /* PAss the address of a pointer pucUDPPayload, because zero-copy is used. */ lBytes = FreeRTOS_recvfrom( xDHCPv4Socket, &( pucUDPPayload ), 0, FREERTOS_ZERO_COPY, NULL, NULL ); - if( lBytes > 0 && pucUDPPayload != NULL ) + if( ( lBytes > 0 ) && ( pucUDPPayload != NULL ) ) { /* Remove it now, destination not found. */ FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); @@ -1317,7 +1317,7 @@ } } } - if (pucUDPPayload != NULL) + if( pucUDPPayload != NULL ) { FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); } @@ -1481,7 +1481,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( xDHCPv4Socket != FREERTOS_INVALID_SOCKET && xDHCPv4Socket != NULL && pucUDPPayloadBuffer != NULL ) + if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) ) { /* Copy in the IP address being requested. */ @@ -1508,7 +1508,7 @@ { /* The packet was not successfully queued for sending and must be * returned to the stack. */ - if (pucUDPPayloadBuffer != NULL) + if( pucUDPPayloadBuffer != NULL ) { FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); } @@ -1553,7 +1553,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( xDHCPv4Socket != FREERTOS_INVALID_SOCKET && xDHCPv4Socket != NULL && pucUDPPayloadBuffer != NULL ) + if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) ) { const void * pvCopySource; void * pvCopyDest; @@ -1593,7 +1593,7 @@ { /* The packet was not successfully queued for sending and must be * returned to the stack. */ - if (pucUDPPayloadBuffer != NULL) + if( pucUDPPayloadBuffer != NULL ) { FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer ); } diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index bbc7694516..39b8e5bbbc 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -87,7 +87,15 @@ BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, size_t uxAddressLength, BaseType_t xInternal ) { - return 0; + /* Return value is set to zero assuming socket bind will succeed. If it doesnt, it + will hit an assert in the function. */ + BaseType_t xRet = 0; + __CPROVER_assert( pxSocket != NULL, + "FreeRTOS precondition: pxSocket != NULL" ); + __CPROVER_assert( pxBindAddress != NULL, + "FreeRTOS precondition: pxBindAddress != NULL" ); + + return xRet; } From 53db8bdfdc4f5768c2c969860e94fa50439ba348 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 11:54:07 +0530 Subject: [PATCH 16/21] adding more non determinism to the proof --- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 39b8e5bbbc..1f88277ef0 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -139,25 +139,29 @@ void harness() { BaseType_t xReset; BaseType_t xDoCheck; - //eDHCPState_t eExpectedState; pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); - pxNetworkEndPoints->pxNext->pxNext = NULL; /* Interface init. */ pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); - pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface; - __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL ); + if( nondet_bool() ) + { + pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); + pxNetworkEndPoints->pxNext->pxNext = NULL; + pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface; + } + else + { + pxNetworkEndPoints->pxNext = NULL; + } NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); pxNetworkEndPoint_Temp->pxNext = NULL; - //pxNetworkEndPoint_Temp->xDHCPData.eExpectedState = eExpectedState; /**************************************************************** * Initialize the counter used to bound the number of times From 2b974a9356395d64096cdcdb7d7ddda76d717687 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 14:10:45 +0530 Subject: [PATCH 17/21] free memory in FreeRTOS_ReleaseUDPPayloadBuffer --- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 5 +++-- test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 2 -- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 1f88277ef0..af99995741 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -120,6 +120,9 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) { __CPROVER_assert( pvBuffer != NULL, "FreeRTOS precondition: pvBuffer != NULL" ); + + /* Free buffer after adjusting offsets. */ + free( ( ( ( uint8_t * ) pvBuffer ) - ( ipUDP_PAYLOAD_OFFSET_IPv4 + ipIP_TYPE_OFFSET ) ) ); } /* CALLED BY FREERTOS @@ -186,8 +189,6 @@ void harness() } - __CPROVER_assume( xDHCPv4Socket != NULL ); - xDHCPv4Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP ); __CPROVER_file_local_FreeRTOS_DHCP_c_vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp ); diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 813c4bfc98..2a738ac573 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -41,8 +41,6 @@ "CBMCFLAGS": [ "--unwind 4", "--unwindset strlen.0:11,memcmp.0:7", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", "--nondet-static --flush" ], "OPT": From 243b0a5995532f3764b98c018a5a60d6fa9f36f3 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 01:52:51 +0530 Subject: [PATCH 18/21] WIP DHCPProcess CBMC proof --- source/FreeRTOS_DHCP.c | 15 +++++++++++---- test/cbmc/patches/FreeRTOSIPConfig.h | 4 +++- .../DHCP/DHCPProcess/DHCPProcess_harness.c | 16 ++++++++++++---- test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 10 ++++++++-- 4 files changed, 34 insertions(+), 11 deletions(-) diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index d67b8b89e5..8f53b2d2fd 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -1350,7 +1350,11 @@ #if ( ipconfigDHCP_REGISTER_HOSTNAME == 1 ) const char * pucHostName = pcApplicationHostnameHook(); - size_t uxNameLength = strlen( pucHostName ); + size_t uxNameLength = 0; + if( pucHostName != NULL ) + { + uxNameLength = strlen( pucHostName ); + } uint8_t * pucPtr; /* memcpy() helper variables for MISRA Rule 21.15 compliance*/ @@ -1425,10 +1429,13 @@ * compliant with MISRA Rule 21.15. These should be * optimized away. */ - pvCopySource = pucHostName; - pvCopyDest = &pucPtr[ 2U ]; + if( pucHostName != NULL ) + { + pvCopySource = pucHostName; + pvCopyDest = &pucPtr[ 2U ]; - ( void ) memcpy( pvCopyDest, pvCopySource, uxNameLength ); + ( void ) memcpy( pvCopyDest, pvCopySource, uxNameLength ); + } pucPtr[ 2U + uxNameLength ] = ( uint8_t ) dhcpOPTION_END_BYTE; *pxOptionsArraySize += ( size_t ) ( 2U + uxNameLength ); } diff --git a/test/cbmc/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h index 8e9db1031c..6c3e2f7e46 100644 --- a/test/cbmc/patches/FreeRTOSIPConfig.h +++ b/test/cbmc/patches/FreeRTOSIPConfig.h @@ -135,7 +135,9 @@ extern uint32_t ulRand(); * reason. The static configuration used is that passed into the stack by the * FreeRTOS_IPInit() function call. */ #define ipconfigUSE_DHCP 1 -#define ipconfigDHCP_REGISTER_HOSTNAME 1 +#ifndef ipconfigDHCP_REGISTER_HOSTNAME + #define ipconfigDHCP_REGISTER_HOSTNAME 1 +#endif #define ipconfigDHCP_USES_UNICAST 1 /* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index af99995741..cffc9be6ce 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -129,10 +129,18 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) * Hook to return a human-readable name */ const char * pcApplicationHostnameHook( void ) { - const char * name; - - name = "hostname"; - return name; + size_t xHostNameLength; + __CPROVER_assume( ( xHostNameLength > 0 ) && ( xHostNameLength <= MAX_HOSTNAME_LEN ) ); + char * pcHost = malloc( xHostNameLength ); + + __CPROVER_assume( pcHost != NULL ); + + memset(pcHost, 'a', xHostNameLength); + // if( pcHost != NULL) + // { + pcHost[ xHostNameLength - 1 ] = '\0'; + // } + return pcHost; } /**************************************************************** * The proof of vDHCPProcess diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 2a738ac573..f855130409 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -30,6 +30,8 @@ "ENTRY": "DHCPProcess", # Minimal buffer size for maximum coverage, see harness for details. + "MAX_HOSTNAME_LEN": 5, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", "BUFFER_SIZE": 299, "ENDPOINT_DNS_ADDRESS_COUNT": 5, @@ -40,7 +42,9 @@ "CBMCFLAGS": [ "--unwind 4", - "--unwindset strlen.0:11,memcmp.0:7", + "--unwindset strlen.0:{HOSTNAME_UNWIND},memcmp.0:7", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", "--nondet-static --flush" ], "OPT": @@ -60,8 +64,10 @@ "DEF": [ "BUFFER_SIZE={BUFFER_SIZE}", + "ipconfigDHCP_REGISTER_HOSTNAME=1", "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}", - "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" + "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" ] } From e2c9b2ff16fff79a1481bcbcfd4d6021c4c621b2 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 15:22:40 +0530 Subject: [PATCH 19/21] wip DHCP process --- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index cffc9be6ce..d3ae8f08d7 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -130,16 +130,11 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) const char * pcApplicationHostnameHook( void ) { size_t xHostNameLength; - __CPROVER_assume( ( xHostNameLength > 0 ) && ( xHostNameLength <= MAX_HOSTNAME_LEN ) ); + __CPROVER_assume( xHostNameLength == 5 ); char * pcHost = malloc( xHostNameLength ); - __CPROVER_assume( pcHost != NULL ); - memset(pcHost, 'a', xHostNameLength); - // if( pcHost != NULL) - // { - pcHost[ xHostNameLength - 1 ] = '\0'; - // } + pcHost[ xHostNameLength - 1 ] = '\0'; return pcHost; } /**************************************************************** From 5f4dc29aba1b4a29c5568381c08342b607df9760 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 23:19:40 +0530 Subject: [PATCH 20/21] reverting back to old version --- .../proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 12 ------------ test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 12 ++---------- 2 files changed, 2 insertions(+), 22 deletions(-) diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index d3ae8f08d7..99e9ff7a17 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -125,18 +125,6 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) free( ( ( ( uint8_t * ) pvBuffer ) - ( ipUDP_PAYLOAD_OFFSET_IPv4 + ipIP_TYPE_OFFSET ) ) ); } -/* CALLED BY FREERTOS - * Hook to return a human-readable name */ -const char * pcApplicationHostnameHook( void ) -{ - size_t xHostNameLength; - __CPROVER_assume( xHostNameLength == 5 ); - char * pcHost = malloc( xHostNameLength ); - __CPROVER_assume( pcHost != NULL ); - memset(pcHost, 'a', xHostNameLength); - pcHost[ xHostNameLength - 1 ] = '\0'; - return pcHost; -} /**************************************************************** * The proof of vDHCPProcess ****************************************************************/ diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index f855130409..6a12b553d9 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -30,21 +30,16 @@ "ENTRY": "DHCPProcess", # Minimal buffer size for maximum coverage, see harness for details. - "MAX_HOSTNAME_LEN": 5, - "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", "BUFFER_SIZE": 299, "ENDPOINT_DNS_ADDRESS_COUNT": 5, # The number of times GetNetworkBufferWithDescriptor can be allowed to fail # (plus 1). "FAILURE_BOUND": 2, - "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", "CBMCFLAGS": [ "--unwind 4", - "--unwindset strlen.0:{HOSTNAME_UNWIND},memcmp.0:7", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", - "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}", + "--unwindset strlen.0:11,memcmp.0:7", "--nondet-static --flush" ], "OPT": @@ -60,14 +55,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" ], - "DEF": [ "BUFFER_SIZE={BUFFER_SIZE}", "ipconfigDHCP_REGISTER_HOSTNAME=1", "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", - "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}", - "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}", - "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" ] } From b6e96c37c133ed63f1e54e4581351ee550a82d53 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 21 Feb 2023 15:53:56 +0530 Subject: [PATCH 21/21] adding more comments --- test/cbmc/patches/FreeRTOSIPConfig.h | 6 +++--- test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 2 ++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/test/cbmc/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h index 6c3e2f7e46..449cc89f49 100644 --- a/test/cbmc/patches/FreeRTOSIPConfig.h +++ b/test/cbmc/patches/FreeRTOSIPConfig.h @@ -135,9 +135,9 @@ extern uint32_t ulRand(); * reason. The static configuration used is that passed into the stack by the * FreeRTOS_IPInit() function call. */ #define ipconfigUSE_DHCP 1 -#ifndef ipconfigDHCP_REGISTER_HOSTNAME - #define ipconfigDHCP_REGISTER_HOSTNAME 1 -#endif + +#define ipconfigDHCP_REGISTER_HOSTNAME 1 + #define ipconfigDHCP_USES_UNICAST 1 /* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 99e9ff7a17..651ed9dead 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -79,6 +79,8 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_ BaseType_t xSocketValid( const ConstSocket_t xSocket ) { + /* This proof assumes that the socket will be valid to make the proof run + without causing asserts in the DHCP source [configASSERT( xSocketValid( xDHCPv4Socket ) == pdTRUE );] */ return pdTRUE; }