diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ba6a8c1660..a012e162bc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -406,7 +406,7 @@ jobs: - name: Set up CBMC runner uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main with: - cbmc_version: "5.95.1" + cbmc_version: "6.3.1" - env: stepName: Install Dependencies diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index eccba8d5d7..819d2c59e0 100644 --- a/source/FreeRTOS_DHCP.c +++ b/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. @@ -880,7 +880,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 ) { diff --git a/source/FreeRTOS_DHCPv6.c b/source/FreeRTOS_DHCPv6.c index 6c26b87069..6bf6fc50a0 100644 --- a/source/FreeRTOS_DHCPv6.c +++ b/source/FreeRTOS_DHCPv6.c @@ -80,11 +80,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, @@ -146,7 +146,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. @@ -1495,7 +1495,13 @@ static BaseType_t prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint, } else { - ulOptionsReceived |= ( ( ( uint32_t ) 1U ) << usOption ); + /* ulOptionsReceived has only 32-bits, it's not allowed to shift more than 32-bits on it. */ + 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 ) ); } diff --git a/source/FreeRTOS_DNS_Parser.c b/source/FreeRTOS_DNS_Parser.c index 13fb75a858..6aa3306f69 100644 --- a/source/FreeRTOS_DNS_Parser.c +++ b/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. */ diff --git a/source/FreeRTOS_IP_Utils.c b/source/FreeRTOS_IP_Utils.c index 02e1cbe46c..f7491c6390 100644 --- a/source/FreeRTOS_IP_Utils.c +++ b/source/FreeRTOS_IP_Utils.c @@ -1706,6 +1706,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. diff --git a/source/FreeRTOS_TCP_Reception.c b/source/FreeRTOS_TCP_Reception.c index cad11e9a96..4f1003a67c 100644 --- a/source/FreeRTOS_TCP_Reception.c +++ b/source/FreeRTOS_TCP_Reception.c @@ -98,7 +98,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 ] ) ); @@ -236,7 +236,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; } @@ -429,7 +439,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 ) ] ) ); diff --git a/source/FreeRTOS_TCP_WIN.c b/source/FreeRTOS_TCP_WIN.c index 543ce28769..87f4488b2c 100644 --- a/source/FreeRTOS_TCP_WIN.c +++ b/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 lWeight = 0; + int32_t lDivisor = 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 ); + lWeight = winSRTT_DECREMENT_CURRENT; + lDivisor = 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 ); + lWeight = winSRTT_INCREMENT_CURRENT; + lDivisor = winSRTT_INCREMENT_NEW + winSRTT_INCREMENT_CURRENT; + mS = FreeRTOS_multiply_int32( mS, + winSRTT_INCREMENT_NEW ); } + lSum = FreeRTOS_multiply_int32( pxWindow->lSRTT, lWeight ); + lSum = FreeRTOS_add_int32( lSum, mS ); + pxWindow->lSRTT = lSum / lDivisor; + /* 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; diff --git a/source/include/FreeRTOS_IP.h b/source/include/FreeRTOS_IP.h index b9ba9b7bbd..ecd12a1c94 100644 --- a/source/include/FreeRTOS_IP.h +++ b/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 ( ( int32_t ) 0x7FFFFFFF ) + +/* The minimum of int32 value. */ +#define ipINT32_MIN_VALUE ( ( int32_t ) 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, diff --git a/source/include/FreeRTOS_TCP_IP.h b/source/include/FreeRTOS_TCP_IP.h index 0e00c8a729..e2a5dc398b 100644 --- a/source/include/FreeRTOS_TCP_IP.h +++ b/source/include/FreeRTOS_TCP_IP.h @@ -96,25 +96,26 @@ typedef enum eTCP_STATE /* * A few values of the TCP options: */ -#define tcpTCP_OPT_END 0U /**< End of TCP options list. */ -#define tcpTCP_OPT_NOOP 1U /**< "No-operation" TCP option. */ -#define tcpTCP_OPT_MSS 2U /**< Maximum segment size TCP option. */ -#define tcpTCP_OPT_WSOPT 3U /**< TCP Window Scale Option (3-byte long). */ -#define tcpTCP_OPT_SACK_P 4U /**< Advertise that SACK is permitted. */ -#define tcpTCP_OPT_SACK_A 5U /**< SACK option with first/last. */ -#define tcpTCP_OPT_TIMESTAMP 8U /**< Time-stamp option. */ +#define tcpTCP_OPT_END 0U /**< End of TCP options list. */ +#define tcpTCP_OPT_NOOP 1U /**< "No-operation" TCP option. */ +#define tcpTCP_OPT_MSS 2U /**< Maximum segment size TCP option. */ +#define tcpTCP_OPT_WSOPT 3U /**< TCP Window Scale Option (3-byte long). */ +#define tcpTCP_OPT_SACK_P 4U /**< Advertise that SACK is permitted. */ +#define tcpTCP_OPT_SACK_A 5U /**< SACK option with first/last. */ +#define tcpTCP_OPT_TIMESTAMP 8U /**< Time-stamp option. */ -#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_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. */ +#define tcpTCP_OPT_TIMESTAMP_LEN 10 /**< fixed length of the time-stamp option. */ /** @brief * Minimum segment length as outlined by RFC 791 section 3.1. * Minimum segment length ( 536 ) = Minimum MTU ( 576 ) - IP Header ( 20 ) - TCP Header ( 20 ). */ -#define tcpMINIMUM_SEGMENT_LENGTH 536U +#define tcpMINIMUM_SEGMENT_LENGTH 536U /** @brief * The macro tcpNOW_CONNECTED() is use to determine if the connection makes a diff --git a/test/Coverity/README.md b/test/Coverity/README.md index 8b4614eed5..7307141ea7 100644 --- a/test/Coverity/README.md +++ b/test/Coverity/README.md @@ -13,7 +13,7 @@ see the [MISRA.md](https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA ## Getting Started ### Prerequisites -You can run this on a platform supported by Coverity. The list and other details can be found [here](https://sig-docs.synopsys.com/polaris/topics/c_coverity-compatible-platforms.html). +You can run this on a platform supported by Coverity. The list and other details can be found [here](https://documentation.blackduck.com/bundle/coverity-docs/page/deploy-install-guide/topics/supported_platforms_for_coverity_analysis.html). To compile and run the Coverity target successfully, you must have the following: 1. CMake version > 3.13.0 (You can check whether you have this by typing `cmake --version`) diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c index 9b1e4b227c..51bad65b7e 100644 --- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c +++ b/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 ); } 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 03c74e467c..24762ed1cd 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 @@ -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; 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 b87ae8b30e..af3abf26e9 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 @@ -80,6 +80,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; diff --git a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c index 8ac5d6a827..3da849aaf4 100644 --- a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c +++ b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -32,8 +32,6 @@ void __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( const uint * Proof of prvReadSackOption function contract ****************************************************************/ - - void harness() { /* pucPtr points into a buffer */ @@ -97,6 +95,8 @@ void harness() /* Assuming quite a bit more about the initialization of pxSocket */ __CPROVER_assume( pucPtr != NULL ); __CPROVER_assume( pxSocket != NULL ); + /* lSRTT is guaranteed to be always greater than or equal to minimum value. */ + __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.lSRTT >= ipconfigTCP_SRTT_MINIMUM_VALUE_MS ); __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( pucPtr, uxIndex, pxSocket ); diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c index 29fabf6576..6ba76d4be0 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -49,6 +49,7 @@ /* Static members defined in FreeRTOS_DHCP.c */ extern DHCPData_t xDHCPData; extern Socket_t xDHCPv4Socket; +extern BaseType_t xDHCPSocketUserCount; void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint ); uint32_t uxSocketCloseCnt = 0; @@ -182,6 +183,9 @@ void harness() BaseType_t xReset; eDHCPState_t eExpectedState; + /* The only possibility of making xDHCPSocketUserCount overflow is having more than BaseType_t endpoints, which is assumed not possible here. */ + __CPROVER_assume( xDHCPSocketUserCount >= 0 && xDHCPSocketUserCount <= ENDPOINT_DNS_ADDRESS_COUNT ); + pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index f74a67537a..8de985a953 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -33,6 +33,7 @@ "BUFFER_SIZE={BUFFER_SIZE}", "ipconfigDHCP_REGISTER_HOSTNAME=1", "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", - "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}", + "ENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ] } diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c index bd53b27456..74891fa02a 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c +++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c @@ -51,6 +51,7 @@ /* Static members defined in FreeRTOS_DHCP.c */ extern DHCPData_t xDHCPData; extern Socket_t xDHCPv4Socket; +extern BaseType_t xDHCPSocketUserCount; void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint ); /* Static member defined in freertos_api.c */ @@ -184,6 +185,9 @@ void harness() BaseType_t xReset; BaseType_t xDoCheck; + /* The only possibility of making xDHCPSocketUserCount overflow is having more than BaseType_t endpoints, which is assumed not possible here. */ + __CPROVER_assume( xDHCPSocketUserCount >= 0 && xDHCPSocketUserCount <= ENDPOINT_DNS_ADDRESS_COUNT ); + pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json index 59cfc8cc63..75426470db 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json @@ -34,6 +34,7 @@ "BUFFER_SIZE={BUFFER_SIZE}", "ipconfigDHCP_REGISTER_HOSTNAME=1", "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1", - "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}" + "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}", + "ENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ] } diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c index bba0186807..cb8a71af06 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c @@ -52,6 +52,19 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( struct xNetw size_t uxTotalLength, DHCPMessage_IPv6_t * pxDHCPMessage ); +/* prvDHCPv6_handleOption is tested separately. Using mock function in this test case. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption( struct xNetworkEndPoint * pxEndPoint, + uint16_t usOption, + const DHCPOptionSet_t * pxSet, + DHCPMessage_IPv6_t * pxDHCPMessage, + BitConfig_t * pxMessage ) +{ + __CPROVER_assert( __CPROVER_r_ok( pxEndPoint, sizeof( struct xNetworkEndPoint ) ), "pxEndPoint region must be readable" ); + __CPROVER_assert( __CPROVER_r_ok( pxSet, sizeof( DHCPOptionSet_t ) ), "pxSet region must be readable" ); + __CPROVER_assert( __CPROVER_r_ok( pxDHCPMessage, sizeof( DHCPMessage_IPv6_t ) ), "pxDHCPMessage region must be readable" ); + __CPROVER_assert( __CPROVER_r_ok( pxMessage, sizeof( BitConfig_t ) ), "pxMessage region must be readable" ); +} + void harness() { size_t uxTotalLength; diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json index 08e8432de6..8a2b998f63 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json @@ -9,7 +9,6 @@ ], "INSTFLAGS": [ - "--remove-function-body __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption", "--malloc-may-fail" ], "OPT": diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c index 6e82bf284b..980c620853 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c @@ -46,6 +46,7 @@ extern Socket_t xDHCPv6Socket; extern DHCPMessage_IPv6_t xDHCPMessage; +extern BaseType_t xDHCPv6SocketUserCount; void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( NetworkEndPoint_t * pxEndPoint ); @@ -156,6 +157,8 @@ void harness() { BaseType_t xReset; + __CPROVER_assume( xDHCPv6SocketUserCount >= 0 && xDHCPv6SocketUserCount <= ENDPOINT_DNS_ADDRESS_COUNT ); + NetworkEndPoint_t * pxNetworkEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint != NULL ); diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json index fba06214ba..5a2d345cb4 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json @@ -1,6 +1,7 @@ { "ENTRY": "DHCPv6Process", "LOOP_UNWIND_COUNT": 4, + "ENDPOINT_DNS_ADDRESS_COUNT": 5, "CBMCFLAGS": [ "--unwind {LOOP_UNWIND_COUNT}", @@ -13,7 +14,8 @@ "DEF": [ "ipconfigUSE_DHCPv6=1", - "FR_RECV_FROM_SUCCESS_COUNT={LOOP_UNWIND_COUNT}" + "FR_RECV_FROM_SUCCESS_COUNT={LOOP_UNWIND_COUNT}", + "ENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ], "OBJS": [ diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c index 350c13cce2..adf753da71 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c @@ -47,6 +47,7 @@ /* Static members defined in FreeRTOS_DHCP.c */ extern Socket_t xDHCPv6Socket; +extern BaseType_t xDHCPv6SocketUserCount; void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( NetworkEndPoint_t * pxEndPoint ); BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6ProcessEndPoint_HandleState( NetworkEndPoint_t * pxEndPoint, @@ -147,6 +148,8 @@ void harness() { BaseType_t xReset, xGivingUp; + __CPROVER_assume( xDHCPv6SocketUserCount >= 0 && xDHCPv6SocketUserCount <= ENDPOINT_DNS_ADDRESS_COUNT ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json index 21e1105ac8..25d5a8d6f9 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json @@ -1,5 +1,6 @@ { "ENTRY": "DHCPv6ProcessEndPoint", + "ENDPOINT_DNS_ADDRESS_COUNT": 5, "CBMCFLAGS": [ "--nondet-static --flush", @@ -11,7 +12,8 @@ ], "DEF": [ - "ipconfigUSE_DHCPv6=1" + "ipconfigUSE_DHCPv6=1", + "ENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}" ], "OBJS": [ diff --git a/test/cbmc/proofs/DNS/CreateDNSMessage/CreateDNSMessage_harness.c b/test/cbmc/proofs/DNS/CreateDNSMessage/CreateDNSMessage_harness.c index 34120f3dbd..76725b659b 100644 --- a/test/cbmc/proofs/DNS/CreateDNSMessage/CreateDNSMessage_harness.c +++ b/test/cbmc/proofs/DNS/CreateDNSMessage/CreateDNSMessage_harness.c @@ -55,6 +55,7 @@ void harness() /* pcHostName is tested to be valid prior */ char * pcHostName = malloc( len ); + __CPROVER_assume( pcHostName != NULL ); if( len && pcHostName ) { @@ -81,6 +82,7 @@ void harness() /* pucUDPPayloadBuffer is tested to be valid prior */ uint8_t * pucUDPPayloadBuffer = malloc( uxExpectedPayloadLength ); + __CPROVER_assume( pucUDPPayloadBuffer != NULL ); __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( pucUDPPayloadBuffer, pcHostName, uxIdentifier, uxHostType ); } diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c index 52106ba65f..85bb0b8fac 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c +++ b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c @@ -26,5 +26,7 @@ void harness() NetworkBufferDescriptor_t xNetworkBuffer; xNetworkBuffer.pucEthernetBuffer = malloc( sizeof( UDPPacket_t ) + sizeof( DNSMessage_t ) ); + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); + ulDNSHandlePacket( &xNetworkBuffer ); } diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c index 7d1d706698..54d13c4d6f 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c +++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c @@ -133,6 +133,7 @@ void harness() if( nondet_bool() ) { + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp; } else diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 15cf815dbb..847b0a8f2a 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -124,13 +124,13 @@ goto: # report if the proof failed. If the proof failed, we separately fail # the entire job using the check-cbmc-result rule. cbmc.xml: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 + -cbmc $(CBMCFLAGS) $(SOLVER) --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto - cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 + cbmc $(CBMCFLAGS) --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 coverage.xml: $(ENTRY).goto - cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 + cbmc $(CBMCFLAGS) --no-standard-checks --malloc-may-fail --malloc-fail-null --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 cbmc: cbmc.xml diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json index 7ada3e1dca..79e8b7bfbe 100644 --- a/test/cbmc/proofs/MakefileCommon.json +++ b/test/cbmc/proofs/MakefileCommon.json @@ -32,9 +32,7 @@ "CBMCFLAGS ": [ "--object-bits 8", - "--32", - "--bounds-check", - "--pointer-check" + "--32" ], "FORWARD_SLASH": ["/"], diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c index 123b945277..c8a7953453 100644 --- a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c +++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c @@ -82,6 +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 ); + /* ipconfigTCP_MSS is guaranteed not less than tcpMINIMUM_SEGMENT_LENGTH by FreeRTOSIPConfigDefaults.h */ + __CPROVER_assume( pxSocket->u.xTCP.usMSS >= tcpMINIMUM_SEGMENT_LENGTH ); + __CPROVER_assume( ulByteCount > 0U ); pcData = safeMalloc( ulByteCount ); __CPROVER_assume( pcData != NULL ); diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c index c73802300d..fddf816a3c 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -256,6 +256,8 @@ void harness() __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 ) ); + /* ucPeerWinScaleFactor is limited in range [0,14]. */ + __CPROVER_assume( pxSocket->u.xTCP.ucPeerWinScaleFactor <= tcpTCP_OPT_WSOPT_MAXIMUM_VALUE ); if( xIsCallingFromIPTask() == pdFALSE ) { @@ -275,6 +277,7 @@ void harness() /* Allocates min. buffer size required for the proof */ pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ); __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + pxNetworkBuffer->xDataLength = sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ); if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE ) { diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c index 02009b61f6..1e5d4dbc35 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c @@ -224,6 +224,8 @@ void harness() /* The code does not expect both of these to be equal to NULL at the same time. */ __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL ); + /* ucPeerWinScaleFactor is limited in range [0,14]. */ + __CPROVER_assume( pxSocket->u.xTCP.ucMyWinScaleFactor <= tcpTCP_OPT_WSOPT_MAXIMUM_VALUE ); /* If network buffer is properly created. */ if( pxNetworkBuffer != NULL ) 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 a5d1827c89..a51fa8ef0c 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c @@ -203,6 +203,8 @@ void harness() /* The code does not expect both of these to be equal to NULL at the same time. */ __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL ); + /* ucPeerWinScaleFactor is limited in range [0,14]. */ + __CPROVER_assume( pxSocket->u.xTCP.ucMyWinScaleFactor <= tcpTCP_OPT_WSOPT_MAXIMUM_VALUE ); /* If network buffer is properly created. */ if( pxNetworkBuffer != NULL ) diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json index f7ef2a84df..b5abd6f010 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json @@ -2,6 +2,9 @@ "ENTRY": "vProcessGeneratedUDPPacket", "CBMCFLAGS": [ + "--unwind 1", + "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3", + "--nondet-static" ], "OBJS": [ diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index 429d787342..af7bad7ca0 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -186,7 +186,7 @@ def add_proof_jobs(proof_directory, proof_root): # Run 3 CBMC tasks - cbmc_out = str(proof_directory / "cbmc.txt") + cbmc_out = str(proof_directory / "cbmc.xml") run_cmd([ "litani", "add-job", "--command", "make cbmc", @@ -301,12 +301,12 @@ def main(): if not args.no_standalone: run_build(args.parallel_jobs) - out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest" - out_dir = out_sym.resolve() + out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest" + out_dir = out_sym.resolve() - local_copy = pathlib.Path("output")/"latest" - local_copy.parent.mkdir(exist_ok=True) - local_copy.symlink_to(out_dir) + local_copy = pathlib.Path("output")/"latest" + local_copy.parent.mkdir(exist_ok=True) + local_copy.symlink_to(out_dir) if __name__ == "__main__": diff --git a/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c b/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c index 29a0492331..aa44055356 100644 --- a/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c +++ b/test/unit-test/FreeRTOS_DHCPv6/FreeRTOS_DHCPv6_utest.c @@ -729,6 +729,34 @@ static void prvPrepareAdvertiseNoServerID() prvAddOptionPreference( pdFALSE ); } +/** + * @brief Prepare buffer content as DHCPv6 advertise with extra option value 32. + */ +static void prvPrepareAdvertiseExtraOptionValue32() +{ + /* We hard code the option sequence in advertise message. + * 1. Client ID + * 2. Server ID + * 3. IA_NA + * - Sub-option IA Address + * - Sub-option IA Prefix + * - Sub-option Status Code + * 4. Status Code + * 5. Preference + * 6. Extra Option 32 + */ + uint16_t usVal; + + prvPrepareAdvertise(); + /* Add extra option with value 32. */ + usVal = 32; + vAddBitOperation( eTestDHCPv6BitOperationRead16, &usVal, 2, "ExtraOption32" ); + usVal = 2U; + vAddBitOperation( eTestDHCPv6BitOperationRead16, &usVal, 2, "ExtraOption32Length" ); + usVal = 0U; + vAddBitOperation( eTestDHCPv6BitOperationReadCustom, &usVal, 2, "ExtraOptionStatusValue" ); +} + /** * @brief Prepare buffer content as DHCPv6 advertise. */ @@ -2046,6 +2074,54 @@ void test_vDHCPv6Process_prvDHCPv6Analyse_LackServerID() TEST_ASSERT_EQUAL( eWaitingOffer, xEndPoint.xDHCPData.eDHCPState ); } +/** + * @brief Check if vDHCPv6Process can skip setting bit map when the option value is 32. + */ +void test_vDHCPv6Process_prvDHCPv6Analyse_ExtraOptionValue32() +{ + NetworkEndPoint_t xEndPoint; + DHCPMessage_IPv6_t xDHCPMessage; + struct xSOCKET xLocalDHCPv6Socket; + + memset( &xEndPoint, 0, sizeof( NetworkEndPoint_t ) ); + memset( &xLocalDHCPv6Socket, 0, sizeof( struct xSOCKET ) ); + memset( &xDHCPMessage, 0, sizeof( DHCPMessage_IPv6_t ) ); + + pxNetworkEndPoints = &xEndPoint; + + memcpy( xEndPoint.xMACAddress.ucBytes, ucDefaultMACAddress, sizeof( ucDefaultMACAddress ) ); + memcpy( xEndPoint.ipv6_settings.xPrefix.ucBytes, &xDefaultNetPrefix.ucBytes, sizeof( IPv6_Address_t ) ); + xEndPoint.ipv6_settings.uxPrefixLength = 64; + xEndPoint.bits.bIPv6 = pdTRUE; + xEndPoint.bits.bWantDHCP = pdTRUE; + + xEndPoint.xDHCPData.eDHCPState = eWaitingOffer; + xEndPoint.xDHCPData.eExpectedState = eWaitingOffer; + xEndPoint.xDHCPData.ulTransactionId = TEST_DHCPV6_TRANSACTION_ID; + xEndPoint.xDHCPData.xDHCPSocket = &xLocalDHCPv6Socket; + memcpy( xEndPoint.xDHCPData.ucClientDUID, ucTestDHCPv6OptionClientID, sizeof( ucTestDHCPv6OptionClientID ) ); + + xEndPoint.pxDHCPMessage = &xDHCPMessage; + + FreeRTOS_recvfrom_IgnoreAndReturn( 150 ); + FreeRTOS_recvfrom_IgnoreAndReturn( 0 ); + xTaskGetTickCount_IgnoreAndReturn( 0 ); + + prvPrepareAdvertiseExtraOptionValue32(); + + xApplicationGetRandomNumber_Stub( xStubxApplicationGetRandomNumber ); + FreeRTOS_inet_pton6_IgnoreAndReturn( pdTRUE ); + FreeRTOS_sendto_IgnoreAndReturn( 0 ); + + prvPrepareRequest(); + + vDHCPv6Process( pdFALSE, &xEndPoint ); + + /* The endpoint receives the DHCPv6 Advertise message from DHCPv6 server. + * Then change the state to eWaitingAcknowledge. */ + TEST_ASSERT_EQUAL( eWaitingAcknowledge, xEndPoint.xDHCPData.eDHCPState ); +} + /** * @brief Check if vDHCPv6Process can drop packets while failing on initialization of bit configuration. */ diff --git a/test/unit-test/FreeRTOS_IP_Utils/FreeRTOS_IP_Utils_utest.c b/test/unit-test/FreeRTOS_IP_Utils/FreeRTOS_IP_Utils_utest.c index cac95bf173..22b4b97fc4 100644 --- a/test/unit-test/FreeRTOS_IP_Utils/FreeRTOS_IP_Utils_utest.c +++ b/test/unit-test/FreeRTOS_IP_Utils/FreeRTOS_IP_Utils_utest.c @@ -2923,6 +2923,65 @@ void test_FreeRTOS_min_size_t( void ) } } +/** + * @brief test_FreeRTOS_add_int32 + * To validate FreeRTOS_add_int32. + */ +void test_FreeRTOS_add_int32( void ) +{ + int32_t lResult; + + lResult = FreeRTOS_add_int32( 1, 2 ); + TEST_ASSERT_EQUAL( 3, lResult ); + + lResult = FreeRTOS_add_int32( ipINT32_MAX_VALUE, 1 ); + TEST_ASSERT_EQUAL( ipINT32_MAX_VALUE, lResult ); + + lResult = FreeRTOS_add_int32( ipINT32_MIN_VALUE, -1 ); + TEST_ASSERT_EQUAL( ipINT32_MIN_VALUE, lResult ); + + lResult = FreeRTOS_add_int32( -1, 1 ); + TEST_ASSERT_EQUAL( 0, lResult ); +} + +/** + * @brief test_FreeRTOS_multiply_int32 + * To validate FreeRTOS_multiply_int32. + */ +void test_FreeRTOS_multiply_int32( void ) +{ + int32_t lResult; + + /* a > 0 */ + lResult = FreeRTOS_multiply_int32( ipINT32_MAX_VALUE, ipINT32_MAX_VALUE ); + TEST_ASSERT_EQUAL( ipINT32_MAX_VALUE, lResult ); + + lResult = FreeRTOS_multiply_int32( 10, ipINT32_MIN_VALUE ); + TEST_ASSERT_EQUAL( ipINT32_MIN_VALUE, lResult ); + + lResult = FreeRTOS_multiply_int32( 10, 10 ); + TEST_ASSERT_EQUAL( 100, lResult ); + + lResult = FreeRTOS_multiply_int32( 10, -1 ); + TEST_ASSERT_EQUAL( -10, lResult ); + + lResult = FreeRTOS_multiply_int32( 10, 0 ); + TEST_ASSERT_EQUAL( 0, lResult ); + + /* a <= 0 */ + lResult = FreeRTOS_multiply_int32( ipINT32_MIN_VALUE, 10 ); + TEST_ASSERT_EQUAL( ipINT32_MIN_VALUE, lResult ); + + lResult = FreeRTOS_multiply_int32( ipINT32_MIN_VALUE, ipINT32_MIN_VALUE ); + TEST_ASSERT_EQUAL( ipINT32_MAX_VALUE, lResult ); + + lResult = FreeRTOS_multiply_int32( -1, 10 ); + TEST_ASSERT_EQUAL( -10, lResult ); + + lResult = FreeRTOS_multiply_int32( -2, -2 ); + TEST_ASSERT_EQUAL( 4, lResult ); +} + /** * @brief test_FreeRTOS_round_up * To validate FreeRTOS_round_up. diff --git a/test/unit-test/FreeRTOS_TCP_Reception/FreeRTOS_TCP_Reception_utest.c b/test/unit-test/FreeRTOS_TCP_Reception/FreeRTOS_TCP_Reception_utest.c index a12479374b..32df8586db 100644 --- a/test/unit-test/FreeRTOS_TCP_Reception/FreeRTOS_TCP_Reception_utest.c +++ b/test/unit-test/FreeRTOS_TCP_Reception/FreeRTOS_TCP_Reception_utest.c @@ -557,6 +557,36 @@ void test_prvSingleStepTCPHeaderOptions_Invalid_Length_WS( void ) TEST_ASSERT_EQUAL( -1, result ); } +/* Test for prvSingleStepTCPHeaderOptions function with valid WSopt value. */ +void test_prvSingleStepTCPHeaderOptions_Valid_WS( void ) +{ + int32_t result; + + /* Setup TCP option for tests */ + pxNetworkBuffer = &xNetworkBuffer; + pxNetworkBuffer->pucEthernetBuffer = ucEthernetBuffer; + size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER; + + ProtocolHeaders_t * pxProtocolHeader = ( ( ProtocolHeaders_t * ) + &( pxNetworkBuffer->pucEthernetBuffer[ ( size_t ) ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER ] ) ); + TCPHeader_t * pxTCPHeader = &( pxProtocolHeader->xTCPHeader ); + + pxTCPHeader->ucTCPOffset = 0x80; + pxNetworkBuffer->xDataLength = 0x50; + /* Input TCP option is tcpTCP_OPT_WSOPT, length 3 bytes, and the value is 6. */ + uint8_t ucTCPOptions[] = { 0x03, 0x03, 0x06 }; + memcpy( ( void * ) pxTCPHeader->ucOptdata, ( void * ) &ucTCPOptions, sizeof( ucTCPOptions ) ); + + result = prvSingleStepTCPHeaderOptions( + pxTCPHeader->ucOptdata, + 3, + pxSocket, + pdTRUE ); + + TEST_ASSERT_EQUAL( 3, result ); + TEST_ASSERT_EQUAL( 6, pxSocket->u.xTCP.ucPeerWinScaleFactor ); +} + static uint32_t ulCalled = 0; static void xLocalFunctionPointer( Socket_t xSocket, size_t xLength ) diff --git a/test/unit-test/FreeRTOS_TCP_WIN/FreeRTOS_TCP_WIN_utest.c b/test/unit-test/FreeRTOS_TCP_WIN/FreeRTOS_TCP_WIN_utest.c index 365f450201..b6e8aa23ad 100644 --- a/test/unit-test/FreeRTOS_TCP_WIN/FreeRTOS_TCP_WIN_utest.c +++ b/test/unit-test/FreeRTOS_TCP_WIN/FreeRTOS_TCP_WIN_utest.c @@ -49,6 +49,10 @@ #include "mock_FreeRTOS_IP.h" #include "mock_task.h" +#define winSRTT_INCREMENT_NEW 2 /**< New increment for the smoothed RTT. */ +#define winSRTT_INCREMENT_CURRENT 6 /**< Current increment for the smoothed RTT. */ +#define winSRTT_DECREMENT_NEW 1 /**< New decrement for the smoothed RTT. */ +#define winSRTT_DECREMENT_CURRENT 7 /**< Current decrement for the smoothed RTT. */ static void initializeList( List_t * const pxList ); @@ -2477,6 +2481,9 @@ void test_ulTCPWindowTxSack( void ) /* --->ulTimerGetAge */ xTaskGetTickCount_ExpectAndReturn( 23 ); /* -->prvTCPWindowTxCheckAck_CalcSRTT */ + FreeRTOS_multiply_int32_ExpectAndReturn( 23, winSRTT_DECREMENT_NEW, 23 * winSRTT_DECREMENT_NEW ); + FreeRTOS_multiply_int32_ExpectAndReturn( xWindow.lSRTT, winSRTT_DECREMENT_CURRENT, xWindow.lSRTT * winSRTT_DECREMENT_CURRENT ); + FreeRTOS_add_int32_ExpectAndReturn( xWindow.lSRTT * winSRTT_DECREMENT_CURRENT, 23 * winSRTT_DECREMENT_NEW, xWindow.lSRTT * winSRTT_DECREMENT_CURRENT + 23 * winSRTT_DECREMENT_NEW ); /* ->prvTCPWindowTxCheckAck */ uxListRemove_ExpectAnyArgsAndReturn( pdTRUE ); /* ulTCPWindowTxSack */ @@ -2521,6 +2528,10 @@ void test_ulTCPWindowTxSack_prvTCPWindowFastRetransmit_1( void ) /* -->prvTCPWindowTxCheckAck_CalcSRTT */ /* --->ulTimerGetAge */ xTaskGetTickCount_ExpectAndReturn( 69 ); + FreeRTOS_multiply_int32_ExpectAndReturn( 69, winSRTT_INCREMENT_NEW, 69 * winSRTT_INCREMENT_NEW ); + FreeRTOS_multiply_int32_ExpectAndReturn( xWindow.lSRTT, winSRTT_INCREMENT_CURRENT, xWindow.lSRTT * winSRTT_INCREMENT_CURRENT ); + FreeRTOS_add_int32_ExpectAndReturn( xWindow.lSRTT * winSRTT_INCREMENT_CURRENT, 69 * winSRTT_INCREMENT_NEW, xWindow.lSRTT * winSRTT_INCREMENT_CURRENT + 69 * winSRTT_INCREMENT_NEW ); + /* <--prvTCPWindowTxCheckAck_CalcSRTT */ /* <-prvTCPWindowTxCheckAck */ /* ulTCPWindowTxSack */ @@ -2701,3 +2712,54 @@ void test_ulTCPWindowTxSack_prvTCPWindowFastRetransmit_4_LoggingLTZero( void ) xTCPWindowLoggingLevel = xBackup; } + + +void test_ulTCPWindowTxSack_prvTCPWindowFastRetransmit_5_ulTimerGetAgeReturnNegative( void ) +{ + uint32_t ulAckCount; + TCPWindow_t xWindow; + uint32_t ulFirst = 33; + uint32_t ulLast = 63; + TCPSegment_t mockSegment; + ListItem_t mockListItem; + + initializeListItem( &mockListItem ); + + xWindow.tx.ulCurrentSequenceNumber = 32; + xWindow.lSRTT = ipconfigTCP_SRTT_MINIMUM_VALUE_MS + 30; + mockSegment.u.bits.bAcked = pdFALSE_UNSIGNED; + mockSegment.lDataLength = 30; + + mockSegment.u.bits.ucTransmitCount = 1U; + mockSegment.ulSequenceNumber = 33; + mockListItem.pxContainer = &xWindow.xPriorityQueue; + mockSegment.xQueueItem = mockListItem; + mockSegment.xQueueItem.pxContainer = NULL; + mockSegment.u.bits.ucDupAckCount = 1U; + + /* ->prvTCPWindowTxCheckAck */ + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) &mockListItem ); + listGET_LIST_ITEM_OWNER_ExpectAnyArgsAndReturn( &mockSegment ); + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) &xWindow.xTxSegments.xListEnd ); + /* -->prvTCPWindowTxCheckAck_CalcSRTT */ + /* --->ulTimerGetAge */ + xTaskGetTickCount_ExpectAndReturn( 0xFFFFFFFF ); /* prvTCPWindowTxCheckAck_CalcSRTT replaces negative value with ipINT32_MAX_VALUE. */ + FreeRTOS_multiply_int32_ExpectAndReturn( ipINT32_MAX_VALUE, winSRTT_INCREMENT_NEW, ipINT32_MAX_VALUE ); + FreeRTOS_multiply_int32_ExpectAndReturn( xWindow.lSRTT, winSRTT_INCREMENT_CURRENT, xWindow.lSRTT * winSRTT_INCREMENT_CURRENT ); + FreeRTOS_add_int32_ExpectAndReturn( xWindow.lSRTT * winSRTT_INCREMENT_CURRENT, ipINT32_MAX_VALUE, ipINT32_MAX_VALUE ); + + /* <--prvTCPWindowTxCheckAck_CalcSRTT */ + /* <-prvTCPWindowTxCheckAck */ + /* ulTCPWindowTxSack */ + /* ->prvTCPWindowFastRetransmit */ + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) &mockListItem ); + listGET_LIST_ITEM_OWNER_ExpectAnyArgsAndReturn( &mockSegment ); + /* exit the loop */ + listGET_NEXT_ExpectAnyArgsAndReturn( ( ListItem_t * ) &xWindow.xWaitQueue.xListEnd ); + + ulAckCount = ulTCPWindowTxSack( &xWindow, + ulFirst, + ulLast ); + TEST_ASSERT_EQUAL( 0, ulAckCount ); + TEST_ASSERT_EQUAL( 268435455, xWindow.lSRTT ); /* Expected result is: ( 0x7FFFFFFF / 8 ). */ +}