Fix build and proof failures for CBMC ARP proofs #709

tony-josi-aws · 2023-02-13T11:43:38Z

This PR fixes the build issues and proof failures for the ARP CBMC proofs post the IPv6 changes.

Description

Major changes:

As the support multiple endpoint was added in dev/IPv6_integration, this PR allocates endpoints to get rid of asserts and validate functions
Removed —nondet-static for ARPGetCacheEntryByMac proof: as proof fails if its there as the endpoint gets random value
Increased global object-bits to --object-bits 8 from 7: as some of the existing proofs were having issues with more number addressed objects: too many addressed objects: maximum number of objects is set to 2^n=128 (with n=7);

Test Steps

cd test/cbmc/proofs/
python run-cbmc-proofs.py

Related Issue

Failing CBMC proofs

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

Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <[email protected]>

* Adds /source/FreeRTOS_Routing.c to ARPAgeCache proof build * Assumes pxNetworkEndPoints and pxNetworkEndPoints->pxNetworkInterface are properly initialized before ARPAgeCache is used. * Assumes one endpoint and interface are only present Changes to CBMC flags/configs: * Added: * `--unwindset FreeRTOS_OutputARPRequest.0:3` and `--unwindset vARPAgeCache.1:3` as per number of endpoints * Modified: * `--object-bits 8` to address: too many addressed objects: maximum number of objects is set to 2^n=128 (with n=7);

…arARP: * New flags: * "--unwindset FreeRTOS_ClearARP.0:7" to support loop in cleararp function * Added argument to FreeRTOS_ClearARP in harness to support new change in API

Changes ------- Removed --nondet-static: proof fails if that option is enabled as the endpoint gets random value even if there is NULL check before its usage

Changes: ------- ARPProcessPacket takes new arg (NetworkBufferDescriptor_t *)

AniruddhaKanhere · 2023-02-13T17:34:55Z

test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c

+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    return 0;


I think it would be better if we check the validity of the pointers in the stub by adding something like this:

__CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." ); __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );

AniruddhaKanhere · 2023-02-13T17:36:39Z

test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c

+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );


I think that instead of __CPROVER_assume, we can just set this value to NULL.
as in pxNetworkEndPoints->pxNext->pxNext = NULL;

fixed all cases

AniruddhaKanhere · 2023-02-13T17:37:16Z

test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c

+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );


Same here, we can get away with just setting it to NULL.

AniruddhaKanhere · 2023-02-13T17:37:34Z

test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c

+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );


And here as well.

AniruddhaKanhere · 2023-02-13T17:39:47Z

test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c

+     */
+    uint8_t ucBUFFER_SIZE;
+
+    __CPROVER_assume( ucBUFFER_SIZE < CBMC_MAX_OBJECT_SIZE );


Isn't this true automatically? the ucBUFFER_SIZE is an unsigned 8-bit integer meaning that it will never go beyond 255. I assume that CBMC_MAX_OBJECT_SIZE will at least be 16-bit value...

AniruddhaKanhere · 2023-02-13T17:40:22Z

test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c

-    eARPProcessPacket( &xARPFrame );
+    /*
+     * The assumption made here is that the buffer pointed by pucEthernetBuffer
+     * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.


Suggested change

* is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.

* is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.

AniruddhaKanhere · 2023-02-13T17:41:24Z

test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c

+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );


Set this to NULL directly.

updated all

AniruddhaKanhere · 2023-02-13T17:41:48Z

test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c

+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );


Why not try this with more than one network endpoint?

AniruddhaKanhere · 2023-02-13T17:47:58Z

test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c

+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+


We should add asserts on the pointers to make sure that they are not NULL when stub is called.

AniruddhaKanhere · 2023-02-13T17:52:45Z

test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c

    {
-        vReleaseNetworkBufferAndDescriptor( pxDescriptor );
+        vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
    }


Assert on pointers being non-NULL here.

This reverts commit b1f9e46.

AniruddhaKanhere

Approved with one minor comment.

AniruddhaKanhere · 2023-02-21T00:32:05Z

test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c

+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
+    return 0;


Why are we returning 0 and not nondet_uint32?

karkhaz and others added 15 commits February 4, 2023 09:02

Fixes CBMC proof build failure and proof failure for ARP_FreeRTOS_Cle…

a1371d9

…arARP: * New flags: * "--unwindset FreeRTOS_ClearARP.0:7" to support loop in cleararp function * Added argument to FreeRTOS_ClearARP in harness to support new change in API

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_arp

8068a1d

Fixed ARPGenerateRequestPacket CBMC proof

ff05ea3

Fixed ARPGetCacheEntryByMac proof:

be35723

Changes ------- Removed --nondet-static: proof fails if that option is enabled as the endpoint gets random value even if there is NULL check before its usage

Fix ARPProcessPacket CBMC proof:

441e266

Changes: ------- ARPProcessPacket takes new arg (NetworkBufferDescriptor_t *)

Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc1 diff configs

1999639

Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc2 diff configs

e0f3d75

Fix CBMC proof for ARPGetCacheEntry

c17d11d

Fixed proofs for ARPRefreshCacheEntry

759182e

Fixed CBMC proof for ARP_FreeRTOS_OutputARPRequest

2895b31

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_arp

e3313df

Fix cbmc proof for ARPProcessPacket

a5d9b57

fixed cbmc target func not called issue in ARP_FreeRTOS_PrintARPCache

a48c5ef

tony-josi-aws requested a review from a team as a code owner February 13, 2023 11:43

AniruddhaKanhere reviewed Feb 13, 2023

View reviewed changes

tony-josi-aws added 9 commits February 14, 2023 10:41

adding changes as per review comments

62f0638

add multiple endpoints

563b329

config fix for multiple end point

7b22b34

wip

f575184

assigning null instead of assuming

b6b388d

fixe minor isssue

e6e3b81

update asume to assignment

b1f9e46

more comments

f516277

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_arp

39d8c53

tony-josi-aws force-pushed the fix_cbmc_proof_arp branch from 4574eae to 39d8c53 Compare February 17, 2023 06:20

tony-josi-aws added 3 commits February 17, 2023 11:51

Revert "update asume to assignment"

a338c5c

This reverts commit b1f9e46.

reverting kernel submodule change

49cbd55

addding non deterministic number of endpoints

55a3ed9

tony-josi-aws added 4 commits February 17, 2023 23:42

addding non deterministic number of endpoints

7e0a5b6

addding non deterministic number of endpoints

195e024

addding non deterministic number of endpoints

e9c8861

addding non deterministic number of endpoints

4954db6

AniruddhaKanhere approved these changes Feb 21, 2023

View reviewed changes

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_arp

2322350

tony-josi-aws merged commit a489ea5 into FreeRTOS:dev/IPv6_integration Feb 21, 2023

	* is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.
	* is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.

Fix build and proof failures for CBMC ARP proofs #709

Fix build and proof failures for CBMC ARP proofs #709

Uh oh!

Conversation

tony-josi-aws commented Feb 13, 2023

Description

Test Steps

Related Issue

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tony-josi-aws Feb 15, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AniruddhaKanhere left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tony-josi-aws Feb 15, 2023 •

edited

Loading