Fix DNSgetHostByName_cancel CBMC test

FreeRTOS · Jul 16, 2024 · e561de7 · e561de7
1 parent 274ea9e
commit e561de7
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 23 deletions.
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
@@ -8,6 +8,8 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
 
 /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
 
@@ -20,27 +22,37 @@ BaseType_t xDNSSetCallBack( const char * pcHostName,
                             TickType_t xIdentifier,
                             BaseType_t xIsIPv6 );
 
-void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
+/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */
+void vListInitialise( List_t * const pxList )
 {
-    if( xWantedSize == 0 )
-    {
-        return NULL;
-    }
+    __CPROVER_assert( pxList != NULL, "pxList cannot be NULL" );
 
-    uint8_t byte;
+    pxList->pxIndex = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->xListEnd.xItemValue = portMAX_DELAY;
 
-    return byte ? malloc( xWantedSize ) : NULL;
+    /* The list end next and previous pointers point to itself so we know
+     * when the list is empty. */
+    pxList->xListEnd.pxNext = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->xListEnd.pxPrevious = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->uxNumberOfItems = ( UBaseType_t ) 0U;
 }
 
-/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
-                                 TickType_t * const pxTicksToWait )
+/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */
+UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
 {
-}
+    List_t * const pxList = pxItemToRemove->pxContainer;
+    pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
+    pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
 
-/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskResumeAll( void )
-{
+    if( pxList->pxIndex == pxItemToRemove )
+    {
+        pxList->pxIndex = pxItemToRemove->pxPrevious;
+    }
+
+    pxItemToRemove->pxContainer = NULL;
+    ( pxList->uxNumberOfItems )--;
+
+    return pxList->uxNumberOfItems;
 }
 
 /* The function func mimics the callback function.*/
@@ -61,13 +73,11 @@ void harness()
     size_t len;
     BaseType_t xReturn;
 
-    __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
+    __CPROVER_assume( len > 0 && len <= MAX_HOSTNAME_LEN );
     char * pcHostName = safeMalloc( len );
-
-    if( len && pcHostName )
-    {
-        pcHostName[ len - 1 ] = NULL;
-    }
+    __CPROVER_assume( pcHostName != NULL );
+    __CPROVER_havoc_slice( pcHostName, len - 1 );
+    pcHostName[ len - 1 ] = NULL;
 
     xReturn = xDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier, xIsIPv6 ); /* Add an item to be able to check the cancel function if the list is non-empty. */
     FreeRTOS_gethostbyname_cancel( &pvSearchID );

diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
@@ -10,14 +10,18 @@
   [
     "--unwind 1",
     "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}",
-    "--nondet-static"
+    "--unwindset strncpy.0:{HOSTNAME_UNWIND}"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Callback.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "DEF":
   [