Add back deleted files

test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json

@@ -0,0 +1,28 @@
+{
+    "ENTRY": "SendDHCPMessage",
+    "CBMCFLAGS":
+    [
+      "--nondet-static"
+    ],
+    "INSTFLAGS":
+    [
+      "--generate-function-body 'xApplicationGetRandomNumber|ulApplicationTimeHook|xBitConfig_init|vBitConfig_write_8|vBitConfig_write_16|vBitConfig_write_32|FreeRTOS_inet_pton6|FreeRTOS_sendto|vBitConfig_release'",
+      "--generate-function-body-options nondet-return"
+    ],
+    "OPT":
+    [
+      "--export-file-local-symbols"
+    ],
+    "DEF":
+    [
+      "ipconfigUSE_DHCPv6=1"
+    ],
+    "OBJS":
+    [
+      "$(ENTRY)_harness.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+    ]
+}

test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c

@@ -0,0 +1,69 @@
+/*
+ * FreeRTOS memory safety proofs with CBMC.
+ * Copyright (C) 2022 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use, copy,
+ * modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
+ * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
+ * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ *
+ * http://aws.amazon.com/freertos
+ * http://www.FreeRTOS.org
+ */
+
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.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 "FreeRTOS_DHCPv6.h"
+#include "FreeRTOS_ARP.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+
+
+void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint );
+
+
+void harness()
+{
+    NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) );
+
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+
+    /* The application provides the random number and time hook in a memory safe manner. */
+
+    pxNetworkEndPoint_Temp->pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) );
+
+    /* All calls to prvSendDHCPMessage are after asserts to make sure pxDHCPMessage
+     * is never NULL. [xDHCPv6ProcessEndPoint_HandleState(): configASSERT( pxDHCPMessage != NULL );] */
+    __CPROVER_assume( pxNetworkEndPoint_Temp->pxDHCPMessage != NULL );
+
+    __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( pxNetworkEndPoint_Temp );
+}

test/cbmc/proofs/ProcessDHCPReplies/Makefile.json

@@ -0,0 +1,56 @@
+# The proof depends on one parameter:
+#   BUFFER_SIZE is the size of the buffer being parsed
+# The buffer size must be bounded because we must bound the number of
+# iterations loops iterating over the buffer.
+
+{
+  "ENTRY": "ProcessDHCPReplies",
+
+################################################################
+# Buffer header: sizeof(DHCPMessage_t) = 241
+# Buffer header: sizeof(DHCPMessage_IPv4_t) = 240
+  "BUFFER_HEADER": 240,
+  "ENDPOINT_DNS_ADDRESS_COUNT": 5,
+
+################################################################
+# Buffer size
+# Reasonable sizes are  BUFFER_SIZE > BUFFER_HEADER
+# Sizes smaller than this causes CBMC to fail in simplify_byte_extract
+  "BUFFER_SIZE": 252,
+
+################################################################
+# Buffer payload
+  "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 1",
+  "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
+
+################################################################
+
+  "CBMCFLAGS": [
+      # "--nondet-static",
+      "--unwind 1",
+      "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.0:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+      "--unwindset __CPROVER_file_local_FreeRTOS_DHCP_c_vProcessHandleOption.1:{ENDPOINT_DNS_ADDRESS_COUNT_UNWIND}",
+      "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+  ],
+  "OPT":
+  [
+    "--export-file-local-symbols"
+  ],
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_2.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/event_groups.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto"
+  ],
+
+  "DEF":
+  [
+    "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
+    "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}",
+    "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
+  ]
+}

test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c

@@ -0,0 +1,43 @@
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.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 "FreeRTOS_ARP.h"
+
+
+/****************************************************************
+* Signature of function under test
+****************************************************************/
+
+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 * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+
+    __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
+    pxNetworkEndPoint_Temp->pxNext = NULL;
+
+    __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxNetworkEndPoint_Temp );
+}