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

Handled minor TODOs in proof headers.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-28 10:36:17 -05:00
parent 75111c247c
commit f15540cecc
7 changed files with 6 additions and 76 deletions
Download patch file Download diff file Expand all files Collapse all files

3
Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/vf_rewrite.sh
View file

@ -39,9 +39,8 @@ echo "Delete fixed-sized array typedefs"
rewrite "typedef .*\[[0-9]*\];" ""
echo "Delete attributes"
#rewrite "\_\_attribute\_\_\(\(\_\_[a-z\_]*\_\_\)\)" ""
rewrite "__attribute__(([_a-z]*))" ""
# TODO: Why does matching `\s` or `:space:` not work on MacOs?
# Note: `\s` or `:space:` not work on MacOs.
rewrite "__attribute__( ( [_a-z]* ) )" ""
echo "Delete void casts (used to suppress compiler warnings)"

3
Test/VeriFast/tasks/vTaskSwitchContext/include/list.h
View file

@ -80,9 +80,6 @@
* 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 */
/*

2
Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
View file

@ -84,8 +84,6 @@
#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

3
Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h
View file

@ -3,9 +3,6 @@
// We want our proofs to hold for an arbitrary number of cores.
/* TODO: Can we use the original function `get_core_num` instead without
* adding the contract inside the pico sdk file (platform.h)?
*/
#undef portGET_CORE_ID
#define portGET_CORE_ID() VF__get_core_num()

2
Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h
View file

@ -320,7 +320,7 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
//@ assert( forall(gOwners, (mem_list_elem)(gTasks)) == true );
//@ forall_remove_nth(index_of(pxTaskItem, gCells), gOwners, (mem_list_elem)(gTasks));
//@ assert( forall(gOwners2, (mem_list_elem)(gTasks)) == true );
//@ forall_mem_implies_subset(gOwners2, gTasks);
//@ forall_mem_implies_superset(gTasks, gOwners2);
//@ assert( subset(gOwners2, gTasks) == true );
vListInsertEnd( pxReadyList, pxTaskItem );

4
Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs_extended/scp_list_predicates_extended.h
View file

@ -239,8 +239,8 @@ ensures
assert( gValsRes == append(gValsPrefix, cons(gItemVal, nil)) );
drop_cons(gCells, index_of(pxItem, gCells));
drop_cons(gVals, index_of(pxItem, gCells));
drop_n_plus_one(gCells, index_of(pxItem, gCells));
drop_n_plus_one(gVals, index_of(pxItem, gCells));
nth_index(gCells, pxItem);
assert( gCellsRes == gCells );

65
Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h
View file

@ -5,55 +5,30 @@
* of VeriFast's standard library.
*/
// Most of the following lemmas are axioms.
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
/*@
lemma void head_drop_n_equals_nths<t>(list<t> xs, int n);
requires n >= 0;
ensures head(drop(n, xs)) == nth(n, xs);
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void drop_index_equals_singleton_implies_last_element<t>(list<t> xs, t x);
requires drop(index_of(x, xs), xs) == cons(x, nil);
ensures index_of(x, xs) == length(xs) - 1;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
// Can we replace this by standard lemma `drop_n_plus_one`?
lemma void drop_cons<t>(list<t> xs, int n);
requires n < length(xs);
ensures drop(n, xs) == cons(nth(n, xs), drop(n+1, xs));
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void nth_index<t>(list<t> xs, t x)
lemma void nth_index<t>(list<t> xs, t x);
requires mem(x, xs) == true;
ensures nth(index_of(x, xs), xs) == x;
{
// Will prove later. For now, we only validate with an example.
list<int> _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil)))))));
int _x = 4;
int i = index_of(_x, _xs);
int nthi = nth(index_of(_x, _xs), _xs);
assert( nth(index_of(_x, _xs), _xs) == _x );
// ADMIT LEMMA, PROVE LATER
assume(false);
}
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void mem_prefix_implies_mem<t>(t x, list<t> xs, int n);
requires mem(x, take(n, xs)) == true;
ensures mem(x, xs) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void mem_suffix_implies_mem<t>(t x, list<t> xs, int n);
requires mem(x, drop(n, xs)) == true;
ensures mem(x, xs) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void drop_n_plus_m<t>(list<t> xs, int n, int m);
requires true;
ensures drop(n, drop(m, xs)) == drop(n + m, xs);
@ -78,7 +53,6 @@ fixpoint bool superset<t>(list<t> super, list<t> sub) {
}
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void update_out_of_bounds<t>(int index, t x, list<t> xs)
requires (index < 0 || index >= length(xs));
ensures update(index, x, xs) == xs;
@ -91,7 +65,6 @@ ensures update(index, x, xs) == xs;
}
}
lemma void index_of_different<t>(t x1, t x2, list<t> xs)
requires x1 != x2 &*& mem(x1, xs) == true &*& mem(x2, xs) == true;
ensures index_of(x1, xs) != index_of(x2, xs);
@ -105,91 +78,57 @@ ensures index_of(x1, xs) != index_of(x2, xs);
}
}
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void subset_cons_tail<t>(list<t> xs);
requires xs == cons(?h, ?t);
ensures subset(t, xs) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void remove_result_subset<t>(t x, list<t> xs);
requires true;
ensures subset(remove(x, xs), xs) == true;
// TODO: Revisit this lemma
// {
// switch(xs) {
// case nil:
// case cons(h, t):
// remove_result_subset(x, t);
// if(h == x) {
// assert( remove(x, xs) == t );
// subset_cons_tail(xs);
// assert( subset(t, cons(x, t) ) == true );
// } else {
// ;
// }
// }
// }
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
// Special case of `nth_update` from `listex.gh`.
lemma void update_preserves_rest<t>(int i, int u, t v, list<t> xs);
requires 0 <= i && i < length(xs) && 0 <= u && u < length(xs) && i != u;
ensures nth(i, update(u, v, xs)) == nth(i, xs);
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void append_take_nth_drop<t>(int n, list<t> xs);
requires 0 <= n &*& n < length(xs);
ensures xs == append( take(n, xs), cons(nth(n, xs), drop(n+1, xs)) );
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
// Note: `listex.gh` contains lemma `forall_drop` but no corresponding
// `forall_take`.
lemma void forall_take<t>(list<t> xs, fixpoint(t, bool) p, int i);
requires forall(xs, p) == true;
ensures forall(take(i, xs), p) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void forall_mem_implies_superset<t>(list<t> super, list<t> sub);
requires forall(sub, (mem_list_elem)(super)) == true;
ensures superset(super, sub) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
// TODO: Rename into "forall_mem_implies_superset"
lemma void forall_mem_implies_subset<t>(list<t> sub, list<t> super);
requires forall(sub, (mem_list_elem)(super)) == true;
ensures superset(super, sub) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void subset_implies_forall_mem<t>(list<t> sub, list<t> super);
requires subset(sub, super) == true;
ensures forall(sub, (mem_list_elem)(super)) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void forall_remove<t>(t x, list<t> xs, fixpoint(t, bool) p);
requires forall(xs, p) == true;
ensures forall(remove(x, xs), p) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void forall_remove_nth<t>(int n, list<t> xs, fixpoint(t, bool) p);
requires forall(xs, p) == true;
ensures forall(remove_nth(n, xs), p) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void nth_implies_mem<t>(int n, list<t> xs);
requires 0 <= n &*& n < length(xs);
ensures mem(nth(n, xs), xs) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void subset_append<t>(list<t> sub1, list<t> sub2, list<t> super);
requires subset(sub1, super) == true &*& subset(sub2, super) == true;
ensures subset(append(sub1, sub2), super) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void subset_take<t>(int i, list<t> xs);
requires true;
ensures subset(take(i, xs), xs) == true;
// TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void subset_drop<t>(int i, list<t> xs);
requires true;
ensures subset(drop(i, xs), xs) == true;