From 4795e1b592f61a1e475a509c1515b081986264f4 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 18 Oct 2021 11:00:44 -0400 Subject: [PATCH] Removes all instances of mallocCanFail from CBMC proofs Signed-off-by: Felipe R. Monteiro --- test/cbmc/include/mqtt_cbmc_state.h | 9 +- .../MQTT_Connect/MQTT_Connect_harness.c | 2 +- .../MQTT_DeserializeAck_harness.c | 5 +- .../MQTT_DeserializePublish_harness.c | 2 +- .../MQTT_GetPacketId_harness.c | 2 +- .../MQTT_GetSubAckStatusCodes_harness.c | 4 +- .../cbmc/proofs/MQTT_Init/MQTT_Init_harness.c | 10 +-- .../MQTT_MatchTopic/MQTT_MatchTopic_harness.c | 6 +- .../MQTT_SerializePublishHeader_harness.c | 2 +- test/cbmc/sources/mqtt_cbmc_state.c | 84 ++++--------------- 10 files changed, 34 insertions(+), 92 deletions(-) diff --git a/test/cbmc/include/mqtt_cbmc_state.h b/test/cbmc/include/mqtt_cbmc_state.h index 379935186..9526492e9 100644 --- a/test/cbmc/include/mqtt_cbmc_state.h +++ b/test/cbmc/include/mqtt_cbmc_state.h @@ -31,14 +31,7 @@ /* mqtt.h must precede including this header. */ -/** - * @brief Proof model for malloc that can fail and return NULL. - * - * @param[in] size The size in bytes of memory to allocate. - * - * @return NULL or requested memory. - */ -void * mallocCanFail( size_t size ); +#define IMPLIES( a, b ) ( !( a ) || ( b ) ) /** * @brief Allocate a #MQTTPacketInfo_t object. diff --git a/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c b/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c index 59ac9d3f6..1815bebb6 100644 --- a/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c +++ b/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c @@ -44,7 +44,7 @@ void harness() pWillInfo = allocateMqttPublishInfo( NULL ); __CPROVER_assume( isValidMqttPublishInfo( pWillInfo ) ); - pSessionPresent = mallocCanFail( sizeof( bool ) ); + pSessionPresent = malloc( sizeof( bool ) ); /* The MQTT_RECEIVE_TIMEOUT is used here to control the number of loops * when receiving on the network. The default is used here because memory diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c index 31f5caaa4..37ac9569d 100644 --- a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c +++ b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c @@ -35,10 +35,11 @@ void harness() pIncomingPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) ); + __CPROVER_assume( IMPLIES( pIncomingPacket != NULL, pIncomingPacket->remainingLength < REMAINING_LENGTH_MAX ) ); /* These are allocated for coverage of a NULL input. */ - pPacketId = mallocCanFail( sizeof( uint16_t ) ); - pSessionPresent = mallocCanFail( sizeof( bool ) ); + pPacketId = malloc( sizeof( uint16_t ) ); + pSessionPresent = malloc( sizeof( bool ) ); MQTT_DeserializeAck( pIncomingPacket, pPacketId, diff --git a/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c b/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c index ade8ae93f..2afb9a7d8 100644 --- a/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c +++ b/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c @@ -40,7 +40,7 @@ void harness() pPublishInfo = allocateMqttPublishInfo( NULL ); __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) ); - pPacketId = mallocCanFail( sizeof( uint16_t ) ); + pPacketId = malloc( sizeof( uint16_t ) ); /* This function grabs the topic name, the topic name length, the * the payload, and the payload length. */ diff --git a/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c b/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c index 780b98a0b..4dfa72c54 100644 --- a/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c +++ b/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c @@ -34,7 +34,7 @@ void harness() * MQTT_GetPacketId() touches only the nextPacketId field in MQTTContext_t. * This nextPacketId is left unbounded to verify the function under harness. */ - MQTTContext_t * pContext = mallocCanFail( sizeof( MQTTContext_t ) ); + MQTTContext_t * pContext = malloc( sizeof( MQTTContext_t ) ); MQTT_GetPacketId( pContext ); } diff --git a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 931bef463..75718d842 100644 --- a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -39,8 +39,8 @@ void harness() /* pPayloadStart and pPayloadSize are output parameters, and * thus, don't carry any assumptions. */ - pPayloadStart = mallocCanFail( sizeof( uint8_t * ) ); - pPayloadSize = mallocCanFail( sizeof( size_t ) ); + pPayloadStart = malloc( sizeof( uint8_t * ) ); + pPayloadSize = malloc( sizeof( size_t ) ); MQTT_GetSubAckStatusCodes( pSubackPacket, pPayloadStart, diff --git a/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c b/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c index 2ec5736a0..2ba88a3e4 100644 --- a/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c +++ b/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c @@ -36,11 +36,11 @@ void harness() MQTTEventCallback_t userCallback; MQTTFixedBuffer_t * pNetworkBuffer; - pContext = mallocCanFail( sizeof( MQTTContext_t ) ); - pTransportInterface = mallocCanFail( sizeof( TransportInterface_t ) ); - getTimeFunction = mallocCanFail( sizeof( MQTTGetCurrentTimeFunc_t ) ); - userCallback = mallocCanFail( sizeof( MQTTEventCallback_t ) ); - pNetworkBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) ); + pContext = malloc( sizeof( MQTTContext_t ) ); + pTransportInterface = malloc( sizeof( TransportInterface_t ) ); + getTimeFunction = malloc( sizeof( MQTTGetCurrentTimeFunc_t ) ); + userCallback = malloc( sizeof( MQTTEventCallback_t ) ); + pNetworkBuffer = malloc( sizeof( MQTTFixedBuffer_t ) ); MQTT_Init( pContext, pTransportInterface, diff --git a/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c b/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c index 72d941f95..e3ee4271f 100644 --- a/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c +++ b/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c @@ -37,10 +37,10 @@ void harness() bool * pMatchResult; __CPROVER_assume( nameLength < MAX_TOPIC_NAME_FILTER_LENGTH ); - pTopicName = mallocCanFail( ( sizeof( char ) * nameLength ) ); + pTopicName = malloc( ( sizeof( char ) * nameLength ) ); __CPROVER_assume( filterLength < MAX_TOPIC_NAME_FILTER_LENGTH ); - pTopicFilter = mallocCanFail( ( sizeof( char ) * filterLength ) ); - pMatchResult = mallocCanFail( sizeof( bool ) ); + pTopicFilter = malloc( ( sizeof( char ) * filterLength ) ); + pMatchResult = malloc( sizeof( bool ) ); MQTT_MatchTopic( pTopicName, nameLength, diff --git a/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c b/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c index e71c5bf00..10c61ef81 100644 --- a/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c +++ b/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c @@ -45,7 +45,7 @@ void harness() /* Allocate space for a returned header size to get coverage of a possibly * NULL input. */ - pHeaderSize = mallocCanFail( sizeof( size_t ) ); + pHeaderSize = malloc( sizeof( size_t ) ); /* Before calling MQTT_SerializePublishHeader() it is up to the application * to verify that the information in MQTTPublishInfo_t can fit into the diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index 24c71335c..bb643fd1b 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -50,25 +50,16 @@ #define REMAINING_LENGTH_MAX CBMC_MAX_OBJECT_SIZE #endif -void * mallocCanFail( size_t size ) -{ - __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "mallocCanFail size is too big" ); - return nondet_bool() ? NULL : malloc( size ); -} - MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo ) { if( pPacketInfo == NULL ) { - pPacketInfo = mallocCanFail( sizeof( MQTTPacketInfo_t ) ); + pPacketInfo = malloc( sizeof( MQTTPacketInfo_t ) ); } if( pPacketInfo != NULL ) { - __CPROVER_assert( REMAINING_LENGTH_MAX <= CBMC_MAX_OBJECT_SIZE, - "REMAINING_LENGTH_MAX size is too big" ); - __CPROVER_assume( pPacketInfo->remainingLength < REMAINING_LENGTH_MAX ); - pPacketInfo->pRemainingData = mallocCanFail( pPacketInfo->remainingLength ); + pPacketInfo->pRemainingData = malloc( pPacketInfo->remainingLength ); } return pPacketInfo; @@ -78,13 +69,6 @@ bool isValidMqttPacketInfo( const MQTTPacketInfo_t * pPacketInfo ) { bool isValid = true; - if( pPacketInfo != NULL ) - { - __CPROVER_assert( REMAINING_LENGTH_MAX <= CBMC_MAX_OBJECT_SIZE, - "REMAINING_LENGTH_MAX size is too big" ); - isValid = pPacketInfo->remainingLength < REMAINING_LENGTH_MAX; - } - return isValid; } @@ -92,15 +76,13 @@ MQTTPublishInfo_t * allocateMqttPublishInfo( MQTTPublishInfo_t * pPublishInfo ) { if( pPublishInfo == NULL ) { - pPublishInfo = mallocCanFail( sizeof( MQTTPublishInfo_t ) ); + pPublishInfo = malloc( sizeof( MQTTPublishInfo_t ) ); } if( pPublishInfo != NULL ) { - __CPROVER_assume( pPublishInfo->topicNameLength < CBMC_MAX_OBJECT_SIZE ); - pPublishInfo->pTopicName = mallocCanFail( pPublishInfo->topicNameLength ); - __CPROVER_assume( pPublishInfo->payloadLength < CBMC_MAX_OBJECT_SIZE ); - pPublishInfo->pPayload = mallocCanFail( pPublishInfo->payloadLength ); + pPublishInfo->pTopicName = malloc( pPublishInfo->topicNameLength ); + pPublishInfo->pPayload = malloc( pPublishInfo->payloadLength ); } return pPublishInfo; @@ -110,12 +92,6 @@ bool isValidMqttPublishInfo( const MQTTPublishInfo_t * pPublishInfo ) { bool isValid = true; - if( pPublishInfo != NULL ) - { - isValid = isValid && ( pPublishInfo->topicNameLength < CBMC_MAX_OBJECT_SIZE ); - isValid = isValid && ( pPublishInfo->payloadLength < CBMC_MAX_OBJECT_SIZE ); - } - return isValid; } @@ -123,17 +99,14 @@ MQTTConnectInfo_t * allocateMqttConnectInfo( MQTTConnectInfo_t * pConnectInfo ) { if( pConnectInfo == NULL ) { - pConnectInfo = mallocCanFail( sizeof( MQTTConnectInfo_t ) ); + pConnectInfo = malloc( sizeof( MQTTConnectInfo_t ) ); } if( pConnectInfo != NULL ) { - __CPROVER_assume( pConnectInfo->clientIdentifierLength < CBMC_MAX_OBJECT_SIZE ); - pConnectInfo->pClientIdentifier = mallocCanFail( pConnectInfo->clientIdentifierLength ); - __CPROVER_assume( pConnectInfo->userNameLength < CBMC_MAX_OBJECT_SIZE ); - pConnectInfo->pUserName = mallocCanFail( pConnectInfo->userNameLength ); - __CPROVER_assume( pConnectInfo->passwordLength < CBMC_MAX_OBJECT_SIZE ); - pConnectInfo->pPassword = mallocCanFail( pConnectInfo->passwordLength ); + pConnectInfo->pClientIdentifier = malloc( pConnectInfo->clientIdentifierLength ); + pConnectInfo->pUserName = malloc( pConnectInfo->userNameLength ); + pConnectInfo->pPassword = malloc( pConnectInfo->passwordLength ); } return pConnectInfo; @@ -143,13 +116,6 @@ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo ) { bool isValid = true; - if( pConnectInfo != NULL ) - { - isValid = isValid && ( pConnectInfo->clientIdentifierLength < CBMC_MAX_OBJECT_SIZE ); - isValid = isValid && ( pConnectInfo->userNameLength < CBMC_MAX_OBJECT_SIZE ); - isValid = isValid && ( pConnectInfo->passwordLength < CBMC_MAX_OBJECT_SIZE ); - } - return isValid; } @@ -157,13 +123,12 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ) { if( pFixedBuffer == NULL ) { - pFixedBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) ); + pFixedBuffer = malloc( sizeof( MQTTFixedBuffer_t ) ); } if( pFixedBuffer != NULL ) { - __CPROVER_assume( pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE ); - pFixedBuffer->pBuffer = mallocCanFail( pFixedBuffer->size ); + pFixedBuffer->pBuffer = malloc( pFixedBuffer->size ); } return pFixedBuffer; @@ -173,11 +138,6 @@ bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer ) { bool isValid = true; - if( pFixedBuffer != NULL ) - { - isValid = pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE; - } - return isValid; } @@ -186,16 +146,14 @@ MQTTSubscribeInfo_t * allocateMqttSubscriptionList( MQTTSubscribeInfo_t * pSubsc { if( pSubscriptionList == NULL ) { - __CPROVER_assume( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount < CBMC_MAX_OBJECT_SIZE ); - pSubscriptionList = mallocCanFail( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount ); + pSubscriptionList = malloc( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount ); } if( pSubscriptionList != NULL ) { for( int i = 0; i < subscriptionCount; i++ ) { - __CPROVER_assume( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE ); - pSubscriptionList[ i ].pTopicFilter = mallocCanFail( pSubscriptionList[ i ].topicFilterLength ); + pSubscriptionList[ i ].pTopicFilter = malloc( pSubscriptionList[ i ].topicFilterLength ); } } @@ -207,14 +165,6 @@ bool isValidMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList, { bool isValid = true; - if( pSubscriptionList != NULL ) - { - for( int i = 0; i < subscriptionCount; i++ ) - { - isValid = isValid && ( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE ); - } - } - return isValid; } @@ -226,10 +176,10 @@ MQTTContext_t * allocateMqttContext( MQTTContext_t * pContext ) if( pContext == NULL ) { - pContext = mallocCanFail( sizeof( MQTTContext_t ) ); + pContext = malloc( sizeof( MQTTContext_t ) ); } - pTransportInterface = mallocCanFail( sizeof( TransportInterface_t ) ); + pTransportInterface = malloc( sizeof( TransportInterface_t ) ); if( pTransportInterface != NULL ) { @@ -241,7 +191,6 @@ MQTTContext_t * allocateMqttContext( MQTTContext_t * pContext ) } pNetworkBuffer = allocateMqttFixedBuffer( NULL ); - __CPROVER_assume( isValidMqttFixedBuffer( pNetworkBuffer ) ); /* It is part of the API contract to call MQTT_Init() with the MQTTContext_t * before any other function in core_mqtt.h. */ @@ -271,8 +220,7 @@ bool isValidMqttContext( const MQTTContext_t * pContext ) if( pContext != NULL ) { - isValid = isValid && pContext->networkBuffer.size < CBMC_MAX_OBJECT_SIZE; - isValid = isValid && isValidMqttFixedBuffer( &( pContext->networkBuffer ) ); + isValid = isValidMqttFixedBuffer( &( pContext->networkBuffer ) ); } return isValid;