Add CBMC proof of checkDataType function #293

Bujain · 2021-09-21T15:19:12Z

Add CBMC proof of checkDataType function

Description

This PR adds files required for the CBMC proof of checkDataType function.

Checklist:

I have tested my changes. No regression in existing tests.
My code is formatted using Uncrustify.
I have read and applied the rules stated in CONTRIBUTING.md.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

…t-embedded-sdk into cbmc_infra

Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setDataInterface function * removed unnecessary variables * Updated documentation * Uncrustified * Updated year in copyright notice Co-authored-by: Aniruddha Kanhere <[email protected]>

Add assert checks for http interface functions (aws#231)

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of OTA_HTTP_strerror function * Removed extra line and updated error log * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC Proof of requestDataBlock_Http function * Removed extra line * Update Comments Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for OTA_MQTT_strerror function * Removed extra line * Updated comments * Fixed formatting errors * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]>

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setControlInterface function * Removed extra line * Added macro for the function * Fix formating errors * Fix spell check errors * Added preprocessor definition for setControlInterface function Co-authored-by: Aniruddha Kanhere <[email protected]>

…t-embedded-sdk into cbmc_infra

* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of initFileTransfer_Http function * Removed extra line * Updated Comments * Updated error log and comments * Updated comments * Fix formatting errors Co-authored-by: Aniruddha Kanhere <[email protected]>

…-iot-embedded-sdk into checkDataType

divekarshubham · 2021-09-28T00:14:20Z

test/cbmc/proofs/checkDataType/Makefile

+DEFINES +=
+INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/tinycbor/src/
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=


Please remove unused vars.

Updated in 632b2de

paulbartell · 2021-09-28T18:55:09Z

test/cbmc/proofs/checkDataType/checkDataType_harness.c

+/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */
+/* SPDX-License-Identifier: Apache-2.0 */
+
+/**


Should this file have the same header and license as the other proofs?

The copyright license needs to be updated in all the proofs with the updated version. There has been discussion going on. I will need to run a script in the main repo to update all the licenses in all the proofs.

paulbartell · 2021-09-28T19:08:54Z

test/cbmc/proofs/checkDataType/checkDataType_harness.c

+     * before checkDataType is called. */
+    pcborValue = &cborvalue;
+
+    __CPROVER_file_local_ota_cbor_c_checkDataType( expectedType, pcborValue );


Should the return value be checked?

There are multiple return values for different tests. It would be difficult to check for the return value. If the return value is certain only then are we checking it.

I agree with @paulbartell, we can assert on the range of all the values using below (pseudo)code:

__CPROVER_assert( ( returnValue >= LOWEST_CborError_VALUE ) && ( returnValue <= HIGHEST_CborError_VALUE ) );

…-iot-embedded-sdk into checkDataType

aggarg · 2021-10-21T20:33:05Z

test/cbmc/proofs/checkDataType/checkDataType_harness.c

+     * before checkDataType is called. */
+    pcborValue = &cborvalue;
+
+    cborResult = __CPROVER_file_local_ota_cbor_c_checkDataType( expectedType, pcborValue );


Is it not possible to directly do the following:

cborResult = __CPROVER_file_local_ota_cbor_c_checkDataType( expectedType, &cborvalue);

Or is this something that you need for CBMC?

It is not required for the CBMC and I have updated that in 55375df

…-iot-embedded-sdk into checkDataType

Bujain and others added 30 commits August 4, 2021 23:32

Add CBMC-proofs infrastructure

0bbf408

Add CBMC-proofs infrastructure (aws#242)

95529f8

Added value to not update the submodule

21ee448

Added Include paths and preprocessor defines

4b189aa

Added template define file

ae17c09

Updated to ignore the output files on git push

4a2ed43

Added words

6c5d6f5

Updated Project Name

b4a774c

Updated source directory path

db409b7

Merge branch 'cbmc-proof' into cbmc_infra

402e6b8

Update ci.yml

92b5b00

Add checks on the branch

62ddec4

Updated Submodule update value

67ad6b0

Merge branch 'cbmc_infra' of https://github.com/Bujain/ota-for-aws-io…

1f5668f

…t-embedded-sdk into cbmc_infra

Added litani submodule update

3bda16a

Update Project name

2c7f2ee

Co-authored-by: Aniruddha Kanhere <[email protected]>

Added new line in the end of the file

e88c8c0

Remove whitespace

d274f81

Added template inside proof directory

f561a6c

Merge pull request #2 from aws/main

6122c14

Add assert checks for http interface functions (aws#231)

removed extra line

4a2b21d

Merge branch 'cbmc_infra' of https://github.com/Bujain/ota-for-aws-io…

08b6b5c

…t-embedded-sdk into cbmc_infra

Uncrustified'

b331892

Bujain and others added 5 commits September 27, 2021 23:21

add words

094d06e

Merge branch 'main' into checkDataType

cd3c2d9

Fix spell check errors

23a3835

Merge branch 'checkDataType' of https://github.com/Bujain/ota-for-aws…

92afbdd

…-iot-embedded-sdk into checkDataType

Fix spell check error

8c01a98

Bujain requested a review from divekarshubham September 27, 2021 23:48

divekarshubham reviewed Sep 28, 2021

View reviewed changes

Removed unused variables

632b2de

divekarshubham previously approved these changes Sep 28, 2021

View reviewed changes

paulbartell reviewed Sep 28, 2021

View reviewed changes

Add return value check

b3b01fb

Bujain dismissed divekarshubham’s stale review via b3b01fb October 18, 2021 21:40

Bujain and others added 7 commits October 18, 2021 14:40

Merge branch 'main' into checkDataType

2854e0c

uncrustified

e805e06

Merge branch 'checkDataType' of https://github.com/Bujain/ota-for-aws…

ab9451d

…-iot-embedded-sdk into checkDataType

Merge branch 'main' into checkDataType

9b519d6

Add check for return value

245ac12

Merge branch 'checkDataType' of https://github.com/Bujain/ota-for-aws…

0d0efbf

…-iot-embedded-sdk into checkDataType

Uncrustified

3927400

AniruddhaKanhere previously approved these changes Oct 20, 2021

View reviewed changes

Merge branch 'main' into checkDataType

837e9d1

aggarg reviewed Oct 21, 2021

View reviewed changes

Bujain added 2 commits October 22, 2021 21:17

remove optional variables

74a5c64

Merge branch 'checkDataType' of https://github.com/Bujain/ota-for-aws…

55375df

…-iot-embedded-sdk into checkDataType

Bujain dismissed AniruddhaKanhere’s stale review via 55375df October 22, 2021 21:17

aggarg approved these changes Oct 22, 2021

View reviewed changes

Merge branch 'main' into checkDataType

851523c

divekarshubham approved these changes Oct 25, 2021

View reviewed changes

Bujain merged commit cee0641 into aws:main Oct 25, 2021

Bujain deleted the checkDataType branch November 1, 2021 22:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add CBMC proof of checkDataType function #293

Add CBMC proof of checkDataType function #293

Bujain commented Sep 21, 2021 •

edited

Loading

divekarshubham Sep 28, 2021

Bujain Sep 28, 2021

paulbartell Sep 28, 2021

Bujain Sep 28, 2021

paulbartell Sep 28, 2021

Bujain Sep 28, 2021

AniruddhaKanhere Sep 29, 2021

aggarg Oct 21, 2021

Bujain Oct 22, 2021

Add CBMC proof of checkDataType function #293

Add CBMC proof of checkDataType function #293

Conversation

Bujain commented Sep 21, 2021 • edited Loading

Description

Checklist:

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Bujain commented Sep 21, 2021 •

edited

Loading