Add CBMC proof for prvProcessEthernetPacket (#199)

* Add proof

* Remove and Rename files

* Modify the makefile

* Update Makefile.json

* Add _static to FreeRTOS_IP.c

* Update prvProcessEthernetPacket_harness.c

* Update the proof and add list to stubs

* add assertions

* Update the proof

* cleanup

* Update

* Update after @yanjos-dev's comment

* Remove unnecessary assumption

3 files changed, 97 insertions, 0 deletions

diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/Makefile.json
new file mode 100644
index 000000000..7c7af9985
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/Makefile.json
@@ -0,0 +1,32 @@
+{
+  "ENTRY": "prvProcessEthernetPacket",
+  "CBMCFLAGS":
+  [
+    "--unwind 1",
+    "--unwindset prvTCPSendRepeated.0:13",
+    "--nondet-static",
+    "--flush"
+  ],
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto"
+  ],
+  "INSTFLAGS":
+  [
+  ],
+  "OPT":
+  [
+    "--export-file-local-symbols"
+  ],
+  "DEF":
+  [
+    "FREERTOS_TCP_ENABLE_VERIFICATION"
+  ],
+  "INC":
+  [
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility",
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs"
+  ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c
new file mode 100644
index 000000000..c70bfaa94
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c
@@ -0,0 +1,63 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "queue.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_Sockets.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_DHCP.h"
+#include "NetworkInterface.h"
+#include "NetworkBufferManagement.h"
+#include "FreeRTOS_ARP.h"
+
+#include "memory_assignments.c"
+#include "freertos_api.c"
+
+/****************************************************************
+ * Signature of function under test
+ ****************************************************************/
+void __CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( NetworkBufferDescriptor_t * const pxNetworkBuffer );
+
+
+/* This function has been proved to be memory safe in another proof (in ARP/ARPRefreshCacheEntry). Hence we assume it to be correct here. */
+void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress )
+{
+	/* pxMACAddress can be NULL or non-NULL. No need to assert. */
+}
+
+/* This function has been proved to be memory safe in another proof (in ARP/ARPProcessPacket). Hence we assume it to be correct here. */
+eFrameProcessingResult_t eARPProcessPacket( ARPPacket_t * const pxARPFrame )
+{
+	__CPROVER_assert( pxARPFrame != NULL, "pxARPFrame cannot be NULL" );
+
+	eFrameProcessingResult_t eReturn;
+	return eReturn;
+}
+
+/* This function has been proved to be memory safe in another proof (in parsing/ProcessIPPacket). Hence we assume it to be correct here. */
+eFrameProcessingResult_t  __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( IPPacket_t * pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+	__CPROVER_assert( pxIPPacket != NULL, "pxIPPacket cannot be NULL" );
+	__CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
+
+	eFrameProcessingResult_t result;
+	return result;
+}
+
+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 );
+
+	__CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( pxNetworkBuffer );
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
index 6bcb9319a..9866eff26 100644
--- a/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 #define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length)
 
 /* Implementation of safe malloc which returns NULL if the requested size is 0.