diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/include/proof')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/include/proof/common.gh | 555 | ||||
| -rw-r--r-- | FreeRTOS/Test/VeriFast/include/proof/queue.h | 550 | ||||
| -rw-r--r-- | FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h | 57 |
3 files changed, 1162 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/include/proof/common.gh b/FreeRTOS/Test/VeriFast/include/proof/common.gh new file mode 100644 index 000000000..c3b064939 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/common.gh @@ -0,0 +1,555 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef COMMON_H +#define 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); +} + +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 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 void index_of_distinct<t>(list<t> xs, t x1, t x2) + requires mem(x1, xs) == true &*& mem(x2, xs) == true &*& x1 != x2; + ensures index_of(x1, xs) != index_of(x2, xs); +{ + switch (xs) { + case nil: + case cons(h, tl): + if (h == x1 || h == x2) { + /* trivial */ + } else { + index_of_distinct(tl, x1, x2); + } + } +} + +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); + } + } +} + +/* 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 /* COMMON_H */ diff --git a/FreeRTOS/Test/VeriFast/include/proof/queue.h b/FreeRTOS/Test/VeriFast/include/proof/queue.h new file mode 100644 index 000000000..610bc03d9 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/queue.h @@ -0,0 +1,550 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef QUEUE_H +#define QUEUE_H + +#define VERIFAST +#include <stdlib.h> +#include <stdint.h> +#include <string.h> +#include <threading.h> +/*@#include "common.gh"@*/ + +typedef size_t TickType_t; +typedef size_t UBaseType_t; +typedef ssize_t BaseType_t; + +/* Empty/no-op macros */ +/* Tracing */ +#define traceBLOCKING_ON_QUEUE_PEEK(x) +#define traceBLOCKING_ON_QUEUE_RECEIVE(x) +#define traceBLOCKING_ON_QUEUE_SEND(x) +#define traceQUEUE_CREATE(x) +#define traceQUEUE_CREATE_FAILED(x) +#define traceQUEUE_DELETE(x) +#define traceQUEUE_PEEK(x) +#define traceQUEUE_PEEK_FAILED(x) +#define traceQUEUE_PEEK_FROM_ISR(x) +#define traceQUEUE_PEEK_FROM_ISR_FAILED(x) +#define traceQUEUE_RECEIVE(x) +#define traceQUEUE_RECEIVE_FAILED(x) +#define traceQUEUE_RECEIVE_FROM_ISR(x) +#define traceQUEUE_RECEIVE_FROM_ISR_FAILED(x) +#define traceQUEUE_SEND(x) +#define traceQUEUE_SEND_FAILED(x) +#define traceQUEUE_SEND_FROM_ISR(x) +#define traceQUEUE_SEND_FROM_ISR_FAILED(x) +/* Coverage */ +#define mtCOVERAGE_TEST_MARKER() +/* Asserts */ +#define configASSERT(x) +#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID() + +/* Map portable memory management functions */ +#define pvPortMalloc malloc +#define vPortFree free + +#define queueSEND_TO_BACK ( ( BaseType_t ) 0 ) +#define queueSEND_TO_FRONT ( ( BaseType_t ) 1 ) +#define queueOVERWRITE ( ( BaseType_t ) 2 ) + +#define pdTRUE 1 +#define pdFALSE 0 + +#define pdPASS pdTRUE +#define pdFAIL pdFALSE +#define errQUEUE_FULL 0 +#define errQUEUE_EMPTY 0 + +/* Constants used with the cRxLock and cTxLock structure members. */ +#define queueUNLOCKED ( ( int8_t ) -1 ) +#define queueLOCKED_UNMODIFIED ( ( int8_t ) 0 ) +#define queueINT8_MAX ( ( int8_t ) 127 ) + +typedef struct QueuePointers +{ + int8_t * pcTail; /*< Points to the byte at the end of the queue storage area. Once more byte is allocated than necessary to store the queue items, this is used as a marker. */ + int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */ +} QueuePointers_t; + +typedef struct SemaphoreData +{ +#ifdef VERIFAST /*< do not model xMutexHolder */ + void *xMutexHolder; +#else + TaskHandle_t xMutexHolder; /*< The handle of the task that holds the mutex. */ +#endif + UBaseType_t uxRecursiveCallCount; /*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */ +} SemaphoreData_t; + +/* VeriFast does not support unions so we replace with a struct */ +struct fake_union_t { + QueuePointers_t xQueue; + SemaphoreData_t xSemaphore; +}; + +typedef struct xLIST { + UBaseType_t uxNumberOfItems; +#ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */ + struct xLIST_ITEM *pxIndex; + MiniListItem_t xListEnd; +#endif +} List_t; + +typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */ +{ + int8_t * pcHead; /*< Points to the beginning of the queue storage area. */ + int8_t * pcWriteTo; /*< Points to the free next place in the storage area. */ + +#ifdef VERIFAST /*< VeriFast does not model unions */ + struct fake_union_t u; +#else + union + { + QueuePointers_t xQueue; /*< Data required exclusively when this structure is used as a queue. */ + SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */ + } u; +#endif + + List_t xTasksWaitingToSend; /*< List of tasks that are blocked waiting to post onto this queue. Stored in priority order. */ + List_t xTasksWaitingToReceive; /*< List of tasks that are blocked waiting to read from this queue. Stored in priority order. */ + + volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */ + UBaseType_t uxLength; /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */ + UBaseType_t uxItemSize; /*< The size of each items that the queue will hold. */ + + volatile int8_t cRxLock; /*< Stores the number of items received from the queue (removed from the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + volatile int8_t cTxLock; /*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */ + + #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) ) + uint8_t ucStaticallyAllocated; /*< Set to pdTRUE if the memory used by the queue was statically allocated to ensure no attempt is made to free the memory. */ + #endif + + #if ( configUSE_QUEUE_SETS == 1 ) + struct QueueDefinition * pxQueueSetContainer; + #endif + + #if ( configUSE_TRACE_FACILITY == 1 ) + UBaseType_t uxQueueNumber; + uint8_t ucQueueType; + #endif + + /*@struct mutex *irqMask;@*/ /*< Ghost mutex simulates the effect of irq masking */ + /*@struct mutex *schedulerSuspend;@*/ /*< Ghost mutex simulates the effect of scheduler suspension */ + /*@struct mutex *locked;@*/ /*< Ghost mutex simulates the effect of queue locking */ +} xQUEUE; + +typedef xQUEUE Queue_t; + +typedef struct QueueDefinition * QueueHandle_t; + +/*@ +#define QUEUE_SHAPE(q, Storage, N, M, K) \ + malloc_block_QueueDefinition(q) &*& \ + q->pcHead |-> Storage &*& \ + q->pcWriteTo |-> ?WPtr &*& \ + q->u.xQueue.pcTail |-> ?End &*& \ + q->u.xQueue.pcReadFrom |-> ?RPtr &*& \ + q->uxItemSize |-> M &*& \ + q->uxLength |-> N &*& \ + q->uxMessagesWaiting |-> K &*& \ + q->cRxLock |-> ?rxLock &*& \ + q->cTxLock |-> ?txLock &*& \ + struct_QueuePointers_padding(&q->u.xQueue) &*& \ + struct_SemaphoreData_padding(&q->u.xSemaphore) &*& \ + struct_fake_union_t_padding(&q->u) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToSend) &*& \ + struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \ + q->u.xSemaphore.xMutexHolder |-> _ &*& \ + q->u.xSemaphore.uxRecursiveCallCount |-> _ &*& \ + true + +predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + 1 + K) % N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left((R+1)%N, contents)) &*& + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* A buffer allows us to interpret a flat character array of `N*M` bytes as a +list of `N` elements where each element is `M` bytes */ +/*@ +predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) = + N == 0 + ? elements == nil + : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs); + +lemma void buffer_length(char *buffer, size_t N, size_t M) +requires buffer(buffer, N, M, ?elements); +ensures buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + open buffer(buffer, N, M, elements); + close buffer(buffer, N, M, elements); + } else { + open buffer(buffer, N, M, elements); + buffer_length(buffer+M, N-1, M); + } +} +@*/ + +/* +There is no need in the queue proofs to preserve a relationship between `cs` +and `elements` (i.e., `flatten(elements) == cs`) because we only move in one +direction from `cs` to `elements` during queue creation when the contents is +fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from +elements back to cs then this would require a stronger lemma. +*/ +/*@ +lemma void buffer_from_chars(char *buffer, size_t N, size_t M) +requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M; +ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N; +{ + if (N == 0) { + close exists(nil); + } else { + int i = 0; + while (i < N) + invariant 0 <= i &*& i <= N &*& + chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*& + buffer(buffer + (N-i)*M, i, M, ?ys); + decreases N-i; + { + mul_mono_l(0, N-i-1, M); + chars_split(buffer, (N-i-1)*M); + mul_mono_l(i, N, M); + mul_mono_l(N-i, N, M); + take_take((N-i-1)*M, (N-i)*M, cs); + i++; + } + close exists(ys); + buffer_length(buffer, N, M); + } +} + +lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M) +requires + buffer(buffer, N1, M, ?elements1) &*& + buffer(buffer + N1 * M, N2, M, ?elements2) &*& + 0 <= N1 &*& 0 <= N2; +ensures buffer(buffer, N1+N2, M, append(elements1, elements2)); +{ + if (N1 == 0) { + open buffer(buffer, 0, M, _); + } else if (N2 == 0) { + open buffer(buffer + N1 * M, 0, M, _); + } else { + open buffer(buffer, N1, M, elements1); + append_buffer(buffer + M, N1-1, N2, M); + close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2))); + } +} + +lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i) +requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N; +ensures + buffer(buffer, i, M, take(i, elements)) &*& + chars(buffer + i * M, M, nth(i, elements)) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements)); +{ + if (i == 0) { + // straightforward + } else { + buffer_length(buffer, N, M); + int j = 0; + while (j < i) + invariant 0 <= j &*& j <= i &*& + buffer(buffer, j, M, take(j, elements)) &*& + buffer(buffer + j * M, N-j, M, drop(j, elements)); + decreases i-j; + { + drop_drop(1, j, elements); + nth_drop2(elements, j); + open buffer(buffer + j * M, N-j, M, drop(j, elements)); + assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements); + close buffer(buffer + j * M, 1, M, singleton(x)); + append_buffer(buffer, j, 1, M); + take_plus_one(j, elements); + j++; + } + drop_drop(1, j, elements); + nth_drop2(elements, i); + open buffer(buffer + (i+1) * M, (N-1-i), M, _); + } +} + +lemma void join_element(char *buffer, size_t N, size_t M, size_t i) +requires + 0 <= i &*& i < N &*& + buffer(buffer, i, M, ?prefix) &*& + chars(buffer + i * M, M, ?element) &*& + buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix); +ensures buffer(buffer, N, M, append(prefix, cons(element, suffix))); +{ + if (i == 0) { + open buffer(buffer, i, M, prefix); + assert prefix == nil; + close buffer(buffer, N, M, cons(element, suffix)); + } else { + close buffer(buffer + i * M, N-i, M, cons(element, suffix)); + append_buffer(buffer, i, N-i, M); + } +} + +predicate list(List_t *l;) = + l->uxNumberOfItems |-> _; + +predicate queuelists(QueueHandle_t q;) = + list(&q->xTasksWaitingToSend) &*& + list(&q->xTasksWaitingToReceive); +@*/ + +/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the +queue predicate above does not hold as a postcondition. If the caller +subsequently decrements K then the queue predicate can be reinstated. */ +/*@ +predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) = + QUEUE_SHAPE(q, Storage, N, M, K) &*& + 0 < N &*& + 0 < M &*& + 0 <= W &*& W < N &*& + 0 <= R &*& R < N &*& + 0 <= K &*& K <= N &*& + W == (R + K) % N &*& //< Differs from queue predicate + (-1) <= rxLock &*& + (-1) <= txLock &*& + (is_locked ? 0 <= rxLock : (-1) == rxLock) &*& + (is_locked ? 0 <= txLock : (-1) == txLock) &*& + WPtr == Storage + (W*M) &*& + RPtr == Storage + (R*M) &*& + End == Storage + (N*M) &*& + buffer(Storage, N, M, ?contents) &*& + length(contents) == N &*& + abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate + malloc_block(Storage, N*M) &*& + true + ; +@*/ + +/* Can't be called `mutex` as this clashes with VeriFast's predicate */ +/*@ +predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) = + QUEUE_SHAPE(q, Storage, N, 0, K) &*& + queuelists(q) &*& + 0 < N &*& + 0 <= K &*& K <= N &*& + (-1) <= rxLock &*& + (-1) <= txLock &*& + WPtr == Storage &*& + RPtr == Storage &*& + End == Storage &*& + malloc_block(Storage, 0) &*& + chars(Storage, 0, _) &*& + true + ; +@*/ + +/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost +`irqMask` gives access to the core queue resources. The permissions granted +after masking interrupts depends on the caller: +- A task has access to the queue and the queuelists +- An ISR has access to the queue and, if the queue is unlocked, the queuelists */ +/*@ +predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) = + q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr)); + +predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() = + queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_isr && is_locked ? true : queuelists(queue)); +@*/ + +/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */ +/*@ +predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() = + queue->locked |-> ?m &*& + mutex(m, queue_locked_invariant(queue)); + +predicate queuesuspend(QueueHandle_t q;) = + q->schedulerSuspend |-> ?m &*& + mutex(m, scheduler_suspended_invariant(q)); +@*/ + +/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */ +/*@ +predicate queuelock(QueueHandle_t q;) = + q->locked |-> ?m &*& + mutex(m, queue_locked_invariant(q)); + +predicate_ctor queue_locked_invariant(QueueHandle_t queue)() = + queuelists(queue); +@*/ + +BaseType_t vListInitialise(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +BaseType_t listLIST_IS_EMPTY(List_t *list); +/*@requires list->uxNumberOfItems |-> ?len;@*/ +/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/ + +typedef struct xTIME_OUT +{ + BaseType_t xOverflowCount; + TickType_t xTimeOnEntering; +} TimeOut_t; + +/*@ +predicate xTIME_OUT(struct xTIME_OUT *to;) = + to->xOverflowCount |-> _ &*& + to->xTimeOnEntering |-> _ &*& + struct_xTIME_OUT_padding(to); +@*/ + +void vTaskInternalSetTimeOutState( TimeOut_t * x); +/*@requires xTIME_OUT(x);@*/ +/*@ensures xTIME_OUT(x);@*/ + +BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ); +/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ +/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/ + +BaseType_t xTaskRemoveFromEventList(List_t *list); +/*@requires list(list);@*/ +/*@ensures list(list);@*/ + +void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait ); +/*@requires list(pxEventList);@*/ +/*@ensures list(pxEventList);@*/ + +void vTaskMissedYield(); +/*@requires true;@*/ +/*@ensures true;@*/ + +void vTaskSuspendAll(); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ + +BaseType_t xTaskResumeAll( void ); +/*@requires exists<QueueHandle_t>(?xQueue) &*& + [1/2]xQueue->schedulerSuspend |-> ?m &*& + mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*& + xQueue->locked |-> ?m2 &*& + mutex(m2, queue_locked_invariant(xQueue));@*/ +/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*& + [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/ + +void prvLockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]queuelock(xQueue); @*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ + +void prvUnlockQueue( QueueHandle_t xQueue ); +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& + [1/2]xQueue->locked |-> ?m &*& + mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*& + queue_locked_invariant(xQueue)();@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& + [1/2]queuelock(xQueue);@*/ + +void setInterruptMask(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + queuelists(xQueue);@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ +} + +void clearInterruptMask(QueueHandle_t xQueue) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*& + queuelists(xQueue);@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, false)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, false);@*/ +} + +#define taskENTER_CRITICAL() setInterruptMask(xQueue) +#define taskEXIT_CRITICAL() clearInterruptMask(xQueue) +#define portYIELD_WITHIN_API() +#define queueYIELD_IF_USING_PREEMPTION() + +UBaseType_t setInterruptMaskFromISR(QueueHandle_t xQueue) +/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/ +/*@ensures [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*& + queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (is_locked ? true : queuelists(xQueue));@*/ +{ + /*@open queuehandle(xQueue, N, M, is_isr);@*/ + mutex_acquire(xQueue->irqMask); + /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/ + return 0; +} + +void clearInterruptMaskFromISR(QueueHandle_t xQueue, UBaseType_t uxSavedInterruptStatus) +/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + [1/2]xQueue->irqMask |-> ?m &*& + mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*& + (is_locked ? true : queuelists(xQueue));@*/ +/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/ +{ + /*@close irqs_masked_invariant(xQueue, N, M, true)();@*/ + mutex_release(xQueue->irqMask); + /*@close [1/2]queuehandle(xQueue, N, M, true);@*/ +} + +#define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR(xQueue) +#define portCLEAR_INTERRUPT_MASK_FROM_ISR(uxSavedInterruptStatus) clearInterruptMaskFromISR(xQueue, uxSavedInterruptStatus) + +#endif /* QUEUE_H */ diff --git a/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h new file mode 100644 index 000000000..c590a6324 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h @@ -0,0 +1,57 @@ +/* + * FreeRTOS VeriFast Proofs + * Copyright (C) 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. + */ + +#ifndef QUEUECONTRACTS_H +#define QUEUECONTRACTS_H + +#include "queue.h" + +void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer ); +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& 0 < K &*& chars(pvBuffer, M, _);@*/ +/*@ensures queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs) &*& + chars(pvBuffer, M, head(abs));@*/ + +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ); +/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& + (K < N || xPosition == queueOVERWRITE) &*& + chars(pvItemToQueue, M, ?x) &*& + (xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/ +/*@ensures + (xPosition == queueSEND_TO_BACK + ? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))) + : (xPosition == queueSEND_TO_FRONT + ? (R == 0 + ? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs)) + : queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs))) + : xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x))) + ) &*& + chars(pvItemToQueue, M, x);@*/ + +BaseType_t prvIsQueueEmpty( Queue_t * pxQueue ); +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ + +BaseType_t prvIsQueueFull( Queue_t * pxQueue ); +/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ +/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ + +#endif /* QUEUECONTRACTS_H */ |