From b1fc658413b38201a70c82194b8c99f4ad24f2b1 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Fri, 18 Nov 2022 15:38:32 -0500 Subject: [PATCH] Added single-core list predicates and proofs. Most proofs are commented out for the moment. --- .../single_core_proofs/list_predicates.h | 77 --- .../proof/single_core_proofs/scp_common.h | 635 ++++++++++++++++++ .../single_core_proofs/scp_list_predicates.h | 433 ++++++++++++ verification/verifast/proof/task_predicates.h | 2 +- .../verifast/start-vfide--preprocessed.sh | 1 + 5 files changed, 1070 insertions(+), 78 deletions(-) delete mode 100644 verification/verifast/proof/single_core_proofs/list_predicates.h create mode 100644 verification/verifast/proof/single_core_proofs/scp_common.h create mode 100644 verification/verifast/proof/single_core_proofs/scp_list_predicates.h diff --git a/verification/verifast/proof/single_core_proofs/list_predicates.h b/verification/verifast/proof/single_core_proofs/list_predicates.h deleted file mode 100644 index 400dbf91c..000000000 --- a/verification/verifast/proof/single_core_proofs/list_predicates.h +++ /dev/null @@ -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 cells, - list 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, - listcells, - listvals) = - 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 */ \ No newline at end of file diff --git a/verification/verifast/proof/single_core_proofs/scp_common.h b/verification/verifast/proof/single_core_proofs/scp_common.h new file mode 100644 index 000000000..a1ade6f14 --- /dev/null +++ b/verification/verifast/proof/single_core_proofs/scp_common.h @@ -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 + +fixpoint list rotate_left(int n, list xs) { + return append(drop(n, xs), take(n, xs)); +} + +fixpoint list singleton(t x) { + return cons(x, nil); +} + +@*/ +#ifdef VERIFAST_TODO + +lemma void note(bool b) + requires b; + ensures b; +{} + +lemma_auto void rotate_length(int n, list xs) + requires 0 <= n && n <= length(xs); + ensures length(rotate_left(n, xs)) == length(xs); +{} + +lemma void take_length_eq(int k, list xs, list 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(list xs, list 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(int i, list 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(int i, list 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(int i, int j, t x, list 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(int i, int j, t x, list 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(int i, int j, t x, list 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(int i, int j, t x, list 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(int i, t x, list 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(int n, list xs, list 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(int m, int n, list 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(int m, int n, list 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(list 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(list 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 x, int n, list 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(list 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(int k, int i, list xs, list 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(int k, int i, list xs, list 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(int k, int i, list xs, list 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(int k, int i, list xs, list 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(listprefix, t x, listsuffix, int i, list 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(list 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(listprefix, t x, listsuffix, int i, list 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 */ diff --git a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h new file mode 100644 index 000000000..3f044594e --- /dev/null +++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h @@ -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 + #include + //@#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 cells, + list 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 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, + listcells, + listvals) = + 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 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 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 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 cells, + list 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 cells1, + list vals1, + struct xLIST_ITEM *n2, + struct xLIST_ITEM *nprev2, + struct xLIST_ITEM *mnext2, + struct xLIST_ITEM *m2, + list cells2, + list 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( + list 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(list 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 x, list l1, list 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* */ diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h index 02fc7c806..57e3a89bc 100644 --- a/verification/verifast/proof/task_predicates.h +++ b/verification/verifast/proof/task_predicates.h @@ -2,7 +2,7 @@ #define TASKS_GH -#include "single_core_proofs/list_predicates.h" +#include "single_core_proofs/scp_list_predicates.h" /*@ diff --git a/verification/verifast/start-vfide--preprocessed.sh b/verification/verifast/start-vfide--preprocessed.sh index de528818f..39d4ff706 100755 --- a/verification/verifast/start-vfide--preprocessed.sh +++ b/verification/verifast/start-vfide--preprocessed.sh @@ -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