begriffs open source - cmsis-freertos/blob - Test/VeriFast/list/uxListRemove.c

   1 /*
   2  * FreeRTOS V202107.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 #include "proof/list.h"
  28
  29 UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
  30
  31 /*@requires
  32  *  exists<struct xLIST * >(?l) &*&
  33  *  xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
  34  *  end != pxItemToRemove &*&
  35  *  mem(pxItemToRemove, cells) == true;@*/
  36
  37 /*@ensures
  38  *  result == len-1 &*&
  39  *  xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, NULL) &*&
  40  *  pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*&
  41  *  xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx,  end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals));@*/
  42 {
  43     /* For brevity we alias x to pxItemToRemove */
  44     /*@struct xLIST_ITEM *x = pxItemToRemove;@*/
  45
  46     /* Start by establishing that the list must be non-empty since x != end */
  47     /*@open xLIST(l, len, idx, end, cells, vals);@*/
  48     /*@assert DLS(end, ?endprev, end, _, cells, vals, l);@*/
  49     /*@assert vals == cons(portMAX_DELAY, _);@*/
  50     /*@dls_not_empty(end, endprev, cells, x);@*/
  51
  52     /* We know the xLIST is a DLS: end...endprev
  53      * Split this into DLS1:end...xprev and DLS2:x...endprev */
  54     /*@int i = index_of(x, cells);@*/
  55     /*@split(end, endprev, end, endprev, cells, vals, x, i);@*/
  56     /*@list<struct xLIST_ITEM *> ys = take(i, cells);@*/
  57     /*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
  58     /*@list<TickType_t> vs = take(i, vals);@*/
  59     /*@list<TickType_t> ws = drop(i, vals);@*/
  60     /*@assert length(ys) == length(vs);@*/
  61     /*@assert length(zs) == length(ws);@*/
  62     /*@assert DLS(end, endprev, x, ?xprev, ys, vs, l);@*/ /*< DLS1 (ys, vs) */
  63     /*@assert DLS(x, xprev, end, endprev, zs, ws, l);@*/  /*< DLS2 (zs, ws) */
  64
  65     /* Now case split to open DLS1 and DLS2 appropriately */
  66
  67     /*@
  68      * if (end == xprev)
  69      * {
  70      *  if (x == endprev)
  71      *  {
  72      *      //Case A
  73      *      //DLS1: extract end=prev=next
  74      *      open DLS(end, endprev, x, xprev, ys, vs, l);
  75      *      open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
  76      *      //DLS2: extract x
  77      *      open DLS(x, xprev, end, endprev, zs, ws, l);
  78      *      //Lengths
  79      *      assert length(ys) == 1;
  80      *      assert length(zs) == 1;
  81      *  }
  82      *  else
  83      *  {
  84      *      //Case B
  85      *      //DLS1: extract end=prev
  86      *      open DLS(end, endprev, x, xprev, ys, vs, l);
  87      *      open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
  88      *      //DLS2: extract next and x
  89      *      open DLS(x, end, end, endprev, zs, ws, l);
  90      *      assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), l);
  91      *      open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
  92      *      open xLIST_ITEM(xnext, _, _, x, l);
  93      *      //Lengths
  94      *      assert length(ys) == 1;
  95      *  }
  96      * }
  97      * else
  98      * {
  99      *  if (x == endprev)
 100      *  {
 101      *      //Case C
 102      *      //DLS1: extract end=next and prev
 103      *      dls_last_mem(end, endprev, x, xprev, ys);
 104      *      assert mem(xprev, ys) == true;
 105      *      open DLS(end, endprev, x, xprev, ys, vs, l);
 106      *      open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
 107      *      if (endnext == xprev)
 108      *      {
 109      *          open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
 110      *          open xLIST_ITEM(xprev, _, x, _, l);
 111      *      }
 112      *      else
 113      *      {
 114      *          assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
 115      *          int k = index_of(xprev, tail(ys));
 116      *          dls_last_mem(endnext, end, x, xprev, tail(ys));
 117      *          split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
 118      *          open DLS(xprev, _, x, xprev, _, _, l);
 119      *          open xLIST_ITEM(xprev, _, x, _, l);
 120      *      }
 121      *      //DLS2: extract x
 122      *      open DLS(x, xprev, end, endprev, zs, ws, l);
 123      *      //Lengths
 124      *      assert length(zs) == 1;
 125      *  }
 126      *  else
 127      *  {
 128      *      //Case D
 129      *      //DLS1: extract prev
 130      *      dls_last_mem(end, endprev, x, xprev, ys);
 131      *      int j = index_of(xprev, ys);
 132      *      open DLS(end, endprev, x, xprev, ys, vs, l);
 133      *      open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
 134      *      if (endnext == xprev)
 135      *      {
 136      *          open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
 137      *          assert tail(ys) == singleton(xprev);
 138      *          open xLIST_ITEM(xprev, _, x, _, l);
 139      *      }
 140      *      else
 141      *      {
 142      *          assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
 143      *          int k = index_of(xprev, tail(ys));
 144      *          dls_last_mem(endnext, end, x, xprev, tail(ys));
 145      *          split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
 146      *          open DLS(xprev, _, x, xprev, _, _, l);
 147      *          open xLIST_ITEM(xprev, _, x, _, l);
 148      *      }
 149      *      //DLS2: extract next and x
 150      *      open DLS(x, xprev, end, endprev, zs, ws, l);
 151      *      assert xLIST_ITEM(x, _, ?xnext, _, l);
 152      *      open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
 153      *      open xLIST_ITEM(xnext, _, _, x, l);
 154      *  }
 155      * }
 156      * @*/
 157     /*@drop_nth_index_of(vals, i);@*/
 158     /*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, l);@*/
 159
 160 /* The list item knows which list it is in.  Obtain the list from the list
 161  * item. */
 162     #ifdef VERIFAST /*< const pointer declaration */
 163         List_t * pxList = pxItemToRemove->pxContainer;
 164     #else
 165         List_t * const pxList = pxItemToRemove->pxContainer;
 166     #endif
 167
 168     pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
 169     pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
 170
 171     /* Only used during decision coverage testing. */
 172     mtCOVERAGE_TEST_DELAY();
 173
 174     /* Make sure the index is left pointing to a valid item. */
 175     if( pxList->pxIndex == pxItemToRemove )
 176     {
 177         pxList->pxIndex = pxItemToRemove->pxPrevious;
 178     }
 179     else
 180     {
 181         mtCOVERAGE_TEST_MARKER();
 182     }
 183
 184     pxItemToRemove->pxContainer = NULL;
 185     ( pxList->uxNumberOfItems )--;
 186
 187     return pxList->uxNumberOfItems;
 188
 189     /*@
 190      * // Reassemble DLS1 and a modified DLS2, which no longer includes x
 191      * if (end == xprev)
 192      * {
 193      *  if (x == endprev)
 194      *  {
 195      *      //Case A
 196      *      close xLIST_ITEM(end, portMAX_DELAY, _, _, _);
 197      *      close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), l);
 198      *  }
 199      *  else
 200      *  {
 201      *      //Case B
 202      *      close xLIST_ITEM(xprev, _, xnext, endprev, l);
 203      *      close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), l);
 204      *      close xLIST_ITEM(xnext, _, _, xprev, l);
 205      *      close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
 206      *      join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY),
 207      *           xnext, xprev, end, endprev, tail(zs), tail(ws));
 208      *  }
 209      * }
 210      * else
 211      * {
 212      *  if (x == endprev)
 213      *  {
 214      *      //Case C
 215      *      close xLIST_ITEM(end, _, ?endnext, xprev, l);
 216      *      close xLIST_ITEM(xprev, ?xprev_val, end, _, l);
 217      *      if (endnext == xprev)
 218      *      {
 219      *          close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), l);
 220      *          close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), l);
 221      *      }
 222      *      else
 223      *      {
 224      *          close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
 225      *          assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
 226      *          join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
 227      *               xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
 228      *          close DLS(end, xprev, end, xprev, ys, vs, l);
 229      *      }
 230      *  }
 231      *  else
 232      *  {
 233      *      //Case D
 234      *      close xLIST_ITEM(xnext, _, ?xnextnext, xprev, l);
 235      *      close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
 236      *      close xLIST_ITEM(end, _, ?endnext, endprev, l);
 237      *      close xLIST_ITEM(xprev, ?xprev_val, xnext, _, l);
 238      *      if (endnext == xprev)
 239      *      {
 240      *          close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
 241      *          close DLS(end, endprev, xnext, xprev, ys, vs, l);
 242      *          join(end, endprev, xnext, xprev, ys, vs,
 243      *               xnext, xprev, end, endprev, tail(zs), tail(ws));
 244      *      }
 245      *      else
 246      *      {
 247      *          close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
 248      *          assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
 249      *          join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
 250      *               xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
 251      *          close DLS(end, endprev, xnext, xprev, ys, vs, l);
 252      *          join(end, endprev, xnext, xprev, ys, vs,
 253      *               xnext, xprev, end, endprev, tail(zs), tail(ws));
 254      *      }
 255      *  }
 256      * }
 257      * @*/
 258     /*@remove_remove_nth(cells, x);@*/
 259
 260     /*@
 261      * if (idx == x)
 262      * {
 263      *  close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)));
 264      * }
 265      * else
 266      * {
 267      *  idx_remains_in_list(cells, idx, x, i);
 268      *  close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)));
 269      * }
 270      * @*/
 271     /*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, NULL);@*/
 272 }
 273
 274 ListItem_t * client_example( List_t * l )
 275
 276 /*@requires
 277  *  xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
 278  *  idx != end &*&
 279  *  cells == cons(end, cons(idx, ?cells_tl)) &*&
 280  *  vals == cons(portMAX_DELAY, cons(42, ?vals_tl));@*/
 281
 282 /*@ensures
 283  *  xLIST(l, len - 1, _, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
 284  *  xLIST_ITEM(result, 42, _, _, NULL);@*/
 285 {
 286     /*@open xLIST(l, len, idx, end, cells, vals);@*/
 287     ListItem_t * index = l->pxIndex;
 288
 289     /*@close xLIST(l, len, idx, end, cells, vals);@*/
 290     /*@close exists(l);@*/
 291     uxListRemove( index );
 292     return index;
 293 }
 294
 295 void client_example2( List_t * l )
 296
 297 /*@requires
 298  *  xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
 299  *  cells == cons(end, cons(?x1, cons(?x2, ?cells_tl))) &*&
 300  *  idx == x2 &*&
 301  *  vals == cons(portMAX_DELAY, cons(1, cons(2, ?vals_tl)));@*/
 302
 303 /*@ensures
 304  *  xLIST(l, len-2, end, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
 305  *  xLIST_ITEM(_, 1, _, _, NULL) &*&
 306  *  xLIST_ITEM(_, 2, _, _, NULL);@*/
 307 {
 308     /*@xLIST_distinct_cells(l);@*/
 309     /*@open xLIST(l, len, idx, end, cells, vals);@*/
 310     ListItem_t * index = l->pxIndex;
 311
 312     /*@close xLIST(l, len, idx, end, cells, vals);@*/
 313     /*@close exists(l);@*/
 314     uxListRemove( index );
 315     /*@open xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
 316     index = l->pxIndex;
 317     /*@close xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
 318     /*@close exists(l);@*/
 319     uxListRemove( index );
 320 }