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
SocketWakeupCallback_Stub(struct xSOCKET * pxSocket)133 void SocketWakeupCallback_Stub( struct xSOCKET * pxSocket )
134 {
135 __CPROVER_assert( pxSocket != NULL,
136 "The pxSocket cannot be NULL" );
137 }
138
harness()139 void harness()
140 {
141 FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
142
143 __CPROVER_assume( pxSocket != NULL );
144 __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
145
146 pxSocket->pxUserWakeCallback = SocketWakeupCallback_Stub;
147
148 pxSocket->pxSocketSet = safeMalloc( sizeof( struct xSOCKET_SET ) );
149
150 if( pxSocket->pxSocketSet != NULL )
151 {
152 pxSocket->pxSocketSet->xSelectGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );
153
154 /* The event group cannot be NULL. */
155 __CPROVER_assume( pxSocket->pxSocketSet->xSelectGroup != NULL );
156 }
157
158 pxSocket->pxUserSemaphore = safeMalloc( sizeof( xQUEUE ) );
159
160 if( pxSocket->pxUserSemaphore != NULL )
161 {
162 /* The item size must be zero since this queue will act as a semaphore. */
163 __CPROVER_assume( pxSocket->pxUserSemaphore->uxItemSize == 0 );
164 }
165
166 pxSocket->xEventGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );
167
168 /* Call to init the socket list. */
169 vNetworkSocketsInit();
170
171 vSocketWakeUpUser( pxSocket );
172 }
173
