Skip to content
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

Jump to bottom

Remove all instances of mallocCanFail #119

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Remove all instances of mallocCanFail #119

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
5 changes: 5 additions & 0 deletions source/core_http_client.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1727,6 +1727,11 @@ HTTPStatus_t HTTPClient_AddRangeHeader( HTTPRequestHeaders_t * pRequestHeaders,
LogError( ( "Parameter check failed: pRequestHeaders->pBuffer is NULL." ) );
returnStatus = HTTPInvalidParameter;
}
else if( pRequestHeaders->bufferLen > UINT32_MAX )
{
LogError( ( "Parameter check failed: pRequestHeaders->bufferLen > UINT32_MAX." ) );
returnStatus = HTTPInvalidParameter;
}
else if( pRequestHeaders->headersLen > pRequestHeaders->bufferLen )
{
LogError( ( "Parameter check failed: pRequestHeaders->headersLen > pRequestHeaders->bufferLen." ) );
Expand Down
13 changes: 0 additions & 13 deletions test/cbmc/include/http_cbmc_state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,19 +46,6 @@ struct NetworkContext
*/
bool nondet_bool();

/**
* @brief Calls malloc based on given size or returns NULL for coverage.
*
* Implementation of safe malloc which returns NULL if the requested size is 0.
* The behavior of malloc(0) is platform dependent.
* It is possible for malloc(0) to return an address without allocating memory.
*
* @param[in] size Requested size to malloc.
*
* @return Requested memory or NULL.
*/
void * mallocCanFail( size_t size );

/**
* @brief Allocates an #HTTPRequestHeaders_t object.
*
Expand Down
6 changes: 2 additions & 4 deletions test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,12 +42,10 @@ void HTTPClient_AddHeader_harness()
__CPROVER_assume( isValidHttpRequestHeaders( pRequestHeaders ) );

/* Initialize and make assumptions for header field. */
__CPROVER_assume( fieldLen < CBMC_MAX_OBJECT_SIZE );
pField = mallocCanFail( fieldLen );
pField = malloc( fieldLen );

/* Initialize and make assumptions for header value. */
__CPROVER_assume( valueLen < CBMC_MAX_OBJECT_SIZE );
pValue = mallocCanFail( valueLen );
pValue = malloc( valueLen );

HTTPClient_AddHeader( pRequestHeaders,
pField, fieldLen, pValue, valueLen );
Expand Down
6 changes: 2 additions & 4 deletions test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,10 @@ void HTTPClient_ReadHeader_harness()
size_t valueLen;

/* Initialize and make assumptions for header field. */
__CPROVER_assume( fieldLen < CBMC_MAX_OBJECT_SIZE );
pField = mallocCanFail( fieldLen );
pField = malloc( fieldLen );

/* Initialize and make assumptions for header value. */
__CPROVER_assume( valueLen < CBMC_MAX_OBJECT_SIZE );
pValue = mallocCanFail( sizeof( char * ) );
pValue = malloc( sizeof( char * ) );

/* Initialize and make assumptions for response object. */
pResponse = allocateHttpResponse( NULL );
Expand Down
3 changes: 1 addition & 2 deletions test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,7 @@ void HTTPClient_Send_harness()
__CPROVER_assume( isValidHttpRequestHeaders( pRequestHeaders ) );

/* Initialize and make assumptions for buffer to receive request body. */
__CPROVER_assume( reqBodyBufLen < CBMC_MAX_OBJECT_SIZE );
pRequestBodyBuf = mallocCanFail( reqBodyBufLen );
pRequestBodyBuf = malloc( reqBodyBufLen );

/* Initialize and make assumptions for response object. */
pResponse = allocateHttpResponse( NULL );
Expand Down
1 change: 0 additions & 1 deletion test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,6 @@ void findHeaderFieldParserCallback_harness()
__CPROVER_assume( fieldOffset <= pResponse->bufferLen - fieldLen );
pFieldLoc = pResponse->pBuffer + fieldOffset;

__CPROVER_assume( 0 < fieldContextLen && fieldContextLen < CBMC_MAX_OBJECT_SIZE );
pFindHeaderContext->pField = ( char * ) malloc( fieldContextLen );
__CPROVER_assume( pFindHeaderContext->pField != NULL );
pFindHeaderContext->fieldLen = fieldContextLen;
Expand Down
55 changes: 11 additions & 44 deletions test/cbmc/sources/http_cbmc_state.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,23 +29,16 @@

#include "http_cbmc_state.h"

void * mallocCanFail( size_t size )
{
__CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "mallocCanFail size is too big" );
return malloc( size );
}

HTTPRequestHeaders_t * allocateHttpRequestHeaders( HTTPRequestHeaders_t * pRequestHeaders )
{
if( pRequestHeaders == NULL )
{
pRequestHeaders = mallocCanFail( sizeof( HTTPRequestHeaders_t ) );
pRequestHeaders = malloc( sizeof( HTTPRequestHeaders_t ) );
}

if( pRequestHeaders != NULL )
{
__CPROVER_assume( pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE );
pRequestHeaders->pBuffer = mallocCanFail( pRequestHeaders->bufferLen );
pRequestHeaders->pBuffer = malloc( pRequestHeaders->bufferLen );
}

return pRequestHeaders;
Expand All @@ -54,33 +47,21 @@ HTTPRequestHeaders_t * allocateHttpRequestHeaders( HTTPRequestHeaders_t * pReque
bool isValidHttpRequestHeaders( const HTTPRequestHeaders_t * pRequestHeaders )
{
bool isValid = true;

if( pRequestHeaders )
{
isValid = pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE &&
pRequestHeaders->headersLen < CBMC_MAX_OBJECT_SIZE;
}

return isValid;
}

HTTPRequestInfo_t * allocateHttpRequestInfo( HTTPRequestInfo_t * pRequestInfo )
{
if( pRequestInfo == NULL )
{
pRequestInfo = mallocCanFail( sizeof( HTTPRequestInfo_t ) );
pRequestInfo = malloc( sizeof( HTTPRequestInfo_t ) );
}

if( pRequestInfo != NULL )
{
__CPROVER_assume( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE );
pRequestInfo->pMethod = mallocCanFail( pRequestInfo->methodLen );

__CPROVER_assume( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE );
pRequestInfo->pHost = mallocCanFail( pRequestInfo->hostLen );

__CPROVER_assume( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
pRequestInfo->pPath = mallocCanFail( pRequestInfo->pathLen );
pRequestInfo->pMethod = malloc( pRequestInfo->methodLen );
pRequestInfo->pHost = malloc( pRequestInfo->hostLen );
pRequestInfo->pPath = malloc( pRequestInfo->pathLen );
}

return pRequestInfo;
Expand All @@ -89,14 +70,6 @@ HTTPRequestInfo_t * allocateHttpRequestInfo( HTTPRequestInfo_t * pRequestInfo )
bool isValidHttpRequestInfo( const HTTPRequestInfo_t * pRequestInfo )
{
bool isValid = true;

if( pRequestInfo )
{
isValid = ( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE ) &&
( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE ) &&
( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
}

return isValid;
}

Expand All @@ -106,13 +79,12 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )

if( pResponse == NULL )
{
pResponse = mallocCanFail( sizeof( HTTPResponse_t ) );
pResponse = malloc( sizeof( HTTPResponse_t ) );
}

if( pResponse != NULL )
{
__CPROVER_assume( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE );
pResponse->pBuffer = mallocCanFail( pResponse->bufferLen );
pResponse->pBuffer = malloc( pResponse->bufferLen );

__CPROVER_assume( headerOffset <= pResponse->bufferLen );

Expand Down Expand Up @@ -163,8 +135,7 @@ bool isValidHttpResponse( const HTTPResponse_t * pResponse )

if( pResponse )
{
isValid = ( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE ) &&
( pResponse->bodyLen < pResponse->bufferLen ) &&
isValid = ( pResponse->bodyLen < pResponse->bufferLen ) &&
( pResponse->headersLen < pResponse->bufferLen );
isValid = isValid || pResponse->pBody == NULL;
}
Expand All @@ -176,12 +147,12 @@ TransportInterface_t * allocateTransportInterface( TransportInterface_t * pTrans
{
if( pTransport == NULL )
{
pTransport = mallocCanFail( sizeof( TransportInterface_t ) );
pTransport = malloc( sizeof( TransportInterface_t ) );
}

if( pTransport != NULL )
{
pTransport->pNetworkContext = mallocCanFail( sizeof( NetworkContext_t ) );
pTransport->pNetworkContext = malloc( sizeof( NetworkContext_t ) );
}

return pTransport;
Expand Down Expand Up @@ -244,10 +215,6 @@ HTTPParsingContext_t * allocateHttpSendParsingContext( HTTPParsingContext_t * pH
bool isValidHttpSendParsingContext( const HTTPParsingContext_t * pHttpParsingContext )
{
bool isValid = true;

isValid = isValid && ( pHttpParsingContext->lastHeaderFieldLen ) <= ( SIZE_MAX - CBMC_MAX_OBJECT_SIZE );
isValid = isValid && ( pHttpParsingContext->lastHeaderValueLen ) <= ( SIZE_MAX - CBMC_MAX_OBJECT_SIZE );

return isValid;
}

Expand Down
2 changes: 0 additions & 2 deletions test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,8 +54,6 @@ size_t http_parser_execute( http_parser * parser,
"http_parser_execute settings is NULL" );
__CPROVER_assert( data != NULL,
"http_parser_execute data is NULL" );
__CPROVER_assert( len < CBMC_MAX_OBJECT_SIZE,
"http_parser_execute len >= CBMC_MAX_OBJECT_SIZE" );

parser->http_errno = http_errno;

Expand Down
2 changes: 0 additions & 2 deletions test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,6 @@ size_t http_parser_execute( http_parser * parser,
"http_parser_execute settings is NULL" );
__CPROVER_assert( data != NULL,
"http_parser_execute data is NULL" );
__CPROVER_assert( len < CBMC_MAX_OBJECT_SIZE,
"http_parser_execute len >= CBMC_MAX_OBJECT_SIZE" );

__CPROVER_assume( fieldLength <= len );
__CPROVER_assume( valueLength <= len );
Expand Down