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

Added ready list lemmas.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-29 08:32:32 -05:00
parent 2048fb85da
commit b310efa029
1 changed files with 63 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

97
verification/verifast/proof/ready_list_predicates.h
View file

@ -4,43 +4,72 @@
#include "single_core_proofs/scp_list_predicates.h" #include "single_core_proofs/scp_list_predicates.h"
/*@ /*@
predicate List_array_p(List_t* array, int size) = predicate List_array_p(List_t* array, int size,
list<list<struct xLIST_ITEM*> > cellLists) =
size >= 0 &*& size >= 0 &*&
length(cellLists) == size &*&
size > 0 size > 0
? ( ? (
cellLists == cons(?gCells, ?gTailcellLists) &*&
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
xLIST(array, xLIST(array, ?gNumberOfItems, ?gIndex, ?gListEnd, gCells, ?gVals)
?uxNumberOfItems,
?pxIndex,
?xListEnd,
?cells,
?vals)
&*& &*&
List_array_p(array + 1, size - 1) List_array_p(array + 1, size - 1, gTailcellLists)
) )
: true; : cellLists == nil;
lemma void List_array_get_l(List_t* array, int index) lemma void List_array_size_positive(List_t* pxArray)
requires List_array_p(array, ?size) &*& requires List_array_p(pxArray, ?gSize, ?gCellLists);
0 <= index &*& index < size; ensures List_array_p(pxArray, gSize, gCellLists) &*&
ensures List_array_p(array, index) &*& gSize >= 0 &*& gSize == length(gCellLists);
pointer_within_limits(array) == true &*&
xLIST(array + index,
?uxNumberOfItems,
?pxIndex,
?xListEnd,
?cells,
?vals) &*&
List_array_p(array + index + 1, size-index-1);
{ {
if( index == 0) { open List_array_p(pxArray, gSize, gCellLists);
open List_array_p(array, size); close List_array_p(pxArray, gSize, gCellLists);
close List_array_p(array, 0); }
} else {
open List_array_p(array, size); lemma void List_array_split(List_t* array, int index)
List_array_get_l(array + 1, index - 1); requires
close List_array_p(array, index); List_array_p(array, ?gSize, ?gCellLists) &*&
0 <= index &*& index < gSize;
ensures
List_array_p(array, index, ?gPrefCellLists) &*&
gPrefCellLists == take(index, gCellLists) &*&
pointer_within_limits(array) == true &*&
xLIST(array + index, _, _, _, ?gCells, ?vals) &*&
gCells == nth(index, gCellLists) &*&
List_array_p(array + index + 1, gSize-index-1, ?gSufCellLists) &*&
gSufCellLists == drop(index+1, gCellLists);
{
open List_array_p(array, gSize, gCellLists);
if( index > 0 ) {
List_array_split(array + 1, index - 1);
} }
close List_array_p(array, index, take(index, gCellLists));
}
lemma void List_array_join(List_t* array)
requires
List_array_p(array, ?gPrefSize, ?gPrefCellLists) &*&
xLIST(array + gPrefSize, _, _, _, ?gCells, _) &*&
pointer_within_limits(array + gPrefSize) == true &*&
List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists);
ensures
List_array_p(array, ?gSize, ?gCellLists) &*&
gSize == length(gCellLists) &*&
gSize == gPrefSize + 1 + gSufSize &*&
gCellLists == append(gPrefCellLists, cons(gCells, gSufCellLists));
{
open List_array_p(array, gPrefSize, gPrefCellLists);
List_array_size_positive(array + gPrefSize + 1);
if( gPrefSize > 0 ) {
List_array_join(array + 1);
}
close List_array_p(array, gPrefSize + 1 + gSufSize,
append(gPrefCellLists, cons(gCells, gSufCellLists)));
} }
@*/ @*/
@ -49,22 +78,22 @@ ensures List_array_p(array, index) &*&
// TODO: We know that the list of priority 0 is never empty. // TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else. // It contains the idle task and nothing else.
predicate readyLists_p() = predicate readyLists_p() =
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES); List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, ?gCellLists);
@*/ @*/
/*@ /*@
lemma void List_array_p_index_within_limits(List_t* array, int index) lemma void List_array_p_index_within_limits(List_t* array, int index)
requires List_array_p(array, ?size) &*& requires List_array_p(array, ?gSize, ?gCellListss) &*&
0 <= index &*& index < size; 0 <= index &*& index < gSize;
ensures List_array_p(array, size) &*& ensures List_array_p(array, gSize, gCellListss) &*&
pointer_within_limits(&array[index]) == true; pointer_within_limits(&array[index]) == true;
{ {
open List_array_p(array, size); open List_array_p(array, gSize, gCellListss);
if( index > 0) { if( index > 0) {
List_array_p_index_within_limits(&array[1], index-1); List_array_p_index_within_limits(&array[1], index-1);
} }
close List_array_p(array, size); close List_array_p(array, gSize, gCellListss);
} }
@*/ @*/