diff --git a/include/list.h b/include/list.h index d1543dfed..332f3f413 100644 --- a/include/list.h +++ b/include/list.h @@ -56,35 +56,10 @@ #ifndef LIST_H #define LIST_H - -#ifdef VERIFAST - /* Reason for rewrite: - * VeriFast bug: - * Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H` - * evaluate to true. See minimal example `define_name`. - */ - #define INC_FREERTOS_H - /* Remember that this header is included indirectly `tasks.c` after it - * includes `FreeRTOS.h`. - */ - // TODO: Remove this work-around once VF has been fixed. -#endif /* VERIFAST */ - #ifndef INC_FREERTOS_H #error "FreeRTOS.h must be included before list.h" #endif -#ifdef VERIFAST - /* Reason for rewrite: - * VeriFast's normal and context-free preprocessor consume different - * numbers of tokens when expanding `PRIVILEGED_FUNCTION` in this file. - */ - #define PRIVILEGED_FUNCTION - // TODO: Figure out why the preprocessors consume different amounts of - // of tokens. This most likely has to do with the path/context - // from which this header is included. -#endif /* VERIFAST */ - /* * The list structure members are modified from within interrupts, and therefore * by rights should be declared volatile. However, they are only modified in a @@ -193,15 +168,7 @@ typedef struct xLIST listFIRST_LIST_INTEGRITY_CHECK_VALUE /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */ volatile UBaseType_t uxNumberOfItems; ListItem_t * configLIST_VOLATILE pxIndex; /*< Used to walk through the list. Points to the last item returned by a call to listGET_OWNER_OF_NEXT_ENTRY (). */ - #ifdef VERIFAST - /* Reason for rewrite: - * This change allows us to reuse the existing single-core list proofs, - * for which an identical rewrite for assumed. - */ - ListItem_t xListEnd; - #else - MiniListItem_t xListEnd; /*< List item that contains the maximum possible item value meaning it is always at the end of the list and is therefore used as a marker. */ - #endif /* VERIFAST */ + MiniListItem_t xListEnd; /*< List item that contains the maximum possible item value meaning it is always at the end of the list and is therefore used as a marker. */ listSECOND_LIST_INTEGRITY_CHECK_VALUE /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */ } List_t; @@ -323,7 +290,6 @@ typedef struct xLIST } - /* * Access function to obtain the owner of the first entry in a list. Lists * are normally sorted in ascending item value order. @@ -390,8 +356,6 @@ void vListInitialise( List_t * const pxList ) PRIVILEGED_FUNCTION; * \ingroup LinkedList */ void vListInitialiseItem( ListItem_t * const pxItem ) PRIVILEGED_FUNCTION; -//@ requires pxItem->pxContainer |-> _; -//@ ensures pxItem->pxContainer |-> 0; /* * Insert a list item into a list. The item will be inserted into the list in diff --git a/include/portable.h b/include/portable.h index d9bb2e720..6a3564547 100644 --- a/include/portable.h +++ b/include/portable.h @@ -128,8 +128,6 @@ StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, TaskFunction_t pxCode, void * pvParameters ) PRIVILEGED_FUNCTION; - ///@ requires true; - ///@ ensures true; #endif #endif /* if ( portUSING_MPU_WRAPPERS == 1 ) */ @@ -172,30 +170,11 @@ void vPortDefineHeapRegions( const HeapRegion_t * const pxHeapRegions ) PRIVILEG */ void vPortGetHeapStats( HeapStats_t * pxHeapStats ); -#ifdef VERIFAST - /* Reason for rewrite: - * VeriFast treats the `malloc` and `free` functions specially, - * in a particular built-in way that cannot be axiomatized within - * VeriFast's specification language. - * - * When `malloc( sizeof(struct S) )` is called for a user defined - * struct `S`, VeriFast instantiates the corresponding - * `malloc_block_S(...)` predicate as well as points-to chunks - * for its fields. - * Reversely, calling `free` cleans up all the predicates instantiated - * by `malloc`. - */ - #define pvPortMalloc malloc - #define vPortFree(ptr) free( (void*) ptr) -#else - /* - * Map to the memory management routines required for the port. - */ - void * pvPortMalloc( size_t xSize ) PRIVILEGED_FUNCTION; - void vPortFree( void * pv ) PRIVILEGED_FUNCTION; -#endif /* VERIFAST */ - - +/* + * Map to the memory management routines required for the port. + */ +void * pvPortMalloc( size_t xSize ) PRIVILEGED_FUNCTION; +void vPortFree( void * pv ) PRIVILEGED_FUNCTION; void vPortInitialiseBlocks( void ) PRIVILEGED_FUNCTION; size_t xPortGetFreeHeapSize( void ) PRIVILEGED_FUNCTION; size_t xPortGetMinimumEverFreeHeapSize( void ) PRIVILEGED_FUNCTION; diff --git a/include/stack_macros.h b/include/stack_macros.h index ea247e406..a80613712 100644 --- a/include/stack_macros.h +++ b/include/stack_macros.h @@ -84,92 +84,19 @@ #if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH < 0 ) ) - /* TODO: Convert this macro into a function such that we can insert proof annotations. - */ - #ifdef VERIFAST - /* Reason for rewrite: - * VeriFast complains about unspecified evaluation order of - * - `pxCurrentTCB->pxStack` - * - `vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName );` - * - */ - #define taskCHECK_FOR_STACK_OVERFLOW() VF__taskCHECK_FOR_STACK_OVERFLOW() - - void VF__taskCHECK_FOR_STACK_OVERFLOW() - /*@ requires prvSeg_TCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*& - coreLocalSeg_TCB_p(gCurrentTCB, ?uxCriticalNesting) &*& - // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` - interruptState_p(coreID_f(), ?state) &*& - interruptsDisabled_f(state) == true &*& - pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); - @*/ - /*@ ensures prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack) &*& - coreLocalSeg_TCB_p(gCurrentTCB, uxCriticalNesting) &*& - // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` - interruptState_p(coreID_f(), state) &*& - interruptsDisabled_f(state) == true &*& - pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); \ - @*/ \ - { \ - /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ - /*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, \ - ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \ - @*/ \ - /*@ open stack_p_2(_, _, _, _, _, _); @*/ \ - /* The detour below allows us to skip proving that `ulFreeBytes` \ - * is a multiple of `sizeof(StackType_t)`. \ - */ \ - /*@ integers__to_chars(pxTopOfStack+1); @*/ \ - /*@ chars_join((char*) pxStack); @*/ \ - /*@ chars_to_integers_(pxStack, sizeof(StackType_t), false, 4); @*/ \ - TCB_t* tcb0 = pxCurrentTCB; \ - const uint32_t * const pulStack = ( uint32_t * ) tcb0->pxStack; \ - const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; \ - \ - /*@ bool gOverflow = false; @*/ \ - if( ( pulStack[ 0 ] != ulCheckValue ) || \ - ( pulStack[ 1 ] != ulCheckValue ) || \ - ( pulStack[ 2 ] != ulCheckValue ) || \ - ( pulStack[ 3 ] != ulCheckValue ) ) \ - { \ - /*@ gOverflow = true; @*/ \ - /*@ integers__to_chars(pxStack); @*/ \ - /*@ chars_join((char*) pxStack); @*/ \ - /*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/ \ - /*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ - ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ - @*/ \ - /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ - TCB_t* tcb1 = pxCurrentTCB; \ - TCB_t* tcb2 = pxCurrentTCB; \ - vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName ); \ - } \ - /*@ \ - if(!gOverflow) { \ - integers__to_chars(pxStack); \ - chars_join((char*) pxStack); \ - chars_split((char*) pxStack, ulFreeBytesOnStack); \ - close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ - ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ - close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); \ - } \ - @*/ \ - } - #else - #define taskCHECK_FOR_STACK_OVERFLOW() \ - { \ - const uint32_t * const pulStack = ( uint32_t * ) pxCurrentTCB->pxStack; \ - const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; \ - \ - if( ( pulStack[ 0 ] != ulCheckValue ) || \ - ( pulStack[ 1 ] != ulCheckValue ) || \ - ( pulStack[ 2 ] != ulCheckValue ) || \ - ( pulStack[ 3 ] != ulCheckValue ) ) \ - { \ - vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \ - } \ - } - #endif /* VERIFAST */ + #define taskCHECK_FOR_STACK_OVERFLOW() \ + { \ + const uint32_t * const pulStack = ( uint32_t * ) pxCurrentTCB->pxStack; \ + const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; \ + \ + if( ( pulStack[ 0 ] != ulCheckValue ) || \ + ( pulStack[ 1 ] != ulCheckValue ) || \ + ( pulStack[ 2 ] != ulCheckValue ) || \ + ( pulStack[ 3 ] != ulCheckValue ) ) \ + { \ + vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \ + } \ + } #endif /* #if( configCHECK_FOR_STACK_OVERFLOW > 1 ) */ /*-----------------------------------------------------------*/ diff --git a/include/task.h b/include/task.h index 56e054299..65cd86e8d 100644 --- a/include/task.h +++ b/include/task.h @@ -28,37 +28,6 @@ #ifndef INC_TASK_H #define INC_TASK_H -#ifdef VERIFAST - /* Reason for rewrite: - * VeriFast bug: - * Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H` - * evaluate to true. See minimal example `define_name`. - */ - #define INC_FREERTOS_H - /* Remember that this header is included by `tasks.c` after it includes - * `FreeRTOS.h`. - */ - // TODO: Remove this work-around once VF has been fixed. -#endif /* VERIFAST */ - - -/* Remark: - * Note that the following VF section renders the previous one obsolete. - * However, we keep the above as a reminder until the corresponding bug - * has been fixed. - */ -#ifdef VERIFAST - /* Reason for rewrite: - * Even though in the current verification setup, `FreeRTOS.h` is always - * included before this file is processed, VeriFast does not consider this - * context when processing this file. VeriFast forbids macro expansions to - * depend on a potentially variable context, e.g, `configSTACK_DEPTH_TYPE` - * which expands to 'uint16_t' if and only if `FreeRTOS.h` has been - * included. - */ - #include "FreeRTOS.h" -#endif /* VERIFAST */ - #ifndef INC_FREERTOS_H #error "include FreeRTOS.h must appear in source files before include task.h" #endif @@ -1863,12 +1832,6 @@ configSTACK_DEPTH_TYPE uxTaskGetStackHighWaterMark2( TaskHandle_t xTask ) PRIVIL */ void vApplicationStackOverflowHook( TaskHandle_t xTask, char * pcTaskName ); - /*@ requires prvSeg_TCB_p(xTask, ?ulFreeBytesOnStack) &*& - coreLocalSeg_TCB_p(xTask, ?uxCriticalNesting); - @*/ - /*@ ensures prvSeg_TCB_p(xTask, ulFreeBytesOnStack) &*& - coreLocalSeg_TCB_p(xTask, uxCriticalNesting); - @*/ #endif diff --git a/list.c b/list.c index 5532d8e59..c679709f7 100644 --- a/list.c +++ b/list.c @@ -71,8 +71,6 @@ void vListInitialise( List_t * const pxList ) /*-----------------------------------------------------------*/ void vListInitialiseItem( ListItem_t * const pxItem ) -//@ requires pxItem->pxContainer |-> _; -//@ ensures pxItem->pxContainer |-> 0; { /* Make sure the list item is not recorded as being on a list. */ pxItem->pxContainer = NULL; @@ -86,423 +84,32 @@ void vListInitialiseItem( ListItem_t * const pxItem ) void vListInsertEnd( List_t * const pxList, ListItem_t * const pxNewListItem ) -#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. - */ - - // TODO: Adapt contract and proof to new version of predicates. +{ + ListItem_t * const pxIndex = pxList->pxIndex; - /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*& - xLIST_ITEM(pxNewListItem, ?val, _, _, ?ow, _) &*& - len < INT_MAX;@*/ - /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals, ?new_owners) &*& - idx == end - ? (new_cells == append(cells, singleton(pxNewListItem)) &*& - new_vals == append(vals, singleton(val)) &*& - new_owners == append(owners, singleton(ow))) - : (new_cells == append(take(index_of(idx, cells), cells), append(singleton(pxNewListItem), drop(index_of(idx, cells), cells))) &*& - new_vals == append(take(index_of(idx, cells), vals), append(singleton(val), drop(index_of(idx, cells), vals))) &*& - new_owners == append(take(index_of(idx, cells), owners), append(singleton(ow), drop(index_of(idx, cells), owners))));@*/ - { - /*@xLIST_star_item(pxList, pxNewListItem);@*/ - /*@assert mem(pxNewListItem, cells) == false;@*/ - /*@open xLIST(pxList, len, idx, end, cells, vals, owners);@*/ - #ifdef VERIFAST /*< const pointer declaration */ - ListItem_t * pxIndex = pxList->pxIndex; - #else - ListItem_t * const pxIndex = pxList->pxIndex; + /* Only effective when configASSERT() is also defined, these tests may catch + * the list data structures being overwritten in memory. They will not catch + * data errors caused by incorrect configuration or use of FreeRTOS. */ + listTEST_LIST_INTEGRITY( pxList ); + listTEST_LIST_ITEM_INTEGRITY( pxNewListItem ); - /* Only effective when configASSERT() is also defined, these tests may catch - * the list data structures being overwritten in memory. They will not catch - * data errors caused by incorrect configuration or use of FreeRTOS. */ - listTEST_LIST_INTEGRITY( pxList ); - listTEST_LIST_ITEM_INTEGRITY( pxNewListItem ); - #endif + /* Insert a new list item into pxList, but rather than sort the list, + * makes the new list item the last item to be removed by a call to + * listGET_OWNER_OF_NEXT_ENTRY(). */ + pxNewListItem->pxNext = pxIndex; + pxNewListItem->pxPrevious = pxIndex->pxPrevious; - /*@open xLIST_ITEM(pxNewListItem, _, _, _, _, _);@*/ - /*@assert DLS(end, ?endprev, end, _, cells, vals, owners, pxList);@*/ - /*@dls_first_mem(end, endprev, end, endprev, cells);@*/ - /*@dls_last_mem(end, endprev, end, endprev, cells);@*/ - /*@ - if (end == idx) - { - open DLS(end, endprev, end, endprev, cells, vals, owners, pxList); - open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, head(owners), pxList); - if (end == endprev) - { - // Case A (singleton): idx==end==endprev - } - else - { - assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), tail(owners), pxList); - if (endnext == endprev) - { - // Case B (two): idx==end and endnext==endprev - open DLS(endnext, end, end, endnext, _, _, _, _); - open xLIST_ITEM(endnext, _, _, _, _, _); - } - else - { - // Case C: idx==end and DLS:endnext...endprev - split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells))); - open DLS(endprev, _, _, _, _, _, _, _); - open xLIST_ITEM(endprev, _, _, _, _, _); - } - } - } - else - { - int i = index_of(idx, cells); - split(end, endprev, end, endprev, cells, vals, idx, i); - assert DLS(end, endprev, idx, ?idxprev, take(i, cells), take(i, vals), take(i, owners), pxList); - assert DLS(idx, idxprev, end, endprev, drop(i, cells), drop(i, vals), drop(i, owners), pxList); - open DLS(idx, idxprev, end, endprev, _, _, _, _); - open xLIST_ITEM(idx, _, _, _, _, _); - if (end == idxprev) - { - // Case D: end==idxprev and DLS:idx...endprev - take_take(1, i, vals); - take_head(vals); - open DLS(end, endprev, idx, idxprev, take(i, cells), take(i, vals), take(i, owners), pxList); - open xLIST_ITEM(end, portMAX_DELAY, _, _, _, _); - assert length(take(i, cells)) == 1; - } - else - { - // Case E: DLS:end...idxprev and DLS:idx...endprev - dls_last_mem(end, endprev, idx, idxprev, take(i, cells)); - split(end, endprev, idx, idxprev, take(i, cells), take(i, vals), idxprev, index_of(idxprev, take(i, cells))); - open DLS(idxprev, _, _, idxprev, _, _, _, _); - length_take(i, cells); - drop_take_singleton(i, vals); - drop_take_singleton(i, owners); - open xLIST_ITEM(idxprev, nth(i-1, vals), _, _, _, _); - } - } - @*/ + /* Only used during decision coverage testing. */ + mtCOVERAGE_TEST_DELAY(); - /* Insert a new list item into pxList, but rather than sort the list, - * makes the new list item the last item to be removed by a call to - * listGET_OWNER_OF_NEXT_ENTRY(). */ - pxNewListItem->pxNext = pxIndex; - pxNewListItem->pxPrevious = pxIndex->pxPrevious; + pxIndex->pxPrevious->pxNext = pxNewListItem; + pxIndex->pxPrevious = pxNewListItem; - /* Only used during decision coverage testing. */ - mtCOVERAGE_TEST_DELAY(); + /* Remember which list the item is in. */ + pxNewListItem->pxContainer = pxList; - pxIndex->pxPrevious->pxNext = pxNewListItem; - pxIndex->pxPrevious = pxNewListItem; - - /* Remember which list the item is in. */ - pxNewListItem->pxContainer = pxList; - - ( pxList->uxNumberOfItems )++; - - /*@ - if (end == idx) - { - close xLIST_ITEM(pxNewListItem, val, end, endprev, ow, pxList); - close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), singleton(ow), pxList); - close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, head(owners), pxList); - if (end == endprev) - { - // Case A (singleton): idx==end==endprev - close DLS(end, pxNewListItem, endnext, end, cells, vals, owners, pxList); - join(end, pxNewListItem, endnext, end, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)), append(owners, singleton(ow))); - } - else - { - close xLIST_ITEM(endprev, ?endprevval, pxNewListItem, ?endprevprev, ?endprevowner, _); - if (endnext == endprev) - { - // Case B (two): idx==end and endnext==endprev - close DLS(endprev, end, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), singleton(endprevowner), pxList); - close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, owners, pxList); - join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)), append(owners, singleton(ow))); - } - else - { - // Case C: idx==end and DLS:endnext...endprev - close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), singleton(endprevowner), pxList); - assert DLS(endnext, end, endprev, endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, _, pxList); - join(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev, vals_endnext_to_endprevprev, - endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval)); - close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, owners, pxList); - join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)), append(owners, singleton(ow))); - } - } - } - else - { - // Case D: end==idxprev and DLS:idx...endprev - // Case E: DLS:end...idxprev and DLS:idx...endprev - int i = index_of(idx, cells); - close xLIST_ITEM(pxNewListItem, val, idx, ?idxprev, ow, pxList); - close xLIST_ITEM(idx, ?idxval, ?idxnext, pxNewListItem, ?idxowner, pxList); - nth_drop2(vals, i); - assert idxval == nth(i, vals); - nth_drop2(owners, i); - assert idxowner == nth(i, owners); - close xLIST_ITEM(idxprev, ?idxprevval, pxNewListItem, ?idxprevprev, ?idxprevowner, pxList); - - if (end == idxprev) - { - close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), singleton(head(owners)), pxList); - } - else - { - length_take(i, cells); - take_take(i-1, i, vals); - take_singleton(i-1, vals); - take_singleton(i, vals); - take_take(i-1, i, owners); - take_singleton(i-1, owners); - take_singleton(i, owners); - assert DLS(end, endprev, idxprev, idxprevprev, ?cells_end_to_idxprevprev, take(i-1, vals), take(i-1, owners), pxList); - close DLS(idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval), singleton(idxprevowner), pxList); - join(end, endprev, idxprev, idxprevprev, cells_end_to_idxprevprev, take(i-1, vals), - idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval)); - } - - if (idx == endprev) - { - close DLS(idx, pxNewListItem, end, idx, singleton(idx), singleton(idxval), singleton(idxowner), pxList); - } - else - { - assert DLS(end, endprev, pxNewListItem, idxprev, ?cells_end_to_idxprev, ?vals_end_to_idxprev, _, pxList); - close DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), drop(i, owners), pxList); - } - - assert DLS(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), take(i, owners), pxList); - assert DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), drop(i, owners), pxList); - assert xLIST_ITEM(pxNewListItem, val, idx, idxprev, ow, pxList); - dls_star_item(idx, endprev, pxNewListItem); - close DLS(pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)), cons(ow, drop(i, owners)), pxList); - join(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), - pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals))); - assert DLS(end, endprev, end, endprev, ?cells_new, ?vals_new, ?owners_new, pxList); - assert cells_new == append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells))); - assert vals_new == append(take(i, vals) , append(singleton(val), drop(i, vals))); - assert owners_new == append(take(i, owners) , append(singleton(ow), drop(i, owners))); - head_append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells))); - take_take(1, i, cells); - head_append(take(i, vals), append(singleton(val), drop(i, vals))); - take_take(1, i, vals); - close xLIST(pxList, len+1, idx, end, cells_new, vals_new, owners_new); - } - @*/ - } -#else - /* The contract and proof below have been wirtten by Aalok Thakkar and Nathan - * Chong in 2020 for the single-core setup. - */ - /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*& - xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/ - /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*& - idx == end - ? (new_cells == append(cells, singleton(pxNewListItem)) &*& - new_vals == append(vals, singleton(val))) - : (new_cells == append(take(index_of(idx, cells), cells), append(singleton(pxNewListItem), drop(index_of(idx, cells), cells))) &*& - new_vals == append(take(index_of(idx, cells), vals), append(singleton(val), drop(index_of(idx, cells), vals))));@*/ - { - /*@xLIST_star_item(pxList, pxNewListItem);@*/ - /*@assert mem(pxNewListItem, cells) == false;@*/ - /*@open xLIST(pxList, len, idx, end, cells, vals);@*/ - #ifdef VERIFAST /*< const pointer declaration */ - ListItem_t * pxIndex = pxList->pxIndex; - #else - ListItem_t * const pxIndex = pxList->pxIndex; - - /* Only effective when configASSERT() is also defined, these tests may catch - * the list data structures being overwritten in memory. They will not catch - * data errors caused by incorrect configuration or use of FreeRTOS. */ - listTEST_LIST_INTEGRITY( pxList ); - listTEST_LIST_ITEM_INTEGRITY( pxNewListItem ); - #endif - - /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/ - /*@assert DLS(end, ?endprev, end, _, cells, vals, pxList);@*/ - /*@dls_first_mem(end, endprev, end, endprev, cells);@*/ - /*@dls_last_mem(end, endprev, end, endprev, cells);@*/ - /*@ - if (end == idx) - { - open DLS(end, endprev, end, endprev, cells, vals, pxList); - open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList); - if (end == endprev) - { - // Case A (singleton): idx==end==endprev - } - else - { - assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList); - if (endnext == endprev) - { - // Case B (two): idx==end and endnext==endprev - open DLS(endnext, end, end, endnext, _, _, _); - open xLIST_ITEM(endnext, _, _, _, _); - } - else - { - // Case C: idx==end and DLS:endnext...endprev - split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells))); - open DLS(endprev, _, _, _, _, _, _); - open xLIST_ITEM(endprev, _, _, _, _); - } - } - } - else - { - int i = index_of(idx, cells); - split(end, endprev, end, endprev, cells, vals, idx, i); - assert DLS(end, endprev, idx, ?idxprev, take(i, cells), take(i, vals), pxList); - assert DLS(idx, idxprev, end, endprev, drop(i, cells), drop(i, vals), pxList); - open DLS(idx, idxprev, end, endprev, _, _, _); - open xLIST_ITEM(idx, _, _, _, _); - if (end == idxprev) - { - // Case D: end==idxprev and DLS:idx...endprev - take_take(1, i, vals); - take_head(vals); - open DLS(end, endprev, idx, idxprev, take(i, cells), take(i, vals), pxList); - open xLIST_ITEM(end, portMAX_DELAY, _, _, _); - assert length(take(i, cells)) == 1; - } - else - { - // Case E: DLS:end...idxprev and DLS:idx...endprev - dls_last_mem(end, endprev, idx, idxprev, take(i, cells)); - split(end, endprev, idx, idxprev, take(i, cells), take(i, vals), idxprev, index_of(idxprev, take(i, cells))); - open DLS(idxprev, _, _, idxprev, _, _, _); - length_take(i, cells); - drop_take_singleton(i, vals); - open xLIST_ITEM(idxprev, nth(i-1, vals), _, _, _); - } - } - @*/ - - /* Insert a new list item into pxList, but rather than sort the list, - * makes the new list item the last item to be removed by a call to - * listGET_OWNER_OF_NEXT_ENTRY(). */ - pxNewListItem->pxNext = pxIndex; - pxNewListItem->pxPrevious = pxIndex->pxPrevious; - - /* Only used during decision coverage testing. */ - mtCOVERAGE_TEST_DELAY(); - - pxIndex->pxPrevious->pxNext = pxNewListItem; - pxIndex->pxPrevious = pxNewListItem; - - /* Remember which list the item is in. */ - pxNewListItem->pxContainer = pxList; - - ( pxList->uxNumberOfItems )++; - - /*@ - if (end == idx) - { - close xLIST_ITEM(pxNewListItem, val, end, endprev, pxList); - close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); - close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList); - if (end == endprev) - { - // Case A (singleton): idx==end==endprev - close DLS(end, pxNewListItem, endnext, end, cells, vals, pxList); - join(end, pxNewListItem, endnext, end, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - } - else - { - close xLIST_ITEM(endprev, ?endprevval, pxNewListItem, ?endprevprev, _); - if (endnext == endprev) - { - // Case B (two): idx==end and endnext==endprev - close DLS(endprev, end, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList); - close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList); - join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - } - else - { - // Case C: idx==end and DLS:endnext...endprev - close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList); - assert DLS(endnext, end, endprev, endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList); - join(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev, vals_endnext_to_endprevprev, - endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval)); - close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList); - join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, - pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - } - } - } - else - { - // Case D: end==idxprev and DLS:idx...endprev - // Case E: DLS:end...idxprev and DLS:idx...endprev - int i = index_of(idx, cells); - close xLIST_ITEM(pxNewListItem, val, idx, ?idxprev, pxList); - close xLIST_ITEM(idx, ?idxval, ?idxnext, pxNewListItem, pxList); - nth_drop2(vals, i); - assert idxval == nth(i, vals); - close xLIST_ITEM(idxprev, ?idxprevval, pxNewListItem, ?idxprevprev, pxList); - - if (end == idxprev) - { - close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList); - } - else - { - length_take(i, cells); - take_take(i-1, i, vals); - take_singleton(i-1, vals); - take_singleton(i, vals); - assert DLS(end, endprev, idxprev, idxprevprev, ?cells_end_to_idxprevprev, take(i-1, vals), pxList); - close DLS(idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval), pxList); - join(end, endprev, idxprev, idxprevprev, cells_end_to_idxprevprev, take(i-1, vals), - idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval)); - } - - if (idx == endprev) - { - close DLS(idx, pxNewListItem, end, idx, singleton(idx), singleton(idxval), pxList); - } - else - { - assert DLS(end, endprev, pxNewListItem, idxprev, ?cells_end_to_idxprev, ?vals_end_to_idxprev, pxList); - close DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList); - } - - assert DLS(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), pxList); - assert DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList); - assert xLIST_ITEM(pxNewListItem, val, idx, idxprev, pxList); - dls_star_item(idx, endprev, pxNewListItem); - close DLS(pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)), pxList); - join(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), - pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals))); - assert DLS(end, endprev, end, endprev, ?cells_new, ?vals_new, pxList); - assert cells_new == append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells))); - assert vals_new == append(take(i, vals) , append(singleton(val), drop(i, vals))); - head_append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells))); - take_take(1, i, cells); - head_append(take(i, vals), append(singleton(val), drop(i, vals))); - take_take(1, i, vals); - close xLIST(pxList, len+1, idx, end, cells_new, vals_new); - } - @*/ - } -#endif /* VERIFAST_SINGLE_CORE */ + ( pxList->uxNumberOfItems )++; +} /*-----------------------------------------------------------*/ void vListInsert( List_t * const pxList, @@ -577,154 +184,10 @@ 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; @@ -746,336 +209,5 @@ 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 8f14ca882..046aed9aa 100644 --- a/tasks.c +++ b/tasks.c @@ -24,26 +24,6 @@ * */ -#ifdef VERIFAST - /* Ghost header include must occur before any non-ghost includes or other - * non-ghost code. Otherwise VeriFast will report an unspecific parse error. - */ - - //@ #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_macro #include "FreeRTOSConfig.h" - - //VF_macro #define NULL 0 -#endif /* VERIFAST */ - - /* Standard includes. */ #include #include @@ -57,41 +37,7 @@ #include "FreeRTOS.h" #include "task.h" #include "timers.h" - -#ifndef VERIFAST - /* Reason for rewrite: - * The stack macros rely on macros defined later in this file, e.g., - * `pxCurrentTCB`. We need to delay this inclusion until the task macros - * have been defined. Otherwise, VeriFast will report unknown symbols when - * checking the stack macro proofs. - */ - #include "stack_macros.h" -#endif /* VERIFAST */ - -/* Verifast proof setup - * - * Note that redefinitions of macros must be included after - * original ones have been included. - */ -#ifdef VERIFAST - #include "verifast_proof_defs.h" - #include "stack_predicates.h" - #include "task_predicates.h" - #include "ready_list_predicates.h" - #include "verifast_RP2040_axioms.h" - #include "verifast_prelude_extended.h" - #include "verifast_bitops_extended.h" - #include "verifast_asm.h" - #include "verifast_port_contracts.h" - #include "verifast_lock_predicates.h" - #include "verifast_lists_extended.h" - #include "single_core_proofs/scp_list_predicates.h" - #include "single_core_proofs_extended/scp_list_predicates_extended.h" - - #include "snippets/rp2040_port_c_snippets.c" - - #include "list.c" -#endif +#include "stack_macros.h" /* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified * because the MPU ports require MPU_WRAPPERS_INCLUDED_FROM_API_FILE to be defined @@ -394,18 +340,6 @@ PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; /*< Poi PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */ PRIVILEGED_DATA static List_t xPendingReadyList; /*< Tasks that have been readied while the scheduler was suspended. They will be moved to the ready list when the scheduler is resumed. */ - -#ifdef VERIFAST - /* Reason for rewrite: - * The stack macros rely on some of the macros defined above, e.g., - * `pxCurrentTCB`. We need to delay this inclusion until the relevant task - * macros have been defined. Otherwise, VeriFast will report unknown symbols - * when checking the stack macro proofs. - */ - #include "stack_macros.h" -#endif /* VERIFAST */ - - #if ( INCLUDE_vTaskDelete == 1 ) PRIVILEGED_DATA static List_t xTasksWaitingTermination; /*< Tasks that have been deleted - but their memory not yet freed. */ @@ -663,31 +597,20 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) PRIVILEGED_FUNCTION; /*-----------------------------------------------------------*/ -#ifndef VERIFAST - /* Reason for rewrite: - * VeriFast cannot handle inline assembler and both `portDISABLE_INTERRUPTS` - * and `portRESTORE_INTERRUPTS` expand to inline assembler instructions. - */ - static BaseType_t prvGetCurrentYieldPending( void ) - { - BaseType_t xReturn; - UBaseType_t ulState; +static BaseType_t prvGetCurrentYieldPending( void ) +{ + BaseType_t xReturn; + UBaseType_t ulState; - ulState = portDISABLE_INTERRUPTS(); - xReturn = xYieldPendings[ portGET_CORE_ID() ]; - portRESTORE_INTERRUPTS( ulState ); + ulState = portDISABLE_INTERRUPTS(); + xReturn = xYieldPendings[ portGET_CORE_ID() ]; + portRESTORE_INTERRUPTS( ulState ); - return xReturn; - } -#endif /* VERIFAST */ + return xReturn; +} /*-----------------------------------------------------------*/ -#ifndef VERIFAST - /* Reason for rewrite: - * VeriFast cannot handle inline assembler and `portCHECK_IF_IN_ISR` - * expands to inline assembler. - */ static void prvCheckForRunStateChange( void ) { UBaseType_t uxPrevCriticalNesting; @@ -762,7 +685,6 @@ static void prvCheckForRunStateChange( void ) } } } -#endif /* VERIFAST */ /*-----------------------------------------------------------*/ @@ -898,46 +820,7 @@ static void prvYieldForTask( TCB_t * pxTCB, #if ( configUSE_PORT_OPTIMISED_TASK_SELECTION == 0 ) static BaseType_t prvSelectHighestPriorityTask( const BaseType_t xCoreID ) - /*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& - xCoreID == coreID_f() &*& - // interrupts are disabled and locks acquired - interruptState_p(xCoreID, ?state) &*& - interruptsDisabled_f(state) == true &*& - taskLockInv_p() &*& - isrLockInv_p() &*& - taskISRLockInv_p() - &*& - // opened predicate `coreLocalInterruptInv_p()` - [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB0) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) -// coreLocalSeg_TCB_p(gCurrentTCB0, 0) - &*& - // read access to current task's stack pointer, etc -// prvSeg_TCB_p(gCurrentTCB0, ?ulFreeBytesOnStack); - true; - @*/ - /*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& - xCoreID == coreID_f() &*& - // interrupts are disabled and locks acquired - interruptState_p(xCoreID, state) &*& - interruptsDisabled_f(state) == true &*& - taskLockInv_p() &*& - isrLockInv_p() &*& - taskISRLockInv_p() - &*& - // opened predicate `coreLocalInterruptInv_p()` - [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) -// coreLocalSeg_TCB_p(gCurrentTCB, 0) - &*& - // read access to current task's stack pointer, etc -// prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); - true; - @*/ { - //@ open taskISRLockInv_p(); - //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority0) ); - //@ assert( gTopReadyPriority0 == uxTopReadyPriority); UBaseType_t uxCurrentPriority = uxTopReadyPriority; BaseType_t xTaskScheduled = pdFALSE; BaseType_t xDecrementTopPriority = pdTRUE; @@ -948,31 +831,8 @@ static void prvYieldForTask( TCB_t * pxTCB, #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) BaseType_t xPriorityDropped = pdFALSE; #endif - //@ close _taskISRLockInv_p(gTopReadyPriority0); while( xTaskScheduled == pdFALSE ) - /*@ invariant - // requires clause - 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& - xCoreID == coreID_f() &*& - // interrupts are disabled and locks acquired - interruptState_p(xCoreID, state) &*& - interruptsDisabled_f(state) == true &*& - taskLockInv_p() &*& - isrLockInv_p() &*& - _taskISRLockInv_p(?gTopReadyPriority) - &*& - // opened predicate `coreLocalInterruptInv_p()` - [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) - &*& - // additional knowledge - (xTaskScheduled == 0 - ? (0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*& - gTopReadyPriority < configMAX_PRIORITIES - ) : true - ); - @*/ { #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) { @@ -986,150 +846,33 @@ static void prvYieldForTask( TCB_t * pxTCB, } #endif - //@ open _taskISRLockInv_p(gTopReadyPriority); - //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates0) ); - //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, gTopReadyPriority) ); - //@ assert( gTopReadyPriority == uxTopReadyPriority); - - //@ open readyLists_p(?gCellLists, ?gOwnerLists); - //@ assert( List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists, gOwnerLists) ); - //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); - //@ List_array_split(pxReadyTasksLists, uxCurrentPriority); - //@ assert( List_array_p(&pxReadyTasksLists, uxCurrentPriority, ?gPrefCellLists, ?gPrefOwnerLists) ); - /*@ assert( List_array_p(&pxReadyTasksLists + uxCurrentPriority + 1, - configMAX_PRIORITIES-uxCurrentPriority-1, ?gSufCellLists, ?gSufOwnerLists) ); - @*/ - //@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority]; - - //@ assert( xLIST(gReadyList, ?gSize, ?gIndex, ?gEnd, ?gCells, ?gVals, ?gOwners) ); - //@ assert( mem(gOwners, gOwnerLists) == true ); - - //@ open xLIST(gReadyList, _, _, _, _, _, _); - //@ assert( length(gCells) == gReadyList->uxNumberOfItems + 1 ); 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, gOwners, gReadyList) ); - @*/ - - - //@ DLS_open_2(pxReadyList->pxIndex); - //@ 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, gOwners); - //@ assert( mem(pxTaskItem, gCells) == true); - - //@ 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); if( ( void * ) pxLastTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) { - //@ assert( gVals == cons(?gV, ?gRest) ); - //@ assert( xLIST_ITEM(?gOldLastTaskItem, gV, ?gO, gEndPrev, _, gReadyList) ); pxLastTaskItem = pxLastTaskItem->pxPrevious; - //@ close xLIST_ITEM(gOldLastTaskItem, gV, gO, gEndPrev, _, gReadyList); } - //@ 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 */ xDecrementTopPriority = pdFALSE; - - //@ mem_nth(uxCurrentPriority, gCellLists); - //@ assert( mem(gCells, gCellLists) == true); - // Prove that `gTasks` contains all tasks in current ready - //@ forall_mem(gOwners, gOwnerLists, (superset)(gTasks)); - - //@ bool gInnerLoopBroken = false; do - /*@ invariant - 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& - xCoreID == coreID_f() &*& - pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& - mem(pxTaskItem, gCells) == true &*& - xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& - gSize > 0 &*& - exists_in_taskISRLockInv_p(gTasks, ?gStates) - &*& - // Read permissions for every task - foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) - &*& - // Write permission for task scheduled on this core - [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& - (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& - nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state - &*& - // Write permissions for unscheduled tasks - foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) - &*& - subset(gOwners, gTasks) == true &*& - List_array_p(&pxReadyTasksLists, uxCurrentPriority, gPrefCellLists, - gPrefOwnerLists) &*& - List_array_p(&pxReadyTasksLists + uxCurrentPriority + 1, - configMAX_PRIORITIES-uxCurrentPriority-1, gSufCellLists, - gSufOwnerLists) &*& - !gInnerLoopBroken; - - @*/ { TCB_t * pxTCB; - //@ 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. - //@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem; - - //@ DLS_open_2(gTaskItem_0); pxTaskItem = pxTaskItem->pxNext; - //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem; - - //@ close xLIST_ITEM(gTaskItem_0, _, _, _, _, gReadyList); - //@ DLS_close_2(gTaskItem_0, gCells, gVals, gOwners); if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) { - // Prove that `gTaskItem_1->pxNext != gEnd` - //@ dls_distinct(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells); - //@ open DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList); - //@ open DLS(?gTaskItem_1_next, _, gEnd, gEndPrev2, _, _, _, gReadyList); - //@ assert( gTaskItem_1_next != gEnd ); - /*@ close DLS(gTaskItem_1_next, _, gEnd, gEndPrev2, - tail(gCells), tail(gVals), tail(gOwners), _); - @*/ - pxTaskItem = pxTaskItem->pxNext; - //@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem; - - //@ close xLIST_ITEM(gTaskItem_1, _, _, _, _, gReadyList); - //@ close DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList); } - //@ struct xLIST_ITEM* gTaskItem_final = pxTaskItem; - //@ DLS_open_2(gTaskItem_final); pxTCB = pxTaskItem->pvOwner; - /*@ close xLIST_ITEM(gTaskItem_final, _, _, _, - pxTCB, gReadyList); - @*/ - //@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners); - - // Getting read access to fields of `pxTCB` - // aka first half of write permission - //@ assert( subset(gOwners, gTasks) == true ); - //@ mem_subset(pxTCB, gOwners, gTasks); - //@ foreach_remove(pxTCB, gTasks); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ @@ -1148,7 +891,6 @@ static void prvYieldForTask( TCB_t * pxTCB, } #endif /* if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) */ - //@ bool gPxTCB_not_running = (pxTCB->xTaskRunState == taskTASK_NOT_RUNNING); if( pxTCB->xTaskRunState == taskTASK_NOT_RUNNING ) { #if ( configNUM_CORES > 1 ) @@ -1157,82 +899,14 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif #endif { - //@ open exists_in_taskISRLockInv_p(gTasks, gStates); - //@ assert( nth(index_of(pxTCB, gTasks), gStates) == taskTASK_NOT_RUNNING); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - - /* We could reuse the read permission to `pxTCB` we extracted before the if statement. - * But putting permissions back as soon as we no longer need them simplifies the - * proof state and elimintates case-splits in the proof. - */ - - // Put read permission for `pxTCB` back - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); - //@ close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); - //@ foreach_unremove(pxTCB, gTasks); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - - // Get 2nd half of write permission for `gCurrentTCB` - //@ foreach_remove(gCurrentTCB, gTasks); - //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - /* If the task is not being executed by any core swap it in */ pxCurrentTCBs[ xCoreID ]->xTaskRunState = taskTASK_NOT_RUNNING; - //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - - // New states list reflects state update above. - //@ list gStates1 = def_state1(gTasks, gStates, gCurrentTCB, pxTCB); - //@ assert( nth(index_of(pxTCB, gTasks), gStates1) == taskTASK_NOT_RUNNING); - - /*@ close_updated_foreach_readOnly_sharedSeg_TCB(gCurrentTCB, gTasks, gStates, - gStates1, taskTASK_NOT_RUNNING); - @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - /*@ stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running - (gCurrentTCB, gTasks, gTasks, gStates, gStates1); - @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) ); - - - // Get write permission for `pxTCB` - //@ foreach_remove(pxTCB, gTasks); - //@ foreach_remove(pxTCB, gTasks); - //@ open readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)(pxTCB); - #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) pxPreviousTCB = pxCurrentTCBs[ xCoreID ]; #endif pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) ); - /*@ list gStates2 = - def_state2(gTasks, gStates, gCurrentTCB, pxTCB, xCoreID); - @*/ - - /*@ close_updated_foreach_readOnly_sharedSeg_TCB(pxTCB, gTasks, gStates1, - gStates2, xCoreID); - @*/ - /*@ startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running - (pxTCB, gTasks, gStates1, gStates2, xCoreID); - @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) ); - - pxCurrentTCBs[ xCoreID ] = pxTCB; xTaskScheduled = pdTRUE; - - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) ); - //@ close exists_in_taskISRLockInv_p(gTasks, gStates2); - - // Putting back first have of write permission to `pxTCB` - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); } } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) @@ -1244,137 +918,33 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif #endif { - //@ assert( pxTCB->xTaskRunState != taskTASK_NOT_RUNNING ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - //@ assert( nth(index_of(pxTCB, gTasks), gStates) != taskTASK_NOT_RUNNING); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - /* The task is already running on this core, mark it as scheduled */ pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; xTaskScheduled = pdTRUE; - - /*@ list gEquivStates - = update(index_of(pxTCB, gTasks), xCoreID, gStates); - @*/ - //@ open exists_in_taskISRLockInv_p(gTasks, gStates); - /*@ scheduleRunning_in_foreach_readOnly_sharedSeg_TCB_IF_not_running - (pxTCB, gTasks, gStates, gEquivStates, xCoreID); - @*/ - - //@ distinct_mem_remove(pxTCB, gTasks); - //@ remove_result_subset(pxTCB, gTasks); - /*@ update_foreach_readOnly_sharedSeg_TCB - (pxTCB, gTasks, remove(pxTCB, gTasks), - gStates, gEquivStates, xCoreID); - @*/ - - //@ close exists_in_taskISRLockInv_p(gTasks, gEquivStates); - - // Put read permission for `pxTCB` back - //@ foreach_unremove(pxTCB, gTasks); - - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gEquivStates)) ); - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); } } - /*@ - if( !gPxTCB_not_running && pxTCB != gCurrentTCB ) { - assert( exists_in_taskISRLockInv_p(gTasks, gStates) ); - // Put read permission for `pxTCB` back - close [1/2]sharedSeg_TCB_p(pxTCB, _); - close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); - foreach_unremove(pxTCB, gTasks); - } - @*/ - - //@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); if( xTaskScheduled != pdFALSE ) { - //@ close exists(gReadyList); - - //@ assert( xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) ); - /* Once a task has been selected to run on this core, * move it to the end of the ready task list. */ -#ifdef VERIFAST - /* Reasons for rewrite: - * - Linearization of subproof for performance reasons: - * The contracts of `uxListRemove` and `vListInserEnd` introduce case distinctions, i.e., - * branch splits in the proof tree. This increases the size of the proof tree exponentially - * and checking the proof with VeriFast takes very long. - * The contract of lemma `VF_reordeReadyList` does not expose these case distinctions. - * Hence, wrapping the function calls inside the lemma linearizes the subproof and - * improves the performance of VeriFast exponentially. - * - Reasoning about the function calls requires us introduce many temporary new facts - * about the cell and owner lists by calling list lemmas. Introducing such facts can - * easily lead to an infinite loop of auto lemmas calls. Encapsulating the subproof in a - * lemma allows us to ingore facts necessary for different parts of the proof. - * That is, makes it easier to ensure that we don't run into an infinite auto lemma call - * loop. - */ - /*@ close VF_reordeReadyList__ghost_args - (gTasks, gCellLists, gOwnerLists, uxCurrentPriority); - @*/ - VF_reordeReadyList( pxReadyList, pxTaskItem); -#else uxListRemove( pxTaskItem ); vListInsertEnd( pxReadyList, pxTaskItem ); -#endif /* VERIFAST */ - //@ assert( readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) ); - //@ assert( forall(gReorderedOwnerLists, (superset)(gTasks)) == true ); - //@ gInnerLoopBroken = true; break; } - - //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStatesEnd) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStatesEnd)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStatesEnd)) ); } while( pxTaskItem != pxLastTaskItem ); - - /* - If the loop above terminated via the break-branch, - * the heap already contains a `readyLists_p` predicate. - * - If the loop terminated normally, the heap matches - * the loop invariant (plus all chunks not touched by the - * loop). In this case, we still have to close the - * `readyLists_p` predicate. - */ - /*@ - if( !gInnerLoopBroken ) { - closeUnchanged_readyLists(gCellLists, gOwnerLists); - - assert( readyLists_p(gCellLists, gOwnerLists) ); - assert( forall(gOwnerLists, (superset)(gTasks)) == true ); - } - @*/ - - - //@ assert( readyLists_p(?gCellLists3, ?gOwnerLists3) ); - //@ assert( forall(gOwnerLists3, (superset)(gTasks)) == true ); } else { if( xDecrementTopPriority != pdFALSE ) { -#if VERIFAST - /* Reason for rewrite: Code not memory safe. - */ - if(uxTopReadyPriority > 0) { - uxTopReadyPriority--; - } -#else uxTopReadyPriority--; -#endif /* VERIFAST */ #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) { xPriorityDropped = pdTRUE; } #endif } - - //@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); - - //@ closeUnchanged_readyLists(gCellLists, gOwnerLists); } /* This function can get called by vTaskSuspend() before the scheduler is started. @@ -1382,61 +952,14 @@ static void prvYieldForTask( TCB_t * pxTCB, * won't find a new task to schedule. Return pdFALSE in this case. */ if( ( xSchedulerRunning == pdFALSE ) && ( uxCurrentPriority == tskIDLE_PRIORITY ) && ( xTaskScheduled == pdFALSE ) ) { - // @ assert( xLIST(gReadyList, ?gReadyListSize, _, _, gCells, gVals, gOwners) ); - // @ assert( gReadyListSize == gSize ); - // @ List_array_join(&pxReadyTasksLists); - // @ assert( List_array_p(&pxReadyTasksLists, ?gSize2, ?gCellLists2, ?gOwnerLists2) ); - // @ assert( gPrefCellLists == take(uxCurrentPriority, gCellLists) ); - // @ assert( gSufCellLists == drop(uxCurrentPriority + 1, gCellLists) ); - // @ assert( gCells == nth(uxCurrentPriority, gCellLists) ); - // @ assert( gCellLists2 == append(gPrefCellLists, cons(gCells, gSufCellLists)) ); - // @ append_take_nth_drop(uxCurrentPriority, gCellLists); - // @ append_take_nth_drop(uxCurrentPriority, gOwnerLists); - - // @ close readyLists_p(gCellLists2, gOwnerLists2); - //@ close taskISRLockInv_p(); return pdFALSE; } -#ifndef VERIFAST configASSERT( ( uxCurrentPriority > tskIDLE_PRIORITY ) || ( xTaskScheduled == pdTRUE ) ); -#endif /* VERIFAST */ - - -#if VERIFAST - /* Reason for rewrite: Code not memory safe. - */ - if(uxCurrentPriority > 0) { - uxCurrentPriority--; - } -#else uxCurrentPriority--; -#endif /* VERIFAST */ + } - // @ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); - // @ assert( xLIST(gReadyList, ?gReadyListSize, _, _, gCells, gVals, gOwners) ); - // @ assert( gReadyListSize == gSize ); - // @ List_array_join(&pxReadyTasksLists); - // @ assert( List_array_p(&pxReadyTasksLists, ?gSize2, ?gCellLists2, ?gOwnerLists2) ); - // @ assert( gPrefCellLists == take(uxCurrentPriority, gCellLists) ); - // @ assert( gSufCellLists == drop(uxCurrentPriority + 1, gCellLists) ); - // @ assert( gCells == nth(uxCurrentPriority, gCellLists) ); - // @ assert( gCellLists2 == append(gPrefCellLists, cons(gCells, gSufCellLists)) ); - // @ append_take_nth_drop(uxCurrentPriority, gCellLists); - // @ append_take_nth_drop(uxCurrentPriority, gOwnerLists); - - -// //@ assert( List_array_p(&pxReadyTasksLists, ?gSize2, ?gCellLists2, ?gOwnerLists2) ); - - - //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStates) ); - // //@ close readyLists_p(gCellLists2, gOwnerLists2); - //@ close _taskISRLockInv_p(uxTopReadyPriority); - } // outer loop end - -#ifndef VERIFAST configASSERT( taskTASK_IS_RUNNING( pxCurrentTCBs[ xCoreID ]->xTaskRunState ) ); -#endif /* VERIFAST */ #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) if( xPriorityDropped != pdFALSE ) @@ -1512,8 +1035,6 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif /* if ( configUSE_CORE_AFFINITY == 1 ) */ #endif /* if ( configNUM_CORES > 1 ) */ - //@ open _taskISRLockInv_p(_); - //@ close taskISRLockInv_p(); return pdTRUE; } @@ -1747,14 +1268,6 @@ static void prvYieldForTask( TCB_t * pxTCB, void * const pvParameters, UBaseType_t uxPriority, TaskHandle_t * const pxCreatedTask ) - /*@ requires usStackDepth * sizeof( StackType_t ) < UINTPTR_MAX &*& - usStackDepth > 18 &*& - // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16. - chars(pcName, 16, _) &*& - *pxCreatedTask |-> _ &*& - interruptState_p(?coreID, _); - @*/ - //@ ensures true; #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) { return xTaskCreateAffinitySet(pxTaskCode, pcName, usStackDepth, pvParameters, uxPriority, tskNO_AFFINITY, pxCreatedTask); @@ -1769,12 +1282,6 @@ static void prvYieldForTask( TCB_t * pxTCB, TaskHandle_t * const pxCreatedTask ) #endif /* ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) */ { - // Proof boken by switch to nightly build Nov 14, 2022 - // TODO: Adapt proof - //@ assume(false); - // ------------------------------------------------------------ - - TCB_t * pxNewTCB; BaseType_t xReturn; @@ -1816,14 +1323,9 @@ static void prvYieldForTask( TCB_t * pxTCB, pxNewTCB = ( TCB_t * ) pvPortMalloc( sizeof( TCB_t ) ); /*lint !e9087 !e9079 All values returned by pvPortMalloc() have at least the alignment required by the MCU's stack, and the first member of TCB_t is always a pointer to the task's stack. */ if( pxNewTCB != NULL ) - { + { /* Store the stack location in the TCB. */ pxNewTCB->pxStack = pxStack; - //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); - //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); - //@ chars__limits((char*) pxNewTCB->pxStack); - //@ assert( pxNewTCB->pxStack + (size_t) usStackDepth <= (StackType_t*) UINTPTR_MAX ); - //@ close uninit_TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); } else { @@ -1858,12 +1360,6 @@ static void prvYieldForTask( TCB_t * pxTCB, } #endif - /* TODO: Continue proof - * For now we stop verification here and concentrate on new - * verification target. - */ - //@ assume(false); - prvAddNewTaskToReadyList( pxNewTCB ); xReturn = pdPASS; } @@ -1872,9 +1368,6 @@ static void prvYieldForTask( TCB_t * pxTCB, xReturn = errCOULD_NOT_ALLOCATE_REQUIRED_MEMORY; } - //@ assume(false); - // TODO: Remove! - // Allows us to focus on verifying called functions. return xReturn; } @@ -1889,25 +1382,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, TaskHandle_t * const pxCreatedTask, TCB_t * pxNewTCB, const MemoryRegion_t * const xRegions ) -/*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*& - stackSize == ulStackDepth * sizeof(StackType_t) &*& - stackSize <= UINTPTR_MAX &*& - ulStackDepth > 18 &*& - // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16. - chars(pcName, 16, _) &*& - *pxCreatedTask |-> _; - @*/ -/*@ ensures TCB_p(pxNewTCB, ?freeBytes) &*& - chars(pcName, 16, _) &*& - *pxCreatedTask |-> _; - @*/ { - // Proof boken by switch to nightly build Nov 14, 2022 - // TODO: Adapt proof - //@ assume(false); - // ------------------------------------------------------------ - - StackType_t * pxTopOfStack; UBaseType_t x; @@ -1926,24 +1401,11 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, uxPriority &= ~portPRIVILEGE_BIT; #endif /* portUSING_MPU_WRAPPERS == 1 */ - - //@ open uninit_TCB_p(_,_); - /* Avoid dependency on memset() if it is not required. */ #if ( tskSET_NEW_STACKS_TO_KNOWN_VALUE == 1 ) { /* Fill the stack with a known value to assist debugging. */ - #ifdef VERIFAST - /* Reason for rewrite: - * - VeriFast reports type mismatch because - * `( int ) tskSTACK_FILL_BYTE` is passed for a char argument. - * - * TODO: Is the type mismatch a real error? - */ - ( void ) memset( pxNewTCB->pxStack, ( char ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) ); - #else - ( void ) memset( pxNewTCB->pxStack, ( int ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) ); - #endif + ( void ) memset( pxNewTCB->pxStack, ( int ) tskSTACK_FILL_BYTE, ( size_t ) ulStackDepth * sizeof( StackType_t ) ); } #endif /* tskSET_NEW_STACKS_TO_KNOWN_VALUE */ @@ -1954,97 +1416,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, #if ( portSTACK_GROWTH < 0 ) { pxTopOfStack = &( pxNewTCB->pxStack[ ulStackDepth - ( uint32_t ) 1 ] ); - //@ StackType_t* gOldTop = pxTopOfStack; - //@ char* gcStack = (char*) pxNewTCB->pxStack; - - /* Set the following flag to skip and expensive part of this proof: - * `VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT` - * - * For VeriFast bit vector proofs are very computation intensive. - * Hence, reasoning about the stack alignment below takes relatively - * long. - */ - #ifndef VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT - // Axiomatize that pointers on RP2040 are 32bit - //@ ptr_range(pxTopOfStack); - - /* Convert top and mask to VeriFast bitvectors and establish - * relation to C variables. - * Note that on RP2040: - * - `portPOINTER_SIZE_TYPE` == `uint32_t` - * - `portBYTE_ALIGNMENT_MASK` == `0x0007` - */ - //@ uint32_t gMask = 0x0007; - //@ Z gzTop = Z_of_uint32((int) pxTopOfStack); - //@ Z gzMask = Z_of_uint32((int) gMask); - //@ bitnot_def(gMask, gzMask); - //@ bitand_def((int) pxTopOfStack, gzTop, ~gMask, Z_not(gzMask)); - #else - /* Axiomatise that no over- or underflow occurs. - * We further assume that `portPOINTER_SIZE_TYPE` evaluates to - * `uint32_t`. - */ - //@ ptr_range(pxTopOfStack); - /*@ assume( ( StackType_t * ) ( ( ( uint32_t ) pxTopOfStack ) - & ( ~( ( uint32_t ) ( 0x0007 ) ) ) ) - > 0 ); - @*/ - /*@ assume( ( StackType_t * ) ( ( ( uint32_t ) pxTopOfStack ) - & ( ~( ( uint32_t ) ( 0x0007 ) ) ) ) - <= (StackType_t*) UINTPTR_MAX ); - @*/ - #endif /* VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT */ - pxTopOfStack = ( StackType_t * ) ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack ) & ( ~( ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception. Avoiding casts between pointers and integers is not practical. Size differences accounted for using portPOINTER_SIZE_TYPE type. Checked by assert(). */ - - #ifndef VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT - //@ uint32_t gUnalignedBytes = (char*) gOldTop - (char*) pxTopOfStack; - - // The following alignment assertions hold but take very long to verify. - ///@ assert( pxTopOfStack <= gOldTop ); - ///@ assert( gOldTop - 7 <= pxTopOfStack ); - - // Same as above but for aligned top pointer: - //@ Z gzAlignedTop = Z_of_uint32((int) pxTopOfStack); - //@ bitand_def((int) pxTopOfStack, gzAlignedTop, gMask, gzMask); - #else - /* Axiomatize that alignmet check succeeds. - * We further assume that `portPOINTER_SIZE_TYPE` evaluates to - * `uint32_t`*/ - //@ ptr_range(pxTopOfStack); - /*@ assume( ( ( uint32_t ) pxTopOfStack & ( uint32_t ) ( 0x0007 ) ) == 0UL ); - @*/ - #endif /* VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT */ /* Check the alignment of the calculated top of stack is correct. */ - configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) ); - - #ifndef VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT - /* Remark: Moving this proof step in front of the above - * assertion increases proof checking time by a lot. - */ - /*@ - if( pxTopOfStack < gOldTop ) - { - chars_split_at(gcStack, (char*) pxTopOfStack + sizeof(StackType_t)); - } - @*/ - #else - /* Axiomatize that bit vector operations did not change stack - * pointer. - */ - /* TODO: Can we simplify the axiomatizations here and above - * by assuming that the top pointer was already aligned? - */ - //@ assume( pxTopOfStack == gOldTop ); - //@ int gUnalignedBytes = 0; - #endif /* VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT */ - - //@ assert( chars(gcStack, ?gFreeBytes, _) ); - //@ char* gUnalignedPtr = (char*) pxNewTCB->pxStack + gFreeBytes; - //@ close unalignedRestOfStack_p(gUnalignedPtr, gUnalignedBytes); - //@ close stack_p_2(pxNewTCB->pxStack, ulStackDepth, pxTopOfStack, gFreeBytes, 0, gUnalignedBytes); - + configASSERT( ( ( ( portPOINTER_SIZE_TYPE ) pxTopOfStack & ( portPOINTER_SIZE_TYPE ) portBYTE_ALIGNMENT_MASK ) == 0UL ) ); #if ( configRECORD_STACK_HIGH_ADDRESS == 1 ) { @@ -2071,9 +1446,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, if( pcName != NULL ) { for( x = ( UBaseType_t ) 0; x < ( UBaseType_t ) configMAX_TASK_NAME_LEN; x++ ) - /*@ invariant chars_(pxNewTCB->pcTaskName, 16, _) &*& - chars(pcName, 16, _); - @*/ { pxNewTCB->pcTaskName[ x ] = pcName[ x ]; @@ -2123,7 +1495,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, vListInitialiseItem( &( pxNewTCB->xStateListItem ) ); vListInitialiseItem( &( pxNewTCB->xEventListItem ) ); - /* Set the pxNewTCB as a link back from the ListItem_t. This is so we can get * back to the containing TCB from a generic item in a list. */ listSET_LIST_ITEM_OWNER( &( pxNewTCB->xStateListItem ), pxNewTCB ); @@ -2132,10 +1503,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, listSET_LIST_ITEM_VALUE( &( pxNewTCB->xEventListItem ), ( TickType_t ) configMAX_PRIORITIES - ( TickType_t ) uxPriority ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ listSET_LIST_ITEM_OWNER( &( pxNewTCB->xEventListItem ), pxNewTCB ); - // Closing predicates early simplifies the symbolic heap and proof debugging. - //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); - //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); - #if ( portCRITICAL_NESTING_IN_TCB == 1 ) { pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U; @@ -2167,24 +1534,14 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, #if ( configNUM_THREAD_LOCAL_STORAGE_POINTERS != 0 ) { - //@ pointers__to_chars_(pxNewTCB->pvThreadLocalStoragePointers); - //@ assert(chars_((char*) pxNewTCB->pvThreadLocalStoragePointers, _, _)); - //@ assert(chars_(_, sizeof( pxNewTCB->pvThreadLocalStoragePointers ), _)); memset( ( void * ) &( pxNewTCB->pvThreadLocalStoragePointers[ 0 ] ), 0x00, sizeof( pxNewTCB->pvThreadLocalStoragePointers ) ); } #endif #if ( configUSE_TASK_NOTIFICATIONS == 1 ) { - ///@ assert( integers__(pxNewTCB->ulNotifiedValue, _, _, 1, _) ); - ///@ integers___to_integers_(pxNewTCB->ulNotifiedValue); - ///@ integers__to_chars(pxNewTCB->ulNotifiedValue); - //@integers___to_integers_(pxNewTCB->ulNotifiedValue); - //@ integers__to_chars(pxNewTCB->ulNotifiedValue); memset( ( void * ) &( pxNewTCB->ulNotifiedValue[ 0 ] ), 0x00, sizeof( pxNewTCB->ulNotifiedValue ) ); - //@ uchars__to_chars_(pxNewTCB->ucNotifyState); memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) ); - //@ chars_to_uchars(pxNewTCB->ucNotifyState); } #endif @@ -2199,12 +1556,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, #if ( INCLUDE_xTaskAbortDelay == 1 ) { - #ifdef VERIFAST - /* Reason for rewrite: Assignment not type safe. */ - pxNewTCB->ucDelayAborted = pd_U_FALSE; - #else - pxNewTCB->ucDelayAborted = pdFALSE; - #endif + pxNewTCB->ucDelayAborted = pdFALSE; } #endif @@ -2303,18 +1655,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode, { mtCOVERAGE_TEST_MARKER(); } - - //@ assert( stack_p_2(_, _, _, ?gFreeBytes, _, _) ); - //@ close TCB_p(pxNewTCB, gFreeBytes); } /*-----------------------------------------------------------*/ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) -/*//@ requires interruptState_p(?coreID, _) &*& - unprotectedGlobalVars(); - @*/ -/*//@ ensures true; - @*/ { /* Ensure interrupts don't access the task lists while the lists are being * updated. */ @@ -2631,18 +1975,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) eTaskState eTaskGetState( TaskHandle_t xTask ) { eTaskState eReturn; - #ifdef VERIFAST - /* Reason for rewrite: - * VeriFast does not support multiple pointer declarations to - * user-defined types in single statement (i.e., `A p1, p2;` is ok, - * `A *p1, *p2;` fails) - */ - List_t const * pxStateList; - List_t const * pxDelayedList; - List_t const * pxOverflowedDelayedList; - #else - List_t const * pxStateList, * pxDelayedList, * pxOverflowedDelayedList; - #endif /* VERIFAST */ + List_t const * pxStateList, * pxDelayedList, * pxOverflowedDelayedList; const TCB_t * const pxTCB = xTask; configASSERT( pxTCB ); @@ -3884,18 +3217,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char static TCB_t * prvSearchForNameWithinSingleList( List_t * pxList, const char pcNameToQuery[] ) { - #ifdef VERIFAST - /* Reason for rewrite: - * VeriFast does not support multiple pointer declarations to - * user-defined types in single statement - * (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails) - */ - TCB_t * pxNextTCB; - TCB_t * pxFirstTCB; - TCB_t * pxReturn = NULL; - #else TCB_t * pxNextTCB, * pxFirstTCB, * pxReturn = NULL; - #endif /* VERIFAST */ UBaseType_t x; char cNextChar; BaseType_t xBreakLoop; @@ -4551,40 +3873,6 @@ BaseType_t xTaskIncrementTick( void ) /*-----------------------------------------------------------*/ void vTaskSwitchContext( BaseType_t xCoreID ) -/*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& - xCoreID == coreID_f() - &*& - // access to locks and disabled interrupts - locked_p(nil) &*& - [?f_ISR]isrLock_p() &*& - [?f_task]taskLock_p() &*& - interruptState_p(xCoreID, ?state) &*& - interruptsDisabled_f(state) == true - &*& - // opened predicate `coreLocalInterruptInv_p()` - pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& - coreLocalSeg_TCB_p(gCurrentTCB, 0) - &*& - // read access to current task's stack pointer, etc - prvSeg_TCB_p(gCurrentTCB, ?ulFreeBytesOnStack); - -@*/ -/*@ ensures // all locks are released and interrupts remain disabled - locked_p(nil) &*& - [f_ISR]isrLock_p() &*& - [f_task]taskLock_p() &*& - interruptState_p(xCoreID, state) - &*& - // opened predicate `coreLocalInterruptInv_p()` - pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& - coreLocalSeg_TCB_p(gCurrentTCB, 0) - &*& - // read access to current task's stack pointer, etc - prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); - // Remark: the part of the post condition relating to TCBs will have to change. -@*/ { /* Acquire both locks: * - The ISR lock protects the ready list from simultaneous access by @@ -4596,38 +3884,16 @@ void vTaskSwitchContext( BaseType_t xCoreID ) portGET_TASK_LOCK(); /* Must always acquire the task lock first */ portGET_ISR_LOCK(); - //@ produce_taskISRLockInv(); { /* vTaskSwitchContext() must never be called from within a critical section. * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */ - #ifdef VERIFAST - /* Reason for rewrite: VeriFast cannot handle non-pure assertions. */ - { - // PROBLEM: - // Line - // UBaseType_t nesting = pxCurrentTCB->uxCriticalNesting; - // leads to VF error - // "This potentially side-effecting expression is not supported in this position, because of C's unspecified evaluation order" - // - // TODO: Inspect reason. - TaskHandle_t currentHandle = pxCurrentTCB; - //@ assert( currentHandle == gCurrentTCB ); - //@ open coreLocalSeg_TCB_p(gCurrentTCB, 0); - UBaseType_t nesting = currentHandle->uxCriticalNesting; - configASSERT( nesting == 0 ); - //@ close coreLocalSeg_TCB_p(gCurrentTCB, 0); - } - #else - configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); - #endif /* VERIFAST */ + configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); - //@ open taskISRLockInv_p(); if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE ) { /* The scheduler is currently suspended - do not allow a context * switch. */ xYieldPendings[ xCoreID ] = pdTRUE; - //@ close taskISRLockInv_p(); } else { @@ -4674,7 +3940,6 @@ void vTaskSwitchContext( BaseType_t xCoreID ) /* Select a new task to run using either the generic C or port * optimised asm code. */ - //@ close taskISRLockInv_p(); ( void ) prvSelectHighestPriorityTask( xCoreID ); traceTASK_SWITCHED_IN(); @@ -4699,7 +3964,6 @@ void vTaskSwitchContext( BaseType_t xCoreID ) #endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */ } } - //@ consume_taskISRLockInv(); portRELEASE_ISR_LOCK(); portRELEASE_TASK_LOCK(); } @@ -5531,17 +4795,7 @@ static void prvCheckTasksWaitingTermination( void ) List_t * pxList, eTaskState eState ) { - #ifdef VERIFAST - /* Reason for rewrite: - * VeriFast does not support multiple pointer declarations to - * user-defined types in single statement - * (i.e., `A p1, p2;` is ok, `A *p1, *p2;` fails) - */ - configLIST_VOLATILE TCB_t * pxNextTCB; - configLIST_VOLATILE TCB_t * pxFirstTCB; - #else - configLIST_VOLATILE TCB_t * pxNextTCB, * pxFirstTCB; - #endif /* VERIFAST */ + configLIST_VOLATILE TCB_t * pxNextTCB, * pxFirstTCB; UBaseType_t uxTask = 0; if( listCURRENT_LIST_LENGTH( pxList ) > ( UBaseType_t ) 0 ) @@ -5740,13 +4994,6 @@ static void prvResetNextTaskUnblockTime( void ) #if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) ) TaskHandle_t xTaskGetCurrentTaskHandle( void ) - /*@ requires interruptState_p(coreID_f(), ?state) &*& - pointer(&pxCurrentTCBs[coreID_f], ?taskHandle); - @*/ - /*@ ensures interruptState_p(coreID_f(), state) &*& - pointer(&pxCurrentTCBs[coreID_f], taskHandle) &*& - result == taskHandle; - @*/ { TaskHandle_t xReturn; uint32_t ulState; @@ -6102,11 +5349,8 @@ void vTaskYieldWithinAPI( void ) #if ( portCRITICAL_NESTING_IN_TCB == 1 ) void vTaskEnterCritical( void ) - ///@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars(); - ///@ ensures false; { portDISABLE_INTERRUPTS(); - //@ open unprotectedGlobalVars(); if( xSchedulerRunning != pdFALSE ) { @@ -7192,4 +6436,4 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait, } #endif -#endif /* if ( configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H == 1 ) */ \ No newline at end of file +#endif /* if ( configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H == 1 ) */