Fix CBMC proofs for socket (#719)

* fixed cbmc proof for vSocketBind

* 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 cbmc proof for vSocketWakeUpUser

* add check with  multiple endpoints

* NULL assume to assignment

* adding non determinitic number of end points

* adding commit review suggestions

* Uncrustify: triggered by comment.

---------

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

Author: 4 people

test/cbmc/patches/FreeRTOSConfig.h

@@ -127,7 +127,7 @@
  * is set to 2 so the formatting functions are included without the stdio.h being
  * included in tasks.c.  That is because this project defines its own sprintf()
  * functions. */
-#define configUSE_STATS_FORMATTING_FUNCTIONS    1
+#define configUSE_STATS_FORMATTING_FUNCTIONS    0
 
 /* Assert call defined for debug builds. */
 extern void vAssertCalled( const char * pcFile,

test/cbmc/proofs/Makefile.template

@@ -119,38 +119,36 @@ goto:
 # Ignore the return code for CBMC, so that we can still generate the
 # report if the proof failed. If the proof failed, we separately fail
 # the entire job using the check-cbmc-result rule.
-cbmc.txt: $(ENTRY).goto
-	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1
+cbmc.xml: $(ENTRY).goto
+	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 property.xml: $(ENTRY).goto
 	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 coverage.xml: $(ENTRY).goto
 	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
 
-cbmc: cbmc.txt
+cbmc: cbmc.xml
 
 property: property.xml
 
 coverage: coverage.xml
 
-report: cbmc.txt property.xml coverage.xml
+report: cbmc.xml property.xml coverage.xml
 	$(VIEWER) \
 	--goto $(ENTRY).goto \
 	--srcdir $(FREERTOS_PLUS_TCP) \
-	--blddir $(FREERTOS_PLUS_TCP) \
-	--htmldir html \
-	--srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \
-	--result cbmc.txt \
+	--reportdir report \
+	--result cbmc.xml \
 	--property property.xml \
-	--block coverage.xml
+	--coverage coverage.xml
 
-# This rule depends only on cbmc.txt and has no dependents, so it will
+# This rule depends only on cbmc.xml and has no dependents, so it will
 # not block the report from being generated if it fails. This rule is
 # intended to fail if and only if the CBMC safety check that emits
-# cbmc.txt yielded a proof failure.
-check-cbmc-result: cbmc.txt
-	grep -e "^VERIFICATION SUCCESSFUL" $^
+# cbmc.xml yielded a proof failure.
+check-cbmc-result: cbmc.xml
+	grep '<cprover-status>SUCCESS</cprover-status>' $^
 
 # ____________________________________________________________________
 # Rules
@@ -160,7 +158,7 @@ check-cbmc-result: cbmc.txt
 clean:
 	@RM@ $(OBJS) $(ENTRY).goto
 	@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
-	@RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-*
+	@RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-*
 	@RM@ *~ \#*
 	@RM@ queue_datastructure.h
 

test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json

@@ -5,11 +5,13 @@
   "ALLOW_TCP":"1",
   "CBMCFLAGS":
   [
-    "--unwind 1"
+    "--unwind 1",
+    "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3"
   ],
   "OBJS":
   [
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
     "$(ENTRY)_harness.goto"
   ],

test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c

@@ -49,6 +49,21 @@ BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber )
 
 void harness()
 {
+    /* Add few endpoints */
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
 
     __CPROVER_assume( pxSocket != NULL );

test/cbmc/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json

@@ -3,11 +3,13 @@
   "ALLOW_SEND_WITHOUT_BIND":"1",
   "CBMCFLAGS":
   [
-    "--unwind 1"
+    "--unwind 1",
+    "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3"
   ],
   "OBJS":
   [
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
     "$(ENTRY)_harness.goto"
   ],

test/cbmc/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c

@@ -47,6 +47,21 @@ BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber )
 
 void harness()
 {
+    /* Add few endpoints */
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
 
     __CPROVER_assume( pxSocket != NULL );

test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json

@@ -3,11 +3,13 @@
   "ALLOW_SEND_WITHOUT_BIND":"0",
   "CBMCFLAGS":
   [
-    "--unwind 1"
+    "--unwind 1",
+    "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3"
   ],
   "OBJS":
   [
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
     "$(ENTRY)_harness.goto"
   ],

test/cbmc/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c

@@ -47,6 +47,21 @@ BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber )
 
 void harness()
 {
+    /* Add few endpoints */
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
 
     __CPROVER_assume( pxSocket != NULL );

test/cbmc/proofs/Socket/vSocketWakeUpUser/vSocketWakeUpUser_harness.c

@@ -130,6 +130,11 @@ EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup,
     return uxReturnBits;
 }
 
+void SocketWakeupCallback_Stub( struct xSOCKET * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL,
+                      "The pxSocket cannot be NULL" );
+}
 
 void harness()
 {
@@ -138,7 +143,7 @@ void harness()
     __CPROVER_assume( pxSocket != NULL );
     __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
 
-    pxSocket->pxUserWakeCallback = safeMalloc( sizeof( SocketWakeupCallback_t ) );
+    pxSocket->pxUserWakeCallback = SocketWakeupCallback_Stub;
 
     pxSocket->pxSocketSet = safeMalloc( sizeof( struct xSOCKET_SET ) );
 

test/cbmc/proofs/utility/memory_assignments.c

@@ -20,6 +20,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
         pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
         pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
         pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+        pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     }
 
     return pxSocket;