Removes all instances of mallocCanFail from CBMC proofs

Signed-off-by: Felipe R. Monteiro <[email protected]>
FreeRTOS · Oct 27, 2021 · 4795e1b · 4795e1b
1 parent 441244b
commit 4795e1b
Show file tree

Hide file tree

Showing 10 changed files with 34 additions and 92 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,29 +69,20 @@ 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;
 }
 
 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,30 +92,21 @@ 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;
 }
 
 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,27 +116,19 @@ 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;
 }
 
 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;