Fix CBMC issues

Author: ActoryOu

source/FreeRTOS_DHCP.c

@@ -81,7 +81,7 @@
 /**
  * @brief The number of end-points that are making use of the UDP-socket.
  */
-    static BaseType_t xDHCPSocketUserCount = 0;
+    _static BaseType_t xDHCPSocketUserCount = 0;
 
 /*
  * Generate a DHCP discover message and send it on the DHCP socket.
@@ -881,7 +881,7 @@
             configASSERT( xSocketValid( xDHCPv4Socket ) == pdTRUE );
 
             /* MISRA Ref 11.4.1 [Socket error and integer to pointer conversion] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-114 */
+            /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-114 */
             /* coverity[misra_c_2012_rule_11_4_violation] */
             if( xSocketValid( xDHCPv4Socket ) == pdTRUE )
             {

source/FreeRTOS_DHCPv6.c

@@ -85,11 +85,11 @@
       ( ( ( uint32_t ) 1U ) << DHCPv6_Option_Server_Identifier ) )
 
 /** @brief The UDP socket which is shared by all end-points that need DHCPv6. */
-static Socket_t xDHCPv6Socket;
+_static Socket_t xDHCPv6Socket;
 
 /** @brief A reference count makes sure that the UDP socket will be deleted when it
  * is not used anymore. */
-static BaseType_t xDHCPv6SocketUserCount;
+_static BaseType_t xDHCPv6SocketUserCount;
 
 static BaseType_t prvIsOptionLengthValid( uint16_t usOption,
                                           size_t uxOptionLength,
@@ -151,7 +151,7 @@ static BaseType_t prvDHCPv6_handleOption( struct xNetworkEndPoint * pxEndPoint,
 /**
  * @brief DHCP IPv6 message object
  */
-static DHCPMessage_IPv6_t xDHCPMessage;
+_static DHCPMessage_IPv6_t xDHCPMessage;
 
 /**
  * @brief Get the DHCP state from a given endpoint.
@@ -1492,6 +1492,7 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
             xSet.uxOptionLength = ( size_t ) usBitConfig_read_16( &xMessage );
             xSet.uxStart = xMessage.uxIndex;
 
+            /* ulOptionsReceived has only 32-bits, it's not allowed to shift more than 32-bits on it. */
             if( xMessage.xHasError != pdFALSE )
             {
                 FreeRTOS_printf( ( "prvDHCPv6Analyse: bad input\n" ) );
@@ -1500,7 +1501,12 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint,
             }
             else
             {
-                ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption );
+                if( usOption < 32 )
+                {
+                    /* Store the option by bit-map only if it's less than 32. */
+                    ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption );
+                }
+
                 xReady = prvDHCPv6_handleOption( pxEndPoint, usOption, &( xSet ), pxDHCPMessage, &( xMessage ) );
             }
 

source/FreeRTOS_DNS_Parser.c

@@ -1093,7 +1093,7 @@
                     /* Define the ASCII value of the capital "A". */
                     const uint8_t ucCharA = ( uint8_t ) 0x41U;
 
-                    ucByte = ( uint8_t ) ( ( ( pucSource[ 0 ] - ucCharA ) << 4 ) |
+                    ucByte = ( uint8_t ) ( ( ( ( pucSource[ 0 ] - ucCharA ) & 0x0F ) << 4 ) |
                                            ( pucSource[ 1 ] - ucCharA ) );
 
                     /* Make sure there are no trailing spaces in the name. */

source/FreeRTOS_IP_Utils.c

@@ -1694,6 +1694,81 @@ size_t FreeRTOS_min_size_t( size_t a,
 }
 /*-----------------------------------------------------------*/
 
+/**
+ * @brief Performs a safe addition of two 32-bit integers, preventing overflow and underflow.
+ * @param[in] a the first value.
+ * @param[in] b the second value.
+ * @return The result of a + b if no overflow/underflow occurs, or INT32_MAX/INT32_MIN if overflow/underflow would occur.
+ */
+int32_t FreeRTOS_add_int32( int32_t a,
+                            int32_t b )
+{
+    int32_t ret;
+
+    if( ( a > 0 ) && ( b > ipINT32_MAX_VALUE - a ) )
+    {
+        ret = ipINT32_MAX_VALUE; /* Positive overflow */
+    }
+    else if( ( a < 0 ) && ( b < ipINT32_MIN_VALUE - a ) )
+    {
+        ret = ipINT32_MIN_VALUE; /* Negative underflow */
+    }
+    else
+    {
+        ret = a + b;
+    }
+
+    return ret;
+}
+/*-----------------------------------------------------------*/
+
+/**
+ * @brief Performs a safe multiplication of two 32-bit integers, preventing overflow and underflow.
+ * @param[in] a the first value.
+ * @param[in] b the second value.
+ * @return The result of a * b if no overflow occurs, or ipINT32_MAX_VALUE if an overflow would occur.
+ */
+int32_t FreeRTOS_multiply_int32( int32_t a,
+                                 int32_t b )
+{
+    int32_t ret;
+
+    /* Check for overflow/underflow */
+    if( a > 0 )
+    {
+        if( ( b > 0 ) && ( a > ipINT32_MAX_VALUE / b ) )
+        {
+            ret = ipINT32_MAX_VALUE; /* Positive overflow */
+        }
+        else if( ( b < 0 ) && ( b < ipINT32_MIN_VALUE / a ) )
+        {
+            ret = ipINT32_MIN_VALUE; /* Negative underflow */
+        }
+        else
+        {
+            ret = a * b;
+        }
+    }
+    else
+    {
+        if( ( b > 0 ) && ( a < ipINT32_MIN_VALUE / b ) )
+        {
+            ret = ipINT32_MIN_VALUE; /* Negative underflow */
+        }
+        else if( ( b < 0 ) && ( a < ipINT32_MAX_VALUE / b ) )
+        {
+            ret = ipINT32_MAX_VALUE; /* Positive overflow */
+        }
+        else
+        {
+            ret = a * b;
+        }
+    }
+
+    return ret;
+}
+/*-----------------------------------------------------------*/
+
 /**
  * @brief Round-up a number to a multiple of 'd'.
  * @param[in] a the first value.

source/FreeRTOS_TCP_Reception.c

@@ -99,7 +99,7 @@
         size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer );
 
         /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+        /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
         /* coverity[misra_c_2012_rule_11_3_violation] */
         const ProtocolHeaders_t * pxProtocolHeaders = ( ( ProtocolHeaders_t * )
                                                         &( pxNetworkBuffer->pucEthernetBuffer[ uxTCPHeaderOffset ] ) );
@@ -237,7 +237,17 @@
                     /* Option is only valid in SYN phase. */
                     if( xHasSYNFlag != 0 )
                     {
-                        pxSocket->u.xTCP.ucPeerWinScaleFactor = pucPtr[ 2 ];
+                        /* From RFC7323 - section 2.3, we should limit the WSopt not larger than 14. */
+                        if( pucPtr[ 2 ] > tcpTCP_OPT_WSOPT_MAXIMUM_VALUE )
+                        {
+                            FreeRTOS_debug_printf( ( "The WSopt(%u) from SYN packet is larger than maximum value.", pucPtr[ 2 ] ) );
+                            pxSocket->u.xTCP.ucPeerWinScaleFactor = tcpTCP_OPT_WSOPT_MAXIMUM_VALUE;
+                        }
+                        else
+                        {
+                            pxSocket->u.xTCP.ucPeerWinScaleFactor = pucPtr[ 2 ];
+                        }
+
                         pxSocket->u.xTCP.bits.bWinScaling = pdTRUE_UNSIGNED;
                     }
 
@@ -430,7 +440,7 @@
         /* Map the ethernet buffer onto the ProtocolHeader_t struct for easy access to the fields. */
 
         /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+        /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
         /* coverity[misra_c_2012_rule_11_3_violation] */
         const ProtocolHeaders_t * pxProtocolHeaders = ( ( ProtocolHeaders_t * )
                                                         &( pxNetworkBuffer->pucEthernetBuffer[ ( size_t ) ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer ) ] ) );

source/FreeRTOS_TCP_WIN.c

@@ -1901,18 +1901,33 @@
                                                      const TCPSegment_t * pxSegment )
         {
             int32_t mS = ( int32_t ) ulTimerGetAge( &( pxSegment->xTransmitTimer ) );
+            int32_t lSum = 0;
+            int32_t weight = 0;
+            int32_t divisor = 0;
+
+            mS = mS < 0 ? ipINT32_MAX_VALUE : mS;
 
             if( pxWindow->lSRTT >= mS )
             {
                 /* RTT becomes smaller: adapt slowly. */
-                pxWindow->lSRTT = ( ( winSRTT_DECREMENT_NEW * mS ) + ( winSRTT_DECREMENT_CURRENT * pxWindow->lSRTT ) ) / ( winSRTT_DECREMENT_NEW + winSRTT_DECREMENT_CURRENT );
+                weight = winSRTT_DECREMENT_CURRENT;
+                divisor = winSRTT_DECREMENT_NEW + winSRTT_DECREMENT_CURRENT;
+                mS = FreeRTOS_multiply_int32( mS,
+                                              winSRTT_DECREMENT_NEW );
             }
             else
             {
                 /* RTT becomes larger: adapt quicker */
-                pxWindow->lSRTT = ( ( winSRTT_INCREMENT_NEW * mS ) + ( winSRTT_INCREMENT_CURRENT * pxWindow->lSRTT ) ) / ( winSRTT_INCREMENT_NEW + winSRTT_INCREMENT_CURRENT );
+                weight = winSRTT_INCREMENT_CURRENT;
+                divisor = winSRTT_INCREMENT_NEW + winSRTT_INCREMENT_CURRENT;
+                mS = FreeRTOS_multiply_int32( mS,
+                                              winSRTT_INCREMENT_NEW );
             }
 
+            lSum = FreeRTOS_multiply_int32( pxWindow->lSRTT, weight );
+            lSum = FreeRTOS_add_int32( lSum, mS );
+            pxWindow->lSRTT = lSum / divisor;
+
             /* Cap to the minimum of 50ms. */
             if( pxWindow->lSRTT < winSRTT_CAP_mS )
             {
@@ -1946,7 +1961,7 @@
             const ListItem_t * pxIterator;
 
             /* MISRA Ref 11.3.1 [Misaligned access] */
-/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
+            /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */
             /* coverity[misra_c_2012_rule_11_3_violation] */
             const ListItem_t * pxEnd = ( ( const ListItem_t * ) &( pxWindow->xTxSegments.xListEnd ) );
             BaseType_t xDoUnlink;

source/include/FreeRTOS_IP.h

@@ -60,6 +60,11 @@
 #define ipSIZE_OF_UDP_HEADER     8U
 #define ipSIZE_OF_TCP_HEADER     20U
 
+/* The maximum of int32 value. */
+#define ipINT32_MAX_VALUE        ( 0x7FFFFFFF )
+
+/* The minimum of int32 value. */
+#define ipINT32_MIN_VALUE        ( 0x80000000 )
 
 /*
  * Generate a randomized TCP Initial Sequence Number per RFC.
@@ -270,6 +275,11 @@ uint32_t FreeRTOS_min_uint32( uint32_t a,
 size_t FreeRTOS_min_size_t( size_t a,
                             size_t b );
 
+int32_t FreeRTOS_add_int32( int32_t a,
+                             int32_t b );
+int32_t FreeRTOS_multiply_int32( int32_t a,
+                             int32_t b );
+
 uint32_t FreeRTOS_round_up( uint32_t a,
                             uint32_t d );
 uint32_t FreeRTOS_round_down( uint32_t a,

source/include/FreeRTOS_TCP_IP.h

@@ -107,6 +107,7 @@ typedef enum eTCP_STATE
 
 #define tcpTCP_OPT_MSS_LEN           4U                  /**< Length of TCP MSS option. */
 #define tcpTCP_OPT_WSOPT_LEN         3U                  /**< Length of TCP WSOPT option. */
+#define tcpTCP_OPT_WSOPT_MAXIMUM_VALUE ( 14U )           /**< Maximum value of TCP WSOPT option. */
 
 #define tcpTCP_OPT_TIMESTAMP_LEN     10                  /**< fixed length of the time-stamp option. */
 

test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c

@@ -12,6 +12,7 @@ void harness()
 {
     uint32_t ulIPAddress;
     MACAddress_t xMACAddress;
+    struct xNetworkEndPoint * pxEndPoint = NULL;
 
     /*
      * For this proof, its assumed that the endpoints and interfaces are correctly
@@ -38,13 +39,5 @@ void harness()
         pxNetworkEndPoints->pxNext = NULL;
     }
 
-    NetworkInterface_t ** ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
-
-    if( ppxInterface )
-    {
-        *ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-        __CPROVER_assume( *ppxInterface != NULL );
-    }
-
-    eARPGetCacheEntry( &ulIPAddress, &xMACAddress, ppxInterface );
+    eARPGetCacheEntry( &ulIPAddress, &xMACAddress, &pxEndPoint );
 }

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c

@@ -100,6 +100,7 @@ void harness()
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;