len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity

Exposed node owners in all predicates related to nodes. Adapted proofs to new predicates.

Browse source 
Changed predicates:
- `xLIST_ITEM`
- `DLS`
- `xLIST`
- `readyLists_p`
- `List_array_p`
This commit is contained in:
Tobias Reinhard 2022-11-30 09:44:25 -05:00
parent 70f1041778
commit e800ebd293
6 changed files with 713 additions and 369 deletions
Download patch file Download diff file Expand all files Collapse all files

57
tasks.c
View file

@ -987,47 +987,47 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
//@ open taskISRLockInv_p(); //@ open taskISRLockInv_p();
//@ open readyLists_p(?gCellLists); //@ open readyLists_p(?gCellLists, ?gOwnerLists);
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
//@ List_array_split(pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(pxReadyTasksLists, uxCurrentPriority);
//@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority]; //@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority];
//@ assert( xLIST(gReadyList, ?gSize, ?gIndex, ?gEnd, ?gCells, ?gVals) ); //@ assert( xLIST(gReadyList, ?gSize, ?gIndex, ?gEnd, ?gCells, ?gVals, ?gOwners) );
//@ open xLIST(gReadyList, _, _, _, _, _); //@ open xLIST(gReadyList, _, _, _, _, _, _);
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{ {
List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] ); List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] );
//@ assert( pxReadyList->pxIndex |-> gIndex ); //@ assert( pxReadyList->pxIndex |-> gIndex );
/*@ assert( DLS(gEnd, ?gEndPrev, gEnd, gEndPrev, /*@ assert( DLS(gEnd, ?gEndPrev, gEnd, gEndPrev,
gCells, gVals, gReadyList) ); gCells, gVals, gOwners, gReadyList) );
@*/ @*/
//@ DLS_open_2(pxReadyList->pxIndex); //@ DLS_open_2(pxReadyList->pxIndex);
//@ assert( xLIST_ITEM(gIndex, _, ?gIndexNext, ?gIndexPrev, gReadyList) ); //@ assert( xLIST_ITEM(gIndex, _, ?gIndexNext, ?gIndexPrev, _, gReadyList) );
ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious; ListItem_t * pxLastTaskItem = pxReadyList->pxIndex->pxPrevious;
ListItem_t * pxTaskItem = pxLastTaskItem; ListItem_t * pxTaskItem = pxLastTaskItem;
//@ close xLIST_ITEM(gIndex, _, gIndexNext, gIndexPrev, gReadyList); //@ close xLIST_ITEM(gIndex, _, gIndexNext, gIndexPrev, _, gReadyList);
//@ DLS_close_2(pxReadyList->pxIndex, gCells, gVals); //@ DLS_close_2(pxReadyList->pxIndex, gCells, gVals, gOwners);
//@ assert( mem(pxTaskItem, gCells) == true); //@ assert( mem(pxTaskItem, gCells) == true);
//@ open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gReadyList); //@ open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gReadyList);
//@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList) ); //@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, _, gReadyList) );
//@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList); //@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, _, gReadyList);
// opening required to prove validity of `&( pxReadyList->xListEnd )` // opening required to prove validity of `&( pxReadyList->xListEnd )`
///@ assert( pointer_within_limits( &pxReadyList->xListEnd ) == true ); ///@ assert( pointer_within_limits( &pxReadyList->xListEnd ) == true );
//@ close xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList); //@ close xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, _, gReadyList);
if( ( void * ) pxLastTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) if( ( void * ) pxLastTaskItem == ( void * ) &( pxReadyList->xListEnd ) )
{ {
//@ assert( gVals == cons(?gV, ?gRest) ); //@ assert( gVals == cons(?gV, ?gRest) );
//@ assert( xLIST_ITEM(?gOldLastTaskItem, gV, ?gO, gEndPrev, gReadyList) ); //@ assert( xLIST_ITEM(?gOldLastTaskItem, gV, ?gO, gEndPrev, _, gReadyList) );
pxLastTaskItem = pxLastTaskItem->pxPrevious; pxLastTaskItem = pxLastTaskItem->pxPrevious;
//@ close xLIST_ITEM(gOldLastTaskItem, gV, gO, gEndPrev, gReadyList); //@ close xLIST_ITEM(gOldLastTaskItem, gV, gO, gEndPrev, _, gReadyList);
} }
//@ close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gReadyList); //@ close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gReadyList);
//@ close xLIST(gReadyList, _, gIndex, gEnd, gCells, gVals); //@ close xLIST(gReadyList, _, gIndex, gEnd, gCells, gVals, gOwners);
/* The ready task list for uxCurrentPriority is not empty, so uxTopReadyPriority /* The ready task list for uxCurrentPriority is not empty, so uxTopReadyPriority
* must not be decremented any further */ * must not be decremented any further */
@ -1035,19 +1035,20 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ mem_nth(uxCurrentPriority, gCellLists); //@ mem_nth(uxCurrentPriority, gCellLists);
//@ assert( mem(gCells, gCellLists) == true); //@ assert( mem(gCells, gCellLists) == true);
//@ open_collection_of_sharedSeg_TCB(gCellLists, gCells); // //@ open_collection_of_sharedSeg_TCB(gCellLists, gCells);
do do
/*@ invariant /*@ invariant
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals) &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
foreach(gCells, sharedSeg_TCB_of_itemOwner); // foreach(gCells, sharedSeg_TCB_of_itemOwner);
true;
@*/ @*/
{ {
TCB_t * pxTCB; TCB_t * pxTCB;
//@ open xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals); //@ open xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
//@ assert( DLS(gEnd, ?gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gReadyList) ); //@ assert( DLS(gEnd, ?gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList) );
// Building an SSA for important variables helps us to // Building an SSA for important variables helps us to
// refer to the right instances. // refer to the right instances.
@ -1057,8 +1058,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
//@ close xLIST_ITEM(gTaskItem_0, _, _, _, gReadyList); //@ close xLIST_ITEM(gTaskItem_0, _, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_0, gCells, gVals); //@ DLS_close_2(gTaskItem_0, gCells, gVals, gOwners);
if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) )
{ {
@ -1066,20 +1067,20 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem;
//@ close xLIST_ITEM(gTaskItem_1, _, _, _, gReadyList); //@ close xLIST_ITEM(gTaskItem_1, _, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_1, gCells, gVals); //@ DLS_close_2(gTaskItem_1, gCells, gVals, gOwners);
} }
//@ struct xLIST_ITEM* gTaskItem_3 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_3 = pxTaskItem;
//@ DLS_open_2(gTaskItem_3); //@ DLS_open_2(gTaskItem_3);
pxTCB = pxTaskItem->pvOwner; pxTCB = pxTaskItem->pvOwner;
//@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList); //@ close xLIST_ITEM(gTaskItem_3, _, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_3, gCells, gVals); //@ DLS_close_2(gTaskItem_3, gCells, gVals, gOwners);
// Get access to sharedSeg_TCB_p(pxTCB). // Get access to sharedSeg_TCB_p(pxTCB).
//@ foreach_remove(gTaskItem_3, gCells); // //@ foreach_remove(gTaskItem_3, gCells);
//@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3); // //@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3);
/*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */

78
verification/verifast/proof/ready_list_predicates.h
View file

@ -7,69 +7,86 @@
/*@ /*@
// TODO: We know that the list of priority 0 is never empty. // TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else. // It contains the idle task and nothing else.
predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) = predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists,
list<list<void*> > gOwnerLists) =
configMAX_PRIORITIES == length(gCellLists) &*& configMAX_PRIORITIES == length(gCellLists) &*&
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists); List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES,
gCellLists, gOwnerLists);
predicate List_array_p(List_t* array, int size, predicate List_array_p(List_t* array, int size,
list<list<struct xLIST_ITEM*> > cellLists) = list<list<struct xLIST_ITEM*> > cellLists,
list<list<void*> > ownerLists) =
size >= 0 &*& size >= 0 &*&
length(cellLists) == size &*& length(cellLists) == size &*&
length(ownerLists) == length(cellLists) &*&
size > 0 size > 0
? ( ? (
cellLists == cons(?gCells, ?gTailcellLists) &*& cellLists == cons(?gCells, ?gTailCellLists) &*&
ownerLists == cons(?gOwners, ?gTailOwnerLists) &*&
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
xLIST(array, ?gNumberOfItems, ?gIndex, ?gListEnd, gCells, ?gVals) xLIST(array, ?gNumberOfItems, ?gIndex, ?gListEnd, gCells, ?gVals,
gOwners)
&*& &*&
List_array_p(array + 1, size - 1, gTailcellLists) List_array_p(array + 1, size - 1, gTailCellLists, gTailOwnerLists)
) )
: cellLists == nil; : (
cellLists == nil &*&
ownerLists == nil
);
lemma void List_array_size_positive(List_t* pxArray) lemma void List_array_size_positive(List_t* pxArray)
requires List_array_p(pxArray, ?gSize, ?gCellLists); requires List_array_p(pxArray, ?gSize, ?gCellLists, ?gOwnerLists);
ensures List_array_p(pxArray, gSize, gCellLists) &*& ensures
gSize >= 0 &*& gSize == length(gCellLists); List_array_p(pxArray, gSize, gCellLists, gOwnerLists) &*&
gSize >= 0 &*&
gSize == length(gCellLists) &*&
length(gCellLists) == length(gOwnerLists);
{ {
open List_array_p(pxArray, gSize, gCellLists); open List_array_p(pxArray, gSize, gCellLists, gOwnerLists);
close List_array_p(pxArray, gSize, gCellLists); close List_array_p(pxArray, gSize, gCellLists, gOwnerLists);
} }
lemma void List_array_split(List_t* array, int index) lemma void List_array_split(List_t* array, int index)
requires requires
List_array_p(array, ?gSize, ?gCellLists) &*& List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*&
0 <= index &*& index < gSize; 0 <= index &*& index < gSize;
ensures ensures
List_array_p(array, index, ?gPrefCellLists) &*& List_array_p(array, index, ?gPrefCellLists, ?gPrefOwnerLists) &*&
gPrefCellLists == take(index, gCellLists) &*& gPrefCellLists == take(index, gCellLists) &*&
gPrefOwnerLists == take(index, gOwnerLists) &*&
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
xLIST(array + index, _, _, _, ?gCells, ?vals) &*& xLIST(array + index, _, _, _, ?gCells, ?gVals, ?gOwners) &*&
gCells == nth(index, gCellLists) &*& gCells == nth(index, gCellLists) &*&
List_array_p(array + index + 1, gSize-index-1, ?gSufCellLists) &*& gOwners == nth(index, gOwnerLists) &*&
gSufCellLists == drop(index+1, gCellLists); List_array_p(array + index + 1, gSize-index-1, ?gSufCellLists, ?gSufOwnerLists) &*&
gSufCellLists == drop(index+1, gCellLists) &*&
gSufOwnerLists == drop(index+1, gOwnerLists);
{ {
open List_array_p(array, gSize, gCellLists); open List_array_p(array, gSize, gCellLists, gOwnerLists);
if( index > 0 ) { if( index > 0 ) {
List_array_split(array + 1, index - 1); List_array_split(array + 1, index - 1);
} }
close List_array_p(array, index, take(index, gCellLists)); close List_array_p(array, index, take(index, gCellLists), take(index, gOwnerLists));
} }
lemma void List_array_join(List_t* array) lemma void List_array_join(List_t* array)
requires requires
List_array_p(array, ?gPrefSize, ?gPrefCellLists) &*& List_array_p(array, ?gPrefSize, ?gPrefCellLists, ?gPrefOwnerLists) &*&
xLIST(array + gPrefSize, _, _, _, ?gCells, _) &*& xLIST(array + gPrefSize, _, _, _, ?gCells, _, ?gOwners) &*&
pointer_within_limits(array + gPrefSize) == true &*& pointer_within_limits(array + gPrefSize) == true &*&
List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists); List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists, ?gSufOwnerLists);
ensures ensures
List_array_p(array, ?gSize, ?gCellLists) &*& List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*&
gSize == length(gCellLists) &*& gSize == length(gCellLists) &*&
length(gCellLists) == length(gOwnerLists) &*&
gSize == gPrefSize + 1 + gSufSize &*& gSize == gPrefSize + 1 + gSufSize &*&
gCellLists == append(gPrefCellLists, cons(gCells, gSufCellLists)); gCellLists == append(gPrefCellLists, cons(gCells, gSufCellLists)) &*&
gOwnerLists == append(gPrefOwnerLists, cons(gOwners, gSufOwnerLists));
{ {
open List_array_p(array, gPrefSize, gPrefCellLists); open List_array_p(array, gPrefSize, gPrefCellLists, gPrefOwnerLists);
List_array_size_positive(array + gPrefSize + 1); List_array_size_positive(array + gPrefSize + 1);
if( gPrefSize > 0 ) { if( gPrefSize > 0 ) {
@ -77,7 +94,8 @@ ensures
} }
close List_array_p(array, gPrefSize + 1 + gSufSize, close List_array_p(array, gPrefSize + 1 + gSufSize,
append(gPrefCellLists, cons(gCells, gSufCellLists))); append(gPrefCellLists, cons(gCells, gSufCellLists)),
append(gPrefOwnerLists, cons(gOwners, gSufOwnerLists)));
} }
@*/ @*/
@ -87,16 +105,16 @@ ensures
/*@ /*@
lemma void List_array_p_index_within_limits(List_t* array, int index) lemma void List_array_p_index_within_limits(List_t* array, int index)
requires List_array_p(array, ?gSize, ?gCellListss) &*& requires List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*&
0 <= index &*& index < gSize; 0 <= index &*& index < gSize;
ensures List_array_p(array, gSize, gCellListss) &*& ensures List_array_p(array, gSize, gCellLists, gOwnerLists) &*&
pointer_within_limits(&array[index]) == true; pointer_within_limits(&array[index]) == true;
{ {
open List_array_p(array, gSize, gCellListss); open List_array_p(array, gSize, gCellLists, gOwnerLists);
if( index > 0) { if( index > 0) {
List_array_p_index_within_limits(&array[1], index-1); List_array_p_index_within_limits(&array[1], index-1);
} }
close List_array_p(array, gSize, gCellListss); close List_array_p(array, gSize, gCellLists, gOwnerLists);
} }
@*/ @*/

737
verification/verifast/proof/single_core_proofs/scp_list_predicates.h
View file

@ -129,10 +129,12 @@
#endif /* VERIFAST_SINGLE_CORE */ #endif /* VERIFAST_SINGLE_CORE */
#ifndef VERIFAST_SINGLE_CORE #ifndef VERIFAST_SINGLE_CORE
/* Reason for deletion: /* Reasons for rewrite:
* Breaking change in VeriFast. VeriFast now ensures that no uninitialised * - Breaking change in VeriFast. VeriFast now ensures that no uninitialised
* values are read. `x |-> _` is interpreted as "uninitialised", * values are read. `x |-> _` is interpreted as "uninitialised",
* `x |-> ?v` is interpreted as "initialised". * `x |-> ?v` is interpreted as "initialised".
* - In order to verify the scheduler, we have to reason about each node's
* owner. Hence, the predicate has to expose it.
*/ */
/*@ /*@
predicate xLIST_ITEM( predicate xLIST_ITEM(
@ -140,11 +142,12 @@
TickType_t xItemValue, TickType_t xItemValue,
struct xLIST_ITEM *pxNext, struct xLIST_ITEM *pxNext,
struct xLIST_ITEM *pxPrevious, struct xLIST_ITEM *pxPrevious,
void* pxOwner,
struct xLIST *pxContainer;) = struct xLIST *pxContainer;) =
n->xItemValue |-> xItemValue &*& n->xItemValue |-> xItemValue &*&
n->pxNext |-> pxNext &*& n->pxNext |-> pxNext &*&
n->pxPrevious |-> pxPrevious &*& n->pxPrevious |-> pxPrevious &*&
n->pvOwner |-> ?gOwner &*& n->pvOwner |-> pxOwner &*&
n->pxContainer |-> pxContainer; n->pxContainer |-> pxContainer;
@*/ @*/
#else #else
@ -163,240 +166,522 @@
@*/ @*/
#endif /* VERIFAST_SINGLE_CORE */ #endif /* VERIFAST_SINGLE_CORE */
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/*@
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
lemma void dls_star_item( #ifndef VERIFAST_SINGLE_CORE
struct xLIST_ITEM *n, /* Reason for rewrite:
struct xLIST_ITEM *m, * In order to verify the scheduler, we have to reason about each node's
struct xLIST_ITEM *o) * owner. Hence, the predicate has to expose it.
requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2); */
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
{ /* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
open DLS(n, nprev, mnext, m, cells, vals, l); /*@
if (n == m) { predicate DLS(
assert xLIST_ITEM(n, _, _, _, _); struct xLIST_ITEM *n,
open xLIST_ITEM(n, _, _, _, _); struct xLIST_ITEM *nprev,
open xLIST_ITEM(o, _, _, _, _); struct xLIST_ITEM *mnext,
assert n != o; struct xLIST_ITEM *m,
close xLIST_ITEM(o, _, _, _, _); list<struct xLIST_ITEM * > cells,
close xLIST_ITEM(n, _, _, _, _); list<TickType_t > vals,
close DLS(n, nprev, mnext, m, cells, vals, l); list<void*> owners,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
owners == cons(?ow, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, ow, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
owners == cons(?ow, ?owners0) &*&
xLIST_ITEM(n, v, ?o, nprev, ow, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, owners0, pxContainer);
@*/
#else
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/*@
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
@*/
#endif /* VERIFAST_SINGLE_CORE */
#ifndef VERIFAST_SINGLE_CORE
/* Reason for rewrite:
* Predicates `xLIST_ITEM` and `DLS` have been extended to expose node
* owners. Proofs using these predicates must be adapted as well.
*/
/*@
lemma void dls_star_item(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
struct xLIST_ITEM *o)
requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?owners, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?ow, ?l2);
ensures DLS(n, nprev, mnext, m, cells, vals, owners, l) &*& xLIST_ITEM(o, v, onext, oprev, ow, l2) &*& mem(o, cells) == false;
{
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
if (n == m) {
assert xLIST_ITEM(n, _, _, _, _, _);
open xLIST_ITEM(n, _, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
}
else {
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
dls_star_item(nnext, m, o);
open xLIST_ITEM(n, _, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
}
} }
else {
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_star_item(nnext, m, o); lemma void dls_distinct(
open xLIST_ITEM(n, _, _, _, _); struct xLIST_ITEM *n,
open xLIST_ITEM(o, _, _, _, _); struct xLIST_ITEM *nprev,
assert n != o; struct xLIST_ITEM *mnext,
close xLIST_ITEM(o, _, _, _, _); struct xLIST_ITEM *m,
close xLIST_ITEM(n, _, _, _, _); list<struct xLIST_ITEM * > cells)
close DLS(n, nprev, mnext, m, cells, vals, l); requires DLS(n, nprev, mnext, m, cells, ?vals, ?owners, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, owners, l) &*& distinct(cells) == true;
{
if (n == m) {
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
} else {
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
dls_distinct(nnext, n, mnext, m, tail(cells));
dls_star_item(nnext, m, n);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
}
} }
} @*/
#else
/*@
lemma void dls_distinct( lemma void dls_star_item(
struct xLIST_ITEM *n, struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev, struct xLIST_ITEM *m,
struct xLIST_ITEM *mnext, struct xLIST_ITEM *o)
struct xLIST_ITEM *m, requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2);
list<struct xLIST_ITEM * > cells) ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l); {
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
{
if (n == m) {
open DLS(n, nprev, mnext, m, cells, vals, l); open DLS(n, nprev, mnext, m, cells, vals, l);
close DLS(n, nprev, mnext, m, cells, vals, l); if (n == m) {
} else { assert xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
else {
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_star_item(nnext, m, o);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_distinct(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
{
if (n == m) {
open DLS(n, nprev, mnext, m, cells, vals, l);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
open DLS(n, nprev, mnext, m, cells, vals, l);
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_distinct(nnext, n, mnext, m, tail(cells));
dls_star_item(nnext, m, n);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
@*/
#endif /* VERIFAST_SINGLE_CORE */
#ifndef VERIFAST_SINGLE_CORE
/* Reason for rewrite:
* In order to verify the scheduler, we have to reason about each node's
* owner. Hence, the predicate has to expose it.
*/
/*@
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals,
list<void*> owners) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
length(owners) == length(cells) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, owners, l);
@*/
#else
/*@
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
@*/
#endif /* VERIFAST_SINGLE_CORE */
#ifndef VERIFAST_SINGLE_CORE
/* Reason for rewrite:
* Predicates `xLIST_ITEM`, `DLS` and `xLIST` have been extended to expose
* node owners. Proofs using these predicates must be adapted as well.
*/
/*@
lemma void xLIST_distinct_cells(struct xLIST *l)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals, ?owners);
ensures xLIST(l, n, idx, end, cells, vals, owners) &*& distinct(cells) == true;
{
open xLIST(l, n, idx, end, cells, vals, owners);
assert DLS(end, ?endprev, end, _, cells, vals, owners, l);
dls_distinct(end, endprev, end, endprev, cells);
close xLIST(l, n, idx, end, cells, vals, owners);
}
lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals, ?owners) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?ow, ?l2);
ensures xLIST(l, n, idx, end, cells, vals, owners) &*& xLIST_ITEM(x, v, xnext, xprev, ow, l2) &*& mem(x, cells) == false;
{
open xLIST(l, n, idx, end, cells, vals, owners);
assert DLS(end, ?endprev, end, _, cells, vals, owners, l);
dls_distinct(end, endprev, end, endprev, cells);
dls_star_item(end, endprev, x);
close xLIST(l, n, idx, end, cells, vals, owners);
}
lemma void dls_first_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?owners, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, owners, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
{
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
if (n == m) {
assert cells == cons(n, nil);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
} else {
assert cells == cons(n, ?tail);
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
}
}
lemma void dls_not_empty(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
struct xLIST_ITEM *x)
requires DLS(n, m, n, m, cells, ?vals, ?owners, ?l) &*& mem(x, cells) == true &*& x != n;
ensures DLS(n, m, n, m, cells, vals, owners, l) &*& n != m;
{
open DLS(n, m, n, m, cells, vals, owners, l);
close DLS(n, m, n, m, cells, vals, owners, l);
}
lemma void dls_last_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?owners, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, owners, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
{
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
if (n == m) {
// trivial
} else {
open xLIST_ITEM(n, _, ?nnext, _, _, l);
assert DLS(?o, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
dls_last_mem(o, n, mnext, m, tail(cells));
close xLIST_ITEM(n, _, nnext, _, _, l);
}
close DLS(n, nprev, mnext, m, cells, vals, owners, l);
}
lemma void split(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST_ITEM *x,
int i)
requires DLS(n, nprev, mnext, m, cells, vals, ?owners, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), take(i, owners), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), drop(i, owners), l) &*& xprev == nth(i-1, cells);
{
open DLS(n, nprev, mnext, m, cells, vals, owners, l);
assert n != m;
assert xLIST_ITEM(n, ?v, ?nnext, _, ?ow, _);
assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
if (nnext == x) {
close DLS(n, nprev, x, n, singleton(n), singleton(v), singleton(ow), l);
open DLS(x, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
open xLIST_ITEM(x, _, ?xnext, ?xprev, ?xow, l);
close xLIST_ITEM(x, _, xnext, xprev, xow, l);
close DLS(x, n, mnext, m, tail(cells), tail(vals), tail(owners), l);
} else {
assert nnext != x;
split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), take(i-1, tail(owners)), l);
dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
dls_star_item(nnext, xprev, n);
dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
assert n != xprev;
close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), take(i, owners), l);
}
}
lemma void join(
struct xLIST_ITEM *n1,
struct xLIST_ITEM *nprev1,
struct xLIST_ITEM *mnext1,
struct xLIST_ITEM *m1,
list<struct xLIST_ITEM * > cells1,
list<TickType_t > vals1,
struct xLIST_ITEM *n2,
struct xLIST_ITEM *nprev2,
struct xLIST_ITEM *mnext2,
struct xLIST_ITEM *m2,
list<struct xLIST_ITEM * > cells2,
list<TickType_t > vals2)
requires
DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?owners1, ?l) &*&
DLS(n2, nprev2, mnext2, m2, cells2, vals2, ?owners2, l) &*&
mnext1 == n2 &*& m1 == nprev2;
ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), append(owners1, owners2), l);
{
if (n1 == m1) {
dls_first_mem(n1, nprev1, mnext1, m1, cells1);
dls_last_mem(n2, nprev2, mnext2, m2, cells2);
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, owners1, l);
dls_star_item(n2, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), append(owners1, owners2) ,l);
} else {
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, owners1, l);
assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, ?owners1_tail, l);
join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
n2, nprev2, mnext2, m2, cells2, vals2);
assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), append(owners1_tail, owners2), l);
dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
dls_star_item(o, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), append(owners1, owners2), l);
}
}
@*/
#else
/*@
lemma void xLIST_distinct_cells(struct xLIST *l)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2);
ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
dls_star_item(end, endprev, x);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void dls_first_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
{
open DLS(n, nprev, mnext, m, cells, vals, l); open DLS(n, nprev, mnext, m, cells, vals, l);
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l); if (n == m) {
dls_distinct(nnext, n, mnext, m, tail(cells)); assert cells == cons(n, nil);
dls_star_item(nnext, m, n); close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
assert cells == cons(n, ?tail);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_not_empty(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
struct xLIST_ITEM *x)
requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n;
ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
{
open DLS(n, m, n, m, cells, vals, l);
close DLS(n, m, n, m, cells, vals, l);
}
lemma void dls_last_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
// trivial
} else {
open xLIST_ITEM(n, _, ?nnext, _, l);
assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l);
dls_last_mem(o, n, mnext, m, tail(cells));
close xLIST_ITEM(n, _, nnext, _, l);
}
close DLS(n, nprev, mnext, m, cells, vals, l); close DLS(n, nprev, mnext, m, cells, vals, l);
} }
}
predicate xLIST( lemma void split(
struct xLIST *l, struct xLIST_ITEM *n,
int uxNumberOfItems, struct xLIST_ITEM *nprev,
struct xLIST_ITEM *pxIndex, struct xLIST_ITEM *mnext,
struct xLIST_ITEM *xListEnd, struct xLIST_ITEM *m,
list<struct xLIST_ITEM *>cells, list<struct xLIST_ITEM * > cells,
list<TickType_t >vals) = list<TickType_t > vals,
l->uxNumberOfItems |-> uxNumberOfItems &*& struct xLIST_ITEM *x,
l->pxIndex |-> pxIndex &*& int i)
mem(pxIndex, cells) == true &*& requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
xListEnd == &(l->xListEnd) &*& ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), l) &*& xprev == nth(i-1, cells);
xListEnd == head(cells) &*& {
portMAX_DELAY == head(vals) &*& open DLS(n, nprev, mnext, m, cells, vals, l);
struct_xLIST_ITEM_padding(&l->xListEnd) &*& assert n != m;
length(cells) == length(vals) &*& assert xLIST_ITEM(n, ?v, ?nnext, _, _);
uxNumberOfItems + 1 == length(cells) &*& assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l); if (nnext == x) {
close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
lemma void xLIST_distinct_cells(struct xLIST *l) open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals); open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true; close xLIST_ITEM(x, _, xnext, xprev, l);
{ close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
open xLIST(l, n, idx, end, cells, vals); } else {
assert DLS(end, ?endprev, end, _, cells, vals, l); assert nnext != x;
dls_distinct(end, endprev, end, endprev, cells); split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
close xLIST(l, n, idx, end, cells, vals); assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
} dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
dls_star_item(nnext, xprev, n);
lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x) dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2); assert n != xprev;
ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false; close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
{ }
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
dls_star_item(end, endprev, x);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void dls_first_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
assert cells == cons(n, nil);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
assert cells == cons(n, ?tail);
close DLS(n, nprev, mnext, m, cells, vals, l);
} }
}
lemma void dls_not_empty( lemma void join(
struct xLIST_ITEM *n, struct xLIST_ITEM *n1,
struct xLIST_ITEM *m, struct xLIST_ITEM *nprev1,
list<struct xLIST_ITEM * > cells, struct xLIST_ITEM *mnext1,
struct xLIST_ITEM *x) struct xLIST_ITEM *m1,
requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n; list<struct xLIST_ITEM * > cells1,
ensures DLS(n, m, n, m, cells, vals, l) &*& n != m; list<TickType_t > vals1,
{ struct xLIST_ITEM *n2,
open DLS(n, m, n, m, cells, vals, l); struct xLIST_ITEM *nprev2,
close DLS(n, m, n, m, cells, vals, l); struct xLIST_ITEM *mnext2,
} struct xLIST_ITEM *m2,
list<struct xLIST_ITEM * > cells2,
lemma void dls_last_mem( list<TickType_t > vals2)
struct xLIST_ITEM *n, requires
struct xLIST_ITEM *nprev, DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
struct xLIST_ITEM *mnext, DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
struct xLIST_ITEM *m, mnext1 == n2 &*& m1 == nprev2;
list<struct xLIST_ITEM * > cells) ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l); {
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1; if (n1 == m1) {
{ dls_first_mem(n1, nprev1, mnext1, m1, cells1);
open DLS(n, nprev, mnext, m, cells, vals, l); dls_last_mem(n2, nprev2, mnext2, m2, cells2);
if (n == m) { open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
// trivial dls_star_item(n2, m2, n1);
} else { close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
open xLIST_ITEM(n, _, ?nnext, _, l); } else {
assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l); open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
dls_last_mem(o, n, mnext, m, tail(cells)); assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
close xLIST_ITEM(n, _, nnext, _, l); join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
n2, nprev2, mnext2, m2, cells2, vals2);
assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
dls_star_item(o, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
}
} }
close DLS(n, nprev, mnext, m, cells, vals, l); @*/
} #endif /* VERIFAST_SINGLE_CORE */
lemma void split(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST_ITEM *x,
int i)
requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), l) &*& xprev == nth(i-1, cells);
{
open DLS(n, nprev, mnext, m, cells, vals, l);
assert n != m;
assert xLIST_ITEM(n, ?v, ?nnext, _, _);
assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
if (nnext == x) {
close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
close xLIST_ITEM(x, _, xnext, xprev, l);
close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
} else {
assert nnext != x;
split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
dls_star_item(nnext, xprev, n);
dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
assert n != xprev;
close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
}
}
lemma void join(
struct xLIST_ITEM *n1,
struct xLIST_ITEM *nprev1,
struct xLIST_ITEM *mnext1,
struct xLIST_ITEM *m1,
list<struct xLIST_ITEM * > cells1,
list<TickType_t > vals1,
struct xLIST_ITEM *n2,
struct xLIST_ITEM *nprev2,
struct xLIST_ITEM *mnext2,
struct xLIST_ITEM *m2,
list<struct xLIST_ITEM * > cells2,
list<TickType_t > vals2)
requires
DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
mnext1 == n2 &*& m1 == nprev2;
ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
{
if (n1 == m1) {
dls_first_mem(n1, nprev1, mnext1, m1, cells1);
dls_last_mem(n2, nprev2, mnext2, m2, cells2);
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
dls_star_item(n2, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
} else {
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
n2, nprev2, mnext2, m2, cells2, vals2);
assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
dls_star_item(o, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
}
}
@*/
#ifdef VERIFAST_TODO #ifdef VERIFAST_TODO
lemma void idx_remains_in_list<t>( lemma void idx_remains_in_list<t>(

197
verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
View file

@ -359,6 +359,7 @@ ensures
} }
@*/ @*/
#ifdef IGNORE_DEPRECATED
/* By verifying the following function, we can validate that the above lemmas /* By verifying the following function, we can validate that the above lemmas
* apply to the use cases they are meant for. * apply to the use cases they are meant for.
*/ */
@ -410,6 +411,7 @@ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem)
//@ assert( mem(pxItem_1, gCells) == true ); //@ assert( mem(pxItem_1, gCells) == true );
} }
#endif I/* GNORE_DEPRECATED */
@ -429,6 +431,7 @@ predicate DLS_prefix(
// prefix args // prefix args
list<struct xLIST_ITEM*> prefCells, list<struct xLIST_ITEM*> prefCells,
list<TickType_t> prefVals, list<TickType_t> prefVals,
list<void*> prefOwners,
struct xLIST_ITEM* item, struct xLIST_ITEM* item,
struct xLIST_ITEM* itemPrev, struct xLIST_ITEM* itemPrev,
// unsplit DLS args // unsplit DLS args
@ -436,22 +439,26 @@ predicate DLS_prefix(
struct xLIST_ITEM *endPrev, struct xLIST_ITEM *endPrev,
struct xLIST *pxContainer) = struct xLIST *pxContainer) =
length(prefCells) == length(prefVals) &*& length(prefCells) == length(prefVals) &*&
length(prefOwners) == length(prefCells) &*&
switch(prefCells) { switch(prefCells) {
case nil: return case nil: return
prefVals == nil &*& prefVals == nil &*&
prefOwners == nil &*&
item == end &*& item == end &*&
itemPrev == endPrev; itemPrev == endPrev;
case cons(headItem, tailCells): return case cons(headItem, tailCells): return
item != end &*& item != end &*&
// itemPrev != endPrev &*& // do we need to know this? // itemPrev != endPrev &*& // do we need to know this?
headItem == end &*& headItem == end &*&
DLS(end, endPrev, item, itemPrev, prefCells, prefVals, pxContainer); DLS(end, endPrev, item, itemPrev, prefCells, prefVals, prefOwners,
pxContainer);
}; };
predicate DLS_suffix( predicate DLS_suffix(
// suffix args // suffix args
list<struct xLIST_ITEM*> sufCells, list<struct xLIST_ITEM*> sufCells,
list<TickType_t> sufVals, list<TickType_t> sufVals,
list<void*> sufOwners,
struct xLIST_ITEM* item, struct xLIST_ITEM* item,
struct xLIST_ITEM* itemNext, struct xLIST_ITEM* itemNext,
// unsplit DLS args // unsplit DLS args
@ -459,38 +466,43 @@ predicate DLS_suffix(
struct xLIST_ITEM *endPrev, struct xLIST_ITEM *endPrev,
struct xLIST *pxContainer) = struct xLIST *pxContainer) =
length(sufCells) == length(sufVals) &*& length(sufCells) == length(sufVals) &*&
length(sufOwners) == length(sufCells) &*&
switch(sufCells) { switch(sufCells) {
case nil: return case nil: return
sufVals == nil &*& sufVals == nil &*&
sufOwners == nil &*&
item == endPrev &*& item == endPrev &*&
itemNext == end; itemNext == end;
case cons(headItem, tailCells): return case cons(headItem, tailCells): return
item != endPrev &*& item != endPrev &*&
mem(endPrev, sufCells) == true &*& mem(endPrev, sufCells) == true &*&
index_of(endPrev, sufCells) == length(sufCells)-1 &*& index_of(endPrev, sufCells) == length(sufCells)-1 &*&
DLS(itemNext, item, end, endPrev, sufCells, sufVals, pxContainer); DLS(itemNext, item, end, endPrev, sufCells, sufVals, sufOwners,
pxContainer);
}; };
lemma void DLS_open_2(struct xLIST_ITEM* pxItem) lemma void DLS_open_2(struct xLIST_ITEM* pxItem)
requires requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*&
mem(pxItem, gCells) == true &*& mem(pxItem, gCells) == true &*&
gEnd == head(gCells) &*& gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
length(gOwners) == length(gCells) &*&
length(gCells) > 1; length(gCells) > 1;
ensures ensures
DLS_prefix(?gPrefCells, ?gPrefVals, pxItem, ?gItemPrev, DLS_prefix(?gPrefCells, ?gPrefVals, ?gPrefOwners, pxItem, ?gItemPrev,
gEnd, gEndPrev, gList) gEnd, gEndPrev, gList)
&*& &*&
xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, gList) xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, ?gOw, gList)
&*& &*&
DLS_suffix(?gSufCells, ?gSufVals, pxItem, gItemNext, gEnd, gEndPrev, gList) DLS_suffix(?gSufCells, ?gSufVals, ?gSufOwners, pxItem, gItemNext,
gEnd, gEndPrev, gList)
&*& &*&
// gCells == gPrefCells + item + gSufCells // lists have form "prefix + element + suffix"
gCells == append(gPrefCells, append(singleton(pxItem), gSufCells)) &*& gCells == append(gPrefCells, append(singleton(pxItem), gSufCells)) &*&
// gVals == gPrefVals + item + gSufVals gVals == append(gPrefVals, append(singleton(gItemVal), gSufVals)) &*&
gVals == append(gPrefVals, append(singleton(gItemVal), gSufVals)) gOwners == append(gPrefOwners, append(singleton(gOw), gSufOwners))
&*& &*&
// next in cells // next in cells
mem(gItemNext, gCells) == true &*& mem(gItemNext, gCells) == true &*&
@ -502,25 +514,27 @@ ensures
// pxItem is first/ left-most item in the list // pxItem is first/ left-most item in the list
// -> empty prefix // -> empty prefix
open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList);
assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, ?gItemPrev, gList) ); assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, ?gItemPrev, ?gOw, gList) );
assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, ?gSufCells, ?gSufVals, assert( DLS(gItemNext, pxItem, gEnd, gEndPrev,
gList) ); ?gSufCells, ?gSufVals, ?gSufOwners, gList) );
close DLS_prefix(nil, nil, pxItem, gItemPrev, close DLS_prefix(nil, nil, nil, pxItem, gItemPrev,
gEnd, gEndPrev, gList); gEnd, gEndPrev, gList);
// Prove: `mem(gItemNext, gCells) == true` // Prove: `mem(gItemNext, gCells) == true`
open DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, gList); open DLS(gItemNext, pxItem, gEnd, gEndPrev,
gSufCells, gSufVals, gSufOwners, gList);
assert( mem(gItemNext, gCells) == true ); assert( mem(gItemNext, gCells) == true );
close DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, gList); close DLS(gItemNext, pxItem, gEnd, gEndPrev,
gSufCells, gSufVals, gSufOwners, gList);
// Prove: `mem(gItemPrev, gCells) == true ` // Prove: `mem(gItemPrev, gCells) == true `
assert( gItemPrev == gEndPrev ); assert( gItemPrev == gEndPrev );
dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells); dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells);
assert( mem(gItemPrev, gCells) == true ); assert( mem(gItemPrev, gCells) == true );
close DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, gEndPrev, close DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gList); gEnd, gEndPrev, gList);
} else { } else {
// pxItem is not the first/ left-most item in the list // pxItem is not the first/ left-most item in the list
// -> non-empty prefix // -> non-empty prefix
@ -529,13 +543,13 @@ ensures
int gItemIndex = index_of(pxItem, gCells); int gItemIndex = index_of(pxItem, gCells);
split(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxItem, gItemIndex); split(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxItem, gItemIndex);
assert( DLS(gEnd, gEndPrev, pxItem, ?gItemPrev, ?gPrefCells, ?gPrefVals, assert( DLS(gEnd, gEndPrev, pxItem, ?gItemPrev,
gList) ); ?gPrefCells, ?gPrefVals, ?gPrefOwners, gList) );
// -> Will be wrapped inside the prefix constructed at the end of this // -> Will be wrapped inside the prefix constructed at the end of this
// lemma. // lemma.
assert( DLS(pxItem, gItemPrev, gEnd, gEndPrev, ?gPartCells, ?gPartVals, assert( DLS(pxItem, gItemPrev, gEnd, gEndPrev,
gList) ); ?gPartCells, ?gPartVals, ?gPartOwners, gList) );
// -> The tail of this DLS will make up the suffix constructed at the // -> The tail of this DLS will make up the suffix constructed at the
// end of this lemma. // end of this lemma.
@ -547,16 +561,16 @@ ensures
// Prove: `head(gPrefCells) == gEnd` // Prove: `head(gPrefCells) == gEnd`
// Necessary to construct prefix later. // Necessary to construct prefix later.
// Implies `mem(gItemPrev, gCells) == true`. // Implies `mem(gItemPrev, gCells) == true`.
open DLS(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, open DLS(gEnd, gEndPrev, pxItem, gItemPrev,
gList); gPrefCells, gPrefVals, gPrefOwners, gList);
assert( head(gPrefCells) == gEnd ); assert( head(gPrefCells) == gEnd );
close DLS(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, close DLS(gEnd, gEndPrev, pxItem, gItemPrev,
gList); gPrefCells, gPrefVals, gPrefOwners, gList);
assert( mem(gItemPrev, gCells) == true ); assert( mem(gItemPrev, gCells) == true );
open DLS(pxItem, gItemPrev, gEnd, gEndPrev, gPartCells, gPartVals, open DLS(pxItem, gItemPrev, gEnd, gEndPrev,
gList); gPartCells, gPartVals, gPartOwners, gList);
assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, gList) ); assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, ?gOw, gList) );
if( pxItem == gEndPrev ) { if( pxItem == gEndPrev ) {
// pxItem is the last/ right-most item in the list. // pxItem is the last/ right-most item in the list.
@ -572,69 +586,78 @@ ensures
// prove: mem(gItemNext, gCells) == true // prove: mem(gItemNext, gCells) == true
open xLIST_ITEM(pxItem, gItemVal, gItemNext, gItemPrev, gList); open xLIST_ITEM(pxItem, gItemVal, gItemNext, gItemPrev, gOw,
gList);
assert( gItemNext == gEnd ); assert( gItemNext == gEnd );
assert( mem(gItemNext, gCells) == true ); assert( mem(gItemNext, gCells) == true );
close xLIST_ITEM(pxItem, gItemVal, gItemNext, gItemPrev, gList); close xLIST_ITEM(pxItem, gItemVal, gItemNext, gItemPrev, gOw,
gList);
close DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, close DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, pxItem,
gItemPrev, gEnd, gEndPrev, gList);
close DLS_suffix(nil, nil, nil, pxItem, gItemNext,
gEnd, gEndPrev, gList); gEnd, gEndPrev, gList);
close DLS_suffix(nil, nil, pxItem, gItemNext, gEnd, gEndPrev, gList);
} else { } else {
// pxItem is not the last/ right-most item in the list. // pxItem is not the last/ right-most item in the list.
// -> non-empty suffix // -> non-empty suffix
assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, ?gSufCells, ?gSufVals, assert( DLS(gItemNext, pxItem, gEnd, gEndPrev,
gList) ); ?gSufCells, ?gSufVals, ?gSufOwners, gList) );
assert( gSufCells == drop(1, gPartCells) ); assert( gSufCells == drop(1, gPartCells) );
// Prove: - `drop(gItemIndex+1, gCells) == gSufCells` // Prove: - `drop(gItemIndex+1, gCells) == gSufCells`
// - `drop(gItemIndex+1, gVals) == gSufVals` // - `drop(gItemIndex+1, gVals) == gSufVals`
// - `drop(gItemIndex+1, gOwners) == gSufOwners`
// -> Required to prove `mem(gItemNext, gCells) == true` and also to // -> Required to prove `mem(gItemNext, gCells) == true` and also to
// prove relationship between gCells/gVals and their segmentation. // prove relationship between gCells/gVals and their segmentation.
assert( drop(1, drop(gItemIndex, gCells)) == gSufCells ); assert( drop(1, drop(gItemIndex, gCells)) == gSufCells );
assert( drop(1, drop(gItemIndex, gVals)) == gSufVals ); assert( drop(1, drop(gItemIndex, gVals)) == gSufVals );
assert( drop(1, drop(gItemIndex, gOwners)) == gSufOwners );
drop_n_plus_m(gCells, 1, gItemIndex); drop_n_plus_m(gCells, 1, gItemIndex);
drop_n_plus_m(gVals, 1, gItemIndex); drop_n_plus_m(gVals, 1, gItemIndex);
drop_n_plus_m(gOwners, 1, gItemIndex);
assert( drop(gItemIndex+1, gCells) == gSufCells ); assert( drop(gItemIndex+1, gCells) == gSufCells );
assert( drop(gItemIndex+1, gVals) == gSufVals ); assert( drop(gItemIndex+1, gVals) == gSufVals );
assert( drop(gItemIndex+1, gOwners) == gSufOwners );
// Prove: `mem(gItemNext, gCells) == true` // Prove: `mem(gItemNext, gCells) == true`
open DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, open DLS(gItemNext, pxItem, gEnd, gEndPrev,
gList); gSufCells, gSufVals, gSufOwners, gList);
assert( mem(gItemNext, gSufCells) == true ); assert( mem(gItemNext, gSufCells) == true );
mem_suffix_implies_mem(gItemNext, gCells, gItemIndex+1); mem_suffix_implies_mem(gItemNext, gCells, gItemIndex+1);
assert( mem(gItemNext, gCells) == true ); assert( mem(gItemNext, gCells) == true );
close DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, close DLS(gItemNext, pxItem, gEnd, gEndPrev,
gList); gSufCells, gSufVals, gSufOwners, gList);
close DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, close DLS_prefix(gPrefCells, gPrefVals, gPrefOwners,
gEnd, gEndPrev, gList); pxItem, gItemPrev, gEnd, gEndPrev, gList);
dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells); dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells);
close DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, close DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gEndPrev, gList); gEnd, gEndPrev, gList);
} }
} }
} }
lemma void DLS_close_2(struct xLIST_ITEM* pxItem, lemma void DLS_close_2(struct xLIST_ITEM* pxItem,
list<struct xLIST_ITEM*> gCells, list<struct xLIST_ITEM*> gCells,
list<TickType_t> gVals) list<TickType_t> gVals,
list<void*> gOwners)
requires requires
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
DLS_prefix(?gPrefCells, ?gPrefVals, pxItem, ?gItemPrev, DLS_prefix(?gPrefCells, ?gPrefVals, ?gPrefOwners, pxItem, ?gItemPrev,
?gEnd, ?gEndPrev, ?gList) ?gEnd, ?gEndPrev, ?gList)
&*& &*&
gEnd == head(gCells) gEnd == head(gCells)
&*& &*&
xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, gList) xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, ?gOw, gList)
&*& &*&
DLS_suffix(?gSufCells, ?gSufVals, pxItem, gItemNext, gEnd, gEndPrev, gList) DLS_suffix(?gSufCells, ?gSufVals, ?gSufOwners, pxItem, gItemNext,
gEnd, gEndPrev, gList)
&*& &*&
// gCells == gPrefCells + item + gSufCells // lists have form "prefix + element + suffix"
gCells == append(gPrefCells, append(singleton(pxItem), gSufCells)) &*& gCells == append(gPrefCells, append(singleton(pxItem), gSufCells)) &*&
// gVals == gPrefVals + item + gSufVals gVals == append(gPrefVals, append(singleton(gItemVal), gSufVals)) &*&
gVals == append(gPrefVals, append(singleton(gItemVal), gSufVals)) gOwners == append(gPrefOwners, append(singleton(gOw), gSufOwners))
&*& &*&
// next in cells // next in cells
mem(gItemNext, gCells) == true &*& mem(gItemNext, gCells) == true &*&
@ -642,7 +665,7 @@ requires
mem(gItemPrev, gCells) == true mem(gItemPrev, gCells) == true
; ;
ensures ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*&
mem(pxItem, gCells) == true &*& mem(pxItem, gCells) == true &*&
mem(gItemNext, gCells) == true &*& mem(gItemNext, gCells) == true &*&
mem(gItemPrev, gCells) == true &*& mem(gItemPrev, gCells) == true &*&
@ -654,7 +677,7 @@ ensures
// pxItem is first/ left-most item in the list // pxItem is first/ left-most item in the list
// -> empty prefix // -> empty prefix
open DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, open DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, pxItem, gItemPrev,
gEnd, gEndPrev, gList); gEnd, gEndPrev, gList);
assert( pxItem == gEnd ); assert( pxItem == gEnd );
assert( gPrefVals == nil ); assert( gPrefVals == nil );
@ -662,36 +685,39 @@ ensures
if( gSufCells == nil ) { if( gSufCells == nil ) {
// pxItem is last/ right-most item in the list // pxItem is last/ right-most item in the list
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gEndPrev, gList); gEnd, gEndPrev, gList);
assert( pxItem == gEndPrev ); assert( pxItem == gEndPrev );
assert( gSufVals == nil ); assert( gSufVals == nil );
close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners,
gList);
} else { } else {
// pxItem is not last/ right-most item in the list // pxItem is not last/ right-most item in the list
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gEndPrev, gList); gEnd, gEndPrev, gList);
close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners,
gList);
} }
} else { } else {
// pxItem is not the first/ left-most item in the list // pxItem is not the first/ left-most item in the list
// -> non-empty prefix // -> non-empty prefix
// (potentially empty suffix) // (potentially empty suffix)
open DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, open DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, pxItem, gItemPrev,
gEnd, gEndPrev, gList); gEnd, gEndPrev, gList);
if( gSufCells == nil ) { if( gSufCells == nil ) {
// pxItem is the last/ right-most item in the list // pxItem is the last/ right-most item in the list
// -> empty suffix // -> empty suffix
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gEndPrev, gList); gEnd, gEndPrev, gList);
assert( pxItem == gEndPrev ); assert( pxItem == gEndPrev );
close DLS(pxItem, gItemPrev, gEnd, gEndPrev, close DLS(pxItem, gItemPrev, gEnd, gEndPrev,
singleton(pxItem), singleton(gItemVal), gList); singleton(pxItem), singleton(gItemVal), singleton(gOw),
gList);
join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals,
pxItem, gItemPrev, gEnd, gEndPrev, pxItem, gItemPrev, gEnd, gEndPrev,
singleton(pxItem), singleton(gItemVal)); singleton(pxItem), singleton(gItemVal));
@ -699,10 +725,11 @@ ensures
// pxItem is not the last/ right-most item in the list // pxItem is not the last/ right-most item in the list
// -> non-empty suffix // -> non-empty suffix
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext,
gEndPrev, gList); gEnd, gEndPrev, gList);
close DLS(pxItem, gItemPrev, gEnd, gEndPrev, close DLS(pxItem, gItemPrev, gEnd, gEndPrev,
cons(pxItem, gSufCells), cons(gItemVal, gSufVals), cons(pxItem, gSufCells), cons(gItemVal, gSufVals),
cons(gOw, gSufOwners),
gList); gList);
join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals,
pxItem, gItemPrev, gEnd, gEndPrev, pxItem, gItemPrev, gEnd, gEndPrev,
@ -714,14 +741,15 @@ ensures
struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem) struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem)
/*@ requires /*@ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
gEnd == head(gCells) &*& gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
length(gOwners) == length(gCells) &*&
length(gCells) > 1; length(gCells) > 1;
@*/ @*/
/*@ ensures /*@ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
mem(result, gCells) == true; mem(result, gCells) == true;
@*/ @*/
@ -732,30 +760,34 @@ struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskIt
//@ DLS_open_2(gTaskItem_0); //@ DLS_open_2(gTaskItem_0);
/*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val, /*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val,
?gTaskItem_0_next, ?gTaskItem_0_prev, gList) ); ?gTaskItem_0_next, ?gTaskItem_0_prev, ?gTaskItem_0_owner,
gList) );
@*/ @*/
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val, /*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val,
gTaskItem_0_next, gTaskItem_0_prev, gList); gTaskItem_0_next, gTaskItem_0_prev, gTaskItem_0_owner,
gList);
@*/ @*/
//@ DLS_close_2(gTaskItem_0, gCells, gVals); //@ DLS_close_2(gTaskItem_0, gCells, gVals, gOwners);
// second iteration step // second iteration step
//@ DLS_open_2(gTaskItem_1); //@ DLS_open_2(gTaskItem_1);
/*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val, /*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val,
?gTaskItem_1_next, ?gTaskItem_1_prev, gList) ); ?gTaskItem_1_next, ?gTaskItem_1_prev, ?gTaskItem_1_owner,
gList) );
@*/ @*/
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val, /*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val,
gTaskItem_1_next, gTaskItem_1_prev, gList); gTaskItem_1_next, gTaskItem_1_prev, gTaskItem_1_owner,
gList);
@*/ @*/
//@ DLS_close_2(gTaskItem_1, gCells, gVals); //@ DLS_close_2(gTaskItem_1, gCells, gVals, gOwners);
//@ assert( mem(gTaskItem_2, gCells) == true ); //@ assert( mem(gTaskItem_2, gCells) == true );
@ -765,14 +797,15 @@ struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskIt
struct xLIST_ITEM* lemma_validation__DLS_item_prev_2(struct xLIST_ITEM* pxTaskItem) struct xLIST_ITEM* lemma_validation__DLS_item_prev_2(struct xLIST_ITEM* pxTaskItem)
/*@ requires /*@ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
gEnd == head(gCells) &*& gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
length(gOwners) == length(gCells) &*&
length(gCells) > 1; length(gCells) > 1;
@*/ @*/
/*@ ensures /*@ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
mem(result, gCells) == true; mem(result, gCells) == true;
@*/ @*/
@ -783,30 +816,34 @@ struct xLIST_ITEM* lemma_validation__DLS_item_prev_2(struct xLIST_ITEM* pxTaskIt
//@ DLS_open_2(gTaskItem_0); //@ DLS_open_2(gTaskItem_0);
/*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val, /*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val,
?gTaskItem_0_next, ?gTaskItem_0_prev, gList) ); ?gTaskItem_0_next, ?gTaskItem_0_prev, ?gTaskItem_0_owner,
gList) );
@*/ @*/
pxTaskItem = pxTaskItem->pxPrevious; pxTaskItem = pxTaskItem->pxPrevious;
//@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val, /*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val,
gTaskItem_0_next, gTaskItem_0_prev, gList); gTaskItem_0_next, gTaskItem_0_prev, gTaskItem_0_owner,
gList);
@*/ @*/
//@ DLS_close_2(gTaskItem_0, gCells, gVals); //@ DLS_close_2(gTaskItem_0, gCells, gVals, gOwners);
// second iteration step // second iteration step
//@ DLS_open_2(gTaskItem_1); //@ DLS_open_2(gTaskItem_1);
/*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val, /*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val,
?gTaskItem_1_next, ?gTaskItem_1_prev, gList) ); ?gTaskItem_1_next, ?gTaskItem_1_prev, ?gTaskItem_1_owner,
gList) );
@*/ @*/
pxTaskItem = pxTaskItem->pxPrevious; pxTaskItem = pxTaskItem->pxPrevious;
//@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val, /*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val,
gTaskItem_1_next, gTaskItem_1_prev, gList); gTaskItem_1_next, gTaskItem_1_prev,gTaskItem_1_owner,
gList);
@*/ @*/
//@ DLS_close_2(gTaskItem_1, gCells, gVals); //@ DLS_close_2(gTaskItem_1, gCells, gVals, gOwners);
//@ assert( mem(gTaskItem_2, gCells) == true ); //@ assert( mem(gTaskItem_2, gCells) == true );

8
verification/verifast/proof/task_predicates.h
View file

@ -12,9 +12,9 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxTopOfStack |-> _ &*& tcb->pxTopOfStack |-> _ &*&
xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*&
xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& xLIST_ITEM(&tcb->xEventListItem, _, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*& tcb->uxPriority |-> _ &*&
@ -59,9 +59,9 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
stack_p_2(stackPtr, ?ulStackDepth, topPtr, stack_p_2(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*& ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*&
xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*&
xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& xLIST_ITEM(&tcb->xEventListItem, _, _, _, _, _) &*&
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*& tcb->uxPriority |-> _ &*&

5
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -92,7 +92,7 @@ predicate taskISRLockInv_p() =
integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*& integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
&*& &*&
readyLists_p(?gCellLists) readyLists_p(?gCellLists, ?gOwnerLists)
&*& &*&
// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner) // ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
//foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner); //foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner);
@ -117,6 +117,9 @@ ensures locked_p(otherLocks);
// ∀items ∈ itemLists. ∀it ∈ items. sharedSeg_TCB_p(it->pvOwner) // ∀items ∈ itemLists. ∀it ∈ items. sharedSeg_TCB_p(it->pvOwner)
predicate collection_of_sharedSeg_TCB_p(list<list<struct xLIST_ITEM*> > itemLists) = predicate collection_of_sharedSeg_TCB_p(list<list<struct xLIST_ITEM*> > itemLists) =
true;
@*/
/*
foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner); foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner);
// Auxiliary prediactes to express nested quantification // Auxiliary prediactes to express nested quantification