1 /* Standard includes. */
2 #include <stdint.h>
3 #include <stdio.h>
4 
5 /* FreeRTOS includes. */
6 #include "FreeRTOS.h"
7 #include "list.h"
8 
9 /* FreeRTOS+TCP includes. */
10 #include "FreeRTOS_IP.h"
11 #include "FreeRTOS_IP_Private.h"
12 #include "FreeRTOS_Sockets.h"
13 
14 #include "freertos_api.c"
15 #include "memory_assignments.c"
16 
17 /* The memory safety of vTCPWindowDestroy has already been proved in
18  * proofs/TCPWin/vTCPWindowDestroy. */
vTCPWindowDestroy(TCPWindow_t const * xWindow)19 void vTCPWindowDestroy( TCPWindow_t const * xWindow )
20 {
21     __CPROVER_assert( xWindow != NULL, "xWindow cannot be NULL" );
22 
23     /* Do nothing. */
24 }
25 
harness()26 void harness()
27 {
28     size_t xRequestedSizeBytes;
29     TickType_t xBlockTimeTicks;
30     FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
31 
32     /* Socket cannot be NULL or invalid for this proof. This is allowed since vSocketClose is called by IP task only. */
33     __CPROVER_assume( pxSocket != NULL );
34     __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
35 
36     /* Request a random number of bytes keeping in mind the maximum bound of CBMC. */
37     __CPROVER_assume( xRequestedSizeBytes < ( CBMC_MAX_OBJECT_SIZE - ipBUFFER_PADDING ) );
38 
39     /* Non-deterministically malloc the callback function. */
40     pxSocket->pxUserWakeCallback = safeMalloc( sizeof( SocketWakeupCallback_t ) );
41 
42     /* Non deterministically add an event group. */
43     if( nondet_bool() )
44     {
45         pxSocket->xEventGroup = xEventGroupCreate();
46         __CPROVER_assume( pxSocket->xEventGroup != NULL );
47     }
48     else
49     {
50         pxSocket->xEventGroup = NULL;
51     }
52 
53     /* Create and fill the socket in the bound socket list. This socket will then be
54      * removed by a call to the vSocketClose. */
55     List_t BoundSocketList;
56     vListInitialise( &BoundSocketList );
57 
58     /* Non-deterministically add the socket to bound socket list. */
59     if( nondet_bool() )
60     {
61         vListInitialiseItem( &( pxSocket->xBoundSocketListItem ) );
62         pxSocket->xBoundSocketListItem.pxContainer = &( BoundSocketList );
63         vListInsertEnd( &BoundSocketList, &( pxSocket->xBoundSocketListItem ) );
64     }
65     else
66     {
67         pxSocket->xBoundSocketListItem.pxContainer = NULL;
68     }
69 
70     /* See Configurations.json for details. Protocol can be UDP or TCP. */
71     pxSocket->ucProtocol = PROTOCOL;
72 
73     NetworkBufferDescriptor_t * NetworkBuffer;
74 
75     /* Get a network buffer descriptor with requested bytes. See the constraints
76      * on the number of requested bytes above. And block for random timer ticks. */
77     if( pxSocket->ucProtocol == FREERTOS_IPPROTO_TCP )
78     {
79         pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) );
80         pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) );
81 
82         /* Non deterministically allocate/not-allocate the network buffer descriptor. */
83         if( nondet_bool() )
84         {
85             pxSocket->u.xTCP.pxAckMessage = pxGetNetworkBufferWithDescriptor( xRequestedSizeBytes, xBlockTimeTicks );
86         }
87         else
88         {
89             pxSocket->u.xTCP.pxAckMessage = NULL;
90         }
91     }
92     else if( pxSocket->ucProtocol == FREERTOS_IPPROTO_UDP )
93     {
94         /* Initialise the waiting packet list. */
95         vListInitialise( &( pxSocket->u.xUDP.xWaitingPacketsList ) );
96 
97         /* Non-deterministically either add/not-add item to the waiting packet list. */
98         if( nondet_bool() )
99         {
100             NetworkBuffer = pxGetNetworkBufferWithDescriptor( xRequestedSizeBytes, xBlockTimeTicks );
101             /* Assume non-NULL network buffer for this case. */
102             __CPROVER_assume( NetworkBuffer != NULL );
103 
104             /* Initialise the buffer list item. */
105             vListInitialiseItem( &( NetworkBuffer->xBufferListItem ) );
106 
107             /*Set the item owner as the buffer itself. */
108             listSET_LIST_ITEM_OWNER( &( NetworkBuffer->xBufferListItem ), ( void * ) NetworkBuffer );
109 
110             /* Set the container of the buffer list item as the waiting packet list. */
111             NetworkBuffer->xBufferListItem.pxContainer = &( pxSocket->u.xUDP.xWaitingPacketsList );
112 
113             /* Insert the list-item into the waiting packet list. */
114             vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( NetworkBuffer->xBufferListItem ) );
115         }
116     }
117 
118     /* Call to init the socket list. */
119     vNetworkSocketsInit();
120 
121     /* Call the function. */
122     vSocketClose( pxSocket );
123 
124     /* No post checking to be done. */
125 }
126