Fix the CBMC proof of DNSgetHostByName_a (FreeRTOS#172)

* Update the proof

* Uncrustify and spell check.

* Update after review comments

* Update after comments

Co-authored-by: Gary Wicker <[email protected]>

Author: AniruddhaKanhere

FreeRTOS_DNS.c

@@ -377,8 +377,8 @@
     }
     #include "pack_struct_end.h"
     typedef struct xDNSAnswerRecord DNSAnswerRecord_t;
-/** @brief this is for debugging only. */
-    static struct freertos_addrinfo * pxLastInfo = NULL;
+/** @brief Used for additional error checking when asserts are enabled. */
+    _static struct freertos_addrinfo * pxLastInfo = NULL;
 
 
 /**

test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c

@@ -14,6 +14,7 @@
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_DHCP.h"
+#include "FreeRTOS_Routing.h"
 #include "NetworkBufferManagement.h"
 #include "NetworkInterface.h"
 
@@ -37,6 +38,68 @@
 * bound the iterations of strcmp.
 ****************************************************************/
 
+/* This variable is defined in FreeRTOS_DNS.c  */
+extern struct freertos_addrinfo * pxLastInfo;
+
+/* Function Abstraction:
+ * pxGetNetworkBufferWithDescriptor allocates a Network buffer after taking it
+ * out of a list of network buffers maintained by the TCP stack. To prove the memory
+ * safety of the function under test, we do not need to initialise the list - it
+ * would make the proof more complex and deviate from its objective.
+ * Keeping this in mind, the below stub perform some basic checks required and
+ * allocates the required amount of memory without making any other assumptions
+ * whatsoever.
+ */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    __CPROVER_assert(
+        xRequestedSizeBytes + ipBUFFER_PADDING < CBMC_MAX_OBJECT_SIZE,
+        "pxGetNetworkBufferWithDescriptor: request too big" );
+
+    /* Arbitrarily return NULL or a valid pointer. */
+    NetworkBufferDescriptor_t * pxReturn = nondet_bool() ? NULL : malloc( sizeof( *pxReturn ) );
+
+    if( pxReturn != NULL )
+    {
+        /* Allocate the ethernet buffer. */
+        pxReturn->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipBUFFER_PADDING );
+
+        __CPROVER_assume( pxReturn->pucEthernetBuffer != NULL );
+
+        pxReturn->xDataLength = xRequestedSizeBytes;
+
+        /* Move the pointer ipBUFFER_PADDING (defined in FreeRTOS_IP.h) bytes
+         * ahead. This space is used to store data by the TCP stack for its own
+         * use whilst processing the packet. */
+        pxReturn->pucEthernetBuffer += ipBUFFER_PADDING;
+    }
+
+    return pxReturn;
+}
+
+/* Function Abstraction:
+ * vReleaseNetworkBufferAndDescriptor frees the memory associated with the ethernet
+ * buffer and returns the network buffer to a list maintained by the +TCP stack. But
+ * for the function under test, we do not need to initialise and maintain the list,
+ * as it would make the proof unnecessarily complex.
+ * Keeping this in mind, the stub below asserts some basic condition(s) and frees
+ * the memory allocated by the pxGetNetworkBufferWithDescriptor stub above.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    if( pxNetworkBuffer->pucEthernetBuffer != NULL )
+    {
+        pxNetworkBuffer->pucEthernetBuffer -= ipBUFFER_PADDING;
+        free( pxNetworkBuffer->pucEthernetBuffer );
+    }
+
+    free( pxNetworkBuffer );
+}
+
 /****************************************************************
 * Abstract prvParseDNSReply proved memory safe in ParseDNSReply.
 *
@@ -47,9 +110,10 @@
 * function.
 ****************************************************************/
 
-uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                           size_t xBufferLength,
-                           BaseType_t xExpected )
+uint32_t __CPROVER_file_local_FreeRTOS_DNS_c_prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                                                               size_t xBufferLength,
+                                                               struct freertos_addrinfo ** ppxAddressInfo,
+                                                               BaseType_t xExpected )
 {
     __CPROVER_assert( pucUDPPayloadBuffer != NULL,
                       "Precondition: pucUDPPayloadBuffer != NULL" );
@@ -67,9 +131,10 @@ uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
 * unconstrained data and returns and unconstrained length.
 ****************************************************************/
 
-size_t prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
-                            const char * pcHostName,
-                            TickType_t uxIdentifier )
+size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDPPayloadBuffer,
+                                                                const char * pcHostName,
+                                                                TickType_t uxIdentifier,
+                                                                UBaseType_t uxHostType )
 {
     __CPROVER_assert( pucUDPPayloadBuffer != NULL,
                       "Precondition: pucUDPPayloadBuffer != NULL" );
@@ -90,24 +155,49 @@ void func( const char * pcHostName,
 {
 }
 
+
+/** A list of all network end-points.  Each element has a next pointer. */
+extern struct xNetworkEndPoint * pxNetworkEndPoints;
+
+/** A list of all network interfaces: */
+extern struct xNetworkInterface * pxNetworkInterfaces;
+
+
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname_a.
 ****************************************************************/
-
 void harness()
 {
     size_t len;
 
-    __CPROVER_assume( len <= MAX_HOSTNAME_LEN );
-    char * pcHostName = safeMalloc( len );
+    __CPROVER_assume( ( len <= MAX_HOSTNAME_LEN ) && ( len > 0 ) );
 
-    __CPROVER_assume( len > 0 ); /* prvProcessDNSCache strcmp */
-    __CPROVER_assume( pcHostName != NULL );
-    pcHostName[ len - 1 ] = NULL;
+    /* Arbitrarily assign a proper memory or NULL to the hostname. */
+    char * pcHostName = nondet_bool() ? malloc( len ) : NULL;
 
-    FOnDNSEvent pCallback = func;
+    /* NULL terminate the string if the pcHostName is allocated. */
+    if( pcHostName != NULL )
+    {
+        pcHostName[ len - 1 ] = NULL;
+    }
+
+    /* Arbitrarily assign a NULL/valid-function to the function-pointer
+     * being used in the callback. */
+    FOnDNSEvent pCallback = nondet_bool() ? func : NULL;
     TickType_t xTimeout;
     void * pvSearchID;
 
+    /* Assume that the list of interfaces/endpoints is not initialized.
+     * Note: These variables are defined in FreeRTOS_Routing.c in global scope.
+     *       They serve as a list to the network interfaces and the corresponding
+     *       endpoints respectively. And are defined as NULL initially. */
+    __CPROVER_assume( pxNetworkInterfaces == NULL );
+    __CPROVER_assume( pxNetworkEndPoints == NULL );
+
+    /* Assume that the last info pointer is NULL at the beginning. This is defined
+     * in FreeRTOS_DNS.c and is used for debugging purpose. It is declared NULL
+     * initially. */
+    __CPROVER_assume( pxLastInfo == NULL );
+
     FreeRTOS_gethostbyname_a( pcHostName, pCallback, pvSearchID, xTimeout );
 }

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

@@ -6,25 +6,36 @@
   "callback": 1,
   "MAX_HOSTNAME_LEN": 10,
   "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
+  "DNS_REQ_ATTEMPTS":2,
+  "DNS_REQUEST_ATTEMPTS": "__eval {DNS_REQ_ATTEMPTS} + 1",
+  "DNS_CACHE_ENTRIES":3,
+  "DNS_CACHE_ENTRIES_UNWIND": "__eval {DNS_CACHE_ENTRIES} + 1",
   "CBMCFLAGS":
   [
     "--unwind 1",
-    "--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}",
+    "--unwindset FreeRTOS_freeaddrinfo.0:2,__CPROVER_file_local_FreeRTOS_DNS_c_prvReadDNSCache.0:2,__CPROVER_file_local_FreeRTOS_DNS_c_prvGetHostByName.1:{DNS_REQUEST_ATTEMPTS},__CPROVER_file_local_FreeRTOS_DNS_c_prvProcessDNSCache.0:{DNS_CACHE_ENTRIES_UNWIND},prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},__CPROVER_file_local_FreeRTOS_DNS_c_prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND},strncpy.0:255",
     "--nondet-static"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/FreeRTOS_IP.goto"
   ],
   "DEF":
   [
     "ipconfigDNS_USE_CALLBACKS={callback}",
     "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
+    "ipconfigDNS_REQUEST_ATTEMPTS={DNS_REQ_ATTEMPTS}",
     # This value is defined only when ipconfigUSE_DNS_CACHE==1
     "ipconfigDNS_CACHE_NAME_LENGTH=254"
+  ],
+  "OPT":
+  [
+    # Flag to access the static function of a file
+    "--export-file-local-symbols"
   ]
 }