From 9d553d03427667359c78714de30d2aadc9a001b2 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 13 Jan 2023 17:42:24 +0000 Subject: [PATCH 1/8] Use CBMC XML output to enable VSCode debugger (#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle --- test/cbmc/proofs/Makefile.template | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 375c15c120..094fd560c1 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -119,8 +119,8 @@ goto: # Ignore the return code for CBMC, so that we can still generate the # report if the proof failed. If the proof failed, we separately fail # the entire job using the check-cbmc-result rule. -cbmc.txt: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 +cbmc.xml: $(ENTRY).goto + -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 @@ -128,29 +128,27 @@ property.xml: $(ENTRY).goto coverage.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 -cbmc: cbmc.txt +cbmc: cbmc.xml property: property.xml coverage: coverage.xml -report: cbmc.txt property.xml coverage.xml +report: cbmc.xml property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS_PLUS_TCP) \ - --blddir $(FREERTOS_PLUS_TCP) \ - --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ - --result cbmc.txt \ + --reportdir report \ + --result cbmc.xml \ --property property.xml \ - --block coverage.xml + --coverage coverage.xml -# This rule depends only on cbmc.txt and has no dependents, so it will +# 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.txt yielded a proof failure. -check-cbmc-result: cbmc.txt - grep -e "^VERIFICATION SUCCESSFUL" $^ +# cbmc.xml yielded a proof failure. +check-cbmc-result: cbmc.xml + grep 'SUCCESS' $^ # ____________________________________________________________________ # Rules @@ -160,7 +158,7 @@ check-cbmc-result: cbmc.txt clean: @RM@ $(OBJS) $(ENTRY).goto @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt - @RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* + @RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-* @RM@ *~ \#* @RM@ queue_datastructure.h From 1e0086822bea5e672b99c603f0342ff8f9abb7b0 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 11:52:01 +0000 Subject: [PATCH 2/8] fix the CBMC proof build and fail due to non inclusion of actaul src files --- source/FreeRTOS_TCP_IP.c | 2 +- test/cbmc/patches/FreeRTOSConfig.h | 2 +- test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json | 1 + .../proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c | 7 ++++++- test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json | 3 ++- .../proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c | 3 ++- test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json | 3 ++- 7 files changed, 15 insertions(+), 6 deletions(-) diff --git a/source/FreeRTOS_TCP_IP.c b/source/FreeRTOS_TCP_IP.c index b3936dc1ec..5762f4d8ef 100644 --- a/source/FreeRTOS_TCP_IP.c +++ b/source/FreeRTOS_TCP_IP.c @@ -86,7 +86,7 @@ /* MISRA Ref 8.9.1 [File scoped variables] */ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-89 */ /* coverity[misra_c_2012_rule_8_9_violation] */ - static FreeRTOS_Socket_t * xSocketToListen = NULL; + _static FreeRTOS_Socket_t * xSocketToListen = NULL; #if ( ipconfigHAS_DEBUG_PRINTF != 0 ) diff --git a/test/cbmc/patches/FreeRTOSConfig.h b/test/cbmc/patches/FreeRTOSConfig.h index e3ed1f8ad5..7e61af32f1 100644 --- a/test/cbmc/patches/FreeRTOSConfig.h +++ b/test/cbmc/patches/FreeRTOSConfig.h @@ -127,7 +127,7 @@ * is set to 2 so the formatting functions are included without the stdio.h being * included in tasks.c. That is because this project defines its own sprintf() * functions. */ -#define configUSE_STATS_FORMATTING_FUNCTIONS 1 +#define configUSE_STATS_FORMATTING_FUNCTIONS 0 /* Assert call defined for debug builds. */ extern void vAssertCalled( const char * pcFile, diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json index 8b415eafab..7f898c6162 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json @@ -40,6 +40,7 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c index 801b2c2687..d49300c726 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -37,6 +37,8 @@ #include "../../utility/memory_assignments.c" +extern FreeRTOS_Socket_t * xSocketToListen; + /* Abstraction of xTaskGetCurrentTaskHandle */ TaskHandle_t xTaskGetCurrentTaskHandle( void ) { @@ -86,9 +88,12 @@ void harness() NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); size_t bufferSize = sizeof( NetworkBufferDescriptor_t ); + FreeRTOS_Socket_t xSck; + xSocketToListen = &xSck; + if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) ) { - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) ); + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + ipSIZE_OF_ETH_HEADER + uxIPHeaderSizeSocket( pxSocket ) + sizeof(TCPHeader_t) ); } if( ensure_memory_is_valid( pxSocket, socketSize ) && diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json index c1a102bef4..97cbf2b02d 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -37,7 +37,8 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], "DEF": [ diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index 34c59869ca..d3c2d71546 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -65,9 +65,10 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS void harness() { FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL ); NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); size_t socketSize = sizeof( FreeRTOS_Socket_t ); - size_t bufferSize = sizeof( TCPPacket_t ); + size_t bufferSize = sizeof( TCPPacket_t ) + ipSIZE_OF_ETH_HEADER + uxIPHeaderSizeSocket( pxSocket ) + sizeof( TCPHeader_t ) ; if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) { diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json index aac271e9d1..26b767489f 100644 --- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json +++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -39,7 +39,8 @@ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto" ], "DEF": [ From 4d87f4400bcc797b4a9052a813cf860a3d22a3d5 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 12:12:41 +0000 Subject: [PATCH 3/8] fix the CBMC proof build and fail due to non inclusion of actaul src files --- .../prvTCPPrepareSend/TCPPrepareSend_harness.c | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index d3c2d71546..830fe263d3 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -62,10 +62,23 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS return pxBuffer; } +/* Get rid of configASSERT in FreeRTOS_TCP_IP.c */ +BaseType_t xIsCallingFromIPTask( void ) +{ + return pdTRUE; +} + void harness() { - FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + __CPROVER_assume( pxSocket != NULL ); + pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume( pxSocket->u.xTCP.rxStream != NULL ); + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL ); + pxSocket->u.xTCP.pxPeerSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL ); + NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); size_t socketSize = sizeof( FreeRTOS_Socket_t ); size_t bufferSize = sizeof( TCPPacket_t ) + ipSIZE_OF_ETH_HEADER + uxIPHeaderSizeSocket( pxSocket ) + sizeof( TCPHeader_t ) ; From be91a96386660acaee76c1cc6bc058e8e7567a8f Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 12:42:18 +0000 Subject: [PATCH 4/8] adding tcp transmission v4 src to build --- test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json | 1 + 1 file changed, 1 insertion(+) diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json index f1d1331ff7..f77c5af428 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -14,6 +14,7 @@ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPV4.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Utils.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto" From 7450301805f315efa217c53ecc76ad0a8a786cf9 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 15:02:08 +0000 Subject: [PATCH 5/8] fix cbmc proof for CheckOptionsInner --- source/FreeRTOS_TCP_Reception.c | 4 ++-- test/cbmc/proofs/CheckOptionsInner/Makefile.json | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/source/FreeRTOS_TCP_Reception.c b/source/FreeRTOS_TCP_Reception.c index df9fb21790..7faa181e59 100644 --- a/source/FreeRTOS_TCP_Reception.c +++ b/source/FreeRTOS_TCP_Reception.c @@ -74,7 +74,7 @@ * Skip past TCP header options when doing Selective ACK, until there are no * more options left. */ - static void prvReadSackOption( const uint8_t * const pucPtr, + _static void prvReadSackOption( const uint8_t * const pucPtr, size_t uxIndex, FreeRTOS_Socket_t * const pxSocket ); #endif /* ( ipconfigUSE_TCP_WIN == 1 ) */ @@ -369,7 +369,7 @@ * @param[in] uxIndex: Index of options in the TCP packet options. * @param[in] pxSocket: Socket handling the TCP connection. */ - static void prvReadSackOption( const uint8_t * const pucPtr, + _static void prvReadSackOption( const uint8_t * const pucPtr, size_t uxIndex, FreeRTOS_Socket_t * const pxSocket ) { diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index 9ed192b172..d97245f73b 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -7,6 +7,7 @@ "OBJS": [ "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", @@ -15,5 +16,6 @@ ], "DEF": [ + "ipconfigUSE_TCP=1" ] } From 6749399ffdce8660cf26ee5b825ba986086613ac Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Tue, 14 Feb 2023 13:15:08 +0000 Subject: [PATCH 6/8] updating as per review comments --- source/FreeRTOS_TCP_Reception.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/source/FreeRTOS_TCP_Reception.c b/source/FreeRTOS_TCP_Reception.c index 7faa181e59..df9fb21790 100644 --- a/source/FreeRTOS_TCP_Reception.c +++ b/source/FreeRTOS_TCP_Reception.c @@ -74,7 +74,7 @@ * Skip past TCP header options when doing Selective ACK, until there are no * more options left. */ - _static void prvReadSackOption( const uint8_t * const pucPtr, + static void prvReadSackOption( const uint8_t * const pucPtr, size_t uxIndex, FreeRTOS_Socket_t * const pxSocket ); #endif /* ( ipconfigUSE_TCP_WIN == 1 ) */ @@ -369,7 +369,7 @@ * @param[in] uxIndex: Index of options in the TCP packet options. * @param[in] pxSocket: Socket handling the TCP connection. */ - _static void prvReadSackOption( const uint8_t * const pucPtr, + static void prvReadSackOption( const uint8_t * const pucPtr, size_t uxIndex, FreeRTOS_Socket_t * const pxSocket ) { From b1c4564f590f81389c8f8a94d24d272d6c67971a Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 15 Feb 2023 22:00:49 +0530 Subject: [PATCH 7/8] fix check option CBMC proofs --- .../CheckOptions/CheckOptions_harness.c | 35 ++++++++++++++++--- test/cbmc/proofs/CheckOptions/Makefile.json | 11 +++--- .../CheckOptionsInner_harness.c | 4 +-- .../proofs/CheckOptionsInner/Makefile.json | 7 +++- test/cbmc/proofs/MakefileCommon.json | 2 +- 5 files changed, 46 insertions(+), 13 deletions(-) diff --git a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c index 7e74803939..a01d256544 100644 --- a/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c +++ b/test/cbmc/proofs/CheckOptions/CheckOptions_harness.c @@ -24,8 +24,15 @@ * Signature of function under test ****************************************************************/ -BaseType_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvCheckOptions( FreeRTOS_Socket_t * pxSocket, - const NetworkBufferDescriptor_t * pxNetworkBuffer ); +BaseType_t prvCheckOptions( FreeRTOS_Socket_t * pxSocket, + const NetworkBufferDescriptor_t * pxNetworkBuffer ); + +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ); + +int32_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, + size_t uxTotalLength, + FreeRTOS_Socket_t * const pxSocket, + BaseType_t xHasSYNFlag ); /**************************************************************** * Declare the buffer size external to the harness so it can be @@ -33,12 +40,13 @@ BaseType_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvCheckOptions( FreeRTOS_Sock * give the buffer size an unconstrained value in the harness itself. ****************************************************************/ size_t buffer_size; +size_t uxIPHeaderSizePacket_uxResult; /**************************************************************** * Function contract proved correct by CheckOptionsOuter ****************************************************************/ -int32_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, +int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, size_t uxTotalLength, FreeRTOS_Socket_t * const pxSocket, BaseType_t xHasSYNFlag ) @@ -65,6 +73,14 @@ int32_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions( co return index; } +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +{ + + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer shouldnt be NULL" ); + return uxIPHeaderSizePacket_uxResult; + +} + /**************************************************************** * Proof of CheckOptions ****************************************************************/ @@ -74,6 +90,17 @@ void harness() /* Give buffer_size an unconstrained value */ size_t buf_size; + if(nondet_bool()) + { + uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv6_HEADER; + } + else + { + uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv4_HEADER; + } + + __CPROVER_assume( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) ); + buffer_size = buf_size; /* pxSocket can be any socket */ @@ -99,5 +126,5 @@ void harness() /* Buffer must be big enough to hold pxTCPPacket and pxTCPHeader */ __CPROVER_assume( buffer_size > 47 ); - __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvCheckOptions( &pxSocket, &pxNetworkBuffer ); + prvCheckOptions( &pxSocket, &pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/CheckOptions/Makefile.json b/test/cbmc/proofs/CheckOptions/Makefile.json index 3ef9e76211..49926c50af 100644 --- a/test/cbmc/proofs/CheckOptions/Makefile.json +++ b/test/cbmc/proofs/CheckOptions/Makefile.json @@ -3,12 +3,17 @@ "CBMCFLAGS": [ "--unwind 1", - " --unwindset __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvCheckOptions.0:41" + "--unwindset prvCheckOptions.0:41" + ], + "OPT": + [ + "--export-file-local-symbols" ], "OBJS": [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto", @@ -19,9 +24,5 @@ "DEF": [ "BUFFER_SIZE={BUFFER_SIZE}" - ], - "OPT": - [ - "--export-file-local-symbols" ] } diff --git a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c index b070dfce30..76d675b6b8 100644 --- a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c +++ b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -24,7 +24,7 @@ * Signature of function under test ****************************************************************/ -void prvReadSackOption( const uint8_t * const pucPtr, +void __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( const uint8_t * const pucPtr, size_t uxIndex, FreeRTOS_Socket_t * const pxSocket ); @@ -98,7 +98,7 @@ void harness() __CPROVER_assume( pucPtr != NULL ); __CPROVER_assume( pxSocket != NULL ); - prvReadSackOption( pucPtr, uxIndex, pxSocket ); + __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption( pucPtr, uxIndex, pxSocket ); /* No postconditions required */ } diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index d97245f73b..ada3510b2c 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -2,7 +2,12 @@ "ENTRY": "CheckOptionsInner", "CBMCFLAGS": [ "--unwind 1", - "--unwindset prvTCPWindowTxCheckAck.1:2,prvTCPWindowFastRetransmit.2:2" + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.1:2", + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.2:2" + ], + "OPT": + [ + "--export-file-local-symbols" ], "OBJS": [ diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json index ace4a5c352..7ada3e1dca 100644 --- a/test/cbmc/proofs/MakefileCommon.json +++ b/test/cbmc/proofs/MakefileCommon.json @@ -31,7 +31,7 @@ ], "CBMCFLAGS ": [ - "--object-bits 7", + "--object-bits 8", "--32", "--bounds-check", "--pointer-check" From 29878eb0ef9fbade7c1b039f8af60b68290012d6 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 15:10:22 +0530 Subject: [PATCH 8/8] removing unused assumptions --- .../proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c | 3 ++- .../proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c | 6 ++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c index d49300c726..199d032716 100644 --- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -93,7 +93,8 @@ void harness() if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) ) { - pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + ipSIZE_OF_ETH_HEADER + uxIPHeaderSizeSocket( pxSocket ) + sizeof(TCPHeader_t) ); + /* Allocates min. buffer size required for the proof */ + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ); } if( ensure_memory_is_valid( pxSocket, socketSize ) && diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index 830fe263d3..19f782f675 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -73,15 +73,13 @@ void harness() FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); __CPROVER_assume( pxSocket != NULL ); pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) ); - __CPROVER_assume( pxSocket->u.xTCP.rxStream != NULL ); pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); - __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL ); pxSocket->u.xTCP.pxPeerSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); - __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL ); NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); size_t socketSize = sizeof( FreeRTOS_Socket_t ); - size_t bufferSize = sizeof( TCPPacket_t ) + ipSIZE_OF_ETH_HEADER + uxIPHeaderSizeSocket( pxSocket ) + sizeof( TCPHeader_t ) ; + /* Allocates min. buffer size required for the proof */ + size_t bufferSize = sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ; if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) {