From b04c65f3c1a6ab3b81e4e51e319c3ec9ad44d703 Mon Sep 17 00:00:00 2001
From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Wed, 21 Sep 2022 15:26:58 -0700
Subject: [PATCH] Fix bugs in receiveSingleIteration and optimize
sendMessageVector (#218)
* Update the timout check in the send function
* Fix direction of check
* Allow processing of data in the buffer
* Fix formatting and unit-tests
* Update comment to clarify control flow
* Fix Disconnect CBMC proof and update size table
* Fix formatting and CBMC proofs
* Fix last CBMC proof
* Fix broken unit tests and add branch coverage
---
docs/doxygen/include/size_table.md | 4 +-
lexicon.txt | 1 +
source/core_mqtt.c | 35 +++++++--
source/core_mqtt_serializer.c | 3 +
.../MQTT_Disconnect/MQTT_Disconnect_harness.c | 2 +
test/unit-test/core_mqtt_utest.c | 78 ++++++++++++++++++-
6 files changed, 111 insertions(+), 12 deletions(-)
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
index 8aeb5ec40..4d198e3ab 100644
--- a/docs/doxygen/include/size_table.md
+++ b/docs/doxygen/include/size_table.md
@@ -10,7 +10,7 @@
| core_mqtt.c |
3.9K |
- 3.3K |
+ 3.4K |
| core_mqtt_state.c |
@@ -25,6 +25,6 @@
| Total estimates |
8.4K |
- 6.8K |
+ 6.9K |
diff --git a/lexicon.txt b/lexicon.txt
index e27c0df01..bf60d72ec 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -17,6 +17,7 @@ bytesreceived
bytesrecvd
bytesremaining
bytessent
+bytessentthisvector
bytestoread
bytestoreceive
bytestorecv
diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index bd51beebd..22c361c02 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -736,7 +736,6 @@ static int32_t sendMessageVector( MQTTContext_t * pContext,
uint32_t timeoutTime;
uint32_t bytesToSend = 0U;
int32_t bytesSentOrError = 0;
- uint64_t temp = 0;
TransportOutVector_t * pIoVectIterator;
size_t vectorsToBeSent = ioVecCount;
@@ -751,15 +750,13 @@ static int32_t sendMessageVector( MQTTContext_t * pContext,
/* Count the total number of bytes to be sent as outlined in the vector. */
for( pIoVectIterator = pIoVec; pIoVectIterator <= &( pIoVec[ ioVecCount - 1U ] ); pIoVectIterator++ )
{
- temp += pIoVectIterator->iov_len;
bytesToSend += ( uint32_t ) pIoVectIterator->iov_len;
}
/* Reset the iterator to point to the first entry in the array. */
pIoVectIterator = pIoVec;
- while( ( pContext->getTime() < timeoutTime ) &&
- ( bytesSentOrError < ( int32_t ) bytesToSend ) )
+ while( bytesSentOrError < ( int32_t ) bytesToSend )
{
int32_t sendResult;
uint32_t bytesSentThisVector = 0U;
@@ -785,6 +782,7 @@ static int32_t sendMessageVector( MQTTContext_t * pContext,
else
{
bytesSentOrError = sendResult;
+
break;
}
@@ -806,6 +804,12 @@ static int32_t sendMessageVector( MQTTContext_t * pContext,
pIoVectIterator->iov_base = ( const void * ) &( ( ( const uint8_t * ) pIoVectIterator->iov_base )[ bytesSentThisVector ] );
pIoVectIterator->iov_len -= bytesSentThisVector;
}
+
+ /* Check for timeout. */
+ if( pContext->getTime() > timeoutTime )
+ {
+ break;
+ }
}
return bytesSentOrError;
@@ -816,7 +820,7 @@ static int32_t sendBuffer( MQTTContext_t * pContext,
size_t bytesToSend )
{
const uint8_t * pIndex = pBufferToSend;
- size_t bytesRemaining = bytesToSend;
+ size_t bytesRemaining;
int32_t totalBytesSent = 0, bytesSent;
uint32_t lastSendTimeMs = 0U, timeSinceLastSendMs = 0U;
bool sendError = false;
@@ -1650,11 +1654,15 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext,
/* The receive function has failed. Bubble up the error up to the user. */
status = MQTTRecvFailed;
}
- else if( recvBytes == 0 )
+ else if( ( recvBytes == 0 ) && ( pContext->index == 0 ) )
{
- /* No more bytes available since the last read. */
+ /* No more bytes available since the last read and neither is anything in
+ * the buffer. */
status = MQTTNoDataAvailable;
}
+
+ /* Either something was received, or there is still data to be processed in the
+ * buffer, or both. */
else
{
/* Update the number of bytes in the MQTT fixed buffer. */
@@ -2088,6 +2096,11 @@ static MQTTStatus_t sendConnectWithoutCopy( MQTTContext_t * pContext,
LogError( ( "pWillInfo->pTopicName cannot be NULL if Will is present." ) );
status = MQTTBadParameter;
}
+ else if( ( pWillInfo != NULL ) && ( pWillInfo->pPayload == NULL ) )
+ {
+ LogError( ( "pWillInfo->pPayload cannot be NULL if Will is present." ) );
+ status = MQTTBadParameter;
+ }
else
{
pIndex = MQTT_SerializeConnectFixedHeader( pIndex,
@@ -2321,6 +2334,10 @@ static MQTTStatus_t handleSessionResumption( MQTTContext_t * pContext,
assert( pContext != NULL );
+ /* Reset the index and clear the buffer when a new session is established. */
+ pContext->index = 0;
+ memset( pContext->networkBuffer.pBuffer, 0, pContext->networkBuffer.size );
+
if( sessionPresent == true )
{
/* Get the next packet ID for which a PUBREL need to be resent. */
@@ -2969,6 +2986,10 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext )
{
LogInfo( ( "Disconnected from the broker." ) );
pContext->connectStatus = MQTTNotConnected;
+
+ /* Reset the index and clean the buffer on a successful disconnect. */
+ pContext->index = 0;
+ ( void ) memset( pContext->networkBuffer.pBuffer, 0, pContext->networkBuffer.size );
}
return status;
diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c
index 595ecd2fc..57b63eaa7 100644
--- a/source/core_mqtt_serializer.c
+++ b/source/core_mqtt_serializer.c
@@ -868,6 +868,8 @@ static MQTTStatus_t processRemainingLength( const uint8_t * pBuffer,
{
remainingLength = MQTT_REMAINING_LENGTH_INVALID;
+ LogError( ( "Invalid remaining length in the packet.\n" ) );
+
status = MQTTBadResponse;
}
else
@@ -904,6 +906,7 @@ static MQTTStatus_t processRemainingLength( const uint8_t * pBuffer,
if( bytesDecoded != expectedSize )
{
+ LogError( ( "Expected and actual length of decoded bytes do not match.\n" ) );
status = MQTTBadResponse;
}
else
diff --git a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c
index 7a751a16a..ea6397289 100644
--- a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c
+++ b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c
@@ -33,6 +33,8 @@ void harness()
pContext = allocateMqttContext( NULL );
__CPROVER_assume( isValidMqttContext( pContext ) );
+ __CPROVER_assume( pContext != NULL );
+ __CPROVER_assume( pContext->networkBuffer.pBuffer != NULL );
MQTT_Disconnect( pContext );
}
diff --git a/test/unit-test/core_mqtt_utest.c b/test/unit-test/core_mqtt_utest.c
index 094ad349b..afe3312c6 100644
--- a/test/unit-test/core_mqtt_utest.c
+++ b/test/unit-test/core_mqtt_utest.c
@@ -1025,6 +1025,8 @@ void test_MQTT_Connect_ProperWIllInfo( void )
willInfo.pTopicName = "MQTTTopic";
willInfo.topicNameLength = strlen( willInfo.pTopicName );
+ willInfo.pPayload = "MQTTPayload";
+ willInfo.payloadLength = strlen( willInfo.pPayload );
connectInfo.pUserName = "MQTTUser";
connectInfo.userNameLength = strlen( connectInfo.pUserName );
@@ -1054,6 +1056,60 @@ void test_MQTT_Connect_ProperWIllInfo( void )
TEST_ASSERT_EQUAL_INT( MQTTSendFailed, status );
}
+/**
+ * @brief Test MQTT_Connect, with no payload in will message.
+ */
+void test_MQTT_Connect_ImproperWIllInfo( void )
+{
+ MQTTContext_t mqttContext = { 0 };
+ MQTTConnectInfo_t connectInfo = { 0 };
+ uint32_t timeout = 2;
+ bool sessionPresent;
+ MQTTStatus_t status;
+ TransportInterface_t transport = { 0 };
+ MQTTFixedBuffer_t networkBuffer = { 0 };
+ size_t remainingLength;
+ size_t packetSize;
+ MQTTPublishInfo_t willInfo;
+
+ setupTransportInterface( &transport );
+ transport.writev = transportWritevFail;
+ setupNetworkBuffer( &networkBuffer );
+
+ memset( &mqttContext, 0x0, sizeof( mqttContext ) );
+ memset( &willInfo, 0, sizeof( MQTTPublishInfo_t ) );
+
+ willInfo.pTopicName = "MQTTTopic";
+ willInfo.topicNameLength = strlen( willInfo.pTopicName );
+
+ connectInfo.pUserName = "MQTTUser";
+ connectInfo.userNameLength = strlen( connectInfo.pUserName );
+ connectInfo.pPassword = "NotSafePassword";
+ connectInfo.passwordLength = strlen( connectInfo.pPassword );
+
+ MQTT_Init( &mqttContext, &transport, getTime, eventCallback, &networkBuffer );
+
+ /* Transport send failed when sending CONNECT. */
+
+ /* Choose 10 bytes variable header + 1 byte payload for the remaining
+ * length of the CONNECT. The packet size needs to be nonzero for this test
+ * as that is the amount of bytes used in the call to send the packet. */
+ packetSize = 13;
+ remainingLength = 11;
+ mqttContext.transportInterface.send = transportSendFailure;
+ MQTT_SerializeConnectFixedHeader_Stub( MQTT_SerializeConnectFixedHeader_cb );
+ MQTT_GetConnectPacketSize_ExpectAnyArgsAndReturn( MQTTSuccess );
+ MQTT_GetConnectPacketSize_IgnoreArg_pPacketSize();
+ MQTT_GetConnectPacketSize_IgnoreArg_pRemainingLength();
+ MQTT_GetConnectPacketSize_ReturnThruPtr_pPacketSize( &packetSize );
+ MQTT_GetConnectPacketSize_ReturnThruPtr_pRemainingLength( &remainingLength );
+ MQTT_SerializeConnect_IgnoreAndReturn( MQTTSuccess );
+
+ status = MQTT_Connect( &mqttContext, &connectInfo, &willInfo, timeout, &sessionPresent );
+
+ TEST_ASSERT_EQUAL_INT( MQTTBadParameter, status );
+}
+
/**
* @brief Test MQTT_Connect, except for receiving the CONNACK.
*/
@@ -1633,6 +1689,8 @@ void test_MQTT_Connect_happy_path3()
willInfo.pTopicName = "test";
willInfo.topicNameLength = 4;
+ willInfo.pPayload = "Payload";
+ willInfo.payloadLength = 7;
incomingPacket.type = MQTT_PACKET_TYPE_CONNACK;
MQTT_SerializeConnect_IgnoreAndReturn( MQTTSuccess );
MQTT_GetConnectPacketSize_IgnoreAndReturn( MQTTSuccess );
@@ -2545,6 +2603,9 @@ void test_MQTT_Disconnect4( void )
MQTTFixedBuffer_t networkBuffer = { 0 };
size_t disconnectSize = 2;
+ /* Fill the buffer with garbage data. */
+ memset( mqttBuffer, 0xAB, MQTT_TEST_BUFFER_LENGTH );
+
setupTransportInterface( &transport );
setupNetworkBuffer( &networkBuffer );
networkContext.buffer = &bufPtr;
@@ -2570,7 +2631,8 @@ void test_MQTT_Disconnect4( void )
TEST_ASSERT_EQUAL( MQTTSuccess, status );
TEST_ASSERT_EQUAL( MQTTNotConnected, mqttContext.connectStatus );
- TEST_ASSERT_EQUAL_MEMORY( mqttBuffer, buffer, 1 );
+ /* At disconnect, the buffer is cleared of any pending packets. */
+ TEST_ASSERT_EACH_EQUAL_UINT8( 0, mqttBuffer, MQTT_TEST_BUFFER_LENGTH );
}
/* ========================================================================== */
@@ -3886,11 +3948,21 @@ void test_MQTT_ReceiveLoop( void )
TEST_ASSERT_EQUAL( MQTTBadParameter, mqttStatus );
setupNetworkBuffer( &( context.networkBuffer ) );
- MQTT_ProcessIncomingPacketTypeAndLength_ExpectAnyArgsAndReturn( MQTTRecvFailed );
+ MQTT_ProcessIncomingPacketTypeAndLength_ExpectAnyArgsAndReturn( MQTTBadResponse );
/* Error case, for branch coverage. */
mqttStatus = MQTT_ReceiveLoop( &context );
- TEST_ASSERT_EQUAL( MQTTRecvFailed, mqttStatus );
+ TEST_ASSERT_EQUAL( MQTTBadResponse, mqttStatus );
+
+ /* This will cover the case when there is data available in the buffer to be processed but
+ * no additional bytes have been received by the transport interface. */
+ context.transportInterface.recv = transportRecvNoData;
+ MQTT_ProcessIncomingPacketTypeAndLength_ExpectAnyArgsAndReturn( MQTTBadResponse );
+ /* Error case, for branch coverage. */
+ mqttStatus = MQTT_ReceiveLoop( &context );
+ TEST_ASSERT_EQUAL( MQTTBadResponse, mqttStatus );
+ /* Reset the index to clear the buffer of any remaining data. */
+ context.index = 0;
/* Keep Alive should not trigger.*/
context.keepAliveIntervalSec = 1;
mqttStatus = MQTT_ReceiveLoop( &context );