diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index f65d5599c9..8f53b2d2fd 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 ) + if( ( lBytes > 0 ) && ( pucUDPPayload != NULL ) ) { /* Remove it now, destination not found. */ FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); @@ -1317,8 +1317,10 @@ } } } - - FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); + if( pucUDPPayload != NULL ) + { + FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload ); + } } /* if( lBytes > 0 ) */ return xReturn; @@ -1348,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*/ @@ -1423,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 ); } @@ -1479,7 +1488,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( pucUDPPayloadBuffer != NULL ) + if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) ) { /* Copy in the IP address being requested. */ @@ -1506,7 +1515,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 { @@ -1548,7 +1560,7 @@ &( uxOptionsLength ), pxEndPoint ); - if( pucUDPPayloadBuffer != NULL ) + if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) ) { const void * pvCopySource; void * pvCopyDest; @@ -1588,7 +1600,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/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h index 8e9db1031c..449cc89f49 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 + #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 cd628ff0be..651ed9dead 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -42,32 +42,91 @@ #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 + + + /**************************************************************** * The signature of the function under test. ****************************************************************/ -void vDHCPProcess( BaseType_t xReset, - eDHCPState_t eExpectedState ); +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(); } +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; +} + +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + /* 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; +} + + +/*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" ); + + /* Free buffer after adjusting offsets. */ + free( ( ( ( uint8_t * ) pvBuffer ) - ( ipUDP_PAYLOAD_OFFSET_IPv4 + ipIP_TYPE_OFFSET ) ) ); +} + /**************************************************************** * The proof of vDHCPProcess ****************************************************************/ @@ -75,7 +134,30 @@ BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ) void harness() { BaseType_t xReset; - eDHCPState_t eExpectedState; + BaseType_t xDoCheck; + + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + + /* Interface init. */ + pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); + __CPROVER_assume( pxNetworkEndPoints->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; /**************************************************************** * Initialize the counter used to bound the number of times @@ -93,12 +175,15 @@ 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, eExpectedState ); + 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 5fcd044318..6a12b553d9 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -31,12 +31,21 @@ # 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, - "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", + "--nondet-static --flush" + ], + "OPT": + [ + "--export-file-local-symbols" + ], "OBJS": [ "$(ENTRY)_harness.goto", @@ -46,10 +55,10 @@ "$(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}" ] 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" ], diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json index 1fa2aa6888..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,15 +21,21 @@ ################################################################ # 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 memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + "--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" ], - "OBJS": [ "$(ENTRY)_harness.goto", @@ -43,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}" ] } diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c index 99e94dd3fd..9ad18e06aa 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 __CPROVER_file_local_FreeRTOS_DHCP_c_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 ); + pxNetworkEndPoint_Temp->pxNext = NULL; + + __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp ); } diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index 15407a6398..f52a1573f2 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; }