From cd3fa4e577b8adfd77484eba86f9552d236a05e3 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 1 Dec 2022 11:47:52 -0500 Subject: [PATCH] Added adaptation of Aalok's and Nathan's single-core proof for `uxListRemove` --- list.c | 477 +++++++++++++++++- tasks.c | 7 +- .../proof/single_core_proofs/scp_common.h | 5 +- .../single_core_proofs/scp_list_predicates.h | 2 +- 4 files changed, 484 insertions(+), 7 deletions(-) diff --git a/list.c b/list.c index c97b8cc8a..91ac6dea7 100644 --- a/list.c +++ b/list.c @@ -186,10 +186,154 @@ void vListInsert( List_t * const pxList, /*-----------------------------------------------------------*/ UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove ) -{ +#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. + */ + + /*@requires + exists(?l) &*& + xLIST(l, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*& + end != pxItemToRemove &*& + mem(pxItemToRemove, cells) == true;@*/ + /*@ensures + result == len-1 &*& + xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, nth(index_of(pxItemToRemove, cells), owners), NULL) &*& + pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*& + xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx, end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals), remove_nth(index_of(pxItemToRemove, cells), owners)); + @*/ + { + /* For brevity we alias x to pxItemToRemove */ + /*@struct xLIST_ITEM *x = pxItemToRemove;@*/ + + /* Start by establishing that the list must be non-empty since x != end */ + /*@open xLIST(l, len, idx, end, cells, vals, owners);@*/ + /*@assert DLS(end, ?endprev, end, _, cells, vals, owners, l);@*/ + /*@assert vals == cons(portMAX_DELAY, _);@*/ + /*@dls_not_empty(end, endprev, cells, x);@*/ + + /* We know the xLIST is a DLS: end...endprev + Split this into DLS1:end...xprev and DLS2:x...endprev */ + /*@int i = index_of(x, cells);@*/ + /*@split(end, endprev, end, endprev, cells, vals, x, i);@*/ + /*@list ys = take(i, cells);@*/ + /*@list zs = drop(i, cells);@*/ + /*@list vs = take(i, vals);@*/ + /*@list ws = drop(i, vals);@*/ + /*@list ts = take(i, owners);@*/ + /*@list us = drop(i, owners);@*/ + /*@assert length(ys) == length(vs);@*/ + /*@assert length(zs) == length(ws);@*/ + /*@assert length(ts) == length(vs);@*/ + /*@assert length(us) == length(ws);@*/ + /*@assert DLS(end, endprev, x, ?xprev, ys, vs, ts, l);@*/ /*< DLS1 (ys, vs) */ + /*@assert DLS(x, xprev, end, endprev, zs, ws, us, l);@*/ /*< DLS2 (zs, ws) */ + + /* Now case split to open DLS1 and DLS2 appropriately */ + /*@ + if (end == xprev) + { + if (x == endprev) + { + //Case A + //DLS1: extract end=prev=next + open DLS(end, endprev, x, xprev, ys, vs, ts, l); + assert owners == cons(_, _); + open xLIST_ITEM(end, portMAX_DELAY, x, endprev, head(owners), l); + //DLS2: extract x + open DLS(x, xprev, end, endprev, zs, ws, us, l); + //Lengths + assert length(ys) == 1; + assert length(zs) == 1; + assert length(us) == 1; + } + else + { + //Case B + //DLS1: extract end=prev + open DLS(end, endprev, x, xprev, ys, vs, ts, l); + open xLIST_ITEM(end, portMAX_DELAY, x, endprev, head(owners), l); + //DLS2: extract next and x + open DLS(x, end, end, endprev, zs, ws, us, l); + assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l); + open DLS(xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l); + open xLIST_ITEM(xnext, _, _, x, _, l); + //Lengths + assert length(ys) == 1; + } + } + else + { + if (x == endprev) + { + //Case C + //DLS1: extract end=next and prev + dls_last_mem(end, endprev, x, xprev, ys); + assert mem(xprev, ys) == true; + open DLS(end, endprev, x, xprev, ys, vs, ts, l); + open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, head(ts), l); + if (endnext == xprev) + { + open DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l); + open xLIST_ITEM(xprev, _, x, _, _, l); + } + else + { + assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l); + int k = index_of(xprev, tail(ys)); + dls_last_mem(endnext, end, x, xprev, tail(ys)); + split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k); + open DLS(xprev, _, x, xprev, _, _, _, l); + open xLIST_ITEM(xprev, _, x, _, _, l); + } + //DLS2: extract x + open DLS(x, xprev, end, endprev, zs, ws, us, l); + //Lengths + assert length(zs) == 1; + } + else + { + //Case D + //DLS1: extract prev + dls_last_mem(end, endprev, x, xprev, ys); + int j = index_of(xprev, ys); + open DLS(end, endprev, x, xprev, ys, vs, ts, l); + open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, head(ts), l); + if (endnext == xprev) + { + open DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l); + assert tail(ys) == singleton(xprev); + open xLIST_ITEM(xprev, _, x, _, _, l); + } + else + { + assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l); + int k = index_of(xprev, tail(ys)); + dls_last_mem(endnext, end, x, xprev, tail(ys)); + split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k); + open DLS(xprev, _, x, xprev, _, _, _, l); + open xLIST_ITEM(xprev, _, x, _, _, l); + } + //DLS2: extract next and x + open DLS(x, xprev, end, endprev, zs, ws, us, l); + assert xLIST_ITEM(x, _, ?xnext, _, _, l); + open DLS(xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l); + open xLIST_ITEM(xnext, _, _, x, _, l); + } + } + @*/ + /*@drop_nth_index_of(vals, i);@*/ + /*@drop_nth_index_of(owners, i);@*/ + /*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, nth(i, owners), l);@*/ + /* The list item knows which list it is in. Obtain the list from the list * item. */ +#ifdef VERIFAST /*< const pointer declaration */ + List_t * pxList = pxItemToRemove->pxContainer; +#else List_t * const pxList = pxItemToRemove->pxContainer; +#endif pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious; pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext; @@ -211,5 +355,336 @@ UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove ) ( pxList->uxNumberOfItems )--; return pxList->uxNumberOfItems; + + /*@ + // Reassemble DLS1 and a modified DLS2, which no longer includes x + if (end == xprev) + { + if (x == endprev) + { + //Case A + close xLIST_ITEM(end, portMAX_DELAY, _, _, _, _); + close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), singleton(head(owners)), l); + } + else + { + //Case B + close xLIST_ITEM(xprev, _, xnext, endprev, head(owners), l); + close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), singleton(head(owners)), l); + close xLIST_ITEM(xnext, _, _, xprev, _, l); + close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), tail(us), l); + join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + } + else + { + if (x == endprev) + { + //Case C + close xLIST_ITEM(end, _, ?endnext, xprev, head(ts), l); + close xLIST_ITEM(xprev, ?xprev_val, end, _, ?xprev_owner, l); + if (endnext == xprev) + { + close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l); + close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), cons(head(ts), singleton(xprev_owner)), l); + } + else + { + close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l); + assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, _, l); + join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev, + xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val)); + close DLS(end, xprev, end, xprev, ys, vs, ts, l); + } + } + else + { + //Case D + close xLIST_ITEM(xnext, _, ?xnextnext, xprev, ?xnext_owner, l); + close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), tail(us), l); + close xLIST_ITEM(end, _, ?endnext, endprev, head(ts), l); + close xLIST_ITEM(xprev, ?xprev_val, xnext, _, ?xprev_owner, l); + if (endnext == xprev) + { + close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l); + close DLS(end, endprev, xnext, xprev, ys, vs, ts, l); + join(end, endprev, xnext, xprev, ys, vs, + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + else + { + close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l); + assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, _, l); + join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev, + xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val)); + close DLS(end, endprev, xnext, xprev, ys, vs, ts, l); + join(end, endprev, xnext, xprev, ys, vs, + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + } + } + @*/ + /*@remove_remove_nth(cells, x);@*/ + /*@ + if (idx == x) + { + close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)), append(ts, tail(us))); + } + else + { + idx_remains_in_list(cells, idx, x, i); + close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)), append(ts, tail(us))); + } + @*/ + /*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, nth(i, owners), NULL);@*/ } +#else + // Contract and proof written by Aalok Thakkar and Nathan Chong for the + // single-core setup in 2020. + + /*@requires + exists(?l) &*& + xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*& + end != pxItemToRemove &*& + mem(pxItemToRemove, cells) == true;@*/ + /*@ensures + result == len-1 &*& + xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, NULL) &*& + pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*& + xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx, end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals));@*/ + { + /* For brevity we alias x to pxItemToRemove */ + /*@struct xLIST_ITEM *x = pxItemToRemove;@*/ + + /* Start by establishing that the list must be non-empty since x != end */ + /*@open xLIST(l, len, idx, end, cells, vals);@*/ + /*@assert DLS(end, ?endprev, end, _, cells, vals, l);@*/ + /*@assert vals == cons(portMAX_DELAY, _);@*/ + /*@dls_not_empty(end, endprev, cells, x);@*/ + + /* We know the xLIST is a DLS: end...endprev + Split this into DLS1:end...xprev and DLS2:x...endprev */ + /*@int i = index_of(x, cells);@*/ + /*@split(end, endprev, end, endprev, cells, vals, x, i);@*/ + /*@list ys = take(i, cells);@*/ + /*@list zs = drop(i, cells);@*/ + /*@list vs = take(i, vals);@*/ + /*@list ws = drop(i, vals);@*/ + /*@assert length(ys) == length(vs);@*/ + /*@assert length(zs) == length(ws);@*/ + /*@assert DLS(end, endprev, x, ?xprev, ys, vs, l);@*/ /*< DLS1 (ys, vs) */ + /*@assert DLS(x, xprev, end, endprev, zs, ws, l);@*/ /*< DLS2 (zs, ws) */ + + /* Now case split to open DLS1 and DLS2 appropriately */ + /*@ + if (end == xprev) + { + if (x == endprev) + { + //Case A + //DLS1: extract end=prev=next + open DLS(end, endprev, x, xprev, ys, vs, l); + open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l); + //DLS2: extract x + open DLS(x, xprev, end, endprev, zs, ws, l); + //Lengths + assert length(ys) == 1; + assert length(zs) == 1; + } + else + { + //Case B + //DLS1: extract end=prev + open DLS(end, endprev, x, xprev, ys, vs, l); + open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l); + //DLS2: extract next and x + open DLS(x, end, end, endprev, zs, ws, l); + assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), l); + open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l); + open xLIST_ITEM(xnext, _, _, x, l); + //Lengths + assert length(ys) == 1; + } + } + else + { + if (x == endprev) + { + //Case C + //DLS1: extract end=next and prev + dls_last_mem(end, endprev, x, xprev, ys); + assert mem(xprev, ys) == true; + open DLS(end, endprev, x, xprev, ys, vs, l); + open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l); + if (endnext == xprev) + { + open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l); + open xLIST_ITEM(xprev, _, x, _, l); + } + else + { + assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l); + int k = index_of(xprev, tail(ys)); + dls_last_mem(endnext, end, x, xprev, tail(ys)); + split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k); + open DLS(xprev, _, x, xprev, _, _, l); + open xLIST_ITEM(xprev, _, x, _, l); + } + //DLS2: extract x + open DLS(x, xprev, end, endprev, zs, ws, l); + //Lengths + assert length(zs) == 1; + } + else + { + //Case D + //DLS1: extract prev + dls_last_mem(end, endprev, x, xprev, ys); + int j = index_of(xprev, ys); + open DLS(end, endprev, x, xprev, ys, vs, l); + open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l); + if (endnext == xprev) + { + open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l); + assert tail(ys) == singleton(xprev); + open xLIST_ITEM(xprev, _, x, _, l); + } + else + { + assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l); + int k = index_of(xprev, tail(ys)); + dls_last_mem(endnext, end, x, xprev, tail(ys)); + split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k); + open DLS(xprev, _, x, xprev, _, _, l); + open xLIST_ITEM(xprev, _, x, _, l); + } + //DLS2: extract next and x + open DLS(x, xprev, end, endprev, zs, ws, l); + assert xLIST_ITEM(x, _, ?xnext, _, l); + open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l); + open xLIST_ITEM(xnext, _, _, x, l); + } + } + @*/ + /*@drop_nth_index_of(vals, i);@*/ + /*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, l);@*/ + + /* The list item knows which list it is in. Obtain the list from the list + * item. */ + #ifdef VERIFAST /*< const pointer declaration */ + List_t * pxList = pxItemToRemove->pxContainer; + #else + List_t * const pxList = pxItemToRemove->pxContainer; + #endif + + pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious; + pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext; + + /* Only used during decision coverage testing. */ + mtCOVERAGE_TEST_DELAY(); + + /* Make sure the index is left pointing to a valid item. */ + if( pxList->pxIndex == pxItemToRemove ) + { + pxList->pxIndex = pxItemToRemove->pxPrevious; + } + else + { + mtCOVERAGE_TEST_MARKER(); + } + + pxItemToRemove->pxContainer = NULL; + ( pxList->uxNumberOfItems )--; + + return pxList->uxNumberOfItems; + + /*@ + // Reassemble DLS1 and a modified DLS2, which no longer includes x + if (end == xprev) + { + if (x == endprev) + { + //Case A + close xLIST_ITEM(end, portMAX_DELAY, _, _, _); + close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), l); + } + else + { + //Case B + close xLIST_ITEM(xprev, _, xnext, endprev, l); + close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), l); + close xLIST_ITEM(xnext, _, _, xprev, l); + close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l); + join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + } + else + { + if (x == endprev) + { + //Case C + close xLIST_ITEM(end, _, ?endnext, xprev, l); + close xLIST_ITEM(xprev, ?xprev_val, end, _, l); + if (endnext == xprev) + { + close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), l); + close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), l); + } + else + { + close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l); + assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l); + join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev, + xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val)); + close DLS(end, xprev, end, xprev, ys, vs, l); + } + } + else + { + //Case D + close xLIST_ITEM(xnext, _, ?xnextnext, xprev, l); + close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l); + close xLIST_ITEM(end, _, ?endnext, endprev, l); + close xLIST_ITEM(xprev, ?xprev_val, xnext, _, l); + if (endnext == xprev) + { + close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), l); + close DLS(end, endprev, xnext, xprev, ys, vs, l); + join(end, endprev, xnext, xprev, ys, vs, + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + else + { + close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l); + assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l); + join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev, + xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val)); + close DLS(end, endprev, xnext, xprev, ys, vs, l); + join(end, endprev, xnext, xprev, ys, vs, + xnext, xprev, end, endprev, tail(zs), tail(ws)); + } + } + } + @*/ + /*@remove_remove_nth(cells, x);@*/ + /*@ + if (idx == x) + { + close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws))); + } + else + { + idx_remains_in_list(cells, idx, x, i); + close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws))); + } + @*/ + /*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, NULL);@*/ + } + + + +#endif /* VERIFAST_SINGLE_CORE */ + /*-----------------------------------------------------------*/ diff --git a/tasks.c b/tasks.c index 553e4d9e4..0e6a02de0 100644 --- a/tasks.c +++ b/tasks.c @@ -31,13 +31,14 @@ //@ #include //@ #include "list.gh" + //@ #include /* The following includes will be visible to VeriFast in the preprocessed * code. VeriFast requires includes to occur befor definitions. Hence, * all includes visible to VeriFast must occur before the preprocessed * ones. */ - //VF_include #include "FreeRTOSConfig.h" + //VF_macro #include "FreeRTOSConfig.h" //VF_macro #define NULL 0 #endif /* VERIFAST */ @@ -1217,8 +1218,12 @@ static void prvYieldForTask( TCB_t * pxTCB, } } + //@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); + if( xTaskScheduled != pdFALSE ) { + //@ close exists(gReadyList); + /* Once a task has been selected to run on this core, * move it to the end of the ready task list. */ uxListRemove( pxTaskItem ); diff --git a/verification/verifast/proof/single_core_proofs/scp_common.h b/verification/verifast/proof/single_core_proofs/scp_common.h index a1ade6f14..1c3f72ec9 100644 --- a/verification/verifast/proof/single_core_proofs/scp_common.h +++ b/verification/verifast/proof/single_core_proofs/scp_common.h @@ -60,9 +60,6 @@ fixpoint list singleton(t x) { return cons(x, nil); } -@*/ -#ifdef VERIFAST_TODO - lemma void note(bool b) requires b; ensures b; @@ -630,6 +627,6 @@ lemma void combine_list_update(listprefix, t x, listsuffix, int i, list } @*/ -#endif /* VERIFAST_TODO */ + #endif /* SCP_COMMON_H */ 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 9b8ac49df..57c3c7fbf 100644 --- a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h +++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h @@ -683,7 +683,7 @@ @*/ #endif /* VERIFAST_SINGLE_CORE */ -#ifdef VERIFAST_TODO +/*@ lemma void idx_remains_in_list( list cells, t idx,