Skip to content

Fix build and proof failures for CBMC TCP proofs #710

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 13 commits into from
Feb 21, 2023
Merged

Fix build and proof failures for CBMC TCP proofs #710

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
9d553d0
Use CBMC XML output to enable VSCode debugger (#673)
karkhaz Jan 13, 2023
a3f9bc9
Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_tcp
tony-josi-aws Feb 9, 2023
14875c6
Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_tcp
tony-josi-aws Feb 11, 2023
1e00868
fix the CBMC proof build and fail due to non inclusion of actaul src …
tony-josi-aws Feb 13, 2023
4d87f44
fix the CBMC proof build and fail due to non inclusion of actaul src …
tony-josi-aws Feb 13, 2023
be91a96
adding tcp transmission v4 src to build
tony-josi-aws Feb 13, 2023
7450301
fix cbmc proof for CheckOptionsInner
tony-josi-aws Feb 13, 2023
6749399
updating as per review comments
tony-josi-aws Feb 14, 2023
b1c4564
fix check option CBMC proofs
tony-josi-aws Feb 15, 2023
29878eb
removing unused assumptions
tony-josi-aws Feb 17, 2023
a40c70b
Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_tcp
tony-josi-aws Feb 17, 2023
2fbe732
Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_tcp
tony-josi-aws Feb 21, 2023
c562d79
Merge branch 'dev/IPv6_integration' of github.com:FreeRTOS/FreeRTOS-P…
tony-josi-aws Feb 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion source/FreeRTOS_TCP_IP.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )

Expand Down
35 changes: 31 additions & 4 deletions test/cbmc/proofs/CheckOptions/CheckOptions_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,21 +24,29 @@
* 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
* accessed by the preconditions of prvSingleStepTCPHeaderOptions, and
* 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 )
Expand All @@ -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
****************************************************************/
Expand All @@ -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 */
Expand All @@ -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 );
}
11 changes: 6 additions & 5 deletions test/cbmc/proofs/CheckOptions/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -19,9 +24,5 @@
"DEF":
[
"BUFFER_SIZE={BUFFER_SIZE}"
],
"OPT":
[
"--export-file-local-symbols"
]
}
4 changes: 2 additions & 2 deletions test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down Expand Up @@ -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 */
}
9 changes: 8 additions & 1 deletion test/cbmc/proofs/CheckOptionsInner/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -15,5 +21,6 @@
],
"DEF":
[
"ipconfigUSE_TCP=1"
]
}
1 change: 1 addition & 0 deletions test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
8 changes: 7 additions & 1 deletion test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@

#include "../../utility/memory_assignments.c"

extern FreeRTOS_Socket_t * xSocketToListen;

/* Abstraction of xTaskGetCurrentTaskHandle */
TaskHandle_t xTaskGetCurrentTaskHandle( void )
{
Expand Down Expand Up @@ -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 ) &&
Expand Down
3 changes: 2 additions & 1 deletion test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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":
[
Expand Down
16 changes: 14 additions & 2 deletions test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Copy link
Member

@AniruddhaKanhere AniruddhaKanhere Feb 21, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This comment just tells me what is written in the code right below.

Ideally, comments should answer questions like why does the proof need exactly sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) and not just sizeof( TCPPacket_t ).

We could improve on these comments.

size_t bufferSize = sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) ;

if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) )
{
Expand Down
3 changes: 2 additions & 1 deletion test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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":
[
Expand Down
1 change: 1 addition & 0 deletions test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down