xref: /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/include/queue_init.h (revision 9d15770091225885eac5dbecba5cdb6840843db2) 
1 #include "FreeRTOS.h"
2 #include "queue.h"
3 #include "queue_datastructure.h"
4 
5 #ifndef CBMC_OBJECT_BITS
6     #define CBMC_OBJECT_BITS    7
7 #endif
8 
9 #ifndef CBMC_OBJECT_MAX_SIZE
10     #define CBMC_OBJECT_MAX_SIZE    ( UINT32_MAX >> ( CBMC_OBJECT_BITS + 1 ) )
11 #endif
12 
13 /* Using prvCopyDataToQueue together with prvNotifyQueueSetContainer
14  * leads to a problem space explosion. Therefore, we use this stub
15  * and a separated proof on prvCopyDataToQueue to deal with it.
16  * As prvNotifyQueueSetContainer is disabled if configUSE_QUEUE_SETS != 1,
17  * in other cases the original implementation should be used. */
18 #if ( configUSE_QUEUE_SETS == 1 )
prvCopyDataToQueue(Queue_t * const pxQueue,const void * pvItemToQueue,const BaseType_t xPosition)19     BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
20                                    const void * pvItemToQueue,
21                                    const BaseType_t xPosition )
22     {
23         if( pxQueue->uxItemSize > ( UBaseType_t ) 0 )
24         {
25             __CPROVER_assert( __CPROVER_r_ok( pvItemToQueue, ( size_t ) pxQueue->uxItemSize ), "pvItemToQueue region must be readable" );
26 
27             if( xPosition == queueSEND_TO_BACK )
28             {
29                 __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize ), "pxQueue->pcWriteTo region must be writable" );
30             }
31             else
32             {
33                 __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ), "pxQueue->u.xQueue.pcReadFrom region must be writable" );
34             }
35 
36             return pdFALSE;
37         }
38         else
39         {
40             return nondet_BaseType_t();
41         }
42     }
43 #endif /* if ( configUSE_QUEUE_SETS == 1 ) */
44 
45 /* xQueueCreateSet is compiled out if configUSE_QUEUE_SETS != 1.*/
46 #if ( configUSE_QUEUE_SETS == 1 )
xUnconstrainedQueueSet()47     QueueSetHandle_t xUnconstrainedQueueSet()
48     {
49         UBaseType_t uxEventQueueLength = 2;
50         QueueSetHandle_t xSet = xQueueCreateSet( uxEventQueueLength );
51 
52         if( xSet )
53         {
54             xSet->cTxLock = nondet_int8_t();
55             __CPROVER_assume( xSet->cTxLock != 127 );
56             xSet->cRxLock = nondet_int8_t();
57             xSet->uxMessagesWaiting = nondet_UBaseType_t();
58             xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
59 
60             /* This is an invariant checked with a couple of asserts in the code base.
61              * If it is false from the beginning, the CBMC proofs are not able to succeed*/
62             __CPROVER_assume( xSet->uxMessagesWaiting < xSet->uxLength );
63             xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
64         }
65 
66         return xSet;
67     }
68 #endif /* if ( configUSE_QUEUE_SETS == 1 ) */
69 
70 /* Create a mostly unconstrained Queue but bound the max item size.
71  * This is required for performance reasons in CBMC at the moment. */
xUnconstrainedQueueBoundedItemSize(UBaseType_t uxItemSizeBound)72 QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound )
73 {
74     UBaseType_t uxQueueLength;
75     UBaseType_t uxItemSize;
76     uint8_t ucQueueType;
77 
78     __CPROVER_assume( uxQueueLength > 0 );
79     __CPROVER_assume( uxItemSize < uxItemSizeBound );
80 
81     /* QueueGenericCreate method does not check for multiplication overflow */
82     size_t uxQueueStorageSize;
83 
84     __CPROVER_assume( uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE );
85     __CPROVER_assume( uxItemSize < uxQueueStorageSize / uxQueueLength );
86 
87     QueueHandle_t xQueue =
88         xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
89 
90     if( xQueue )
91     {
92         xQueue->cTxLock = nondet_int8_t();
93         __CPROVER_assume( xQueue->cTxLock != 127 );
94         xQueue->cRxLock = nondet_int8_t();
95         xQueue->uxMessagesWaiting = nondet_UBaseType_t();
96 
97         /* This is an invariant checked with a couple of asserts in the code base.
98          * If it is false from the beginning, the CBMC proofs are not able to succeed*/
99         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );
100         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
101         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
102         #if ( configUSE_QUEUE_SETS == 1 )
103             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );
104         #endif
105     }
106 
107     return xQueue;
108 }
109 
110 /* Create a mostly unconstrained Queue */
xUnconstrainedQueue(void)111 QueueHandle_t xUnconstrainedQueue( void )
112 {
113     UBaseType_t uxQueueLength;
114     UBaseType_t uxItemSize;
115     uint8_t ucQueueType;
116 
117     __CPROVER_assume( uxQueueLength > 0 );
118 
119     /* QueueGenericCreate method does not check for multiplication overflow */
120     size_t uxQueueStorageSize;
121 
122     __CPROVER_assume( uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE );
123     __CPROVER_assume( uxItemSize < uxQueueStorageSize / uxQueueLength );
124 
125     QueueHandle_t xQueue =
126         xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
127 
128     if( xQueue )
129     {
130         xQueue->cTxLock = nondet_int8_t();
131         __CPROVER_assume( xQueue->cTxLock != 127 );
132         xQueue->cRxLock = nondet_int8_t();
133         xQueue->uxMessagesWaiting = nondet_UBaseType_t();
134 
135         /* This is an invariant checked with a couple of asserts in the code base.
136          * If it is false from the beginning, the CBMC proofs are not able to succeed*/
137         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );
138         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
139         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
140         #if ( configUSE_QUEUE_SETS == 1 )
141             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );
142         #endif
143     }
144 
145     return xQueue;
146 }
147 
148 /* Create a mostly unconstrained Mutex */
xUnconstrainedMutex(void)149 QueueHandle_t xUnconstrainedMutex( void )
150 {
151     uint8_t ucQueueType;
152     QueueHandle_t xQueue =
153         xQueueCreateMutex( ucQueueType );
154 
155     if( xQueue )
156     {
157         xQueue->cTxLock = nondet_int8_t();
158         __CPROVER_assume( xQueue->cTxLock != 127 );
159         xQueue->cRxLock = nondet_int8_t();
160         xQueue->uxMessagesWaiting = nondet_UBaseType_t();
161 
162         /* This is an invariant checked with a couple of asserts in the code base.
163          * If it is false from the beginning, the CBMC proofs are not able to succeed*/
164         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );
165         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
166         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
167         #if ( configUSE_QUEUE_SETS == 1 )
168             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );
169         #endif
170     }
171 
172     return xQueue;
173 }
174