From b831762a45d2c0f9fdcc341afba8dc97cb0985f2 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 May 2024 14:42:32 +0530 Subject: [PATCH 1/4] generate func bodies --- .../cbmc/proofs/ARP/ARPAgeCache/Makefile.json | 5 ++ .../ARP/ARPGetCacheEntry/Configurations.json | 5 ++ .../proofs/ARP/ARPProcessPacket/Makefile.json | 5 ++ .../ARP/ARPSendGratuitous/Makefile.json | 5 ++ .../Configurations.json | 5 ++ .../Configurations.json | 5 ++ .../Configurations.json | 5 ++ .../proofs/CheckOptionsInner/Makefile.json | 5 ++ .../proofs/CheckOptionsOuter/Makefile.json | 5 ++ .../proofs/DHCP/DHCPProcess/Makefile.json | 5 ++ .../DHCP/DHCPProcessEndPoint/Makefile.json | 5 ++ .../proofs/DHCPv6/DHCPv6Analyse/Makefile.json | 3 +- .../DHCPv6/DHCPv6HandleOption/Makefile.json | 5 +- .../proofs/DHCPv6/DHCPv6Process/Makefile.json | 5 ++ .../DHCPv6/SendDHCPMessage/Makefile.json | 37 ---------- .../SendDHCPMessage/SendDHCPMessage_harness.c | 69 ------------------- .../proofs/DNS/DNSHandlePacket/Makefile.json | 5 ++ .../proofs/DNS/DNSTreatNBNS/Makefile.json | 5 ++ .../proofs/DNS/DNSgetHostByName/Makefile.json | 6 +- .../DNS/DNSgetHostByName_a/Makefile.json | 5 ++ .../DNS/DNSgetHostByName_cancel/Makefile.json | 5 ++ .../DNS/prepareReplyDNSMessage/Makefile.json | 5 ++ .../IP/ProcessEthernetPacket/Makefile.json | 5 ++ .../proofs/IP/SendEventToIPTask/Makefile.json | 5 ++ .../usGenerateProtocolChecksum/Makefile.json | 3 +- .../Makefile.json | 3 +- test/cbmc/proofs/Makefile.template | 11 +++ .../prvProcessICMPMessage_IPv6/Makefile.json | 5 ++ .../ND/prvReturnICMP_IPv6/Makefile.json | 5 ++ .../proofs/ProcessDHCPReplies/Makefile.json | 56 --------------- .../ProcessDHCPReplies_harness.c | 43 ------------ test/cbmc/proofs/RA/vReceiveRA/Makefile.json | 5 ++ .../RA/vReceiveRA_ReadReply/Makefile.json | 5 ++ .../Routing/MatchingEndpoint/Makefile.json | 5 ++ .../proofs/Socket/lTCPAddRxdata/Makefile.json | 5 ++ .../Makefile.json | 2 + .../Socket/vSocketClose/Configurations.json | 5 ++ .../proofs/TCP/prvHandleListen/Makefile.json | 9 +-- .../TCP/prvHandleListen_IPv6/Makefile.json | 9 +-- .../cbmc/proofs/TCP/prvSendData/Makefile.json | 5 ++ .../TCP/prvTCPHandleState/Makefile.json | 11 +-- .../TCP/prvTCPPrepareSend/Makefile.json | 5 ++ .../TCP/prvTCPReturnPacket/Makefile.json | 5 ++ .../TCP/prvTCPReturnPacket_IPv6/Makefile.json | 5 ++ .../vProcessGeneratedUDPPacket/Makefile.json | 5 ++ .../ProcessIPPacket/Configurations.json | 5 ++ .../ProcessReceivedTCPPacket/Makefile.json | 7 +- .../Makefile.json | 4 +- .../ProcessReceivedUDPPacket/Makefile.json | 5 ++ .../prvChecksumIPv6Checks/Makefile.json | 8 ++- test/cbmc/proofs/run-cbmc-proofs.py | 12 ++++ 51 files changed, 229 insertions(+), 234 deletions(-) delete mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json delete mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c delete mode 100644 test/cbmc/proofs/ProcessDHCPReplies/Makefile.json delete mode 100644 test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json index 24de2ff3c..a1c285c45 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json index aa4d60296..7d34c97db 100644 --- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json index 00079ded1..9766e9975 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json index f069f5959..f11e5145d 100644 --- a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json index 62bb3e052..e8e8bb1b6 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json index e243382c3..e235e6794 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json index 5b2cdd30d..169ed87d8 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index a902bcc94..3a9dbd15c 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index d97be23e6..f6e26cc8e 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 99e79d3b2..08ec0c8bc 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json index ed7497613..34f33b5a1 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json index 08e8432de..47d64f298 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json +++ b/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": diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json index 09859a60b..0b9e6d05d 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json +++ b/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": [ diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json index 40839470b..d2480b5e7 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json deleted file mode 100644 index 08cb3e73a..000000000 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json +++ /dev/null @@ -1,37 +0,0 @@ -{ - "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" - ] -} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c deleted file mode 100644 index fc2886720..000000000 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ /dev/null @@ -1,69 +0,0 @@ -/* - * 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 - -/* 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 ); -} diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json index 27864b146..fa08c7798 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json +++ b/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": [ ] diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json index 458443eb7..1ba42ffb1 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json +++ b/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}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 66b7cad54..a48a0c657 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -36,7 +36,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], - + "INSTFLAGS": + [ + "--generate-function-body 'Prepare_CacheLookup|vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|xApplicationGetRandomNumber|FreeRTOS_ReleaseUDPPayloadBuffer|FreeRTOS_inet_addr'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_IPv6=1", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index f67cb0a11..cc4f09d8d 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -30,6 +30,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|DNS_SendRequest|xApplicationGetRandomNumber|vDNSSetCallBack|ulChar2u32|DNS_CloseSocket|DNS_ReadReply|FreeRTOS_inet_addr'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json index 8f568fb54..0a2ba1425 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -19,6 +19,11 @@ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vDNSCallbackInitialise|vDNSSetCallBack|vDNSCheckCallBack'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json index f4f366afb..9e30a765a 100644 --- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json +++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json @@ -13,6 +13,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'uxIPHeaderSizePacket'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_DNS_CACHE={USE_CACHE}", diff --git a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json index 4a2b35b44..641cc8bdf 100644 --- a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json +++ b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json @@ -4,6 +4,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|vIPTimerStartARPResolution'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json index 30727432c..09c6c52c6 100644 --- a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json +++ b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json @@ -32,6 +32,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'uxQueueMessagesWaiting|vIPSetTCPTimerExpiredState|xIsCallingFromIPTask|xQueueGenericSend'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json index dc882f519..98b83571d 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json @@ -7,7 +7,8 @@ ], "INSTFLAGS": [ - "--remove-function-body prvChecksumIPv6Checks" + "--generate-function-body 'prvChecksumIPv6Checks'", + "--generate-function-body-options nondet-return" ], "OBJS": [ diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json index ddf4febda..5cb256237 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json @@ -10,7 +10,8 @@ ], "INSTFLAGS": [ - "--remove-function-body prvChecksumIPv4Checks" + "--generate-function-body 'prvChecksumIPv4Checks'", + "--generate-function-body-options nondet-return" ], "OBJS": [ diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 094fd560c..6466adae5 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -150,6 +150,17 @@ report: cbmc.xml property.xml coverage.xml check-cbmc-result: cbmc.xml grep 'SUCCESS' $^ +# This rule depends only on cbmc.xml and has no dependents, so it will +# not block the report from being generated if it fails. This rule is +# intended to fail if and only if the CBMC safety check that emits +# cbmc.xml yielded a warning about undefined functions. +check-cbmc-undefined-functions: cbmc.xml + if grep '**** WARNING: no body for function' $^; then \ + exit 1; \ + else \ + exit 0; \ + fi + # ____________________________________________________________________ # Rules # diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json index 09f7d0beb..f6275dca3 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json @@ -5,6 +5,11 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json index cdc3a4f0a..b746a4b5c 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json @@ -5,6 +5,11 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json deleted file mode 100644 index 09d5c8d4e..000000000 --- a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json +++ /dev/null @@ -1,56 +0,0 @@ -# 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}" - ] -} diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c deleted file mode 100644 index ef0068b9e..000000000 --- a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c +++ /dev/null @@ -1,43 +0,0 @@ -/* Standard includes. */ -#include - -/* 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 ); -} diff --git a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json index 8b995fc8d..89b4b6bac 100644 --- a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json @@ -6,6 +6,11 @@ "--unwindset FreeRTOS_NextEndPoint.0:1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vDHCP_RATimerReload|vNDSendNeighbourSolicitation|FreeRTOS_CreateIPv6Address'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json index 61d93b3d5..c863c6b8e 100644 --- a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json @@ -5,6 +5,11 @@ "--unwind 3", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'ulChar2u32'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json index 3c235d92b..38f05ea32 100644 --- a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json +++ b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json @@ -6,6 +6,11 @@ "--unwindset pxEasyFit.0:{MAX_ENDPOINT_COUNT_LOOP}", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'xIsIPv6Loopback'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json index 6a4799f87..04dd1bb4d 100644 --- a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json +++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json @@ -4,6 +4,11 @@ [ "--unwind 1" ], + "INSTFLAGS": + [ + "--generate-function-body 'vTCPStateChange|xSendEventToIPTask|uxStreamBufferAdd|uxStreamBufferFrontSpace'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json index 379ae7a39..013b864fb 100644 --- a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json +++ b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json @@ -17,6 +17,8 @@ ], "INSTFLAGS": [ + "--generate-function-body 'vTaskSuspendAll|xTaskResumeAll'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json index 50df09417..e97e737b7 100644 --- a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json +++ b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json @@ -5,6 +5,11 @@ [ "--unwind 2" ], + "INSTFLAGS": + [ + "--generate-function-body 'vEventGroupDelete|xEventGroupCreate'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", diff --git a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json index 856e50c30..85fc8b13b 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json @@ -5,6 +5,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress|ulApplicationGetNextSequenceNumber'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", @@ -17,10 +22,6 @@ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPSendReset" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json index aa1ee4f70..13eab4922 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json @@ -14,15 +14,16 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv6.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|xApplicationGetRandomNumber|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPSendReset" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvSendData/Makefile.json b/test/cbmc/proofs/TCP/prvSendData/Makefile.json index cfc73e67e..bab3bf136 100644 --- a/test/cbmc/proofs/TCP/prvSendData/Makefile.json +++ b/test/cbmc/proofs/TCP/prvSendData/Makefile.json @@ -5,6 +5,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|uxIPHeaderSizeSocket|prvTCPReturnPacket_IPV4'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json index a192cca2d..07948b1fb 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json @@ -46,17 +46,18 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPReturnPacket", + "--generate-function-body 'ulTCPWindowTxAck|prvTCPAddTxData|prvSetSynAckOptions|lTCPWindowRxCheck|vTaskSuspendAll|xTCPWindowTxDone|xTaskResumeAll|uxStreamBufferGet|prvSetOptions|lTCPAddRxdata|uxStreamBufferGetSpace|vTCPWindowInit|prvTCPSendReset|xTCPWindowRxEmpty|vSocketClose|xTaskGetTickCount|vSocketWakeUpUser|prvTCPPrepareSend|FreeRTOS_inet_ntop|FreeRTOS_listen|prvSendData'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", "FREERTOS_TCP_ENABLE_VERIFICATION" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json index 97cbf2b02..b3bed0caf 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -33,6 +33,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|xTCPWindowTxDone|vTaskSuspendAll|xTaskResumeAll|vSocketWakeUpUser|uxStreamBufferDistance|uxStreamBufferGet|vSocketClose|ulTCPWindowTxGet|FreeRTOS_listen|xTaskGetTickCount|prvTCPSocketIsActive'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json index 1b67f5a07..c0610595d 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -43,6 +43,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv4.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|FreeRTOS_min_uint32'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json index 9b28c3b34..a4b420e84 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json @@ -15,6 +15,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV4|eNDGetCacheEntry|FreeRTOS_min_uint32'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json index f7ef2a84d..9ca86c95b 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json @@ -3,6 +3,11 @@ "CBMCFLAGS": [ ], + "INSTFLAGS": + [ + "--generate-function-body 'vProcessGeneratedUDPPacket_IPv6'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json index 1ef122113..40ca60609 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json @@ -7,6 +7,11 @@ "--unwindset FreeRTOS_AllEndPointsUp.0:2", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'xGetExtensionOrder|vNDRefreshCacheEntry|ProcessICMPPacket|xCheckRequiresARPResolution|vARPRefreshCacheEntryAge|eHandleIPv6ExtensionHeaders|prvAllowIPPacketIPv6|FreeRTOS_FindEndPointOnIP_IPv4|prvProcessICMPMessage_IPv6'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json index f2643c9b9..6ceb92875 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -24,11 +24,8 @@ "INSTFLAGS": [ "--remove-function-body prvSingleStepTCPHeaderOptions", - "--remove-function-body prvCheckOptions", - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket", - "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPHandleState|vTCPStateChange|xSequenceGreaterThan|prvCheckOptions|prvTCPPrepareSend|xSequenceLessThan|xTCPWindowTxHasData|xTaskGetTickCount|prvTCPReturnPacket'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json index 53a28f733..f5d271f73 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json @@ -22,7 +22,9 @@ "--remove-function-body prvTCPPrepareSend", "--remove-function-body prvTCPReturnPacket", "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" + "--remove-function-body vTCPStateChange", + "--generate-function-body 'xProcessReceivedTCPPacket_IPV6'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json index bc0bc61db..06bef8c3c 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -8,6 +8,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vARPRefreshCacheEntryAge'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json index 9645ee00a..7a7dcbbab 100644 --- a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json +++ b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json @@ -9,15 +9,17 @@ "--unwindset prvPrepareExtensionHeaders.0:{MAX_EXT_HEADER_NUM}", "--flush" ], + "INSTFLAGS": + [ + "--generate-function-body 'xGetExtensionOrder'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Utils.goto" ], - "INSTFLAGS": - [ - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index 429d78734..04c2b7fa3 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -226,6 +226,18 @@ def add_proof_jobs(proof_directory, proof_root): "--description", ("%s: computing coverage" % proof_name), ], check=True) + # Check whether the CBMC proof doesn't have undefined functions. + # More details in the Makefile rule for check-cbmc-undefined-functions. + run_cmd([ + "litani", "add-job", + "--command", "make check-cbmc-undefined-functions", + "--inputs", cbmc_out, + "--pipeline-name", proof_name, + "--ci-stage", "report", + "--cwd", str(proof_directory), + "--description", ("%s: checking for undefined functions" % proof_name), + ], check=True) + # Check whether the CBMC proof actually passed. More details in the # Makefile rule for check-cbmc-result. run_cmd([ From 62cd07b043bdfb1c3d488b0e139b76a91f630c87 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 May 2024 14:49:09 +0530 Subject: [PATCH 2/4] cbmc enhancements --- test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json | 5 ----- .../proofs/ARP/ARPGetCacheEntry/Configurations.json | 5 ----- test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json | 5 ----- test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json | 5 ----- .../Configurations.json | 5 ----- .../Configurations.json | 5 ----- .../Configurations.json | 5 ----- test/cbmc/proofs/CheckOptionsInner/Makefile.json | 5 ----- test/cbmc/proofs/CheckOptionsOuter/Makefile.json | 5 ----- test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 5 ----- .../proofs/DHCP/DHCPProcessEndPoint/Makefile.json | 5 ----- test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json | 3 +-- .../proofs/DHCPv6/DHCPv6HandleOption/Makefile.json | 5 +++-- test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json | 5 ----- test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json | 5 ----- test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json | 5 ----- test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 6 +----- .../cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json | 5 ----- .../proofs/DNS/DNSgetHostByName_cancel/Makefile.json | 5 ----- .../proofs/DNS/prepareReplyDNSMessage/Makefile.json | 5 ----- .../proofs/IP/ProcessEthernetPacket/Makefile.json | 5 ----- test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json | 5 ----- .../IPUtils/usGenerateProtocolChecksum/Makefile.json | 3 +-- .../usGenerateProtocolChecksum_IPv6/Makefile.json | 3 +-- test/cbmc/proofs/Makefile.template | 11 ----------- .../ND/prvProcessICMPMessage_IPv6/Makefile.json | 5 ----- test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json | 5 ----- test/cbmc/proofs/RA/vReceiveRA/Makefile.json | 5 ----- .../proofs/RA/vReceiveRA_ReadReply/Makefile.json | 5 ----- .../proofs/Routing/MatchingEndpoint/Makefile.json | 5 ----- test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json | 5 ----- .../Makefile.json | 2 -- .../proofs/Socket/vSocketClose/Configurations.json | 5 ----- test/cbmc/proofs/TCP/prvHandleListen/Makefile.json | 9 ++++----- .../proofs/TCP/prvHandleListen_IPv6/Makefile.json | 9 ++++----- test/cbmc/proofs/TCP/prvSendData/Makefile.json | 5 ----- test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json | 11 +++++------ test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json | 5 ----- .../cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json | 5 ----- .../proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json | 5 ----- .../UDP/vProcessGeneratedUDPPacket/Makefile.json | 5 ----- .../parsing/ProcessIPPacket/Configurations.json | 5 ----- .../parsing/ProcessReceivedTCPPacket/Makefile.json | 7 +++++-- .../ProcessReceivedTCPPacket_IPv6/Makefile.json | 4 +--- .../parsing/ProcessReceivedUDPPacket/Makefile.json | 5 ----- test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json | 8 +++----- test/cbmc/proofs/run-cbmc-proofs.py | 12 ------------ 47 files changed, 29 insertions(+), 229 deletions(-) diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json index a1c285c45..24de2ff3c 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json @@ -9,11 +9,6 @@ "--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", diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json index 7d34c97db..aa4d60296 100644 --- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json +++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -10,11 +10,6 @@ "--unwindset FreeRTOS_FindGateWay.0:3", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vSetMultiCastIPv4MacAddress|xIsIPv4Multicast'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json index 9766e9975..00079ded1 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json @@ -7,11 +7,6 @@ "--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", diff --git a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json index f11e5145d..f069f5959 100644 --- a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json +++ b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -5,11 +5,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'xQueueGenericSend|xIsCallingFromIPTask'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json index e8e8bb1b6..62bb3e052 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -32,11 +32,6 @@ [ "--unwind 20" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|xIsCallingFromIPTask'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json index e235e6794..e243382c3 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -6,11 +6,6 @@ "--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", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json index 169ed87d8..5b2cdd30d 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json +++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -6,11 +6,6 @@ "--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", diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index 3a9dbd15c..a902bcc94 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -5,11 +5,6 @@ "--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" diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index f6e26cc8e..d97be23e6 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json @@ -5,11 +5,6 @@ "--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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 08ec0c8bc..99e79d3b2 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json @@ -14,11 +14,6 @@ "--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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json index 34f33b5a1..ed7497613 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json +++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json @@ -14,11 +14,6 @@ "--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" diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json index 47d64f298..08e8432de 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json @@ -9,8 +9,7 @@ ], "INSTFLAGS": [ - "--generate-function-body '__CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption'", - "--generate-function-body-options nondet-return", + "--remove-function-body __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption", "--malloc-may-fail" ], "OPT": diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json index 0b9e6d05d..09859a60b 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json @@ -7,8 +7,9 @@ ], "INSTFLAGS": [ - "--generate-function-body 'usBitConfig_read_16|xBitConfig_read_uc|ucBitConfig_read_8'", - "--generate-function-body-options nondet-return" + "--remove-function-body usBitConfig_read_16", + "--remove-function-body xBitConfig_read_uc", + "--remove-function-body ucBitConfig_read_8" ], "OPT": [ diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json index d2480b5e7..40839470b 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json @@ -6,11 +6,6 @@ "--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" diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json index fa08c7798..27864b146 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json @@ -6,11 +6,6 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'DNS_ParseDNSReply|uxIPHeaderSizePacket'", - "--generate-function-body-options nondet-return" - ], "DEF": [ ] diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json index 1ba42ffb1..458443eb7 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json @@ -14,11 +14,6 @@ "$(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}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index a48a0c657..66b7cad54 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -36,11 +36,7 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'Prepare_CacheLookup|vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|xApplicationGetRandomNumber|FreeRTOS_ReleaseUDPPayloadBuffer|FreeRTOS_inet_addr'", - "--generate-function-body-options nondet-return" - ], + "DEF": [ "ipconfigUSE_IPv6=1", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index cc4f09d8d..f67cb0a11 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -30,11 +30,6 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|DNS_SendRequest|xApplicationGetRandomNumber|vDNSSetCallBack|ulChar2u32|DNS_CloseSocket|DNS_ReadReply|FreeRTOS_inet_addr'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json index 0a2ba1425..8f568fb54 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -19,11 +19,6 @@ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'vDNSCallbackInitialise|vDNSSetCallBack|vDNSCheckCallBack'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json index 9e30a765a..f4f366afb 100644 --- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json +++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json @@ -13,11 +13,6 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'uxIPHeaderSizePacket'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigUSE_DNS_CACHE={USE_CACHE}", diff --git a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json index 641cc8bdf..4a2b35b44 100644 --- a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json +++ b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json @@ -4,11 +4,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|vIPTimerStartARPResolution'", - "--generate-function-body-options nondet-return" - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json index 09c6c52c6..30727432c 100644 --- a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json +++ b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json @@ -32,11 +32,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'uxQueueMessagesWaiting|vIPSetTCPTimerExpiredState|xIsCallingFromIPTask|xQueueGenericSend'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json index 98b83571d..dc882f519 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json @@ -7,8 +7,7 @@ ], "INSTFLAGS": [ - "--generate-function-body 'prvChecksumIPv6Checks'", - "--generate-function-body-options nondet-return" + "--remove-function-body prvChecksumIPv6Checks" ], "OBJS": [ diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json index 5cb256237..ddf4febda 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json @@ -10,8 +10,7 @@ ], "INSTFLAGS": [ - "--generate-function-body 'prvChecksumIPv4Checks'", - "--generate-function-body-options nondet-return" + "--remove-function-body prvChecksumIPv4Checks" ], "OBJS": [ diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 6466adae5..094fd560c 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -150,17 +150,6 @@ report: cbmc.xml property.xml coverage.xml check-cbmc-result: cbmc.xml grep 'SUCCESS' $^ -# This rule depends only on cbmc.xml and has no dependents, so it will -# not block the report from being generated if it fails. This rule is -# intended to fail if and only if the CBMC safety check that emits -# cbmc.xml yielded a warning about undefined functions. -check-cbmc-undefined-functions: cbmc.xml - if grep '**** WARNING: no body for function' $^; then \ - exit 1; \ - else \ - exit 0; \ - fi - # ____________________________________________________________________ # Rules # diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json index f6275dca3..09f7d0beb 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json @@ -5,11 +5,6 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json index b746a4b5c..cdc3a4f0a 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json @@ -5,11 +5,6 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json index 89b4b6bac..8b995fc8d 100644 --- a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json @@ -6,11 +6,6 @@ "--unwindset FreeRTOS_NextEndPoint.0:1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vDHCP_RATimerReload|vNDSendNeighbourSolicitation|FreeRTOS_CreateIPv6Address'", - "--generate-function-body-options nondet-return" - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json index c863c6b8e..61d93b3d5 100644 --- a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json @@ -5,11 +5,6 @@ "--unwind 3", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'ulChar2u32'", - "--generate-function-body-options nondet-return" - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json index 38f05ea32..3c235d92b 100644 --- a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json +++ b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json @@ -6,11 +6,6 @@ "--unwindset pxEasyFit.0:{MAX_ENDPOINT_COUNT_LOOP}", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'xIsIPv6Loopback'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json index 04dd1bb4d..6a4799f87 100644 --- a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json +++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json @@ -4,11 +4,6 @@ [ "--unwind 1" ], - "INSTFLAGS": - [ - "--generate-function-body 'vTCPStateChange|xSendEventToIPTask|uxStreamBufferAdd|uxStreamBufferFrontSpace'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json index 013b864fb..379ae7a39 100644 --- a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json +++ b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json @@ -17,8 +17,6 @@ ], "INSTFLAGS": [ - "--generate-function-body 'vTaskSuspendAll|xTaskResumeAll'", - "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json index e97e737b7..50df09417 100644 --- a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json +++ b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json @@ -5,11 +5,6 @@ [ "--unwind 2" ], - "INSTFLAGS": - [ - "--generate-function-body 'vEventGroupDelete|xEventGroupCreate'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", diff --git a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json index 85fc8b13b..856e50c30 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json @@ -5,11 +5,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress|ulApplicationGetNextSequenceNumber'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", @@ -22,6 +17,10 @@ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPSendReset" + ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json index 13eab4922..aa1ee4f70 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json @@ -14,16 +14,15 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv6.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|xApplicationGetRandomNumber|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPSendReset" + ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvSendData/Makefile.json b/test/cbmc/proofs/TCP/prvSendData/Makefile.json index bab3bf136..cfc73e67e 100644 --- a/test/cbmc/proofs/TCP/prvSendData/Makefile.json +++ b/test/cbmc/proofs/TCP/prvSendData/Makefile.json @@ -5,11 +5,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|uxIPHeaderSizeSocket|prvTCPReturnPacket_IPV4'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json index 07948b1fb..a192cca2d 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json @@ -46,18 +46,17 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPReturnPacket", - "--generate-function-body 'ulTCPWindowTxAck|prvTCPAddTxData|prvSetSynAckOptions|lTCPWindowRxCheck|vTaskSuspendAll|xTCPWindowTxDone|xTaskResumeAll|uxStreamBufferGet|prvSetOptions|lTCPAddRxdata|uxStreamBufferGetSpace|vTCPWindowInit|prvTCPSendReset|xTCPWindowRxEmpty|vSocketClose|xTaskGetTickCount|vSocketWakeUpUser|prvTCPPrepareSend|FreeRTOS_inet_ntop|FreeRTOS_listen|prvSendData'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", "FREERTOS_TCP_ENABLE_VERIFICATION" ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket" + ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json index b3bed0caf..97cbf2b02 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -33,11 +33,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|xTCPWindowTxDone|vTaskSuspendAll|xTaskResumeAll|vSocketWakeUpUser|uxStreamBufferDistance|uxStreamBufferGet|vSocketClose|ulTCPWindowTxGet|FreeRTOS_listen|xTaskGetTickCount|prvTCPSocketIsActive'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json index c0610595d..1b67f5a07 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -43,11 +43,6 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv4.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|FreeRTOS_min_uint32'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json index a4b420e84..9b28c3b34 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json @@ -15,11 +15,6 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], - "INSTFLAGS": - [ - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV4|eNDGetCacheEntry|FreeRTOS_min_uint32'", - "--generate-function-body-options nondet-return" - ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json index 9ca86c95b..f7ef2a84d 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json @@ -3,11 +3,6 @@ "CBMCFLAGS": [ ], - "INSTFLAGS": - [ - "--generate-function-body 'vProcessGeneratedUDPPacket_IPv6'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json index 40ca60609..1ef122113 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json @@ -7,11 +7,6 @@ "--unwindset FreeRTOS_AllEndPointsUp.0:2", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'xGetExtensionOrder|vNDRefreshCacheEntry|ProcessICMPPacket|xCheckRequiresARPResolution|vARPRefreshCacheEntryAge|eHandleIPv6ExtensionHeaders|prvAllowIPPacketIPv6|FreeRTOS_FindEndPointOnIP_IPv4|prvProcessICMPMessage_IPv6'", - "--generate-function-body-options nondet-return" - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json index 6ceb92875..f2643c9b9 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -24,8 +24,11 @@ "INSTFLAGS": [ "--remove-function-body prvSingleStepTCPHeaderOptions", - "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPHandleState|vTCPStateChange|xSequenceGreaterThan|prvCheckOptions|prvTCPPrepareSend|xSequenceLessThan|xTCPWindowTxHasData|xTaskGetTickCount|prvTCPReturnPacket'", - "--generate-function-body-options nondet-return" + "--remove-function-body prvCheckOptions", + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket", + "--remove-function-body prvTCPHandleState", + "--remove-function-body vTCPStateChange" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json index f5d271f73..53a28f733 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json @@ -22,9 +22,7 @@ "--remove-function-body prvTCPPrepareSend", "--remove-function-body prvTCPReturnPacket", "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange", - "--generate-function-body 'xProcessReceivedTCPPacket_IPV6'", - "--generate-function-body-options nondet-return" + "--remove-function-body vTCPStateChange" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json index 06bef8c3c..bc0bc61db 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -8,11 +8,6 @@ "--unwind 1", "--nondet-static" ], - "INSTFLAGS": - [ - "--generate-function-body 'vARPRefreshCacheEntryAge'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json index 7a7dcbbab..9645ee00a 100644 --- a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json +++ b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json @@ -9,17 +9,15 @@ "--unwindset prvPrepareExtensionHeaders.0:{MAX_EXT_HEADER_NUM}", "--flush" ], - "INSTFLAGS": - [ - "--generate-function-body 'xGetExtensionOrder'", - "--generate-function-body-options nondet-return" - ], "OBJS": [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Utils.goto" ], + "INSTFLAGS": + [ + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index 04c2b7fa3..429d78734 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -226,18 +226,6 @@ def add_proof_jobs(proof_directory, proof_root): "--description", ("%s: computing coverage" % proof_name), ], check=True) - # Check whether the CBMC proof doesn't have undefined functions. - # More details in the Makefile rule for check-cbmc-undefined-functions. - run_cmd([ - "litani", "add-job", - "--command", "make check-cbmc-undefined-functions", - "--inputs", cbmc_out, - "--pipeline-name", proof_name, - "--ci-stage", "report", - "--cwd", str(proof_directory), - "--description", ("%s: checking for undefined functions" % proof_name), - ], check=True) - # Check whether the CBMC proof actually passed. More details in the # Makefile rule for check-cbmc-result. run_cmd([ From f290fef9ce2f081e84f0f51cb7c0cbac5daaaacd Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 May 2024 14:55:20 +0530 Subject: [PATCH 3/4] CBMC enhancements --- test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json | 5 +++++ .../proofs/ARP/ARPGetCacheEntry/Configurations.json | 5 +++++ test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json | 5 +++++ test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json | 5 +++++ .../Configurations.json | 5 +++++ .../Configurations.json | 5 +++++ .../Configurations.json | 5 +++++ test/cbmc/proofs/CheckOptionsInner/Makefile.json | 5 +++++ test/cbmc/proofs/CheckOptionsOuter/Makefile.json | 5 +++++ test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json | 5 +++++ .../proofs/DHCP/DHCPProcessEndPoint/Makefile.json | 5 +++++ test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json | 3 ++- .../proofs/DHCPv6/DHCPv6HandleOption/Makefile.json | 5 ++--- test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json | 5 +++++ test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json | 5 +++++ test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json | 5 +++++ test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json | 6 +++++- .../cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json | 5 +++++ .../proofs/DNS/DNSgetHostByName_cancel/Makefile.json | 5 +++++ .../proofs/DNS/prepareReplyDNSMessage/Makefile.json | 5 +++++ .../proofs/IP/ProcessEthernetPacket/Makefile.json | 5 +++++ test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json | 5 +++++ .../IPUtils/usGenerateProtocolChecksum/Makefile.json | 3 ++- .../usGenerateProtocolChecksum_IPv6/Makefile.json | 3 ++- test/cbmc/proofs/Makefile.template | 11 +++++++++++ .../ND/prvProcessICMPMessage_IPv6/Makefile.json | 5 +++++ test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json | 5 +++++ test/cbmc/proofs/RA/vReceiveRA/Makefile.json | 5 +++++ .../proofs/RA/vReceiveRA_ReadReply/Makefile.json | 5 +++++ .../proofs/Routing/MatchingEndpoint/Makefile.json | 5 +++++ test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json | 5 +++++ .../Makefile.json | 2 ++ .../proofs/Socket/vSocketClose/Configurations.json | 5 +++++ test/cbmc/proofs/TCP/prvHandleListen/Makefile.json | 9 +++++---- .../proofs/TCP/prvHandleListen_IPv6/Makefile.json | 9 +++++---- test/cbmc/proofs/TCP/prvSendData/Makefile.json | 5 +++++ test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json | 11 ++++++----- test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json | 5 +++++ .../cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json | 5 +++++ .../proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json | 5 +++++ .../UDP/vProcessGeneratedUDPPacket/Makefile.json | 5 +++++ .../parsing/ProcessIPPacket/Configurations.json | 5 +++++ .../parsing/ProcessReceivedTCPPacket/Makefile.json | 7 ++----- .../ProcessReceivedTCPPacket_IPv6/Makefile.json | 4 +++- .../parsing/ProcessReceivedUDPPacket/Makefile.json | 5 +++++ test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json | 8 +++++--- test/cbmc/proofs/run-cbmc-proofs.py | 12 ++++++++++++ 47 files changed, 229 insertions(+), 29 deletions(-) diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json index 24de2ff3c..a1c285c45 100644 --- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json index aa4d60296..7d34c97db 100644 --- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json index 00079ded1..9766e9975 100644 --- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json index f069f5959..f11e5145d 100644 --- a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json index 62bb3e052..e8e8bb1b6 100644 --- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json index e243382c3..e235e6794 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json index 5b2cdd30d..169ed87d8 100644 --- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json +++ b/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", diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index a902bcc94..3a9dbd15c 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json index d97be23e6..f6e26cc8e 100644 --- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json index 99e79d3b2..08ec0c8bc 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json index ed7497613..34f33b5a1 100644 --- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json index 08e8432de..47d64f298 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json +++ b/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": diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json index 09859a60b..0b9e6d05d 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json +++ b/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": [ diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json index 40839470b..d2480b5e7 100644 --- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json +++ b/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" diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json index 27864b146..fa08c7798 100644 --- a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json +++ b/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": [ ] diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json index 458443eb7..1ba42ffb1 100644 --- a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json +++ b/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}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json index 66b7cad54..a48a0c657 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json @@ -36,7 +36,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], - + "INSTFLAGS": + [ + "--generate-function-body 'Prepare_CacheLookup|vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|xApplicationGetRandomNumber|FreeRTOS_ReleaseUDPPayloadBuffer|FreeRTOS_inet_addr'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_IPv6=1", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json index f67cb0a11..cc4f09d8d 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -30,6 +30,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|DNS_BindSocket|DNS_SendRequest|xApplicationGetRandomNumber|vDNSSetCallBack|ulChar2u32|DNS_CloseSocket|DNS_ReadReply|FreeRTOS_inet_addr'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json index 8f568fb54..0a2ba1425 100644 --- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json +++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -19,6 +19,11 @@ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto", "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vDNSCallbackInitialise|vDNSSetCallBack|vDNSCheckCallBack'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigDNS_USE_CALLBACKS={callback}", diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json index f4f366afb..9e30a765a 100644 --- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json +++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json @@ -13,6 +13,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'uxIPHeaderSizePacket'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_DNS_CACHE={USE_CACHE}", diff --git a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json index 4a2b35b44..641cc8bdf 100644 --- a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json +++ b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json @@ -4,6 +4,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|vIPTimerStartARPResolution'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json index 30727432c..09c6c52c6 100644 --- a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json +++ b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json @@ -32,6 +32,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'uxQueueMessagesWaiting|vIPSetTCPTimerExpiredState|xIsCallingFromIPTask|xQueueGenericSend'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json index dc882f519..98b83571d 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum/Makefile.json @@ -7,7 +7,8 @@ ], "INSTFLAGS": [ - "--remove-function-body prvChecksumIPv6Checks" + "--generate-function-body 'prvChecksumIPv6Checks'", + "--generate-function-body-options nondet-return" ], "OBJS": [ diff --git a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json index ddf4febda..5cb256237 100644 --- a/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json +++ b/test/cbmc/proofs/IPUtils/usGenerateProtocolChecksum_IPv6/Makefile.json @@ -10,7 +10,8 @@ ], "INSTFLAGS": [ - "--remove-function-body prvChecksumIPv4Checks" + "--generate-function-body 'prvChecksumIPv4Checks'", + "--generate-function-body-options nondet-return" ], "OBJS": [ diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 094fd560c..6466adae5 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -150,6 +150,17 @@ report: cbmc.xml property.xml coverage.xml check-cbmc-result: cbmc.xml grep 'SUCCESS' $^ +# This rule depends only on cbmc.xml and has no dependents, so it will +# not block the report from being generated if it fails. This rule is +# intended to fail if and only if the CBMC safety check that emits +# cbmc.xml yielded a warning about undefined functions. +check-cbmc-undefined-functions: cbmc.xml + if grep '**** WARNING: no body for function' $^; then \ + exit 1; \ + else \ + exit 0; \ + fi + # ____________________________________________________________________ # Rules # diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json index 09f7d0beb..f6275dca3 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json @@ -5,6 +5,11 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json index cdc3a4f0a..b746a4b5c 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json @@ -5,6 +5,11 @@ "--unwindset vNDRefreshCacheEntry.0:25", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|uxIPHeaderSizePacket|vIPSetARPResolutionTimerEnableState|vReceiveRA'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json index 8b995fc8d..89b4b6bac 100644 --- a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json @@ -6,6 +6,11 @@ "--unwindset FreeRTOS_NextEndPoint.0:1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vDHCP_RATimerReload|vNDSendNeighbourSolicitation|FreeRTOS_CreateIPv6Address'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json index 61d93b3d5..c863c6b8e 100644 --- a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json +++ b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json @@ -5,6 +5,11 @@ "--unwind 3", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'ulChar2u32'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json index 3c235d92b..38f05ea32 100644 --- a/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json +++ b/test/cbmc/proofs/Routing/MatchingEndpoint/Makefile.json @@ -6,6 +6,11 @@ "--unwindset pxEasyFit.0:{MAX_ENDPOINT_COUNT_LOOP}", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'xIsIPv6Loopback'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json index 6a4799f87..04dd1bb4d 100644 --- a/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json +++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/Makefile.json @@ -4,6 +4,11 @@ [ "--unwind 1" ], + "INSTFLAGS": + [ + "--generate-function-body 'vTCPStateChange|xSendEventToIPTask|uxStreamBufferAdd|uxStreamBufferFrontSpace'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json index 379ae7a39..013b864fb 100644 --- a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json +++ b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json @@ -17,6 +17,8 @@ ], "INSTFLAGS": [ + "--generate-function-body 'vTaskSuspendAll|xTaskResumeAll'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json index 50df09417..e97e737b7 100644 --- a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json +++ b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json @@ -5,6 +5,11 @@ [ "--unwind 2" ], + "INSTFLAGS": + [ + "--generate-function-body 'vEventGroupDelete|xEventGroupCreate'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto", diff --git a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json index 856e50c30..85fc8b13b 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json @@ -5,6 +5,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress|ulApplicationGetNextSequenceNumber'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", @@ -17,10 +22,6 @@ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPSendReset" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json index aa1ee4f70..13eab4922 100644 --- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json @@ -14,15 +14,16 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv6.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'prvSocketSetMSS|vSocketBind|prvTCPSendReset|vTCPStateChange|xApplicationGetRandomNumber|prvTCPCreateWindow|vSocketClose|FreeRTOS_GetLocalAddress'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "FREERTOS_TCP_ENABLE_VERIFICATION", "ipconfigNETWORK_MTU=586" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPSendReset" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvSendData/Makefile.json b/test/cbmc/proofs/TCP/prvSendData/Makefile.json index cfc73e67e..bab3bf136 100644 --- a/test/cbmc/proofs/TCP/prvSendData/Makefile.json +++ b/test/cbmc/proofs/TCP/prvSendData/Makefile.json @@ -5,6 +5,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|uxIPHeaderSizeSocket|prvTCPReturnPacket_IPV4'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json index a192cca2d..07948b1fb 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json @@ -46,17 +46,18 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPReturnPacket", + "--generate-function-body 'ulTCPWindowTxAck|prvTCPAddTxData|prvSetSynAckOptions|lTCPWindowRxCheck|vTaskSuspendAll|xTCPWindowTxDone|xTaskResumeAll|uxStreamBufferGet|prvSetOptions|lTCPAddRxdata|uxStreamBufferGetSpace|vTCPWindowInit|prvTCPSendReset|xTCPWindowRxEmpty|vSocketClose|xTaskGetTickCount|vSocketWakeUpUser|prvTCPPrepareSend|FreeRTOS_inet_ntop|FreeRTOS_listen|prvSendData'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", "FREERTOS_TCP_ENABLE_VERIFICATION" ], - "INSTFLAGS": - [ - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket" - ], "INC": [ "$(FREERTOS_PLUS_TCP)/test/cbmc/include" diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json index 97cbf2b02..b3bed0caf 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -33,6 +33,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|xTCPWindowTxDone|vTaskSuspendAll|xTaskResumeAll|vSocketWakeUpUser|uxStreamBufferDistance|uxStreamBufferGet|vSocketClose|ulTCPWindowTxGet|FreeRTOS_listen|xTaskGetTickCount|prvTCPSocketIsActive'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json index 1b67f5a07..c0610595d 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -43,6 +43,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv4.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV6|FreeRTOS_min_uint32'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json index 9b28c3b34..a4b420e84 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json @@ -15,6 +15,11 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], + "INSTFLAGS": + [ + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPReturnPacket_IPV4|eNDGetCacheEntry|FreeRTOS_min_uint32'", + "--generate-function-body-options nondet-return" + ], "DEF": [ "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json index f7ef2a84d..9ca86c95b 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json @@ -3,6 +3,11 @@ "CBMCFLAGS": [ ], + "INSTFLAGS": + [ + "--generate-function-body 'vProcessGeneratedUDPPacket_IPv6'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json index 1ef122113..40ca60609 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/Configurations.json @@ -7,6 +7,11 @@ "--unwindset FreeRTOS_AllEndPointsUp.0:2", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'xGetExtensionOrder|vNDRefreshCacheEntry|ProcessICMPPacket|xCheckRequiresARPResolution|vARPRefreshCacheEntryAge|eHandleIPv6ExtensionHeaders|prvAllowIPPacketIPv6|FreeRTOS_FindEndPointOnIP_IPv4|prvProcessICMPMessage_IPv6'", + "--generate-function-body-options nondet-return" + ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json index f2643c9b9..6ceb92875 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -24,11 +24,8 @@ "INSTFLAGS": [ "--remove-function-body prvSingleStepTCPHeaderOptions", - "--remove-function-body prvCheckOptions", - "--remove-function-body prvTCPPrepareSend", - "--remove-function-body prvTCPReturnPacket", - "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" + "--generate-function-body 'vReleaseNetworkBufferAndDescriptor|prvTCPHandleState|vTCPStateChange|xSequenceGreaterThan|prvCheckOptions|prvTCPPrepareSend|xSequenceLessThan|xTCPWindowTxHasData|xTaskGetTickCount|prvTCPReturnPacket'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json index 53a28f733..f5d271f73 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json @@ -22,7 +22,9 @@ "--remove-function-body prvTCPPrepareSend", "--remove-function-body prvTCPReturnPacket", "--remove-function-body prvTCPHandleState", - "--remove-function-body vTCPStateChange" + "--remove-function-body vTCPStateChange", + "--generate-function-body 'xProcessReceivedTCPPacket_IPV6'", + "--generate-function-body-options nondet-return" ], "DEF": [ diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json index bc0bc61db..06bef8c3c 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -8,6 +8,11 @@ "--unwind 1", "--nondet-static" ], + "INSTFLAGS": + [ + "--generate-function-body 'vARPRefreshCacheEntryAge'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", diff --git a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json index 9645ee00a..7a7dcbbab 100644 --- a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json +++ b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json @@ -9,15 +9,17 @@ "--unwindset prvPrepareExtensionHeaders.0:{MAX_EXT_HEADER_NUM}", "--flush" ], + "INSTFLAGS": + [ + "--generate-function-body 'xGetExtensionOrder'", + "--generate-function-body-options nondet-return" + ], "OBJS": [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Utils.goto" ], - "INSTFLAGS": - [ - ], "OPT": [ "--export-file-local-symbols" diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index 429d78734..04c2b7fa3 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -226,6 +226,18 @@ def add_proof_jobs(proof_directory, proof_root): "--description", ("%s: computing coverage" % proof_name), ], check=True) + # Check whether the CBMC proof doesn't have undefined functions. + # More details in the Makefile rule for check-cbmc-undefined-functions. + run_cmd([ + "litani", "add-job", + "--command", "make check-cbmc-undefined-functions", + "--inputs", cbmc_out, + "--pipeline-name", proof_name, + "--ci-stage", "report", + "--cwd", str(proof_directory), + "--description", ("%s: checking for undefined functions" % proof_name), + ], check=True) + # Check whether the CBMC proof actually passed. More details in the # Makefile rule for check-cbmc-result. run_cmd([ From 5ce74cf40483b4436de49f65e5753d88173635f4 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 9 May 2024 12:43:37 +0530 Subject: [PATCH 4/4] Add back deleted files --- .../DHCPv6/SendDHCPMessage/Makefile.json | 28 ++++++++ .../SendDHCPMessage/SendDHCPMessage_harness.c | 69 +++++++++++++++++++ .../proofs/ProcessDHCPReplies/Makefile.json | 56 +++++++++++++++ .../ProcessDHCPReplies_harness.c | 43 ++++++++++++ 4 files changed, 196 insertions(+) create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json create mode 100644 test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c create mode 100644 test/cbmc/proofs/ProcessDHCPReplies/Makefile.json create mode 100644 test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json new file mode 100644 index 000000000..524738820 --- /dev/null +++ b/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" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c new file mode 100644 index 000000000..05f24cb27 --- /dev/null +++ b/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 + +/* 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 ); +} diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json new file mode 100644 index 000000000..4bdca6f7c --- /dev/null +++ b/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}" + ] +} diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 000000000..f43404c28 --- /dev/null +++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,43 @@ +/* Standard includes. */ +#include + +/* 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 ); +}