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

Added lemma DLS_end_next_close to help closing DLS opened with DLS_end_next_open

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-23 08:31:07 -05:00
parent 5e2f51caa8
commit 9e3ea9016e
2 changed files with 78 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -14,7 +14,7 @@ requires
&*& &*&
pxItem == gEnd; pxItem == gEnd;
ensures ensures
xLIST_ITEM(gEnd, ?gItemVal, ?gItem_next, gEndPrev, pxList) &*& xLIST_ITEM(gEnd, head(gVals), ?gItem_next, gEndPrev, pxList) &*&
DLS(gItem_next, gEnd, gEnd, gEndPrev, drop(1, gCells), drop(1, gVals), pxList ) &*& DLS(gItem_next, gEnd, gEnd, gEndPrev, drop(1, gCells), drop(1, gVals), pxList ) &*&
mem(gItem_next, gCells) == true; mem(gItem_next, gCells) == true;
{ {
@ -43,6 +43,28 @@ ensures
} }
lemma void DLS_end_next_close(struct xLIST* pxList, struct xLIST_ITEM* pxItem)
requires
xLIST_ITEM(?gEnd, ?gItemVal, ?gItem_next, ?gEndPrev, pxList) &*&
DLS(gItem_next, gEnd, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*&
// mem(gItem_next, gCells) == true &*&
length(gCells) == length(gVals) &*&
length(gCells) > 0 &*&
pxItem == gEnd;
ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev,
cons(gEnd, gCells), cons(gItemVal, gVals), pxList);
{
open DLS(gItem_next, gEnd, gEnd, gEndPrev, gCells, gVals, pxList);
close DLS(gItem_next, gEnd, gEnd, gEndPrev, gCells, gVals, pxList);
dls_star_item(gItem_next, gEndPrev, gEnd);
dls_distinct(gItem_next, gEnd, gEnd, gEndPrev, gCells);
dls_last_mem(gItem_next, gEnd, gEnd, gEndPrev, gCells);
close DLS(gEnd, gEndPrev, gEnd, gEndPrev,
cons(gEnd, gCells), cons(gItemVal, gVals), pxList);
}
lemma void DLS_nonEndItem_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem) lemma void DLS_nonEndItem_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem)
requires requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*&
@ -59,7 +81,8 @@ ensures // DLS prefix
pxList) pxList)
&*& &*&
// item of interest // item of interest
xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) xLIST_ITEM(pxItem, nth(index_of(pxItem, gCells), gVals),
?pxItem_next, pxItem_prev, pxList)
&*& &*&
// DLS suffix // DLS suffix
(pxItem != gEndPrev (pxItem != gEndPrev
@ -91,6 +114,9 @@ ensures // DLS prefix
drop(pxItemIndex_0, gCells), drop(pxItemIndex_0, gVals), drop(pxItemIndex_0, gCells), drop(pxItemIndex_0, gVals),
pxList); pxList);
assert( xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) ); assert( xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) );
assert( gItemVal == head(drop(pxItemIndex_0, gVals)) );
head_drop_n_equals_nths(gVals, pxItemIndex_0);
assert( gItemVal == nth(index_of(pxItem, gCells), gVals) );
// open DLS and xLIST_ITEM predicates to prove // open DLS and xLIST_ITEM predicates to prove
@ -143,25 +169,24 @@ ensures // DLS prefix
*/ */
void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem)
/*@ requires /*@ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?pxList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
gEnd == head(gCells) &*& gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
length(gCells) > 1; length(gCells) > 1;
@*/ @*/
/*@ ensures /*@ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*&
mem(pxTaskItem, gCells) == true; mem(pxTaskItem, gCells) == true;
@*/ @*/
{ {
//@ int pxItemIndex_0 = index_of(pxTaskItem, gCells); //@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem;
//@ struct xLIST_ITEM* pxItem = pxTaskItem;
/*@ /*@
if( pxItem == gEnd ) { if( gTaskItem_0 == gEnd ) {
DLS_end_next_open(pxList, pxItem); DLS_end_next_open(gList, gTaskItem_0);
} else { } else {
DLS_nonEndItem_next_open(pxList, pxItem); DLS_nonEndItem_next_open(gList, gTaskItem_0);
} }
@*/ @*/
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
@ -170,10 +195,26 @@ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem)
//@ assert( mem(pxItem_1, gCells) == true ); //@ assert( mem(pxItem_1, gCells) == true );
//@ close xLIST_ITEM(gTaskItem_0, ?gTaskItemVal, _, _, gList);
/*@
if( gTaskItem_0 == gEnd ) {
DLS_end_next_close(gList, gTaskItem_0);
assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, ?gCells2, ?gVals2, gList) );
// why is this necessary?
assert( gCells == cons( _, _) );
assert( gVals == cons(_, _) );
// ignore post condition until closing lemmas are finished // gVals2 == cons (|(intbox) | (|(int) | (head gVals)
//@ assume(false); assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, _, gList) );
assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) );
} else {
assume(false);
//DLS_nonEndItem_next_close(gList, gTaskItem_0);
}
@*/
;;
} }

26
verification/verifast/proof/verifast_lists_extended.h
View file

@ -12,4 +12,30 @@ requires mem(x, drop(i, xs)) == true;
ensures mem(x, xs) == true; ensures mem(x, xs) == true;
@*/ @*/
// TODO: prove
/*@
lemma void head_drop_n_equals_nths<t>(list<t> xs, int n)
requires n >= 0;
ensures head(drop(n, xs)) == nth(n, xs);
{
// Will prove later. For now, we only validate with an example.
list<int> _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil)))))));
int _n = 4;
list<int> dn = drop(_n, _xs);
int hdn = head(dn);
int nthn = nth(_n, _xs);
assert( hdn == head(drop(_n, _xs)) );
assert( nthn == nth(_n, _xs ));
assert( head(drop(_n, _xs)) == nth(_n, _xs) );
// ADMIT LEMMA, PROVE LATER
assume(false);
}
@*/
#endif /* VERIFAST_LISTS_EXTENDED_H */ #endif /* VERIFAST_LISTS_EXTENDED_H */