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

Added single-core list predicates and proofs. Most proofs are commented out for the moment.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-18 15:38:32 -05:00
parent f5c0a64f86
commit b1fc658413
5 changed files with 1070 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

77
verification/verifast/proof/single_core_proofs/list_predicates.h
View file

@ -1,77 +0,0 @@
#ifndef LIST_PREDICATES_H
#define LIST_PREDICATES_H
/*
* The code below has been taken from:
* pull request:
* https://github.com/FreeRTOS/FreeRTOS/pull/836
* file:
* FreeRTOS/Test/VeriFast/include/proof/list.h
*
*/
/*@
predicate xLIST_ITEM(
struct xLIST_ITEM *n,
TickType_t xItemValue,
struct xLIST_ITEM *pxNext,
struct xLIST_ITEM *pxPrevious,
struct xLIST *pxContainer;)
=
n->xItemValue |-> xItemValue &*&
n->pxNext |-> pxNext &*&
n->pxPrevious |-> pxPrevious &*&
n->pvOwner |-> _ &*&
n->pxContainer |-> pxContainer;
// by Tobias Reinhard
predicate xList_gen(struct xLIST *l) =
l->uxNumberOfItems |-> _ &*&
l->pxIndex |-> _;
predicate List_p(List_t* l);
@*/
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/* @
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
@*/
/* @
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
@*/
#endif /* LIST_PREDICATES_H */

635
verification/verifast/proof/single_core_proofs/scp_common.h Normal file
View file

@ -0,0 +1,635 @@
/*
* The code below has been taken from:
* pull request:
* https://github.com/FreeRTOS/FreeRTOS/pull/836
* file:
* FreeRTOS/Test/VeriFast/include/proof/list.h
*
* The file has been converted from a ghost header
* into a regular header.
* It has also been renamed from `common.h` into
* `scp_common.h`.
* The include guards have been updated accordingly.
*
* All changes to the proofs, predicates, etc.
* are guarded by a check that `VERIFAST_SINGLE_CORE` is
* NOT defined.
*
* Temporary removals are guarded by `VERIFAST_TODO`.
*/
/*
* FreeRTOS V202112.00
* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
* https://www.FreeRTOS.org
* https://github.com/FreeRTOS
*
*/
#ifndef SCP_COMMON_H
#define SCP_COMMON_H
/*@
#include <listex.gh>
fixpoint list<t> rotate_left<t>(int n, list<t> xs) {
return append(drop(n, xs), take(n, xs));
}
fixpoint list<t> singleton<t>(t x) {
return cons(x, nil);
}
@*/
#ifdef VERIFAST_TODO
lemma void note(bool b)
requires b;
ensures b;
{}
lemma_auto void rotate_length<t>(int n, list<t> xs)
requires 0 <= n && n <= length(xs);
ensures length(rotate_left(n, xs)) == length(xs);
{}
lemma void take_length_eq<t>(int k, list<t> xs, list<t> ys)
requires 0 <= k && k <= length(xs) && take(k, xs) == ys;
ensures length(ys) == k;
{}
lemma void leq_bound(int x, int b)
requires b <= x && x <= b;
ensures x == b;
{}
lemma void mul_mono_l_strict(int x, int y, int n)
requires 0 < n &*& x < y;
ensures x * n < y * n;
{
for (int i = 1; i < n; i++)
invariant i <= n &*& x * i < y * i;
decreases n - i;
{}
}
lemma void div_leq(int x, int y, int n)
requires 0 < n && x * n <= y * n;
ensures x <= y;
{
assert x * n <= y * n;
if (x <= y) {
mul_mono_l(x,y,n);
} else {
mul_mono_l_strict(y,x,n); //< contradiction
}
}
lemma void div_lt(int x, int y, int n)
requires 0 < n && x * n < y * n;
ensures x < y;
{
assert x * n <= y * n;
if (x == y) {
} else if (x <= y) {
mul_mono_l(x,y,n);
} else {
assert y < x;
mul_mono_l(y,x,n); //< contradiction
}
}
lemma_auto void mod_same(int n)
requires 0 < n;
ensures n % n == 0;
{
div_rem_nonneg(n, n);
if (n / n < 1) {} else if (n / n > 1) {
mul_mono_l(2, n/n, n);
} else {}
}
lemma void mod_lt(int x, int n)
requires 0 <= x && x < n;
ensures x % n == x;
{
div_rem_nonneg(x, n);
if (x / n > 0) {
mul_mono_l(1, x / n, n);
} else {
}
}
lemma void mod_plus_one(int x, int y, int n)
requires 0 <= y && 0 < n && x == (y % n);
ensures ((x+1) % n) == ((y+1) % n);
{
div_rem_nonneg(y, n);
div_rem_nonneg(y+1, n);
div_rem_nonneg(y%n+1, n);
if (y%n+1 < n) {
mod_lt(y%n+1, n);
assert y%n == y - y/n*n;
assert (y+1)%n == y + 1 - (y + 1)/n*n;
if ((y+1)/n > y/n) {
mul_mono_l(y/n + 1, (y+1)/n, n);
} else if ((y+1)/n < y/n) {
mul_mono_l((y+1)/n + 1, y/n, n);
}
assert y - (y+1)/n*n == y - y/n*n;
assert y+1 - (y+1)/n*n == y - y/n*n + 1;
assert (y+1)%n == y%n + 1;
} else {
assert y%n+1 == n;
assert (y%n+1)%n == 0;
if (y/n + 1 < (y+1)/n) {
mul_mono_l(y/n + 2, (y+1)/n, n);
} else if (y/n + 1 > (y+1)/n) {
mul_mono_l((y+1)/n, y/n, n);
}
assert (y+1)/n == y/n + 1;
note((y+1)/n*n == (y/n + 1)*n);
assert (y+1)%n == 0;
}
assert (y%n+1)%n == (y+1)%n;
}
lemma void mod_mul(int x, int n, int y)
requires 0 < n && 0 <= x && 0 <= y;
ensures (x*n + y)%n == y%n;
{
mul_mono_l(0, x, n);
div_rem_nonneg(x*n+y, n);
div_rem_nonneg(y, n);
if ((x*n+y)/n > x + y/n) {
mul_mono_l(x + y/n + 1, (x*n+y)/n, n);
} else if ((x*n+y)/n < x + y/n) {
mul_mono_l((x*n+y)/n + 1, x + y/n, n);
}
note((x*n + y)/n == x + y/n);
note((x*n + y)/n*n == (x + y/n)*n);
}
lemma void mod_plus_distr(int x, int y, int n)
requires 0 < n && 0 <= x && 0 <= y;
ensures ((x % n) + y) % n == (x + y) % n;
{
div_rem_nonneg(x, n);
div_rem_nonneg(x%n+y, n);
div_rem_nonneg(x+y, n);
assert x == x/n*n + x%n;
mod_mul(x/n, n, x%n + y);
}
lemma_auto void mod_mod(int x, int n)
requires 0 < n && 0 <= x;
ensures (x % n) % n == (x % n);
{
mod_plus_distr(x, 0, n);
}
lemma void mod_plus(int x, int y, int n);
requires 0 < n && 0 <= x && 0 <= y;
ensures (x + y) % n == ((x % n) + (y % n)) % n;
lemma_auto void mod_range(int x, int n)
requires 0 <= x && 0 < n;
ensures 0 <= (x % n) && (x % n) < n;
{
div_rem_nonneg(x, n);
}
lemma void head_append<t>(list<t> xs, list<t> ys)
requires 0 < length(xs);
ensures head(append(xs, ys)) == head(xs);
{
switch(xs)
{
case cons(c, cs):
case nil:
}
}
lemma void drop_take_singleton<t>(int i, list<t> xs)
requires 0 < i && i < length(xs);
ensures drop(i-1, take(i, xs)) == singleton(nth(i-1, xs));
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 1) {
} else {
drop_take_singleton(i-1, xs0);
}
}
}
lemma void take_singleton<t>(int i, list<t> xs)
requires 0 <= i && i < length(xs);
ensures append(take(i, xs), singleton(nth(i, xs))) == take(i+1, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 0) {
} else {
take_singleton(i-1, xs0);
}
}
}
lemma void drop_update_le<t>(int i, int j, t x, list<t> xs)
requires 0 <= i && i <= j && j < length(xs);
ensures drop(i, update(j, x, xs)) == update(j - i, x, drop(i, xs));
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 0) {
} else {
drop_update_le(i - 1, j - 1, x, xs0);
}
}
}
lemma void drop_update_ge<t>(int i, int j, t x, list<t> xs)
requires 0 <= j && j < i && i < length(xs);
ensures drop(i, update(j, x, xs)) == drop(i, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (j == 0) {
} else {
drop_update_ge(i - 1, j - 1, x, xs0);
}
}
}
lemma void take_update_le<t>(int i, int j, t x, list<t> xs)
requires 0 <= i && i <= j;
ensures take(i, update(j, x, xs)) == take(i, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 0) {
} else {
take_update_le(i - 1, j - 1, x, xs0);
}
}
}
lemma void take_update_ge<t>(int i, int j, t x, list<t> xs)
requires 0 <= j && j < i && i <= length(xs);
ensures take(i, update(j, x, xs)) == update(j, x, take(i, xs));
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (j == 0) {
} else {
take_update_ge(i - 1, j - 1, x, xs0);
}
}
}
lemma void update_eq_append<t>(int i, t x, list<t> xs)
requires 0 <= i && i < length(xs);
ensures update(i, x, xs) == append(take(i, xs), cons(x, drop(i + 1, xs)));
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 0) {
} else {
update_eq_append(i - 1, x, xs0);
}
}
}
lemma void take_append_ge<t>(int n, list<t> xs, list<t> ys)
requires length(xs) <= n;
ensures take(n, append(xs, ys)) == append(xs, take(n - length(xs), ys));
{
switch (xs) {
case nil:
case cons(x0, xs0):
take_append_ge(n - 1, xs0, ys);
}
}
lemma void drop_drop<t>(int m, int n, list<t> xs)
requires 0 <= m && 0 <= n;
ensures drop(m, drop(n, xs)) == drop(m+n, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (n == 0) {} else {
drop_drop(m, n-1, xs0);
}
}
}
lemma void take_take<t>(int m, int n, list<t> xs)
requires 0 <= m && m <= n && n <= length(xs);
ensures take(m, take(n, xs)) == take(m, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (m == 0) {} else {
take_take(m - 1, n - 1, xs0);
}
}
}
lemma_auto void take_head<t>(list<t> xs)
requires 0 < length(xs);
ensures take(1, xs) == singleton(head(xs));
{
switch(xs) {
case nil:
case cons(x0, xs0):
}
}
// Following lemma from `verifast/bin/rt/_list.java`
lemma void remove_remove_nth<t>(list<t> xs, t x)
requires mem(x, xs) == true;
ensures remove(x, xs) == remove_nth(index_of(x, xs), xs);
{
switch (xs) {
case nil:
case cons(h, tl):
if (x == h) {
assert index_of(x, xs) == 0;
} else {
remove_remove_nth(tl, x);
}
}
}
lemma void mem_take_false<t>(t x, int n, list<t> xs)
requires mem(x, xs) == false;
ensures mem(x, take(n, xs)) == false;
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (x0 != x && n != 0)
mem_take_false(x, n - 1, xs0);
}
}
// Following lemma from `verifast/bin/rt/_list.java`. Renamed to
// avoid clash with listex.c's nth_drop lemma.
lemma void nth_drop2<t>(list<t> vs, int i)
requires 0 <= i && i < length(vs);
ensures nth(i, vs) == head(drop(i, vs));
{
switch (vs) {
case nil:
case cons(v, vs0):
if (i == 0) {
} else {
nth_drop2(vs0, i - 1);
}
}
}
lemma void enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
requires 0 <= k && 0 <= i && 0 < length(xs) && k < length(xs) && i < length(xs) && take(k, rotate_left(i, xs)) == ys;
ensures take(k+1, rotate_left(i, update((i+k)%length(xs), z, xs))) == append(ys, cons(z, nil));
{
int j = (i+k)%length(xs);
assert take(k, append(drop(i, xs), take(i, xs))) == ys;
if (i + k < length(xs)) {
mod_lt(i + k, length(xs));
assert j == i + k;
drop_update_le(i, i + k, z, xs);
assert drop(i, update(i + k, z, xs)) == update(k, z, drop(i, xs));
take_update_le(i, i + k, z, xs);
assert take(i, update(i + k, z, xs)) == take(i, xs);
take_append(k+1, update(k, z, drop(i, xs)), take(i, xs));
assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) == take(k+1, update(k, z, drop(i, xs)));
update_eq_append(k, z, drop(i, xs));
assert update(k, z, drop(i, xs)) == append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))));
take_append_ge(k+1, take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))));
assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) ==
append(take(k, drop(i, xs)), {z});
take_append(k, drop(i, xs), take(i, xs));
assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
assert take(k+1, update(k, z, drop(i, xs))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
assert take(k+1, append(drop(i, update(i + k, z, xs)), take(i, update(i + k, z, xs)))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
} else {
assert i + k < 2 * length(xs);
div_rem_nonneg(i + k, length(xs));
if ((i + k) / length(xs) > 1) {
mul_mono_l(2, (i + k) / length(xs), length(xs));
} else if ((i + k) / length(xs) < 1) {
mul_mono_l((i + k) / length(xs), 0, length(xs));
}
assert j == i + k - length(xs);
assert j < i;
drop_update_ge(i, j, z, xs);
assert drop(i, update(j, z, xs)) == drop(i, xs);
take_update_ge(i, j, z, xs);
assert update(j, z, take(i, xs)) == take(i, update(j, z, xs));
take_append_ge(k+1, drop(i, xs), take(i, update(j, z, xs)));
assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) ==
append(drop(i, xs), take(j+1, update(j, z, take(i, xs))));
update_eq_append(j, z, take(i, xs));
assert update(j, z, take(i, xs)) == append(take(j, take(i, xs)), cons(z, drop(j + 1, take(i, xs))));
take_take(j, i, xs);
assert update(j, z, take(i, xs)) == append(take(j, xs), cons(z, drop(j+1, take(i, xs))));
take_append_ge(j+1, take(j, xs), cons(z, drop(j+1, take(i, xs))));
assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) ==
append(drop(i, xs), append(take(j, xs), {z}));
take_append_ge(k, drop(i, xs), take(i, xs));
append_assoc(drop(i, xs), take(j, xs), {z});
assert append(drop(i, xs), append(take(j, xs), {z})) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
}
assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) ==
append(take(k, append(drop(i, xs), take(i, xs))), {z});
assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) == append(ys, {z});
}
lemma void front_enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
requires 0 < length(xs) && 0 <= k && k < length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left((i+1)%length(xs), xs)) == ys;
ensures take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys);
{
int n = length(xs);
if (i+1 < n) {
mod_lt(i+1, n);
assert i < n;
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs))));
drop_update_le(i, i, z, xs);
take_update_le(i, i, z, xs);
assert take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs)))) ==
take(k+1, append(update(0, z, drop(i, xs)), take(i, xs)));
update_eq_append(0, z, drop(i, xs));
assert update(0, z, drop(i, xs)) == cons(z, drop(1, drop(i, xs)));
drop_drop(1, i, xs);
assert take(k+1, append(update(0, z, drop(i, xs)), take(i, xs))) ==
take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs)));
assert take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs))) ==
cons(z, take(k, append(drop(i+1, xs), take(i, xs))));
assert ys == take(k, rotate_left(i+1, xs));
assert ys == take(k, append(drop(i+1, xs), take(i+1, xs)));
if (k <= length(drop(i+1, xs))) {
take_append(k, drop(i+1, xs), take(i+1, xs));
take_append(k, drop(i+1, xs), take(i, xs));
} else {
take_append_ge(k, drop(i+1, xs), take(i+1, xs));
take_append_ge(k, drop(i+1, xs), take(i, xs));
assert (i+1) + k < 2 * n;
div_rem_nonneg((i+1) + k, n);
if (((i+1) + k) / n > 1) {
mul_mono_l(2, ((i+1) + k) / n, n);
} else if (((i+1) + k) / n < 1) {
mul_mono_l(((i+1) + k) / n, 0, n);
}
int j = ((i+1)+k)%n;
assert j <= i;
int l = length(drop(i+1, xs));
assert l == n - i - 1;
take_take(k - l, i + 1, xs);
take_take(k - l, i, xs);
}
} else {
assert i == (n-1);
assert (i + 1) % n == 0;
drop_update_le(i, i, z, xs);
update_eq_append(0, z, xs);
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs))));
drop_update_le(i, i, z, xs);
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
take(k+1, append(update(0, z, drop(i, xs)), take(i, update(i, z, xs))));
update_eq_append(0, z, drop(i, xs));
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
take(k+1, append(cons(z, drop(1, drop(i, xs))), take(i, update(i, z, xs))));
drop_drop(1, i, xs);
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
take(k+1, append(cons(z, nil), take(i, update(i, z, xs))));
take_update_le(i, i, z, xs);
assert take(k+1, rotate_left(i, update(i, z, xs))) ==
cons(z, take(k, take(i, xs)));
take_take(k, i, xs);
assert take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys);
}
}
lemma void deq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
requires 0 < k && k <= length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys && z == head(ys);
ensures take(k-1, rotate_left((i+1)%length(xs), xs)) == tail(ys);
{
int j = (i+1)%length(xs);
drop_n_plus_one(i, xs);
assert tail(take(k, append(drop(i, xs), take(i, xs)))) == take(k-1, append(drop(i+1, xs), take(i, xs)));
if (i+1 < length(xs)) {
mod_lt(i+1, length(xs));
assert j == i+1;
if (k-1 <= length(xs)-j) {
take_append(k-1, drop(j, xs), take(j, xs));
take_append(k-1, drop(j, xs), take(i, xs));
} else {
assert k+i > length(xs);
take_append_ge(k-1, drop(j, xs), take(j, xs));
take_append_ge(k-1, drop(j, xs), take(i, xs));
assert k-1-(length(xs)-j) == k+i-length(xs);
assert k+i-length(xs) <= i;
take_take(k+i-length(xs), j, xs);
take_take(k+i-length(xs), i, xs);
assert take(k+i-length(xs), take(j, xs)) == take(k+i-length(xs), take(i, xs));
}
} else {
assert i+1 == length(xs);
assert (i+1)%length(xs) == 0;
assert j == 0;
assert append(drop(j, xs), take(j, xs)) == xs;
assert append(drop(i+1, xs), take(i, xs)) == take(i, xs);
take_append_ge(k-1, drop(i+1, xs), take(i, xs));
take_take(k-1, i, xs);
}
assert take(k-1, append(drop(j, xs), take(j, xs))) == take(k-1, append(drop(i+1, xs), take(i, xs)));
assert take(k-1, append(drop(j, xs), take(j, xs))) == tail(take(k, append(drop(i, xs), take(i, xs))));
}
lemma void deq_value_lemma<t>(int k, int i, list<t> xs, list<t> ys)
requires 0 < k && k <= length(ys) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys;
ensures nth(i, xs) == head(ys);
{
drop_n_plus_one(i, xs);
assert nth(i, xs) == head(take(k, append(drop(i, xs), take(i, xs))));
}
lemma void combine_list_no_change<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs)
requires 0 <= i && i < length(xs) && prefix == take(i, xs) && x == nth(i, xs) && suffix == drop(i+1, xs);
ensures xs == append(prefix, cons(x, suffix));
{
drop_n_plus_one(i, xs);
}
// Following lemma from `verifast/examples/vstte2010/problem4.java`.
lemma void update_rewrite<t>(list<t> vs, t v, int pos)
requires 0 <= pos && pos < length(vs);
ensures update(pos, v, vs) == append(take(pos, vs), cons(v, (drop(pos+1, vs))));
{
switch(vs) {
case nil:
case cons(h, t):
if (pos == 0) {
} else {
update_rewrite(t, v, pos - 1);
}
}
}
lemma void combine_list_update<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs)
requires 0 <= i && i < length(xs) && prefix == take(i, xs) && suffix == drop(i+1, xs);
ensures update(i, x, xs) == append(prefix, cons(x, suffix));
{
update_rewrite(xs, x, i);
}
@*/
#endif /* VERIFAST_TODO */
#endif /* SCP_COMMON_H */

433
verification/verifast/proof/single_core_proofs/scp_list_predicates.h Normal file
View file

@ -0,0 +1,433 @@
/*
* The code below has been taken from:
* pull request:
* https://github.com/FreeRTOS/FreeRTOS/pull/836
* file:
* FreeRTOS/Test/VeriFast/include/proof/list.h
*
* The file has been renamed from `list.h` into
* `scp_list_predicates.h` to avoid naming conflicts.
* The include guards have been updated accordingly.
*
* All changes to the proofs, predicates, etc.
* are guarded by a check that `VERIFAST_SINGLE_CORE` is
* NOT defined.
*
* Temporary removals are guarded by `VERIFAST_TODO`.
*/
/*
* FreeRTOS V202112.00
* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
* https://www.FreeRTOS.org
* https://github.com/FreeRTOS
*
*/
/* *INDENT-OFF* */
#ifndef SCP_LIST_PREDICATES_H
#define SCP_LIST_PREDICATES_H
#ifndef VERIFAST_SINGLE_CORE
/* Reasons for rewrite:
* - "common.gh" was converted into regular header "scp_common.h"
* - Using existing proof setup instead of definitions below.
*/
#include "scp_common.h"
#else
#define VERIFAST
#include <stdlib.h>
#include <stdint.h>
//@#include "common.gh"
typedef size_t TickType_t;
typedef size_t UBaseType_t;
typedef ssize_t BaseType_t;
#define pdTRUE 1
#define pdFALSE 0
/* Empty/no-op macros */
#define mtCOVERAGE_TEST_MARKER()
#define mtCOVERAGE_TEST_DELAY()
#define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )
#define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )
#define listTEST_LIST_INTEGRITY( pxList )
#define listTEST_LIST_ITEM_INTEGRITY( pxListItem )
#define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
#define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
#endif /* VERIFAST_SINGLE_CORE */
/* Max value stored in sentinel xListEnd element */
#ifndef VERIFAST_SINGLE_CORE
/* Reason for rewrite: Match RP2040 port. */
//VF_macro #define portMAX_DELAY 0xffffffffUL
/* Verify that the preprocessor and our VeriFast proofs evaluate
* `portMAX_DELAY` to the same values.
*/
void validate_portMAX_DELAY_value()
//@ requires true;
//@ ensures true;
{
//@ TickType_t gVal = portMAX_DELAY;
TickType_t val = portMAX_DELAY;
//@ assert(val == gVal);
}
#else
#define portMAX_DELAY UINT_MAX
#endif /* VERIFAST_SINGLE_CORE */
#ifdef VERIFAST_SINGLE_CORE
/* Reason for deletion:
* structs already defined in FreeRTOS header "list.h"
*/
struct xLIST;
struct xLIST_ITEM {
TickType_t xItemValue;
struct xLIST_ITEM * pxNext;
struct xLIST_ITEM * pxPrevious;
void * pvOwner;
struct xLIST *pxContainer;
};
typedef struct xLIST_ITEM ListItem_t;
typedef struct xLIST {
UBaseType_t uxNumberOfItems;
struct xLIST_ITEM *pxIndex;
#ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
struct xLIST_ITEM xListEnd;
#else
MiniListItem_t xListEnd;
#endif
} List_t;
#endif /* VERIFAST_SINGLE_CORE */
/*@
predicate xLIST_ITEM(
struct xLIST_ITEM *n,
TickType_t xItemValue,
struct xLIST_ITEM *pxNext,
struct xLIST_ITEM *pxPrevious,
struct xLIST *pxContainer;) =
n->xItemValue |-> xItemValue &*&
n->pxNext |-> pxNext &*&
n->pxPrevious |-> pxPrevious &*&
n->pvOwner |-> _ &*&
n->pxContainer |-> pxContainer;
@*/
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/*@
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
@*/
#ifdef VERIFAST_TODO
lemma void dls_star_item(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
struct xLIST_ITEM *o)
requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
assert xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
else {
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_star_item(nnext, m, o);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_distinct(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
{
if (n == m) {
open DLS(n, nprev, mnext, m, cells, vals, l);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
open DLS(n, nprev, mnext, m, cells, vals, l);
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_distinct(nnext, n, mnext, m, tail(cells));
dls_star_item(nnext, m, n);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
lemma void xLIST_distinct_cells(struct xLIST *l)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2);
ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
dls_star_item(end, endprev, x);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void dls_first_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
assert cells == cons(n, nil);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
assert cells == cons(n, ?tail);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_not_empty(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
struct xLIST_ITEM *x)
requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n;
ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
{
open DLS(n, m, n, m, cells, vals, l);
close DLS(n, m, n, m, cells, vals, l);
}
lemma void dls_last_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
// trivial
} else {
open xLIST_ITEM(n, _, ?nnext, _, l);
assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l);
dls_last_mem(o, n, mnext, m, tail(cells));
close xLIST_ITEM(n, _, nnext, _, l);
}
close DLS(n, nprev, mnext, m, cells, vals, l);
}
lemma void split(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST_ITEM *x,
int i)
requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), l) &*& xprev == nth(i-1, cells);
{
open DLS(n, nprev, mnext, m, cells, vals, l);
assert n != m;
assert xLIST_ITEM(n, ?v, ?nnext, _, _);
assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
if (nnext == x) {
close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
close xLIST_ITEM(x, _, xnext, xprev, l);
close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
} else {
assert nnext != x;
split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
dls_star_item(nnext, xprev, n);
dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
assert n != xprev;
close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
}
}
lemma void join(
struct xLIST_ITEM *n1,
struct xLIST_ITEM *nprev1,
struct xLIST_ITEM *mnext1,
struct xLIST_ITEM *m1,
list<struct xLIST_ITEM * > cells1,
list<TickType_t > vals1,
struct xLIST_ITEM *n2,
struct xLIST_ITEM *nprev2,
struct xLIST_ITEM *mnext2,
struct xLIST_ITEM *m2,
list<struct xLIST_ITEM * > cells2,
list<TickType_t > vals2)
requires
DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
mnext1 == n2 &*& m1 == nprev2;
ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
{
if (n1 == m1) {
dls_first_mem(n1, nprev1, mnext1, m1, cells1);
dls_last_mem(n2, nprev2, mnext2, m2, cells2);
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
dls_star_item(n2, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
} else {
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
n2, nprev2, mnext2, m2, cells2, vals2);
assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
dls_star_item(o, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
}
}
lemma void idx_remains_in_list<t>(
list<t> cells,
t idx,
t x,
int ix)
requires
idx != x &*&
mem(idx, cells) == true &*&
mem(x, cells) == true &*&
index_of(x, cells) == ix;
ensures mem(idx, remove_nth(ix, cells)) == true;
{
neq_mem_remove(idx, x, cells);
remove_remove_nth(cells, x);
}
@*/
// Following lemma from `verifast/examples/shared_boxes/concurrentqueue.c`.
// Used in the uxListRemove proof to show that the item to remove `x` must
// have value `nth(i, vals)` where `i == index_of(x, cells)`.
/*@
lemma void drop_nth_index_of<t>(list<t> vs, int i)
requires
0 <= i && i < length(vs);
ensures
head(drop(i , vs)) == nth(i, vs);
{
switch(vs) {
case nil:
case cons(h, t):
if (i == 0) {
// trivial
} else {
drop_nth_index_of(t, i - 1);
}
}
}
@*/
/*@
lemma void remove_append<t>(t x, list<t> l1, list<t> l2)
requires mem(x, l1) == false;
ensures remove(x, append(l1, l2)) == append(l1, remove(x, l2));
{
switch(l1) {
case nil:
case cons(h1, t1):
remove_append(x, t1, l2);
}
}
@*/
#endif /* VERIFAST_TODO */
#endif /* SCP_LIST_PREDICATES_H */
/* *INDENT-ON* */

2
verification/verifast/proof/task_predicates.h
View file

@ -2,7 +2,7 @@
#define TASKS_GH
#include "single_core_proofs/list_predicates.h"
#include "single_core_proofs/scp_list_predicates.h"
/*@

1
verification/verifast/start-vfide--preprocessed.sh
View file

@ -35,6 +35,7 @@ echo "\n\nPreprocessing script finished\n\n"
# - Need z3v4.5 to handle bitvector arithmetic
"$VF_DIR/bin/vfide" "$PP_TASK_C" \
-I proof_setup \
-I proofs \
-codeFont "$FONT_SIZE" -traceFont "$FONT_SIZE" \
-assume_no_provenance \
-prover z3v4.5