Skip to content

Commit

Permalink
Fix bugs in receiveSingleIteration and optimize sendMessageVector (#218)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@AniruddhaKanhere
AniruddhaKanhere authored Sep 21, 2022
1 parent 522d9cb commit b04c65f
Show file tree
Hide file tree
Showing 6 changed files with 111 additions and 12 deletions.
4 changes: 2 additions & 2 deletions docs/doxygen/include/size_table.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
<tr>
<td>core_mqtt.c</td>
<td><center>3.9K</center></td>
<td><center>3.3K</center></td>
<td><center>3.4K</center></td>
</tr>
<tr>
<td>core_mqtt_state.c</td>
Expand All @@ -25,6 +25,6 @@
<tr>
<td><b>Total estimates</b></td>
<td><b><center>8.4K</center></b></td>
<td><b><center>6.8K</center></b></td>
<td><b><center>6.9K</center></b></td>
</tr>
</table>
1 change: 1 addition & 0 deletions lexicon.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ bytesreceived
bytesrecvd
bytesremaining
bytessent
bytessentthisvector
bytestoread
bytestoreceive
bytestorecv
Expand Down
35 changes: 28 additions & 7 deletions source/core_mqtt.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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;
Expand All @@ -785,6 +782,7 @@ static int32_t sendMessageVector( MQTTContext_t * pContext,
else
{
bytesSentOrError = sendResult;

break;
}

Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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. */
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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. */
Expand Down Expand Up @@ -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;
Expand Down
3 changes: 3 additions & 0 deletions source/core_mqtt_serializer.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
}
78 changes: 75 additions & 3 deletions test/unit-test/core_mqtt_utest.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
Expand Down Expand Up @@ -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.
*/
Expand Down Expand Up @@ -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 );
Expand Down Expand Up @@ -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;
Expand All @@ -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 );
}
/* ========================================================================== */

Expand Down Expand Up @@ -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 );
Expand Down

0 comments on commit b04c65f

Please sign in to comment.