Skip to content

Fixes for FreeRTOS proof errors. #4

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

Open
AmPaschal wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Fixes for FreeRTOS proof errors. #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0d57715
Fixes for FreeRTOS proof errors.
AmPaschal Apr 15, 2025
902d3a4
Added more comments
AmPaschal Apr 15, 2025
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
16 changes: 13 additions & 3 deletions test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
{
uint16_t usReturn;

// BUG: This assertion is violated by this proof. This may be a real bug in the calling function or just an overly constrained assertion.
__CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "Data must be valid" );

/* Return an indeterminate value. */
Expand All @@ -131,11 +132,17 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ
{
NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );

if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
// BUG: Changed this condition because the previous version reported an assertion
if( pxNetworkBuffer != NULL )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength );
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
pxNetworkBuffer->xDataLength = xNewLength;

// Added this to resolve a null pointer violation in a location where pxEndPoint was used.
// This may be a real NULL pointer dereferencing bug if pxEndpoint can be NULL.
pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
__CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
}

return pxNetworkBuffer;
Expand All @@ -147,6 +154,7 @@ void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer,
{
__CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" );
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" );
// BUG: This assertion is violated by this proof. This may be a real bug in the calling function or just an overly constrained assertion.
__CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" );
}

Expand Down Expand Up @@ -180,7 +188,9 @@ void harness()
"TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" );

__CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE );
// BUG: Removing this assumption because TEST_PACKET_SIZE is only 29 bytes.
// With this assumption, the target function is never verified.
// __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE );

lIsIPv6Packet = IS_TESTING_IPV6;

Expand Down
9 changes: 7 additions & 2 deletions test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,8 @@ void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
uint32_t ulLen,
BaseType_t xReleaseAfterSend )
{
// BUG: xProcessReceivedTCPPacket calls this prvTCPReturnPacket function with pxSocket being NULL.
// This causes this assertion to be violated.
__CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
__CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
__CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
Expand Down Expand Up @@ -151,7 +153,8 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
if( pxNetworkBuffer )
{
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes );
__CPROVER_assume( pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof( int32_t ) );
// BUG: The previous version fixed the xDataLength value, preventing code coverage.
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
}

return pxNetworkBuffer;
Expand All @@ -174,8 +177,10 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
void harness()
{
NetworkBufferDescriptor_t * pxNetworkBuffer;
// BUG: We need to make the size of input packet nondeterministic.
size_t tcpPacketSize;

pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 );
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 );

/* To avoid asserting on the network buffer being NULL. */
__CPROVER_assume( pxNetworkBuffer != NULL );
Expand Down