xref: /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/Socket/vSocketWakeUpUser/vSocketWakeUpUser_harness.c (revision 766040fbaa705e1573b1ba76d6d517ce8d5c390d) 
1 /* Standard includes. */
2 #include <stdint.h>
3 #include <stdio.h>
4 
5 /* FreeRTOS includes. */
6 #include "FreeRTOS.h"
7 #include "queue.h"
8 #include "semphr.h"
9 #include "event_groups.h"
10 
11 /* FreeRTOS+TCP includes. */
12 #include "FreeRTOS_IP.h"
13 #include "FreeRTOS_IP_Private.h"
14 #include "FreeRTOS_Sockets.h"
15 
16 #include "memory_assignments.c"
17 
18 
19 /*********************************************************************************
20  *
21  * The below structure definitions are just copy pasted from the FreeRTOS-Kernel.
22  * To understand the proof, you need not understand the structures and they can
23  * be ignored safely.
24  *
25  ********************************************************************************/
26 
27 /* Define the bits used by Kernel. */
28 #define eventEVENT_BITS_CONTROL_BYTES    0xff000000UL
29 
30 typedef struct EventGroupDef_t
31 {
32     EventBits_t uxEventBits;
33     List_t xTasksWaitingForBits;
34 
35     #if ( configUSE_TRACE_FACILITY == 1 )
36         UBaseType_t uxEventGroupNumber;
37     #endif
38 
39     #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) )
40         uint8_t ucStaticallyAllocated;
41     #endif
42 } EventGroup_t;
43 
44 typedef struct QueuePointers
45 {
46     int8_t * pcTail;
47     int8_t * pcReadFrom;
48 } QueuePointers_t;
49 
50 typedef struct SemaphoreData
51 {
52     TaskHandle_t xMutexHolder;
53     UBaseType_t uxRecursiveCallCount;
54 } SemaphoreData_t;
55 
56 typedef struct QueueDefinition
57 {
58     int8_t * pcHead;
59     int8_t * pcWriteTo;
60 
61     union
62     {
63         QueuePointers_t xQueue;
64         SemaphoreData_t xSemaphore;
65     } u;
66 
67     List_t xTasksWaitingToSend;
68     List_t xTasksWaitingToReceive;
69 
70     volatile UBaseType_t uxMessagesWaiting;
71     UBaseType_t uxLength;
72     UBaseType_t uxItemSize;
73 
74     volatile int8_t cRxLock;
75     volatile int8_t cTxLock;
76 
77     #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) )
78         uint8_t ucStaticallyAllocated;
79     #endif
80 
81     #if ( configUSE_QUEUE_SETS == 1 )
82         struct QueueDefinition * pxQueueSetContainer;
83     #endif
84 
85     #if ( configUSE_TRACE_FACILITY == 1 )
86         UBaseType_t uxQueueNumber;
87         uint8_t ucQueueType;
88     #endif
89 } xQUEUE;
90 
91 /********************************************************/
92 /********* End Kernel cut-paste section *****************/
93 /********************************************************/
94 
95 
96 /* The memory safety of xQueueGenericSend has been proved before.
97  * See github.com/FreeRTOS/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend.
98  */
xQueueGenericSend(QueueHandle_t xQueue,const void * const pvItemToQueue,TickType_t xTicksToWait,const BaseType_t xCopyPosition)99 BaseType_t xQueueGenericSend( QueueHandle_t xQueue,
100                               const void * const pvItemToQueue,
101                               TickType_t xTicksToWait,
102                               const BaseType_t xCopyPosition )
103 {
104     BaseType_t xResult;
105 
106     /* These asserts are copied over from the original function itself. */
107     __CPROVER_assert( xQueue != NULL, "xQueue cannot be NULL" );
108     __CPROVER_assert( !( ( pvItemToQueue == NULL ) && ( xQueue->uxItemSize != ( UBaseType_t ) 0U ) ),
109                       "If itemsize is non-zero, then pvItemToQueue cannot be NULL." );
110     __CPROVER_assert( !( ( xCopyPosition == queueOVERWRITE ) && ( xQueue->uxLength != 1 ) ),
111                       "If length is one, then check the copy position" );
112 
113     /* Return any random value. */
114     return xResult;
115 }
116 
117 
xEventGroupSetBits(EventGroupHandle_t xEventGroup,const EventBits_t uxBitsToSet)118 EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup,
119                                 const EventBits_t uxBitsToSet )
120 {
121     EventBits_t uxReturnBits;
122 
123     /* The below asserts are copied over from the original function itself. */
124     __CPROVER_assert( xEventGroup != NULL,
125                       "The event group cannot be NULL" );
126     __CPROVER_assert( ( uxBitsToSet & eventEVENT_BITS_CONTROL_BYTES ) == 0,
127                       "Cannot set Kernel bits" );
128 
129     /* Return any random value. */
130     return uxReturnBits;
131 }
132 
133 
harness()134 void harness()
135 {
136     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
137 
138     __CPROVER_assume( pxSocket != NULL );
139     __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
140 
141     pxSocket->pxUserWakeCallback = safeMalloc( sizeof( SocketWakeupCallback_t ) );
142 
143     pxSocket->pxSocketSet = safeMalloc( sizeof( struct xSOCKET_SET ) );
144 
145     if( pxSocket->pxSocketSet != NULL )
146     {
147         pxSocket->pxSocketSet->xSelectGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );
148 
149         /* The event group cannot be NULL. */
150         __CPROVER_assume( pxSocket->pxSocketSet->xSelectGroup != NULL );
151     }
152 
153     pxSocket->pxUserSemaphore = safeMalloc( sizeof( xQUEUE ) );
154 
155     if( pxSocket->pxUserSemaphore != NULL )
156     {
157         /* The item size must be zero since this queue will act as a semaphore.  */
158         __CPROVER_assume( pxSocket->pxUserSemaphore->uxItemSize == 0 );
159     }
160 
161     pxSocket->xEventGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );
162 
163     /* Call to init the socket list. */
164     vNetworkSocketsInit();
165 
166     vSocketWakeUpUser( pxSocket );
167 }
168