From a2d57280b6717958d56a6871c30ca9c82568d954 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Tue, 26 Jul 2022 16:40:24 -0700 Subject: [PATCH 01/16] Add stateful process-loop function --- source/core_mqtt.c | 216 +++++++++++++++++++++----- source/core_mqtt_serializer.c | 166 ++++++++++++++++++++ source/include/core_mqtt.h | 7 +- source/include/core_mqtt_serializer.h | 45 ++++++ 4 files changed, 389 insertions(+), 45 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index 4226a7372..4f99ffede 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -101,6 +101,8 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType ); static int32_t recvExact( const MQTTContext_t * pContext, size_t bytesToRecv ); +static int32_t recvAndStoreExact( MQTTContext_t * pContext ); + /** * @brief Discard a packet from the transport interface. * @@ -127,6 +129,9 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext, MQTTPacketInfo_t incomingPacket, uint32_t remainingTimeMs ); +static MQTTStatus_t receiveAndStorePacket( MQTTContext_t * pContext, + MQTTStoredPacketInfo_t * pIncomingPacket ); + /** * @brief Get the correct ack type to send. * @@ -213,7 +218,6 @@ static MQTTStatus_t handleIncomingAck( MQTTContext_t * pContext, * #MQTTSuccess on success. */ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, - uint32_t remainingTimeMs, bool manageKeepAlive ); /** @@ -789,6 +793,88 @@ static int32_t recvExact( const MQTTContext_t * pContext, /*-----------------------------------------------------------*/ +static int32_t recvAndStoreExact( MQTTContext_t * pContext ) +{ + uint8_t * pIndex = NULL; + MQTTStoredPacketInfo_t * pPacketInformation = &( pContext->lastRxPacket ); + size_t bytesRemaining = pPacketInformation->bytesPendingRecv; + int32_t totalBytesRecvd = 0, bytesRecvd; + uint32_t lastDataRecvTimeMs = 0U, timeSinceLastRecvMs = 0U; + TransportRecv_t recvFunc = NULL; + MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL; + size_t index; + bool receiveError = false; + + assert( pContext != NULL ); + assert( pPacketInformation->remainingTotalPacketLength >= pPacketInformation->bytesPendingRecv ); + assert( pPacketInformation->remainingTotalPacketLength <= pContext->networkBuffer.size ); + assert( pContext->getTime != NULL ); + assert( pContext->transportInterface.recv != NULL ); + assert( pContext->networkBuffer.pBuffer != NULL ); + + index = pPacketInformation->remainingTotalPacketLength - bytesRemaining; + pIndex = &( pContext->networkBuffer.pBuffer[ index ] ); + recvFunc = pContext->transportInterface.recv; + getTimeStampMs = pContext->getTime; + + /* Part of the MQTT packet has been read before calling this function. */ + lastDataRecvTimeMs = getTimeStampMs(); + + while( ( bytesRemaining > 0U ) && ( receiveError == false ) ) + { + bytesRecvd = recvFunc( pContext->transportInterface.pNetworkContext, + pIndex, + bytesRemaining ); + + if( bytesRecvd < 0 ) + { + LogError( ( "Network error while receiving packet: ReturnCode=%ld.", + ( long int ) bytesRecvd ) ); + totalBytesRecvd = bytesRecvd; + receiveError = true; + } + else if( bytesRecvd > 0 ) + { + /* Reset the starting time as we have received some data from the network. */ + lastDataRecvTimeMs = getTimeStampMs(); + + /* It is a bug in the application's transport receive implementation + * if more bytes than expected are received. To avoid a possible + * overflow in converting bytesRemaining from unsigned to signed, + * this assert must exist after the check for bytesRecvd being + * negative. */ + assert( ( size_t ) bytesRecvd <= bytesRemaining ); + + bytesRemaining -= ( size_t ) bytesRecvd; + totalBytesRecvd += ( int32_t ) bytesRecvd; + pIndex += bytesRecvd; + LogDebug( ( "BytesReceived=%ld, BytesRemaining=%lu, TotalBytesReceived=%ld.", + ( long int ) bytesRecvd, + ( unsigned long ) bytesRemaining, + ( long int ) totalBytesRecvd ) ); + } + else + { + /* No bytes were read from the network. */ + timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs ); + + /* Check for timeout if we have been waiting to receive any byte on the network. */ + if( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) + { + LogError( ( "Unable to receive packet: Timed out in transport recv." ) ); + receiveError = true; + } + } + } + + /* Store the information back in the context. */ + pPacketInformation->bytesPendingRecv = bytesRemaining; + + return totalBytesRecvd; +} + +/*-----------------------------------------------------------*/ + static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, size_t remainingLength, uint32_t timeoutMs ) @@ -901,6 +987,62 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext, /*-----------------------------------------------------------*/ +static MQTTStatus_t receiveAndStorePacket( MQTTContext_t * pContext, + MQTTStoredPacketInfo_t * pIncomingPacket ) +{ + MQTTStatus_t status = MQTTSuccess; + int32_t bytesReceived = 0; + size_t bytesToReceive = 0U; + + assert( pContext != NULL ); + assert( pContext->networkBuffer.pBuffer != NULL ); + /* This stage should not be reached until the length is completely read. */ + assert( pIncomingPacket->lengthReadComplete == true ); + assert( pIncomingPacket->newPacket == false ); + + if( pIncomingPacket->remainingTotalPacketLength > pContext->networkBuffer.size ) + { + LogError( ( "Incoming packet will be dumped: " + "Packet length exceeds network buffer size." + "PacketSize=%lu, NetworkBufferSize=%lu.", + ( unsigned long ) pIncomingPacket->remainingTotalPacketLength, + ( unsigned long ) pContext->networkBuffer.size ) ); + status = discardPacket( pContext, + pIncomingPacket->remainingTotalPacketLength, + 0 ); + } + else + { + bytesReceived = recvAndStoreExact( pContext ); + + if( pContext->lastRxPacket.bytesPendingRecv == 0 ) + { + /* Receive successful, bytesReceived == bytesToReceive. */ + LogDebug( ( "Packet received. ReceivedBytes=%ld.", + ( long int ) bytesReceived ) ); + } + else if( bytesReceived > 0 ) + { + /* Non-zero bytes received but the complete packet is yet to be + * received. The status will indicate no data to be available + * unless the whole packet is received. */ + status = MQTTNoDataAvailable; + } + else + { + LogError( ( "Packet reception failed. ReceivedBytes=%ld, " + "ExpectedBytes=%lu.", + ( long int ) bytesReceived, + ( unsigned long ) bytesToReceive ) ); + status = MQTTRecvFailed; + } + } + + return status; +} + +/*-----------------------------------------------------------*/ + static uint8_t getAckTypeToSend( MQTTPublishState_t state ) { uint8_t packetTypeByte = 0U; @@ -1305,18 +1447,27 @@ static MQTTStatus_t handleIncomingAck( MQTTContext_t * pContext, /*-----------------------------------------------------------*/ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, - uint32_t remainingTimeMs, bool manageKeepAlive ) { MQTTStatus_t status = MQTTSuccess; MQTTPacketInfo_t incomingPacket; + MQTTStoredPacketInfo_t * pIncomingPacketStore = &pContext->lastRxPacket; assert( pContext != NULL ); assert( pContext->networkBuffer.pBuffer != NULL ); - status = MQTT_GetIncomingPacketTypeAndLength( pContext->transportInterface.recv, - pContext->transportInterface.pNetworkContext, - &incomingPacket ); + /* Start reading the first byte/length bytes only when: + * - This is a new packet being received OR + * - This is an old incomplete packet whole length is yet to be read. + */ + if( ( pIncomingPacketStore->newPacket == true ) || + ( ( pIncomingPacketStore->newPacket == false ) && + ( pIncomingPacketStore->lengthReadComplete == false ) ) ) + { + status = MQTT_StoreIncomingPacketTypeAndLength( pContext->transportInterface.recv, + pContext->transportInterface.pNetworkContext, + pIncomingPacketStore ); + } if( status == MQTTNoDataAvailable ) { @@ -1329,8 +1480,8 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, if( status == MQTTSuccess ) { - /* Reset the status to indicate that we should not try to read - * a packet from the transport interface. */ + /* Reset the status to indicate that nothing was read + * from the transport interface. */ status = MQTTNoDataAvailable; } } @@ -1343,18 +1494,21 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, { /* Receive packet. Remaining time is recalculated before calling this * function. */ - status = receivePacket( pContext, incomingPacket, remainingTimeMs ); + status = receiveAndStorePacket( pContext, pIncomingPacketStore ); } - /* Handle received packet. If no data was read then this will not execute. */ + /* Handle received packet. If incomplete data was read then this will not execute. */ if( status == MQTTSuccess ) { incomingPacket.pRemainingData = pContext->networkBuffer.pBuffer; + incomingPacket.type = pIncomingPacketStore->type; + incomingPacket.remainingLength = pIncomingPacketStore->remainingTotalPacketLength; + pContext->lastPacketRxTime = pContext->getTime(); /* PUBLISH packets allow flags in the lower four bits. For other * packet types, they are reserved. */ - if( ( incomingPacket.type & 0xF0U ) == MQTT_PACKET_TYPE_PUBLISH ) + if( ( pIncomingPacketStore->type & 0xF0U ) == MQTT_PACKET_TYPE_PUBLISH ) { status = handleIncomingPublish( pContext, &incomingPacket ); } @@ -1362,6 +1516,14 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, { status = handleIncomingAck( pContext, &incomingPacket, manageKeepAlive ); } + + /* Reset the fields in the context and clean up for next packet. */ + memset( pIncomingPacketStore, 0, sizeof( MQTTStoredPacketInfo_t ) ); + /* Set the multiplier back to 1. It is used for remaining length calculation. */ + pIncomingPacketStore->multipler = 1; + /* Set the field to show that the next packet is a new packet. Old one + * has been processed. */ + pIncomingPacketStore->newPacket = true; } if( status == MQTTNoDataAvailable ) @@ -2176,11 +2338,9 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext ) /*-----------------------------------------------------------*/ -MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext, - uint32_t timeoutMs ) +MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ) { MQTTStatus_t status = MQTTBadParameter; - uint32_t entryTimeMs = 0U, remainingTimeMs = timeoutMs, elapsedTimeMs = 0U; if( pContext == NULL ) { @@ -2196,37 +2356,11 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext, } else { - entryTimeMs = pContext->getTime(); pContext->controlPacketSent = false; status = MQTTSuccess; } - while( status == MQTTSuccess ) - { - status = receiveSingleIteration( pContext, remainingTimeMs, true ); - - /* We don't need to break here since the status is already checked in - * the loop condition, and we do not want multiple breaks in a loop. */ - if( status != MQTTSuccess ) - { - LogError( ( "Exiting process loop due to failure: ErrorStatus=%s", - MQTT_Status_strerror( status ) ) ); - } - else - { - /* Recalculate remaining time and check if loop should exit. This is - * done at the end so the loop will run at least a single iteration. */ - elapsedTimeMs = calculateElapsedTime( pContext->getTime(), - entryTimeMs ); - - if( elapsedTimeMs >= timeoutMs ) - { - break; - } - - remainingTimeMs = timeoutMs - elapsedTimeMs; - } - } + status = receiveSingleIteration( pContext, true ); return status; } @@ -2259,7 +2393,7 @@ MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext, while( status == MQTTSuccess ) { - status = receiveSingleIteration( pContext, remainingTimeMs, false ); + status = receiveSingleIteration( pContext, false ); /* We don't need to break here since the status is already checked in * the loop condition, and we do not want multiple breaks in a loop. */ diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c index cfc1f00d3..51e3d18c6 100644 --- a/source/core_mqtt_serializer.c +++ b/source/core_mqtt_serializer.c @@ -298,6 +298,10 @@ static uint8_t * encodeString( uint8_t * pDestination, static size_t getRemainingLength( TransportRecv_t recvFunc, NetworkContext_t * pNetworkContext ); +static size_t storeRemainingLength( TransportRecv_t recvFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacketStore ); + /** * @brief Check if an incoming packet type is valid. * @@ -758,6 +762,86 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, /*-----------------------------------------------------------*/ +static size_t storeRemainingLength( TransportRecv_t recvFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacketStore ) +{ + size_t remainingLength = pIncomingPacketStore->remainingTotalPacketLength; + size_t multiplier = pIncomingPacketStore->multipler; + size_t bytesDecoded = pIncomingPacketStore->totalLengthBytesRead; + size_t expectedSize = 0; + uint8_t encodedByte = 0; + int32_t bytesReceived = 0; + + /* This algorithm is copied from the MQTT v3.1.1 spec. */ + do + { + if( multiplier > 2097152U ) /* 128 ^ 3 */ + { + remainingLength = MQTT_REMAINING_LENGTH_INVALID; + + /* Complete, albeit incorrect, length has been read. */ + pIncomingPacketStore->lengthReadComplete = true; + } + else + { + bytesReceived = recvFunc( pNetworkContext, &encodedByte, 1U ); + + if( bytesReceived == 1 ) + { + remainingLength += ( ( size_t ) encodedByte & 0x7FU ) * multiplier; + multiplier *= 128U; + bytesDecoded++; + } + else + { + /* In case nothing is received from the transport interface, + * save the state. */ + pIncomingPacketStore->multipler = multiplier; + pIncomingPacketStore->remainingTotalPacketLength = remainingLength; + pIncomingPacketStore->totalLengthBytesRead = bytesDecoded; + pIncomingPacketStore->lengthReadComplete = false; + + /* And break out of the loop. */ + break; + } + } + + if( remainingLength == MQTT_REMAINING_LENGTH_INVALID ) + { + break; + } + } while( ( encodedByte & 0x80U ) != 0U ); + + if( ( encodedByte & 0x80U ) == 0U ) + { + /* If this is the last byte, then the length has been fully received. + * Fill in the data in the context. + */ + pIncomingPacketStore->lengthReadComplete = true; + pIncomingPacketStore->multipler = multiplier; + pIncomingPacketStore->remainingTotalPacketLength = remainingLength; + pIncomingPacketStore->totalLengthBytesRead = bytesDecoded; + pIncomingPacketStore->bytesPendingRecv = remainingLength; + } + + /* Check that the decoded remaining length conforms to the MQTT specification. */ + if( ( pIncomingPacketStore->lengthReadComplete == true ) && + ( remainingLength != MQTT_REMAINING_LENGTH_INVALID ) ) + { + expectedSize = remainingLengthEncodedSize( remainingLength ); + + if( bytesDecoded != expectedSize ) + { + remainingLength = MQTT_REMAINING_LENGTH_INVALID; + } + } + + return remainingLength; +} + +/*-----------------------------------------------------------*/ + static bool incomingPacketValid( uint8_t packetType ) { bool status = false; @@ -2417,3 +2501,85 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, } /*-----------------------------------------------------------*/ + +MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacket ) +{ + MQTTStatus_t status = MQTTSuccess; + int32_t bytesReceived = 0; + + if( pIncomingPacket == NULL ) + { + LogError( ( "Invalid parameter: pIncomingPacket is NULL." ) ); + status = MQTTBadParameter; + } + else + { + /* Read the first byte (type) only if this is a new packet. */ + if( pIncomingPacket->newPacket == true ) + { + /* Read a single byte. */ + bytesReceived = readFunc( pNetworkContext, + &( pIncomingPacket->type ), + 1U ); + } + else + { + /* Show that the first byte has been received. */ + bytesReceived = 1; + } + } + + if( bytesReceived == 1 ) + { + /* Check validity. */ + if( incomingPacketValid( pIncomingPacket->type ) == true ) + { + /* Update this field showing that this packet is not 'new'. */ + pIncomingPacket->newPacket = false; + + pIncomingPacket->remainingTotalPacketLength = storeRemainingLength( readFunc, + pNetworkContext, + pIncomingPacket ); + + if( pIncomingPacket->remainingTotalPacketLength == MQTT_REMAINING_LENGTH_INVALID ) + { + LogError( ( "Incoming packet remaining length invalid." ) ); + status = MQTTBadResponse; + } + } + else + { + /* Update this field showing that the next byte received will be + * treated as belonging to a new packet. */ + pIncomingPacket->newPacket = true; + + LogError( ( "Incoming packet invalid: Packet type=%u.", + ( unsigned int ) pIncomingPacket->type ) ); + status = MQTTBadResponse; + } + } + else if( ( status != MQTTBadParameter ) && ( bytesReceived == 0 ) ) + { + status = MQTTNoDataAvailable; + } + + /* If the input packet was valid, then any other number of bytes received is + * a failure. */ + else if( status != MQTTBadParameter ) + { + LogError( ( "A single byte was not read from the transport: " + "transportStatus=%ld.", + ( long int ) bytesReceived ) ); + status = MQTTRecvFailed; + } + else + { + /* Empty else MISRA 15.7 */ + } + + return status; +} + +/*-----------------------------------------------------------*/ diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h index 4feca99c5..b815b11f7 100644 --- a/source/include/core_mqtt.h +++ b/source/include/core_mqtt.h @@ -227,6 +227,7 @@ typedef struct MQTTContext uint16_t keepAliveIntervalSec; /**< @brief Keep Alive interval. */ uint32_t pingReqSendTimeMs; /**< @brief Timestamp of the last sent PINGREQ. */ bool waitingForPingResp; /**< @brief If the library is currently awaiting a PINGRESP. */ + MQTTStoredPacketInfo_t lastRxPacket; } MQTTContext_t; /** @@ -648,13 +649,12 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext ); * * // Variables used in this example. * MQTTStatus_t status; - * uint32_t timeoutMs = 100; * // This context is assumed to be initialized and connected. * MQTTContext_t * pContext; * * while( true ) * { - * status = MQTT_ProcessLoop( pContext, timeoutMs ); + * status = MQTT_ProcessLoop( pContext ); * * if( status != MQTTSuccess ) * { @@ -669,8 +669,7 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext ); * @endcode */ /* @[declare_mqtt_processloop] */ -MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext, - uint32_t timeoutMs ); +MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ); /* @[declare_mqtt_processloop] */ /** diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index bf3d974f4..4ff2b0438 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -265,6 +265,47 @@ typedef struct MQTTPacketInfo size_t remainingLength; } MQTTPacketInfo_t; + +typedef struct MQTTStoredPacketInfo +{ + /** + * @brief This boolean value represents whether any data has been received + * or not. + */ + bool newPacket; + + /** + * @brief Whether the complete length field has been read or not. + */ + bool lengthReadComplete; + + /** + * @brief Type of the packet being received. First byte of the header. + */ + uint8_t type; + + /** + * @brief How many (1-4) bytes have been read for the length. + */ + size_t totalLengthBytesRead; + + /** + * @brief The value of multipler used to calculate remaining bytes. + */ + size_t multipler; + + /** + * @brief Total number of bytes in the packet. This is calculated using + * length[4] array. + */ + size_t remainingTotalPacketLength; + + /** + * @brief Total number of bytes which are yet to be received from the + * socket. + */ + size_t bytesPendingRecv; +} MQTTStoredPacketInfo_t; /** * @brief Get the size and Remaining Length of an MQTT CONNECT packet. * @@ -1177,6 +1218,10 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, MQTTPacketInfo_t * pIncomingPacket ); /* @[declare_mqtt_getincomingpackettypeandlength] */ +MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacket ); + /* *INDENT-OFF* */ #ifdef __cplusplus } From c4f76fc3a20725aba3a17cb932606da344b73acb Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Wed, 27 Jul 2022 15:52:35 -0700 Subject: [PATCH 02/16] Add extra checks; fix bugs and add description of functions --- source/core_mqtt.c | 13 +++-- source/core_mqtt_serializer.c | 78 ++++++++++++++++----------- source/include/core_mqtt_serializer.h | 22 +++++++- 3 files changed, 77 insertions(+), 36 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index 4f99ffede..c35b6767d 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -1490,15 +1490,20 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, LogError( ( "Receiving incoming packet length failed. Status=%s", MQTT_Status_strerror( status ) ) ); } - else + else if( pIncomingPacketStore->lengthReadComplete == true ) { - /* Receive packet. Remaining time is recalculated before calling this - * function. */ + /* Receive the packet only when the length has been completely read. + * Remaining time is recalculated before calling this function. */ status = receiveAndStorePacket( pContext, pIncomingPacketStore ); } + else + { + /* Receiving the length was not complete. Do nothing. */ + } /* Handle received packet. If incomplete data was read then this will not execute. */ - if( status == MQTTSuccess ) + if( ( status == MQTTSuccess ) && + ( pIncomingPacketStore->lengthReadComplete == true ) ) { incomingPacket.pRemainingData = pContext->networkBuffer.pBuffer; incomingPacket.type = pIncomingPacketStore->type; diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c index 51e3d18c6..7d6a6f01e 100644 --- a/source/core_mqtt_serializer.c +++ b/source/core_mqtt_serializer.c @@ -298,9 +298,22 @@ static uint8_t * encodeString( uint8_t * pDestination, static size_t getRemainingLength( TransportRecv_t recvFunc, NetworkContext_t * pNetworkContext ); -static size_t storeRemainingLength( TransportRecv_t recvFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacketStore ); +/** + * @brief Retrieves, decodes and stores the Remaining Length from the network + * interface by reading a single byte at a time. + * + * @param[in] recvFunc Network interface receive function. + * @param[in] pNetworkContext Network interface context to the receive function. + * @param[in] pIncomingPacketStore Strucutre used to hold the fields of the + * incoming packet. + * + * @return MQTTIncomingRecvIncomplete is returned to show that the incoming + * packet is not yet fully received and decoded. Otherwise, MQTTSuccess + * shows that processing of the packet was successful. + */ +static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacketStore ); /** * @brief Check if an incoming packet type is valid. @@ -762,9 +775,9 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, /*-----------------------------------------------------------*/ -static size_t storeRemainingLength( TransportRecv_t recvFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacketStore ) +static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, + NetworkContext_t * pNetworkContext, + MQTTStoredPacketInfo_t * pIncomingPacketStore ) { size_t remainingLength = pIncomingPacketStore->remainingTotalPacketLength; size_t multiplier = pIncomingPacketStore->multipler; @@ -772,6 +785,7 @@ static size_t storeRemainingLength( TransportRecv_t recvFunc, size_t expectedSize = 0; uint8_t encodedByte = 0; int32_t bytesReceived = 0; + MQTTStatus_t status = MQTTSuccess; /* This algorithm is copied from the MQTT v3.1.1 spec. */ do @@ -782,6 +796,8 @@ static size_t storeRemainingLength( TransportRecv_t recvFunc, /* Complete, albeit incorrect, length has been read. */ pIncomingPacketStore->lengthReadComplete = true; + + status = MQTTBadResponse; } else { @@ -795,49 +811,55 @@ static size_t storeRemainingLength( TransportRecv_t recvFunc, } else { + if( bytesReceived == 0 ) + { + status = MQTTIncomingRecvIncomplete; + } + else + { + /* Bubble up the error to the user. */ + status = MQTTBadResponse; + } + /* In case nothing is received from the transport interface, * save the state. */ pIncomingPacketStore->multipler = multiplier; pIncomingPacketStore->remainingTotalPacketLength = remainingLength; pIncomingPacketStore->totalLengthBytesRead = bytesDecoded; pIncomingPacketStore->lengthReadComplete = false; - - /* And break out of the loop. */ - break; - } + } } - if( remainingLength == MQTT_REMAINING_LENGTH_INVALID ) + /* If the response is incorrect, or no more data is available, then + * break out of the loop. */ + if( ( remainingLength == MQTT_REMAINING_LENGTH_INVALID ) || + ( status != MQTTSuccess ) ) { break; } } while( ( encodedByte & 0x80U ) != 0U ); - if( ( encodedByte & 0x80U ) == 0U ) + if( status == MQTTSuccess ) { /* If this is the last byte, then the length has been fully received. * Fill in the data in the context. */ - pIncomingPacketStore->lengthReadComplete = true; - pIncomingPacketStore->multipler = multiplier; + pIncomingPacketStore->lengthReadComplete = true; + /* Reset the multiplier. */ + pIncomingPacketStore->multipler = 1; pIncomingPacketStore->remainingTotalPacketLength = remainingLength; - pIncomingPacketStore->totalLengthBytesRead = bytesDecoded; pIncomingPacketStore->bytesPendingRecv = remainingLength; - } - /* Check that the decoded remaining length conforms to the MQTT specification. */ - if( ( pIncomingPacketStore->lengthReadComplete == true ) && - ( remainingLength != MQTT_REMAINING_LENGTH_INVALID ) ) - { + /* Check that the decoded remaining length conforms to the MQTT specification. */ expectedSize = remainingLengthEncodedSize( remainingLength ); if( bytesDecoded != expectedSize ) { - remainingLength = MQTT_REMAINING_LENGTH_INVALID; + status = MQTTBadResponse; } } - return remainingLength; + return status; } /*-----------------------------------------------------------*/ @@ -2539,15 +2561,9 @@ MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, /* Update this field showing that this packet is not 'new'. */ pIncomingPacket->newPacket = false; - pIncomingPacket->remainingTotalPacketLength = storeRemainingLength( readFunc, - pNetworkContext, - pIncomingPacket ); - - if( pIncomingPacket->remainingTotalPacketLength == MQTT_REMAINING_LENGTH_INVALID ) - { - LogError( ( "Incoming packet remaining length invalid." ) ); - status = MQTTBadResponse; - } + status = storeRemainingLength( readFunc, + pNetworkContext, + pIncomingPacket ); } else { diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index 4ff2b0438..8b9d32ce2 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -105,7 +105,8 @@ typedef enum MQTTStatus MQTTNoDataAvailable, /**< No data available from the transport interface. */ MQTTIllegalState, /**< An illegal state in the state record. */ MQTTStateCollision, /**< A collision with an existing state record entry. */ - MQTTKeepAliveTimeout /**< Timeout while waiting for PINGRESP. */ + MQTTKeepAliveTimeout, /**< Timeout while waiting for PINGRESP. */ + MQTTIncomingRecvIncomplete /**< Error to show that the MQTT_ProcessLoop has received incomplete data. */ } MQTTStatus_t; /** @@ -1218,6 +1219,25 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, MQTTPacketInfo_t * pIncomingPacket ); /* @[declare_mqtt_getincomingpackettypeandlength] */ +/** + * @brief Extract the MQTT packet type and length from incoming packet. + * + * This function must be called for every incoming packet to retrieve the + * #MQTTPacketInfo_t.type and #MQTTPacketInfo_t.remainingLength. A + * #MQTTPacketInfo_t is not valid until this routine has been invoked. + * + * @param[in] readFunc Transport layer read function pointer. + * @param[in] pNetworkContext The network context pointer provided by the application. + * @param[out] pIncomingPacket Pointer to MQTTStoredPacketInfo_t structure. This is + * where type, remaining length and packet identifier are stored and used in later + * iterations. + * + * @return #MQTTSuccess on successful extraction of type and length, + * #MQTTBadParameter if @p pIncomingPacket is invalid, + * #MQTTRecvFailed on transport receive failure, + * #MQTTBadResponse if an invalid packet is read, and + * #MQTTNoDataAvailable if there is nothing to read. + */ MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, NetworkContext_t * pNetworkContext, MQTTStoredPacketInfo_t * pIncomingPacket ); From ce878e557a789067893621a01354256e4a94e832 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Wed, 3 Aug 2022 20:06:53 -0700 Subject: [PATCH 03/16] Add index based stateful processloop --- source/core_mqtt.c | 312 ++++++++++---------------- source/core_mqtt_serializer.c | 131 ++++------- source/include/core_mqtt.h | 4 +- source/include/core_mqtt_serializer.h | 30 +-- 4 files changed, 178 insertions(+), 299 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index c35b6767d..fc94c4ce4 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -101,7 +101,8 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType ); static int32_t recvExact( const MQTTContext_t * pContext, size_t bytesToRecv ); -static int32_t recvAndStoreExact( MQTTContext_t * pContext ); +static int32_t processPacket( MQTTContext_t * pContext, + MQTTPacketInfo_t * pIncomingPacket ); /** * @brief Discard a packet from the transport interface. @@ -116,6 +117,8 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, size_t remainingLength, uint32_t timeoutMs ); +static MQTTStatus_t discardStoredPacket( const MQTTContext_t * pContext, + MQTTPacketInfo_t * pPacketInfo ); /** * @brief Receive a packet from the transport interface. * @@ -130,7 +133,7 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext, uint32_t remainingTimeMs ); static MQTTStatus_t receiveAndStorePacket( MQTTContext_t * pContext, - MQTTStoredPacketInfo_t * pIncomingPacket ); + MQTTPacketInfo_t * pIncomingPacket ); /** * @brief Get the correct ack type to send. @@ -793,106 +796,93 @@ static int32_t recvExact( const MQTTContext_t * pContext, /*-----------------------------------------------------------*/ -static int32_t recvAndStoreExact( MQTTContext_t * pContext ) +static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, + size_t remainingLength, + uint32_t timeoutMs ) { - uint8_t * pIndex = NULL; - MQTTStoredPacketInfo_t * pPacketInformation = &( pContext->lastRxPacket ); - size_t bytesRemaining = pPacketInformation->bytesPendingRecv; - int32_t totalBytesRecvd = 0, bytesRecvd; - uint32_t lastDataRecvTimeMs = 0U, timeSinceLastRecvMs = 0U; - TransportRecv_t recvFunc = NULL; + MQTTStatus_t status = MQTTRecvFailed; + int32_t bytesReceived = 0; + size_t bytesToReceive = 0U; + uint32_t totalBytesReceived = 0U, entryTimeMs = 0U, elapsedTimeMs = 0U; MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL; - size_t index; bool receiveError = false; assert( pContext != NULL ); - assert( pPacketInformation->remainingTotalPacketLength >= pPacketInformation->bytesPendingRecv ); - assert( pPacketInformation->remainingTotalPacketLength <= pContext->networkBuffer.size ); assert( pContext->getTime != NULL ); - assert( pContext->transportInterface.recv != NULL ); - assert( pContext->networkBuffer.pBuffer != NULL ); - index = pPacketInformation->remainingTotalPacketLength - bytesRemaining; - pIndex = &( pContext->networkBuffer.pBuffer[ index ] ); - recvFunc = pContext->transportInterface.recv; + bytesToReceive = pContext->networkBuffer.size; getTimeStampMs = pContext->getTime; - /* Part of the MQTT packet has been read before calling this function. */ - lastDataRecvTimeMs = getTimeStampMs(); + entryTimeMs = getTimeStampMs(); - while( ( bytesRemaining > 0U ) && ( receiveError == false ) ) + while( ( totalBytesReceived < remainingLength ) && ( receiveError == false ) ) { - bytesRecvd = recvFunc( pContext->transportInterface.pNetworkContext, - pIndex, - bytesRemaining ); - - if( bytesRecvd < 0 ) + if( ( remainingLength - totalBytesReceived ) < bytesToReceive ) { - LogError( ( "Network error while receiving packet: ReturnCode=%ld.", - ( long int ) bytesRecvd ) ); - totalBytesRecvd = bytesRecvd; - receiveError = true; + bytesToReceive = remainingLength - totalBytesReceived; } - else if( bytesRecvd > 0 ) - { - /* Reset the starting time as we have received some data from the network. */ - lastDataRecvTimeMs = getTimeStampMs(); - /* It is a bug in the application's transport receive implementation - * if more bytes than expected are received. To avoid a possible - * overflow in converting bytesRemaining from unsigned to signed, - * this assert must exist after the check for bytesRecvd being - * negative. */ - assert( ( size_t ) bytesRecvd <= bytesRemaining ); + bytesReceived = recvExact( pContext, bytesToReceive ); - bytesRemaining -= ( size_t ) bytesRecvd; - totalBytesRecvd += ( int32_t ) bytesRecvd; - pIndex += bytesRecvd; - LogDebug( ( "BytesReceived=%ld, BytesRemaining=%lu, TotalBytesReceived=%ld.", - ( long int ) bytesRecvd, - ( unsigned long ) bytesRemaining, - ( long int ) totalBytesRecvd ) ); + if( bytesReceived != ( int32_t ) bytesToReceive ) + { + LogError( ( "Receive error while discarding packet." + "ReceivedBytes=%ld, ExpectedBytes=%lu.", + ( long int ) bytesReceived, + ( unsigned long ) bytesToReceive ) ); + receiveError = true; } else { - /* No bytes were read from the network. */ - timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs ); + totalBytesReceived += ( uint32_t ) bytesReceived; - /* Check for timeout if we have been waiting to receive any byte on the network. */ - if( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) + elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs ); + + /* Check for timeout. */ + if( elapsedTimeMs >= timeoutMs ) { - LogError( ( "Unable to receive packet: Timed out in transport recv." ) ); + LogError( ( "Time expired while discarding packet." ) ); receiveError = true; } } } - /* Store the information back in the context. */ - pPacketInformation->bytesPendingRecv = bytesRemaining; - - return totalBytesRecvd; -} + if( totalBytesReceived == remainingLength ) + { + LogError( ( "Dumped packet. DumpedBytes=%lu.", + ( unsigned long ) totalBytesReceived ) ); + /* Packet dumped, so no data is available. */ + status = MQTTNoDataAvailable; + } -/*-----------------------------------------------------------*/ + return status; +} -static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, - size_t remainingLength, - uint32_t timeoutMs ) +static MQTTStatus_t discardStoredPacket( MQTTContext_t * pContext, + MQTTPacketInfo_t * pPacketInfo ) { MQTTStatus_t status = MQTTRecvFailed; int32_t bytesReceived = 0; size_t bytesToReceive = 0U; - uint32_t totalBytesReceived = 0U, entryTimeMs = 0U, elapsedTimeMs = 0U; - MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL; + uint32_t totalBytesReceived = 0U; bool receiveError = false; + size_t mqttPacketSize = 0; + size_t remainingLength; assert( pContext != NULL ); - assert( pContext->getTime != NULL ); + assert( pPacketInfo != NULL ); + + mqttPacketSize = pPacketInfo->remainingLength + pPacketInfo->headerLength; + + /* Assert that the packet being discarded is bigger than the + * receive buffer. */ + assert( mqttPacketSize > pContext->networkBuffer.size ); + /* Discard these many bytes at a time. */ bytesToReceive = pContext->networkBuffer.size; - getTimeStampMs = pContext->getTime; - entryTimeMs = getTimeStampMs(); + /* Number of bytes depicted by 'index' have already been received. */ + remainingLength = mqttPacketSize - pContext->index; while( ( totalBytesReceived < remainingLength ) && ( receiveError == false ) ) { @@ -914,15 +904,6 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, else { totalBytesReceived += ( uint32_t ) bytesReceived; - - elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs ); - - /* Check for timeout. */ - if( elapsedTimeMs >= timeoutMs ) - { - LogError( ( "Time expired while discarding packet." ) ); - receiveError = true; - } } } @@ -934,6 +915,14 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, status = MQTTNoDataAvailable; } + /* Clear the buffer */ + memset( pContext->networkBuffer.pBuffer, + 0, + pContext->networkBuffer.size ); + + /* Reset the index. */ + pContext->index = 0; + return status; } @@ -987,62 +976,6 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext, /*-----------------------------------------------------------*/ -static MQTTStatus_t receiveAndStorePacket( MQTTContext_t * pContext, - MQTTStoredPacketInfo_t * pIncomingPacket ) -{ - MQTTStatus_t status = MQTTSuccess; - int32_t bytesReceived = 0; - size_t bytesToReceive = 0U; - - assert( pContext != NULL ); - assert( pContext->networkBuffer.pBuffer != NULL ); - /* This stage should not be reached until the length is completely read. */ - assert( pIncomingPacket->lengthReadComplete == true ); - assert( pIncomingPacket->newPacket == false ); - - if( pIncomingPacket->remainingTotalPacketLength > pContext->networkBuffer.size ) - { - LogError( ( "Incoming packet will be dumped: " - "Packet length exceeds network buffer size." - "PacketSize=%lu, NetworkBufferSize=%lu.", - ( unsigned long ) pIncomingPacket->remainingTotalPacketLength, - ( unsigned long ) pContext->networkBuffer.size ) ); - status = discardPacket( pContext, - pIncomingPacket->remainingTotalPacketLength, - 0 ); - } - else - { - bytesReceived = recvAndStoreExact( pContext ); - - if( pContext->lastRxPacket.bytesPendingRecv == 0 ) - { - /* Receive successful, bytesReceived == bytesToReceive. */ - LogDebug( ( "Packet received. ReceivedBytes=%ld.", - ( long int ) bytesReceived ) ); - } - else if( bytesReceived > 0 ) - { - /* Non-zero bytes received but the complete packet is yet to be - * received. The status will indicate no data to be available - * unless the whole packet is received. */ - status = MQTTNoDataAvailable; - } - else - { - LogError( ( "Packet reception failed. ReceivedBytes=%ld, " - "ExpectedBytes=%lu.", - ( long int ) bytesReceived, - ( unsigned long ) bytesToReceive ) ); - status = MQTTRecvFailed; - } - } - - return status; -} - -/*-----------------------------------------------------------*/ - static uint8_t getAckTypeToSend( MQTTPublishState_t state ) { uint8_t packetTypeByte = 0U; @@ -1450,23 +1383,38 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, bool manageKeepAlive ) { MQTTStatus_t status = MQTTSuccess; - MQTTPacketInfo_t incomingPacket; - MQTTStoredPacketInfo_t * pIncomingPacketStore = &pContext->lastRxPacket; + MQTTPacketInfo_t incomingPacket = { 0 }; + int32_t recvBytes; + size_t totalMQTTPacketLength = 0; assert( pContext != NULL ); assert( pContext->networkBuffer.pBuffer != NULL ); - /* Start reading the first byte/length bytes only when: - * - This is a new packet being received OR - * - This is an old incomplete packet whole length is yet to be read. - */ - if( ( pIncomingPacketStore->newPacket == true ) || - ( ( pIncomingPacketStore->newPacket == false ) && - ( pIncomingPacketStore->lengthReadComplete == false ) ) ) + /* Read as many bytes as possible into the network buffer. */ + recvBytes = pContext->transportInterface.recv( pContext->transportInterface.pNetworkContext, + &( pContext->networkBuffer.pBuffer[ pContext->index ] ), + pContext->networkBuffer.size - pContext->index ); + + if( recvBytes < 0 ) { - status = MQTT_StoreIncomingPacketTypeAndLength( pContext->transportInterface.recv, - pContext->transportInterface.pNetworkContext, - pIncomingPacketStore ); + /* The receive function has failed. Bubble up the error up to the user. */ + status = MQTTRecvFailed; + } + else if( recvBytes == 0 ) + { + /* No more bytes available since the last read. */ + status = MQTTNoDataAvailable; + } + else + { + /* Update the number of bytes in the MQTT fixed buffer. */ + pContext->index += recvBytes; + + status = MQTT_StoreIncomingPacketTypeAndLength( pContext->networkBuffer.pBuffer, + &pContext->index, + &incomingPacket ); + + totalMQTTPacketLength = incomingPacket.remainingLength + incomingPacket.headerLength; } if( status == MQTTNoDataAvailable ) @@ -1490,30 +1438,31 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, LogError( ( "Receiving incoming packet length failed. Status=%s", MQTT_Status_strerror( status ) ) ); } - else if( pIncomingPacketStore->lengthReadComplete == true ) + /* If the MQTT Packet size is bigger than the buffer itself. */ + else if( totalMQTTPacketLength > pContext->networkBuffer.size ) { - /* Receive the packet only when the length has been completely read. - * Remaining time is recalculated before calling this function. */ - status = receiveAndStorePacket( pContext, pIncomingPacketStore ); + /* Discard the packet from the buffer and from the socket buffer. */ + status = discardStoredPacket( pContext, + &incomingPacket ); + } + /* If the total packet is of more length than the bytes we have available. */ + else if( totalMQTTPacketLength > pContext->index ) + { + status = MQTTNeedMoreBytes; } else { - /* Receiving the length was not complete. Do nothing. */ + /* MISRA else */ } /* Handle received packet. If incomplete data was read then this will not execute. */ - if( ( status == MQTTSuccess ) && - ( pIncomingPacketStore->lengthReadComplete == true ) ) + if( status == MQTTSuccess ) { - incomingPacket.pRemainingData = pContext->networkBuffer.pBuffer; - incomingPacket.type = pIncomingPacketStore->type; - incomingPacket.remainingLength = pIncomingPacketStore->remainingTotalPacketLength; - - pContext->lastPacketRxTime = pContext->getTime(); + incomingPacket.pRemainingData = &pContext->networkBuffer.pBuffer[ incomingPacket.headerLength ]; /* PUBLISH packets allow flags in the lower four bits. For other * packet types, they are reserved. */ - if( ( pIncomingPacketStore->type & 0xF0U ) == MQTT_PACKET_TYPE_PUBLISH ) + if( ( incomingPacket.type & 0xF0U ) == MQTT_PACKET_TYPE_PUBLISH ) { status = handleIncomingPublish( pContext, &incomingPacket ); } @@ -1522,13 +1471,13 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, status = handleIncomingAck( pContext, &incomingPacket, manageKeepAlive ); } - /* Reset the fields in the context and clean up for next packet. */ - memset( pIncomingPacketStore, 0, sizeof( MQTTStoredPacketInfo_t ) ); - /* Set the multiplier back to 1. It is used for remaining length calculation. */ - pIncomingPacketStore->multipler = 1; - /* Set the field to show that the next packet is a new packet. Old one - * has been processed. */ - pIncomingPacketStore->newPacket = true; + /* Update the index to reflect the remining bytes in the buffer. */ + pContext->index -= totalMQTTPacketLength; + + /* Move the remaining bytes to the front of the buffer. */ + memmove( pContext->networkBuffer.pBuffer, + &( pContext->networkBuffer.pBuffer[ totalMQTTPacketLength ] ), + pContext->index ); } if( status == MQTTNoDataAvailable ) @@ -2362,21 +2311,17 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ) else { pContext->controlPacketSent = false; - status = MQTTSuccess; - } - - status = receiveSingleIteration( pContext, true ); + status = receiveSingleIteration( pContext, true ); + } return status; } /*-----------------------------------------------------------*/ -MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext, - uint32_t timeoutMs ) +MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext ) { MQTTStatus_t status = MQTTBadParameter; - uint32_t entryTimeMs = 0U, remainingTimeMs = timeoutMs, elapsedTimeMs = 0U; if( pContext == NULL ) { @@ -2391,36 +2336,9 @@ MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext, LogError( ( "Invalid input parameter: MQTT context's networkBuffer must not be NULL." ) ); } else - { - entryTimeMs = pContext->getTime(); - status = MQTTSuccess; - } - - while( status == MQTTSuccess ) { status = receiveSingleIteration( pContext, false ); - - /* We don't need to break here since the status is already checked in - * the loop condition, and we do not want multiple breaks in a loop. */ - if( status != MQTTSuccess ) - { - LogError( ( "Exiting receive loop. Error status=%s", - MQTT_Status_strerror( status ) ) ); - } - else - { - /* Recalculate remaining time and check if loop should exit. This is - * done at the end so the loop will run at least a single iteration. */ - elapsedTimeMs = calculateElapsedTime( pContext->getTime(), entryTimeMs ); - - if( elapsedTimeMs >= timeoutMs ) - { - break; - } - - remainingTimeMs = timeoutMs - elapsedTimeMs; - } - } + } return status; } diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c index 7d6a6f01e..f64810158 100644 --- a/source/core_mqtt_serializer.c +++ b/source/core_mqtt_serializer.c @@ -311,9 +311,9 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, * packet is not yet fully received and decoded. Otherwise, MQTTSuccess * shows that processing of the packet was successful. */ -static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacketStore ); +static MQTTStatus_t storeRemainingLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ); /** * @brief Check if an incoming packet type is valid. @@ -775,16 +775,15 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, /*-----------------------------------------------------------*/ -static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacketStore ) +static MQTTStatus_t storeRemainingLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ) { - size_t remainingLength = pIncomingPacketStore->remainingTotalPacketLength; - size_t multiplier = pIncomingPacketStore->multipler; - size_t bytesDecoded = pIncomingPacketStore->totalLengthBytesRead; + size_t remainingLength = 0; + size_t multiplier = 1; + size_t bytesDecoded = 0; size_t expectedSize = 0; uint8_t encodedByte = 0; - int32_t bytesReceived = 0; MQTTStatus_t status = MQTTSuccess; /* This algorithm is copied from the MQTT v3.1.1 spec. */ @@ -794,39 +793,23 @@ static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, { remainingLength = MQTT_REMAINING_LENGTH_INVALID; - /* Complete, albeit incorrect, length has been read. */ - pIncomingPacketStore->lengthReadComplete = true; - status = MQTTBadResponse; } else { - bytesReceived = recvFunc( pNetworkContext, &encodedByte, 1U ); - - if( bytesReceived == 1 ) + if( *pIndex > ( bytesDecoded + 1 ) ) { + /* Get the next byte. It is at the next position after the bytes + * decoded till now since the header of one byte was read before. */ + encodedByte = pBuffer[ bytesDecoded + 1 ]; + remainingLength += ( ( size_t ) encodedByte & 0x7FU ) * multiplier; multiplier *= 128U; bytesDecoded++; } else { - if( bytesReceived == 0 ) - { - status = MQTTIncomingRecvIncomplete; - } - else - { - /* Bubble up the error to the user. */ - status = MQTTBadResponse; - } - - /* In case nothing is received from the transport interface, - * save the state. */ - pIncomingPacketStore->multipler = multiplier; - pIncomingPacketStore->remainingTotalPacketLength = remainingLength; - pIncomingPacketStore->totalLengthBytesRead = bytesDecoded; - pIncomingPacketStore->lengthReadComplete = false; + status = MQTTNeedMoreBytes; } } @@ -841,15 +824,6 @@ static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, if( status == MQTTSuccess ) { - /* If this is the last byte, then the length has been fully received. - * Fill in the data in the context. - */ - pIncomingPacketStore->lengthReadComplete = true; - /* Reset the multiplier. */ - pIncomingPacketStore->multipler = 1; - pIncomingPacketStore->remainingTotalPacketLength = remainingLength; - pIncomingPacketStore->bytesPendingRecv = remainingLength; - /* Check that the decoded remaining length conforms to the MQTT specification. */ expectedSize = remainingLengthEncodedSize( remainingLength ); @@ -857,6 +831,11 @@ static MQTTStatus_t storeRemainingLength( TransportRecv_t recvFunc, { status = MQTTBadResponse; } + else + { + pIncomingPacket->remainingLength = remainingLength; + pIncomingPacket->headerLength = bytesDecoded + 1; + } } return status; @@ -2524,76 +2503,56 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, /*-----------------------------------------------------------*/ -MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacket ) +MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ) { MQTTStatus_t status = MQTTSuccess; - int32_t bytesReceived = 0; if( pIncomingPacket == NULL ) { LogError( ( "Invalid parameter: pIncomingPacket is NULL." ) ); status = MQTTBadParameter; } + else if( pIndex == NULL ) + { + LogError( ( "Invalid parameter: pIndex is NULL." ) ); + status = MQTTBadParameter; + } + else if( pBuffer == NULL ) + { + LogError( ( "Invalid parameter: pBuffer is NULL." ) ); + status = MQTTBadParameter; + } + /* There should be at least one byte in the buffer */ + else if( *pIndex < 1 ) + { + /* No data is available. There are 0 bytes received from the network + * receive function. */ + status = MQTTNoDataAvailable; + } else { - /* Read the first byte (type) only if this is a new packet. */ - if( pIncomingPacket->newPacket == true ) - { - /* Read a single byte. */ - bytesReceived = readFunc( pNetworkContext, - &( pIncomingPacket->type ), - 1U ); - } - else - { - /* Show that the first byte has been received. */ - bytesReceived = 1; - } + /* At least one byte is present which should be deciphered. */ + pIncomingPacket->type = pBuffer[ 0 ]; } - if( bytesReceived == 1 ) + if( status == MQTTSuccess ) { /* Check validity. */ if( incomingPacketValid( pIncomingPacket->type ) == true ) { - /* Update this field showing that this packet is not 'new'. */ - pIncomingPacket->newPacket = false; - - status = storeRemainingLength( readFunc, - pNetworkContext, + status = storeRemainingLength( pBuffer, + pIndex, pIncomingPacket ); } else { - /* Update this field showing that the next byte received will be - * treated as belonging to a new packet. */ - pIncomingPacket->newPacket = true; - LogError( ( "Incoming packet invalid: Packet type=%u.", ( unsigned int ) pIncomingPacket->type ) ); status = MQTTBadResponse; } } - else if( ( status != MQTTBadParameter ) && ( bytesReceived == 0 ) ) - { - status = MQTTNoDataAvailable; - } - - /* If the input packet was valid, then any other number of bytes received is - * a failure. */ - else if( status != MQTTBadParameter ) - { - LogError( ( "A single byte was not read from the transport: " - "transportStatus=%ld.", - ( long int ) bytesReceived ) ); - status = MQTTRecvFailed; - } - else - { - /* Empty else MISRA 15.7 */ - } return status; } diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h index b815b11f7..bf17f1ea8 100644 --- a/source/include/core_mqtt.h +++ b/source/include/core_mqtt.h @@ -228,6 +228,7 @@ typedef struct MQTTContext uint32_t pingReqSendTimeMs; /**< @brief Timestamp of the last sent PINGREQ. */ bool waitingForPingResp; /**< @brief If the library is currently awaiting a PINGRESP. */ MQTTStoredPacketInfo_t lastRxPacket; + size_t index; } MQTTContext_t; /** @@ -735,8 +736,7 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ); * @endcode */ /* @[declare_mqtt_receiveloop] */ -MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext, - uint32_t timeoutMs ); +MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext ); /* @[declare_mqtt_receiveloop] */ /** diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index 8b9d32ce2..d0975f197 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -95,18 +95,18 @@ struct MQTTPacketInfo; */ typedef enum MQTTStatus { - MQTTSuccess = 0, /**< Function completed successfully. */ - MQTTBadParameter, /**< At least one parameter was invalid. */ - MQTTNoMemory, /**< A provided buffer was too small. */ - MQTTSendFailed, /**< The transport send function failed. */ - MQTTRecvFailed, /**< The transport receive function failed. */ - MQTTBadResponse, /**< An invalid packet was received from the server. */ - MQTTServerRefused, /**< The server refused a CONNECT or SUBSCRIBE. */ - MQTTNoDataAvailable, /**< No data available from the transport interface. */ - MQTTIllegalState, /**< An illegal state in the state record. */ - MQTTStateCollision, /**< A collision with an existing state record entry. */ + MQTTSuccess = 0, /**< Function completed successfully. */ + MQTTBadParameter, /**< At least one parameter was invalid. */ + MQTTNoMemory, /**< A provided buffer was too small. */ + MQTTSendFailed, /**< The transport send function failed. */ + MQTTRecvFailed, /**< The transport receive function failed. */ + MQTTBadResponse, /**< An invalid packet was received from the server. */ + MQTTServerRefused, /**< The server refused a CONNECT or SUBSCRIBE. */ + MQTTNoDataAvailable, /**< No data available from the transport interface. */ + MQTTIllegalState, /**< An illegal state in the state record. */ + MQTTStateCollision, /**< A collision with an existing state record entry. */ MQTTKeepAliveTimeout, /**< Timeout while waiting for PINGRESP. */ - MQTTIncomingRecvIncomplete /**< Error to show that the MQTT_ProcessLoop has received incomplete data. */ + MQTTNeedMoreBytes /**< Error to show that the MQTT_ProcessLoop has received incomplete data. */ } MQTTStatus_t; /** @@ -264,6 +264,8 @@ typedef struct MQTTPacketInfo * @brief Length of remaining serialized data. */ size_t remainingLength; + + size_t headerLength; } MQTTPacketInfo_t; @@ -1238,9 +1240,9 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, * #MQTTBadResponse if an invalid packet is read, and * #MQTTNoDataAvailable if there is nothing to read. */ -MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( TransportRecv_t readFunc, - NetworkContext_t * pNetworkContext, - MQTTStoredPacketInfo_t * pIncomingPacket ); +MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( uint8_t * pBuffer, + size_t * index, + MQTTPacketInfo_t * pIncomingPacket ); /* *INDENT-OFF* */ #ifdef __cplusplus From 0e3082b18ec307f5cd595b456500090b6107c5a8 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Wed, 3 Aug 2022 20:42:28 -0700 Subject: [PATCH 04/16] Clean up --- source/core_mqtt.c | 2 +- source/include/core_mqtt.h | 7 +++-- source/include/core_mqtt_serializer.h | 44 ++------------------------- 3 files changed, 9 insertions(+), 44 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index fc94c4ce4..398e313b7 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -117,7 +117,7 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, size_t remainingLength, uint32_t timeoutMs ); -static MQTTStatus_t discardStoredPacket( const MQTTContext_t * pContext, +static MQTTStatus_t discardStoredPacket( MQTTContext_t * pContext, MQTTPacketInfo_t * pPacketInfo ); /** * @brief Receive a packet from the transport interface. diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h index bf17f1ea8..c73858981 100644 --- a/source/include/core_mqtt.h +++ b/source/include/core_mqtt.h @@ -223,12 +223,15 @@ typedef struct MQTTContext */ bool controlPacketSent; + /** + * @brief Index to keep track of the number of bytes received in network buffer. + */ + size_t index; + /* Keep alive members. */ uint16_t keepAliveIntervalSec; /**< @brief Keep Alive interval. */ uint32_t pingReqSendTimeMs; /**< @brief Timestamp of the last sent PINGREQ. */ bool waitingForPingResp; /**< @brief If the library is currently awaiting a PINGRESP. */ - MQTTStoredPacketInfo_t lastRxPacket; - size_t index; } MQTTContext_t; /** diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index d0975f197..b2523af16 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -265,50 +265,12 @@ typedef struct MQTTPacketInfo */ size_t remainingLength; - size_t headerLength; -} MQTTPacketInfo_t; - - -typedef struct MQTTStoredPacketInfo -{ /** - * @brief This boolean value represents whether any data has been received - * or not. + * @brief The length of the MQTT header including the type and length. */ - bool newPacket; + size_t headerLength; +} MQTTPacketInfo_t; - /** - * @brief Whether the complete length field has been read or not. - */ - bool lengthReadComplete; - - /** - * @brief Type of the packet being received. First byte of the header. - */ - uint8_t type; - - /** - * @brief How many (1-4) bytes have been read for the length. - */ - size_t totalLengthBytesRead; - - /** - * @brief The value of multipler used to calculate remaining bytes. - */ - size_t multipler; - - /** - * @brief Total number of bytes in the packet. This is calculated using - * length[4] array. - */ - size_t remainingTotalPacketLength; - - /** - * @brief Total number of bytes which are yet to be received from the - * socket. - */ - size_t bytesPendingRecv; -} MQTTStoredPacketInfo_t; /** * @brief Get the size and Remaining Length of an MQTT CONNECT packet. * From 0139fe13871a405921350e73b6438491c84f350a Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Wed, 3 Aug 2022 20:47:58 -0700 Subject: [PATCH 05/16] Renamed functions to make them more coherent with their function --- source/core_mqtt.c | 6 +++--- source/core_mqtt_serializer.c | 24 ++++++++++++------------ source/include/core_mqtt_serializer.h | 6 +++--- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index 398e313b7..e662221e7 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -1410,9 +1410,9 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, /* Update the number of bytes in the MQTT fixed buffer. */ pContext->index += recvBytes; - status = MQTT_StoreIncomingPacketTypeAndLength( pContext->networkBuffer.pBuffer, - &pContext->index, - &incomingPacket ); + status = MQTT_ProcessIncomingPacketTypeAndLength( pContext->networkBuffer.pBuffer, + &pContext->index, + &incomingPacket ); totalMQTTPacketLength = incomingPacket.remainingLength + incomingPacket.headerLength; } diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c index f64810158..ba4d5ba25 100644 --- a/source/core_mqtt_serializer.c +++ b/source/core_mqtt_serializer.c @@ -311,9 +311,9 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, * packet is not yet fully received and decoded. Otherwise, MQTTSuccess * shows that processing of the packet was successful. */ -static MQTTStatus_t storeRemainingLength( uint8_t * pBuffer, - size_t * pIndex, - MQTTPacketInfo_t * pIncomingPacket ); +static MQTTStatus_t processRemainingLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ); /** * @brief Check if an incoming packet type is valid. @@ -775,9 +775,9 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, /*-----------------------------------------------------------*/ -static MQTTStatus_t storeRemainingLength( uint8_t * pBuffer, - size_t * pIndex, - MQTTPacketInfo_t * pIncomingPacket ) +static MQTTStatus_t processRemainingLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ) { size_t remainingLength = 0; size_t multiplier = 1; @@ -2503,9 +2503,9 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, /*-----------------------------------------------------------*/ -MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( uint8_t * pBuffer, - size_t * pIndex, - MQTTPacketInfo_t * pIncomingPacket ) +MQTTStatus_t MQTT_ProcessIncomingPacketTypeAndLength( uint8_t * pBuffer, + size_t * pIndex, + MQTTPacketInfo_t * pIncomingPacket ) { MQTTStatus_t status = MQTTSuccess; @@ -2542,9 +2542,9 @@ MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( uint8_t * pBuffer, /* Check validity. */ if( incomingPacketValid( pIncomingPacket->type ) == true ) { - status = storeRemainingLength( pBuffer, - pIndex, - pIncomingPacket ); + status = processRemainingLength( pBuffer, + pIndex, + pIncomingPacket ); } else { diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index b2523af16..f9231e00e 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -1202,9 +1202,9 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, * #MQTTBadResponse if an invalid packet is read, and * #MQTTNoDataAvailable if there is nothing to read. */ -MQTTStatus_t MQTT_StoreIncomingPacketTypeAndLength( uint8_t * pBuffer, - size_t * index, - MQTTPacketInfo_t * pIncomingPacket ); +MQTTStatus_t MQTT_ProcessIncomingPacketTypeAndLength( uint8_t * pBuffer, + size_t * index, + MQTTPacketInfo_t * pIncomingPacket ); /* *INDENT-OFF* */ #ifdef __cplusplus From 211f64ab122df2c266356b95618e5f6a2702055c Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Wed, 3 Aug 2022 22:43:21 -0700 Subject: [PATCH 06/16] Remove unused function declarations --- source/core_mqtt.c | 6 ------ 1 file changed, 6 deletions(-) diff --git a/source/core_mqtt.c b/source/core_mqtt.c index e662221e7..cc15ccd3e 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -101,9 +101,6 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType ); static int32_t recvExact( const MQTTContext_t * pContext, size_t bytesToRecv ); -static int32_t processPacket( MQTTContext_t * pContext, - MQTTPacketInfo_t * pIncomingPacket ); - /** * @brief Discard a packet from the transport interface. * @@ -132,9 +129,6 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext, MQTTPacketInfo_t incomingPacket, uint32_t remainingTimeMs ); -static MQTTStatus_t receiveAndStorePacket( MQTTContext_t * pContext, - MQTTPacketInfo_t * pIncomingPacket ); - /** * @brief Get the correct ack type to send. * From 8ddd781a909eb02017972f2de98ce710a4fa38c8 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere Date: Thu, 11 Aug 2022 00:15:31 +0000 Subject: [PATCH 07/16] Fixed failing CI checks from previous commits except unit-test --- lexicon.txt | 1 + source/core_mqtt.c | 20 +++++++++++++++----- source/core_mqtt_serializer.c | 11 ++++++----- source/include/core_mqtt.h | 4 ---- source/include/core_mqtt_serializer.h | 12 ++++++------ 5 files changed, 28 insertions(+), 20 deletions(-) diff --git a/lexicon.txt b/lexicon.txt index f3e782b6b..46adb9881 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -153,6 +153,7 @@ mqttfixedbuffer mqttgetcurrenttimefunc mqttillegalstate mqttkeepalivetimeout +mqttneedmorebytes mqttnodataavailable mqttnomemory mqttnotconnected diff --git a/source/core_mqtt.c b/source/core_mqtt.c index 1548bb106..e919aaed8 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -114,8 +114,17 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, size_t remainingLength, uint32_t timeoutMs ); +/** + * @brief Discard a packet from the MQTT buffer and the transport interface. + * + * @param[in] pContext MQTT Connection context. + * @param[in] pPacketInfo Information struct of the packet to be discarded. + * + * @return #MQTTRecvFailed or #MQTTNoDataAvailable. + */ static MQTTStatus_t discardStoredPacket( MQTTContext_t * pContext, MQTTPacketInfo_t * pPacketInfo ); + /** * @brief Receive a packet from the transport interface. * @@ -202,7 +211,6 @@ static MQTTStatus_t handleIncomingAck( MQTTContext_t * pContext, * @brief Run a single iteration of the receive loop. * * @param[in] pContext MQTT Connection context. - * @param[in] remainingTimeMs Remaining time for the loop in milliseconds. * @param[in] manageKeepAlive Flag indicating if keep alive should be handled. * * @return #MQTTRecvFailed if a network error occurs during reception; @@ -852,6 +860,8 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext, return status; } +/*-----------------------------------------------------------*/ + static MQTTStatus_t discardStoredPacket( MQTTContext_t * pContext, MQTTPacketInfo_t * pPacketInfo ) { @@ -1403,7 +1413,7 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, { /* Update the number of bytes in the MQTT fixed buffer. */ pContext->index += recvBytes; - + status = MQTT_ProcessIncomingPacketTypeAndLength( pContext->networkBuffer.pBuffer, &pContext->index, &incomingPacket ); @@ -1471,7 +1481,7 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, /* Move the remaining bytes to the front of the buffer. */ memmove( pContext->networkBuffer.pBuffer, &( pContext->networkBuffer.pBuffer[ totalMQTTPacketLength ] ), - pContext->index ); + pContext->index ); } if( status == MQTTNoDataAvailable ) @@ -2319,7 +2329,7 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ) { pContext->controlPacketSent = false; status = receiveSingleIteration( pContext, true ); - } + } return status; } @@ -2345,7 +2355,7 @@ MQTTStatus_t MQTT_ReceiveLoop( MQTTContext_t * pContext ) else { status = receiveSingleIteration( pContext, false ); - } + } return status; } diff --git a/source/core_mqtt_serializer.c b/source/core_mqtt_serializer.c index ba4d5ba25..c8d02475c 100644 --- a/source/core_mqtt_serializer.c +++ b/source/core_mqtt_serializer.c @@ -302,12 +302,13 @@ static size_t getRemainingLength( TransportRecv_t recvFunc, * @brief Retrieves, decodes and stores the Remaining Length from the network * interface by reading a single byte at a time. * - * @param[in] recvFunc Network interface receive function. - * @param[in] pNetworkContext Network interface context to the receive function. - * @param[in] pIncomingPacketStore Strucutre used to hold the fields of the + * @param[in] pBuffer The buffer holding the raw data to be processed + * @param[in] pIndex Pointer to the index within the buffer to marking the end of raw data + * available. + * @param[in] pIncomingPacket Structure used to hold the fields of the * incoming packet. * - * @return MQTTIncomingRecvIncomplete is returned to show that the incoming + * @return MQTTNeedMoreBytes is returned to show that the incoming * packet is not yet fully received and decoded. Otherwise, MQTTSuccess * shows that processing of the packet was successful. */ @@ -810,7 +811,7 @@ static MQTTStatus_t processRemainingLength( uint8_t * pBuffer, else { status = MQTTNeedMoreBytes; - } + } } /* If the response is incorrect, or no more data is available, then diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h index d6ef7b7f6..d13f75c0d 100644 --- a/source/include/core_mqtt.h +++ b/source/include/core_mqtt.h @@ -642,8 +642,6 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext ); * In that case, the #MQTT_ReceiveLoop API function should be used instead. * * @param[in] pContext Initialized and connected MQTT context. - * @param[in] timeoutMs Minimum time in milliseconds that the receive loop will - * run, unless an error occurs. * * @note Calling this function blocks the calling context for a time period that * depends on the passed @p timeoutMs, the configuration macros, #MQTT_RECV_POLLING_TIMEOUT_MS @@ -701,8 +699,6 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext ); * and #MQTT_SEND_RETRY_TIMEOUT_MS timeout configurations MUST be set to 0. * * @param[in] pContext Initialized and connected MQTT context. - * @param[in] timeoutMs Minimum time in milliseconds that the receive loop will - * run, unless an error occurs. * * @note Calling this function blocks the calling context for a time period that * depends on the passed @p timeoutMs, the configuration macros, #MQTT_RECV_POLLING_TIMEOUT_MS diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index f9231e00e..bef37193e 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -1190,11 +1190,11 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, * #MQTTPacketInfo_t.type and #MQTTPacketInfo_t.remainingLength. A * #MQTTPacketInfo_t is not valid until this routine has been invoked. * - * @param[in] readFunc Transport layer read function pointer. - * @param[in] pNetworkContext The network context pointer provided by the application. - * @param[out] pIncomingPacket Pointer to MQTTStoredPacketInfo_t structure. This is - * where type, remaining length and packet identifier are stored and used in later - * iterations. + * @param[in] pBuffer The buffer holding the raw data to be processed + * @param[in] pIndex Pointer to the index within the buffer to marking the end of raw data + * available. + * @param[in] pIncomingPacket Strucutre used to hold the fields of the + * incoming packet. * * @return #MQTTSuccess on successful extraction of type and length, * #MQTTBadParameter if @p pIncomingPacket is invalid, @@ -1203,7 +1203,7 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, * #MQTTNoDataAvailable if there is nothing to read. */ MQTTStatus_t MQTT_ProcessIncomingPacketTypeAndLength( uint8_t * pBuffer, - size_t * index, + size_t * pIndex, MQTTPacketInfo_t * pIncomingPacket ); /* *INDENT-OFF* */ From 151a802a2a9c78e28e9d33a687897ca6f21be0a6 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 11 Aug 2022 00:27:21 +0000 Subject: [PATCH 08/16] Fixed spell check and updated size-table --- docs/doxygen/include/size_table.md | 8 ++++---- lexicon.txt | 1 + source/core_mqtt.c | 2 +- source/include/core_mqtt_serializer.h | 2 +- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md index 1fc9af4f3..3c4566ad8 100644 --- a/docs/doxygen/include/size_table.md +++ b/docs/doxygen/include/size_table.md @@ -19,12 +19,12 @@ core_mqtt_serializer.c -
2.5K
-
2.0K
+
2.7K
+
2.1K
Total estimates -
7.1K
 -
5.8K
 +
7.3K
 +
5.9K
 diff --git a/lexicon.txt b/lexicon.txt index 46adb9881..86cd3b913 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -234,6 +234,7 @@ pfilterindex pfixedbuffer pheadersize pincomingpacket +pindex pingreq pingreqs pingreqsendtimems diff --git a/source/core_mqtt.c b/source/core_mqtt.c index e919aaed8..6f794a645 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -1475,7 +1475,7 @@ static MQTTStatus_t receiveSingleIteration( MQTTContext_t * pContext, status = handleIncomingAck( pContext, &incomingPacket, manageKeepAlive ); } - /* Update the index to reflect the remining bytes in the buffer. */ + /* Update the index to reflect the remaining bytes in the buffer. */ pContext->index -= totalMQTTPacketLength; /* Move the remaining bytes to the front of the buffer. */ diff --git a/source/include/core_mqtt_serializer.h b/source/include/core_mqtt_serializer.h index bef37193e..b62ae2853 100644 --- a/source/include/core_mqtt_serializer.h +++ b/source/include/core_mqtt_serializer.h @@ -1193,7 +1193,7 @@ MQTTStatus_t MQTT_GetIncomingPacketTypeAndLength( TransportRecv_t readFunc, * @param[in] pBuffer The buffer holding the raw data to be processed * @param[in] pIndex Pointer to the index within the buffer to marking the end of raw data * available. - * @param[in] pIncomingPacket Strucutre used to hold the fields of the + * @param[in] pIncomingPacket Structure used to hold the fields of the * incoming packet. * * @return #MQTTSuccess on successful extraction of type and length, From 5637b145717a4b3c7ab6ffe00ebd64f54a2e2e34 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 11 Aug 2022 00:46:54 +0000 Subject: [PATCH 09/16] Fix CBMC proofs --- .../proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c | 9 +-------- .../proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c | 9 +-------- 2 files changed, 2 insertions(+), 16 deletions(-) diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c b/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c index 088aaff65..2b48da1fe 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c +++ b/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c @@ -30,16 +30,9 @@ void harness() { MQTTContext_t * pContext; - uint32_t timeoutMs; pContext = allocateMqttContext( NULL ); __CPROVER_assume( isValidMqttContext( pContext ) ); - /* 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 - * safety can be proven in only a few iterations. Please see this proof's - * Makefile for more information. */ - __CPROVER_assume( timeoutMs < MQTT_RECEIVE_TIMEOUT ); - - MQTT_ProcessLoop( pContext, timeoutMs ); + MQTT_ProcessLoop( pContext ); } diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c b/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c index 0859beb3b..3eeeeba30 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c @@ -30,16 +30,9 @@ void harness() { MQTTContext_t * pContext; - uint32_t timeoutMs; pContext = allocateMqttContext( NULL ); __CPROVER_assume( isValidMqttContext( pContext ) ); - /* 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 - * safety can be proven in only a few iterations. Please see this proof's - * Makefile for more information. */ - __CPROVER_assume( timeoutMs < MQTT_RECEIVE_TIMEOUT ); - - MQTT_ReceiveLoop( pContext, timeoutMs ); + MQTT_ReceiveLoop( pContext ); } From f69a32a7fbc48bdf630e45554d29839bbe4869d6 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 11 Aug 2022 03:31:55 +0000 Subject: [PATCH 10/16] Empty-Commit to trigger CBMC proofs From a4dbd53b6d7ec86aa0f11724bf92ca991c677c44 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 11 Aug 2022 22:58:37 +0000 Subject: [PATCH 11/16] Fix loop unwinding values in the Makefile --- test/cbmc/proofs/MQTT_ProcessLoop/Makefile | 5 ++--- test/cbmc/proofs/MQTT_ReceiveLoop/Makefile | 5 ++--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile index 4848d08be..3103462e2 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile @@ -49,8 +49,7 @@ REMOVE_FUNCTION_BODY += MQTT_Ping REMOVE_FUNCTION_BODY += MQTT_DeserializeAck REMOVE_FUNCTION_BODY += MQTT_SerializeAck -UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardStoredPacket.0:$(MAX_NETWORK_RECV_TRIES) UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES) # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error @@ -61,7 +60,7 @@ UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TR # The getRemainingLength loop is unwound 5 times because getRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_getRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_processRemainingLength.0:5 # These loops will run for the maximum number of publishes pending # acknowledgements plus one. This value is set in # test/cbmc/include/core_mqtt_config.h. diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile index 3d5c9dcbe..4950a7238 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile @@ -31,8 +31,7 @@ REMOVE_FUNCTION_BODY += MQTT_DeserializeAck REMOVE_FUNCTION_BODY += MQTT_SerializeAck # The loops below are unwound once more than the exclusive timeout bound. -UNWINDSET += MQTT_ReceiveLoop.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardStoredPacket.0:$(MAX_NETWORK_RECV_TRIES) UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES) # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error @@ -43,7 +42,7 @@ UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TR # The getRemainingLength loop is unwound 5 times because getRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_getRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_processRemainingLength.0:5 # These loops will run for the maximum number of publishes pending acknowledgement. # This is set in test/cbmc/include/core_mqtt_config.h. UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) From af119f08fc1d0914fd68d32d343f7032cf9ad2ef Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 11 Aug 2022 23:52:42 +0000 Subject: [PATCH 12/16] Add upper bound on the buffer size of MQTT --- test/cbmc/sources/mqtt_cbmc_state.c | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index 5da1fc0b3..f8bc9575f 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -50,6 +50,10 @@ #define REMAINING_LENGTH_MAX CBMC_MAX_OBJECT_SIZE #endif +#ifndef MAXIMUM_SOCKET_MEMORY + #define MAXIMUM_SOCKET_MEMORY ( 100 * 1024 ) +#endif + MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo ) { if( pPacketInfo == NULL ) @@ -143,6 +147,11 @@ bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer ) { bool isValid = true; + if( pFixedBuffer->size >= MAXIMUM_SOCKET_MEMORY ) + { + isValid = false; + } + return isValid; } From 64f91116aff43f5b92a355cf066b2a654d704925 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Fri, 12 Aug 2022 06:13:23 +0000 Subject: [PATCH 13/16] Increase minimum limit on buffer size to >0 --- test/cbmc/sources/mqtt_cbmc_state.c | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index f8bc9575f..5575b9274 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -50,10 +50,6 @@ #define REMAINING_LENGTH_MAX CBMC_MAX_OBJECT_SIZE #endif -#ifndef MAXIMUM_SOCKET_MEMORY - #define MAXIMUM_SOCKET_MEMORY ( 100 * 1024 ) -#endif - MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo ) { if( pPacketInfo == NULL ) @@ -137,6 +133,7 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ) if( pFixedBuffer != NULL ) { + __CPROVER_assume( pFixedBuffer->size > 0 ); pFixedBuffer->pBuffer = malloc( pFixedBuffer->size ); } @@ -147,11 +144,6 @@ bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer ) { bool isValid = true; - if( pFixedBuffer->size >= MAXIMUM_SOCKET_MEMORY ) - { - isValid = false; - } - return isValid; } From 3c1ab45ea0a7dd543cc61469c7770a127bbc199b Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Fri, 12 Aug 2022 07:14:17 +0000 Subject: [PATCH 14/16] Add upper bound on the size of the buffer as well --- test/cbmc/sources/mqtt_cbmc_state.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index 5575b9274..19f62ee9d 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -134,6 +134,10 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ) if( pFixedBuffer != NULL ) { __CPROVER_assume( pFixedBuffer->size > 0 ); + /* The buffer should be less than an signed 32-bit integer value since the + * transport interface cannot return more than that value. */ + __CPROVER_assume( pFixedBuffer->size < 0x7FFFFFFF ); + pFixedBuffer->pBuffer = malloc( pFixedBuffer->size ); } From 9c16611a4c7cf548460b100fca77c4333419cb1c Mon Sep 17 00:00:00 2001 From: "Mark R. Tuttle" Date: Fri, 19 Aug 2022 18:38:59 +0000 Subject: [PATCH 15/16] CBMC: Add memmove stub to accelerate coverage The commit adds a stub for memmove accelerate CBMC coverage calculation. Without this stub, coverage for `MQTT_ProcessLoop` and `MQTT_ReceiveLoop` fails to converge (gets stuck generating the SAT formula for the memmove in `receiveSingleIteration`). This stub checks that src and dst are nonnull pointers and havocs dst. --- test/cbmc/proofs/MQTT_ProcessLoop/Makefile | 2 ++ test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json | 4 +++- test/cbmc/proofs/MQTT_ReceiveLoop/Makefile | 2 ++ test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json | 3 ++- test/cbmc/stubs/memmove.c | 8 ++++++++ 5 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test/cbmc/stubs/memmove.c diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile index 3103462e2..bfb14f7e4 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile @@ -48,6 +48,7 @@ INCLUDES += REMOVE_FUNCTION_BODY += MQTT_Ping REMOVE_FUNCTION_BODY += MQTT_DeserializeAck REMOVE_FUNCTION_BODY += MQTT_SerializeAck +REMOVE_FUNCTION_BODY += memmove # Use stub UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardStoredPacket.0:$(MAX_NETWORK_RECV_TRIES) UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES) @@ -72,6 +73,7 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memmove.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_serializer.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json b/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json index 8f4faa1b0..df53905c0 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json @@ -1,6 +1,8 @@ { "expected-missing-functions": [ - + "MQTT_Ping", + "MQTT_SerializeAck", + "MQTT_DeserializeAck" ], "proof-name": "MQTT_ProcessLoop", "proof-root": "test/cbmc/proofs" diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile index 4950a7238..d8778405d 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile @@ -29,6 +29,7 @@ INCLUDES += # These functions have their memory saftey proven in other harnesses. REMOVE_FUNCTION_BODY += MQTT_DeserializeAck REMOVE_FUNCTION_BODY += MQTT_SerializeAck +REMOVE_FUNCTION_BODY += memmove # Use stub # The loops below are unwound once more than the exclusive timeout bound. UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardStoredPacket.0:$(MAX_NETWORK_RECV_TRIES) @@ -53,6 +54,7 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memmove.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_serializer.c PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json b/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json index 882c3810d..5d7cc94f7 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json @@ -1,6 +1,7 @@ { "expected-missing-functions": [ - + "MQTT_DeserializeAck", + "MQTT_SerializeAck" ], "proof-name": "MQTT_ReceiveLoop", "proof-root": "test/cbmc/proofs" diff --git a/test/cbmc/stubs/memmove.c b/test/cbmc/stubs/memmove.c new file mode 100644 index 000000000..944cb1f3d --- /dev/null +++ b/test/cbmc/stubs/memmove.c @@ -0,0 +1,8 @@ +#include + +void * memmove ( void * destination, const void * source, size_t num ) { + __CPROVER_assert(destination, "memmove destination is nonnull"); + __CPROVER_assert(source, "memmove source is nonnull"); + __CPROVER_havoc_object(destination); + return destination; +} From cbaa2cd627397d54c1db6cc23b26e7927f04ca32 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Fri, 19 Aug 2022 19:19:51 +0000 Subject: [PATCH 16/16] Fix formatting --- test/cbmc/sources/mqtt_cbmc_state.c | 1 + test/cbmc/stubs/memmove.c | 13 ++++++++----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index 19f62ee9d..026b363b2 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -134,6 +134,7 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ) if( pFixedBuffer != NULL ) { __CPROVER_assume( pFixedBuffer->size > 0 ); + /* The buffer should be less than an signed 32-bit integer value since the * transport interface cannot return more than that value. */ __CPROVER_assume( pFixedBuffer->size < 0x7FFFFFFF ); diff --git a/test/cbmc/stubs/memmove.c b/test/cbmc/stubs/memmove.c index 944cb1f3d..00412c3ee 100644 --- a/test/cbmc/stubs/memmove.c +++ b/test/cbmc/stubs/memmove.c @@ -1,8 +1,11 @@ #include -void * memmove ( void * destination, const void * source, size_t num ) { - __CPROVER_assert(destination, "memmove destination is nonnull"); - __CPROVER_assert(source, "memmove source is nonnull"); - __CPROVER_havoc_object(destination); - return destination; +void * memmove( void * destination, + const void * source, + size_t num ) +{ + __CPROVER_assert( destination, "memmove destination is nonnull" ); + __CPROVER_assert( source, "memmove source is nonnull" ); + __CPROVER_havoc_object( destination ); + return destination; }