[Draft] CBMC: replace any missing functions by assert-false

source/FreeRTOS_DNS_Cache.c

@@ -448,10 +448,9 @@
         /* Add or update the item. */
         if( strlen( pcName ) < ( size_t ) ipconfigDNS_CACHE_NAME_LENGTH )
         {
-            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, ipconfigDNS_CACHE_NAME_LENGTH );
+            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, strlen( pcName ) );
             ( void ) memcpy( &( xDNSCache[ uxFreeEntry ].xAddresses[ 0 ] ), pxIP, sizeof( *pxIP ) );
 
-
             xDNSCache[ uxFreeEntry ].ulTTL = ulTTL;
             xDNSCache[ uxFreeEntry ].ulTimeWhenAddedInSeconds = ulCurrentTimeSeconds;
             #if ( ipconfigDNS_CACHE_ADDRESSES_PER_ENTRY > 1 )

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

@@ -33,6 +33,12 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     return 0;
 }
 
+
+void FreeRTOS_OutputAdvertiseIPv6( NetworkEndPoint_t * pxEndPoint )
+{
+    __CPROVER_assert( pxEndPoint != NULL, "The Endpoint cannot be NULL." );
+}
+
 void harness()
 {
     /*

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

@@ -15,6 +15,9 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
   ],
   "DEF":

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

@@ -14,6 +14,8 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   "DEF":

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

@@ -1,5 +1,3 @@
-#include "cbmc.h"
-
 /* FreeRTOS includes. */
 #include "FreeRTOS.h"
 #include "queue.h"
@@ -10,8 +8,37 @@
 #include "FreeRTOS_ARP.h"
 #include "FreeRTOS_Routing.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
+
 /* This pointer is maintained by the IP-task. Defined in FreeRTOS_IP.c */
 extern NetworkBufferDescriptor_t * pxARPWaitingNetworkBuffer;
+NetworkEndPoint_t * pxNetworkEndPoint_Temp;
+
+/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the
+ * correctness of the proof */
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask_IPv6( const IPv6_Address_t * pxIPv6Address )
+{
+    __CPROVER_assert( pxIPv6Address != NULL, "Precondition: pxIPv6Address != NULL" );
+
+    /* Assume at least one end-point is available */
+    return pxNetworkEndPoint_Temp;
+}
+
+/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the
+ * correctness of the proof */
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress,
+                                                    uint32_t ulWhere )
+{
+    /* Assume at least one end-point is available */
+    return pxNetworkEndPoint_Temp;
+}
+
+/* Get rid of configASSERT in FreeRTOS_TCP_IP.c */
+BaseType_t xIsCallingFromIPTask( void )
+{
+    return pdTRUE;
+}
 
 /* This is an output function and need not be tested with this proof. */
 void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
@@ -36,9 +63,19 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress,
 
 void harness()
 {
-    NetworkBufferDescriptor_t xLocalBuffer;
+    NetworkBufferDescriptor_t * pxLocalBuffer;
+    NetworkBufferDescriptor_t * pxNetworkBuffer2;
+    TickType_t xBlockTimeTicks;
     uint16_t usEthernetBufferSize;
 
+    /*
+     * 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;
+
+
     /* Non deterministically determine whether the pxARPWaitingNetworkBuffer will
      * point to some valid data or will it be NULL. */
     if( nondet_bool() )
@@ -47,48 +84,34 @@ void harness()
          * checked in the function as the pointer is stored by the IP-task itself
          * and therefore it will always be of the required size. */
         __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_t ) );
-
-        /* Add matching data length to the network buffer descriptor. */
-        __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize );
-
-        xLocalBuffer.pucEthernetBuffer = malloc( usEthernetBufferSize );
+        pxLocalBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, xBlockTimeTicks );
 
         /* Since this pointer is maintained by the IP-task, either the pointer
-         * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer
+         * pxARPWaitingNetworkBuffer will be NULL or pxLocalBuffer->pucEthernetBuffer
          * will be non-NULL. */
-        __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer->pucEthernetBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer->xDataLength == usEthernetBufferSize );
 
-        pxARPWaitingNetworkBuffer = &xLocalBuffer;
+        pxARPWaitingNetworkBuffer = pxLocalBuffer;
     }
     else
     {
         pxARPWaitingNetworkBuffer = NULL;
     }
 
-    /*
-     * 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 );
+    pxNetworkBuffer2 = pxGetNetworkBufferWithDescriptor( ucBUFFER_SIZE + sizeof( ARPPacket_t ), xBlockTimeTicks );
+    __CPROVER_assume( pxNetworkBuffer2 != NULL );
+    __CPROVER_assume( pxNetworkBuffer2->pucEthernetBuffer != NULL );
 
     /*
      * 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;
+    pxNetworkBuffer2->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkBuffer2->pxEndPoint != NULL );
+    pxNetworkBuffer2->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 );
+     * pxNetworkBuffer2->pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL );   */
+    eARPProcessPacket( pxNetworkBuffer2 );
 }

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

@@ -11,6 +11,9 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ]
 }

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

@@ -10,7 +10,9 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [

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

@@ -37,7 +37,9 @@
     "$(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)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"
   ],
   #That is the minimal required size for an ARPPacket_t plus offset in the buffer.
   "MINIMUM_PACKET_BYTES": 50,

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

@@ -35,6 +35,8 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
 
 ARPPacket_t xARPPacket;
 NetworkBufferDescriptor_t xNetworkBuffer;
@@ -56,22 +58,37 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
 {
     #ifdef CBMC_PROOF_ASSUMPTION_HOLDS
         #if ( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 )
-            xNetworkBuffer.pucEthernetBuffer = malloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES );
+            xNetworkBuffer.pucEthernetBuffer = safeMalloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES );
         #else
-            xNetworkBuffer.pucEthernetBuffer = malloc( xRequestedSizeBytes );
+            xNetworkBuffer.pucEthernetBuffer = safeMalloc( xRequestedSizeBytes );
         #endif
     #else
         uint32_t malloc_size;
         __CPROVER_assert( !__CPROVER_overflow_mult( 2, xRequestedSizeBytes ) );
         __CPROVER_assume( malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes );
-        xNetworkBuffer.pucEthernetBuffer = malloc( malloc_size );
+        xNetworkBuffer.pucEthernetBuffer = safeMalloc( malloc_size );
     #endif
     __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
 
     xNetworkBuffer.xDataLength = xRequestedSizeBytes;
     return &xNetworkBuffer;
 }
 
+/* STUB!
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should just free the allocated pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    if( pxNetworkBuffer->pucEthernetBuffer != NULL )
+    {
+        free( pxNetworkBuffer->pucEthernetBuffer );
+    }
+}
+
 BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                 BaseType_t xReleaseAfterSend )
@@ -81,6 +98,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
 
 void harness()
 {
@@ -92,16 +117,16 @@ void harness()
      * Assumes one endpoint and interface is present.
      */
 
-    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
 
     /* Interface init. */
-    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
 
     if( nondet_bool() )
     {
-        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
         __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
         pxNetworkEndPoints->pxNext->pxNext = NULL;
         pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;

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

@@ -14,7 +14,9 @@
     "$(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"
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [

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

@@ -75,6 +75,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     }
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
 
 void harness()
 {

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

@@ -14,7 +14,9 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_2.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto"
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto"
   ],
   "DEF":
   [

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

@@ -55,6 +55,15 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     }
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
+
 void harness()
 {
     BaseType_t xRes = xNetworkBuffersInitialise();

test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c

@@ -87,7 +87,7 @@ void harness()
     /* Preconditions */
 
     /* CBMC model of pointers limits the size of the buffer */
-    __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE );
+    __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU );
 
     /* Both preconditions are required to avoid integer overflow in the */
     /* pointer offset of the pointer pucPtr + uxIndex + 8 */

test/cbmc/proofs/CheckOptionsInner/Makefile.json

@@ -12,6 +12,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto",
@@ -21,6 +22,7 @@
   ],
   "DEF":
   [
-    "ipconfigUSE_TCP=1"
+    "ipconfigUSE_TCP=1",
+    "ipconfigNETWORK_MTU=586"
   ]
 }

test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c

@@ -81,7 +81,7 @@ void harness()
     ****************************************************************/
 
     /* CBMC model of pointers limits the size of the buffer */
-    __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE );
+    __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU );
 
     /* Preconditions */
     __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */

test/cbmc/proofs/CheckOptionsOuter/Makefile.json

@@ -12,6 +12,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto",
@@ -20,5 +21,6 @@
   ],
   "DEF":
   [
+    "ipconfigNETWORK_MTU=586"
   ]
 }