Fix CBMC proofs for IP (#725)

* Fixed CBMC proof for ProcessIPPacket

* Use CBMC XML output to enable VSCode debugger (#673)

Prior to this commit, CBMC would emit logging information in plain text
format, which does not contain information required for the CBMC VSCode
debugger. This commit makes CBMC use XML instead of plain text.

Co-authored-by: Mark Tuttle <[email protected]>

* Fix CBMX proof for prvProcessEthernetPacket

* adding more asserts

* updating as per review comments

---------

Co-authored-by: Kareem Khazem <[email protected]>
Co-authored-by: Mark Tuttle <[email protected]>

Author: 3 people

test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c

@@ -63,8 +63,9 @@ void harness()
 
     __CPROVER_assume( pxNetworkBuffer != NULL );
 
-    /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/
-    pxNetworkBuffer->pucEthernetBuffer = malloc( ipTOTAL_ETHERNET_FRAME_SIZE );
+    /* Points to ethernet buffer offset by ipIP_TYPE_OFFSET, this make sure the buffer allocation is similar
+    to the pxGetNetworkBufferWithDescriptor */
+    pxNetworkBuffer->pucEthernetBuffer = ( ( ( uint8_t * ) malloc( ipTOTAL_ETHERNET_FRAME_SIZE ) ) + ipIP_TYPE_OFFSET );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
     /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */

test/cbmc/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c

@@ -56,12 +56,33 @@ eFrameProcessingResult_t __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket(
     return result;
 }
 
+
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    BaseType_t xRet;
+    __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 xRet;
+}
+
 void harness()
 {
     NetworkBufferDescriptor_t * const pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ipTOTAL_ETHERNET_FRAME_SIZE, 0 );
-
     /* The network buffer cannot be NULL for this function call. If it is, it will hit an assert in the function. */
     __CPROVER_assume( pxNetworkBuffer != NULL );
 
+    /* Add an endpoint */
+    pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
+
+    /* Interface init. */
+    pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
+    pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
+
     __CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( pxNetworkBuffer );
 }