begriffs open source - cmsis-freertos/blob - Test/VeriFast/include/proof/list.h

   1 /*
   2  * FreeRTOS V202111.00
   3  * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
   6  * this software and associated documentation files (the "Software"), to deal in
   7  * the Software without restriction, including without limitation the rights to
   8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
   9  * the Software, and to permit persons to whom the Software is furnished to do so,
  10  * subject to the following conditions:
  11  *
  12  * The above copyright notice and this permission notice shall be included in all
  13  * copies or substantial portions of the Software.
  14  *
  15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
  17  * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
  18  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  21  *
  22  * https://www.FreeRTOS.org
  23  * https://github.com/FreeRTOS
  24  *
  25  */
  26
  27 #ifndef LIST_H
  28 #define LIST_H
  29
  30 #define VERIFAST
  31 #include <stdlib.h>
  32 #include <stdint.h>
  33 /*@#include "common.gh" */
  34
  35 typedef size_t    TickType_t;
  36 typedef size_t    UBaseType_t;
  37 typedef ssize_t   BaseType_t;
  38
  39 #define pdTRUE     1
  40 #define pdFALSE    0
  41
  42 /* Empty/no-op macros */
  43 #define mtCOVERAGE_TEST_MARKER()
  44 #define mtCOVERAGE_TEST_DELAY()
  45 #define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )
  46 #define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )
  47 #define listTEST_LIST_INTEGRITY( pxList )
  48 #define listTEST_LIST_ITEM_INTEGRITY( pxListItem )
  49 #define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
  50 #define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
  51
  52 /* Max value stored in sentinel xListEnd element */
  53 #define portMAX_DELAY    UINT_MAX
  54
  55 struct xLIST;
  56
  57 struct xLIST_ITEM
  58 {
  59     TickType_t xItemValue;
  60     struct xLIST_ITEM * pxNext;
  61     struct xLIST_ITEM * pxPrevious;
  62     void * pvOwner;
  63     struct xLIST * pxContainer;
  64 };
  65 typedef struct xLIST_ITEM ListItem_t;
  66
  67 typedef struct xLIST
  68 {
  69     UBaseType_t uxNumberOfItems;
  70     struct xLIST_ITEM * pxIndex;
  71     #ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
  72         struct xLIST_ITEM xListEnd;
  73     #else
  74         MiniListItem_t xListEnd;
  75     #endif
  76 } List_t;
  77
  78 /*@
  79  * predicate xLIST_ITEM(
  80  *  struct xLIST_ITEM *n,
  81  *  TickType_t xItemValue,
  82  *  struct xLIST_ITEM *pxNext,
  83  *  struct xLIST_ITEM *pxPrevious,
  84  *  struct xLIST *pxContainer;) =
  85  *  n->xItemValue |-> xItemValue &*&
  86  *  n->pxNext |-> pxNext &*&
  87  *  n->pxPrevious |-> pxPrevious &*&
  88  *  n->pvOwner |-> _ &*&
  89  *  n->pxContainer |-> pxContainer;
  90  * @*/
  91
  92 /* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
  93
  94 /*@
  95  * predicate DLS(
  96  *  struct xLIST_ITEM *n,
  97  *  struct xLIST_ITEM *nprev,
  98  *  struct xLIST_ITEM *mnext,
  99  *  struct xLIST_ITEM *m,
 100  *  list<struct xLIST_ITEM * > cells,
 101  *  list<TickType_t > vals,
 102  *  struct xLIST *pxContainer) =
 103  *  n == m
 104  *      ? cells == cons(n, nil) &*&
 105  *          vals == cons(?v, nil) &*&
 106  *          xLIST_ITEM(n, v, mnext, nprev, pxContainer)
 107  *      : cells == cons(n, ?cells0) &*&
 108  *          vals == cons(?v, ?vals0) &*&
 109  *          xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
 110  *
 111  * lemma void dls_star_item(
 112  *  struct xLIST_ITEM *n,
 113  *  struct xLIST_ITEM *m,
 114  *  struct xLIST_ITEM *o)
 115  * requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2);
 116  * ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
 117  * {
 118  *  open DLS(n, nprev, mnext, m, cells, vals, l);
 119  *  if (n == m) {
 120  *      assert xLIST_ITEM(n, _, _, _, _);
 121  *      open xLIST_ITEM(n, _, _, _, _);
 122  *      open xLIST_ITEM(o, _, _, _, _);
 123  *      assert n != o;
 124  *      close xLIST_ITEM(o, _, _, _, _);
 125  *      close xLIST_ITEM(n, _, _, _, _);
 126  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 127  *  }
 128  *  else {
 129  *      assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
 130  *      dls_star_item(nnext, m, o);
 131  *      open xLIST_ITEM(n, _, _, _, _);
 132  *      open xLIST_ITEM(o, _, _, _, _);
 133  *      assert n != o;
 134  *      close xLIST_ITEM(o, _, _, _, _);
 135  *      close xLIST_ITEM(n, _, _, _, _);
 136  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 137  *  }
 138  * }
 139  *
 140  * lemma void dls_distinct(
 141  *  struct xLIST_ITEM *n,
 142  *  struct xLIST_ITEM *nprev,
 143  *  struct xLIST_ITEM *mnext,
 144  *  struct xLIST_ITEM *m,
 145  *  list<struct xLIST_ITEM * > cells)
 146  * requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
 147  * ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
 148  * {
 149  *  if (n == m) {
 150  *      open DLS(n, nprev, mnext, m, cells, vals, l);
 151  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 152  *  } else {
 153  *      open DLS(n, nprev, mnext, m, cells, vals, l);
 154  *      assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
 155  *      dls_distinct(nnext, n, mnext, m, tail(cells));
 156  *      dls_star_item(nnext, m, n);
 157  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 158  *  }
 159  * }
 160  *
 161  * predicate xLIST(
 162  *  struct xLIST *l,
 163  *  int uxNumberOfItems,
 164  *  struct xLIST_ITEM *pxIndex,
 165  *  struct xLIST_ITEM *xListEnd,
 166  *  list<struct xLIST_ITEM *>cells,
 167  *  list<TickType_t >vals) =
 168  *  l->uxNumberOfItems |-> uxNumberOfItems &*&
 169  *  l->pxIndex |-> pxIndex &*&
 170  *  mem(pxIndex, cells) == true &*&
 171  *  xListEnd == &(l->xListEnd) &*&
 172  *  xListEnd == head(cells) &*&
 173  *  portMAX_DELAY == head(vals) &*&
 174  *  struct_xLIST_ITEM_padding(&l->xListEnd) &*&
 175  *  length(cells) == length(vals) &*&
 176  *  uxNumberOfItems + 1 == length(cells) &*&
 177  *  DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
 178  *
 179  * lemma void xLIST_distinct_cells(struct xLIST *l)
 180  * requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
 181  * ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
 182  * {
 183  *  open xLIST(l, n, idx, end, cells, vals);
 184  *  assert DLS(end, ?endprev, end, _, cells, vals, l);
 185  *  dls_distinct(end, endprev, end, endprev, cells);
 186  *  close xLIST(l, n, idx, end, cells, vals);
 187  * }
 188  *
 189  * lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
 190  * requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2);
 191  * ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false;
 192  * {
 193  *  open xLIST(l, n, idx, end, cells, vals);
 194  *  assert DLS(end, ?endprev, end, _, cells, vals, l);
 195  *  dls_distinct(end, endprev, end, endprev, cells);
 196  *  dls_star_item(end, endprev, x);
 197  *  close xLIST(l, n, idx, end, cells, vals);
 198  * }
 199  *
 200  * lemma void dls_first_mem(
 201  *  struct xLIST_ITEM *n,
 202  *  struct xLIST_ITEM *nprev,
 203  *  struct xLIST_ITEM *mnext,
 204  *  struct xLIST_ITEM *m,
 205  *  list<struct xLIST_ITEM * > cells)
 206  * requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
 207  * ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
 208  * {
 209  *  open DLS(n, nprev, mnext, m, cells, vals, l);
 210  *  if (n == m) {
 211  *      assert cells == cons(n, nil);
 212  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 213  *  } else {
 214  *      assert cells == cons(n, ?tail);
 215  *      close DLS(n, nprev, mnext, m, cells, vals, l);
 216  *  }
 217  * }
 218  *
 219  * lemma void dls_not_empty(
 220  *  struct xLIST_ITEM *n,
 221  *  struct xLIST_ITEM *m,
 222  *  list<struct xLIST_ITEM * > cells,
 223  *  struct xLIST_ITEM *x)
 224  * requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n;
 225  * ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
 226  * {
 227  *  open DLS(n, m, n, m, cells, vals, l);
 228  *  close DLS(n, m, n, m, cells, vals, l);
 229  * }
 230  *
 231  * lemma void dls_last_mem(
 232  *  struct xLIST_ITEM *n,
 233  *  struct xLIST_ITEM *nprev,
 234  *  struct xLIST_ITEM *mnext,
 235  *  struct xLIST_ITEM *m,
 236  *  list<struct xLIST_ITEM * > cells)
 237  * requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
 238  * ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
 239  * {
 240  *  open DLS(n, nprev, mnext, m, cells, vals, l);
 241  *  if (n == m) {
 242  *      // trivial
 243  *  } else {
 244  *      open xLIST_ITEM(n, _, ?nnext, _, l);
 245  *      assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l);
 246  *      dls_last_mem(o, n, mnext, m, tail(cells));
 247  *      close xLIST_ITEM(n, _, nnext, _, l);
 248  *  }
 249  *  close DLS(n, nprev, mnext, m, cells, vals, l);
 250  * }
 251  *
 252  * lemma void split(
 253  *  struct xLIST_ITEM *n,
 254  *  struct xLIST_ITEM *nprev,
 255  *  struct xLIST_ITEM *mnext,
 256  *  struct xLIST_ITEM *m,
 257  *  list<struct xLIST_ITEM * > cells,
 258  *  list<TickType_t > vals,
 259  *  struct xLIST_ITEM *x,
 260  *  int i)
 261  * requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
 262  * 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);
 263  * {
 264  *  open DLS(n, nprev, mnext, m, cells, vals, l);
 265  *  assert n != m;
 266  *  assert xLIST_ITEM(n, ?v, ?nnext, _, _);
 267  *  assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
 268  *  if (nnext == x) {
 269  *      close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
 270  *      open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
 271  *      open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
 272  *      close xLIST_ITEM(x, _, xnext, xprev, l);
 273  *      close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
 274  *  } else {
 275  *      assert nnext != x;
 276  *      split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
 277  *      assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
 278  *      dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
 279  *      dls_star_item(nnext, xprev, n);
 280  *      dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
 281  *      assert n != xprev;
 282  *      close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
 283  *  }
 284  * }
 285  *
 286  * lemma void join(
 287  *  struct xLIST_ITEM *n1,
 288  *  struct xLIST_ITEM *nprev1,
 289  *  struct xLIST_ITEM *mnext1,
 290  *  struct xLIST_ITEM *m1,
 291  *  list<struct xLIST_ITEM * > cells1,
 292  *  list<TickType_t > vals1,
 293  *  struct xLIST_ITEM *n2,
 294  *  struct xLIST_ITEM *nprev2,
 295  *  struct xLIST_ITEM *mnext2,
 296  *  struct xLIST_ITEM *m2,
 297  *  list<struct xLIST_ITEM * > cells2,
 298  *  list<TickType_t > vals2)
 299  * requires
 300  *  DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
 301  *  DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
 302  *  mnext1 == n2 &*& m1 == nprev2;
 303  * ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
 304  * {
 305  *  if (n1 == m1) {
 306  *      dls_first_mem(n1, nprev1, mnext1, m1, cells1);
 307  *      dls_last_mem(n2, nprev2, mnext2, m2, cells2);
 308  *      open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
 309  *      dls_star_item(n2, m2, n1);
 310  *      close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
 311  *  } else {
 312  *      open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
 313  *      assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
 314  *      join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
 315  *          n2, nprev2, mnext2, m2, cells2, vals2);
 316  *      assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
 317  *      dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
 318  *      dls_star_item(o, m2, n1);
 319  *      close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
 320  *  }
 321  * }
 322  *
 323  * lemma void idx_remains_in_list<t>(
 324  *  list<t> cells,
 325  *  t idx,
 326  *  t x,
 327  *  int ix)
 328  * requires
 329  *  idx != x &*&
 330  *  mem(idx, cells) == true &*&
 331  *  mem(x, cells) == true &*&
 332  *  index_of(x, cells) == ix;
 333  * ensures mem(idx, remove_nth(ix, cells)) == true;
 334  * {
 335  *  neq_mem_remove(idx, x, cells);
 336  *  remove_remove_nth(cells, x);
 337  * }
 338  * @*/
 339
 340 /* Following lemma from `verifast/examples/shared_boxes/concurrentqueue.c`.
 341  * Used in the uxListRemove proof to show that the item to remove `x` must
 342  * have value `nth(i, vals)` where `i == index_of(x, cells)`. */
 343
 344 /*@
 345  * lemma void drop_nth_index_of<t>(list<t> vs, int i)
 346  * requires
 347  *  0 <= i && i < length(vs);
 348  * ensures
 349  *  head(drop(i , vs)) == nth(i, vs);
 350  * {
 351  *  switch(vs) {
 352  *      case nil:
 353  *      case cons(h, t):
 354  *      if (i == 0) {
 355  *          // trivial
 356  *      } else {
 357  *          drop_nth_index_of(t, i - 1);
 358  *      }
 359  *  }
 360  * }
 361  * @*/
 362
 363 /*@
 364  * lemma void remove_append<t>(t x, list<t> l1, list<t> l2)
 365  *  requires mem(x, l1) == false;
 366  *  ensures remove(x, append(l1, l2)) == append(l1, remove(x, l2));
 367  * {
 368  *  switch(l1) {
 369  *      case nil:
 370  *      case cons(h1, t1):
 371  *          remove_append(x, t1, l2);
 372  *  }
 373  * }
 374  * @*/
 375
 376 #endif /* LIST_H */