Fix CBMC proof for DHCP

source/FreeRTOS_DHCP.c

@@ -287,7 +287,7 @@
                     /* PAss the address of a pointer pucUDPPayload, because zero-copy is used. */
                     lBytes = FreeRTOS_recvfrom( xDHCPv4Socket, &( pucUDPPayload ), 0, FREERTOS_ZERO_COPY, NULL, NULL );
 
-                    if( lBytes > 0 )
+                    if( ( lBytes > 0 ) && ( pucUDPPayload != NULL ) )
                     {
                         /* Remove it now, destination not found. */
                         FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
@@ -1317,8 +1317,10 @@
                     }
                 }
             }
-
-            FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+            if( pucUDPPayload != NULL )
+            {
+                FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+            }
         } /* if( lBytes > 0 ) */
 
         return xReturn;
@@ -1348,7 +1350,11 @@
 
         #if ( ipconfigDHCP_REGISTER_HOSTNAME == 1 )
             const char * pucHostName = pcApplicationHostnameHook();
-            size_t uxNameLength = strlen( pucHostName );
+            size_t uxNameLength = 0;
+            if( pucHostName != NULL )
+            {
+                uxNameLength = strlen( pucHostName );
+            }
             uint8_t * pucPtr;
 
 /* memcpy() helper variables for MISRA Rule 21.15 compliance*/
@@ -1423,10 +1429,13 @@
                      * compliant with MISRA Rule 21.15.  These should be
                      * optimized away.
                      */
-                    pvCopySource = pucHostName;
-                    pvCopyDest = &pucPtr[ 2U ];
+                    if( pucHostName != NULL )
+                    {
+                        pvCopySource = pucHostName;
+                        pvCopyDest = &pucPtr[ 2U ];
 
-                    ( void ) memcpy( pvCopyDest, pvCopySource, uxNameLength );
+                        ( void ) memcpy( pvCopyDest, pvCopySource, uxNameLength );
+                    }
                     pucPtr[ 2U + uxNameLength ] = ( uint8_t ) dhcpOPTION_END_BYTE;
                     *pxOptionsArraySize += ( size_t ) ( 2U + uxNameLength );
                 }
@@ -1479,7 +1488,7 @@
                                                         &( uxOptionsLength ),
                                                         pxEndPoint );
 
-        if( pucUDPPayloadBuffer != NULL )
+        if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) )
         {
             /* Copy in the IP address being requested. */
 
@@ -1506,7 +1515,10 @@
             {
                 /* The packet was not successfully queued for sending and must be
                  * returned to the stack. */
-                FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer );
+                if( pucUDPPayloadBuffer != NULL )
+                {
+                    FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer );
+                }
             }
             else
             {
@@ -1548,7 +1560,7 @@
                                                         &( uxOptionsLength ),
                                                         pxEndPoint );
 
-        if( pucUDPPayloadBuffer != NULL )
+        if( ( xDHCPv4Socket != FREERTOS_INVALID_SOCKET ) && ( xDHCPv4Socket != NULL ) && ( pucUDPPayloadBuffer != NULL ) )
         {
             const void * pvCopySource;
             void * pvCopyDest;
@@ -1588,7 +1600,10 @@
             {
                 /* The packet was not successfully queued for sending and must be
                  * returned to the stack. */
-                FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer );
+                if( pucUDPPayloadBuffer != NULL ) 
+                {
+                    FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayloadBuffer );
+                }
             }
             else
             {

test/cbmc/patches/FreeRTOSIPConfig.h

@@ -135,7 +135,9 @@ extern uint32_t ulRand();
  * reason.  The static configuration used is that passed into the stack by the
  * FreeRTOS_IPInit() function call. */
 #define ipconfigUSE_DHCP                         1
+
 #define ipconfigDHCP_REGISTER_HOSTNAME           1
+
 #define ipconfigDHCP_USES_UNICAST                1
 
 /* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must

test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c

@@ -42,40 +42,122 @@
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_ARP.h"
 
+#include "NetworkBufferManagement.h"
+
+#include "cbmc.h"
+
 /* Static members defined in FreeRTOS_DHCP.c */
 extern DHCPData_t xDHCPData;
-extern Socket_t xDHCPSocket;
-void prvCreateDHCPSocket();
+extern Socket_t xDHCPv4Socket;
+void prvCreateDHCPSocket( NetworkEndPoint_t * pxEndPoint );
 
 /* Static member defined in freertos_api.c */
 #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND
     extern uint32_t GetNetworkBuffer_failure_count;
 #endif
 
+
+
+
 /****************************************************************
 * The signature of the function under test.
 ****************************************************************/
 
-void vDHCPProcess( BaseType_t xReset,
-                   eDHCPState_t eExpectedState );
+void __CPROVER_file_local_FreeRTOS_DHCP_c_vDHCPProcessEndPoint( BaseType_t xReset,
+                            BaseType_t xDoCheck,
+                            NetworkEndPoint_t * pxEndPoint );
 
 /****************************************************************
 * Abstract prvProcessDHCPReplies proved memory safe in ProcessDHCPReplies.
 ****************************************************************/
 
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint )
 {
     return nondet_BaseType();
 }
 
+BaseType_t xSocketValid( const ConstSocket_t xSocket )
+{
+    /* This proof assumes that the socket will be valid to make the proof run
+    without causing asserts in the DHCP source [configASSERT( xSocketValid( xDHCPv4Socket ) == pdTRUE );] */
+    return pdTRUE;
+}
+
+BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket,
+                        struct freertos_sockaddr * pxBindAddress,
+                        size_t uxAddressLength,
+                        BaseType_t xInternal )
+{
+    /* Return value is set to zero assuming socket bind will succeed. If it doesnt, it
+    will hit an assert in the function.  */
+    BaseType_t xRet = 0;
+    __CPROVER_assert( pxSocket != NULL,
+                    "FreeRTOS precondition: pxSocket != NULL" );
+    __CPROVER_assert( pxBindAddress != NULL,
+                      "FreeRTOS precondition: pxBindAddress != NULL" );
+
+    return xRet;
+}
+
+
+/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
+/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
+
+    __CPROVER_assume( pxNetworkBuffer != NULL );
+    __CPROVER_assume( xRequestedSizeBytes > (dhcpFIRST_OPTION_BYTE_OFFSET + sizeof( MACAddress_t ) + ipIP_TYPE_OFFSET) );
+
+    pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ( ipIP_TYPE_OFFSET) )) + ipIP_TYPE_OFFSET;
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+
+    pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
+    return pxNetworkBuffer;
+}
+
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+
+    /* Free buffer after adjusting offsets. */
+    free( ( ( ( uint8_t * ) pvBuffer ) - ( ipUDP_PAYLOAD_OFFSET_IPv4 + ipIP_TYPE_OFFSET ) ) );
+}
+
 /****************************************************************
 * The proof of vDHCPProcess
 ****************************************************************/
 
 void harness()
 {
     BaseType_t xReset;
-    eDHCPState_t eExpectedState;
+    BaseType_t xDoCheck;
+
+    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 * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+    pxNetworkEndPoint_Temp->pxNext = NULL;
 
     /****************************************************************
     * Initialize the counter used to bound the number of times
@@ -93,12 +175,15 @@ void harness()
     * xReset==True resets the state to eWaitingSendFirstDiscover.
     ****************************************************************/
 
-    if( !( ( xDHCPData.eDHCPState == eInitialWait ) ||
+    if( !( ( pxNetworkEndPoint_Temp->xDHCPData.eDHCPState == eInitialWait ) ||
            ( xReset != pdFALSE ) ) )
     {
-        prvCreateDHCPSocket();
-        __CPROVER_assume( xDHCPSocket != NULL );
+        prvCreateDHCPSocket( pxNetworkEndPoint_Temp );
+
     }
 
-    vDHCPProcess( xReset, eExpectedState );
+    xDHCPv4Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP );
+
+    __CPROVER_file_local_FreeRTOS_DHCP_c_vDHCPProcessEndPoint( xReset, xDoCheck, pxNetworkEndPoint_Temp );
+
 }

test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json

@@ -31,12 +31,21 @@
 
   # Minimal buffer size for maximum coverage, see harness for details.
   "BUFFER_SIZE": 299,
+  "ENDPOINT_DNS_ADDRESS_COUNT": 5,
 
   # The number of times GetNetworkBufferWithDescriptor can be allowed to fail
   # (plus 1).
   "FAILURE_BOUND": 2,
 
-  "CBMCFLAGS": "--unwind 4 --unwindset strlen.0:11,memcmp.0:7,prvProcessDHCPReplies.0:8,prvCreatePartDHCPMessage.0:{FAILURE_BOUND} --nondet-static --flush",
+  "CBMCFLAGS": [
+    "--unwind 4",
+    "--unwindset strlen.0:11,memcmp.0:7",
+    "--nondet-static --flush"
+  ],
+  "OPT":
+  [
+    "--export-file-local-symbols"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
@@ -46,10 +55,10 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
-
   "DEF":
   [
     "BUFFER_SIZE={BUFFER_SIZE}",
+    "ipconfigDHCP_REGISTER_HOSTNAME=1",
     "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL=1",
     "CBMC_GETNETWORKBUFFER_FAILURE_BOUND={FAILURE_BOUND}"
   ]

test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json

@@ -24,6 +24,7 @@
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
   ],
 

test/cbmc/proofs/ProcessDHCPReplies/Makefile.json

@@ -10,6 +10,7 @@
 # Buffer header: sizeof(DHCPMessage_t) = 241
 # Buffer header: sizeof(DHCPMessage_IPv4_t) = 240
   "BUFFER_HEADER": 240,
+  "ENDPOINT_DNS_ADDRESS_COUNT": 5,
 
 ################################################################
 # Buffer size
@@ -20,15 +21,21 @@
 ################################################################
 # Buffer payload
   "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 1",
+  "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
 
 ################################################################
 
   "CBMCFLAGS": [
       # "--nondet-static",
       "--unwind 1",
-      "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+      "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+      "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+      "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+  ],
+  "OPT":
+  [
+    "--export-file-local-symbols"
   ],
-
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
@@ -43,6 +50,7 @@
   "DEF":
   [
     "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
-    "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"
+    "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}",
+    "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
   ]
 }

test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c

@@ -19,7 +19,8 @@
 * Signature of function under test
 ****************************************************************/
 
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint );
 
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
@@ -33,5 +34,9 @@ void harness()
 
     BaseType_t xExpectedMessageType;
 
-    prvProcessDHCPReplies( xExpectedMessageType );
+    NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+    pxNetworkEndPoint_Temp->pxNext = NULL;
+
+    __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp );
 }

test/cbmc/stubs/freertos_api.c

@@ -43,7 +43,7 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     }
     else
     {
-        void * ptr = malloc( sizeof( Socket_t ) );
+        void * ptr = malloc( sizeof( struct xSOCKET ) );
         __CPROVER_assume( ptr != NULL );
         return ptr;
     }