diff --git a/tasks.c b/tasks.c index 3a35acd28..fd6f74a94 100644 --- a/tasks.c +++ b/tasks.c @@ -987,47 +987,47 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif //@ open taskISRLockInv_p(); - //@ open readyLists_p(?gCellLists); + //@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(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 ) { List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] ); //@ assert( pxReadyList->pxIndex |-> gIndex ); /*@ assert( DLS(gEnd, ?gEndPrev, gEnd, gEndPrev, - gCells, gVals, gReadyList) ); + gCells, gVals, gOwners, gReadyList) ); @*/ //@ 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 * pxTaskItem = pxLastTaskItem; - //@ close xLIST_ITEM(gIndex, _, gIndexNext, gIndexPrev, gReadyList); - //@ DLS_close_2(pxReadyList->pxIndex, gCells, gVals); + //@ close xLIST_ITEM(gIndex, _, gIndexNext, gIndexPrev, _, gReadyList); + //@ DLS_close_2(pxReadyList->pxIndex, gCells, gVals, gOwners); //@ assert( mem(pxTaskItem, gCells) == true); - //@ open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gReadyList); - //@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList) ); - //@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList); + //@ open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gReadyList); + //@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, _, gReadyList) ); + //@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, _, gReadyList); // opening required to prove validity of `&( pxReadyList->xListEnd )` ///@ 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 ) ) { //@ assert( gVals == cons(?gV, ?gRest) ); - //@ assert( xLIST_ITEM(?gOldLastTaskItem, gV, ?gO, gEndPrev, gReadyList) ); + //@ assert( xLIST_ITEM(?gOldLastTaskItem, gV, ?gO, gEndPrev, _, gReadyList) ); 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 xLIST(gReadyList, _, gIndex, gEnd, gCells, gVals); + //@ close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gReadyList); + //@ close xLIST(gReadyList, _, gIndex, gEnd, gCells, gVals, gOwners); /* The ready task list for uxCurrentPriority is not empty, so uxTopReadyPriority * must not be decremented any further */ @@ -1035,19 +1035,20 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ mem_nth(uxCurrentPriority, gCellLists); //@ assert( mem(gCells, gCellLists) == true); - //@ open_collection_of_sharedSeg_TCB(gCellLists, gCells); +// //@ open_collection_of_sharedSeg_TCB(gCellLists, gCells); do /*@ invariant mem(pxTaskItem, gCells) == true &*& - xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals) &*& - foreach(gCells, sharedSeg_TCB_of_itemOwner); + xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& +// foreach(gCells, sharedSeg_TCB_of_itemOwner); + true; @*/ { TCB_t * pxTCB; - //@ open xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals); - //@ assert( DLS(gEnd, ?gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gReadyList) ); + //@ open xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); + //@ assert( DLS(gEnd, ?gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList) ); // Building an SSA for important variables helps us to // refer to the right instances. @@ -1057,8 +1058,8 @@ static void prvYieldForTask( TCB_t * pxTCB, pxTaskItem = pxTaskItem->pxNext; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; - //@ close xLIST_ITEM(gTaskItem_0, _, _, _, gReadyList); - //@ DLS_close_2(gTaskItem_0, gCells, gVals); + //@ close xLIST_ITEM(gTaskItem_0, _, _, _, _, gReadyList); + //@ DLS_close_2(gTaskItem_0, gCells, gVals, gOwners); if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) { @@ -1066,20 +1067,20 @@ static void prvYieldForTask( TCB_t * pxTCB, pxTaskItem = pxTaskItem->pxNext; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; - //@ close xLIST_ITEM(gTaskItem_1, _, _, _, gReadyList); - //@ DLS_close_2(gTaskItem_1, gCells, gVals); + //@ close xLIST_ITEM(gTaskItem_1, _, _, _, _, gReadyList); + //@ DLS_close_2(gTaskItem_1, gCells, gVals, gOwners); } //@ struct xLIST_ITEM* gTaskItem_3 = pxTaskItem; //@ DLS_open_2(gTaskItem_3); pxTCB = pxTaskItem->pvOwner; - //@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList); - //@ DLS_close_2(gTaskItem_3, gCells, gVals); + //@ close xLIST_ITEM(gTaskItem_3, _, _, _, _, gReadyList); + //@ DLS_close_2(gTaskItem_3, gCells, gVals, gOwners); // Get access to sharedSeg_TCB_p(pxTCB). - //@ foreach_remove(gTaskItem_3, gCells); - //@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3); +// //@ foreach_remove(gTaskItem_3, gCells); +// //@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3); /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h index d058465cc..8a0da795a 100644 --- a/verification/verifast/proof/ready_list_predicates.h +++ b/verification/verifast/proof/ready_list_predicates.h @@ -7,69 +7,86 @@ /*@ // TODO: We know that the list of priority 0 is never empty. // It contains the idle task and nothing else. -predicate readyLists_p(list > gCellLists) = +predicate readyLists_p(list > gCellLists, + list > gOwnerLists) = 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, - list > cellLists) = + list > cellLists, + list > ownerLists) = size >= 0 &*& length(cellLists) == size &*& + length(ownerLists) == length(cellLists) &*& size > 0 ? ( - cellLists == cons(?gCells, ?gTailcellLists) &*& + cellLists == cons(?gCells, ?gTailCellLists) &*& + ownerLists == cons(?gOwners, ?gTailOwnerLists) &*& 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) -requires List_array_p(pxArray, ?gSize, ?gCellLists); -ensures List_array_p(pxArray, gSize, gCellLists) &*& - gSize >= 0 &*& gSize == length(gCellLists); +requires List_array_p(pxArray, ?gSize, ?gCellLists, ?gOwnerLists); +ensures + List_array_p(pxArray, gSize, gCellLists, gOwnerLists) &*& + gSize >= 0 &*& + gSize == length(gCellLists) &*& + length(gCellLists) == length(gOwnerLists); { - open List_array_p(pxArray, gSize, gCellLists); - close List_array_p(pxArray, gSize, gCellLists); + open List_array_p(pxArray, gSize, gCellLists, gOwnerLists); + close List_array_p(pxArray, gSize, gCellLists, gOwnerLists); } lemma void List_array_split(List_t* array, int index) requires - List_array_p(array, ?gSize, ?gCellLists) &*& + List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*& 0 <= index &*& index < gSize; ensures - List_array_p(array, index, ?gPrefCellLists) &*& + List_array_p(array, index, ?gPrefCellLists, ?gPrefOwnerLists) &*& gPrefCellLists == take(index, gCellLists) &*& + gPrefOwnerLists == take(index, gOwnerLists) &*& pointer_within_limits(array) == true &*& - xLIST(array + index, _, _, _, ?gCells, ?vals) &*& + xLIST(array + index, _, _, _, ?gCells, ?gVals, ?gOwners) &*& gCells == nth(index, gCellLists) &*& - List_array_p(array + index + 1, gSize-index-1, ?gSufCellLists) &*& - gSufCellLists == drop(index+1, gCellLists); + gOwners == nth(index, gOwnerLists) &*& + 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 ) { 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) requires - List_array_p(array, ?gPrefSize, ?gPrefCellLists) &*& - xLIST(array + gPrefSize, _, _, _, ?gCells, _) &*& + List_array_p(array, ?gPrefSize, ?gPrefCellLists, ?gPrefOwnerLists) &*& + xLIST(array + gPrefSize, _, _, _, ?gCells, _, ?gOwners) &*& pointer_within_limits(array + gPrefSize) == true &*& - List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists); + List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists, ?gSufOwnerLists); ensures - List_array_p(array, ?gSize, ?gCellLists) &*& + List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*& gSize == length(gCellLists) &*& + length(gCellLists) == length(gOwnerLists) &*& 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); if( gPrefSize > 0 ) { @@ -77,7 +94,8 @@ ensures } 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) -requires List_array_p(array, ?gSize, ?gCellListss) &*& +requires List_array_p(array, ?gSize, ?gCellLists, ?gOwnerLists) &*& 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; { - open List_array_p(array, gSize, gCellListss); + open List_array_p(array, gSize, gCellLists, gOwnerLists); if( index > 0) { 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); } @*/ diff --git a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h index a839ee314..9b8ac49df 100644 --- a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h +++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h @@ -129,10 +129,12 @@ #endif /* VERIFAST_SINGLE_CORE */ #ifndef VERIFAST_SINGLE_CORE - /* Reason for deletion: - * Breaking change in VeriFast. VeriFast now ensures that no uninitialised - * values are read. `x |-> _` is interpreted as "uninitialised", - * `x |-> ?v` is interpreted as "initialised". + /* Reasons for rewrite: + * - Breaking change in VeriFast. VeriFast now ensures that no uninitialised + * values are read. `x |-> _` is interpreted as "uninitialised", + * `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( @@ -140,11 +142,12 @@ TickType_t xItemValue, struct xLIST_ITEM *pxNext, struct xLIST_ITEM *pxPrevious, + void* pxOwner, struct xLIST *pxContainer;) = n->xItemValue |-> xItemValue &*& n->pxNext |-> pxNext &*& n->pxPrevious |-> pxPrevious &*& - n->pvOwner |-> ?gOwner &*& + n->pvOwner |-> pxOwner &*& n->pxContainer |-> pxContainer; @*/ #else @@ -163,240 +166,522 @@ @*/ #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 cells, - list 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( - struct xLIST_ITEM *n, - struct xLIST_ITEM *m, - struct xLIST_ITEM *o) -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; -{ - open DLS(n, nprev, mnext, m, cells, vals, 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, l); +#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. + */ + + /* 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 cells, + list vals, + list 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 cells, + list 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); - 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 cells) + 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); + } } -} - - -lemma void dls_distinct( - struct xLIST_ITEM *n, - struct xLIST_ITEM *nprev, - struct xLIST_ITEM *mnext, - struct xLIST_ITEM *m, - list 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) { + @*/ +#else + /*@ + 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, ?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; + { open DLS(n, nprev, mnext, m, cells, vals, l); - close DLS(n, nprev, mnext, m, cells, vals, l); - } else { + 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, 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 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, + listcells, + listvals, + list 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, + listcells, + listvals) = + 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 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 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 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 cells, + list 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 cells1, + list vals1, + struct xLIST_ITEM *n2, + struct xLIST_ITEM *nprev2, + struct xLIST_ITEM *mnext2, + struct xLIST_ITEM *m2, + list cells2, + list 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 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); - 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); + 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( + struct xLIST_ITEM *n, + struct xLIST_ITEM *m, + list 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 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); } -} -predicate xLIST( - struct xLIST *l, - int uxNumberOfItems, - struct xLIST_ITEM *pxIndex, - struct xLIST_ITEM *xListEnd, - listcells, - listvals) = - 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); - -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 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 split( + struct xLIST_ITEM *n, + struct xLIST_ITEM *nprev, + struct xLIST_ITEM *mnext, + struct xLIST_ITEM *m, + list cells, + list 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 dls_not_empty( - struct xLIST_ITEM *n, - struct xLIST_ITEM *m, - list 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 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); + lemma void join( + struct xLIST_ITEM *n1, + struct xLIST_ITEM *nprev1, + struct xLIST_ITEM *mnext1, + struct xLIST_ITEM *m1, + list cells1, + list vals1, + struct xLIST_ITEM *n2, + struct xLIST_ITEM *nprev2, + struct xLIST_ITEM *mnext2, + struct xLIST_ITEM *m2, + list cells2, + list 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); + } } - close DLS(n, nprev, mnext, m, cells, vals, l); -} - - -lemma void split( - struct xLIST_ITEM *n, - struct xLIST_ITEM *nprev, - struct xLIST_ITEM *mnext, - struct xLIST_ITEM *m, - list cells, - list 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 cells1, - list vals1, - struct xLIST_ITEM *n2, - struct xLIST_ITEM *nprev2, - struct xLIST_ITEM *mnext2, - struct xLIST_ITEM *m2, - list cells2, - list 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); - } -} -@*/ + @*/ +#endif /* VERIFAST_SINGLE_CORE */ #ifdef VERIFAST_TODO lemma void idx_remains_in_list( diff --git a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h index 5229895f2..48e9afb0f 100644 --- a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h +++ b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h @@ -359,6 +359,7 @@ ensures } @*/ +#ifdef IGNORE_DEPRECATED /* By verifying the following function, we can validate that the above lemmas * 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 ); } +#endif I/* GNORE_DEPRECATED */ @@ -429,6 +431,7 @@ predicate DLS_prefix( // prefix args list prefCells, list prefVals, + list prefOwners, struct xLIST_ITEM* item, struct xLIST_ITEM* itemPrev, // unsplit DLS args @@ -436,22 +439,26 @@ predicate DLS_prefix( struct xLIST_ITEM *endPrev, struct xLIST *pxContainer) = length(prefCells) == length(prefVals) &*& + length(prefOwners) == length(prefCells) &*& switch(prefCells) { case nil: return prefVals == nil &*& + prefOwners == nil &*& item == end &*& itemPrev == endPrev; case cons(headItem, tailCells): return item != end &*& // itemPrev != endPrev &*& // do we need to know this? headItem == end &*& - DLS(end, endPrev, item, itemPrev, prefCells, prefVals, pxContainer); + DLS(end, endPrev, item, itemPrev, prefCells, prefVals, prefOwners, + pxContainer); }; predicate DLS_suffix( // suffix args list sufCells, list sufVals, + list sufOwners, struct xLIST_ITEM* item, struct xLIST_ITEM* itemNext, // unsplit DLS args @@ -459,38 +466,43 @@ predicate DLS_suffix( struct xLIST_ITEM *endPrev, struct xLIST *pxContainer) = length(sufCells) == length(sufVals) &*& + length(sufOwners) == length(sufCells) &*& switch(sufCells) { case nil: return sufVals == nil &*& + sufOwners == nil &*& item == endPrev &*& itemNext == end; case cons(headItem, tailCells): return item != endPrev &*& mem(endPrev, sufCells) == true &*& 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) requires - DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& + DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*& mem(pxItem, gCells) == true &*& gEnd == head(gCells) &*& length(gCells) == length(gVals) &*& + length(gOwners) == length(gCells) &*& length(gCells) > 1; ensures - DLS_prefix(?gPrefCells, ?gPrefVals, pxItem, ?gItemPrev, + DLS_prefix(?gPrefCells, ?gPrefVals, ?gPrefOwners, pxItem, ?gItemPrev, 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)) &*& - // 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 mem(gItemNext, gCells) == true &*& @@ -502,25 +514,27 @@ ensures // pxItem is first/ left-most item in the list // -> empty prefix - open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); - assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, ?gItemPrev, gList) ); - assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, ?gSufCells, ?gSufVals, - gList) ); - close DLS_prefix(nil, nil, pxItem, gItemPrev, + open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList); + assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, ?gItemPrev, ?gOw, gList) ); + assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, + ?gSufCells, ?gSufVals, ?gSufOwners, gList) ); + close DLS_prefix(nil, nil, nil, pxItem, gItemPrev, gEnd, gEndPrev, gList); // 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 ); - close DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, gList); + close DLS(gItemNext, pxItem, gEnd, gEndPrev, + gSufCells, gSufVals, gSufOwners, gList); // Prove: `mem(gItemPrev, gCells) == true ` assert( gItemPrev == gEndPrev ); dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells); assert( mem(gItemPrev, gCells) == true ); - close DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, gEndPrev, - gList); + close DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); } else { // pxItem is not the first/ left-most item in the list // -> non-empty prefix @@ -529,13 +543,13 @@ ensures int gItemIndex = index_of(pxItem, gCells); split(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxItem, gItemIndex); - assert( DLS(gEnd, gEndPrev, pxItem, ?gItemPrev, ?gPrefCells, ?gPrefVals, - gList) ); + assert( DLS(gEnd, gEndPrev, pxItem, ?gItemPrev, + ?gPrefCells, ?gPrefVals, ?gPrefOwners, gList) ); // -> Will be wrapped inside the prefix constructed at the end of this // lemma. - assert( DLS(pxItem, gItemPrev, gEnd, gEndPrev, ?gPartCells, ?gPartVals, - gList) ); + assert( DLS(pxItem, gItemPrev, gEnd, gEndPrev, + ?gPartCells, ?gPartVals, ?gPartOwners, gList) ); // -> The tail of this DLS will make up the suffix constructed at the // end of this lemma. @@ -547,16 +561,16 @@ ensures // Prove: `head(gPrefCells) == gEnd` // Necessary to construct prefix later. // Implies `mem(gItemPrev, gCells) == true`. - open DLS(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, - gList); + open DLS(gEnd, gEndPrev, pxItem, gItemPrev, + gPrefCells, gPrefVals, gPrefOwners, gList); assert( head(gPrefCells) == gEnd ); - close DLS(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, - gList); + close DLS(gEnd, gEndPrev, pxItem, gItemPrev, + gPrefCells, gPrefVals, gPrefOwners, gList); assert( mem(gItemPrev, gCells) == true ); - open DLS(pxItem, gItemPrev, gEnd, gEndPrev, gPartCells, gPartVals, - gList); - assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, gList) ); + open DLS(pxItem, gItemPrev, gEnd, gEndPrev, + gPartCells, gPartVals, gPartOwners, gList); + assert( xLIST_ITEM(pxItem, ?gItemVal, ?gItemNext, gItemPrev, ?gOw, gList) ); if( pxItem == gEndPrev ) { // pxItem is the last/ right-most item in the list. @@ -572,69 +586,78 @@ ensures // 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( 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); - close DLS_suffix(nil, nil, pxItem, gItemNext, gEnd, gEndPrev, gList); } else { // pxItem is not the last/ right-most item in the list. // -> non-empty suffix - assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, ?gSufCells, ?gSufVals, - gList) ); + assert( DLS(gItemNext, pxItem, gEnd, gEndPrev, + ?gSufCells, ?gSufVals, ?gSufOwners, gList) ); assert( gSufCells == drop(1, gPartCells) ); // Prove: - `drop(gItemIndex+1, gCells) == gSufCells` // - `drop(gItemIndex+1, gVals) == gSufVals` + // - `drop(gItemIndex+1, gOwners) == gSufOwners` // -> Required to prove `mem(gItemNext, gCells) == true` and also to // prove relationship between gCells/gVals and their segmentation. assert( drop(1, drop(gItemIndex, gCells)) == gSufCells ); 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(gVals, 1, gItemIndex); + drop_n_plus_m(gOwners, 1, gItemIndex); assert( drop(gItemIndex+1, gCells) == gSufCells ); assert( drop(gItemIndex+1, gVals) == gSufVals ); + assert( drop(gItemIndex+1, gOwners) == gSufOwners ); // 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, gSufCells) == true ); mem_suffix_implies_mem(gItemNext, gCells, gItemIndex+1); assert( mem(gItemNext, gCells) == true ); - close DLS(gItemNext, pxItem, gEnd, gEndPrev, gSufCells, gSufVals, - gList); + close DLS(gItemNext, pxItem, gEnd, gEndPrev, + gSufCells, gSufVals, gSufOwners, gList); - close DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, - gEnd, gEndPrev, gList); + close DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, + pxItem, gItemPrev, gEnd, gEndPrev, gList); dls_last_mem(gItemNext, pxItem, gEnd, gEndPrev, gSufCells); - close DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, - gEndPrev, gList); + close DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); } } } lemma void DLS_close_2(struct xLIST_ITEM* pxItem, list gCells, - list gVals) + list gVals, + list gOwners) requires length(gCells) == length(gVals) &*& - DLS_prefix(?gPrefCells, ?gPrefVals, pxItem, ?gItemPrev, + DLS_prefix(?gPrefCells, ?gPrefVals, ?gPrefOwners, pxItem, ?gItemPrev, ?gEnd, ?gEndPrev, ?gList) &*& 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)) &*& - // 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 mem(gItemNext, gCells) == true &*& @@ -642,7 +665,7 @@ requires mem(gItemPrev, gCells) == true ; ensures - DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& + DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*& mem(pxItem, gCells) == true &*& mem(gItemNext, gCells) == true &*& mem(gItemPrev, gCells) == true &*& @@ -654,7 +677,7 @@ ensures // pxItem is first/ left-most item in the list // -> empty prefix - open DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, + open DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, pxItem, gItemPrev, gEnd, gEndPrev, gList); assert( pxItem == gEnd ); assert( gPrefVals == nil ); @@ -662,36 +685,39 @@ ensures if( gSufCells == nil ) { // pxItem is last/ right-most item in the list - open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, - gEndPrev, gList); + open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); assert( pxItem == gEndPrev ); assert( gSufVals == nil ); - close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); + close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, + gList); } else { // pxItem is not last/ right-most item in the list - open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, - gEndPrev, gList); - close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList); + open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); + close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, + gList); } } else { // pxItem is not the first/ left-most item in the list // -> non-empty prefix // (potentially empty suffix) - open DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev, + open DLS_prefix(gPrefCells, gPrefVals, gPrefOwners, pxItem, gItemPrev, gEnd, gEndPrev, gList); if( gSufCells == nil ) { // pxItem is the last/ right-most item in the list // -> empty suffix - open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, - gEndPrev, gList); + open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); assert( pxItem == 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, pxItem, gItemPrev, gEnd, gEndPrev, singleton(pxItem), singleton(gItemVal)); @@ -699,10 +725,11 @@ ensures // pxItem is not the last/ right-most item in the list // -> non-empty suffix - open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd, - gEndPrev, gList); + open DLS_suffix(gSufCells, gSufVals, gSufOwners, pxItem, gItemNext, + gEnd, gEndPrev, gList); close DLS(pxItem, gItemPrev, gEnd, gEndPrev, cons(pxItem, gSufCells), cons(gItemVal, gSufVals), + cons(gOw, gSufOwners), gList); join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals, pxItem, gItemPrev, gEnd, gEndPrev, @@ -714,14 +741,15 @@ ensures struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem) /*@ requires - DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& + DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*& mem(pxTaskItem, gCells) == true &*& gEnd == head(gCells) &*& length(gCells) == length(gVals) &*& + length(gOwners) == length(gCells) &*& length(gCells) > 1; @*/ /*@ ensures - DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& + DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*& mem(pxTaskItem, 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); /*@ 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; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; /*@ 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 //@ DLS_open_2(gTaskItem_1); /*@ 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; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; /*@ 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 ); @@ -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) /*@ requires - DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& + DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gOwners, ?gList) &*& mem(pxTaskItem, gCells) == true &*& gEnd == head(gCells) &*& length(gCells) == length(gVals) &*& + length(gOwners) == length(gCells) &*& length(gCells) > 1; @*/ /*@ ensures - DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& + DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gOwners, gList) &*& mem(pxTaskItem, 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); /*@ 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; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; /*@ 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 //@ DLS_open_2(gTaskItem_1); /*@ 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; //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; /*@ 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 ); diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h index b583cd7ce..6d824a368 100644 --- a/verification/verifast/proof/task_predicates.h +++ b/verification/verifast/proof/task_predicates.h @@ -12,9 +12,9 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) = malloc_block_tskTaskControlBlock(tcb) &*& tcb->pxTopOfStack |-> _ &*& - xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& + xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*& struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& - xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& + xLIST_ITEM(&tcb->xEventListItem, _, _, _, _, _) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& tcb->uxPriority |-> _ &*& @@ -59,9 +59,9 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) = stack_p_2(stackPtr, ?ulStackDepth, topPtr, ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*& - xLIST_ITEM(&tcb->xStateListItem, _, _, _, _) &*& + xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*& struct_xLIST_ITEM_padding(&tcb->xStateListItem) &*& - xLIST_ITEM(&tcb->xEventListItem, _, _, _, _) &*& + xLIST_ITEM(&tcb->xEventListItem, _, _, _, _, _) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& tcb->uxPriority |-> _ &*& diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index e949d161d..87bfba9af 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -92,7 +92,7 @@ predicate taskISRLockInv_p() = integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*& 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES &*& - readyLists_p(?gCellLists) + readyLists_p(?gCellLists, ?gOwnerLists) &*& // ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner) //foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner); @@ -117,6 +117,9 @@ ensures locked_p(otherLocks); // ∀items ∈ itemLists. ∀it ∈ items. sharedSeg_TCB_p(it->pvOwner) predicate collection_of_sharedSeg_TCB_p(list > itemLists) = + true; +@*/ +/* foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner); // Auxiliary prediactes to express nested quantification