Merge branch 'main' into fix_dns_ip_preference

source/FreeRTOS_ARP.c

@@ -228,7 +228,7 @@ _static ARPCacheRow_t xARPCache[ ipconfigARP_CACHE_ENTRIES ];
                     uxARPClashCounter++;
 
                     /* Send out a defensive ARP request. */
-                    FreeRTOS_OutputARPRequest( pxTargetEndPoint->ipv4_settings.ulIPAddress );
+                    FreeRTOS_OutputARPRequest_Multi( pxTargetEndPoint, pxTargetEndPoint->ipv4_settings.ulIPAddress );
 
                     /* Since an ARP Request for this IP was just sent, do not send a gratuitous
                      * ARP for arpGRATUITOUS_ARP_PERIOD. */
@@ -539,7 +539,7 @@ BaseType_t xCheckRequiresARPResolution( const NetworkBufferDescriptor_t * pxNetw
                         * then we should send out ARP for finding the MAC address. */
                        if( xIsIPInARPCache( pxIPHeader->ulSourceIPAddress ) == pdFALSE )
                        {
-                           FreeRTOS_OutputARPRequest( pxIPHeader->ulSourceIPAddress );
+                           FreeRTOS_OutputARPRequest_Multi( pxNetworkBuffer->pxEndPoint, pxIPHeader->ulSourceIPAddress );
 
                            /* This packet needs resolution since this is on the same subnet
                             * but not in the ARP cache. */
@@ -1222,7 +1222,7 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress,
                     {
                         #if ( ipconfigUSE_IPv4 != 0 )
                             case pdFALSE_UNSIGNED:
-                                FreeRTOS_OutputARPRequest( pxEndPoint->ipv4_settings.ulIPAddress );
+                                FreeRTOS_OutputARPRequest_Multi( pxEndPoint, pxEndPoint->ipv4_settings.ulIPAddress );
                                 break;
                         #endif /* ( ipconfigUSE_IPv4 != 0 ) */
 
@@ -1264,80 +1264,95 @@ static BaseType_t prvFindCacheEntry( const MACAddress_t * pxMACAddress,
 /*-----------------------------------------------------------*/
 
 /**
- * @brief Create and send an ARP request packet.
+ * @brief Create and send an ARP request packet to given IPv4 endpoint.
  *
+ * @param[in] pxEndPoint Endpoint through which the requests should be sent.
  * @param[in] ulIPAddress A 32-bit representation of the IP-address whose
  *                         physical (MAC) address is required.
  */
-    void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
+    void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
+                                          uint32_t ulIPAddress )
     {
         NetworkBufferDescriptor_t * pxNetworkBuffer;
-        NetworkEndPoint_t * pxEndPoint;
 
-        /* Send an ARP request to every end-point which has the type IPv4,
-         * and which already has an IP-address assigned. */
-        for( pxEndPoint = FreeRTOS_FirstEndPoint( NULL );
-             pxEndPoint != NULL;
-             pxEndPoint = FreeRTOS_NextEndPoint( NULL, pxEndPoint ) )
+        if( ( pxEndPoint->bits.bIPv6 == pdFALSE_UNSIGNED ) &&
+            ( pxEndPoint->ipv4_settings.ulIPAddress != 0U ) )
         {
-            if( ( pxEndPoint->bits.bIPv6 == pdFALSE_UNSIGNED ) &&
-                ( pxEndPoint->ipv4_settings.ulIPAddress != 0U ) )
+            /* This is called from the context of the IP event task, so a block time
+             * must not be used. */
+            pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( ARPPacket_t ), ( TickType_t ) 0U );
+
+            if( pxNetworkBuffer != NULL )
             {
-                /* This is called from the context of the IP event task, so a block time
-                 * must not be used. */
-                pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( ARPPacket_t ), ( TickType_t ) 0U );
+                pxNetworkBuffer->xIPAddress.ulIP_IPv4 = ulIPAddress;
+                pxNetworkBuffer->pxEndPoint = pxEndPoint;
+                pxNetworkBuffer->pxInterface = pxEndPoint->pxNetworkInterface;
+                vARPGenerateRequestPacket( pxNetworkBuffer );
 
-                if( pxNetworkBuffer != NULL )
+                #if ( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 )
                 {
-                    pxNetworkBuffer->xIPAddress.ulIP_IPv4 = ulIPAddress;
-                    pxNetworkBuffer->pxEndPoint = pxEndPoint;
-                    pxNetworkBuffer->pxInterface = pxEndPoint->pxNetworkInterface;
-                    vARPGenerateRequestPacket( pxNetworkBuffer );
-
-                    #if ( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 )
+                    if( pxNetworkBuffer->xDataLength < ( size_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES )
                     {
-                        if( pxNetworkBuffer->xDataLength < ( size_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES )
-                        {
-                            BaseType_t xIndex;
+                        BaseType_t xIndex;
 
-                            for( xIndex = ( BaseType_t ) pxNetworkBuffer->xDataLength; xIndex < ( BaseType_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES; xIndex++ )
-                            {
-                                pxNetworkBuffer->pucEthernetBuffer[ xIndex ] = 0U;
-                            }
-
-                            pxNetworkBuffer->xDataLength = ( size_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES;
+                        for( xIndex = ( BaseType_t ) pxNetworkBuffer->xDataLength; xIndex < ( BaseType_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES; xIndex++ )
+                        {
+                            pxNetworkBuffer->pucEthernetBuffer[ xIndex ] = 0U;
                         }
+
+                        pxNetworkBuffer->xDataLength = ( size_t ) ipconfigETHERNET_MINIMUM_PACKET_BYTES;
                     }
-                    #endif /* if( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) */
+                }
+                #endif /* if( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) */
 
-                    if( xIsCallingFromIPTask() != pdFALSE )
-                    {
-                        iptraceNETWORK_INTERFACE_OUTPUT( pxNetworkBuffer->xDataLength, pxNetworkBuffer->pucEthernetBuffer );
+                if( xIsCallingFromIPTask() != pdFALSE )
+                {
+                    iptraceNETWORK_INTERFACE_OUTPUT( pxNetworkBuffer->xDataLength, pxNetworkBuffer->pucEthernetBuffer );
 
-                        /* Only the IP-task is allowed to call this function directly. */
-                        if( pxEndPoint->pxNetworkInterface != NULL )
-                        {
-                            ( void ) pxEndPoint->pxNetworkInterface->pfOutput( pxEndPoint->pxNetworkInterface, pxNetworkBuffer, pdTRUE );
-                        }
-                    }
-                    else
+                    /* Only the IP-task is allowed to call this function directly. */
+                    if( pxEndPoint->pxNetworkInterface != NULL )
                     {
-                        IPStackEvent_t xSendEvent;
+                        ( void ) pxEndPoint->pxNetworkInterface->pfOutput( pxEndPoint->pxNetworkInterface, pxNetworkBuffer, pdTRUE );
+                    }
+                }
+                else
+                {
+                    IPStackEvent_t xSendEvent;
 
-                        /* Send a message to the IP-task to send this ARP packet. */
-                        xSendEvent.eEventType = eNetworkTxEvent;
-                        xSendEvent.pvData = pxNetworkBuffer;
+                    /* Send a message to the IP-task to send this ARP packet. */
+                    xSendEvent.eEventType = eNetworkTxEvent;
+                    xSendEvent.pvData = pxNetworkBuffer;
 
-                        if( xSendEventStructToIPTask( &xSendEvent, ( TickType_t ) portMAX_DELAY ) == pdFAIL )
-                        {
-                            /* Failed to send the message, so release the network buffer. */
-                            vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
-                        }
+                    if( xSendEventStructToIPTask( &xSendEvent, ( TickType_t ) portMAX_DELAY ) == pdFAIL )
+                    {
+                        /* Failed to send the message, so release the network buffer. */
+                        vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
                     }
                 }
             }
         }
     }
+
+/*-----------------------------------------------------------*/
+
+/**
+ * @brief Create and send an ARP request packet.
+ *
+ * @param[in] ulIPAddress A 32-bit representation of the IP-address whose
+ *                         physical (MAC) address is required.
+ */
+    void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
+    {
+        /* 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 );
+
+        if( pxEndPoint != NULL )
+        {
+            FreeRTOS_OutputARPRequest_Multi( pxEndPoint, ulIPAddress );
+        }
+    }
 /*-----------------------------------------------------------*/
 
 /**

source/FreeRTOS_ND.c

@@ -964,6 +964,7 @@
         ICMPPacket_IPv6_t * pxICMPPacket = ( ( ICMPPacket_IPv6_t * ) pxNetworkBuffer->pucEthernetBuffer );
         /* coverity[misra_c_2012_rule_11_3_violation] */
         ICMPHeader_IPv6_t * pxICMPHeader_IPv6 = ( ( ICMPHeader_IPv6_t * ) &( pxICMPPacket->xICMPHeaderIPv6 ) );
+        /* Note: pxNetworkBuffer->pxEndPoint is already verified to be non-NULL in prvProcessEthernetPacket() */
         NetworkEndPoint_t * pxEndPoint = pxNetworkBuffer->pxEndPoint;
         size_t uxNeededSize;
 

source/include/FreeRTOS_ARP.h

@@ -165,6 +165,12 @@ void vARPGenerateRequestPacket( NetworkBufferDescriptor_t * const pxNetworkBuffe
 
 void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress );
 
+/*
+ * Create and send an ARP request packet to IPv4 endpoints of an interface.
+ */
+void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
+                                      uint32_t ulIPAddress );
+
 /* Clear all entries in the ARp cache. */
 void FreeRTOS_ClearARP( const struct xNetworkEndPoint * pxEndPoint );
 

source/include/FreeRTOS_IP_Utils.h

@@ -49,7 +49,6 @@
 #include "FreeRTOS_Sockets.h"
 #include "FreeRTOS_Routing.h"
 #include "FreeRTOS_IP_Private.h"
-#include "FreeRTOS_ARP.h"
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_DHCP.h"
 #include "NetworkInterface.h"

test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json

@@ -5,6 +5,7 @@
       "--unwind 1",
       "--unwindset vARPAgeCache.0:7",
       "--unwindset FreeRTOS_OutputARPRequest.0:3",
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
       "--unwindset vARPAgeCache.1:3",
       "--nondet-static"
   ],

test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c

@@ -8,12 +8,14 @@
 #include "FreeRTOS_IP.h"
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
+#include "FreeRTOS_Routing.h"
 
 /* This pointer is maintained by the IP-task. Defined in FreeRTOS_IP.c */
 extern NetworkBufferDescriptor_t * pxARPWaitingNetworkBuffer;
 
 /* This is an output function and need not be tested with this proof. */
-void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
+void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
+                                      uint32_t ulIPAddress )
 {
 }
 

test/cbmc/proofs/ARP/xCheckRequiresARPResolution/xCheckRequiresARPResolution_harness.c

@@ -5,7 +5,7 @@
 /* FreeRTOS+TCP includes. */
 #include "FreeRTOS_IP.h"
 #include "FreeRTOS_ARP.h"
-
+#include "FreeRTOS_Routing.h"
 /* CBMC includes. */
 #include "cbmc.h"
 
@@ -38,8 +38,9 @@ size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
     return xReturn;
 }
 
-/* Abstraction of FreeRTOS_OutputARPRequest. */
-void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
+/* Abstraction of FreeRTOS_OutputARPRequest_Multi. */
+void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
+                                      uint32_t ulIPAddress )
 {
 }
 

test/cbmc/proofs/IP/ProcessEthernetPacket/ProcessEthernetPacket_harness.c

@@ -75,6 +75,8 @@ void __CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( NetworkBufferD
 /* The harness test proceeds to call prvProcessEthernetPacket with an unconstrained value */
 void harness()
 {
+    struct xNetworkInterface xInterface;
+
     /* Needs a valid network buffer to be passed */
     NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
 
@@ -87,5 +89,8 @@ void harness()
     pxNetworkBuffer->pucEthernetBuffer = ( ( ( uint8_t * ) safeMalloc( pxNetworkBuffer->xDataLength ) ) );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
+    /* Its assumed that every RX packet will have a valid network interface assigned. (Asserted in code) */
+    pxNetworkBuffer->pxInterface = &xInterface;
+
     __CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( pxNetworkBuffer );
 }

test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c

@@ -32,6 +32,7 @@
 
 /* FreeRTOS+TCP includes. */
 #include "FreeRTOS_IP.h"
+#include "FreeRTOS_ARP.h"
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_TCP_IP.h"
 #include "FreeRTOS_TCP_Transmission.h"