[IPv6] Add CBMC test for xCheckLoopback and xCheckRequiresARPResolution.

.github/lexicon.txt

@@ -1931,6 +1931,7 @@ xiscallingfromiptask
 xisforrx
 xisglobal
 xisinputstream
+xisipinarpcache
 xiswaitingarpresolution
 xitemvalue
 xlastacttime

source/FreeRTOS_ARP.c

@@ -1458,44 +1458,53 @@ void FreeRTOS_ClearARP( const struct xNetworkEndPoint * pxEndPoint )
  NetworkBufferDescriptor_t * pxUseDescriptor = pxDescriptor;
 
  /* 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 IPPacket_t * pxIPPacket = ( ( IPPacket_t * ) pxUseDescriptor->pucEthernetBuffer );
+ const IPPacket_t * pxIPPacket;
 
- if( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE )
+ if( ( pxUseDescriptor == NULL ) || ( pxUseDescriptor->xDataLength < sizeof( IPPacket_t ) ) )
  {
- NetworkEndPoint_t * pxEndPoint;
-
- pxEndPoint = FreeRTOS_FindEndPointOnMAC( &( pxIPPacket->xEthernetHeader.xDestinationAddress ), NULL );
+ /* The packet is too small to parse. */
+ }
+ else
+ {
+ pxIPPacket = ( ( IPPacket_t * ) pxUseDescriptor->pucEthernetBuffer );
 
- if( ( pxEndPoint != NULL ) &&
- ( memcmp( pxIPPacket->xEthernetHeader.xDestinationAddress.ucBytes, pxEndPoint->xMACAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) )
+ if( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE )
  {
- xResult = pdTRUE;
+ NetworkEndPoint_t * pxEndPoint;
 
- if( bReleaseAfterSend == pdFALSE )
- {
- /* Driver is not allowed to transfer the ownership
- * of descriptor, so make a copy of it */
- pxUseDescriptor =
- pxDuplicateNetworkBufferWithDescriptor( pxDescriptor, pxDescriptor->xDataLength );
- }
+ pxEndPoint = FreeRTOS_FindEndPointOnMAC( &( pxIPPacket->xEthernetHeader.xDestinationAddress ), NULL );
 
- if( pxUseDescriptor != NULL )
+ if( ( pxEndPoint != NULL ) &&
+ ( memcmp( pxIPPacket->xEthernetHeader.xDestinationAddress.ucBytes, pxEndPoint->xMACAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) )
  {
- IPStackEvent_t xRxEvent;
-
- pxUseDescriptor->pxInterface = pxEndPoint->pxNetworkInterface;
- pxUseDescriptor->pxEndPoint = pxEndPoint;
+ xResult = pdTRUE;
 
- xRxEvent.eEventType = eNetworkRxEvent;
- xRxEvent.pvData = pxUseDescriptor;
+ if( bReleaseAfterSend == pdFALSE )
+ {
+ /* Driver is not allowed to transfer the ownership
+ * of descriptor, so make a copy of it */
+ pxUseDescriptor =
+ pxDuplicateNetworkBufferWithDescriptor( pxDescriptor, pxDescriptor->xDataLength );
+ }
 
- if( xSendEventStructToIPTask( &xRxEvent, 0U ) != pdTRUE )
+ if( pxUseDescriptor != NULL )
  {
- vReleaseNetworkBufferAndDescriptor( pxUseDescriptor );
- iptraceETHERNET_RX_EVENT_LOST();
- FreeRTOS_printf( ( "prvEMACRxPoll: Can not queue return packet!\n" ) );
+ IPStackEvent_t xRxEvent;
+
+ pxUseDescriptor->pxInterface = pxEndPoint->pxNetworkInterface;
+ pxUseDescriptor->pxEndPoint = pxEndPoint;
+
+ xRxEvent.eEventType = eNetworkRxEvent;
+ xRxEvent.pvData = pxUseDescriptor;
+
+ if( xSendEventStructToIPTask( &xRxEvent, 0U ) != pdTRUE )
+ {
+ vReleaseNetworkBufferAndDescriptor( pxUseDescriptor );
+ iptraceETHERNET_RX_EVENT_LOST();
+ FreeRTOS_printf( ( "prvEMACRxPoll: Can not queue return packet!\n" ) );
+ }
  }
  }
  }

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

@@ -0,0 +1,17 @@
+{
+ "ENTRY": "xCheckLoopback",
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--unwindset memcmp.0:10"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
+ ],
+ "DEF":
+ [
+ ]
+}

test/cbmc/proofs/ARP/xCheckLoopback/xCheckLoopback_harness.c

@@ -0,0 +1,61 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_ARP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Abstraction of FreeRTOS_FindEndPointOnMAC. */
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnMAC( const MACAddress_t * pxMACAddress,
+ const NetworkInterface_t * pxInterface )
+{
+ NetworkEndPoint_t * pxReturnEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+
+ return pxReturnEndPoint;
+}
+
+/* Abstraction of pxDuplicateNetworkBufferWithDescriptor. */
+NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
+ size_t uxNewLength )
+{
+ /* In this function, we can either return NULL or valid pointer as return value. */
+ NetworkBufferDescriptor_t * pxReturnNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+ if( pxReturnNetworkBuffer )
+ {
+ /* If the pointer is valid, we must have enough ethernet buffer for it with correct data length. */
+ pxReturnNetworkBuffer->pucEthernetBuffer = safeMalloc( uxNewLength );
+ __CPROVER_assume( pxReturnNetworkBuffer->pucEthernetBuffer != NULL );
+
+ pxReturnNetworkBuffer->xDataLength = uxNewLength;
+ }
+
+ return pxReturnNetworkBuffer;
+}
+
+void harness()
+{
+ size_t xBufferLength;
+ NetworkBufferDescriptor_t * pxNetworkBuffer;
+ BaseType_t bReleaseAfterSend;
+
+ __CPROVER_assume( ( xBufferLength >= 0 ) &&
+ ( xBufferLength < ipconfigNETWORK_MTU ) );
+
+ pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+ if( pxNetworkBuffer )
+ {
+ /* If buffer pointer is valid, allocate ethernet buffer and set data length for it. */
+ pxNetworkBuffer->xDataLength = xBufferLength;
+
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xBufferLength );
+ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+ }
+
+ ( void ) xCheckLoopback( pxNetworkBuffer, bReleaseAfterSend );
+}

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

@@ -0,0 +1,17 @@
+{
+ "ENTRY": "xCheckRequiresARPResolution",
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--unwindset memcmp.0:10"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
+ ],
+ "DEF":
+ [
+ ]
+}

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

@@ -0,0 +1,117 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_ARP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Global variables. */
+BaseType_t xIsIPv6;
+
+/* Abstraction of xIsIPInARPCache. */
+BaseType_t xIsIPInARPCache( uint32_t ulAddressToLookup )
+{
+ BaseType_t xReturn;
+
+ __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+ return xReturn;
+}
+
+/* Function uxIPHeaderSizePacket is proven to be correct separately.*/
+size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+ size_t xReturn = ipSIZE_OF_IPv4_HEADER;
+
+ __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer, sizeof( NetworkBufferDescriptor_t ) ), "pxNetworkBuffer must be readable" );
+ __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "pxNetworkBuffer;s buffer must be readable" );
+
+ if( xIsIPv6 )
+ {
+ xReturn = ipSIZE_OF_IPv6_HEADER;
+ }
+
+ return xReturn;
+}
+
+/* Abstraction of FreeRTOS_OutputARPRequest. */
+void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
+{
+}
+
+/* Abstraction of xIPv6_GetIPType. */
+IPv6_Type_t xIPv6_GetIPType( const IPv6_Address_t * pxAddress )
+{
+ IPv6_Type_t eType;
+
+ __CPROVER_assert( __CPROVER_r_ok( pxAddress, sizeof( IPv6_Address_t ) ), "pxAddress must be readable" );
+
+ return eType;
+}
+
+/* Abstraction of eNDGetCacheEntry. */
+eARPLookupResult_t eNDGetCacheEntry( IPv6_Address_t * pxIPAddress,
+ MACAddress_t * const pxMACAddress,
+ struct xNetworkEndPoint ** ppxEndPoint )
+{
+ eARPLookupResult_t xReturn;
+
+ __CPROVER_assert( __CPROVER_r_ok( pxIPAddress, sizeof( IPv6_Address_t ) ), "pxIPAddress must be readable" );
+ __CPROVER_assert( __CPROVER_w_ok( pxMACAddress, sizeof( MACAddress_t ) ), "pxMACAddress must be writeable" );
+
+ return xReturn;
+}
+
+/* Abstraction of pxGetNetworkBufferWithDescriptor. */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+ TickType_t xBlockTimeTicks )
+{
+ NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+ return pxNetworkBuffer;
+}
+
+/* Abstraction of vNDSendNeighbourSolicitation. */
+void vNDSendNeighbourSolicitation( NetworkBufferDescriptor_t * pxNetworkBuffer,
+ const IPv6_Address_t * pxIPAddress )
+{
+ __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer, sizeof( NetworkBufferDescriptor_t ) ), "pxNetworkBuffer must be readable" );
+ __CPROVER_assert( __CPROVER_r_ok( pxIPAddress, sizeof( IPv6_Address_t ) ), "pxIPAddress must be readable" );
+}
+
+void harness()
+{
+ size_t xBufferLength;
+ NetworkBufferDescriptor_t * pxNetworkBuffer;
+ IPPacket_t * pxIPPacket;
+
+ /* IPv4/IPv6 header size are different. To make sure buffer size is enough,
+ * determine the test case is for IPv4 or IPv6 at the beginning. */
+ xIsIPv6 = nondet_bool();
+
+ if( xIsIPv6 )
+ {
+ __CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_IPv6_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );
+ }
+ else
+ {
+ __CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );
+ }
+
+ pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+ __CPROVER_assume( pxNetworkBuffer != NULL );
+
+ pxNetworkBuffer->xDataLength = xBufferLength;
+
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xBufferLength );
+ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+
+ pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+ __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
+
+ ( void ) xCheckRequiresARPResolution( pxNetworkBuffer );
+}

test/unit-test/FreeRTOS_ARP/FreeRTOS_ARP_utest.c

@@ -66,6 +66,37 @@ static void vResetARPClashCounter( void )
  xTaskCheckForTimeOut_StopIgnore();
 }
 
+void test_xCheckLoopback_NullNetworkBuffer( void )
+{
+ BaseType_t xResult;
+
+ /* bReleaseAfterSend parameter doesn't matter here. */
+ xResult = xCheckLoopback( NULL, pdFALSE );
+ TEST_ASSERT_EQUAL( pdFALSE, xResult );
+ /* =================================================== */
+}
+
+void test_xCheckLoopback_DataLengthTooSmall( void )
+{
+ NetworkBufferDescriptor_t xNetworkBuffer = { 0 };
+ NetworkBufferDescriptor_t * const pxNetworkBuffer = &xNetworkBuffer;
+ uint8_t ucBuffer[ sizeof( IPPacket_t ) + ipBUFFER_PADDING ];
+ BaseType_t xResult;
+
+ pxNetworkBuffer->pucEthernetBuffer = ucBuffer;
+ pxNetworkBuffer->xDataLength = sizeof( IPPacket_t ) - 1;
+
+ IPPacket_t * pxIPPacket = ( IPPacket_t * ) ( pxNetworkBuffer->pucEthernetBuffer );
+
+ /* =================================================== */
+ /* Let the frame-type be anything else than IPv4. */
+ pxIPPacket->xEthernetHeader.usFrameType = ipIPv4_FRAME_TYPE;
+ /* bReleaseAfterSend parameter doesn't matter here. */
+ xResult = xCheckLoopback( pxNetworkBuffer, pdFALSE );
+ TEST_ASSERT_EQUAL( pdFALSE, xResult );
+ /* =================================================== */
+}
+
 void test_xCheckLoopback_IncorrectFrameType( void )
 {
  NetworkBufferDescriptor_t xNetworkBuffer = { 0 };