From 9e445d295c5d43d12cea4cfc586b69f8b937b7bb Mon Sep 17 00:00:00 2001 From: "Ching-Hsin,Lee" Date: Tue, 16 Jul 2024 17:32:34 +0800 Subject: [PATCH 1/5] Update LTS 202406.01 information --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 870125ebb..08ed92b14 100644 --- a/README.md +++ b/README.md @@ -3,10 +3,10 @@ FreeRTOS-Plus-TCP is a lightweight TCP/IP stack for FreeRTOS. It provides a fami This library has undergone static code analysis and checks for compliance with the [MISRA coding standard](https://www.misra.org.uk/). Any deviations from the MISRA C:2012 guidelines are documented under [MISRA Deviations](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md). The library is validated for memory safety and data structure invariance through the [CBMC automated reasoning tool](https://www.cprover.org/cbmc/) for the functions that parse data originating from the network. The library is also protocol tested using Maxwell protocol tester for both IPv4 and IPv6. -**FreeRTOS-Plus-TCP Library V4.2.1 -[source code](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/tree/V4.2.1/source) +**FreeRTOS-Plus-TCP Library V4.2.2 +[source code](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/tree/V4.2.2/source) is part of the -[FreeRTOS 202406.00 LTS](https://github.com/FreeRTOS/FreeRTOS-LTS/tree/202406.00-LTS) +[FreeRTOS 202406.01 LTS](https://github.com/FreeRTOS/FreeRTOS-LTS/tree/202406.01-LTS) release.** ## Getting started From d4a1b9bb238bc00c7639e0253636bb2fce48b23e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 29 Jul 2024 12:06:45 +0200 Subject: [PATCH 2/5] [Draft] CBMC: replace any missing functions by assert-false (#1147) * CBMC: replace any missing functions by assert-false --------- Co-authored-by: ActoryOu --- source/FreeRTOS_DNS_Cache.c | 3 +- .../ARP/ARPAgeCache/ARPAgeCache_harness.c | 6 + .../cbmc/proofs/ARP/ARPAgeCache/Makefile.json | 3 + .../ARP/ARPGetCacheEntry/Configurations.json | 2 + .../ARPProcessPacket_harness.c | 85 ++++--- .../proofs/ARP/ARPProcessPacket/Makefile.json | 5 +- .../ARP/ARPSendGratuitous/Makefile.json | 4 +- .../Configurations.json | 4 +- .../OutputARPRequest_harness.c | 37 ++- .../Configurations.json | 4 +- .../OutputARPRequest_harness.c | 8 + .../Configurations.json | 4 +- .../OutputARPRequest_harness.c | 9 + .../CheckOptionsInner_harness.c | 2 +- .../proofs/CheckOptionsInner/Makefile.json | 4 +- .../CheckOptionsOuter_harness.c | 2 +- .../proofs/CheckOptionsOuter/Makefile.json | 2 + .../DHCP/DHCPProcess/DHCPProcess_harness.c | 7 + .../proofs/DHCP/DHCPProcess/Makefile.json | 3 +- .../DHCPProcessEndPoint_harness.c | 30 +++ .../DHCP/DHCPProcessEndPoint/Makefile.json | 2 + .../DHCPv6HandleOption_harness.c | 17 ++ .../DHCPv6/DHCPv6HandleOption/Makefile.json | 6 - .../proofs/DHCPv6/DHCPv6Process/Makefile.json | 5 +- .../DHCPv6ProcessEndPoint_harness.c | 12 + .../DHCPv6ProcessEndPoint/Makefile.json | 10 +- .../DHCPv6/SendDHCPMessage/Makefile.json | 20 +- .../SendDHCPMessage/SendDHCPMessage_harness.c | 91 ++++++- .../DNSHandlePacket/DNShandlePacket_harness.c | 15 +- .../proofs/DNS/DNSHandlePacket/Makefile.json | 3 +- .../DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c | 27 ++ .../proofs/DNS/DNSTreatNBNS/Makefile.json | 14 +- .../DNSgetHostByName_harness.c | 124 ++++++--- .../proofs/DNS/DNSgetHostByName/Makefile.json | 12 +- .../DNSgetHostByName_a_harness.c | 153 ++++++++++-- .../DNS/DNSgetHostByName_a/Makefile.json | 5 +- .../DNSgetHostByName_cancel_harness.c | 51 ++-- .../DNS/DNSgetHostByName_cancel/Makefile.json | 10 +- .../DNS/prepareReplyDNSMessage/Makefile.json | 1 + .../IP/ProcessEthernetPacket/Makefile.json | 5 +- .../proofs/IP/SendEventToIPTask/Makefile.json | 4 +- .../SendEventToIPTask_harness.c | 10 + test/cbmc/proofs/Makefile.template | 6 +- .../prvProcessICMPMessage_IPv6/Makefile.json | 7 +- .../ProcessICMPMessage_IPv6_harness.c | 51 ++-- .../ND/prvReturnICMP_IPv6/Makefile.json | 7 +- .../ReturnICMP_IPv6_harness.c | 52 ++-- test/cbmc/proofs/RA/vReceiveRA/Makefile.json | 8 +- .../proofs/RA/vReceiveRA/ReceiveRA_harness.c | 60 +++-- .../RA/vReceiveRA_ReadReply/Makefile.json | 1 + .../MatchingEndpoint_harness.c | 10 + .../lTCPAddRxdata/TCPAddRxdata_harness.c | 38 ++- .../Makefile.json | 3 +- .../Socket/vSocketClose/Configurations.json | 1 + .../proofs/TCP/prvHandleListen/Makefile.json | 2 +- .../prvHandleListen/prvHandleListen_harness.c | 60 +++++ .../TCP/prvHandleListen_IPv6/Makefile.json | 2 +- .../prvHandleListen_IPv6_harness.c | 60 +++++ .../cbmc/proofs/TCP/prvSendData/Makefile.json | 3 +- .../proofs/TCP/prvSendData/SendData_harness.c | 66 ++++- .../TCP/prvTCPHandleState/Makefile.json | 11 +- .../TCPHandleState_harness.c | 236 +++++++++++++++--- .../TCP/prvTCPPrepareSend/Makefile.json | 8 +- .../TCPPrepareSend_harness.c | 122 ++++++--- .../TCP/prvTCPReturnPacket/Makefile.json | 9 +- .../TCPReturnPacket_harness.c | 91 +++++-- .../TCP/prvTCPReturnPacket_IPv6/Makefile.json | 9 +- .../TCPReturnPacket_IPv6_harness.c | 103 ++++++-- .../vProcessGeneratedUDPPacket_harness.c | 7 +- .../ProcessIPPacket/ProcessIPPacket_harness.c | 94 ++++++- .../ProcessReceivedTCPPacket/Makefile.json | 11 +- .../ProcessReceivedTCPPacket_harness.c | 83 +++++- .../Makefile.json | 16 +- .../ProcessReceivedTCPPacket_IPv6_harness.c | 12 +- .../ProcessReceivedUDPPacket/Makefile.json | 2 + .../ProcessReceivedUDPPacket_harness.c | 45 ++-- .../prvChecksumIPv6Checks/Makefile.json | 1 + test/cbmc/stubs/freertos_api.c | 54 ++++ test/cbmc/stubs/freertos_kernel_api.c | 88 +++++++ 79 files changed, 1850 insertions(+), 410 deletions(-) diff --git a/source/FreeRTOS_DNS_Cache.c b/source/FreeRTOS_DNS_Cache.c index 7c8e23638..119be881d 100644 --- a/source/FreeRTOS_DNS_Cache.c +++ b/source/FreeRTOS_DNS_Cache.c @@ -448,10 +448,9 @@ /* Add or update the item. */ if( strlen( pcName ) < ( size_t ) ipconfigDNS_CACHE_NAME_LENGTH ) { - ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, ipconfigDNS_CACHE_NAME_LENGTH ); + ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, strlen( pcName ) ); ( void ) memcpy( &( xDNSCache[ uxFreeEntry ].xAddresses[ 0 ] ), pxIP, sizeof( *pxIP ) ); - xDNSCache[ uxFreeEntry ].ulTTL = ulTTL; xDNSCache[ uxFreeEntry ].ulTimeWhenAddedInSeconds = ulCurrentTimeSeconds; #if ( ipconfigDNS_CACHE_ADDRESSES_PER_ENTRY > 1 ) diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c index 5a5b3e7c2..509cacb7b 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c +++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -33,6 +33,12 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes return 0; } + +void FreeRTOS_OutputAdvertiseIPv6( NetworkEndPoint_t * pxEndPoint ) +{ + __CPROVER_assert( pxEndPoint != NULL, "The Endpoint cannot be NULL." ); +} + void harness() { /* diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json index 24de2ff3c..b122ddc7d 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json @@ -15,6 +15,9 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" ], "DEF": diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json index aa4d60296..3301afb40 100644 --- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json +++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -14,6 +14,8 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" ], "DEF": diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c index 539f02d18..7be804559 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c +++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -1,5 +1,3 @@ -#include "cbmc.h" - /* FreeRTOS includes. */ #include "FreeRTOS.h" #include "queue.h" @@ -10,8 +8,37 @@ #include "FreeRTOS_ARP.h" #include "FreeRTOS_Routing.h" +/* CBMC includes. */ +#include "cbmc.h" + /* This pointer is maintained by the IP-task. Defined in FreeRTOS_IP.c */ extern NetworkBufferDescriptor_t * pxARPWaitingNetworkBuffer; +NetworkEndPoint_t * pxNetworkEndPoint_Temp; + +/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the + * correctness of the proof */ +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask_IPv6( const IPv6_Address_t * pxIPv6Address ) +{ + __CPROVER_assert( pxIPv6Address != NULL, "Precondition: pxIPv6Address != NULL" ); + + /* Assume at least one end-point is available */ + return pxNetworkEndPoint_Temp; +} + +/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the + * correctness of the proof */ +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, + uint32_t ulWhere ) +{ + /* Assume at least one end-point is available */ + return pxNetworkEndPoint_Temp; +} + +/* Get rid of configASSERT in FreeRTOS_TCP_IP.c */ +BaseType_t xIsCallingFromIPTask( void ) +{ + return pdTRUE; +} /* This is an output function and need not be tested with this proof. */ void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint, @@ -36,9 +63,19 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress, void harness() { - NetworkBufferDescriptor_t xLocalBuffer; + NetworkBufferDescriptor_t * pxLocalBuffer; + NetworkBufferDescriptor_t * pxNetworkBuffer2; + TickType_t xBlockTimeTicks; uint16_t usEthernetBufferSize; + /* + * The assumption made here is that the buffer pointed by pucEthernetBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer. + * This is not checked inside eARPProcessPacket. + */ + uint8_t ucBUFFER_SIZE; + + /* Non deterministically determine whether the pxARPWaitingNetworkBuffer will * point to some valid data or will it be NULL. */ if( nondet_bool() ) @@ -47,48 +84,34 @@ void harness() * checked in the function as the pointer is stored by the IP-task itself * and therefore it will always be of the required size. */ __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_t ) ); - - /* Add matching data length to the network buffer descriptor. */ - __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize ); - - xLocalBuffer.pucEthernetBuffer = malloc( usEthernetBufferSize ); + pxLocalBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, xBlockTimeTicks ); /* Since this pointer is maintained by the IP-task, either the pointer - * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer + * pxARPWaitingNetworkBuffer will be NULL or pxLocalBuffer->pucEthernetBuffer * will be non-NULL. */ - __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL ); + __CPROVER_assume( pxLocalBuffer != NULL ); + __CPROVER_assume( pxLocalBuffer->pucEthernetBuffer != NULL ); + __CPROVER_assume( pxLocalBuffer->xDataLength == usEthernetBufferSize ); - pxARPWaitingNetworkBuffer = &xLocalBuffer; + pxARPWaitingNetworkBuffer = pxLocalBuffer; } else { pxARPWaitingNetworkBuffer = NULL; } - /* - * The assumption made here is that the buffer pointed by pucEthernetBuffer - * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer. - * This is not checked inside eARPProcessPacket. - */ - uint8_t ucBUFFER_SIZE; - - void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) ); - - __CPROVER_assume( xBuffer != NULL ); - - NetworkBufferDescriptor_t xNetworkBuffer2; - - xNetworkBuffer2.pucEthernetBuffer = xBuffer; - xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( ARPPacket_t ); + pxNetworkBuffer2 = pxGetNetworkBufferWithDescriptor( ucBUFFER_SIZE + sizeof( ARPPacket_t ), xBlockTimeTicks ); + __CPROVER_assume( pxNetworkBuffer2 != NULL ); + __CPROVER_assume( pxNetworkBuffer2->pucEthernetBuffer != NULL ); /* * This proof assumes one end point is present. */ - xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL ); - xNetworkBuffer2.pxEndPoint->pxNext = NULL; + pxNetworkBuffer2->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkBuffer2->pxEndPoint != NULL ); + pxNetworkBuffer2->pxEndPoint->pxNext = NULL; /* eARPProcessPacket will be called in the source code only after checking if - * xNetworkBuffer2.pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL ); */ - eARPProcessPacket( &xNetworkBuffer2 ); + * pxNetworkBuffer2->pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL ); */ + eARPProcessPacket( pxNetworkBuffer2 ); } diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json index 00079ded1..003611ae9 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json @@ -11,6 +11,9 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ] } diff --git a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json index f069f5959..044a2b2c2 100644 --- a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -10,7 +10,9 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json index 62bb3e052..5e2c516c3 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -37,7 +37,9 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto" ], #That is the minimal required size for an ARPPacket_t plus offset in the buffer. "MINIMUM_PACKET_BYTES": 50, diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c index 9337fb4f7..b5b45cf67 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -35,6 +35,8 @@ #include "FreeRTOS_IP_Private.h" #include "FreeRTOS_ARP.h" +/* CBMC includes. */ +#include "cbmc.h" ARPPacket_t xARPPacket; NetworkBufferDescriptor_t xNetworkBuffer; @@ -56,15 +58,15 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS { #ifdef CBMC_PROOF_ASSUMPTION_HOLDS #if ( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) - xNetworkBuffer.pucEthernetBuffer = malloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES ); + xNetworkBuffer.pucEthernetBuffer = safeMalloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES ); #else - xNetworkBuffer.pucEthernetBuffer = malloc( xRequestedSizeBytes ); + xNetworkBuffer.pucEthernetBuffer = safeMalloc( xRequestedSizeBytes ); #endif #else uint32_t malloc_size; __CPROVER_assert( !__CPROVER_overflow_mult( 2, xRequestedSizeBytes ) ); __CPROVER_assume( malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes ); - xNetworkBuffer.pucEthernetBuffer = malloc( malloc_size ); + xNetworkBuffer.pucEthernetBuffer = safeMalloc( malloc_size ); #endif __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); @@ -72,6 +74,21 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS return &xNetworkBuffer; } +/* STUB! + * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor + * stub function above here. In this case, we should just free the allocated pucEthernetBuffer. + */ +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + if( pxNetworkBuffer->pucEthernetBuffer != NULL ) + { + free( pxNetworkBuffer->pucEthernetBuffer ); + } +} + BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, NetworkBufferDescriptor_t * const pxNetworkBuffer, BaseType_t xReleaseAfterSend ) @@ -81,6 +98,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." ); } +BaseType_t xIsCallingFromIPTask( void ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE ); + + return xReturn; +} void harness() { @@ -92,16 +117,16 @@ void harness() * Assumes one endpoint and interface is present. */ - pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); /* Interface init. */ - pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); + pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); if( nondet_bool() ) { - pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); pxNetworkEndPoints->pxNext->pxNext = NULL; pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface; diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json index e243382c3..ff5898c18 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -14,7 +14,9 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_1.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto" + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c index 492d97683..03c74e467 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -75,6 +75,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes } } +BaseType_t xIsCallingFromIPTask( void ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE ); + + return xReturn; +} void harness() { diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json index 5b2cdd30d..d37f17720 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -14,7 +14,9 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_2.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto" + "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c index 4d8493449..b87ae8b30 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -55,6 +55,15 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes } } +BaseType_t xIsCallingFromIPTask( void ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE ); + + return xReturn; +} + void harness() { BaseType_t xRes = xNetworkBuffersInitialise(); diff --git a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c index e4a08e2ee..8ac5d6a82 100644 --- a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c +++ b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -87,7 +87,7 @@ void harness() /* Preconditions */ /* CBMC model of pointers limits the size of the buffer */ - __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU ); /* Both preconditions are required to avoid integer overflow in the */ /* pointer offset of the pointer pucPtr + uxIndex + 8 */ diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index a902bcc94..522ca4cca 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -12,6 +12,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", @@ -21,6 +22,7 @@ ], "DEF": [ - "ipconfigUSE_TCP=1" + "ipconfigUSE_TCP=1", + "ipconfigNETWORK_MTU=586" ] } diff --git a/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c index 3d58d0dd1..867305d93 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c +++ b/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c @@ -81,7 +81,7 @@ void harness() ****************************************************************/ /* CBMC model of pointers limits the size of the buffer */ - __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU ); /* Preconditions */ __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */ diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index d97be23e6..898d1ea5b 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json @@ -12,6 +12,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", @@ -20,5 +21,6 @@ ], "DEF": [ + "ipconfigNETWORK_MTU=586" ] } diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 10c6aacf8..29fabf657 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -166,6 +166,13 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket, return retVal; } +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); + + return NULL; +} + /**************************************************************** * The proof of vDHCPProcess ****************************************************************/ diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 99e79d3b2..f74a67537 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -24,7 +24,8 @@ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c index db482595c..bd53b2745 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c @@ -145,6 +145,35 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, return ensure_FreeRTOS_Socket_t_is_allocated(); } +void vApplicationIPNetworkEventHook_Multi( eIPCallbackEvent_t eNetworkEvent, + struct xNetworkEndPoint * pxEndPoint ) +{ + __CPROVER_assert( eNetworkEvent == eNetworkUp || eNetworkEvent == eNetworkDown, "Network event is not correct" ); + __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" ); +} + +BaseType_t xIsCallingFromIPTask( void ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE ); + + return xReturn; +} + +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" ); + + return NULL; +} + +void vManageSolicitedNodeAddress( const struct xNetworkEndPoint * pxEndPoint, + BaseType_t xNetworkGoingUp ) +{ + __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" ); + __CPROVER_assert( pxEndPoint->pxNetworkInterface != NULL, "The network interface cannot be NULL" ); +} /**************************************************************** * The proof of vDHCPProcess @@ -178,6 +207,7 @@ void harness() __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); pxNetworkEndPoint_Temp->pxNext = NULL; pxNetworkEndPoint_Temp->xDHCPData.xDHCPSocket = NULL; + pxNetworkEndPoint_Temp->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface; /**************************************************************** * Initialize the counter used to bound the number of times diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json index ed7497613..59cfc8cc6 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json @@ -23,8 +23,10 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto" ], "DEF": diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c index 7a5495313..96b30b73c 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c @@ -74,6 +74,23 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t return nondet_BaseType(); } +uint16_t usBitConfig_read_16( BitConfig_t * pxConfig ) +{ + return ( uint16_t ) nondet_uint32(); +} + +uint8_t ucBitConfig_read_8( BitConfig_t * pxConfig ) +{ + return ( uint8_t ) nondet_uint32(); +} + +BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig, + uint8_t * pucData, + size_t uxSize ) +{ + return nondet_BaseType(); +} + void harness() { BaseType_t xResult; diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json index 09859a60b..ba6dbd18f 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json @@ -5,12 +5,6 @@ "--unwind 2", "--nondet-static --flush" ], - "INSTFLAGS": - [ - "--remove-function-body usBitConfig_read_16", - "--remove-function-body xBitConfig_read_uc", - "--remove-function-body ucBitConfig_read_8" - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json index 40839470b..fba06214b 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json @@ -19,6 +19,9 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" ] } \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c index 9157a86f2..350c13cce 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c @@ -77,6 +77,18 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, return pxSocket; } +void vIPNetworkUpCalls( struct xNetworkEndPoint * pxEndPoint ) +{ + __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" ); +} + +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); + + return NULL; +} + /** * For the purpose of this proof we assume that xSocketValid returns true always. * This has to do with assertions in the source code that checks for socket being invalid. diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json index d2d5931bc..21e1105ac 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json @@ -5,14 +5,6 @@ "--nondet-static --flush", "--unwind 1" ], - "INSTFLAGS": - [ - "--remove-function-body vIPSetDHCP_RATimerEnableState", - "--remove-function-body vDHCP_RATimerReload", - "--remove-function-body vIPNetworkUpCalls", - "--remove-function-body prvCloseDHCPv6Socket", - "--remove-function-body prvSendDHCPMessage" - ], "OPT": [ "--export-file-local-symbols" @@ -25,6 +17,8 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json index 08cb3e73a..98bc9f724 100644 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json @@ -4,20 +4,6 @@ [ "--nondet-static" ], - "INSTFLAGS": - [ - "--remove-function-body xApplicationGetRandomNumber", - "--remove-function-body ulApplicationTimeHook", - "--remove-function-body xBitConfig_init", - "--remove-function-body vBitConfig_write_8", - "--remove-function-body vBitConfig_write_uc", - "--remove-function-body vBitConfig_write_16", - "--remove-function-body vBitConfig_write_32", - "--remove-function-body pucBitConfig_peek_last_index_uc", - "--remove-function-body FreeRTOS_inet_pton6", - "--remove-function-body FreeRTOS_sendto", - "--remove-function-body vBitConfig_release" - ], "OPT": [ "--export-file-local-symbols" @@ -29,9 +15,9 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ] } \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c index fc2886720..436b96cf5 100644 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -42,14 +42,103 @@ #include "FreeRTOS_DHCP.h" #include "FreeRTOS_DHCPv6.h" #include "FreeRTOS_ARP.h" +#include "FreeRTOS_BitConfig.h" /* CBMC includes. */ #include "cbmc.h" +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint ); +BaseType_t xBitConfig_init( BitConfig_t * pxConfig, + const uint8_t * pucData, + size_t uxSize ) +{ + BaseType_t xReturn; -void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint ); + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); + + if( nondet_bool() ) + { + xReturn = pdTRUE; + + pxConfig->ucContents = safeMalloc( uxSize ); + __CPROVER_assume( pxConfig->ucContents != NULL ); + } + else + { + xReturn = pdFALSE; + } + + return xReturn; +} + +BaseType_t pucBitConfig_peek_last_index_uc( BitConfig_t * pxConfig, + uint8_t * pucData, + size_t uxSize ) +{ + BaseType_t xReturn; + + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); + __CPROVER_assert( pucData != NULL, "pucData cannot be NULL" ); + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; +} + +void vBitConfig_write_uc( BitConfig_t * pxConfig, + const uint8_t * pucData, + size_t uxSize ) +{ + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); + __CPROVER_assert( pucData != NULL, "pucData cannot be NULL" ); +} + +void vBitConfig_write_8( BitConfig_t * pxConfig, + uint8_t ucValue ) +{ + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); +} +void vBitConfig_write_16( BitConfig_t * pxConfig, + uint16_t usValue ) +{ + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); +} + +void vBitConfig_write_32( BitConfig_t * pxConfig, + uint32_t ulValue ) +{ + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); +} + +void vBitConfig_release( BitConfig_t * pxConfig ) +{ + __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" ); + + if( pxConfig->ucContents != NULL ) + { + free( pxConfig->ucContents ); + } +} + +BaseType_t FreeRTOS_inet_pton6( const char * pcSource, + void * pvDestination ) +{ + BaseType_t xReturn; + + __CPROVER_assert( pcSource != NULL, "pcSource cannot be NULL" ); + __CPROVER_assert( pvDestination != NULL, "pvDestination cannot be NULL" ); + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; +} + +uint32_t ulApplicationTimeHook( void ) +{ + return nondet_uint32(); +} void harness() { diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c index 983f1f109..52106ba65 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c +++ b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c @@ -7,11 +7,18 @@ #include "FreeRTOS_DNS.h" #include "FreeRTOS_IP_Private.h" -/* Function prvParseDNSReply is proven to be correct separately. */ -uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, - size_t xBufferLength, - BaseType_t xExpected ) +/* CBMC includes. */ +#include "cbmc.h" + +/* Function DNS_ParseDNSReply is proven to be correct separately. */ +uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t uxBufferLength, + struct freertos_addrinfo ** ppxAddressInfo, + BaseType_t xExpected, + uint16_t usPort ) { + __CPROVER_assert( pucUDPPayloadBuffer != NULL, "pucUDPPayloadBuffer cannot be NULL" ); + return nondet_uint32(); } void harness() diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json index 27864b146..511a166ca 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json @@ -4,7 +4,8 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c index d6be53942..7d1d70669 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c +++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c @@ -38,6 +38,7 @@ #include "cbmc.h" +const BaseType_t xBufferAllocFixedSize = pdFALSE; NetworkBufferDescriptor_t xNetworkBuffer; NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pvBuffer ) @@ -67,6 +68,11 @@ NetworkBufferDescriptor_t * pxResizeNetworkBufferWithDescriptor( NetworkBufferDe uint8_t * pucNewBuffer = safeMalloc( xNewSizeBytes ); __CPROVER_assume( pucNewBuffer != NULL ); + if( pxNetworkBuffer->pucEthernetBuffer ) + { + free( pxNetworkBuffer->pucEthernetBuffer ); + } + pxNetworkBuffer->pucEthernetBuffer = pucNewBuffer; if( nondet_bool() ) @@ -88,6 +94,26 @@ void prepareReplyDNSMessage( NetworkBufferDescriptor_t * pxNetworkBuffer, __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer: pvBuffer != NULL" ); } +BaseType_t xApplicationDNSQueryHook_Multi( struct xNetworkEndPoint * pxEndPoint, + const char * pcName ) +{ + BaseType_t xReturn; + + __CPROVER_assert( strlen( pcName ) < ipconfigDNS_CACHE_NAME_LENGTH, "The length of domain name must be less than cache size" ); + __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE ); + + return xReturn; +} + +/* vReturnEthernetFrame() is proved separately */ +void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" ); +} + void harness() { uint32_t ulIPAddress; @@ -103,6 +129,7 @@ void harness() xNetworkBuffer.pucEthernetBuffer = safeMalloc( xDataSize ); xNetworkBuffer.xDataLength = xDataSize; + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); if( nondet_bool() ) { diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json index 458443eb7..d3ab0d582 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json @@ -1,18 +1,24 @@ { "ENTRY": "DNS_TreatNBNS", "USE_CACHE":1, + "NBNS_NAME_MAX_LENGTH":17, "CBMCFLAGS": [ "--unwind 1", - "--unwindset DNS_TreatNBNS.0:16", - "--nondet-static" + "--unwindset DNS_TreatNBNS.0:{NBNS_NAME_MAX_LENGTH}", + "--unwindset prvFindEntryIndex.0:2", + "--unwindset strcmp.0:{NBNS_NAME_MAX_LENGTH}", + "--unwindset strlen.0:{NBNS_NAME_MAX_LENGTH}", + "--unwindset strncpy.0:{NBNS_NAME_MAX_LENGTH}" ], "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c index e849b4ee1..9e5658074 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -17,6 +17,7 @@ #include "NetworkBufferManagement.h" #include "NetworkInterface.h" +/* CBMC includes. */ #include "cbmc.h" uint32_t FreeRTOS_dnslookup( const char * pcHostName ); @@ -37,6 +38,7 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP const char * pcHostName, TickType_t uxIdentifier, UBaseType_t uxHostType ); +uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer ); /**************************************************************** * We abstract: @@ -56,6 +58,54 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP * bound the iterations of strcmp. ****************************************************************/ +/*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 * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxNetworkBuffer != NULL ) + { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ); + + if( pxNetworkBuffer->pucEthernetBuffer == NULL ) + { + free( pxNetworkBuffer ); + pxNetworkBuffer = NULL; + } + else + { + pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + } + } + + return pxNetworkBuffer; +} + +/* + * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor + * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer. + */ +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET ); + free( pxNetworkBuffer ); +} + +/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory + * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static + * memory */ +void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); +} + /**************************************************************** * Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply. * @@ -96,6 +146,22 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket, return ret; } +/**************************************************************** +* Abstract DNS_BindSocket +* +* We stub out this function with return constraint of true or false +* +****************************************************************/ +BaseType_t DNS_BindSocket( Socket_t xSocket, + uint16_t usPort ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; +} + /**************************************************************** * Abstract DNS_ReadReply * @@ -106,20 +172,39 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, struct freertos_sockaddr * xAddress, struct xDNSBuffer * pxDNSBuf ) { - BaseType_t ret; int len; + uintptr_t uxTypeOffset; + const uint8_t * pucIPType; + uint8_t ucIPType; + NetworkBufferDescriptor_t * pxNetworkEndPoints; - __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) ); + __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) ); - pxDNSBuf->pucPayloadBuffer = malloc( len ); + pxNetworkEndPoints = pxGetNetworkBufferWithDescriptor( len, 0 ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + __CPROVER_assume( pxNetworkEndPoints->pucEthernetBuffer != NULL ); + pxDNSBuf->pucPayloadBuffer = pxNetworkEndPoints->pucEthernetBuffer; pxDNSBuf->uxPayloadLength = len; - __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL ); - __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength ); - return ret; + /* When IPv6 is supported, find out the type of the packet. + * It is stored 48 bytes before the payload buffer as 0x40 or 0x60. */ + uxTypeOffset = __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( pxDNSBuf->pucPayloadBuffer ); + uxTypeOffset -= ipUDP_PAYLOAD_IP_TYPE_OFFSET; + pucIPType = ( const uint8_t * ) uxTypeOffset; + + /* For an IPv4 packet, pucIPType points to 6 bytes before the pucEthernetBuffer, + * for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */ + ucIPType = pucIPType[ 0 ] & 0xf0U; + + /* To help the translation from a UDP payload pointer to a networkBuffer, + * a byte was stored at a certain negative offset (-48 bytes). + * It must have a value of either 0x4x or 0x6x. */ + __CPROVER_assume( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) ); + + return nondet_basetype(); } @@ -177,30 +262,11 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP return size; } -/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */ -/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */ -NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks ) +uint32_t Prepare_CacheLookup( const char * pcHostName, + BaseType_t xFamily, + struct freertos_addrinfo ** ppxAddressInfo ) { - NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) ); - - if( pxNetworkBuffer != NULL ) - { - pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ); - - if( pxNetworkBuffer->pucEthernetBuffer == NULL ) - { - free( pxNetworkBuffer ); - pxNetworkBuffer = NULL; - } - else - { - pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; - } - } - - return pxNetworkBuffer; + return nondet_uint32(); } /**************************************************************** diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 66b7cad54..46a0c62cf 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -11,6 +11,7 @@ "ENDPOINT_DNS_ADDRESS_COUNT": 5, "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1", + "DNS_CACHE_ENTRIES": 2, "CBMCFLAGS": [ @@ -30,11 +31,13 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "DEF": @@ -42,6 +45,7 @@ "ipconfigUSE_IPv6=1", "ipconfigDNS_USE_CALLBACKS={callback}", "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", - "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" + "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}", + "ipconfigDNS_CACHE_ENTRIES={DNS_CACHE_ENTRIES}" ] } diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c index 7b7c4a3fb..03d1ecb73 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -17,8 +17,11 @@ #include "NetworkBufferManagement.h" #include "NetworkInterface.h" +/* CBMC includes. */ #include "cbmc.h" +uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer ); + /**************************************************************** * We abstract: * @@ -37,6 +40,54 @@ * bound the iterations of strcmp. ****************************************************************/ +/*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 * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxNetworkBuffer != NULL ) + { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET ); + + if( pxNetworkBuffer->pucEthernetBuffer == NULL ) + { + free( pxNetworkBuffer ); + pxNetworkBuffer = NULL; + } + else + { + pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET; + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + } + } + + return pxNetworkBuffer; +} + +/* + * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor + * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer. + */ +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) ); + free( pxNetworkBuffer ); +} + +/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory + * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static + * memory */ +void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, + "FreeRTOS precondition: pvBuffer != NULL" ); +} + /**************************************************************** * Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply. * @@ -111,37 +162,93 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes return ret; } -/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */ -/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */ -NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks ) +Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) { - NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) ); + Socket_t xSock = safeMalloc( sizeof( struct xSOCKET ) ); - if( pxNetworkBuffer != NULL ) - { - pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ); + return xSock; +} - if( pxNetworkBuffer->pucEthernetBuffer == NULL ) - { - free( pxNetworkBuffer ); - pxNetworkBuffer = NULL; - } - else - { - pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET; - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; - } - } +void DNS_CloseSocket( Socket_t xDNSSocket ) +{ + __CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." ); + free( xDNSSocket ); +} - return pxNetworkBuffer; +/**************************************************************** +* Abstract DNS_BindSocket +* +* We stub out this function with return constraint of true or false +* +****************************************************************/ +BaseType_t DNS_BindSocket( Socket_t xSocket, + uint16_t usPort ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; } -Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks ) +/**************************************************************** +* Abstract DNS_SendRequest +* +* We stub out this function with return constraint of true or false +* +****************************************************************/ +uint32_t DNS_SendRequest( Socket_t xDNSSocket, + struct freertos_sockaddr * xAddress, + struct xDNSBuffer * pxDNSBuf ) { - Socket_t xSock = safeMalloc( sizeof( struct xSOCKET ) ); + uint32_t ret; - return xSock; + __CPROVER_assume( ret >= 0 ); + __CPROVER_assume( ret <= 1 ); + + return ret; +} + +/**************************************************************** +* Abstract DNS_ReadReply +* +* We stub out this function which returned a dns_buffer filled with random data +* +****************************************************************/ +BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket, + struct freertos_sockaddr * xAddress, + struct xDNSBuffer * pxDNSBuf ) +{ + int len; + NetworkBufferDescriptor_t * pxNetworkBuffer; + + __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) ); + + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 ); + __CPROVER_assume( pxNetworkBuffer != NULL ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + + pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer; + pxDNSBuf->uxPayloadLength = len; + + __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength ); + + return nondet_basetype(); +} + +/* Function xDNSSetCallBack is proven to be correct separately. */ +BaseType_t xDNSSetCallBack( const char * pcHostName, + void * pvSearchID, + FOnDNSEvent pCallbackFunction, + TickType_t xTimeout, + TickType_t xIdentifier, + BaseType_t xIsIPv6 ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; } uint32_t Prepare_CacheLookup( const char * pcHostName, diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index f67cb0a11..e4114a1a6 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -24,11 +24,12 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c index 4ece6565b..e4ec2ecff 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c @@ -8,6 +8,8 @@ #include "FreeRTOS_DNS.h" #include "FreeRTOS_IP_Private.h" +/* CBMC includes. */ +#include "cbmc.h" /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */ @@ -20,27 +22,38 @@ BaseType_t xDNSSetCallBack( const char * pcHostName, TickType_t xIdentifier, BaseType_t xIsIPv6 ); -void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */ +/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */ +void vListInitialise( List_t * const pxList ) { - if( xWantedSize == 0 ) - { - return NULL; - } + __CPROVER_assert( pxList != NULL, "pxList cannot be NULL" ); - uint8_t byte; + pxList->pxIndex = ( ListItem_t * ) &( pxList->xListEnd ); + pxList->xListEnd.xItemValue = portMAX_DELAY; - return byte ? malloc( xWantedSize ) : NULL; + /* The list end next and previous pointers point to itself so we know + * when the list is empty. */ + pxList->xListEnd.pxNext = ( ListItem_t * ) &( pxList->xListEnd ); + pxList->xListEnd.pxPrevious = ( ListItem_t * ) &( pxList->xListEnd ); + pxList->uxNumberOfItems = ( UBaseType_t ) 0U; } -/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */ -BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, - TickType_t * const pxTicksToWait ) +/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */ +UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove ) { -} + List_t * const pxList = pxItemToRemove->pxContainer; -/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */ -BaseType_t xTaskResumeAll( void ) -{ + pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious; + pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext; + + if( pxList->pxIndex == pxItemToRemove ) + { + pxList->pxIndex = pxItemToRemove->pxPrevious; + } + + pxItemToRemove->pxContainer = NULL; + ( pxList->uxNumberOfItems )--; + + return pxList->uxNumberOfItems; } /* The function func mimics the callback function.*/ @@ -61,13 +74,11 @@ void harness() size_t len; BaseType_t xReturn; - __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN ); + __CPROVER_assume( len > 0 && len <= MAX_HOSTNAME_LEN ); char * pcHostName = safeMalloc( len ); - - if( len && pcHostName ) - { - pcHostName[ len - 1 ] = NULL; - } + __CPROVER_assume( pcHostName != NULL ); + __CPROVER_havoc_slice( pcHostName, len - 1 ); + pcHostName[ len - 1 ] = NULL; xReturn = xDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier, xIsIPv6 ); /* Add an item to be able to check the cancel function if the list is non-empty. */ FreeRTOS_gethostbyname_cancel( &pvSearchID ); diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json index 8f568fb54..fc7bfc4c0 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -10,14 +10,18 @@ [ "--unwind 1", "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}", - "--nondet-static" + "--unwindset strncpy.0:{HOSTNAME_UNWIND}" ], "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Callback.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json index f4f366afb..29e55e2b6 100644 --- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json +++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json @@ -10,6 +10,7 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], diff --git a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json index 4a2b35b44..101f63983 100644 --- a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json +++ b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json @@ -12,6 +12,9 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" ] } diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json index 30727432c..dfffab176 100644 --- a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json +++ b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json @@ -36,6 +36,8 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto" ] } diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c index 706bdb905..665d0ee92 100644 --- a/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c +++ b/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c @@ -36,6 +36,16 @@ #include "FreeRTOS_IP.h" #include "FreeRTOS_IP_Private.h" +/* Abstraction of xIsCallingFromIPTask */ +BaseType_t xIsCallingFromIPTask( void ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + /* The harness test proceeds to call SendEventToIPTask with an unconstrained value */ void harness() { diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 094fd560c..15cf815db 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -105,7 +105,11 @@ $(ENTRY)5.goto: $(ENTRY)4.goto $(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \ > $(ENTRY)5.txt 2>&1 -$(ENTRY).goto: $(ENTRY)5.goto +$(ENTRY)6.goto: $(ENTRY)5.goto + $(GOTO_INSTRUMENT) --generate-function-body '(?!__CPROVER).*' --generate-function-body-options assert-false @RULE_INPUT@ @RULE_OUTPUT@ \ + > $(ENTRY)6.txt 2>&1 + +$(ENTRY).goto: $(ENTRY)6.goto @CP@ @RULE_INPUT@ @RULE_OUTPUT@ # ____________________________________________________________________ diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json index 09f7d0beb..151aefe2e 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json @@ -8,8 +8,11 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto" - + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c index 990736bc7..0b02ac8ed 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c @@ -37,7 +37,6 @@ #include "FreeRTOS_ND.h" /* CBMC includes. */ -#include "../../utility/memory_assignments.c" #include "cbmc.h" extern NDCacheRow_t xNDCache[ ipconfigND_CACHE_ENTRIES ]; @@ -70,6 +69,12 @@ void vReceiveNA( const NetworkBufferDescriptor_t * pxNetworkBuffer ) __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." ); } +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +void vReceiveRA( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." ); +} + /* This function has been tested separately. Therefore, we assume that the implementation is correct. */ BaseType_t xSendEventStructToIPTask( const IPStackEvent_t * pxEvent, TickType_t uxTimeout ) @@ -103,7 +108,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac pxEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) + if( ( pxEndPoints ) && __CPROVER_w_ok( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) { /* Interface init. */ pxEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); @@ -116,21 +121,32 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac return pxEndPoints; } +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + size_t uxResult; + + __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) ); + + return uxResult; +} + void harness() { - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + NetworkBufferDescriptor_t * pxNetworkBuffer; uint32_t ulLen; uint16_t usEthernetBufferSize; - NetworkBufferDescriptor_t xLocalBuffer; + NetworkBufferDescriptor_t * pxLocalARPWaitingNetworkBuffer; + + __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); + + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 ); /* The code does not expect pxNetworkBuffer to be NULL. */ __CPROVER_assume( pxNetworkBuffer != NULL ); - - __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen ); pxNetworkBuffer->xDataLength = ulLen; - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ @@ -147,19 +163,20 @@ void harness() /* The packet must at least be as big as an IPv6 Packet. The size is not * checked in the function as the pointer is stored by the IP-task itself * and therefore it will always be of the required size. */ - __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ); - - /* Add matching data length to the network buffer descriptor. */ - __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize ); - - xLocalBuffer.pucEthernetBuffer = safeMalloc( usEthernetBufferSize ); + __CPROVER_assume( ( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ) && ( usEthernetBufferSize < ipconfigNETWORK_MTU ) ); + pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 ); /* Since this pointer is maintained by the IP-task, either the pointer - * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer + * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer * will be non-NULL. */ - __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL ); + __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL ); + __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL ); + __CPROVER_havoc_slice( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer, usEthernetBufferSize ); + + /* Add matching data length to the network buffer descriptor. */ + pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize; - pxARPWaitingNetworkBuffer = &xLocalBuffer; + pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; } else { diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json index cdc3a4f0a..47de0cd15 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json @@ -8,8 +8,11 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto" - + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "INC": [ diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c index b40437501..e0340a76c 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c @@ -37,7 +37,6 @@ #include "FreeRTOS_ND.h" /* CBMC includes. */ -#include "../../utility/memory_assignments.c" #include "cbmc.h" extern NDCacheRow_t xNDCache[ ipconfigND_CACHE_ENTRIES ]; @@ -72,6 +71,12 @@ void vReceiveNA( const NetworkBufferDescriptor_t * pxNetworkBuffer ) __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." ); } +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +void vReceiveRA( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." ); +} + /* This function has been tested separately. Therefore, we assume that the implementation is correct. */ BaseType_t xSendEventStructToIPTask( const IPStackEvent_t * pxEvent, TickType_t uxTimeout ) @@ -106,7 +111,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac pxEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) + if( ( pxEndPoints ) && __CPROVER_w_ok( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) { /* Interface init. */ pxEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); @@ -119,21 +124,33 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac return pxEndPoints; } +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + size_t uxResult; + + __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) ); + + return uxResult; +} + void harness() { - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + NetworkBufferDescriptor_t * pxNetworkBuffer; uint32_t ulLen; - NetworkBufferDescriptor_t xLocalBuffer; + NetworkBufferDescriptor_t * pxLocalARPWaitingNetworkBuffer; uint16_t usEthernetBufferSize; - /* The code does not expect both of these to be equal to NULL at the same time. */ - __CPROVER_assume( pxNetworkBuffer != NULL ); - __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 ); + + /* The code does not expect pxNetworkBuffer to be NULL. */ + __CPROVER_assume( pxNetworkBuffer != NULL ); + pxNetworkBuffer->xDataLength = ulLen; pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ @@ -149,19 +166,20 @@ void harness() /* The packet must at least be as big as an IPv6 Packet. The size is not * checked in the function as the pointer is stored by the IP-task itself * and therefore it will always be of the required size. */ - __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ); - - /* Add matching data length to the network buffer descriptor. */ - __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize ); - - xLocalBuffer.pucEthernetBuffer = safeMalloc( usEthernetBufferSize ); + __CPROVER_assume( ( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ) && ( usEthernetBufferSize < ipconfigNETWORK_MTU ) ); + pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 ); /* Since this pointer is maintained by the IP-task, either the pointer - * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer + * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer * will be non-NULL. */ - __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL ); + __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL ); + __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL ); + __CPROVER_havoc_slice( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer, usEthernetBufferSize ); + + /* Add matching data length to the network buffer descriptor. */ + pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize; - pxARPWaitingNetworkBuffer = &xLocalBuffer; + pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; prvProcessICMPMessage_IPv6( pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json index 8b995fc8d..1a4edbd46 100644 --- a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json @@ -4,6 +4,7 @@ [ "--unwind 2", "--unwindset FreeRTOS_NextEndPoint.0:1", + "--unwindset FreeRTOS_CreateIPv6Address.0:5", "--nondet-static" ], "OPT": @@ -13,8 +14,13 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "INC": diff --git a/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c b/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c index e7f6cf505..424c45832 100644 --- a/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c +++ b/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c @@ -37,7 +37,6 @@ #include "FreeRTOS_ND.h" /* CBMC includes. */ -#include "../../utility/memory_assignments.c" #include "cbmc.h" /* This function has been tested separately. Therefore, we assume that the implementation is correct. */ @@ -45,6 +44,11 @@ ICMPPrefixOption_IPv6_t * __CPROVER_file_local_FreeRTOS_RA_c_vReceiveRA_ReadRepl { ICMPPrefixOption_IPv6_t * pxPrefixOption = safeMalloc( sizeof( ICMPPrefixOption_IPv6_t ) ); + if( pxPrefixOption ) + { + __CPROVER_assume( ( pxPrefixOption->ucPrefixLength > 0U ) && ( pxPrefixOption->ucPrefixLength <= ( 8U * ipSIZE_OF_IPv6_ADDRESS ) ) ); + } + return pxPrefixOption; } @@ -75,30 +79,56 @@ void vNDSendRouterSolicitation( NetworkBufferDescriptor_t * pxNetworkBuffer, __CPROVER_assert( pxIPAddress != NULL, "The pxIPAddress cannot be NULL." ); } -void harness() +/* The checksum generation is stubbed out since the actual checksum + * does not matter. The stub will return an indeterminate value each time. */ +uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, + size_t uxBufferLength, + BaseType_t xOutgoingPacket ) { - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); - NetworkInterface_t * pxInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); - uint32_t ulLen; + __CPROVER_assert( pucEthernetBuffer != NULL, "Ethernet buffer cannot be NULL" ); - /* The code does not expect pxNetworkBuffer to be NULL. */ - __CPROVER_assume( pxNetworkBuffer != NULL ); - - __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + /* Return an indeterminate value. */ + return ( uint16_t ) nondet_uint32(); +} - pxNetworkBuffer->pxInterface = safeMalloc( sizeof( NetworkInterface_t ) ); - __CPROVER_assume( pxNetworkBuffer->pxInterface != NULL ); +/* vReturnEthernetFrame() is proved separately */ +void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" ); +} - pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); +void harness() +{ + NetworkBufferDescriptor_t * pxNetworkBuffer; + NetworkInterface_t * pxInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); + uint32_t ulLen; /* Initialize global Endpoint variable */ pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxInterface; + pxNetworkEndPoints->pxNetworkInterface = safeMalloc( sizeof( NetworkInterface_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); pxNetworkEndPoints->pxNext = NULL; + /* Initialize network buffer. */ + __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); + + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 ); + + /* The code does not expect pxNetworkBuffer to be NULL. */ + __CPROVER_assume( pxNetworkBuffer != NULL ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen ); + + pxNetworkBuffer->pxInterface = pxNetworkEndPoints->pxNetworkInterface; + pxNetworkBuffer->pxEndPoint = pxNetworkEndPoints; + + /* The prefix length must be equal to or less than 128 to avoid assertion in FreeRTOS_CreateIPv6Address(). */ + __CPROVER_assume( ( pxNetworkEndPoints->ipv6_settings.uxPrefixLength > 0U ) && ( pxNetworkEndPoints->ipv6_settings.uxPrefixLength <= ( 8U * ipSIZE_OF_IPv6_ADDRESS ) ) ); + vReceiveRA( pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json index 61d93b3d5..91ff52732 100644 --- a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json @@ -12,6 +12,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto" ], diff --git a/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c b/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c index dbcde05c0..1496562b1 100644 --- a/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c +++ b/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c @@ -39,6 +39,16 @@ #include "../../utility/memory_assignments.c" #include "cbmc.h" +/* Abstraction of xIsIPv6Loopback returns either true or false. */ +BaseType_t xIsIPv6Loopback( const IPv6_Address_t * pxAddress ) +{ + BaseType_t xReturn; + + __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE ); + + return xReturn; +} + void harness() { NetworkInterface_t * pxNetworkInterface = safeMalloc( sizeof( NetworkInterface_t ) ); diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c index 6e0b9278a..123b94527 100644 --- a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c +++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c @@ -34,11 +34,45 @@ void * pvPortMallocLarge( size_t xWantedSize ) return safeMalloc( xWantedSize ); } +size_t uxStreamBufferFrontSpace( const StreamBuffer_t * const pxBuffer ) +{ + size_t uxReturn; + + return uxReturn; +} + +BaseType_t xSendEventToIPTask( eIPEvent_t eEvent ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +void vTCPStateChange( FreeRTOS_Socket_t * pxSocket, + enum eTCP_STATE eTCPState ) +{ +} + +size_t uxStreamBufferAdd( StreamBuffer_t * const pxBuffer, + size_t uxOffset, + const uint8_t * const pucData, + size_t uxByteCount ) +{ + size_t uxReturn; + + __CPROVER_assert( __CPROVER_r_ok( pucData, uxByteCount ), "Data pointer must be valid to read" ); + __CPROVER_assume( uxReturn <= uxByteCount ); + + return uxReturn; +} + void harness() { FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); size_t uxOffset; - const uint8_t * pcData; + const uint8_t * pcData = NULL; uint32_t ulByteCount; /* This function expect socket to be not NULL, as it has been validated previously */ @@ -48,7 +82,9 @@ void harness() __CPROVER_assume( pxSocket->u.xTCP.uxRxStreamSize >= 0 && pxSocket->u.xTCP.uxRxStreamSize < ipconfigTCP_RX_BUFFER_LENGTH ); __CPROVER_assume( pxSocket->u.xTCP.uxTxStreamSize >= 0 && pxSocket->u.xTCP.uxTxStreamSize < ipconfigTCP_TX_BUFFER_LENGTH ); + __CPROVER_assume( ulByteCount > 0U ); pcData = safeMalloc( ulByteCount ); + __CPROVER_assume( pcData != NULL ); lTCPAddRxdata( pxSocket, uxOffset, pcData, ulByteCount ); } diff --git a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json index 379ae7a39..336e6d2ec 100644 --- a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json +++ b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json @@ -13,7 +13,8 @@ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto", - "$(ENTRY)_harness.goto" + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ], "INSTFLAGS": [ diff --git a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json index 50df09417..f36f3dc53 100644 --- a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json +++ b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json @@ -9,6 +9,7 @@ [ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", "$(ENTRY)_harness.goto" ], "DEF": diff --git a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json index 856e50c30..ab47b60c1 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json @@ -9,6 +9,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_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv4.goto" ], @@ -19,7 +20,6 @@ ], "INSTFLAGS": [ - "--remove-function-body prvTCPSendReset" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c b/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c index a74229372..3fa5aadd8 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c +++ b/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c @@ -53,6 +53,66 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, return ensure_FreeRTOS_Socket_t_is_allocated(); } +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + BaseType_t xRet; + + __CPROVER_assert( pxSocket != NULL, + "FreeRTOS precondition: pxSocket != NULL" ); + __CPROVER_assert( pxBindAddress != NULL, + "FreeRTOS precondition: pxBindAddress != NULL" ); + + return xRet; +} + +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" ); + + return NULL; +} + +BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +void vTCPStateChange( FreeRTOS_Socket_t * pxSocket, + enum eTCP_STATE eTCPState ) +{ +} + +BaseType_t prvTCPCreateWindow( FreeRTOS_Socket_t * pxSocket ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +void prvSocketSetMSS( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); +} + +size_t FreeRTOS_GetLocalAddress( ConstSocket_t xSocket, + struct freertos_sockaddr * pxAddress ) +{ + size_t uxReturn; + + __CPROVER_assert( pxAddress != NULL, "pxAddress cannot be NULL" ); + + return uxReturn; +} + void harness() { size_t xDataLength; diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json index aa1ee4f70..b824b9a39 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json @@ -11,6 +11,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_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv6.goto" ], @@ -21,7 +22,6 @@ ], "INSTFLAGS": [ - "--remove-function-body prvTCPSendReset" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c index 5134b5bca..8be5891f9 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c +++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c @@ -53,6 +53,66 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, return ensure_FreeRTOS_Socket_t_is_allocated(); } +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + BaseType_t xRet; + + __CPROVER_assert( pxSocket != NULL, + "FreeRTOS precondition: pxSocket != NULL" ); + __CPROVER_assert( pxBindAddress != NULL, + "FreeRTOS precondition: pxBindAddress != NULL" ); + + return xRet; +} + +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" ); + + return NULL; +} + +void prvSocketSetMSS( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); +} + +BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +void vTCPStateChange( FreeRTOS_Socket_t * pxSocket, + enum eTCP_STATE eTCPState ) +{ +} + +BaseType_t prvTCPCreateWindow( FreeRTOS_Socket_t * pxSocket ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +size_t FreeRTOS_GetLocalAddress( ConstSocket_t xSocket, + struct freertos_sockaddr * pxAddress ) +{ + size_t uxReturn; + + __CPROVER_assert( pxAddress != NULL, "pxAddress cannot be NULL" ); + + return uxReturn; +} + void harness() { size_t xDataLength; diff --git a/test/cbmc/proofs/TCP/prvSendData/Makefile.json b/test/cbmc/proofs/TCP/prvSendData/Makefile.json index cfc73e67e..f8b8a29f1 100644 --- a/test/cbmc/proofs/TCP/prvSendData/Makefile.json +++ b/test/cbmc/proofs/TCP/prvSendData/Makefile.json @@ -8,7 +8,8 @@ "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c index 83da8405b..1f76a23fc 100644 --- a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c +++ b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c @@ -36,7 +36,7 @@ #include "FreeRTOS_TCP_IP.h" /* CBMC includes. */ -#include "../../utility/memory_assignments.c" +#include "cbmc.h" /**************************************************************** * Declare the IP Header Size external to the harness so it can be @@ -52,15 +52,75 @@ size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) return uxIPHeaderSizePacket_uxResult; } +void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t * pxDescriptor, + uint32_t ulLen, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" ); + __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" ); + __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" ); +} + +void prvTCPReturnPacket_IPV4( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t * pxDescriptor, + uint32_t ulLen, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" ); + __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" ); + __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" ); +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated() +{ + size_t buf_size; /* Give buffer_size an unconstrained value */ + FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxSocket->u.xTCP.pxAckMessage != NULL ) + { + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); + pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size ); + __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL ); + } + + return pxSocket; +} + +/* + * In this function, it only allocates network buffer by harness. + */ +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, + "Precondition: pxNetworkBuffer != NULL" ); + + if( pxNetworkBuffer->pucEthernetBuffer != NULL ) + { + free( pxNetworkBuffer->pucEthernetBuffer ); + } + + free( pxNetworkBuffer ); +} + void harness() { FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + NetworkBufferDescriptor_t * pxNetworkBuffer; uint32_t ulReceiveLength; BaseType_t xByteCount; size_t buf_size; /* Give buffer_size an unconstrained value */ /* The code does not expect pxSocket/pxNetworkBuffer to be equal to NULL. */ + pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); __CPROVER_assume( pxSocket != NULL ); __CPROVER_assume( pxNetworkBuffer != NULL ); @@ -73,7 +133,7 @@ void harness() uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv4_HEADER; } - __CPROVER_assume( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) ); + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); pxNetworkBuffer->pucEthernetBuffer = safeMalloc( buf_size ); __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json index c82fbddc3..bc6f29b9c 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json @@ -45,18 +45,21 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto" ], "DEF": [ + "ipconfigUSE_TCP=1", "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "ipconfigNETWORK_MTU=586" ], "INSTFLAGS": [ - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c index 1f5f99ea6..c73802300 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -35,7 +35,8 @@ #include "FreeRTOS_IP_Private.h" #include "FreeRTOS_TCP_IP.h" -#include "../../utility/memory_assignments.c" +/* CBMC includes. */ +#include "cbmc.h" extern FreeRTOS_Socket_t * xSocketToListen; @@ -61,32 +62,209 @@ TaskHandle_t xTaskGetCurrentTaskHandle( void ) BaseType_t publicTCPHandleState( FreeRTOS_Socket_t * pxSocket, NetworkBufferDescriptor_t ** ppxNetworkBuffer ); +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); + + return NULL; +} + +void vSocketWakeUpUser( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); + + return NULL; +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated() +{ + size_t buf_size; /* Give buffer_size an unconstrained value */ + FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxSocket->u.xTCP.pxAckMessage != NULL ) + { + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); + pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size ); + __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL ); + } + + return pxSocket; +} + +/* lTCPAddRxdata is proven separately. */ +int32_t lTCPAddRxdata( FreeRTOS_Socket_t * pxSocket, + size_t uxOffset, + const uint8_t * pcData, + uint32_t ulByteCount ) +{ + return nondet_int32(); +} + +/* prvSendData is proven separately. */ +BaseType_t prvSendData( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t ** ppxNetworkBuffer, + uint32_t ulReceiveLength, + BaseType_t xByteCount ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" ); + + return nondet_BaseType(); +} + +/* prvTCPPrepareSend is proven separately. */ +int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t ** ppxNetworkBuffer, + UBaseType_t uxOptionsLength ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" ); + + return nondet_int32(); +} + +/* Mock all window APIs */ +int32_t lTCPWindowRxCheck( TCPWindow_t * pxWindow, + uint32_t ulSequenceNumber, + uint32_t ulLength, + uint32_t ulSpace, + uint32_t * pulSkipCount ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" ); + *pulSkipCount = nondet_uint32(); + + return nondet_int32(); +} + +uint32_t ulTCPWindowTxAck( TCPWindow_t * pxWindow, + uint32_t ulSequenceNumber ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" ); + + return nondet_uint32(); +} + +void vTCPWindowInit( TCPWindow_t * pxWindow, + uint32_t ulAckNumber, + uint32_t ulSequenceNumber, + uint32_t ulMSS ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" ); +} + +BaseType_t xTCPWindowRxEmpty( const TCPWindow_t * pxWindow ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" ); + + return nondet_BaseType(); +} + +BaseType_t xTCPWindowTxDone( const TCPWindow_t * pxWindow ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" ); + + return nondet_BaseType(); +} + +/* Mock all stream buffer APIs */ +size_t uxStreamBufferGet( StreamBuffer_t * const pxBuffer, + size_t uxOffset, + uint8_t * const pucData, + size_t uxMaxCount, + BaseType_t xPeek ) +{ + __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" ); + + return nondet_sizet(); +} + +size_t uxStreamBufferGetSpace( const StreamBuffer_t * const pxBuffer ) +{ + __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" ); + + return nondet_sizet(); +} + +/* Mock all transmission APIs. */ +UBaseType_t prvSetOptions( FreeRTOS_Socket_t * pxSocket, + const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); + + return nondet_ubasetype(); +} + +UBaseType_t prvSetSynAckOptions( FreeRTOS_Socket_t * pxSocket, + TCPHeader_t * pxTCPHeader ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( pxTCPHeader != NULL, "pxTCPHeader cannot be NULL" ); + + return nondet_ubasetype(); +} + +void prvTCPAddTxData( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); +} + +BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); + + return nondet_BaseType(); +} + +const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily, + const void * pvSource, + char * pcDestination, + socklen_t uxSize ) +{ + __CPROVER_assert( __CPROVER_r_ok( pcDestination, uxSize ), "input buffer must be available" ); + + __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET6 && __CPROVER_r_ok( pvSource, 16 ) ) || + ( xAddressFamily == FREERTOS_AF_INET && __CPROVER_r_ok( pvSource, 4 ) ), + "input address must be available" ); +} + void harness() { FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - size_t socketSize = sizeof( FreeRTOS_Socket_t ); - if( ensure_memory_is_valid( pxSocket, socketSize ) ) + __CPROVER_assume( pxSocket != NULL ); + + /* ucOptionLength is the number of valid bytes in ulOptionsData[]. + * ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)]. + * This assumption is required for a memcpy function that copies uxOptionsLength + * data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/ + __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof( uint32_t ) * ipSIZE_TCP_OPTIONS / sizeof( uint32_t ) ); + /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume( pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof( size_t ) ); + /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume( pxSocket->u.xTCP.usMSS == sizeof( uint16_t ) ); + + if( xIsCallingFromIPTask() == pdFALSE ) { - /* ucOptionLength is the number of valid bytes in ulOptionsData[]. - * ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)]. - * This assumption is required for a memcpy function that copies uxOptionsLength - * data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/ - __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof( uint32_t ) * ipSIZE_TCP_OPTIONS / sizeof( uint32_t ) ); - /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ - __CPROVER_assume( pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof( size_t ) ); - /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ - __CPROVER_assume( pxSocket->u.xTCP.usMSS == sizeof( uint16_t ) ); - - if( xIsCallingFromIPTask() == pdFALSE ) - { - __CPROVER_assume( pxSocket->u.xTCP.bits.bPassQueued == pdFALSE_UNSIGNED ); - __CPROVER_assume( pxSocket->u.xTCP.bits.bPassAccept == pdFALSE_UNSIGNED ); - } + __CPROVER_assume( pxSocket->u.xTCP.bits.bPassQueued == pdFALSE_UNSIGNED ); + __CPROVER_assume( pxSocket->u.xTCP.bits.bPassAccept == pdFALSE_UNSIGNED ); } - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); - size_t bufferSize = sizeof( NetworkBufferDescriptor_t ); + NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + __CPROVER_assume( pxNetworkBuffer != NULL ); FreeRTOS_Socket_t xSck; xSocketToListen = &xSck; @@ -94,17 +272,15 @@ void harness() /* Call to init the socket list. */ vListInitialise( &xBoundTCPSocketsList ); - if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) ) - { - /* Allocates min. buffer size required for the proof */ - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ); - } + /* Allocates min. buffer size required for the proof */ + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - if( ensure_memory_is_valid( pxSocket, socketSize ) && - ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) && - ensure_memory_is_valid( pxNetworkBuffer->pucEthernetBuffer, sizeof( TCPPacket_t ) ) && - ensure_memory_is_valid( pxSocket->u.xTCP.pxPeerSocket, socketSize ) ) + if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE ) { - publicTCPHandleState( pxSocket, &pxNetworkBuffer ); + /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */ + __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL ); } + + publicTCPHandleState( pxSocket, &pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json index df1df0a68..e1dd2fdf0 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -40,7 +40,10 @@ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "OPT": [ @@ -48,7 +51,8 @@ ], "DEF": [ - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index d889e1638..63bfac279 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -36,30 +36,35 @@ #include "FreeRTOS_TCP_IP.h" #include "FreeRTOS_Stream_Buffer.h" -#include "../../utility/memory_assignments.c" +/* CBMC includes. */ +#include "cbmc.h" /* This proof assumes that pxGetNetworkBufferWithDescriptor is implemented correctly. */ int32_t publicTCPPrepareSend( FreeRTOS_Socket_t * pxSocket, NetworkBufferDescriptor_t ** ppxNetworkBuffer, UBaseType_t uxOptionsLength ); -/* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */ -NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks ) +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated() { - NetworkBufferDescriptor_t * pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); - size_t bufferSize = sizeof( NetworkBufferDescriptor_t ); + size_t buf_size; /* Give buffer_size an unconstrained value */ + FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) ); - if( ensure_memory_is_valid( pxBuffer, bufferSize ) ) + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxSocket->u.xTCP.pxAckMessage != NULL ) { - /* The code does not expect pucEthernetBuffer to be equal to NULL if - * pxBuffer is not NULL. */ - pxBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes ); - __CPROVER_assume( pxBuffer->pucEthernetBuffer != NULL ); - pxBuffer->xDataLength = xRequestedSizeBytes; + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); + pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size ); + __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL ); } - return pxBuffer; + return pxSocket; } /* Get rid of configASSERT in FreeRTOS_TCP_IP.c */ @@ -68,37 +73,94 @@ BaseType_t xIsCallingFromIPTask( void ) return pdTRUE; } -void harness() +/* Mock FreeRTOS_TCP_State_Handling.h APIs */ +BaseType_t prvTCPSocketIsActive( eIPTCPState_t eStatus ) +{ + return nondet_BaseType(); +} + +/* Mock FreeRTOS_TCP_WIN.h APIs */ +BaseType_t xTCPWindowTxDone( const TCPWindow_t * pxWindow ) { - FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + return nondet_uint32(); +} - __CPROVER_assume( pxSocket != NULL ); - pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) ); - pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); - pxSocket->u.xTCP.pxPeerSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); +uint32_t ulTCPWindowTxGet( TCPWindow_t * pxWindow, + uint32_t ulWindowSize, + int32_t * plPosition ) +{ + uint32_t ulReturn = nondet_uint32(); + + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( plPosition != NULL, "plPosition cannot be NULL" ); + + /* This function returns the data length of next sending window, which is never larger than network MTU. */ + __CPROVER_assume( ulReturn < ipconfigNETWORK_MTU ); + return ulReturn; +} + +/* Mock FreeRTOS_Stream_Buffers.h APIs */ +size_t uxStreamBufferDistance( const StreamBuffer_t * const pxBuffer, + size_t uxLower, + size_t uxUpper ) +{ + __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" ); + return nondet_sizet(); +} + +size_t uxStreamBufferGet( StreamBuffer_t * const pxBuffer, + size_t uxOffset, + uint8_t * const pucData, + size_t uxMaxCount, + BaseType_t xPeek ) +{ + __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" ); + return nondet_sizet(); +} + +void * vSocketClose( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); + + return NULL; +} + +void vSocketWakeUpUser( FreeRTOS_Socket_t * pxSocket ) +{ + __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." ); - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + return NULL; +} + +void harness() +{ + NetworkBufferDescriptor_t * pxNetworkBuffer; + FreeRTOS_Socket_t * pxSocket; size_t socketSize = sizeof( FreeRTOS_Socket_t ); /* Allocates min. buffer size required for the proof */ - size_t bufferSize = sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ); + size_t bufferSize; - if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) - { - pxNetworkBuffer->xDataLength = bufferSize; + pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + __CPROVER_assume( pxSocket != NULL ); - /* The code does not expect pucEthernetBuffer to be equal to NULL if - * pxNetworkBuffer is not NULL. */ - pxNetworkBuffer->pucEthernetBuffer = malloc( bufferSize ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE ) + { + /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */ + __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL ); } - UBaseType_t uxOptionsLength; + bufferSize = sizeof( TCPPacket_t ) + ipSIZE_OF_IPv6_HEADER; + + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( bufferSize, 0 ); + __CPROVER_assume( pxNetworkBuffer != NULL ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); /* Call to init the socket list. */ vListInitialise( &xBoundTCPSocketsList ); if( pxSocket ) { - publicTCPPrepareSend( pxSocket, &pxNetworkBuffer, uxOptionsLength ); + publicTCPPrepareSend( pxSocket, &pxNetworkBuffer, 0 ); } } diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json index 1b67f5a07..12a17ef30 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -39,14 +39,19 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv4.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c index 786d10cfd..da15dfe89 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c @@ -37,10 +37,42 @@ #include "FreeRTOS_TCP_IP.h" #include "FreeRTOS_TCP_Transmission.h" -#include "../../utility/memory_assignments.c" - +/* CBMC includes */ #include "cbmc.h" +/* prvTCPReturnPacket_IPV6 is proven separately. */ +void prvTCPReturnPacket_IPV6( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t * pxDescriptor, + uint32_t ulLen, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor cannot be NULL" ); +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated() +{ + size_t buf_size; /* Give buffer_size an unconstrained value */ + FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxSocket->u.xTCP.pxAckMessage != NULL ) + { + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); + pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size ); + __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL ); + } + + return pxSocket; +} + /* * This function is implemented by a third party. * After looking through a couple of samples in the demos folder, it seems @@ -89,27 +121,31 @@ void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket, NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer, size_t xNewLength ) { - NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( xNewLength ); + NetworkBufferDescriptor_t * pxLocalNetworkBuffer; + EthernetHeader_t * pxHeader; + + pxLocalNetworkBuffer = pxGetNetworkBufferWithDescriptor( xNewLength, 0 ); - if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) + if( pxLocalNetworkBuffer != NULL ) { - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + /* In this test case, we only focus on IPv4. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ - pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); - pxNetworkBuffer->pxEndPoint->pxNext = NULL; + pxLocalNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint != NULL ); + pxLocalNetworkBuffer->pxEndPoint->pxNext = NULL; /* Add an interface */ - pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); - __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); + pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); + __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); - pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub; + pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub; } - return pxNetworkBuffer; + return pxLocalNetworkBuffer; } uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, @@ -169,29 +205,38 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress, void harness() { - FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + FreeRTOS_Socket_t * pxSocket; + NetworkBufferDescriptor_t * pxNetworkBuffer; BaseType_t xReleaseAfterSend; uint32_t ulLen; + EthernetHeader_t * pxHeader; + + pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + + if( pxSocket != NULL ) + { + /* In this test case, we only focus on IPv4. */ + __CPROVER_assume( pxSocket->bits.bIsIPv6 == pdFALSE_UNSIGNED ); + } + + __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU - ipSIZE_OF_ETH_HEADER ) ); + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen + ipSIZE_OF_ETH_HEADER, 0 ); /* The code does not expect both of these to be equal to NULL at the same time. */ __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL ); /* If network buffer is properly created. */ - if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) + if( pxNetworkBuffer != NULL ) { - /* Assume that the length is proper. */ - __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen + ipSIZE_OF_ETH_HEADER ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); - - pxNetworkBuffer->xDataLength = ( size_t ) ulLen; + /* In this test case, we only focus on IPv4. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) ) + if( pxNetworkBuffer->pxEndPoint != NULL ) { /* Add an interface */ pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json index 9b28c3b34..629ef713d 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json @@ -11,14 +11,19 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL" ], "INC": [ diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c index ea2e87b2f..95f47538c 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c @@ -35,10 +35,9 @@ #include "FreeRTOS_IP_Private.h" #include "FreeRTOS_TCP_IP.h" #include "FreeRTOS_TCP_Transmission.h" +#include "FreeRTOS_ND.h" /* CBMC includes. */ -#include "../../utility/memory_assignments.c" - #include "cbmc.h" /* @@ -64,6 +63,51 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes return 0; } +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated() +{ + size_t buf_size; /* Give buffer_size an unconstrained value */ + FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) ); + + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) ); + pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + + if( pxSocket->u.xTCP.pxAckMessage != NULL ) + { + __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) ); + pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size ); + __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL ); + } + + return pxSocket; +} + +void prvTCPReturnPacket_IPV4( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t * pxDescriptor, + uint32_t ulLen, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor cannot be NULL" ); +} + +/* Abstraction of eNDGetCacheEntry. */ +eARPLookupResult_t eNDGetCacheEntry( IPv6_Address_t * pxIPAddress, + MACAddress_t * const pxMACAddress, + struct xNetworkEndPoint ** ppxEndPoint ) +{ + eARPLookupResult_t xReturn; + + __CPROVER_assert( __CPROVER_r_ok( pxIPAddress, sizeof( IPv6_Address_t ) ), "pxIPAddress must be readable" ); + __CPROVER_assert( __CPROVER_w_ok( pxMACAddress, sizeof( MACAddress_t ) ), "pxMACAddress must be writeable" ); + + return xReturn; +} + /* Abstraction of this functions creates an endpoint and assign it to network interface * endpoint, real endpoint doesn't matter in this test. */ void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket, @@ -87,27 +131,31 @@ void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket, NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer, size_t xNewLength ) { - NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( xNewLength ); + NetworkBufferDescriptor_t * pxLocalNetworkBuffer; + EthernetHeader_t * pxHeader; + + pxLocalNetworkBuffer = pxGetNetworkBufferWithDescriptor( xNewLength, 0 ); - if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) + if( pxLocalNetworkBuffer != NULL ) { - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + /* In this test case, we only focus on IPv6. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType == ipIPv6_FRAME_TYPE ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ - pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); - pxNetworkBuffer->pxEndPoint->pxNext = NULL; + pxLocalNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint != NULL ); + pxLocalNetworkBuffer->pxEndPoint->pxNext = NULL; /* Add an interface */ - pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); - __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); + pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); + __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); - pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub; + pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub; } - return pxNetworkBuffer; + return pxLocalNetworkBuffer; } uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, @@ -136,29 +184,38 @@ uint16_t usGenerateChecksum( uint16_t usSum, void harness() { - FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + FreeRTOS_Socket_t * pxSocket; + NetworkBufferDescriptor_t * pxNetworkBuffer; BaseType_t xReleaseAfterSend; uint32_t ulLen; + EthernetHeader_t * pxHeader; + + pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + + if( pxSocket != NULL ) + { + /* In this test case, we only focus on IPv6. */ + __CPROVER_assume( pxSocket->bits.bIsIPv6 != pdFALSE_UNSIGNED ); + } + + __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU - ipSIZE_OF_ETH_HEADER ) ); + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen + ipSIZE_OF_ETH_HEADER, 0 ); /* The code does not expect both of these to be equal to NULL at the same time. */ __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL ); /* If network buffer is properly created. */ - if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) + if( pxNetworkBuffer != NULL ) { - /* Assume that the length is proper. */ - __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) ); - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen + ipSIZE_OF_ETH_HEADER ); - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - - pxNetworkBuffer->xDataLength = ( size_t ) ( ulLen + ipSIZE_OF_ETH_HEADER ); + /* In this test case, we only focus on IPv6. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType == ipIPv6_FRAME_TYPE ); /* Add an end point to the network buffer present. Its assumed that the * network interface layer correctly assigns the end point to the generated buffer. */ pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); - if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) ) + if( pxNetworkBuffer->pxEndPoint != NULL ) { /* Add an interface */ pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) ); diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index b56bc475b..5d8239d8a 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -19,6 +19,12 @@ #include "memory_assignments.c" #include "freertos_api.c" +/* vProcessGeneratedUDPPacket_IPv6 is proven separately. */ +void vProcessGeneratedUDPPacket_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); +} + /* We do not need to calculate the actual checksum for the proof to be complete. * Neither does the checksum matter for completeness. */ uint16_t usGenerateChecksum( uint16_t usSum, @@ -33,7 +39,6 @@ uint16_t usGenerateChecksum( uint16_t usSum, return usChecksum; } - /* We do not need to calculate the actual checksum for the proof to be complete. * Neither does the checksum matter for completeness. */ uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c index a1c0c80b0..e8c498ac9 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -9,9 +9,97 @@ /* CBMC includes. */ #include "cbmc.h" +NetworkEndPoint_t xEndpoint; + eFrameProcessingResult_t __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( const IPPacket_t * pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer ); +/* Check if input is a valid extension header ID. */ +BaseType_t xIsExtensionHeader( uint8_t ucCurrentHeader ) +{ + BaseType_t xReturn = pdFALSE; + + switch( ucCurrentHeader ) + { + case ipIPv6_EXT_HEADER_HOP_BY_HOP: + case ipIPv6_EXT_HEADER_DESTINATION_OPTIONS: + case ipIPv6_EXT_HEADER_ROUTING_HEADER: + case ipIPv6_EXT_HEADER_FRAGMENT_HEADER: + case ipIPv6_EXT_HEADER_AUTHEN_HEADER: + case ipIPv6_EXT_HEADER_SECURE_PAYLOAD: + case ipIPv6_EXT_HEADER_MOBILITY_HEADER: + xReturn = pdTRUE; + break; + } + + return xReturn; +} + +/* Abstraction of xGetExtensionOrder. To ensure the result of prepared extension headers is same. */ +BaseType_t xGetExtensionOrder( uint8_t ucProtocol, + uint8_t ucNextHeader ) +{ + return xIsExtensionHeader( ucProtocol ); +} + +BaseType_t xCheckRequiresARPResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + BaseType_t xReturn; + + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" ); +} + +void vARPRefreshCacheEntryAge( const MACAddress_t * pxMACAddress, + const uint32_t ulIPAddress ) +{ + __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" ); +} + +void vNDRefreshCacheEntry( const MACAddress_t * pxMACAddress, + const IPv6_Address_t * pxIPAddress, + NetworkEndPoint_t * pxEndPoint ) +{ + __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" ); + __CPROVER_assert( pxIPAddress != NULL, "pxIPAddress cannot be NULL" ); + __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint cannot be NULL" ); +} + +NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress, + uint32_t ulWhere ) +{ + NetworkEndPoint_t * pxEndpoint = NULL; + + if( nondet_bool() ) + { + pxEndpoint = pxNetworkEndPoints; + } + + return pxEndpoint; +} + +/* proof is done separately */ +eFrameProcessingResult_t ProcessICMPPacket( const NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + eFrameProcessingResult_t xReturn; + + __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" ); + + return xReturn; +} + +/* proof is done separately */ +eFrameProcessingResult_t prvProcessICMPMessage_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + eFrameProcessingResult_t xReturn; + + __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" ); + + return xReturn; +} + /* proof is done separately */ BaseType_t xProcessReceivedTCPPacket( NetworkBufferDescriptor_t * pxNetworkBuffer ) { @@ -67,6 +155,7 @@ void harness() { NetworkBufferDescriptor_t * const pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); uint8_t * pucEthernetBuffer = ( uint8_t * ) safeMalloc( ipTOTAL_ETHERNET_FRAME_SIZE + ipIP_TYPE_OFFSET ); + EthernetHeader_t * pxHeader; __CPROVER_assume( pxNetworkBuffer != NULL ); __CPROVER_assume( pucEthernetBuffer != NULL ); @@ -83,7 +172,10 @@ void harness() __CPROVER_assume( pxNetworkEndPoints != NULL ); __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); - IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer; + /* In this test case, we only focus on IPv4. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE ); + IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer; __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( pxIPPacket, pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json index f2643c9b9..bb142d42a 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -10,6 +10,8 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", @@ -23,16 +25,11 @@ ], "INSTFLAGS": [ - "--remove-function-body prvSingleStepTCPHeaderOptions", - "--remove-function-body prvCheckOptions", - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket", - "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" ], "DEF": [ - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND" ], "INC": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c index 00f6e8014..c15387b90 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -35,6 +35,81 @@ TaskHandle_t xTaskGetCurrentTaskHandle( void ) return pxCurrentTCB; } +/* Abstraction of vTCPStateChange */ +void vTCPStateChange( FreeRTOS_Socket_t * pxSocket, + enum eTCP_STATE eTCPState ) +{ +} + +/* prvTCPReturnPacket is proven separately */ +void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t * pxDescriptor, + uint32_t ulLen, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" ); + __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" ); + __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" ); +} + +/* prvTCPPrepareSend is proven separately. */ +int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t ** ppxNetworkBuffer, + UBaseType_t uxOptionsLength ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" ); + + return nondet_int32(); +} + +/* prvTCPHandleState is proven separately. */ +BaseType_t prvTCPHandleState( FreeRTOS_Socket_t * pxSocket, + NetworkBufferDescriptor_t ** ppxNetworkBuffer ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" ); + + return nondet_basetype(); +} + +/* prvCheckOptions is proven separately. */ +BaseType_t prvCheckOptions( FreeRTOS_Socket_t * pxSocket, + const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" ); + __CPROVER_assert( pxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in *ppxNetworkBuffer must be readable" ); + + return nondet_basetype(); +} + +BaseType_t xTCPWindowTxHasData( TCPWindow_t const * pxWindow, + uint32_t ulWindowSize, + TickType_t * pulDelay ) +{ + __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" ); + __CPROVER_assert( pulDelay != NULL, "pulDelay cannot be NULL" ); + + return nondet_basetype(); +} + +/* Abstraction of xSequenceLessThan */ +BaseType_t xSequenceLessThan( uint32_t a, + uint32_t b ) +{ + return nondet_basetype(); +} + +/* Abstraction of xSequenceGreaterThan */ +BaseType_t xSequenceGreaterThan( uint32_t a, + uint32_t b ) +{ + return nondet_basetype(); +} + /* Abstraction of prvHandleListen_IPV4 */ FreeRTOS_Socket_t * prvHandleListen_IPV4( FreeRTOS_Socket_t * pxSocket, NetworkBufferDescriptor_t * pxNetworkBuffer ) @@ -98,14 +173,12 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket ) void harness() { - NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + NetworkBufferDescriptor_t * pxNetworkBuffer; + + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 ); /* To avoid asserting on the network buffer being NULL. */ __CPROVER_assume( pxNetworkBuffer != NULL ); - - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); - - /* To avoid asserting on the ethernet buffer being NULL. */ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); xProcessReceivedTCPPacket( pxNetworkBuffer ); diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json index 53a28f733..c37bc279d 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json @@ -10,23 +10,17 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP_IPv6.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto" + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto" ], "INSTFLAGS": [ - "--remove-function-body prvSingleStepTCPHeaderOptions", - "--remove-function-body prvCheckOptions", - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket", - "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" ], "DEF": [ - "FREERTOS_TCP_ENABLE_VERIFICATION" + "FREERTOS_TCP_ENABLE_VERIFICATION", + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND" ], "INC": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c index c2be060ce..4135a9144 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c @@ -99,20 +99,18 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket ) void harness() { - NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + NetworkBufferDescriptor_t * pxNetworkBuffer; EthernetHeader_t * pxEthernetHeader; - /* To avoid asserting on the network buffer being NULL. */ - __CPROVER_assume( pxNetworkBuffer != NULL ); - - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_IPv6_t ) ); + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_IPv6_t ), 0 ); /* To avoid asserting on the ethernet buffer being NULL. */ + __CPROVER_assume( pxNetworkBuffer != NULL ); __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - /* Ethernet frame type is checked before calling xProcessReceivedTCPPacket_IPV6. */ + /* In this test case, we focus on IPv6 packets. */ pxEthernetHeader = ( EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer; __CPROVER_assume( pxEthernetHeader->usFrameType == ipIPv6_FRAME_TYPE ); - xProcessReceivedTCPPacket_IPV6( pxNetworkBuffer ); + xProcessReceivedTCPPacket( pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json index bc0bc61db..8c6859f4b 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -11,6 +11,8 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto", diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c index 6d282aca9..0b2b8c14c 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c @@ -9,6 +9,9 @@ #include "FreeRTOS_UDP_IP.h" #include "FreeRTOS_TCP_IP.h" +/* CBMC includes. */ +#include "cbmc.h" + /*This proof assumes that pxUDPSocketLookup is implemented correctly. */ /* This proof was done before. Hence we assume it to be correct here. */ @@ -17,6 +20,12 @@ void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, { } +void vARPRefreshCacheEntryAge( const MACAddress_t * pxMACAddress, + const uint32_t ulIPAddress ) +{ + __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" ); +} + /* This proof was done before. Hence we assume it to be correct here. */ BaseType_t xIsDHCPSocket( Socket_t xSocket ) { @@ -68,19 +77,6 @@ BaseType_t xProcessReceivedUDPPacket_IPv6( NetworkBufferDescriptor_t * pxNetwork return xReturn; } -/* Implementation of safe malloc */ -void * safeMalloc( size_t xWantedSize ) -{ - if( xWantedSize == 0 ) - { - return NULL; - } - - uint8_t byte; - - return byte ? malloc( xWantedSize ) : NULL; -} - /* Abstraction of pxUDPSocketLookup */ FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort ) { @@ -89,26 +85,23 @@ FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort ) void harness() { - NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); - BaseType_t * pxIsWaitingForARPResolution; + NetworkBufferDescriptor_t * pxNetworkBuffer; + BaseType_t xIsWaitingForARPResolution; NetworkEndPoint_t xEndpoint; uint16_t usPort; + EthernetHeader_t * pxHeader; - pxIsWaitingForARPResolution = safeMalloc( sizeof( BaseType_t ) ); - - /* The function under test is only called by the IP-task. The below pointer is an - * address of a local variable which is being passed to the function under test. - * Thus, it cannot ever be NULL. */ - __CPROVER_assume( pxIsWaitingForARPResolution != NULL ); - + pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( UDPPacket_t ), 0 ); /* The network buffer must not be NULL, checked in prvProcessEthernetPacket. */ __CPROVER_assume( pxNetworkBuffer != NULL ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( UDPPacket_t ) ); pxNetworkBuffer->pxEndPoint = &xEndpoint; - /* The ethernet buffer must be valid. */ - __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + /* In this test case, we only focus on IPv4. */ + pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer ); + __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE ); - xProcessReceivedUDPPacket( pxNetworkBuffer, usPort, pxIsWaitingForARPResolution ); + xIsWaitingForARPResolution = nondet_BaseType(); + xProcessReceivedUDPPacket( pxNetworkBuffer, usPort, &xIsWaitingForARPResolution ); } diff --git a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json index 9645ee00a..7d84cfcee 100644 --- a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json +++ b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json @@ -13,6 +13,7 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Utils.goto" ], "INSTFLAGS": diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index d541aa07a..db349a25a 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -49,6 +49,21 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, } } +/**************************************************************** +* 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. +****************************************************************/ + +BaseType_t FreeRTOS_listen( Socket_t xSocket, + BaseType_t xBacklog ) +{ + __CPROVER_assert( xSocket != NULL, "Socket cannot be NULL" ); + return nondet_BaseType(); +} + /**************************************************************** * Abstract FreeRTOS_setsockopt. * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html @@ -388,3 +403,42 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB } /****************************************************************/ + +/**************************************************************** +* Abstract vIPSetARPResolutionTimerEnableState +****************************************************************/ +void vIPSetARPResolutionTimerEnableState( BaseType_t xEnableState ) +{ +} + +/****************************************************************/ + +/**************************************************************** +* Abstract vIPSetARPResolutionTimerEnableState +****************************************************************/ +BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber ) +{ + __CPROVER_assert( pulNumber != NULL, "The input number cannot be NULL" ); + + BaseType_t xReturn; + + *pulNumber = nondet_uint32(); + + /* Return some random value. */ + return xReturn; +} + +/****************************************************************/ + +/**************************************************************** +* Abstract vIPSetARPResolutionTimerEnableState +****************************************************************/ +uint32_t ulApplicationGetNextSequenceNumber( uint32_t ulSourceAddress, + uint16_t usSourcePort, + uint32_t ulDestinationAddress, + uint16_t usDestinationPort ) +{ + return nondet_uint32(); +} + +/****************************************************************/ diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c index b74b4ec09..79fd0ff82 100644 --- a/test/cbmc/stubs/freertos_kernel_api.c +++ b/test/cbmc/stubs/freertos_kernel_api.c @@ -80,3 +80,91 @@ EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup, } /****************************************************************/ + +/**************************************************************** +* Abstract xEventGroupSetBits +****************************************************************/ +void vEventGroupDelete( EventGroupHandle_t xEventGroup ) +{ +} + +/****************************************************************/ + +/**************************************************************** +* Abstract xEventGroupSetBits +****************************************************************/ +EventGroupHandle_t xEventGroupCreate( void ) +{ + EventGroupHandle_t xReturn; + + return xReturn; +} + +/****************************************************************/ + +/**************************************************************** +* Abstract xQueueGenericSend +****************************************************************/ +BaseType_t xQueueGenericSend( QueueHandle_t xQueue, + const void * const pvItemToQueue, + TickType_t xTicksToWait, + const BaseType_t xCopyPosition ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +/****************************************************************/ + +/**************************************************************** +* Abstract uxQueueMessagesWaiting +****************************************************************/ +UBaseType_t uxQueueMessagesWaiting( const QueueHandle_t xQueue ) +{ + UBaseType_t uxReturn; + + __CPROVER_assume( uxReturn <= 2 ); + + return uxReturn; +} + +/****************************************************************/ + +/**************************************************************** +* Abstract vTaskSetTimeOutState +****************************************************************/ +void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut ) +{ +} + +/****************************************************************/ + +/**************************************************************** +* Abstract xTaskCheckForTimeOut +****************************************************************/ +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, + TickType_t * const pxTicksToWait ) +{ + BaseType_t xReturn; + + __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + + return xReturn; +} + +/****************************************************************/ + +/**************************************************************** +* Abstract xTaskGetTickCount +****************************************************************/ +TickType_t xTaskGetTickCount( void ) +{ + TickType_t xReturn; + + return xReturn; +} + +/****************************************************************/ From 43f68ef00100f583ab734952f71587e9bfd34490 Mon Sep 17 00:00:00 2001 From: Holden <68555040+HTRamsey@users.noreply.github.com> Date: Tue, 30 Jul 2024 22:14:20 -0400 Subject: [PATCH 3/5] Remove ipconfigHAS_ROUTING_STATISTICS (#1143) * remove ipconfigHAS_ROUTING_STATISTICS * Fix ARP CBMC failing --------- Co-authored-by: Tony Josi Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> Co-authored-by: ActoryOu --- source/FreeRTOS_ARP.c | 16 ++-- source/FreeRTOS_IP.c | 2 +- source/FreeRTOS_IPv4.c | 2 +- source/FreeRTOS_Routing.c | 82 +++---------------- source/FreeRTOS_Sockets.c | 2 +- source/FreeRTOS_TCP_Transmission.c | 2 +- source/FreeRTOS_UDP_IPv4.c | 2 +- source/include/FreeRTOSIPConfigDefaults.h | 16 ---- source/include/FreeRTOS_Routing.h | 26 +----- .../ARPProcessPacket_harness.c | 3 +- .../prepareReplyDNSMessage_harness.c | 3 +- .../ProcessIPPacket/ProcessIPPacket_harness.c | 3 +- .../FreeRTOS_ARP/FreeRTOS_ARP_utest.c | 30 +++---- ...eRTOS_ARP_DataLenLessThanMinPacket_utest.c | 2 +- .../FreeRTOS_Routing/FreeRTOSIPConfig.h | 2 - .../FreeRTOS_Routing/FreeRTOS_Routing_utest.c | 38 ++++----- .../FreeRTOSIPConfig.h | 2 - ...Routing_ConfigCompatibleWithSingle_utest.c | 14 ++-- .../FreeRTOSIPConfig.h | 2 - .../TCP_Transmission_list_macros.h | 4 +- .../FreeRTOS_UDP_IP_list_macros.h | 4 +- .../FreeRTOS_UDP_IPv4_utest.c | 6 +- 22 files changed, 71 insertions(+), 192 deletions(-) diff --git a/source/FreeRTOS_ARP.c b/source/FreeRTOS_ARP.c index 8fd9672fa..1e1fa615e 100644 --- a/source/FreeRTOS_ARP.c +++ b/source/FreeRTOS_ARP.c @@ -244,7 +244,7 @@ _static ARPCacheRow_t xARPCache[ ipconfigARP_CACHE_ENTRIES ]; /* Process received ARP frame to see if there is a clash. */ #if ( ipconfigARP_USE_CLASH_DETECTION != 0 ) { - NetworkEndPoint_t * pxSourceEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( ulSenderProtocolAddress, 2 ); + NetworkEndPoint_t * pxSourceEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( ulSenderProtocolAddress ); if( ( pxSourceEndPoint != NULL ) && ( pxSourceEndPoint->ipv4_settings.ulIPAddress == ulSenderProtocolAddress ) ) { @@ -699,7 +699,7 @@ void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, { #if ( ipconfigARP_STORES_REMOTE_ADDRESSES == 0 ) /* Only process the IP address if it is on the local network. */ - BaseType_t xAddressIsLocal = ( FreeRTOS_FindEndPointOnNetMask( ulIPAddress, 2 ) != NULL ) ? 1 : 0; /* ARP remote address. */ + BaseType_t xAddressIsLocal = ( FreeRTOS_FindEndPointOnNetMask( ulIPAddress ) != NULL ) ? 1 : 0; /* ARP remote address. */ /* Only process the IP address if it matches with one of the end-points. */ if( xAddressIsLocal != 0 ) @@ -789,7 +789,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, BaseType_t xReturn = pdFALSE; #if ( ipconfigARP_STORES_REMOTE_ADDRESSES != 0 ) - BaseType_t xAddressIsLocal = ( FreeRTOS_FindEndPointOnNetMask( ulIPAddress, 2 ) != NULL ) ? 1 : 0; /* ARP remote address. */ + BaseType_t xAddressIsLocal = ( FreeRTOS_FindEndPointOnNetMask( ulIPAddress ) != NULL ) ? 1 : 0; /* ARP remote address. */ #endif /* Start with the maximum possible number. */ @@ -855,7 +855,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, /* If ARP stores the MAC address of IP addresses outside the * network, than the MAC address of the gateway should not be * overwritten. */ - BaseType_t xOtherIsLocal = ( FreeRTOS_FindEndPointOnNetMask( xARPCache[ x ].ulIPAddress, 3 ) != NULL ) ? 1 : 0; /* ARP remote address. */ + BaseType_t xOtherIsLocal = ( FreeRTOS_FindEndPointOnNetMask( xARPCache[ x ].ulIPAddress ) != NULL ) ? 1 : 0; /* ARP remote address. */ if( xAddressIsLocal == xOtherIsLocal ) { @@ -972,7 +972,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, *( ppxEndPoint ) = NULL; ulAddressToLookup = *pulIPAddress; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( ulAddressToLookup, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( ulAddressToLookup ); if( xIsIPv4Multicast( ulAddressToLookup ) != 0 ) { @@ -999,7 +999,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, { /* This is a broadcast so it uses the broadcast MAC address. */ ( void ) memcpy( pxMACAddress->ucBytes, xBroadcastMACAddress.ucBytes, sizeof( MACAddress_t ) ); - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulAddressToLookup, 4 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulAddressToLookup ); if( pxEndPoint != NULL ) { @@ -1036,7 +1036,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, /* It is assumed that devices with the same netmask are on the same * LAN and don't need a gateway. */ - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulAddressToLookup, 4 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulAddressToLookup ); if( pxEndPoint == NULL ) { @@ -1346,7 +1346,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress, /* Its assumed that IPv4 endpoints belonging to different physical interface * in the system will have a different subnet, but endpoints on same interface * may have it. */ - NetworkEndPoint_t * pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulIPAddress, 12 ); + NetworkEndPoint_t * pxEndPoint = FreeRTOS_FindEndPointOnNetMask( ulIPAddress ); if( pxEndPoint != NULL ) { diff --git a/source/FreeRTOS_IP.c b/source/FreeRTOS_IP.c index 3765e85a4..aadf73be2 100644 --- a/source/FreeRTOS_IP.c +++ b/source/FreeRTOS_IP.c @@ -2123,7 +2123,7 @@ void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, #if ( ipconfigUSE_IPv4 != 0 ) case ipIPv4_FRAME_TYPE: - pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxIPPacket->xIPHeader.ulDestinationIPAddress, 7 ); + pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxIPPacket->xIPHeader.ulDestinationIPAddress ); break; #endif /* ( ipconfigUSE_IPv4 != 0 ) */ diff --git a/source/FreeRTOS_IPv4.c b/source/FreeRTOS_IPv4.c index d095f1266..bd8ab1919 100644 --- a/source/FreeRTOS_IPv4.c +++ b/source/FreeRTOS_IPv4.c @@ -318,7 +318,7 @@ enum eFrameProcessingResult prvAllowIPPacketIPv4( const struct xIP_PACKET * cons } } else if( - ( FreeRTOS_FindEndPointOnIP_IPv4( ulDestinationIPAddress, 4 ) == NULL ) && + ( FreeRTOS_FindEndPointOnIP_IPv4( ulDestinationIPAddress ) == NULL ) && /* Is it an IPv4 broadcast address x.x.x.255 ? */ ( ( FreeRTOS_ntohl( ulDestinationIPAddress ) & 0xffU ) != 0xffU ) && ( xIsIPv4Multicast( ulDestinationIPAddress ) == pdFALSE ) && diff --git a/source/FreeRTOS_Routing.c b/source/FreeRTOS_Routing.c index 5d342c83e..6d89ed186 100644 --- a/source/FreeRTOS_Routing.c +++ b/source/FreeRTOS_Routing.c @@ -140,12 +140,6 @@ struct xIPv6_Couple #if ( ipconfigCOMPATIBLE_WITH_SINGLE == 0 ) - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) - RoutingStats_t xRoutingStatistics; - #endif - -/*-----------------------------------------------------------*/ - /** * @brief Add a network interface to the list of interfaces. Check if the interface was * already added in an earlier call. @@ -379,29 +373,13 @@ struct xIPv6_Couple * @brief Find the end-point which has a given IPv4 address. * * @param[in] ulIPAddress The IP-address of interest, or 0 if any IPv4 end-point may be returned. - * @param[in] ulWhere For maintaining routing statistics ulWhere acts as an index to the data structure - * that keep track of the number of times 'FreeRTOS_FindEndPointOnIP_IPv4()' - * has been called from a particular location. Used only if - * ipconfigHAS_ROUTING_STATISTICS is enabled. * * @return The end-point found or NULL. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress, - uint32_t ulWhere ) + NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress ) { NetworkEndPoint_t * pxEndPoint = pxNetworkEndPoints; - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) - uint32_t ulLocationCount = ( uint32_t ) ( sizeof( xRoutingStatistics.ulLocationsIP ) / sizeof( xRoutingStatistics.ulLocationsIP[ 0 ] ) ); - - xRoutingStatistics.ulOnIp++; - - if( ulWhere < ulLocationCount ) - { - xRoutingStatistics.ulLocationsIP[ ulWhere ]++; - } - #endif /* ( ipconfigHAS_ROUTING_STATISTICS == 1 ) */ - while( pxEndPoint != NULL ) { #if ( ipconfigUSE_IPv4 != 0 ) @@ -456,12 +434,6 @@ struct xIPv6_Couple { NetworkEndPoint_t * pxEndPoint = pxNetworkEndPoints; - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) - { - xRoutingStatistics.ulOnMAC++; - } - #endif - /* If input MAC address is NULL, return NULL. */ if( pxMACAddress == NULL ) { @@ -495,18 +467,12 @@ struct xIPv6_Couple * @brief Find an end-point that handles a given IPv4-address. * * @param[in] ulIPAddress The IP-address for which an end-point is looked-up. - * @param[in] ulWhere For maintaining routing statistics ulWhere acts as an index to the data structure - * that keep track of the number of times 'FreeRTOS_InterfaceEndPointOnNetMask()' - * has been called from a particular location. Used only if - * ipconfigHAS_ROUTING_STATISTICS is enabled. * * @return An end-point that has the same network mask as the given IP-address. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ) + NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ) { - /* The 'ulWhere' parameter is only for debugging purposes. */ - return FreeRTOS_InterfaceEndPointOnNetMask( NULL, ulIPAddress, ulWhere ); + return FreeRTOS_InterfaceEndPointOnNetMask( NULL, ulIPAddress ); } /*-----------------------------------------------------------*/ @@ -517,30 +483,13 @@ struct xIPv6_Couple * pxInterface is NULL. * @param[in] ulIPAddress The IP-address for which an end-point is looked-up. * - * @param[in] ulWhere For maintaining routing statistics ulWhere acts as an index to the data structure - * that keep track of the number of times 'FreeRTOS_InterfaceEndPointOnNetMask()' - * has been called from a particular location. Used only if - * ipconfigHAS_ROUTING_STATISTICS is enabled. - * * @return An end-point that has the same network mask as the given IP-address. */ NetworkEndPoint_t * FreeRTOS_InterfaceEndPointOnNetMask( const NetworkInterface_t * pxInterface, - uint32_t ulIPAddress, - uint32_t ulWhere ) + uint32_t ulIPAddress ) { NetworkEndPoint_t * pxEndPoint = pxNetworkEndPoints; - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) - uint32_t ulLocationCount = ( uint32_t ) ( sizeof( xRoutingStatistics.ulLocations ) / sizeof( xRoutingStatistics.ulLocations[ 0 ] ) ); - - xRoutingStatistics.ulOnNetMask++; - - if( ulWhere < ulLocationCount ) - { - xRoutingStatistics.ulLocations[ ulWhere ]++; - } - #endif /* ( ipconfigHAS_ROUTING_STATISTICS == 1 ) */ - /* Find the best fitting end-point to reach a given IP-address. */ /*_RB_ Presumably then a broadcast reply could go out on a different end point to that on @@ -572,8 +521,8 @@ struct xIPv6_Couple /* This was only for debugging. */ if( pxEndPoint == NULL ) { - FreeRTOS_debug_printf( ( "FreeRTOS_FindEndPointOnNetMask[%d]: No match for %xip\n", - ( unsigned ) ulWhere, ( unsigned ) FreeRTOS_ntohl( ulIPAddress ) ) ); + FreeRTOS_debug_printf( ( "FreeRTOS_FindEndPointOnNetMask: No match for %xip\n", + ( unsigned ) FreeRTOS_ntohl( ulIPAddress ) ) ); } return pxEndPoint; @@ -930,12 +879,6 @@ struct xIPv6_Couple * defined end-point has the best match. */ - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) - { - /* Some stats while developing. */ - xRoutingStatistics.ulMatching++; - } - #endif { uint16_t usFrameType = pxPacket->xUDPPacket.xEthernetHeader.usFrameType; IP_Address_t xIPAddressFrom; @@ -1216,13 +1159,11 @@ struct xIPv6_Couple * * @return The end-point found or NULL. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress, - uint32_t ulWhere ) + NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress ) { NetworkEndPoint_t * pxResult = NULL; ( void ) ulIPAddress; - ( void ) ulWhere; if( ( ulIPAddress == 0U ) || ( pxNetworkEndPoints->ipv4_settings.ulIPAddress == ulIPAddress ) ) { @@ -1265,10 +1206,9 @@ struct xIPv6_Couple * * @return An end-point that has the same network mask as the given IP-address. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ) + NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ) { - return FreeRTOS_InterfaceEndPointOnNetMask( NULL, ulIPAddress, ulWhere ); + return FreeRTOS_InterfaceEndPointOnNetMask( NULL, ulIPAddress ); } /*-----------------------------------------------------------*/ @@ -1337,13 +1277,11 @@ struct xIPv6_Couple * @return An end-point that has the same network mask as the given IP-address. */ NetworkEndPoint_t * FreeRTOS_InterfaceEndPointOnNetMask( const NetworkInterface_t * pxInterface, - uint32_t ulIPAddress, - uint32_t ulWhere ) + uint32_t ulIPAddress ) { NetworkEndPoint_t * pxResult = NULL; ( void ) pxInterface; - ( void ) ulWhere; if( ( ( ulIPAddress ^ pxNetworkEndPoints->ipv4_settings.ulIPAddress ) & pxNetworkEndPoints->ipv4_settings.ulNetMask ) == 0U ) { diff --git a/source/FreeRTOS_Sockets.c b/source/FreeRTOS_Sockets.c index 83d0cb045..a4ffaf389 100644 --- a/source/FreeRTOS_Sockets.c +++ b/source/FreeRTOS_Sockets.c @@ -1821,7 +1821,7 @@ static BaseType_t prvSocketBindAdd( FreeRTOS_Socket_t * pxSocket, #if ( ipconfigUSE_IPv4 != 0 ) if( pxAddress->sin_address.ulIP_IPv4 != FREERTOS_INADDR_ANY ) { - pxSocket->pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( pxAddress->sin_address.ulIP_IPv4, 7 ); + pxSocket->pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( pxAddress->sin_address.ulIP_IPv4 ); } else #endif /* ( ipconfigUSE_IPv4 != 0 ) */ diff --git a/source/FreeRTOS_TCP_Transmission.c b/source/FreeRTOS_TCP_Transmission.c index e05c998b7..306528c6e 100644 --- a/source/FreeRTOS_TCP_Transmission.c +++ b/source/FreeRTOS_TCP_Transmission.c @@ -759,7 +759,7 @@ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */ /* coverity[misra_c_2012_rule_11_3_violation] */ pxIPHeader = ( ( IPHeader_t * ) &( pxNetworkBuffer->pucEthernetBuffer[ ipSIZE_OF_ETH_HEADER ] ) ); - pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxIPHeader->ulDestinationIPAddress, 8 ); + pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxIPHeader->ulDestinationIPAddress ); if( pxNetworkBuffer->pxEndPoint == NULL ) { diff --git a/source/FreeRTOS_UDP_IPv4.c b/source/FreeRTOS_UDP_IPv4.c index ceed53e93..ac601d52d 100644 --- a/source/FreeRTOS_UDP_IPv4.c +++ b/source/FreeRTOS_UDP_IPv4.c @@ -274,7 +274,7 @@ void vProcessGeneratedUDPPacket_IPv4( NetworkBufferDescriptor_t * const pxNetwor /* 'ulIPAddress' might have become the address of the Gateway. * Find the route again. */ - pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxNetworkBuffer->xIPAddress.ulIP_IPv4, 11 ); + pxNetworkBuffer->pxEndPoint = FreeRTOS_FindEndPointOnNetMask( pxNetworkBuffer->xIPAddress.ulIP_IPv4 ); if( pxNetworkBuffer->pxEndPoint == NULL ) { diff --git a/source/include/FreeRTOSIPConfigDefaults.h b/source/include/FreeRTOSIPConfigDefaults.h index cf1a6ba7c..a442ec6e2 100644 --- a/source/include/FreeRTOSIPConfigDefaults.h +++ b/source/include/FreeRTOSIPConfigDefaults.h @@ -3056,22 +3056,6 @@ STATIC_ASSERT( ipconfigDNS_SEND_BLOCK_TIME_TICKS <= portMAX_DELAY ); /*---------------------------------------------------------------------------*/ -/* - * ipconfigHAS_ROUTING_STATISTICS - * - * Type: BaseType_t ( ipconfigENABLE | ipconfigDISABLE ) - */ - -#ifndef ipconfigHAS_ROUTING_STATISTICS - #define ipconfigHAS_ROUTING_STATISTICS ipconfigENABLE -#endif - -#if ( ( ipconfigHAS_ROUTING_STATISTICS != ipconfigDISABLE ) && ( ipconfigHAS_ROUTING_STATISTICS != ipconfigENABLE ) ) - #error Invalid ipconfigHAS_ROUTING_STATISTICS configuration -#endif - -/*---------------------------------------------------------------------------*/ - /*===========================================================================*/ /* ROUTING CONFIG */ /*===========================================================================*/ diff --git a/source/include/FreeRTOS_Routing.h b/source/include/FreeRTOS_Routing.h index 4a68bb319..106db7f91 100644 --- a/source/include/FreeRTOS_Routing.h +++ b/source/include/FreeRTOS_Routing.h @@ -265,8 +265,7 @@ /* * Find the end-point with given IP-address. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress, - uint32_t ulWhere ); + NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress ); #if ( ipconfigUSE_IPv6 != 0 ) /* Find the end-point with given IP-address. */ @@ -283,18 +282,14 @@ /* * Find the best fitting end-point to reach a given IP-address. * Find an end-point whose IP-address is in the same network as the IP-address provided. - * 'ulWhere' is temporary and or debugging only. */ - NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ); + NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ); /* * Find the best fitting IPv4 end-point to reach a given IP-address on a given interface - * 'ulWhere' is temporary and or debugging only. */ NetworkEndPoint_t * FreeRTOS_InterfaceEndPointOnNetMask( const NetworkInterface_t * pxInterface, - uint32_t ulIPAddress, - uint32_t ulWhere ); + uint32_t ulIPAddress ); /* * Finds an endpoint on the given interface which is in the same subnet as the @@ -345,21 +340,6 @@ const uint8_t ucMACAddress[ ipMAC_ADDRESS_LENGTH_BYTES ] ); #endif - #if ( ipconfigHAS_ROUTING_STATISTICS == 1 ) -/** @brief Some simple network statistics. */ - typedef struct xRoutingStats - { - UBaseType_t ulOnIp; /**< The number of times 'FreeRTOS_FindEndPointOnIP_IPv4()' has been called. */ - UBaseType_t ulOnMAC; /**< The number of times 'FreeRTOS_FindEndPointOnMAC()' has been called. */ - UBaseType_t ulOnNetMask; /**< The number of times 'FreeRTOS_InterfaceEndPointOnNetMask()' has been called. */ - UBaseType_t ulMatching; /**< The number of times 'FreeRTOS_MatchingEndpoint()' has been called. */ - UBaseType_t ulLocations[ 14 ]; /**< The number of times 'FreeRTOS_InterfaceEndPointOnNetMask()' has been called from a particular location. */ - UBaseType_t ulLocationsIP[ 8 ]; /**< The number of times 'FreeRTOS_FindEndPointOnIP_IPv4()' has been called from a particular location. */ - } RoutingStats_t; - - extern RoutingStats_t xRoutingStatistics; - #endif /* ( ipconfigHAS_ROUTING_STATISTICS == 1 ) */ - NetworkEndPoint_t * pxGetSocketEndpoint( ConstSocket_t xSocket ); void vSetSocketEndpoint( Socket_t xSocket, NetworkEndPoint_t * pxEndPoint ); diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c index 7be804559..f9cd7798a 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c +++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -27,8 +27,7 @@ NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask_IPv6( const IPv6_Address_t * /* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the * correctness of the proof */ -NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ) +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ) { /* Assume at least one end-point is available */ return pxNetworkEndPoint_Temp; diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/prepareReplyDNSMessage_harness.c b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/prepareReplyDNSMessage_harness.c index 851bd4474..d75332945 100644 --- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/prepareReplyDNSMessage_harness.c +++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/prepareReplyDNSMessage_harness.c @@ -53,8 +53,7 @@ NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask_IPv6( const IPv6_Address_t * /* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the * correctness of the proof */ -NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ) +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ) { /* Assume at least one end-point is available */ return pxNetworkEndPoint_Temp; diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c index e8c498ac9..5b926e4c4 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -65,8 +65,7 @@ void vNDRefreshCacheEntry( const MACAddress_t * pxMACAddress, __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint cannot be NULL" ); } -NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress, - uint32_t ulWhere ) +NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress ) { NetworkEndPoint_t * pxEndpoint = NULL; diff --git a/test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c b/test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c index dcb4e13dd..057d39619 100644 --- a/test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c +++ b/test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c @@ -2377,7 +2377,7 @@ void test_vARPAgeCache( void ) xARPCache[ ucEntryToCheck ].ulIPAddress = 0xAAAAAAAA; xARPCache[ ucEntryToCheck ].pxEndPoint = &xEndPoint; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( xARPCache[ ucEntryToCheck ].ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( xARPCache[ ucEntryToCheck ].ulIPAddress, &xEndPoint ); /* The function which calls 'pxGetNetworkBufferWithDescriptor' is 'FreeRTOS_OutputARPRequest'. * It doesn't return anything and will be tested separately. */ @@ -2400,7 +2400,7 @@ void test_vARPAgeCache( void ) /* Set an IP address */ xARPCache[ ucEntryToCheck ].ulIPAddress = 0xAAAAAAAA; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( xARPCache[ ucEntryToCheck ].ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( xARPCache[ ucEntryToCheck ].ulIPAddress, &xEndPoint ); /* The function which calls 'pxGetNetworkBufferWithDescriptor' is 'FreeRTOS_OutputARPRequest'. * It doesn't return anything and will be tested separately. */ @@ -2506,7 +2506,7 @@ void test_FreeRTOS_OutputARPRequest( void ) /* =================================================== */ - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); @@ -2519,7 +2519,7 @@ void test_FreeRTOS_OutputARPRequest( void ) xNetworkInterfaceOutput_ARP_STUB_CallCount = 0; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); @@ -2533,7 +2533,7 @@ void test_FreeRTOS_OutputARPRequest( void ) /* =================================================== */ xNetworkInterfaceOutput_ARP_STUB_CallCount = 0; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); xIsCallingFromIPTask_IgnoreAndReturn( pdFALSE ); @@ -2549,7 +2549,7 @@ void test_FreeRTOS_OutputARPRequest( void ) /* =================================================== */ xEndPoint.pxNetworkInterface = NULL; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); xIsCallingFromIPTask_IgnoreAndReturn( pdTRUE ); @@ -2564,7 +2564,7 @@ void test_FreeRTOS_OutputARPRequest( void ) /* =================================================== */ xNetworkBuffer.xDataLength = ( size_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); xIsCallingFromIPTask_IgnoreAndReturn( pdTRUE ); @@ -2580,7 +2580,7 @@ void test_FreeRTOS_OutputARPRequest( void ) /* =================================================== */ xEndPoint.bits.bIPv6 = 1; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); FreeRTOS_OutputARPRequest( ulIPAddress ); TEST_ASSERT_EQUAL( xNetworkInterfaceOutput_ARP_STUB_CallCount, 0 ); @@ -2592,7 +2592,7 @@ void test_FreeRTOS_OutputARPRequest( void ) xEndPoint.bits.bIPv6 = 0; xEndPoint.ipv4_settings.ulIPAddress = 0U; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); FreeRTOS_OutputARPRequest( ulIPAddress ); TEST_ASSERT_EQUAL( xNetworkInterfaceOutput_ARP_STUB_CallCount, 0 ); @@ -2606,7 +2606,7 @@ void test_FreeRTOS_OutputARPRequest_NullEndpoint( void ) { uint32_t ulIPAddress = 0x1234ABCD; - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, NULL ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, NULL ); FreeRTOS_OutputARPRequest( ulIPAddress ); } @@ -2687,7 +2687,7 @@ void test_xARPWaitResolution_GNWFailsNoTimeout( void ) /* Make sure that there are enough stubs for all the repetitive calls. */ for( i = 0; i < ipconfigMAX_ARP_RETRANSMISSIONS; i++ ) { - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, NULL ); vTaskDelay_Expect( pdMS_TO_TICKS( 250U ) ); FreeRTOS_FindEndPointOnIP_IPv4_ExpectAnyArgsAndReturn( NULL ); @@ -2738,7 +2738,7 @@ void test_xARPWaitResolution( void ) /* Make sure that there are enough stubs for all the repetitive calls. */ for( i = 0; i < ( ipconfigMAX_ARP_RETRANSMISSIONS - 1 ); i++ ) { - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, NULL ); vTaskDelay_Expect( pdMS_TO_TICKS( 250U ) ); FreeRTOS_FindEndPointOnIP_IPv4_ExpectAnyArgsAndReturn( NULL ); @@ -2747,7 +2747,7 @@ void test_xARPWaitResolution( void ) xTaskCheckForTimeOut_IgnoreAndReturn( pdFALSE ); } - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, NULL ); vTaskDelay_Expect( pdMS_TO_TICKS( 250U ) ); FreeRTOS_FindEndPointOnIP_IPv4_ExpectAnyArgsAndReturn( NULL ); @@ -2786,7 +2786,7 @@ void test_xARPWaitResolution( void ) /* Make sure that there are enough stubs for all the repetitive calls. */ for( i = 0; i < ( ipconfigMAX_ARP_RETRANSMISSIONS - 2 ); i++ ) { - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, NULL ); vTaskDelay_Expect( pdMS_TO_TICKS( 250U ) ); FreeRTOS_FindEndPointOnIP_IPv4_ExpectAnyArgsAndReturn( NULL ); @@ -2795,7 +2795,7 @@ void test_xARPWaitResolution( void ) xTaskCheckForTimeOut_IgnoreAndReturn( pdFALSE ); } - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, NULL ); vTaskDelay_Expect( pdMS_TO_TICKS( 250U ) ); FreeRTOS_FindEndPointOnIP_IPv4_ExpectAnyArgsAndReturn( NULL ); diff --git a/test/unit-test/FreeRTOS_ARP_DataLenLessThanMinPacket/FreeRTOS_ARP_DataLenLessThanMinPacket_utest.c b/test/unit-test/FreeRTOS_ARP_DataLenLessThanMinPacket/FreeRTOS_ARP_DataLenLessThanMinPacket_utest.c index 34b55c43b..75b551501 100644 --- a/test/unit-test/FreeRTOS_ARP_DataLenLessThanMinPacket/FreeRTOS_ARP_DataLenLessThanMinPacket_utest.c +++ b/test/unit-test/FreeRTOS_ARP_DataLenLessThanMinPacket/FreeRTOS_ARP_DataLenLessThanMinPacket_utest.c @@ -54,7 +54,7 @@ void test_FreeRTOS_OutputARPRequest_MinimumPacketSizeLessThanARPPacket( void ) /* =================================================== */ - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, 12, &xEndPoint ); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( ulIPAddress, &xEndPoint ); pxGetNetworkBufferWithDescriptor_ExpectAndReturn( sizeof( ARPPacket_t ), 0, &xNetworkBuffer ); xIsCallingFromIPTask_IgnoreAndReturn( pdTRUE ); diff --git a/test/unit-test/FreeRTOS_Routing/FreeRTOSIPConfig.h b/test/unit-test/FreeRTOS_Routing/FreeRTOSIPConfig.h index 317cc58ab..a3ed8a1a0 100644 --- a/test/unit-test/FreeRTOS_Routing/FreeRTOSIPConfig.h +++ b/test/unit-test/FreeRTOS_Routing/FreeRTOSIPConfig.h @@ -40,8 +40,6 @@ #define ipconfigCOMPATIBLE_WITH_SINGLE ( 0 ) -#define ipconfigHAS_ROUTING_STATISTICS ( 1 ) - /* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to * 1 then FreeRTOS_debug_printf should be defined to the function used to print * out the debugging messages. */ diff --git a/test/unit-test/FreeRTOS_Routing/FreeRTOS_Routing_utest.c b/test/unit-test/FreeRTOS_Routing/FreeRTOS_Routing_utest.c index 4275506bf..8887519ba 100644 --- a/test/unit-test/FreeRTOS_Routing/FreeRTOS_Routing_utest.c +++ b/test/unit-test/FreeRTOS_Routing/FreeRTOS_Routing_utest.c @@ -65,7 +65,6 @@ /* Default IPv4 netmask is 192.168.123.1, which is 0x017BA8C0. */ #define IPV4_DEFAULT_DNS_SERVER ( 0x017BA8C0 ) -extern RoutingStats_t xRoutingStatistics; const struct xIPv6_Address FreeRTOS_in6addr_any; const struct xIPv6_Address FreeRTOS_in6addr_loopback; @@ -1331,7 +1330,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_HappyPath( void ) pxNetworkEndPoints = &xEndPoint; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -1352,7 +1351,6 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_NotFound( void ) { NetworkEndPoint_t xEndPoint[ 2 ]; NetworkEndPoint_t * pxEndPoint = NULL; - uint32_t ulWhere; /* Initialize e0. */ memset( &xEndPoint[ 0 ], 0, sizeof( NetworkEndPoint_t ) ); @@ -1365,9 +1363,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_NotFound( void ) xEndPoint[ 1 ].bits.bIPv6 = pdTRUE; pxNetworkEndPoints->pxNext = &xEndPoint[ 1 ]; - /* Set ulWhere to boundary of array size to toggle corner case. */ - ulWhere = sizeof( xRoutingStatistics.ulLocationsIP ) / sizeof( xRoutingStatistics.ulLocationsIP[ 0 ] ); - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY, ulWhere ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -1399,13 +1395,13 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_MultipleEndpoints( void ) xEndPoint[ 1 ].ipv4_settings.ulIPAddress = IPV4_DEFAULT_GATEWAY; pxNetworkEndPoints->pxNext = &xEndPoint[ 1 ]; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS ); TEST_ASSERT_EQUAL( &xEndPoint[ 0 ], pxEndPoint ); - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY ); TEST_ASSERT_EQUAL( &xEndPoint[ 1 ], pxEndPoint ); - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_DNS_SERVER, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -1433,7 +1429,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_AnyEndpoint( void ) xEndPoint[ 1 ].ipv4_settings.ulIPAddress = IPV4_DEFAULT_GATEWAY; pxNetworkEndPoints->pxNext = &xEndPoint[ 1 ]; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( 0, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( 0 ); TEST_ASSERT_EQUAL( &xEndPoint[ 0 ], pxEndPoint ); } @@ -1459,9 +1455,9 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_ZeroAddressEndpoint( void ) xEndPoint.ipv4_settings.ulIPAddress = 0; pxNetworkEndPoints = &xEndPoint; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -1794,7 +1790,7 @@ void test_FreeRTOS_FindEndPointOnNetMask_HappyPath( void ) pxNetworkEndPoints = &xEndPoint; /* IPV4_DEFAULT_DNS_SERVER is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( IPV4_DEFAULT_DNS_SERVER, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -1823,7 +1819,7 @@ void test_FreeRTOS_FindEndPointOnNetMask_NotFound( void ) pxNetworkEndPoints = &xEndPoint; /* 192.168.1.1 is 0x0101A8C0. */ - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( 0x0101A8C0, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( 0x0101A8C0 ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -1921,7 +1917,6 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_HappyPath( void ) NetworkEndPoint_t xEndPoint; NetworkEndPoint_t * pxEndPoint = NULL; NetworkInterface_t xNetworkInterface; - uint32_t ulWhere; /* Initialize network interface and add it to the list. */ memset( &xNetworkInterface, 0, sizeof( NetworkInterface_t ) ); @@ -1934,10 +1929,8 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_HappyPath( void ) xEndPoint.pxNetworkInterface = &xNetworkInterface; pxNetworkEndPoints = &xEndPoint; - /* Set ulWhere to boundary of array size to toggle corner case. */ - ulWhere = sizeof( xRoutingStatistics.ulLocations ) / sizeof( xRoutingStatistics.ulLocations[ 0 ] ); /* IPV4_DEFAULT_ADDRESS is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER, ulWhere ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -1964,7 +1957,6 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_DifferentInterface( void ) NetworkEndPoint_t xEndPoint[ 2 ]; NetworkEndPoint_t * pxEndPoint = NULL; NetworkInterface_t xNetworkInterface[ 2 ]; - uint32_t ulWhere; /* 192.168.124.223 is 0xDF7CA8C0. */ uint32_t ulE1IPAddress = 0xDF7CA8C0; /* 192.168.124.1 is 0x017CA8C0. */ @@ -1990,10 +1982,8 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_DifferentInterface( void ) xEndPoint[ 1 ].pxNetworkInterface = &xNetworkInterface[ 1 ]; pxNetworkEndPoints->pxNext = &xEndPoint[ 1 ]; - /* Set ulWhere to boundary of array size to toggle corner case. */ - ulWhere = sizeof( xRoutingStatistics.ulLocations ) / sizeof( xRoutingStatistics.ulLocations[ 0 ] ); /* IPV4_DEFAULT_ADDRESS is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface[ 1 ], ulQueryIPAddress, ulWhere ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface[ 1 ], ulQueryIPAddress ); TEST_ASSERT_EQUAL( &xEndPoint[ 1 ], pxEndPoint ); } @@ -2031,7 +2021,7 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_NotFound( void ) pxNetworkEndPoints = &xEndPoint; /* IPV4_DEFAULT_ADDRESS is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER, 0 ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -2078,7 +2068,7 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_Broadcast( void ) pxNetworkEndPoints->pxNext = &xEndPoint[ 1 ]; /* IPV4_DEFAULT_ADDRESS is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, 0xFFFFFFFF, 0 ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, 0xFFFFFFFF ); TEST_ASSERT_EQUAL( &xEndPoint[ 1 ], pxEndPoint ); } diff --git a/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOSIPConfig.h b/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOSIPConfig.h index 9d550f5d2..2f38e010f 100644 --- a/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOSIPConfig.h +++ b/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOSIPConfig.h @@ -42,8 +42,6 @@ #define ipconfigCOMPATIBLE_WITH_SINGLE ( 1 ) -#define ipconfigHAS_ROUTING_STATISTICS ( 0 ) - #define ipconfigPROCESS_CUSTOM_ETHERNET_FRAMES ( 0 ) /* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to diff --git a/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOS_Routing_ConfigCompatibleWithSingle_utest.c b/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOS_Routing_ConfigCompatibleWithSingle_utest.c index 4b3145f32..0ab121e62 100644 --- a/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOS_Routing_ConfigCompatibleWithSingle_utest.c +++ b/test/unit-test/FreeRTOS_Routing_ConfigCompatibleWithSingle/FreeRTOS_Routing_ConfigCompatibleWithSingle_utest.c @@ -740,7 +740,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_HappyPath( void ) pxNetworkEndPoints = &xEndPoint; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_ADDRESS ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -766,7 +766,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_NotFound( void ) xEndPoint.ipv4_settings.ulIPAddress = IPV4_DEFAULT_ADDRESS; pxNetworkEndPoints = &xEndPoint; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( IPV4_DEFAULT_GATEWAY ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -790,7 +790,7 @@ void test_FreeRTOS_FindEndPointOnIP_IPv4_AnyEndpoint( void ) xEndPoint.ipv4_settings.ulIPAddress = IPV4_DEFAULT_ADDRESS; pxNetworkEndPoints = &xEndPoint; - pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( 0, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnIP_IPv4( 0 ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -917,7 +917,7 @@ void test_FreeRTOS_FindEndPointOnNetMask_HappyPath( void ) pxNetworkEndPoints = &xEndPoint; /* IPV4_DEFAULT_DNS_SERVER is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( IPV4_DEFAULT_DNS_SERVER, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -946,7 +946,7 @@ void test_FreeRTOS_FindEndPointOnNetMask_NotFound( void ) pxNetworkEndPoints = &xEndPoint; /* 192.168.1.1 is 0x0101A8C0. */ - pxEndPoint = FreeRTOS_FindEndPointOnNetMask( 0x0101A8C0, 0 ); + pxEndPoint = FreeRTOS_FindEndPointOnNetMask( 0x0101A8C0 ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } @@ -981,7 +981,7 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_HappyPath( void ) pxNetworkEndPoints = &xEndPoint; /* IPV4_DEFAULT_ADDRESS is 192.168.123.1 within the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER, 0 ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, IPV4_DEFAULT_DNS_SERVER ); TEST_ASSERT_EQUAL( &xEndPoint, pxEndPoint ); } @@ -1016,7 +1016,7 @@ void test_FreeRTOS_InterfaceEndPointOnNetMask_NotFound( void ) pxNetworkEndPoints = &xEndPoint; /* 192.168.122.1 is not in the network region. */ - pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, 0x017AA8C0, 0 ); + pxEndPoint = FreeRTOS_InterfaceEndPointOnNetMask( &xNetworkInterface, 0x017AA8C0 ); TEST_ASSERT_EQUAL( NULL, pxEndPoint ); } diff --git a/test/unit-test/FreeRTOS_Routing_ConfigV4Only/FreeRTOSIPConfig.h b/test/unit-test/FreeRTOS_Routing_ConfigV4Only/FreeRTOSIPConfig.h index 47838e9c6..53c48bdef 100644 --- a/test/unit-test/FreeRTOS_Routing_ConfigV4Only/FreeRTOSIPConfig.h +++ b/test/unit-test/FreeRTOS_Routing_ConfigV4Only/FreeRTOSIPConfig.h @@ -44,8 +44,6 @@ #define ipconfigCOMPATIBLE_WITH_SINGLE ( 0 ) -#define ipconfigHAS_ROUTING_STATISTICS ( 1 ) - #define ipconfigPROCESS_CUSTOM_ETHERNET_FRAMES ( 1 ) /* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to diff --git a/test/unit-test/FreeRTOS_TCP_Transmission/TCP_Transmission_list_macros.h b/test/unit-test/FreeRTOS_TCP_Transmission/TCP_Transmission_list_macros.h index b59f487a7..1db6ff432 100644 --- a/test/unit-test/FreeRTOS_TCP_Transmission/TCP_Transmission_list_macros.h +++ b/test/unit-test/FreeRTOS_TCP_Transmission/TCP_Transmission_list_macros.h @@ -50,9 +50,7 @@ NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv6( const IPv6_Address_t * pxIPA /* * Find the best fitting end-point to reach a given IP-address. * Find an end-point whose IP-address is in the same network as the IP-address provided. - * 'ulWhere' is temporary and or debugging only. */ -NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ); +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ); #endif /* ifndef LIST_MACRO_H */ diff --git a/test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_list_macros.h b/test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_list_macros.h index a520eec33..0342e9d1e 100644 --- a/test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_list_macros.h +++ b/test/unit-test/FreeRTOS_UDP_IP/FreeRTOS_UDP_IP_list_macros.h @@ -86,6 +86,6 @@ BaseType_t xProcessReceivedUDPPacket_IPv6( NetworkBufferDescriptor_t * pxNetwork uint16_t usPort, BaseType_t * pxIsWaitingForARPResolution ); -NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress, - uint32_t ulWhere ); +NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress ); + #endif /* ifndef LIST_MACRO_H */ diff --git a/test/unit-test/FreeRTOS_UDP_IPv4/FreeRTOS_UDP_IPv4_utest.c b/test/unit-test/FreeRTOS_UDP_IPv4/FreeRTOS_UDP_IPv4_utest.c index 04e860be8..1df9d111a 100644 --- a/test/unit-test/FreeRTOS_UDP_IPv4/FreeRTOS_UDP_IPv4_utest.c +++ b/test/unit-test/FreeRTOS_UDP_IPv4/FreeRTOS_UDP_IPv4_utest.c @@ -1658,8 +1658,7 @@ void test_vProcessGeneratedUDPPacket_IPv4_UDPCacheMissEndPointFound() eARPGetCacheEntry_IgnoreArg_pulIPAddress(); vARPRefreshCacheEntry_Expect( NULL, pxNetworkBuffer->xIPAddress.ulIP_IPv4, NULL ); - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( pxNetworkBuffer->xIPAddress.ulIP_IPv4, 0, pxEndPoint ); - FreeRTOS_FindEndPointOnNetMask_IgnoreArg_ulWhere(); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( pxNetworkBuffer->xIPAddress.ulIP_IPv4, pxEndPoint ); vARPGenerateRequestPacket_Expect( pxNetworkBuffer ); @@ -1691,8 +1690,7 @@ void test_vProcessGeneratedUDPPacket_IPv4_UDPCacheMissEndPointNotFound() eARPGetCacheEntry_IgnoreArg_pulIPAddress(); vARPRefreshCacheEntry_Expect( NULL, pxNetworkBuffer->xIPAddress.ulIP_IPv4, NULL ); - FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( pxNetworkBuffer->xIPAddress.ulIP_IPv4, 0, NULL ); - FreeRTOS_FindEndPointOnNetMask_IgnoreArg_ulWhere(); + FreeRTOS_FindEndPointOnNetMask_ExpectAndReturn( pxNetworkBuffer->xIPAddress.ulIP_IPv4, NULL ); vReleaseNetworkBufferAndDescriptor_Expect( pxNetworkBuffer ); vProcessGeneratedUDPPacket_IPv4( pxNetworkBuffer ); From 782a7e5e83ed520d2d88fee6d5d0e1d290c8674c Mon Sep 17 00:00:00 2001 From: Holden <68555040+HTRamsey@users.noreply.github.com> Date: Wed, 31 Jul 2024 18:19:50 -0700 Subject: [PATCH 4/5] Improve frame filtering (#1100) * add checks for frame types * address review comments * Fix multicast filtering and finding endpoint * Remove ipCONSIDER_FRAME_FOR_PROCESSING macro * add ipv4 multicast frame check * make tests finish compiling * fix tests * use multicast macros * improve test coverage * Uncrustify: triggered by comment. * Fix unit test to have full coverage * Fix spell check and formatting * Define macro to check ethernet frame type. * Remove unnecessary declaration of xMDNS_MACAddressIPv6. * Replace all usage of xMDNS_MACAddressIPv6 with xMDNS_MacAddressIPv6. --------- Co-authored-by: GitHub Action Co-authored-by: ActoryOu Co-authored-by: Monika Singh --- source/FreeRTOS_DNS.c | 104 +++---- source/FreeRTOS_IP.c | 216 +++++++++----- source/FreeRTOS_IPv4_Utils.c | 6 +- source/FreeRTOS_IPv6_Utils.c | 4 +- source/include/FreeRTOS_DNS.h | 46 ++- source/include/FreeRTOS_IPv4.h | 5 + test/unit-test/ConfigFiles/FreeRTOSIPConfig.h | 1 + .../FreeRTOS_DNS_Callback_utest.c | 76 +++++ .../unit-test/FreeRTOS_IP/FreeRTOS_IP_stubs.c | 6 + .../unit-test/FreeRTOS_IP/FreeRTOS_IP_utest.c | 271 +++++++++++++++++- .../FreeRTOS_IP_DiffConfig_stubs.c | 8 +- .../FreeRTOS_IP_DiffConfig1_stubs.c | 8 +- .../FreeRTOS_IP_DiffConfig1_utest.c | 23 ++ .../FreeRTOSIPConfig.h | 3 +- .../FreeRTOS_IP_DiffConfig2_stubs.c | 6 + .../FreeRTOS_IP_DiffConfig2_utest.c | 112 ++++++++ .../FreeRTOS_IP_DiffConfig3_stubs.c | 6 + 17 files changed, 715 insertions(+), 186 deletions(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index f3eca7605..82e2c6dbf 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -57,6 +57,48 @@ #include "FreeRTOS_DNS_Callback.h" +/** @brief The MAC address used for LLMNR. */ +const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; + +/** @brief The IPv6 link-scope multicast MAC address */ +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +/** @brief The IPv6 link-scope multicast address */ +const IPv6_Address_t ipLLMNR_IP_ADDR_IPv6 = +{ + { /* ff02::1:3 */ + 0xff, 0x02, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x01, + 0x00, 0x03, + } +}; + +/** @brief The MAC address used for MDNS. */ +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +/** @brief The IPv6 multicast DNS MAC address. */ +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; + +/** @brief multicast DNS IPv6 address */ +const IPv6_Address_t ipMDNS_IP_ADDR_IPv6 = +{ + { /* ff02::fb */ + 0xff, 0x02, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0x00, + 0x00, 0xfb, + } +}; + /* Exclude the entire file if DNS is not enabled. */ #if ( ipconfigUSE_DNS != 0 ) @@ -95,69 +137,7 @@ struct freertos_addrinfo ** ppxAddressInfo, BaseType_t xFamily ); - #if ( ipconfigUSE_LLMNR == 1 ) - /** @brief The MAC address used for LLMNR. */ - const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; - #endif /* ipconfigUSE_LLMNR == 1 */ - /*-----------------------------------------------------------*/ - #if ( ipconfigUSE_LLMNR == 1 ) && ( ipconfigUSE_IPv6 != 0 ) - -/** - * @brief The IPv6 link-scope multicast address - */ - const IPv6_Address_t ipLLMNR_IP_ADDR_IPv6 = - { - { /* ff02::1:3 */ - 0xff, 0x02, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x01, - 0x00, 0x03, - } - }; - -/** - * @brief The IPv6 link-scope multicast MAC address - */ - const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; - #endif /* ipconfigUSE_LLMNR && ipconfigUSE_IPv6 */ - - #if ( ipconfigUSE_MDNS == 1 ) && ( ipconfigUSE_IPv6 != 0 ) - -/** - * @brief multicast DNS IPv6 address - */ - const IPv6_Address_t ipMDNS_IP_ADDR_IPv6 = - { - { /* ff02::fb */ - 0xff, 0x02, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0x00, - 0x00, 0xfb, - } - }; - -/** - * @brief The IPv6 multicast DNS MAC address. - * The MAC-addresses are provided here in case a network - * interface needs it. - */ - const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; - #endif /* ( ipconfigUSE_MDNS == 1 ) && ( ipconfigUSE_IPv6 != 0 ) */ - - - #if ( ipconfigUSE_MDNS == 1 ) - /** @brief The MAC address used for MDNS. */ - const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; - #endif /* ipconfigUSE_MDNS == 1 */ /** @brief This global variable is being used to indicate to the driver which IP type * is preferred for name service lookup, either IPv6 or IPv4. */ diff --git a/source/FreeRTOS_IP.c b/source/FreeRTOS_IP.c index aadf73be2..607bc8fdc 100644 --- a/source/FreeRTOS_IP.c +++ b/source/FreeRTOS_IP.c @@ -92,19 +92,11 @@ #endif #endif -/** @brief If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1, then the Ethernet - * driver will filter incoming packets and only pass the stack those packets it - * considers need processing. In this case ipCONSIDER_FRAME_FOR_PROCESSING() can - * be #-defined away. If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 0 - * then the Ethernet driver will pass all received packets to the stack, and the - * stack must do the filtering itself. In this case ipCONSIDER_FRAME_FOR_PROCESSING - * needs to call eConsiderFrameForProcessing. - */ -#if ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES == 0 - #define ipCONSIDER_FRAME_FOR_PROCESSING( pucEthernetBuffer ) eConsiderFrameForProcessing( ( pucEthernetBuffer ) ) -#else - #define ipCONSIDER_FRAME_FOR_PROCESSING( pucEthernetBuffer ) eProcessBuffer -#endif +/** @brief The frame type field in the Ethernet header must have a value greater than 0x0600. + * If the configuration option ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is enabled, the stack + * will discard packets with a frame type value less than or equal to 0x0600. + * However, if this option is disabled, the stack will continue to process these packets. */ +#define ipIS_ETHERNET_FRAME_TYPE_INVALID( usFrameType ) ( ( usFrameType ) <= 0x0600U ) static void prvCallDHCP_RA_Handler( NetworkEndPoint_t * pxEndPoint ); @@ -1451,85 +1443,165 @@ BaseType_t xSendEventStructToIPTask( const IPStackEvent_t * pxEvent, */ eFrameProcessingResult_t eConsiderFrameForProcessing( const uint8_t * const pucEthernetBuffer ) { - eFrameProcessingResult_t eReturn = eProcessBuffer; - const EthernetHeader_t * pxEthernetHeader = NULL; - const NetworkEndPoint_t * pxEndPoint = NULL; + eFrameProcessingResult_t eReturn = eReleaseBuffer; - if( pucEthernetBuffer == NULL ) - { - eReturn = eReleaseBuffer; - } - else + do { - /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + const EthernetHeader_t * pxEthernetHeader = NULL; + const NetworkEndPoint_t * pxEndPoint = NULL; + uint16_t usFrameType; + + /* First, check the packet buffer is non-null. */ + if( pucEthernetBuffer == NULL ) + { + /* The packet buffer was null - release it. */ + break; + } + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ /* MISRA Ref 11.3.1 [Misaligned access] */ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */ /* coverity[misra_c_2012_rule_11_3_violation] */ pxEthernetHeader = ( ( const EthernetHeader_t * ) pucEthernetBuffer ); + usFrameType = pxEthernetHeader->usFrameType; - /* Examine the destination MAC from the Ethernet header to see if it matches - * that of an end point managed by FreeRTOS+TCP. */ + /* Second, filter based on ethernet frame type. */ + /* The frame type field in the Ethernet header must have a value greater than 0x0600. */ + if( ipIS_ETHERNET_FRAME_TYPE_INVALID( FreeRTOS_ntohs( usFrameType ) ) ) + { + /* The packet was not an Ethernet II frame */ + #if ipconfigIS_ENABLED( ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES ) + /* filtering is enabled - release it. */ + break; + #else + /* filtering is disabled - continue filter checks. */ + #endif + } + else if( usFrameType == ipARP_FRAME_TYPE ) + { + /* The frame is an ARP type */ + #if ipconfigIS_DISABLED( ipconfigUSE_IPv4 ) + /* IPv4 is disabled - release it. */ + break; + #else + /* IPv4 is enabled - Continue filter checks. */ + #endif + } + else if( usFrameType == ipIPv4_FRAME_TYPE ) + { + /* The frame is an IPv4 type */ + #if ipconfigIS_DISABLED( ipconfigUSE_IPv4 ) + /* IPv4 is disabled - release it. */ + break; + #else + /* IPv4 is enabled - Continue filter checks. */ + #endif + } + else if( usFrameType == ipIPv6_FRAME_TYPE ) + { + /* The frame is an IPv6 type */ + #if ipconfigIS_DISABLED( ipconfigUSE_IPv6 ) + /* IPv6 is disabled - release it. */ + break; + #else + /* IPv6 is enabled - Continue filter checks. */ + #endif + } + else + { + /* The frame is an unsupported Ethernet II type */ + #if ipconfigIS_DISABLED( ipconfigPROCESS_CUSTOM_ETHERNET_FRAMES ) + /* Processing custom ethernet frames is disabled - release it. */ + break; + #else + /* Processing custom ethernet frames is enabled - Continue filter checks. */ + #endif + } + + /* Third, filter based on destination mac address. */ pxEndPoint = FreeRTOS_FindEndPointOnMAC( &( pxEthernetHeader->xDestinationAddress ), NULL ); if( pxEndPoint != NULL ) { - /* The packet was directed to this node - process it. */ - eReturn = eProcessBuffer; + /* A destination endpoint was found - Continue filter checks. */ } else if( memcmp( xBroadcastMACAddress.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) { - /* The packet was a broadcast - process it. */ - eReturn = eProcessBuffer; + /* The packet was a broadcast - Continue filter checks. */ } - else - #if ( ( ipconfigUSE_LLMNR == 1 ) && ( ipconfigUSE_DNS != 0 ) ) - if( memcmp( xLLMNR_MacAddress.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) - { - /* The packet is a request for LLMNR - process it. */ - eReturn = eProcessBuffer; - } - else - #endif /* ipconfigUSE_LLMNR */ - #if ( ( ipconfigUSE_MDNS == 1 ) && ( ipconfigUSE_DNS != 0 ) ) - if( memcmp( xMDNS_MacAddress.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) - { - /* The packet is a request for MDNS - process it. */ - eReturn = eProcessBuffer; - } - else - #endif /* ipconfigUSE_MDNS */ - if( ( pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] == ipMULTICAST_MAC_ADDRESS_IPv6_0 ) && - ( pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] == ipMULTICAST_MAC_ADDRESS_IPv6_1 ) ) + else if( memcmp( xLLMNR_MacAddress.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) { - /* The packet is a request for LLMNR - process it. */ - eReturn = eProcessBuffer; + /* The packet is a request for LLMNR using IPv4 */ + #if ( ipconfigIS_DISABLED( ipconfigUSE_DNS ) || ipconfigIS_DISABLED( ipconfigUSE_LLMNR ) || ipconfigIS_DISABLED( ipconfigUSE_IPv4 ) ) + /* DNS, LLMNR, or IPv4 is disabled - release it. */ + break; + #else + /* DNS, LLMNR, and IPv4 are enabled - Continue filter checks. */ + #endif } - else + else if( memcmp( xLLMNR_MacAddressIPv6.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) { - /* The packet was not a broadcast, or for this node, just release - * the buffer without taking any other action. */ - eReturn = eReleaseBuffer; + /* The packet is a request for LLMNR using IPv6 */ + #if ( ipconfigIS_DISABLED( ipconfigUSE_DNS ) || ipconfigIS_DISABLED( ipconfigUSE_LLMNR ) || ipconfigIS_DISABLED( ipconfigUSE_IPv6 ) ) + /* DNS, LLMNR, or IPv6 is disabled - release it. */ + break; + #else + /* DNS, LLMNR, and IPv6 are enabled - Continue filter checks. */ + #endif } - } - - #if ( ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES == 1 ) - { - uint16_t usFrameType; - - if( eReturn == eProcessBuffer ) + else if( memcmp( xMDNS_MacAddress.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) { - usFrameType = pxEthernetHeader->usFrameType; - usFrameType = FreeRTOS_ntohs( usFrameType ); - - if( usFrameType <= 0x600U ) - { - /* Not an Ethernet II frame. */ - eReturn = eReleaseBuffer; - } + /* The packet is a request for MDNS using IPv4 */ + #if ( ipconfigIS_DISABLED( ipconfigUSE_DNS ) || ipconfigIS_DISABLED( ipconfigUSE_MDNS ) || ipconfigIS_DISABLED( ipconfigUSE_IPv4 ) ) + /* DNS, MDNS, or IPv4 is disabled - release it. */ + break; + #else + /* DNS, MDNS, and IPv4 are enabled - Continue filter checks. */ + #endif + } + else if( memcmp( xMDNS_MacAddressIPv6.ucBytes, pxEthernetHeader->xDestinationAddress.ucBytes, sizeof( MACAddress_t ) ) == 0 ) + { + /* The packet is a request for MDNS using IPv6 */ + #if ( ipconfigIS_DISABLED( ipconfigUSE_DNS ) || ipconfigIS_DISABLED( ipconfigUSE_MDNS ) || ipconfigIS_DISABLED( ipconfigUSE_IPv6 ) ) + /* DNS, MDNS, or IPv6 is disabled - release it. */ + break; + #else + /* DNS, MDNS, and IPv6 are enabled - Continue filter checks. */ + #endif + } + else if( ( pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] == ipMULTICAST_MAC_ADDRESS_IPv4_0 ) && + ( pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] == ipMULTICAST_MAC_ADDRESS_IPv4_1 ) && + ( pxEthernetHeader->xDestinationAddress.ucBytes[ 2 ] == ipMULTICAST_MAC_ADDRESS_IPv4_2 ) && + ( pxEthernetHeader->xDestinationAddress.ucBytes[ 3 ] <= 0x7fU ) ) + { + /* The packet is an IPv4 Multicast */ + #if ipconfigIS_DISABLED( ipconfigUSE_IPv4 ) + /* IPv4 is disabled - release it. */ + break; + #else + /* IPv4 is enabled - Continue filter checks. */ + #endif + } + else if( ( pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] == ipMULTICAST_MAC_ADDRESS_IPv6_0 ) && + ( pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] == ipMULTICAST_MAC_ADDRESS_IPv6_1 ) ) + { + /* The packet is an IPv6 Multicast */ + #if ipconfigIS_DISABLED( ipconfigUSE_IPv6 ) + /* IPv6 is disabled - release it. */ + break; + #else + /* IPv6 is enabled - Continue filter checks. */ + #endif + } + else + { + /* The packet was not a broadcast, or for this node - release it */ + break; } - } - #endif /* ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES == 1 */ + + /* All checks have been passed, process the packet. */ + eReturn = eProcessBuffer; + } while( ipFALSE_BOOL ); return eReturn; } @@ -1575,8 +1647,6 @@ static void prvProcessEthernetPacket( NetworkBufferDescriptor_t * const pxNetwor break; } - eReturned = ipCONSIDER_FRAME_FOR_PROCESSING( pxNetworkBuffer->pucEthernetBuffer ); - /* Map the buffer onto the Ethernet Header struct for easy access to the fields. */ /* MISRA Ref 11.3.1 [Misaligned access] */ @@ -1586,7 +1656,7 @@ static void prvProcessEthernetPacket( NetworkBufferDescriptor_t * const pxNetwor /* The condition "eReturned == eProcessBuffer" must be true. */ #if ( ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES == 0 ) - if( eReturned == eProcessBuffer ) + if( eConsiderFrameForProcessing( pxNetworkBuffer->pucEthernetBuffer ) == eProcessBuffer ) #endif { /* Interpret the received Ethernet packet. */ diff --git a/source/FreeRTOS_IPv4_Utils.c b/source/FreeRTOS_IPv4_Utils.c index b79bdc8de..f7c1d3f84 100644 --- a/source/FreeRTOS_IPv4_Utils.c +++ b/source/FreeRTOS_IPv4_Utils.c @@ -59,9 +59,9 @@ void vSetMultiCastIPv4MacAddress( uint32_t ulIPAddress, { uint32_t ulIP = FreeRTOS_ntohl( ulIPAddress ); - pxMACAddress->ucBytes[ 0 ] = ( uint8_t ) 0x01U; - pxMACAddress->ucBytes[ 1 ] = ( uint8_t ) 0x00U; - pxMACAddress->ucBytes[ 2 ] = ( uint8_t ) 0x5EU; + pxMACAddress->ucBytes[ 0 ] = ( uint8_t ) ipMULTICAST_MAC_ADDRESS_IPv4_0; + pxMACAddress->ucBytes[ 1 ] = ( uint8_t ) ipMULTICAST_MAC_ADDRESS_IPv4_1; + pxMACAddress->ucBytes[ 2 ] = ( uint8_t ) ipMULTICAST_MAC_ADDRESS_IPv4_2; pxMACAddress->ucBytes[ 3 ] = ( uint8_t ) ( ( ulIP >> 16 ) & 0x7fU ); /* Use 7 bits. */ pxMACAddress->ucBytes[ 4 ] = ( uint8_t ) ( ( ulIP >> 8 ) & 0xffU ); /* Use 8 bits. */ pxMACAddress->ucBytes[ 5 ] = ( uint8_t ) ( ( ulIP ) & 0xffU ); /* Use 8 bits. */ diff --git a/source/FreeRTOS_IPv6_Utils.c b/source/FreeRTOS_IPv6_Utils.c index f35995bb5..9e9f2abd6 100644 --- a/source/FreeRTOS_IPv6_Utils.c +++ b/source/FreeRTOS_IPv6_Utils.c @@ -55,8 +55,8 @@ void vSetMultiCastIPv6MacAddress( const IPv6_Address_t * pxAddress, MACAddress_t * pxMACAddress ) { - pxMACAddress->ucBytes[ 0 ] = 0x33U; - pxMACAddress->ucBytes[ 1 ] = 0x33U; + pxMACAddress->ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv6_0; + pxMACAddress->ucBytes[ 1 ] = ipMULTICAST_MAC_ADDRESS_IPv6_1; pxMACAddress->ucBytes[ 2 ] = pxAddress->ucBytes[ 12 ]; pxMACAddress->ucBytes[ 3 ] = pxAddress->ucBytes[ 13 ]; pxMACAddress->ucBytes[ 4 ] = pxAddress->ucBytes[ 14 ]; diff --git a/source/include/FreeRTOS_DNS.h b/source/include/FreeRTOS_DNS.h index c69db0e93..830e1ae2b 100644 --- a/source/include/FreeRTOS_DNS.h +++ b/source/include/FreeRTOS_DNS.h @@ -41,43 +41,28 @@ #endif /* *INDENT-ON* */ -/* - * LLMNR is very similar to DNS, so is handled by the DNS routines. - */ -uint32_t ulDNSHandlePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ); - -#if ( ipconfigUSE_LLMNR == 1 ) - /* The LLMNR MAC address is 01:00:5e:00:00:fc */ - extern const MACAddress_t xLLMNR_MacAddress; -#endif /* ipconfigUSE_LLMNR */ - -#if ( ipconfigUSE_LLMNR == 1 ) && ( ipconfigUSE_IPv6 != 0 ) - -/* The LLMNR IPv6 address is ff02::1:3 */ - extern const IPv6_Address_t ipLLMNR_IP_ADDR_IPv6; +/* The LLMNR MAC address is 01:00:5e:00:00:fc */ +extern const MACAddress_t xLLMNR_MacAddress; /* The LLMNR IPv6 MAC address is 33:33:00:01:00:03 */ - extern const MACAddress_t xLLMNR_MacAddressIPv6; -#endif /* ipconfigUSE_LLMNR */ - -#if ( ipconfigUSE_MDNS == 1 ) - /* The MDNS MAC address is 01:00:5e:00:00:fc */ - extern const MACAddress_t xMDNS_MacAddress; -#endif /* ipconfigUSE_MDNS */ +extern const MACAddress_t xLLMNR_MacAddressIPv6; -#if ( ipconfigUSE_MDNS == 1 ) && ( ipconfigUSE_IPv6 != 0 ) +/* The LLMNR IPv6 address is ff02::1:3 */ +extern const IPv6_Address_t ipLLMNR_IP_ADDR_IPv6; -/* The MDNS IPv6 address is ff02::1:3 */ - extern const IPv6_Address_t ipMDNS_IP_ADDR_IPv6; +/* The MDNS MAC address is 01:00:5e:00:00:fc */ +extern const MACAddress_t xMDNS_MacAddress; /* The MDNS IPv6 MAC address is 33:33:00:01:00:03 */ /* This type-name was formally "misspelled" as * xMDNS_MACAddressIPv6 with "MAC": */ - extern const MACAddress_t xMDNS_MacAddressIPv6; - /* Guarantee backward compatibility. */ - #define xMDNS_MACAddressIPv6 xMDNS_MacAddressIPv6 -#endif /* ipconfigUSE_MDNS */ +extern const MACAddress_t xMDNS_MacAddressIPv6; +/* Guarantee backward compatibility. */ +#define xMDNS_MACAddressIPv6 xMDNS_MacAddressIPv6 + +/* The MDNS IPv6 address is ff02::1:3 */ +extern const IPv6_Address_t ipMDNS_IP_ADDR_IPv6; /** @brief While doing integration tests, it is necessary to influence the choice * between DNS/IPv4 and DNS/IPv4. Depending on this, a DNS server will be @@ -95,6 +80,11 @@ typedef enum xIPPreference /** @brief This variable determines he choice of DNS server, either IPv4 or IPv6. */ extern IPPreference_t xDNS_IP_Preference; +/* + * LLMNR is very similar to DNS, so is handled by the DNS routines. + */ +uint32_t ulDNSHandlePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ); + #if ( ipconfigUSE_NBNS != 0 ) /* diff --git a/source/include/FreeRTOS_IPv4.h b/source/include/FreeRTOS_IPv4.h index c0f9aa05b..8a9d59320 100644 --- a/source/include/FreeRTOS_IPv4.h +++ b/source/include/FreeRTOS_IPv4.h @@ -58,6 +58,11 @@ struct xIP_PACKET; #define ipIPV4_VERSION_HEADER_LENGTH_MIN 0x45U /**< Minimum IPv4 header length. */ #define ipIPV4_VERSION_HEADER_LENGTH_MAX 0x4FU /**< Maximum IPv4 header length. */ +/* IPv4 multicast MAC address starts with 01-00-5E. */ +#define ipMULTICAST_MAC_ADDRESS_IPv4_0 0x01U +#define ipMULTICAST_MAC_ADDRESS_IPv4_1 0x00U +#define ipMULTICAST_MAC_ADDRESS_IPv4_2 0x5EU + /* * These functions come from the IPv4-only library. * void FreeRTOS_SetIPAddress( uint32_t ulIPAddress ); diff --git a/test/unit-test/ConfigFiles/FreeRTOSIPConfig.h b/test/unit-test/ConfigFiles/FreeRTOSIPConfig.h index 09ddb181c..2dc487b48 100644 --- a/test/unit-test/ConfigFiles/FreeRTOSIPConfig.h +++ b/test/unit-test/ConfigFiles/FreeRTOSIPConfig.h @@ -306,6 +306,7 @@ #define ipconfigUSE_NBNS ( 1 ) #define ipconfigUSE_LLMNR ( 1 ) +#define ipconfigUSE_MDNS ( 1 ) #define ipconfigDNS_USE_CALLBACKS 1 #define ipconfigUSE_ARP_REMOVE_ENTRY 1 diff --git a/test/unit-test/FreeRTOS_DNS_Callback/FreeRTOS_DNS_Callback_utest.c b/test/unit-test/FreeRTOS_DNS_Callback/FreeRTOS_DNS_Callback_utest.c index a23ee1ba6..d35100387 100644 --- a/test/unit-test/FreeRTOS_DNS_Callback/FreeRTOS_DNS_Callback_utest.c +++ b/test/unit-test/FreeRTOS_DNS_Callback/FreeRTOS_DNS_Callback_utest.c @@ -202,6 +202,82 @@ void test_xDNSDoCallback_success_equal_identifier_set_timer( void ) TEST_ASSERT_EQUAL( 1, callback_called ); } +/** + * @brief Happy Path! + */ +void test_xDNSDoCallback_success_equal_port_number_equal_name( void ) +{ + BaseType_t ret; + ParseSet_t pxSet; + struct freertos_addrinfo pxAddress; + DNSMessage_t xDNSMessageHeader; + char pc_name[] = "test"; + uint8_t dnsCallbackMemory[ sizeof( DNSCallback_t ) + ipconfigDNS_CACHE_NAME_LENGTH ]; + DNSCallback_t * pxDnsCallback = ( DNSCallback_t * ) &dnsCallbackMemory; + + pxSet.pxDNSMessageHeader = &xDNSMessageHeader; + pxSet.usPortNumber = FreeRTOS_htons( ipMDNS_PORT ); + strcpy( pxSet.pcName, pc_name ); + pxDnsCallback->pCallbackFunction = dns_callback; + strcpy( pxDnsCallback->pcName, pc_name ); + + /* Expectations */ + listGET_END_MARKER_ExpectAnyArgsAndReturn( ( ListItem_t * ) 4 ); + vTaskSuspendAll_Expect(); + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) 8 ); + + listGET_LIST_ITEM_OWNER_ExpectAnyArgsAndReturn( pxDnsCallback ); + uxListRemove_ExpectAnyArgsAndReturn( pdTRUE ); + vPortFree_ExpectAnyArgs(); + listLIST_IS_EMPTY_ExpectAnyArgsAndReturn( pdTRUE ); + + vIPSetDNSTimerEnableState_ExpectAnyArgs(); + + xTaskResumeAll_ExpectAndReturn( pdFALSE ); + /* API Call */ + ret = xDNSDoCallback( &pxSet, &pxAddress ); + + /* Validations */ + TEST_ASSERT_EQUAL( pdTRUE, ret ); + TEST_ASSERT_EQUAL( 1, callback_called ); +} + +/** + * @brief A failure path occurs when the port number is for MDNS but + * the name does not match. + */ +void test_xDNSDoCallback_fail_equal_port_number_not_equal_name( void ) +{ + BaseType_t ret; + ParseSet_t pxSet; + struct freertos_addrinfo pxAddress; + DNSMessage_t xDNSMessageHeader; + + pxSet.pxDNSMessageHeader = &xDNSMessageHeader; + pxSet.pxDNSMessageHeader->usIdentifier = 123; + pxSet.usPortNumber = FreeRTOS_htons( ipMDNS_PORT ); + char pc_name[] = "test"; + strcpy( pxSet.pcName, pc_name ); + dnsCallback->pCallbackFunction = dns_callback; + dnsCallback->pcName[ 0 ] = '\0'; + + /* Expectations */ + listGET_END_MARKER_ExpectAnyArgsAndReturn( ( ListItem_t * ) 4 ); + vTaskSuspendAll_Expect(); + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) 8 ); + + listGET_LIST_ITEM_OWNER_ExpectAnyArgsAndReturn( dnsCallback ); + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) 4 ); + + xTaskResumeAll_ExpectAndReturn( pdFALSE ); + /* API Call */ + ret = xDNSDoCallback( &pxSet, &pxAddress ); + + /* Validations */ + TEST_ASSERT_EQUAL( pdFALSE, ret ); + TEST_ASSERT_EQUAL( 0, callback_called ); +} + /** * @brief Happy Path! */ diff --git a/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_stubs.c b/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_stubs.c index f25be869e..117d487d1 100644 --- a/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_stubs.c +++ b/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_stubs.c @@ -53,6 +53,12 @@ struct xNetworkEndPoint * pxNetworkEndPoints = NULL; const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; + void vPortEnterCritical( void ) { } diff --git a/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_utest.c b/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_utest.c index 2bc281d81..1e4469d6a 100644 --- a/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_utest.c +++ b/test/unit-test/FreeRTOS_IP/FreeRTOS_IP_utest.c @@ -1560,7 +1560,7 @@ void test_eConsiderFrameForProcessing_LocalMACMatch( void ) /* Align endpoint's & packet's MAC address. */ memset( pxEndPoint->xMACAddress.ucBytes, 0xAA, sizeof( MACAddress_t ) ); memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, pxEndPoint->xMACAddress.ucBytes, sizeof( MACAddress_t ) ); - pxEthernetHeader->usFrameType = FreeRTOS_htons( 0x0800 ); + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1579,9 +1579,6 @@ void test_eConsiderFrameForProcessing_LocalMACMatchInvalidFrameType( void ) uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; EthernetHeader_t * pxEthernetHeader; - /* eConsiderFrameForProcessing */ - FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( pxEndPoint ); - /* Map the buffer onto Ethernet Header struct for easy access to fields. */ pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; @@ -1590,7 +1587,7 @@ void test_eConsiderFrameForProcessing_LocalMACMatchInvalidFrameType( void ) /* Align endpoint's & packet's MAC address. */ memset( pxEndPoint->xMACAddress.ucBytes, 0xAA, sizeof( MACAddress_t ) ); memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, pxEndPoint->xMACAddress.ucBytes, sizeof( MACAddress_t ) ); - pxEthernetHeader->usFrameType = FreeRTOS_htons( 0 ); + pxEthernetHeader->usFrameType = 0; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1609,9 +1606,6 @@ void test_eConsiderFrameForProcessing_LocalMACMatchInvalidFrameType1( void ) uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; EthernetHeader_t * pxEthernetHeader; - /* eConsiderFrameForProcessing */ - FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( pxEndPoint ); - /* Map the buffer onto Ethernet Header struct for easy access to fields. */ pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; @@ -1647,7 +1641,7 @@ void test_eConsiderFrameForProcessing_BroadCastMACMatch( void ) memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xBroadcastMACAddress.ucBytes, sizeof( MACAddress_t ) ); - pxEthernetHeader->usFrameType = 0xFFFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1674,7 +1668,88 @@ void test_eConsiderFrameForProcessing_LLMNR_MACMatch( void ) memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xLLMNR_MacAddress.ucBytes, sizeof( MACAddress_t ) ); - pxEthernetHeader->usFrameType = 0xFFFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eProcessBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_LLMNR_IPv6_MACMatch + * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet + * matches LLMNR MAC address and the frame type is valid. + */ +void test_eConsiderFrameForProcessing_LLMNR_IPv6_MACMatch( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xLLMNR_MacAddressIPv6.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eProcessBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_MDNS_MACMatch + * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet + * matches MDNS MAC address and the frame type is valid. + */ +void test_eConsiderFrameForProcessing_MDNS_MACMatch( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xMDNS_MacAddress.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eProcessBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_MDNS_IPv6_MACMatch + * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet + * matches LLMNR MAC address and the frame type is valid. + */ +void test_eConsiderFrameForProcessing_MDNS_IPv6_MACMatch( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xMDNS_MacAddressIPv6.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1702,7 +1777,7 @@ void test_eConsiderFrameForProcessing_NotMatch( void ) memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, &xMACAddress, sizeof( MACAddress_t ) ); - pxEthernetHeader->usFrameType = 0xFFFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1710,11 +1785,127 @@ void test_eConsiderFrameForProcessing_NotMatch( void ) } /** - * @brief test_eConsiderFrameForProcessing_IPv6BroadCastMACMatch + * @brief test_eConsiderFrameForProcessing_Multicast_MACMatch * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet - * matches IPv6 broadcast MAC address and the frame type is valid. + * matches IPv6 Multicast MAC address and the frame type is valid. */ -void test_eConsiderFrameForProcessing_IPv6BroadCastMACMatch( void ) +void test_eConsiderFrameForProcessing_Multicast_MACMatch( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv4_0; + pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = ipMULTICAST_MAC_ADDRESS_IPv4_1; + pxEthernetHeader->xDestinationAddress.ucBytes[ 2 ] = ipMULTICAST_MAC_ADDRESS_IPv4_2; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eProcessBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_Multicast_MACNotMatch1 + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * does not match IPv4 Multicast MAC address. + */ +void test_eConsiderFrameForProcessing_Multicast_MACNotMatch1( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv4_0; + pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = 0xFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_Multicast_MACNotMatch2 + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * does not match IPv4 Multicast MAC address. + */ +void test_eConsiderFrameForProcessing_Multicast_MACNotMatch2( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv4_0; + pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = ipMULTICAST_MAC_ADDRESS_IPv4_1; + pxEthernetHeader->xDestinationAddress.ucBytes[ 2 ] = 0xFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_Multicast_MACNotMatch3 + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * does not match IPv4 Multicast MAC address. + */ +void test_eConsiderFrameForProcessing_Multicast_MACNotMatch3( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv4_0; + pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = ipMULTICAST_MAC_ADDRESS_IPv4_1; + pxEthernetHeader->xDestinationAddress.ucBytes[ 2 ] = ipMULTICAST_MAC_ADDRESS_IPv4_2; + pxEthernetHeader->xDestinationAddress.ucBytes[ 3 ] = 0xFF; + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_IPv6_Multicast_MACMatch + * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet + * matches IPv6 Multicast MAC address and the frame type is valid. + */ +void test_eConsiderFrameForProcessing_IPv6_Multicast_MACMatch( void ) { eFrameProcessingResult_t eResult; uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; @@ -1730,7 +1921,7 @@ void test_eConsiderFrameForProcessing_IPv6BroadCastMACMatch( void ) pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv6_0; pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = ipMULTICAST_MAC_ADDRESS_IPv6_1; - pxEthernetHeader->usFrameType = 0xFFFF; + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); @@ -1758,6 +1949,56 @@ void test_eConsiderFrameForProcessing_IPv6BroadCastMACPartialMatch( void ) pxEthernetHeader->xDestinationAddress.ucBytes[ 0 ] = ipMULTICAST_MAC_ADDRESS_IPv6_0; pxEthernetHeader->xDestinationAddress.ucBytes[ 1 ] = 0x00; + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_ArpBoardcastMacMatch + * eConsiderFrameForProcessing must return eProcessBuffer when the MAC address in packet + * matches broadcast MAC address and the frame type is ARP. + */ +void test_eConsiderFrameForProcessing_ArpBoardcastMacMatch( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xBroadcastMACAddress.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipARP_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eProcessBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_UnknownFrameType + * eConsiderFrameForProcessing must return eReleaseBuffer when the frame type + * is unknown. + */ +void test_eConsiderFrameForProcessing_UnknownFrameType( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigTCP_MSS ]; + EthernetHeader_t * pxEthernetHeader; + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigTCP_MSS ); + pxEthernetHeader->usFrameType = 0xFFFF; eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig/FreeRTOS_IP_DiffConfig_stubs.c b/test/unit-test/FreeRTOS_IP_DiffConfig/FreeRTOS_IP_DiffConfig_stubs.c index 3b13966be..9a9ea5162 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig/FreeRTOS_IP_DiffConfig_stubs.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig/FreeRTOS_IP_DiffConfig_stubs.c @@ -50,9 +50,15 @@ struct xNetworkInterface * pxNetworkInterfaces = NULL; /** @brief A list of all network end-points. Each element has a next pointer. */ struct xNetworkEndPoint * pxNetworkEndPoints = NULL; +const MACAddress_t xDefault_MacAddress = { { 0x11, 0x22, 0x33, 0x44, 0x55, 0x66 } }; + const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; -const MACAddress_t xDefault_MacAddress = { { 0x11, 0x22, 0x33, 0x44, 0x55, 0x66 } }; +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; void vPortEnterCritical( void ) { diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_stubs.c b/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_stubs.c index 5968e321c..2d454be48 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_stubs.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_stubs.c @@ -51,9 +51,15 @@ struct xNetworkInterface * pxNetworkInterfaces = NULL; /** @brief A list of all network end-points. Each element has a next pointer. */ struct xNetworkEndPoint * pxNetworkEndPoints = NULL; +const MACAddress_t xDefault_MacAddress = { { 0x11, 0x22, 0x33, 0x44, 0x55, 0x66 } }; + const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; -const MACAddress_t xDefault_MacAddress = { { 0x11, 0x22, 0x33, 0x44, 0x55, 0x66 } }; +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; void vPortEnterCritical( void ) { diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_utest.c b/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_utest.c index c103cd264..3a1652158 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_utest.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig1/FreeRTOS_IP_DiffConfig1_utest.c @@ -786,3 +786,26 @@ void test_FreeRTOS_GetUDPPayloadBuffer_BlockTimeEqualToConfig_IPv6NotSupported( TEST_ASSERT_EQUAL_PTR( NULL, pvReturn ); } + +/** + * @brief test_eConsiderFrameForProcessing_IPv6_FrameType_But_Disabled + * eConsiderFrameForProcessing must return eReleaseBuffer when the frame type is IPv6 but + * ipconfigUSE_IPv6 is disabled. + */ +void test_eConsiderFrameForProcessing_IPv6_FrameType_But_Disabled( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigNETWORK_MTU ]; + EthernetHeader_t * pxEthernetHeader; + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigNETWORK_MTU ); + + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOSIPConfig.h b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOSIPConfig.h index cbcbc9385..73c8ac747 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOSIPConfig.h +++ b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOSIPConfig.h @@ -302,7 +302,8 @@ #define ipconfigUSE_NBNS ( 1 ) -#define ipconfigUSE_LLMNR ( 1 ) +#define ipconfigUSE_LLMNR ( 0 ) +#define ipconfigUSE_MDNS ( 0 ) #define ipconfigDNS_USE_CALLBACKS 1 #define ipconfigUSE_ARP_REMOVE_ENTRY 1 diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_stubs.c b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_stubs.c index f35bef306..641b42e4b 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_stubs.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_stubs.c @@ -51,6 +51,12 @@ struct xNetworkEndPoint * pxNetworkEndPoints = NULL; const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; + void vPortEnterCritical( void ) { } diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_utest.c b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_utest.c index 15bfe29cc..25cf53b60 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_utest.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig2/FreeRTOS_IP_DiffConfig2_utest.c @@ -143,3 +143,115 @@ void test_FreeRTOS_IPInit_HappyPathDHCP( void ) TEST_ASSERT_EQUAL( pdPASS, xReturn ); TEST_ASSERT_EQUAL( IPInItHappyPath_xTaskHandleToSet, FreeRTOS_GetIPTaskHandle() ); } + +/** + * @brief test_eConsiderFrameForProcessing_LLMNR_IPv4_MACMatch_But_Disabled + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * matches LLMNR MAC address and the frame type is valid but any of ipconfigUSE_DNS, ipconfigUSE_LLMNR + * or ipconfigUSE_IPv4 is disabled. + */ +void test_eConsiderFrameForProcessing_LLMNR_IPv4_MACMatch_But_Disabled( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigNETWORK_MTU ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigNETWORK_MTU ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xLLMNR_MacAddress.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_LLMNR_IPv6_MACMatch_But_Disabled + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * matches LLMNR MAC address and the frame type is valid but any of ipconfigUSE_DNS, ipconfigUSE_LLMNR + * or ipconfigUSE_IPv6 is disabled. + */ +void test_eConsiderFrameForProcessing_LLMNR_IPv6_MACMatch_But_Disabled( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigNETWORK_MTU ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigNETWORK_MTU ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xLLMNR_MacAddressIPv6.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_MDNS_IPv6_MACMatch_But_Disabled + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * matches MDNS MAC address and the frame type is valid but any of ipconfigUSE_DNS, ipconfigUSE_MDNS + * or ipconfigUSE_IPv6 is disabled. + */ +void test_eConsiderFrameForProcessing_MDNS_IPv6_MACMatch_But_Disabled( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigNETWORK_MTU ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigNETWORK_MTU ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xMDNS_MacAddressIPv6.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv6_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} + +/** + * @brief test_eConsiderFrameForProcessing_MDNS_IPv4_MACMatch_But_Disabled + * eConsiderFrameForProcessing must return eReleaseBuffer when the MAC address in packet + * matches MDNS MAC address and the frame type is valid but any of ipconfigUSE_DNS, ipconfigUSE_MDNS + * or ipconfigUSE_IPv4 is disabled. + */ +void test_eConsiderFrameForProcessing_MDNS_IPv4_MACMatch_But_Disabled( void ) +{ + eFrameProcessingResult_t eResult; + uint8_t ucEthernetBuffer[ ipconfigNETWORK_MTU ]; + EthernetHeader_t * pxEthernetHeader; + + /* eConsiderFrameForProcessing */ + FreeRTOS_FindEndPointOnMAC_ExpectAnyArgsAndReturn( NULL ); + + /* Map the buffer onto Ethernet Header struct for easy access to fields. */ + pxEthernetHeader = ( EthernetHeader_t * ) ucEthernetBuffer; + + memset( ucEthernetBuffer, 0x00, ipconfigNETWORK_MTU ); + + memcpy( pxEthernetHeader->xDestinationAddress.ucBytes, xMDNS_MacAddress.ucBytes, sizeof( MACAddress_t ) ); + pxEthernetHeader->usFrameType = ipIPv4_FRAME_TYPE; + + eResult = eConsiderFrameForProcessing( ucEthernetBuffer ); + + TEST_ASSERT_EQUAL( eReleaseBuffer, eResult ); +} diff --git a/test/unit-test/FreeRTOS_IP_DiffConfig3/FreeRTOS_IP_DiffConfig3_stubs.c b/test/unit-test/FreeRTOS_IP_DiffConfig3/FreeRTOS_IP_DiffConfig3_stubs.c index ddaffbd0a..938937b61 100644 --- a/test/unit-test/FreeRTOS_IP_DiffConfig3/FreeRTOS_IP_DiffConfig3_stubs.c +++ b/test/unit-test/FreeRTOS_IP_DiffConfig3/FreeRTOS_IP_DiffConfig3_stubs.c @@ -52,6 +52,12 @@ struct xNetworkEndPoint * pxNetworkEndPoints = NULL; const MACAddress_t xLLMNR_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfc } }; +const MACAddress_t xLLMNR_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x01, 0x00, 0x03 } }; + +const MACAddress_t xMDNS_MacAddress = { { 0x01, 0x00, 0x5e, 0x00, 0x00, 0xfb } }; + +const MACAddress_t xMDNS_MacAddressIPv6 = { { 0x33, 0x33, 0x00, 0x00, 0x00, 0xFB } }; + void vPortEnterCritical( void ) { } From c1fc5fe3bedb8fe9e90d55405bce27cbd0960726 Mon Sep 17 00:00:00 2001 From: Rahul Kar <118818625+kar-rahul-aws@users.noreply.github.com> Date: Mon, 5 Aug 2024 11:25:48 +0530 Subject: [PATCH 5/5] Update links in ReadMe (#1174) --- README.md | 2 +- .../portable/NetworkInterface/board_family/NetworkInterface.c | 2 +- source/portable/NetworkInterface/board_family/ReadMe.txt | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 08ed92b14..b422dd034 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ release.** The easiest way to use version 4.0.0 and later of FreeRTOS-Plus-TCP is to refer the Getting started Guide (found [here](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/GettingStarted.md)) Another way is to start with the pre-configured IPv4 Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator)) or IPv6 Multi-endpoint Windows Simulator demo (found in [this directory](https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_IPv6_Demo/IPv6_Multi_WinSim_demo)). That way you will have the correct FreeRTOS source files included, and the correct include paths configured. Once a demo application is building and executing you can remove the demo application files, and start to add in your own application source files. See the [FreeRTOS Kernel Quick Start Guide](https://www.freertos.org/FreeRTOS-quick-start-guide.html) for detailed instructions and other useful links. -Additionally, for FreeRTOS-Plus-TCP source code organization refer to the [Documentation](http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Networking_Tutorial.html), and [API Reference](https://freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/FreeRTOS_TCP_API_Functions.html). +Additionally, for FreeRTOS-Plus-TCP source code organization refer to the [Documentation](http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Networking_Tutorial.html), and [API Reference](https://freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/09-API-reference/01-FreeRTOS-plus-TCP-APIs). ### Getting help If you have any questions or need assistance troubleshooting your FreeRTOS project, we have an active community that can help on the [FreeRTOS Community Support Forum](https://forums.freertos.org). Please also refer to [FAQ](http://www.freertos.org/FAQHelp.html) for frequently asked questions. diff --git a/source/portable/NetworkInterface/board_family/NetworkInterface.c b/source/portable/NetworkInterface/board_family/NetworkInterface.c index 0a6fa0505..dfb1979c6 100644 --- a/source/portable/NetworkInterface/board_family/NetworkInterface.c +++ b/source/portable/NetworkInterface/board_family/NetworkInterface.c @@ -31,7 +31,7 @@ * concrete implementations of the functions in this file. * * See the following URL for an explanation of this file and its functions: -* https://freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html +* https://freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/10-Porting/03-Embedded_Ethernet_Porting * *****************************************************************************/ diff --git a/source/portable/NetworkInterface/board_family/ReadMe.txt b/source/portable/NetworkInterface/board_family/ReadMe.txt index 782e42935..352670ab5 100644 --- a/source/portable/NetworkInterface/board_family/ReadMe.txt +++ b/source/portable/NetworkInterface/board_family/ReadMe.txt @@ -2,4 +2,4 @@ Update NetworkInterface.c and include other files needed by FreeRTOS+TCP here. Note: The NetworkInterface.c file in this directory is Not! to be used as is. The purpose of the file is to provide a template for writing a network interface. Each network interface will have to provide concrete implementations of the functions in NetworkInterface.c. -See the following URL for an explanation of the file and its functions: https://freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html \ No newline at end of file +See the following URL for an explanation of the file and its functions: https://freertos.org/Documentation/03-Libraries/02-FreeRTOS-plus/02-FreeRTOS-plus-TCP/10-Porting/03-Embedded_Ethernet_Porting \ No newline at end of file