Merge branch 'main' into unittest-warnings

Author: tony-josi-aws

source/FreeRTOS_DHCP.c

@@ -224,6 +224,13 @@
                     {
                         FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                     }
+                    else if( lBytes >= 0 )
+                    {
+                        vReleaseSinglePacketFromUDPSocket( EP_DHCPData.xDHCPSocket );
+                    }
+                    else
+                    {
+                    }
 
                     break;
                 }
@@ -257,7 +264,7 @@
                     pxIterator = NULL;
                 }
 
-                if( pxIterator != NULL )
+                if( ( pxIterator != NULL ) && ( pxIterator->xDHCPData.eDHCPState == pxIterator->xDHCPData.eExpectedState ) )
                 {
                     /* The second parameter pdTRUE tells to check for a UDP message. */
                     vDHCPProcessEndPoint( pdFALSE, pdTRUE, pxIterator );
@@ -269,15 +276,24 @@
                 }
                 else
                 {
-                    /* Target not found, fetch the message and delete it. */
+                    /* Target not found or there is a state mismatch, fetch the message and delete it. */
                     /* PAss the address of a pointer pucUDPPayload, because zero-copy is used. */
                     lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, FREERTOS_ZERO_COPY, NULL, NULL );
 
                     if( ( lBytes > 0 ) && ( pucUDPPayload != NULL ) )
                     {
                         /* Remove it now, destination not found. */
                         FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
-                        FreeRTOS_printf( ( "vDHCPProcess: Removed a %d-byte message: target not found\n", ( int ) lBytes ) );
+
+                        if( pxIterator == NULL )
+                        {
+                            FreeRTOS_printf( ( "vDHCPProcess: Removed a %d-byte message: target not found\n", ( int ) lBytes ) );
+                        }
+                        else
+                        {
+                            FreeRTOS_printf( ( "vDHCPProcess: Wrong state: expected: %d got: %d : ignore\n",
+                                               pxIterator->xDHCPData.eExpectedState, pxIterator->xDHCPData.eDHCPState ) );
+                        }
                     }
                 }
             }
@@ -489,6 +505,11 @@
                 {
                     /* Give up, start again. */
                     EP_DHCPData.eDHCPState = eInitialWait;
+
+                    /* Reset expected state so that DHCP packets from
+                     * different DHCP servers if available already in the DHCP socket can
+                     * be processed */
+                    EP_DHCPData.eExpectedState = eInitialWait;
                 }
             }
         }
@@ -992,6 +1013,11 @@
                         {
                             /* Start again. */
                             EP_DHCPData.eDHCPState = eInitialWait;
+
+                            /* Reset expected state so that DHCP packets from
+                             * different DHCP servers if available already in the DHCP socket can
+                             * be processed */
+                            EP_DHCPData.eExpectedState = eInitialWait;
                         }
                     }
 

source/FreeRTOS_DHCPv6.c

@@ -436,6 +436,13 @@ void vDHCPv6Process( BaseType_t xReset,
                 {
                     FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                 }
+                else if( lBytes == 0 )
+                {
+                    vReleaseSinglePacketFromUDPSocket( EP_DHCPData.xDHCPSocket );
+                }
+                else
+                {
+                }
 
                 break;
             }
@@ -450,6 +457,8 @@ void vDHCPv6Process( BaseType_t xReset,
             {
                 xDoProcess = xDHCPv6Process_PassReplyToEndPoint( pxEndPoint );
             }
+
+            FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
         }
     }
 

source/FreeRTOS_IP_Utils.c

@@ -1825,6 +1825,27 @@ uint32_t FreeRTOS_round_down( uint32_t a,
 }
 /*-----------------------------------------------------------*/
 
+/**
+ * @brief Release single UDP packet from a given socket
+ * @param[in] xSocket UDP Socket from which the packet should be released.
+ */
+void vReleaseSinglePacketFromUDPSocket( const ConstSocket_t xSocket )
+{
+    uint8_t * pucUDPPayload = NULL;
+    int32_t lBytes;
+
+    /* Passing the address of a pointer (pucUDPPayload) because FREERTOS_ZERO_COPY is used. */
+    lBytes = FreeRTOS_recvfrom( xSocket, &pucUDPPayload, 0U, FREERTOS_ZERO_COPY, NULL, NULL );
+
+    ( void ) lBytes;
+
+    if( pucUDPPayload != NULL )
+    {
+        FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+    }
+}
+/*-----------------------------------------------------------*/
+
 /**
  * @brief Convert character array (of size 4) to equivalent 32-bit value.
  * @param[in] pucPtr The character array.

source/include/FreeRTOS_IP_Utils.h

@@ -109,6 +109,10 @@ void vPreCheckConfigs( void );
  */
 void prvProcessNetworkDownEvent( struct xNetworkInterface * pxInterface );
 
+/**
+ * @brief Release single UDP packet from a given socket
+ */
+void vReleaseSinglePacketFromUDPSocket( const ConstSocket_t xSocket );
 
 /* *INDENT-OFF* */
 #ifdef __cplusplus

test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c

@@ -153,6 +153,16 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket,
     return retVal;
 }
 
+/* For the purpose of this proof we stub the
+ * implementation of FreeRTOS_ReleaseUDPPayloadBuffer here, but make sure that
+ * the pvBuffer is not NULL, its not verified here if the pointer is a valid
+ * payload buffer as its proved in other proofs */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+}
+
 void harness()
 {
     BaseType_t xReset;

test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json

@@ -5,6 +5,7 @@
     "CBMCFLAGS":
     [
       "--unwind {LOOP_UNWIND_COUNT}",
+      "--unwindset memcmp.0:17",
       "--nondet-static --flush"
     ],
     "OPT":

test/unit-test/FreeRTOS_DHCP/FreeRTOS_DHCP_stubs.c

@@ -715,4 +715,38 @@ static int32_t FreeRTOS_recvfrom_eWaitingOfferRecvfromSuccess_LocalMACAddrNotMat
 
     return xSizeofUDPBuffer;
 }
+
+static int32_t FreeRTOS_recvfrom_LoopedCall( const ConstSocket_t xSocket,
+                                             void * pvBuffer,
+                                             size_t uxBufferLength,
+                                             BaseType_t xFlags,
+                                             struct freertos_sockaddr * pxSourceAddress,
+                                             socklen_t * pxSourceAddressLength,
+                                             int callbacks )
+{
+    NetworkEndPoint_t * pxIterator = pxNetworkEndPoints;
+    size_t xSizeRetBufferSize = xSizeofUDPBuffer;
+
+    if( callbacks == 2 )
+    {
+        pxNetworkEndPoints->xDHCPData.eDHCPState = eInitialWait;
+    }
+    else if( callbacks == 4 )
+    {
+        xSizeRetBufferSize = 200;
+    }
+
+    if( ( xFlags & FREERTOS_ZERO_COPY ) != 0 )
+    {
+        *( ( uint8_t ** ) pvBuffer ) = pucUDPBuffer;
+    }
+
+    memset( pucUDPBuffer, 0, xSizeofUDPBuffer );
+    /* Put in correct DHCP cookie. */
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ulDHCPCookie = dhcpCOOKIE;
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ucOpcode = dhcpREPLY_OPCODE;
+    ( ( struct xDHCPMessage_IPv4 * ) pucUDPBuffer )->ulTransactionID = FreeRTOS_htonl( 0x01ABCDEF );
+
+    return xSizeRetBufferSize;
+}
 /*-----------------------------------------------------------*/