Skip to content

Commit a489ea5

Browse files
tony-josi-awskarkhazmarkrtuttle
authored
Fix build and proof failures for CBMC ARP proofs (#709)
* Use CBMC XML output to enable VSCode debugger (#673) 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]> * Fixes CBMC proof for the ARPAgeCache function: * 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); * Fixes CBMC proof build failure and proof failure for ARP_FreeRTOS_ClearARP: * 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 * Fixed ARPGenerateRequestPacket CBMC proof * Fixed ARPGetCacheEntryByMac proof: 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: Changes: ------- ARPProcessPacket takes new arg (NetworkBufferDescriptor_t *) * Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc1 diff configs * Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc2 diff configs * Fix CBMC proof for ARPGetCacheEntry * Fixed proofs for ARPRefreshCacheEntry * Fixed CBMC proof for ARP_FreeRTOS_OutputARPRequest * Fix cbmc proof for ARPProcessPacket * fixed cbmc target func not called issue in ARP_FreeRTOS_PrintARPCache * adding changes as per review comments * add multiple endpoints * config fix for multiple end point * wip * assigning null instead of assuming * fixe minor isssue * update asume to assignment * more comments * Revert "update asume to assignment" This reverts commit b1f9e46. * reverting kernel submodule change * addding non deterministic number of endpoints * addding non deterministic number of endpoints * addding non deterministic number of endpoints * addding non deterministic number of endpoints * addding non deterministic number of endpoints --------- Co-authored-by: Kareem Khazem <[email protected]> Co-authored-by: Mark Tuttle <[email protected]>
1 parent fd5303d commit a489ea5

File tree

22 files changed

+275
-23
lines changed

22 files changed

+275
-23
lines changed

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,45 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
2323
return pxNetworkBuffer;
2424
}
2525

26+
BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
27+
NetworkBufferDescriptor_t * const pxNetworkBuffer,
28+
BaseType_t xReleaseAfterSend )
29+
{
30+
__CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
31+
__CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
32+
__CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
33+
return 0;
34+
}
35+
2636
void harness()
2737
{
38+
/*
39+
For this proof, its assumed that the endpoints and interfaces are correctly
40+
initialised and the pointers are set correctly.
41+
Assumes two endpoints and interface is present.
42+
*/
43+
44+
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
45+
__CPROVER_assume( pxNetworkEndPoints != NULL );
46+
47+
/* Interface init. */
48+
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
49+
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
50+
51+
if( nondet_bool() )
52+
{
53+
pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
54+
__CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
55+
pxNetworkEndPoints->pxNext->pxNext = NULL;
56+
pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
57+
}
58+
else
59+
{
60+
pxNetworkEndPoints->pxNext = NULL;
61+
}
62+
63+
pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
64+
/* No assumption is added for pfOutput as its pointed to a static object/memory location. */
65+
2866
vARPAgeCache();
2967
}

‎test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,15 @@
44
[
55
"--unwind 1",
66
"--unwindset vARPAgeCache.0:7",
7+
"--unwindset FreeRTOS_OutputARPRequest.0:3",
8+
"--unwindset vARPAgeCache.1:3",
79
"--nondet-static"
810
],
911
"OBJS":
1012
[
1113
"$(ENTRY)_harness.goto",
1214
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
15+
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
1316
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
1417
"$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
1518
],

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,13 @@ void harness()
2626
xNetworkBuffer2.pucEthernetBuffer = xBuffer;
2727
xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
2828

29+
/*
30+
This proof assumes one end point is present.
31+
*/
32+
xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
33+
__CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
34+
xNetworkBuffer2.pxEndPoint->pxNext = NULL;
35+
2936
/* vARPGenerateRequestPacket asserts buffer has room for a packet */
3037
__CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof( ARPPacket_t ) );
3138
vARPGenerateRequestPacket( &xNetworkBuffer2 );

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

Lines changed: 34 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,38 @@ void harness()
1313
uint32_t ulIPAddress;
1414
MACAddress_t xMACAddress;
1515

16-
eARPGetCacheEntry( &ulIPAddress, &xMACAddress );
16+
/*
17+
For this proof, its assumed that the endpoints and interfaces are correctly
18+
initialised and the pointers are set correctly.
19+
Assumes one endpoint and interface is present.
20+
*/
21+
22+
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
23+
__CPROVER_assume( pxNetworkEndPoints != NULL );
24+
25+
/* Interface init. */
26+
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
27+
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
28+
29+
if( nondet_bool() )
30+
{
31+
pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
32+
__CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
33+
pxNetworkEndPoints->pxNext->pxNext = NULL;
34+
pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
35+
}
36+
else
37+
{
38+
pxNetworkEndPoints->pxNext = NULL;
39+
}
40+
41+
NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
42+
43+
if ( ppxInterface )
44+
{
45+
*ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
46+
__CPROVER_assume( *ppxInterface != NULL );
47+
}
48+
49+
eARPGetCacheEntry( &ulIPAddress, &xMACAddress, ppxInterface );
1750
}

‎test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,16 @@
44
[
55
"--unwind 1",
66
"--unwindset prvCacheLookup.0:7",
7+
"--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3",
8+
"--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
9+
"--unwindset eARPGetCacheEntry.0:3",
10+
"--unwindset FreeRTOS_FindGateWay.0:3",
711
"--nondet-static"
812
],
913
"OBJS":
1014
[
1115
"$(ENTRY)_harness.goto",
16+
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
1217
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
1318
],
1419
"DEF":

‎test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,22 @@
77
#include "FreeRTOS_IP_Private.h"
88
#include "FreeRTOS_ARP.h"
99

10+
extern ARPCacheRow_t xARPCache[ ipconfigARP_CACHE_ENTRIES ];
11+
12+
static NetworkEndPoint_t xEndPoint_Temp;
13+
1014
void harness()
1115
{
1216
MACAddress_t xMACAddress;
1317
uint32_t ulIPAddress;
1418

15-
eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress );
19+
NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
20+
21+
if ( ppxInterface )
22+
{
23+
*ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
24+
__CPROVER_assume( *ppxInterface != NULL );
25+
}
26+
27+
eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress, ppxInterface );
1628
}

‎test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,7 @@
22
"ENTRY": "ARPGetCacheEntryByMac",
33
"CBMCFLAGS":
44
[
5-
"--unwind 7",
6-
"--nondet-static"
5+
"--unwind 7"
76
],
87
"OBJS":
98
[

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

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include "cbmc.h"
2+
13
/* FreeRTOS includes. */
24
#include "FreeRTOS.h"
35
#include "queue.h"
@@ -17,7 +19,6 @@ void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
1719

1820
void harness()
1921
{
20-
ARPPacket_t xARPFrame;
2122
NetworkBufferDescriptor_t xLocalBuffer;
2223
uint16_t usEthernetBufferSize;
2324

@@ -47,5 +48,30 @@ void harness()
4748
pxARPWaitingNetworkBuffer = NULL;
4849
}
4950

50-
eARPProcessPacket( &xARPFrame );
51+
/*
52+
* The assumption made here is that the buffer pointed by pucEthernetBuffer
53+
* is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.
54+
* This is not checked inside eARPProcessPacket.
55+
*/
56+
uint8_t ucBUFFER_SIZE;
57+
58+
void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
59+
60+
__CPROVER_assume( xBuffer != NULL );
61+
62+
NetworkBufferDescriptor_t xNetworkBuffer2;
63+
64+
xNetworkBuffer2.pucEthernetBuffer = xBuffer;
65+
xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof(ARPPacket_t);
66+
67+
/*
68+
This proof assumes one end point is present.
69+
*/
70+
xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
71+
__CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
72+
xNetworkBuffer2.pxEndPoint->pxNext = NULL;
73+
74+
/* eARPProcessPacket will be called in the source code only after checking if
75+
xNetworkBuffer2.pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL ); */
76+
eARPProcessPacket( &xNetworkBuffer2 );
5177
}

‎test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
[
55
"--unwind 1",
66
"--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17,xIsIPInARPCache.0:7",
7+
"--unwindset prvFindCacheEntry.0:7",
78
"--nondet-static"
89
],
910
"OBJS":

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

Lines changed: 31 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,35 @@ void harness()
1111
MACAddress_t xMACAddress;
1212
uint32_t ulIPAddress;
1313

14-
vARPRefreshCacheEntry( &xMACAddress, ulIPAddress );
15-
vARPRefreshCacheEntry( NULL, ulIPAddress );
14+
/*
15+
For this proof, its assumed that the endpoints and interfaces are correctly
16+
initialised and the pointers are set correctly.
17+
Assumes one endpoints and interface is present.
18+
*/
19+
20+
pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
21+
__CPROVER_assume( pxNetworkEndPoints != NULL );
22+
23+
/* Interface init. */
24+
pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
25+
__CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
26+
27+
if( nondet_bool() )
28+
{
29+
pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
30+
__CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
31+
pxNetworkEndPoints->pxNext->pxNext = NULL;
32+
pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
33+
}
34+
else
35+
{
36+
pxNetworkEndPoints->pxNext = NULL;
37+
}
38+
39+
40+
NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
41+
__CPROVER_assume( pxEndPoint != NULL );
42+
43+
vARPRefreshCacheEntry( &xMACAddress, ulIPAddress, pxEndPoint );
44+
vARPRefreshCacheEntry( NULL, ulIPAddress, pxEndPoint );
1645
}

0 commit comments

Comments
 (0)