Fix build and proof failures for CBMC ARP proofs

test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c

@@ -23,7 +23,45 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return pxNetworkBuffer;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
+    return 0;
+}
+
 void harness()
 {
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes two endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+
     vARPAgeCache();
 }

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

@@ -4,12 +4,15 @@
   [
       "--unwind 1",
       "--unwindset vARPAgeCache.0:7",
+      "--unwindset FreeRTOS_OutputARPRequest.0:3",
+      "--unwindset vARPAgeCache.1:3",
       "--nondet-static"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
   ],

test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c

@@ -26,6 +26,13 @@ void harness()
     xNetworkBuffer2.pucEthernetBuffer = xBuffer;
     xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
 
+    /*
+    This proof assumes one end point is present.
+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
+
     /* vARPGenerateRequestPacket asserts buffer has room for a packet */
     __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof( ARPPacket_t ) );
     vARPGenerateRequestPacket( &xNetworkBuffer2 );

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

@@ -13,5 +13,38 @@ void harness()
     uint32_t ulIPAddress;
     MACAddress_t xMACAddress;
 
-    eARPGetCacheEntry( &ulIPAddress, &xMACAddress );
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoint and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        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 );
 }

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

@@ -4,11 +4,16 @@
   [
       "--unwind 1",
       "--unwindset prvCacheLookup.0:7",
+      "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3",
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
+      "--unwindset eARPGetCacheEntry.0:3",
+      "--unwindset FreeRTOS_FindGateWay.0:3",
       "--nondet-static"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   "DEF":

test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c

@@ -7,10 +7,22 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
 
+extern ARPCacheRow_t xARPCache[ ipconfigARP_CACHE_ENTRIES ];
+
+static NetworkEndPoint_t xEndPoint_Temp;
+
 void harness()
 {
     MACAddress_t xMACAddress;
     uint32_t ulIPAddress;
 
-    eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress );
+    NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
+
+    if ( ppxInterface )
+    {
+        *ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+        __CPROVER_assume( *ppxInterface != NULL );
+    }
+
+    eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress, ppxInterface );
 }

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

@@ -2,8 +2,7 @@
   "ENTRY": "ARPGetCacheEntryByMac",
   "CBMCFLAGS":
   [
-      "--unwind 7",
-      "--nondet-static"
+      "--unwind 7"
   ],
   "OBJS":
   [

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

@@ -1,3 +1,5 @@
+#include "cbmc.h"
+
 /* FreeRTOS includes. */
 #include "FreeRTOS.h"
 #include "queue.h"
@@ -17,7 +19,6 @@ void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
 
 void harness()
 {
-    ARPPacket_t xARPFrame;
     NetworkBufferDescriptor_t xLocalBuffer;
     uint16_t usEthernetBufferSize;
 
@@ -47,5 +48,30 @@ void harness()
         pxARPWaitingNetworkBuffer = NULL;
     }
 
-    eARPProcessPacket( &xARPFrame );
+    /*
+     * The assumption made here is that the buffer pointed by pucEthernetBuffer
+     * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.
+     * This is not checked inside eARPProcessPacket.
+     */
+    uint8_t ucBUFFER_SIZE;
+
+    void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
+
+    __CPROVER_assume( xBuffer != NULL );
+
+    NetworkBufferDescriptor_t xNetworkBuffer2;
+
+    xNetworkBuffer2.pucEthernetBuffer = xBuffer;
+    xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof(ARPPacket_t);
+
+    /*
+    This proof assumes one end point is present.
+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
+
+    /* eARPProcessPacket will be called in the source code only after checking if
+    xNetworkBuffer2.pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL );   */
+    eARPProcessPacket( &xNetworkBuffer2 );
 }

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

@@ -4,6 +4,7 @@
   [
       "--unwind 1",
       "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17,xIsIPInARPCache.0:7",
+      "--unwindset prvFindCacheEntry.0:7", 
       "--nondet-static"
   ],
   "OBJS":

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

@@ -11,6 +11,35 @@ void harness()
     MACAddress_t xMACAddress;
     uint32_t ulIPAddress;
 
-    vARPRefreshCacheEntry( &xMACAddress, ulIPAddress );
-    vARPRefreshCacheEntry( NULL, ulIPAddress );
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
+
+    NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxEndPoint != NULL );
+
+    vARPRefreshCacheEntry( &xMACAddress, ulIPAddress, pxEndPoint );
+    vARPRefreshCacheEntry( NULL, ulIPAddress, pxEndPoint );
 }

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

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

test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c

@@ -8,5 +8,12 @@
 
 void harness()
 {
-    FreeRTOS_ClearARP();
+
+    NetworkEndPoint_t *pxEndPoint_Test = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    /*
+    Here the assumption that pxEndPoint_Test != NULL [__CPROVER_assume( pxEndPoint_Test != NULL );]
+    is not made as pxEndPoint_Test == NULL is a valid use case.
+    */
+
+    FreeRTOS_ClearARP(pxEndPoint_Test);
 }

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

@@ -2,7 +2,8 @@
   "ENTRY": "ClearARP",
   "CBMCFLAGS":
   [
-      "--unwind 1"
+      "--unwind 1",
+      "--unwindset FreeRTOS_ClearARP.0:7"
   ],
   "OBJS":
   [

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

@@ -36,6 +36,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   #That is the minimal required size for an ARPPacket_t plus offset in the buffer.

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

@@ -72,10 +72,49 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return &xNetworkBuffer;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
+
+}
+
 
 void harness()
 {
     uint32_t ulIPAddress;
 
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoint and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+
     FreeRTOS_OutputARPRequest( ulIPAddress );
 }

test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c

@@ -8,6 +8,8 @@
 #include "FreeRTOSIPConfig.h"
 #include "FreeRTOS_ARP.h"
 
+void FreeRTOS_PrintARPCache( void );
+
 void harness()
 {
     FreeRTOS_PrintARPCache();

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

@@ -12,6 +12,7 @@
   ],
   "DEF":
   [
-    "ipconfigARP_CACHE_ENTRIES=6"
+    "ipconfigARP_CACHE_ENTRIES=6",
+    "ipconfigHAS_PRINTF=1"
   ]
 }

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

@@ -11,6 +11,7 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_1.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto"