From 7280d260be5059d63a73557b68e743a1317e8053 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 19:16:28 +0000 Subject: [PATCH 01/11] Add files for proof of MQTT_GetSubAckStatusCodes API function --- .../MQTT_GetSubAckStatusCodes_harness.c | 28 +++++++++++++++++++ .../proofs/MQTT_GetSubAckStatusCodes/Makefile | 16 +++++++++++ .../MQTT_GetSubAckStatusCodes/README.md | 10 +++++++ .../cbmc-viewer.json | 7 +++++ 4 files changed, 61 insertions(+) create mode 100644 libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c create mode 100644 libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile create mode 100644 libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/README.md create mode 100644 libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c new file mode 100644 index 0000000000..ab15cfb89b --- /dev/null +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -0,0 +1,28 @@ +/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */ +/* SPDX-License-Identifier: Apache-2.0 */ + +/* + * Insert copyright notice + */ + +/** + * @file MQTT_GetSubAckStatusCodes_harness.c + * @brief Implements the proof harness for MQTT_GetSubAckStatusCodes function. + */ + +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTPacketInfo_t * pSubackPacket; + uint8_t * pPayloadStart; + uint16_t payloadSize; + + pSubackPacket = allocateMqttPacketInfo( NULL ); + __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); + + MQTT_GetSubAckStatusCodes( pSubackPacket, + &pPayloadStart, + &payloadSize ); +} diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile new file mode 100644 index 0000000000..b12f417ca7 --- /dev/null +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile @@ -0,0 +1,16 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_GetSubAckStatusCodes_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/../../../../../../../src/mqtt.c + +include ../Makefile.common \ No newline at end of file diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/README.md b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/README.md new file mode 100644 index 0000000000..57f2c3af66 --- /dev/null +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/README.md @@ -0,0 +1,10 @@ +MQTT_GetSubAckStatusCodes proof +============== + +This directory contains a memory safety proof for MQTT_GetSubAckStatusCodes. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. \ No newline at end of file diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json new file mode 100644 index 0000000000..d49f007bd1 --- /dev/null +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_GetSubAckStatusCodes", + "proof-root": "../../../../.." +} \ No newline at end of file From 04ada05622bc6f36db77c85dc114e3198be950a4 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 19:23:52 +0000 Subject: [PATCH 02/11] Update Makefile for proof to fix proof build failure --- .../mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile index b12f417ca7..fbf77082b9 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile @@ -11,6 +11,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/../../../../../../../src/mqtt.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c include ../Makefile.common \ No newline at end of file From 9eb4f493818a394b0e86668d9f9526521e416c12 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 20:50:18 +0000 Subject: [PATCH 03/11] Add .yaml file for new proof to enable CI run --- .../mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml new file mode 100644 index 0000000000..87089222ce --- /dev/null +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. \ No newline at end of file From 82ba66bdf6a8caf8b29fdc6abe7078a5514a5950 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 21:16:58 +0000 Subject: [PATCH 04/11] Add copyrights to files --- .../MQTT_GetSubAckStatusCodes_harness.c | 22 +++++++++++++---- .../proofs/MQTT_GetSubAckStatusCodes/Makefile | 24 ++++++++++++++++--- 2 files changed, 39 insertions(+), 7 deletions(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index ab15cfb89b..6bb88ba7d0 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -1,8 +1,22 @@ -/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */ -/* SPDX-License-Identifier: Apache-2.0 */ - /* - * Insert copyright notice + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ /** diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile index fbf77082b9..3c8ad8d093 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile @@ -1,5 +1,23 @@ -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 +# +# Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person obtaining a copy of +# this software and associated documentation files (the "Software"), to deal in +# the Software without restriction, including without limitation the rights to +# use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +# the Software, and to permit persons to whom the Software is furnished to do so, +# subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +# FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +# COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +# IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +# HARNESS_ENTRY=harness HARNESS_FILE=MQTT_GetSubAckStatusCodes_harness @@ -14,4 +32,4 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -include ../Makefile.common \ No newline at end of file +include ../Makefile.common From 797ba2ae7fd0ffbff0dfe963112f029d9fba1e05 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 21:29:38 +0000 Subject: [PATCH 05/11] Add newlines to .yaml and .json files --- .../mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml | 2 +- .../mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml index 87089222ce..7eeb12ad71 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-batch.yaml @@ -1,2 +1,2 @@ # This file marks this directory as containing a CBMC proof. -# The contents of this file will be generated by continuous integration. \ No newline at end of file +# The contents of this file will be generated by continuous integration. diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json index d49f007bd1..95db5bf1d9 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/cbmc-viewer.json @@ -4,4 +4,4 @@ ], "proof-name": "MQTT_GetSubAckStatusCodes", "proof-root": "../../../../.." -} \ No newline at end of file +} From 428a1259bdfeeea3c1ca885fb34108098810a85f Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 22:38:04 +0000 Subject: [PATCH 06/11] Fix MQTT_GetSubAckStatusCodes API for parameter type based on CBMC proof finding --- .../MQTT_GetSubAckStatusCodes_harness.c | 2 +- libraries/standard/mqtt/include/mqtt.h | 60 +++++++++---------- libraries/standard/mqtt/src/mqtt.c | 4 +- 3 files changed, 33 insertions(+), 33 deletions(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 6bb88ba7d0..15ab0d6a8f 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -31,7 +31,7 @@ void harness() { MQTTPacketInfo_t * pSubackPacket; uint8_t * pPayloadStart; - uint16_t payloadSize; + size_t payloadSize; pSubackPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); diff --git a/libraries/standard/mqtt/include/mqtt.h b/libraries/standard/mqtt/include/mqtt.h index 585a43069f..e2a85c72eb 100644 --- a/libraries/standard/mqtt/include/mqtt.h +++ b/libraries/standard/mqtt/include/mqtt.h @@ -322,7 +322,7 @@ MQTTStatus_t MQTT_Init( MQTTContext_t * pContext, * * Example * @code{c} - * + * * // Variables used in this example. * MQTTStatus_t status; * MQTTConnectInfo_t connectInfo = { 0 }; @@ -336,7 +336,7 @@ MQTTStatus_t MQTT_Init( MQTTContext_t * pContext, * // Client ID must be unique to broker. This field is required. * connectInfo.pClientIdentifier = "someClientID"; * connectInfo.clientIdentifierLength = strlen( connectInfo.pClientIdentifier ); - * + * * // The following fields are optional. * // Value for keep alive. * connectInfo.keepAliveSeconds = 60; @@ -345,7 +345,7 @@ MQTTStatus_t MQTT_Init( MQTTContext_t * pContext, * connectInfo.userNameLength = strlen( connectInfo.pUserName ); * connectInfo.pPassword = "somePassword"; * connectInfo.passwordLength = strlen( connectInfo.pPassword ); - * + * * // The last will and testament is optional, it will be published by the broker * // should this client disconnect without sending a DISCONNECT packet. * willInfo.qos = MQTTQoS0; @@ -356,12 +356,12 @@ MQTTStatus_t MQTT_Init( MQTTContext_t * pContext, * * // Send the connect packet. Use 100 ms as the timeout to wait for the CONNACK packet. * status = MQTT_Connect( pContext, &connectInfo, &willInfo, 100, &sessionPresent ); - * + * * if( status == MQTTSuccess ) * { * // Since we requested a clean session, this must be false * assert( sessionPresent == false ); - * + * * // Do something with the connection. * } * @endcode @@ -386,7 +386,7 @@ MQTTStatus_t MQTT_Connect( MQTTContext_t * pContext, * #MQTTBadParameter if invalid parameters are passed; * #MQTTSendFailed if transport write failed; * #MQTTSuccess otherwise. - * + * * Example * @code{c} * @@ -398,7 +398,7 @@ MQTTStatus_t MQTT_Connect( MQTTContext_t * pContext, * MQTTContext_t * pContext; * // This is assumed to be a list of filters we want to subscribe to. * const char * filters[ NUMBER_OF_SUBSCRIPTIONS ]; - * + * * // Set each subscription. * for( int i = 0; i < NUMBER_OF_SUBSCRIPTIONS; i++ ) * { @@ -407,12 +407,12 @@ MQTTStatus_t MQTT_Connect( MQTTContext_t * pContext, * subscriptionList[ i ].pTopicFilter = filters[ i ]; * subscriptionList[ i ].topicFilterLength = strlen( filters[ i ] ); * } - * + * * // Obtain a new packet id for the subscription. * packetId = MQTT_GetPacketId( pContext ); - * + * * status = MQTT_Subscribe( pContext, &subscriptionList[ 0 ], NUMBER_OF_SUBSCRIPTIONS, packetId ); - * + * * if( status == MQTTSuccess ) * { * // We must now call MQTT_ReceiveLoop() or MQTT_ProcessLoop() to receive the SUBACK. @@ -437,29 +437,29 @@ MQTTStatus_t MQTT_Subscribe( MQTTContext_t * pContext, * #MQTTBadParameter if invalid parameters are passed; * #MQTTSendFailed if transport write failed; * #MQTTSuccess otherwise. - * + * * Example * @code{c} - * + * * // Variables used in this example. * MQTTStatus_t status; * MQTTPublishInfo_t publishInfo; * uint16_t packetId; * // This context is assumed to be initialized and connected. * MQTTContext_t * pContext; - * + * * // QoS of publish. * publishInfo.qos = MQTTQoS1; * publishInfo.pTopicName = "/some/topic/name"; * publishInfo.topicNameLength = strlen( publishInfo.pTopicName ); * publishInfo.pPayload = "Hello World!"; * publishInfo.payloadLength = strlen( "Hello World!" ); - * + * * // Packet ID is needed for QoS > 0. * packetId = MQTT_GetPacketId( pContext ); - * + * * status = MQTT_Publish( pContext, &publishInfo, packetId ); - * + * * if( status == MQTTSuccess ) * { * // Since the QoS is > 0, we will need to call MQTT_ReceiveLoop() @@ -497,7 +497,7 @@ MQTTStatus_t MQTT_Ping( MQTTContext_t * pContext ); * #MQTTBadParameter if invalid parameters are passed; * #MQTTSendFailed if transport write failed; * #MQTTSuccess otherwise. - * + * * Example * @code{c} * @@ -509,7 +509,7 @@ MQTTStatus_t MQTT_Ping( MQTTContext_t * pContext ); * MQTTContext_t * pContext; * // This is assumed to be a list of filters we want to unsubscribe from. * const char * filters[ NUMBER_OF_SUBSCRIPTIONS ]; - * + * * // Set information for each unsubscribe request. * for( int i = 0; i < NUMBER_OF_SUBSCRIPTIONS; i++ ) * { @@ -518,12 +518,12 @@ MQTTStatus_t MQTT_Ping( MQTTContext_t * pContext ); * * // The QoS field of MQTT_SubscribeInfo_t is unused for unsubscribing. * } - * + * * // Obtain a new packet id for the unsubscribe request. * packetId = MQTT_GetPacketId( pContext ); - * + * * status = MQTT_Subscribe( pContext, &unsubscribeList[ 0 ], NUMBER_OF_SUBSCRIPTIONS, packetId ); - * + * * if( status == MQTTSuccess ) * { * // We must now call MQTT_ReceiveLoop() or MQTT_ProcessLoop() to receive the UNSUBACK. @@ -566,20 +566,20 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext ); * #MQTTIllegalState if an incoming QoS 1/2 publish or ack causes an * invalid transition for the internal state machine; * #MQTTSuccess on success. - * + * * Example * @code{c} - * + * * // 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 ); - * + * * if( status != MQTTSuccess ) * { * // Determine the error. It's possible we might need to disconnect TCP. @@ -614,18 +614,18 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext, * * Example * @code{c} - * + * * // Variables used in this example. * MQTTStatus_t status; * uint32_t timeoutMs = 100; * uint32_t keepAliveMs = 60 * 1000; * // This context is assumed to be initialized and connected. * MQTTContext_t * pContext; - * + * * while( true ) * { * status = MQTT_ReceiveLoop( pContext, timeoutMs ); - * + * * if( status != MQTTSuccess ) * { * // Determine the error. It's possible we might need to disconnect TCP. @@ -638,7 +638,7 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext, * { * status = MQTT_Ping( pContext ); * } - * + * * // Other application functions. * } * } @@ -683,7 +683,7 @@ uint16_t MQTT_GetPacketId( MQTTContext_t * pContext ); */ MQTTStatus_t MQTT_GetSubAckStatusCodes( const MQTTPacketInfo_t * pSubackPacket, uint8_t ** pPayloadStart, - uint16_t * pPayloadSize ); + size_t * pPayloadSize ); /** * @brief Error code to string conversion for MQTT statuses. diff --git a/libraries/standard/mqtt/src/mqtt.c b/libraries/standard/mqtt/src/mqtt.c index a465fd6875..e1f9570a56 100644 --- a/libraries/standard/mqtt/src/mqtt.c +++ b/libraries/standard/mqtt/src/mqtt.c @@ -1977,7 +1977,7 @@ uint16_t MQTT_GetPacketId( MQTTContext_t * pContext ) MQTTStatus_t MQTT_GetSubAckStatusCodes( const MQTTPacketInfo_t * pSubackPacket, uint8_t ** pPayloadStart, - uint16_t * pPayloadSize ) + size_t * pPayloadSize ) { MQTTStatus_t status = MQTTSuccess; @@ -2025,7 +2025,7 @@ MQTTStatus_t MQTT_GetSubAckStatusCodes( const MQTTPacketInfo_t * pSubackPacket, * Therefore, we add 2 positions for the starting address of the payload, and * subtract 2 bytes from the remaining length for the length of the payload.*/ *pPayloadStart = pSubackPacket->pRemainingData + ( ( uint16_t ) sizeof( uint16_t ) ); - *pPayloadSize = ( uint16_t ) ( pSubackPacket->remainingLength - sizeof( uint16_t ) ); + *pPayloadSize = pSubackPacket->remainingLength - sizeof( uint16_t ); } return status; From ac92c7067a46b0358778f47966187c2f245c1c9e Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 22:51:03 +0000 Subject: [PATCH 07/11] Update unit test for GetSubAckStatusCodes API function --- libraries/standard/mqtt/utest/mqtt_utest.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/libraries/standard/mqtt/utest/mqtt_utest.c b/libraries/standard/mqtt/utest/mqtt_utest.c index 69b49e59f7..e02caae0ad 100644 --- a/libraries/standard/mqtt/utest/mqtt_utest.c +++ b/libraries/standard/mqtt/utest/mqtt_utest.c @@ -2126,13 +2126,13 @@ void test_MQTT_Ping_error_path( void ) /* ========================================================================== */ /** - * @brief Tests that MQTT_GetSubAckPayload works as expected in parsing the + * @brief Tests that MQTT_GetSubAckStatusCodes works as expected in parsing the * payload information of a SUBACK packet. */ -void test_MQTT_GetSubAckPayload( void ) +void test_MQTT_GetSubAckStatusCodes( void ) { MQTTPacketInfo_t mqttPacketInfo; - uint16_t payloadSize; + size_t payloadSize; uint8_t * pPayloadStart; MQTTStatus_t status = MQTTSuccess; uint8_t buffer[ 10 ] = { 0 }; From 74fe680a3be2ea55aed80bd0f78aff37e22e97c7 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 17 Aug 2020 23:14:26 +0000 Subject: [PATCH 08/11] Update harness to achieve full proof coverage for MQTT_GetSubAckStatusCodes --- .../MQTT_GetSubAckStatusCodes_harness.c | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 15ab0d6a8f..0af70cb371 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -30,13 +30,16 @@ void harness() { MQTTPacketInfo_t * pSubackPacket; - uint8_t * pPayloadStart; - size_t payloadSize; + uint8_t ** pPayloadStart; + size_t * pPayloadSize; pSubackPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); + pPayloadStart = safeMalloc( sizeof( uint8_t * ) ); + pPayloadSize = safeMalloc( sizeof( uint8_t ) ); + MQTT_GetSubAckStatusCodes( pSubackPacket, - &pPayloadStart, - &payloadSize ); + pPayloadStart, + pPayloadSize ); } From 707fcef3b87834bbce555f6a7b18b332630baf0b Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Tue, 18 Aug 2020 00:00:58 +0000 Subject: [PATCH 09/11] Change safeMalloc -> mallocCanFail in hanress --- .../MQTT_GetSubAckStatusCodes_harness.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 0af70cb371..d148ed0e67 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -36,8 +36,8 @@ void harness() pSubackPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); - pPayloadStart = safeMalloc( sizeof( uint8_t * ) ); - pPayloadSize = safeMalloc( sizeof( uint8_t ) ); + pPayloadStart = mallocCanFail( sizeof( uint8_t * ) ); + pPayloadSize = mallocCanFail( sizeof( uint8_t ) ); MQTT_GetSubAckStatusCodes( pSubackPacket, pPayloadStart, From 3fbfdb410a68eae18039417603480bf7e182e75c Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Tue, 18 Aug 2020 00:08:12 +0000 Subject: [PATCH 10/11] Fix type of allocated memory in harness for payloadSize --- .../MQTT_GetSubAckStatusCodes_harness.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index d148ed0e67..1ab5935725 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -37,7 +37,7 @@ void harness() __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); pPayloadStart = mallocCanFail( sizeof( uint8_t * ) ); - pPayloadSize = mallocCanFail( sizeof( uint8_t ) ); + pPayloadSize = mallocCanFail( sizeof( size_t ) ); MQTT_GetSubAckStatusCodes( pSubackPacket, pPayloadStart, From a3a1027908aa58c11a016afccc7e53d2125bff0a Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Tue, 18 Aug 2020 19:07:10 +0000 Subject: [PATCH 11/11] Add comment about output parameters --- .../MQTT_GetSubAckStatusCodes_harness.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 1ab5935725..8ca650230f 100644 --- a/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/libraries/standard/mqtt/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -36,6 +36,8 @@ void harness() pSubackPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pSubackPacket ) ); + /* pPayloadStart and pPayloadSize are output parameters, and + * thus, don't carry any assumptions. */ pPayloadStart = mallocCanFail( sizeof( uint8_t * ) ); pPayloadSize = mallocCanFail( sizeof( size_t ) );