Merge pull request FreeRTOS#3 from FreeRTOS/labs/ipv6_multi

Labs/ipv6 multi merge to fork

Author: AniruddhaKanhere

FreeRTOS_DNS.c

@@ -130,10 +130,10 @@
  * uxIdentifier is a random identifier for this look-up, uxHostType is the type
  * of host wanted, dnsTYPE_A_HOST or dnsTYPE_AAA_HOST, i.e. IPv4 or IPv6 resp.
  */
-    _static size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
-                                        const char * pcHostName,
-                                        TickType_t uxIdentifier,
-                                        UBaseType_t uxHostType );
+    static size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
+                                       const char * pcHostName,
+                                       TickType_t uxIdentifier,
+                                       UBaseType_t uxHostType );
 
 /*
  * Simple routine that jumps over the NAME field of a resource record.
@@ -149,10 +149,10 @@
  * The IP address found will be stored in 'ppxAddressInfo' ( IPv4 or IPv6 ).
  * ppxAddressInfo may be NULL if the caller is not interested in the answers.
  */
-    _static uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                                       size_t uxBufferLength,
-                                       struct freertos_addrinfo ** ppxAddressInfo,
-                                       BaseType_t xExpected );
+    static uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                                      size_t uxBufferLength,
+                                      struct freertos_addrinfo ** ppxAddressInfo,
+                                      BaseType_t xExpected );
 
 /*
  * Check if hostname is a literal IP-address, check if the host is found in
@@ -1505,10 +1505,10 @@
  * @return Total size of the generated message, which is the space from the last written byte
  *         to the beginning of the buffer.
  */
-    _static size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
-                                        const char * pcHostName,
-                                        TickType_t uxIdentifier,
-                                        UBaseType_t uxHostType )
+    static size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
+                                       const char * pcHostName,
+                                       TickType_t uxIdentifier,
+                                       UBaseType_t uxHostType )
     {
         DNSMessage_t * pxDNSMessageHeader;
         size_t uxStart, uxIndex;
@@ -1958,10 +1958,10 @@
  *         An error code (dnsPARSE_ERROR) if there was an error in the DNS response.
  *         0 if xExpected set to pdFALSE.
  */
-    _static uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                                       size_t uxBufferLength,
-                                       struct freertos_addrinfo ** ppxAddressInfo,
-                                       BaseType_t xExpected )
+    static uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                                      size_t uxBufferLength,
+                                      struct freertos_addrinfo ** ppxAddressInfo,
+                                      BaseType_t xExpected )
     {
         DNSMessage_t * pxDNSMessageHeader;
 /* This pointer is not used to modify anything */

portable/NetworkInterface/STM32Hxx/NetworkInterface.c

@@ -41,6 +41,7 @@
 #include "FreeRTOS_Sockets.h"
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_DNS.h"
+#include "FreeRTOS_Routing.h"
 #include "NetworkBufferManagement.h"
 #include "NetworkInterface.h"
 
@@ -105,6 +106,8 @@ static SemaphoreHandle_t xTransmissionMutex;
 static ETH_HandleTypeDef xEthHandle;
 static ETH_TxPacketConfig xTxConfig;
 
+static NetworkInterface_t * pxMyInterface = NULL;
+
 /*
  * About the section ".ethernet_data" : the DMA wants the descriptors and buffers allocated in the
  * RAM3 memory, which can be added to the .LD file as follows::
@@ -170,6 +173,24 @@ static void vClearOptionBit( volatile uint32_t * pulValue,
 
 static size_t uxGetOwnCount( ETH_HandleTypeDef * heth );
 
+/* FreeRTOS+TCP/multi :
+ * Each network device has 3 access functions:
+ * - Initialise the device
+ * - Output a network packet
+ * - Return the PHY Link-Status (LS)
+ * They can be defined as static because the function addresses
+ * addresses will be stored in struct NetworkInterface_t. */
+
+static BaseType_t xSTM32H_NetworkInterfaceInitialise( NetworkInterface_t * pxInterface );
+
+static BaseType_t xSTM32H_NetworkInterfaceOutput( NetworkInterface_t * pxInterface,
+                                                  NetworkBufferDescriptor_t * const pxBuffer,
+                                                  BaseType_t xReleaseAfterSend );
+
+static BaseType_t xSTM32H_GetPhyLinkStatus( NetworkInterface_t * pxInterface );
+
+NetworkInterface_t * pxSTM32Hxx_FillInterfaceDescriptor( BaseType_t xEMACIndex,
+                                                         NetworkInterface_t * pxInterface );
 /*-----------------------------------------------------------*/
 
 static EthernetPhy_t xPhyObject;
@@ -205,21 +226,27 @@ static uint8_t * pucGetRXBuffer( size_t uxSize )
 }
 /*-----------------------------------------------------------*/
 
-BaseType_t xNetworkInterfaceInitialise( void )
+static BaseType_t xSTM32H_NetworkInterfaceInitialise( NetworkInterface_t * pxInterface )
 {
     BaseType_t xResult;
+    NetworkEndPoint_t * pxEndPoint;
     HAL_StatusTypeDef xHalEthInitStatus;
     size_t uxIndex = 0;
 
     if( xMacInitStatus == eMACInit )
     {
+        pxMyInterface = pxInterface;
+
+        pxEndPoint = FreeRTOS_FirstEndPoint( pxInterface );
+        configASSERT( pxEndPoint != NULL );
+
         /*
          * Initialize ETH Handler
          * It assumes that Ethernet GPIO and clock configuration
          * are already done in the ETH_MspInit()
          */
         xEthHandle.Instance = ETH;
-        xEthHandle.Init.MACAddr = ( uint8_t * ) FreeRTOS_GetMACAddress();
+        xEthHandle.Init.MACAddr = ( uint8_t * ) pxEndPoint->xMACAddress.ucBytes;
         xEthHandle.Init.MediaInterface = HAL_ETH_RMII_MODE;
         xEthHandle.Init.TxDesc = DMATxDscrTab;
         xEthHandle.Init.RxDesc = DMARxDscrTab;
@@ -325,7 +352,7 @@ BaseType_t xNetworkInterfaceInitialise( void )
 }
 /*-----------------------------------------------------------*/
 
-BaseType_t xGetPhyLinkStatus( void )
+static BaseType_t xSTM32H_GetPhyLinkStatus( NetworkInterface_t * pxInterface )
 {
     BaseType_t xReturn;
 
@@ -342,34 +369,73 @@ BaseType_t xGetPhyLinkStatus( void )
 }
 /*-----------------------------------------------------------*/
 
-BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor,
-                                    BaseType_t xReleaseAfterSend )
+#if ( ipconfigCOMPATIBLE_WITH_SINGLE != 0 )
+
+/* Do not call the following function directly. It is there for downward compatibility.
+ * The function FreeRTOS_IPInit() will call it to initialice the interface and end-point
+ * objects.  See the description in FreeRTOS_Routing.h. */
+    NetworkInterface_t * pxFillInterfaceDescriptor( BaseType_t xEMACIndex,
+                                                    NetworkInterface_t * pxInterface )
+    {
+        pxSTM32Hxx_FillInterfaceDescriptor( xEMACIndex, pxInterface );
+    }
+
+#endif /* ( ipconfigCOMPATIBLE_WITH_SINGLE != 0 ) */
+/*-----------------------------------------------------------*/
+
+NetworkInterface_t * pxSTM32Hxx_FillInterfaceDescriptor( BaseType_t xEMACIndex,
+                                                         NetworkInterface_t * pxInterface )
+{
+    static char pcName[ 17 ];
+
+/* This function pxSTM32Hxx_FillInterfaceDescriptor() adds a network-interface.
+ * Make sure that the object pointed to by 'pxInterface'
+ * is declared static or global, and that it will remain to exist. */
+
+    snprintf( pcName, sizeof( pcName ), "eth%u", ( unsigned ) xEMACIndex );
+
+    memset( pxInterface, '\0', sizeof( *pxInterface ) );
+    pxInterface->pcName = pcName;                    /* Just for logging, debugging. */
+    pxInterface->pvArgument = ( void * ) xEMACIndex; /* Has only meaning for the driver functions. */
+    pxInterface->pfInitialise = xSTM32H_NetworkInterfaceInitialise;
+    pxInterface->pfOutput = xSTM32H_NetworkInterfaceOutput;
+    pxInterface->pfGetPhyLinkStatus = xSTM32H_GetPhyLinkStatus;
+
+    FreeRTOS_AddNetworkInterface( pxInterface );
+
+    return pxInterface;
+}
+/*-----------------------------------------------------------*/
+
+static BaseType_t xSTM32H_NetworkInterfaceOutput( NetworkInterface_t * pxInterface,
+                                                  NetworkBufferDescriptor_t * const pxBuffer,
+                                                  BaseType_t xReleaseAfterSend )
 {
     BaseType_t xResult = pdFAIL;
     TickType_t xBlockTimeTicks = pdMS_TO_TICKS( 100U );
     uint8_t * pucTXBuffer;
 
     #if ( ipconfigZERO_COPY_TX_DRIVER != 0 )
         /* Zero-copy method, pass the buffer. */
-        pucTXBuffer = pxDescriptor->pucEthernetBuffer;
+        pucTXBuffer = pxBuffer->pucEthernetBuffer;
 
         /* As the buffer is passed to the driver, it must exist.
          * The library takes care of this. */
         configASSERT( xReleaseAfterSend != pdFALSE );
     #else
         pucTXBuffer = Tx_Buff[ xEthHandle.TxDescList.CurTxDesc ];
         /* The copy method, left here for educational purposes. */
-        configASSERT( pxDescriptor->xDataLength <= sizeof( Tx_Buff[ 0 ] ) );
+        configASSERT( pxBuffer->xDataLength <= sizeof( Tx_Buff[ 0 ] ) );
     #endif
 
     ETH_BufferTypeDef xTransmitBuffer =
     {
         .buffer = pucTXBuffer,
-        .len    = pxDescriptor->xDataLength,
+        .len    = pxBuffer->xDataLength,
         .next   = NULL  /* FreeRTOS+TCP does not use linked buffers. */
     };
     /* This is the total length, which is equal to the buffer. */
-    xTxConfig.Length = pxDescriptor->xDataLength;
+    xTxConfig.Length = pxBuffer->xDataLength;
     xTxConfig.TxBuffer = &( xTransmitBuffer );
 
     /* This counting semaphore counts the number of free TX DMA descriptors. */
@@ -395,7 +461,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescript
                 }
             #else
                 {
-                    memcpy( pucTXBuffer, pxDescriptor->pucEthernetBuffer, pxDescriptor->xDataLength );
+                    memcpy( pucTXBuffer, pxBuffer->pucEthernetBuffer, pxBuffer->xDataLength );
 
                     /* A memory barrier to make sure that the outgoing packets has been written
                      * to the physical memory. */
@@ -418,7 +484,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescript
 
     if( xReleaseAfterSend != pdFALSE )
     {
-        vReleaseNetworkBufferAndDescriptor( pxDescriptor );
+        vReleaseNetworkBufferAndDescriptor( pxBuffer );
     }
 
     return xResult;
@@ -638,6 +704,9 @@ static BaseType_t prvNetworkInterfaceInput( void )
                     .pvData     = ( void * ) pxReceivedBuffer
                 };
 
+                pxReceivedBuffer->pxInterface = pxMyInterface;
+                pxReceivedBuffer->pxEndPoint = FreeRTOS_MatchingEndpoint( pxMyInterface, pxReceivedBuffer->pucEthernetBuffer );
+
                 /* Send the data to the TCP/IP stack. */
                 if( xSendEventStructToIPTask( &( xRxEvent ), 0 ) != pdFALSE )
                 {

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

@@ -6,10 +6,55 @@
 #include "FreeRTOS_IP.h"
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
+#include "FreeRTOS_Routing.h"
+
+/* Global variables accessible throughout the program. Used in adding
+ * Network interface/endpoint. */
+NetworkInterface_t xNetworkInterface1;
+NetworkEndPoint_t xEndPoint1;
+
+const uint8_t ucIPAddress2[ 4 ];
+const uint8_t ucNetMask2[ 4 ];
+const uint8_t ucGatewayAddress2[ 4 ];
+const uint8_t ucDNSServerAddress2[ 4 ];
+const uint8_t ucMACAddress[ 6 ];
 
 void harness()
 {
+    NetworkBufferDescriptor_t xLocalNetworkBufferDescriptor;
     ARPPacket_t xARPFrame;
+    NetworkEndPoint_t xLocalEndPoint;
+
+    /* The Ethernet buffer must contain the ARP packet. */
+    xLocalNetworkBufferDescriptor.pucEthernetBuffer = &xARPFrame;
+
+    /* Non-deterministically add an end-point to the descriptor. */
+    xLocalNetworkBufferDescriptor.pxEndPoint = nondet_bool() ? NULL : &xLocalEndPoint;
+
+    /* Assume that the list of interfaces/endpoints is not initialized. */
+    __CPROVER_assume( pxNetworkInterfaces == NULL );
+    __CPROVER_assume( pxNetworkEndPoints == NULL );
+
+    /* Non-deterministically add a network-interface. */
+    if( nondet_bool() )
+    {
+        /* Add the network interfaces to the list. */
+        FreeRTOS_AddNetworkInterface( &xNetworkInterface1 );
+
+        /* Non-deterministically add an end-point to the network-interface. */
+        if( nondet_bool() )
+        {
+            /* Fill the endpoints and put them in the network interface. */
+            FreeRTOS_FillEndPoint( &xNetworkInterface1,
+                                   &xEndPoint1,
+                                   ucIPAddress2,
+                                   ucNetMask2,
+                                   ucGatewayAddress2,
+                                   ucDNSServerAddress2,
+                                   ucMACAddress );
+        }
+    }
 
-    eARPProcessPacket( &xARPFrame );
+    /* A valid network buffer must be passed to the function under test. */
+    eARPProcessPacket( &xLocalNetworkBufferDescriptor );
 }

test/cbmc/proofs/ARP/ARPProcessPacket/Configurations.json

@@ -3,13 +3,14 @@
   "CBMCFLAGS":
   [
       "--unwind 1",
-      "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
+      "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17,FreeRTOS_FindEndPointOnIP_IPv4.0:2",
       "--nondet-static"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/FreeRTOS_ARP.goto"
+    "$(FREERTOS_PLUS_TCP)/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/FreeRTOS_Routing.goto"
   ],
   "DEF":
   [

test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c

@@ -5,12 +5,62 @@
 /* FreeRTOS+TCP includes. */
 #include "FreeRTOS_IP.h"
 #include "FreeRTOS_ARP.h"
+#include "FreeRTOS_Routing.h"
+
+/* Global variables accessible throughout the program. Used in adding
+ * Network interface/endpoint. */
+NetworkInterface_t xNetworkInterface1;
+NetworkEndPoint_t xEndPoint1;
+
+const uint8_t ucIPAddress2[ 4 ];
+const uint8_t ucNetMask2[ 4 ];
+const uint8_t ucGatewayAddress2[ 4 ];
+const uint8_t ucDNSServerAddress2[ 4 ];
+const uint8_t ucMACAddress[ 6 ];
+
+/** A list of all network end-points.  Each element has a next pointer. */
+extern struct xNetworkEndPoint * pxNetworkEndPoints;
+
+/** A list of all network interfaces: */
+extern struct xNetworkInterface * pxNetworkInterfaces;
 
 void harness()
 {
     MACAddress_t xMACAddress;
     uint32_t ulIPAddress;
+    struct xNetworkEndPoint xLocalEndPoint;
+    struct xNetworkEndPoint * pxLocalEndPointPointer;
+    MACAddress_t * pxLocalMACPointer;
+
+    /* Assume that the list of interfaces/endpoints is not initialized.
+     * Note: These variables are defined in FreeRTOS_Routing.c in global scope.
+     *       They serve as a list to the network interfaces and the corresponding
+     *       endpoints respectively. And are defined as NULL initially. */
+    __CPROVER_assume( pxNetworkInterfaces == NULL );
+    __CPROVER_assume( pxNetworkEndPoints == NULL );
+
+    /* Non-deterministically add a network-interface and its endpoint. */
+    if( nondet_bool() )
+    {
+        /* Add the network interfaces to the list. */
+        FreeRTOS_AddNetworkInterface( &xNetworkInterface1 );
+
+        /* Fill the endpoints and put them in the network interface. */
+        FreeRTOS_FillEndPoint( &xNetworkInterface1,
+                               &xEndPoint1,
+                               ucIPAddress2,
+                               ucNetMask2,
+                               ucGatewayAddress2,
+                               ucDNSServerAddress2,
+                               ucMACAddress );
+    }
+
+    /* Arbitrarily assign a NULL/non-NULL value to the pointer. */
+    pxLocalEndPointPointer = nondet_bool() ? NULL : &xLocalEndPoint;
+
+    /* Arbitrarily assign a NULL/non-NULL value to the pointer. */
+    pxLocalMACPointer = nondet_bool() ? NULL : &xMACAddress;
 
-    vARPRefreshCacheEntry( &xMACAddress, ulIPAddress );
-    vARPRefreshCacheEntry( NULL, ulIPAddress );
+    /* Call the function under test. */
+    vARPRefreshCacheEntry( pxLocalMACPointer, ulIPAddress, pxLocalEndPointPointer );
 }

test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json

@@ -9,7 +9,8 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/FreeRTOS_ARP.goto"
+    "$(FREERTOS_PLUS_TCP)/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/FreeRTOS_Routing.goto"
   ],
   "DEF":
   [