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/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 9ed192b172..ada3510b2c 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -2,11 +2,17 @@ "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": [ "$(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 +21,6 @@ ], "DEF": [ + "ipconfigUSE_TCP=1" ] } 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..199d032716 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,13 @@ 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 ) ); + /* 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/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..19f782f675 100644 --- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -62,12 +62,24 @@ 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 ) ); + pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + pxSocket->u.xTCP.pxPeerSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); size_t socketSize = sizeof( FreeRTOS_Socket_t ); - size_t bufferSize = sizeof( TCPPacket_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 ) ) ) { 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": [ 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"