[Draft - Do not merge] CBMC enhancements

test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json

@@ -9,6 +9,11 @@
       "--unwindset vARPAgeCache.1:3",
       "--nondet-static"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|FreeRTOS_OutputAdvertiseIPv6|xQueueGenericSend|xIsCallingFromIPTask'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json

@@ -10,6 +10,11 @@
       "--unwindset FreeRTOS_FindGateWay.0:3",
       "--nondet-static"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'vSetMultiCastIPv4MacAddress|xIsIPv4Multicast'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json

@@ -7,6 +7,11 @@
       "--unwindset prvFindCacheEntry.0:7",
       "--nondet-static"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'xTaskCheckForTimeOut|vReleaseNetworkBufferAndDescriptor|xQueueGenericSend|vTaskSetTimeOutState|xIsCallingFromIPTask|FreeRTOS_FindEndPointOnNetMask|xTaskGetTickCount|vIPSetARPResolutionTimerEnableState'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json

@@ -5,6 +5,11 @@
       "--unwind 1",
       "--nondet-static"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'xQueueGenericSend|xIsCallingFromIPTask'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json

@@ -32,6 +32,11 @@
   [
       "--unwind 20"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|xIsCallingFromIPTask'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json

@@ -6,6 +6,11 @@
       "--unwind {MINIMUM_PACKET_BYTES}",
       "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'xTaskGetSchedulerState|vPortExitCritical|vPortEnterCritical|xIsCallingFromIPTask'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json

@@ -6,6 +6,11 @@
       "--unwind {MINIMUM_PACKET_BYTES}",
       "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'xTaskGetSchedulerState|vPortExitCritical|vPortEnterCritical|xIsCallingFromIPTask'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",

test/cbmc/proofs/CheckOptionsInner/Makefile.json

@@ -5,6 +5,11 @@
       "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2",
       "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.0:2"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'ulChar2u32|FreeRTOS_min_size_t'",
+    "--generate-function-body-options nondet-return"
+  ],  
   "OPT":
   [
       "--export-file-local-symbols"

test/cbmc/proofs/CheckOptionsOuter/Makefile.json

@@ -5,6 +5,11 @@
       "--unwind 1",
       "--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.0:32"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'usChar2u16'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OPT":
   [
       "--export-file-local-symbols"

test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json

@@ -14,6 +14,11 @@
     "--unwind {LOOP_UNWIND_COUNT}",
     "--nondet-static --flush"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'FreeRTOS_setsockopt|vSocketClose|FreeRTOS_socket'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OPT":
   [
     "--export-file-local-symbols"

test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json

@@ -14,6 +14,11 @@
     "--unwindset strlen.0:11,memcmp.0:7",
     "--nondet-static --flush"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'vManageSolicitedNodeAddress|xQueueGenericSend|vIPSetDHCP_RATimerEnableState|vDHCP_RATimerReload|xApplicationGetRandomNumber|vARPTimerReload|xIsCallingFromIPTask|vSocketClose|vPortExitCritical|vApplicationIPNetworkEventHook_Multi|xTaskGetTickCount|vPortEnterCritical'",
+    "--generate-function-body-options nondet-return"
+  ],
   "OPT":
   [
     "--export-file-local-symbols"

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

@@ -9,7 +9,8 @@
     ],
     "INSTFLAGS":
     [
-        "--remove-function-body __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption",
+      "--generate-function-body '__CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption'",
+      "--generate-function-body-options nondet-return",
         "--malloc-may-fail"
     ],
     "OPT":

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

@@ -7,9 +7,8 @@
     ],
     "INSTFLAGS":
     [
-        "--remove-function-body usBitConfig_read_16",
-        "--remove-function-body xBitConfig_read_uc",
-        "--remove-function-body ucBitConfig_read_8"
+      "--generate-function-body 'usBitConfig_read_16|xBitConfig_read_uc|ucBitConfig_read_8'",
+      "--generate-function-body-options nondet-return"
     ],
     "OPT":
     [

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

@@ -6,6 +6,11 @@
       "--unwind {LOOP_UNWIND_COUNT}",
       "--nondet-static --flush"
     ],
+    "INSTFLAGS":
+    [
+      "--generate-function-body 'vIPSetDHCP_RATimerEnableState|FreeRTOS_socket|FreeRTOS_setsockopt|vPortExitCritical|vPortEnterCritical'",
+      "--generate-function-body-options nondet-return"
+    ],
     "OPT":
     [
       "--export-file-local-symbols"

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

@@ -1,37 +1,28 @@
-{
-    "ENTRY": "SendDHCPMessage",
-    "CBMCFLAGS":
-    [
-      "--nondet-static"
-    ],
-    "INSTFLAGS":
-    [
-      "--remove-function-body xApplicationGetRandomNumber",
-      "--remove-function-body ulApplicationTimeHook",
-      "--remove-function-body xBitConfig_init",
-      "--remove-function-body vBitConfig_write_8",
-      "--remove-function-body vBitConfig_write_uc",
-      "--remove-function-body vBitConfig_write_16",
-      "--remove-function-body vBitConfig_write_32",
-      "--remove-function-body pucBitConfig_peek_last_index_uc",
-      "--remove-function-body FreeRTOS_inet_pton6",
-      "--remove-function-body FreeRTOS_sendto",
-      "--remove-function-body vBitConfig_release"
-    ],
-    "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"
-    ]
+{
+    "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

@@ -1,69 +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 );
-}
+/*
+ * 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/DNS/DNSHandlePacket/Makefile.json

@@ -6,6 +6,11 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'DNS_ParseDNSReply|uxIPHeaderSizePacket'",
+    "--generate-function-body-options nondet-return"
+  ],
   "DEF":
   [
   ]

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

@@ -14,6 +14,11 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
   ],
+  "INSTFLAGS":
+  [
+    "--generate-function-body 'vReturnEthernetFrame|FreeRTOS_dns_update|xApplicationDNSQueryHook_Multi'",
+    "--generate-function-body-options nondet-return"
+  ],
   "DEF":
   [
     "ipconfigUSE_DNS_CACHE={USE_CACHE}",