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

Reverted modified source and header files to last commit before we started the VeriFast proofs.

Browse source 
Files reset to commit 13f034eb74
This commit is contained in:
Tobias Reinhard 2022-12-09 10:37:50 -05:00
parent dcbaf3863b
commit 1d3fcdfc1f
6 changed files with 59 additions and 1850 deletions
Download patch file Download diff file Expand all files Collapse all files

38
include/list.h
View file

@ -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

31
include/portable.h
View file

@ -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;

99
include/stack_macros.h
View file

@ -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 ) */
/*-----------------------------------------------------------*/

37
include/task.h
View file

@ -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

910
list.c
View file

@ -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<struct xLIST * >(?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<struct xLIST_ITEM *> ys = take(i, cells);@*/
/*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
/*@list<TickType_t> vs = take(i, vals);@*/
/*@list<TickType_t> ws = drop(i, vals);@*/
/*@list<void*> ts = take(i, owners);@*/
/*@list<void*> 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<struct xLIST * >(?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<struct xLIST_ITEM *> ys = take(i, cells);@*/
/*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
/*@list<TickType_t> vs = take(i, vals);@*/
/*@list<TickType_t> 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 */
/*-----------------------------------------------------------*/

794
tasks.c
View file

File diff suppressed because it is too large Load diff