1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
/*
* FreeRTOS memory safety proofs with CBMC.
* Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation
* files (the "Software"), to deal in the Software without
* restriction, including without limitation the rights to use, copy,
* modify, merge, publish, distribute, sublicense, and/or sell copies
* of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
* BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
* ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*
* http://aws.amazon.com/freertos
* http://www.FreeRTOS.org
*/
#include "FreeRTOS.h"
#include "queue.h"
#include "queue_datastructure.h"
#include "cbmc.h"
#ifndef LOCK_BOUND
#define LOCK_BOUND 4
#endif
void prvUnlockQueue( Queue_t * const pxQueue );
BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
{
if(pxQueue->uxItemSize > ( UBaseType_t ) 0)
{
__CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable");
if(xPosition == queueSEND_TO_BACK){
__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable");
}else{
__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable");
}
return pdFALSE;
}else
{
return nondet_BaseType_t();
}
}
QueueSetHandle_t xUnconstrainedQueueSet()
{
UBaseType_t uxEventQueueLength = 2;
QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength);
if( xSet )
{
xSet->cTxLock = nondet_int8_t();
__CPROVER_assume( xSet->cTxLock != 127 );
xSet->cRxLock = nondet_int8_t();
xSet->uxMessagesWaiting = nondet_UBaseType_t();
xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
/* This is an invariant checked with a couple of asserts in the code base.
If it is false from the beginning, there is no chance for the proof to succeed*/
__CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength);
xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
}
return xSet;
}
void harness(){
UBaseType_t uxQueueLength;
UBaseType_t uxItemSize;
uint8_t ucQueueType;
__CPROVER_assume(uxQueueLength > 0);
__CPROVER_assume(uxItemSize < 10);
/* The implicit assumption for the QueueGenericCreate method is,
that there are no overflows in the computation and the inputs are safe.
There is no check for this in the code base */
UBaseType_t upper_bound = portMAX_DELAY - sizeof(Queue_t);
__CPROVER_assume(uxItemSize < (upper_bound)/uxQueueLength);
QueueHandle_t xQueue =
xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
if(xQueue){
xQueue->cTxLock = LOCK_BOUND - 1;
xQueue->cRxLock = LOCK_BOUND - 1;
xQueue->uxMessagesWaiting = nondet_UBaseType_t();
/* This is an invariant checked with a couple of asserts in the code base.
If it is false from the beginning, there is no chance for the proof to succeed*/
__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
#if( configUSE_QUEUE_SETS == 1)
xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
#endif
prvUnlockQueue(xQueue);
}
}
|
