Merge pull request FreeRTOS#4 from FreeRTOS/labs/ipv6_multi

AniruddhaKanhere · web-flow · commit 9fde10540523 · 2021-01-26T15:18:06.000-08:00
Labs/ipv6 multi merge to fork
diff --git a/FreeRTOS_DHCP.c b/FreeRTOS_DHCP.c
@@ -217,8 +217,8 @@
 /*
  * Interpret message received on the DHCP socket.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint );
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint );
 
 /*
  * Generate a DHCP request packet, and send it on the DHCP socket.
@@ -966,8 +966,8 @@
  *
  * @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint )
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint )
     {
         uint8_t * pucUDPPayload;
         int32_t lBytes;
diff --git a/FreeRTOS_DNS.c b/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;
 
 
 /**
diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
@@ -97,8 +97,8 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
 * Function Abstraction:
 * prvProcessDHCPReplies has been proved memory safe in ProcessDHCPReplies.
 ****************************************************************/
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                  NetworkEndPoint_t * pxEndPoint )
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint )
 {
     return nondet_BaseType();
 }
diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
@@ -10,11 +10,16 @@
 
 /* Function Abstraction:
  * Function prvParseDNSReply is proven to be correct separately.
- * The proof can be found here: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/tree/labs/ipv6_multi/test/cbmc/proofs/ParseDNSReply */
-uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                           size_t uxBufferLength,
-                           struct freertos_addrinfo ** ppxAddressInfo,
-                           BaseType_t xExpected )
+ * The proof can be found here: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/tree/labs/ipv6_multi/test/cbmc/proofs/ParseDNSReply.
+ * Note: this function is defined as static in FreeRTOS_DNS.c.
+ * To access this function outside of that file, we have used
+ * a CBMC flag (--export-file-local-symbols). Using that flag
+ * mangles the names of static functions. Thus, the below
+ * function name is also mangled. */
+uint32_t __CPROVER_file_local_FreeRTOS_DNS_c_prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                                                               size_t uxBufferLength,
+                                                               struct freertos_addrinfo ** ppxAddressInfo,
+                                                               BaseType_t xExpected )
 {
     uint32_t ulReturn;
 
@@ -37,9 +42,13 @@ typedef struct xDNSMessage DNSMessage_t;
 void harness()
 {
     NetworkBufferDescriptor_t xNetworkBuffer;
+    size_t xEthernetBufferSize;
 
-    xNetworkBuffer.pucEthernetBuffer = malloc( sizeof( UDPPacket_t ) + sizeof( DNSMessage_t ) );
+    /* Allocate arbitrary number of bytes. */
+    xNetworkBuffer.pucEthernetBuffer = malloc( xEthernetBufferSize );
+    xNetworkBuffer.xDataLength = xEthernetBufferSize;
 
-    /* The parameter to the function cannot be NULL. */
+    /* The parameter to the function cannot be NULL. This function is called
+     * by the +TCP stack internally and is not an API. */
     ulDNSHandlePacket( &xNetworkBuffer );
 }
diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json
@@ -1,6 +1,6 @@
 {
   "ENTRY": "DNShandlePacket",
-  "CBMCFLAGS": "--unwind 1",
+  "CBMCFLAGS":"" ,
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
@@ -10,5 +10,10 @@
   [
     "ipconfigUSE_DNS=1",
     "ipconfigDNS_USE_CALLBACKS=1"
+  ],
+  "OPT":
+  [
+    # Flag to access the static function of a file
+    "--export-file-local-symbols"
   ]
 }
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/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 );
 }
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/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"
   ]
 }
diff --git a/test/cbmc/proofs/DNS/DNSlookup/DNSlookup_harness.c b/test/cbmc/proofs/DNS/DNSlookup/DNSlookup_harness.c
@@ -5,6 +5,7 @@
 
 /* FreeRTOS+TCP includes. */
 #include "FreeRTOS_IP.h"
+#include "FreeRTOS_Sockets.h"
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json
@@ -26,7 +26,7 @@
   "CBMCFLAGS": [
       # "--nondet-static",
       "--unwind 1",
-      "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+      "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
   ],
 
   "OBJS":
@@ -44,5 +44,11 @@
   [
     "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
     "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"
+  ],
+
+  "OPT":
+  [
+    # Flag to access the static function of a file
+    "--export-file-local-symbols"
   ]
 }
diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
@@ -13,25 +13,34 @@
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_ARP.h"
-
+#include "FreeRTOS_Routing.h"
 
 /****************************************************************
 * Signature of function under test
+* The function name (prvProcessDHCPReplies) is mangled due to the
+* use of a CBMC flag (--export-file-local-symbols) which allows us
+* to access this static function outside the source file in which
+* it is defined.
 ****************************************************************/
-
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint );
 
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
 ****************************************************************/
-
 void harness()
 {
     /* Omitting model of an unconstrained xDHCPData because xDHCPData is */
     /* the source of uninitialized data only on line 647 to set a */
     /* transaction id is an outgoing message */
 
     BaseType_t xExpectedMessageType;
+    NetworkEndPoint_t xEndPoint;
+
+    /* The function under test is a private (static) function called only by
+     * the TCP stack. The stack asserts that the endpoint cannot be NULL
+     * before the function under test is invoked. */
+    NetworkEndPoint_t * pxEndPoint = &xEndPoint;
 
-    prvProcessDHCPReplies( xExpectedMessageType );
+    __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxEndPoint );
 }

Original file line number	Diff line number	Diff line change
`@@ -377,8 +377,8 @@`
`377`	`377`	`}`
`378`	`378`	`#include "pack_struct_end.h"`
`379`	`379`	`typedef struct xDNSAnswerRecord DNSAnswerRecord_t;`
`380`		`-/** @brief this is for debugging only. */`
`381`		`- static struct freertos_addrinfo * pxLastInfo = NULL;`
	`380`	`+/** @brief Used for additional error checking when asserts are enabled. */`
	`381`	`+ _static struct freertos_addrinfo * pxLastInfo = NULL;`
`382`	`382`
`383`	`383`
`384`	`384`	`/**`
Original file line number	Diff line number	Diff line change
`@@ -97,8 +97,8 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,`
`97`	`97`	`* Function Abstraction:`
`98`	`98`	`* prvProcessDHCPReplies has been proved memory safe in ProcessDHCPReplies.`
`99`	`99`	`****************************************************************/`
`100`		`-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,`
`101`		`- NetworkEndPoint_t * pxEndPoint )`
	`100`	`+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,`
	`101`	`+ NetworkEndPoint_t * pxEndPoint )`
`102`	`102`	`{`
`103`	`103`	`return nondet_BaseType();`
`104`	`104`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`{`
`2`	`2`	`"ENTRY": "DNShandlePacket",`
`3`		`- "CBMCFLAGS": "--unwind 1",`
	`3`	`+ "CBMCFLAGS":"" ,`
`4`	`4`	`"OBJS":`
`5`	`5`	`[`
`6`	`6`	`"$(ENTRY)_harness.goto",`
`@@ -10,5 +10,10 @@`
`10`	`10`	`[`
`11`	`11`	`"ipconfigUSE_DNS=1",`
`12`	`12`	`"ipconfigDNS_USE_CALLBACKS=1"`
	`13`	`+ ],`
	`14`	`+ "OPT":`
	`15`	`+ [`
	`16`	`+ # Flag to access the static function of a file`
	`17`	`+ "--export-file-local-symbols"`
`13`	`18`	`]`
`14`	`19`	`}`
Original file line number	Diff line number	Diff line change
`@@ -26,7 +26,7 @@`
`26`	`26`	`"CBMCFLAGS": [`
`27`	`27`	`# "--nondet-static",`
`28`	`28`	`"--unwind 1",`
`29`		`- "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"`
	`29`	`+ "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"`
`30`	`30`	`],`
`31`	`31`
`32`	`32`	`"OBJS":`
`@@ -44,5 +44,11 @@`
`44`	`44`	`[`
`45`	`45`	`"CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",`
`46`	`46`	`"CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"`
	`47`	`+ ],`
	`48`	`+`
	`49`	`+ "OPT":`
	`50`	`+ [`
	`51`	`+ # Flag to access the static function of a file`
	`52`	`+ "--export-file-local-symbols"`
`47`	`53`	`]`
`48`	`54`	`}`