begriffs open source - cmsis-freertos/blob - Test/VeriFast/list/vListInsert.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
  30 ListItem_t * choose( List_t * list );
  31 /*@ requires DLS(&(list->xListEnd), ?endprev, &(list->xListEnd), endprev, ?cells, ?vals, ?container);@*/
  32
  33 /*@ ensures DLS(&(list->xListEnd), endprev, &(list->xListEnd), endprev, cells, vals, container) &*&
  34  *  mem(result, cells) == true;@*/
  35
  36 void vListInsert( List_t * const pxList,
  37                   ListItem_t * const pxNewListItem )
  38
  39 /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
  40  *  xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/
  41
  42 /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
  43  *  remove(pxNewListItem, new_cells) == cells
  44  * ;@*/
  45 {
  46     /*@xLIST_star_item(pxList, pxNewListItem);@*/
  47     /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
  48     /*@open xLIST(pxList, len, idx, end, cells, vals);@*/
  49     /*@assert DLS(end, ?endprev, end, endprev, cells, vals, pxList);@*/
  50     ListItem_t * pxIterator;
  51     const TickType_t xValueOfInsertion = pxNewListItem->xItemValue;
  52
  53     /* Only effective when configASSERT() is also defined, these tests may catch
  54      * the list data structures being overwritten in memory.  They will not catch
  55      * data errors caused by incorrect configuration or use of FreeRTOS. */
  56     listTEST_LIST_INTEGRITY( pxList );
  57     listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );
  58
  59     /* Insert the new list item into the list, sorted in xItemValue order.
  60      *
  61      * If the list already contains a list item with the same item value then the
  62      * new list item should be placed after it.  This ensures that TCBs which are
  63      * stored in ready lists (all of which have the same xItemValue value) get a
  64      * share of the CPU.  However, if the xItemValue is the same as the back marker
  65      * the iteration loop below will not end.  Therefore the value is checked
  66      * first, and the algorithm slightly modified if necessary. */
  67     if( xValueOfInsertion == portMAX_DELAY )
  68     {
  69         /*@open DLS(end, endprev, end, endprev, cells, vals, pxList);@*/
  70         /*@open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);@*/
  71
  72         /*@
  73          * if (end != endprev)
  74          * {
  75          *  assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
  76          *  if (endnext == endprev)
  77          *  {
  78          *      // done
  79          *  }
  80          *  else
  81          *  {
  82          *      dls_last_mem(endnext, end, end, endprev, tail(cells));
  83          *      split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
  84          *  }
  85          *  open DLS(endprev, _, _, _, _, _, _);
  86          *  open xLIST_ITEM(endprev, _, _, _, _);
  87          * }
  88          * @*/
  89         pxIterator = pxList->xListEnd.pxPrevious;
  90     }
  91     else
  92     {
  93         /* *** NOTE ***********************************************************
  94         *  If you find your application is crashing here then likely causes are
  95         *  listed below.  In addition see https://www.FreeRTOS.org/FAQHelp.html for
  96         *  more tips, and ensure configASSERT() is defined!
  97         *  https://www.FreeRTOS.org/a00110.html#configASSERT
  98         *
  99         *   1) Stack overflow -
 100         *      see https://www.FreeRTOS.org/Stacks-and-stack-overflow-checking.html
 101         *   2) Incorrect interrupt priority assignment, especially on Cortex-M
 102         *      parts where numerically high priority values denote low actual
 103         *      interrupt priorities, which can seem counter intuitive.  See
 104         *      https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html and the definition
 105         *      of configMAX_SYSCALL_INTERRUPT_PRIORITY on
 106         *      https://www.FreeRTOS.org/a00110.html
 107         *   3) Calling an API function from within a critical section or when
 108         *      the scheduler is suspended, or calling an API function that does
 109         *      not end in "FromISR" from an interrupt.
 110         *   4) Using a queue or semaphore before it has been initialised or
 111         *      before the scheduler has been started (are interrupts firing
 112         *      before vTaskStartScheduler() has been called?).
 113         **********************************************************************/
 114
 115         #ifdef VERIFAST /*< ***over-approximate list insert loop*** */
 116             pxIterator = choose( pxList );
 117         #else
 118             for( pxIterator = ( ListItem_t * ) &( pxList->xListEnd ); pxIterator->pxNext->xItemValue <= xValueOfInsertion; pxIterator = pxIterator->pxNext ) /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM.  This is checked and valid. *//*lint !e440 The iterator moves to a different value, not xValueOfInsertion. */
 119             {
 120                 /* There is nothing to do here, just iterating to the wanted
 121                  * insertion position. */
 122             }
 123         #endif
 124         /*@int i = index_of(pxIterator, cells);@*/
 125
 126         /*@
 127          * if (pxIterator == end)
 128          * {
 129          *  open DLS(end, endprev, end, endprev, cells, vals, pxList);
 130          *  open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
 131          *  if (end != endprev)
 132          *  {
 133          *      assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
 134          *      open DLS(endnext, _, _, _, _, _, _);
 135          *      open xLIST_ITEM(endnext, _, _, _, _);
 136          *  }
 137          * }
 138          * else
 139          * {
 140          *  assert DLS(end, endprev, end, endprev, cells, vals, pxList);
 141          *  dls_first_mem(end, endprev, end, endprev, cells);
 142          *  assert pxIterator != end;
 143          *  assert index_of(end, cells) == 0;
 144          *  split(end, endprev, end, endprev, cells, vals, pxIterator, i);
 145          *  assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList);
 146          *  assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
 147          *  open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
 148          *  open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList);
 149          *  if (pxIterator == endprev)
 150          *  {
 151          *      open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
 152          *      take_take(1, i, vals);
 153          *      assert xLIST_ITEM(end, portMAX_DELAY, _, _, _);
 154          *      open xLIST_ITEM(iternext, _, _, pxIterator, _);
 155          *  }
 156          *  else
 157          *  {
 158          *      open DLS(iternext, pxIterator, end, endprev, _, _, _);
 159          *      open xLIST_ITEM(iternext, _, _, pxIterator, _);
 160          *  }
 161          * }@*/
 162     }
 163
 164     pxNewListItem->pxNext = pxIterator->pxNext;
 165     pxNewListItem->pxNext->pxPrevious = pxNewListItem;
 166     pxNewListItem->pxPrevious = pxIterator;
 167     pxIterator->pxNext = pxNewListItem;
 168
 169     /* Remember which list the item is in.  This allows fast removal of the
 170      * item later. */
 171     pxNewListItem->pxContainer = pxList;
 172
 173     ( pxList->uxNumberOfItems )++;
 174
 175     /*@close xLIST_ITEM(pxNewListItem, val, ?iternext, pxIterator, pxList);@*/
 176     /*@close xLIST_ITEM(pxIterator, ?iterval, pxNewListItem, ?iterprev, pxList);@*/
 177
 178     /*@
 179      * if( xValueOfInsertion == portMAX_DELAY )
 180      * {
 181      *  assert iternext == end;
 182      *  assert pxIterator == endprev;
 183      *  if (end == endprev)
 184      *  {
 185      *      close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
 186      *      close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
 187      *      join(end, pxNewListItem, pxNewListItem, end, cells, vals,
 188      *          pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
 189      *      close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
 190      *  }
 191      *  else
 192      *  {
 193      *      close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
 194      *      close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
 195      *      if (endnext == endprev)
 196      *      {
 197      *          assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList);
 198      *          close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList);
 199      *          close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList);
 200      *          join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY),
 201      *              endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval));
 202      *          assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList);
 203      *      }
 204      *      else
 205      *      {
 206      *          assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
 207      *          assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells));
 208      *          assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1;
 209      *          assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells));
 210      *          assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList);
 211      *          close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
 212      *          dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev);
 213      *          dls_star_item(endnext, endprevprev, end);
 214      *          close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList);
 215      *          join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev),
 216      *              endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
 217      *          assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
 218      *
 219      *      }
 220      *      join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
 221      *          pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
 222      *      remove_append(pxNewListItem, cells, singleton(pxNewListItem));
 223      *      close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
 224      *  }
 225      * }
 226      * else
 227      * {
 228      *  if (pxIterator == end)
 229      *  {
 230      *      if (iternext == end)
 231      *      {
 232      *          close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
 233      *          close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
 234      *          join(end, pxNewListItem, pxNewListItem, end, cells, vals,
 235      *              pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
 236      *          close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
 237      *      }
 238      *      else
 239      *      {
 240      *          close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
 241      *          if (iternext == endprev)
 242      *          {
 243      *              close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
 244      *              dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext));
 245      *          }
 246      *          else
 247      *          {
 248      *              assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList);
 249      *              close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList);
 250      *              dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev));
 251      *          }
 252      *          close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
 253      *          assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList);
 254      *          dls_star_item(iternext, endprev, pxNewListItem);
 255      *          close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList);
 256      *          join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY),
 257      *              pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev));
 258      *          close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev)));
 259      *      }
 260      *  }
 261      *  else
 262      *  {
 263      *      close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
 264      *      if (pxIterator == endprev)
 265      *      {
 266      *          if (iterprev == end)
 267      *          {
 268      *              close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList);
 269      *          }
 270      *          else
 271      *          {
 272      *              assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _);
 273      *              close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList);
 274      *          }
 275      *          int i = index_of(pxIterator, cells);
 276      *          assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
 277      *          close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList);
 278      *          close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
 279      *          join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals),
 280      *              pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals));
 281      *          join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals,
 282      *              pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
 283      *          close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
 284      *          remove_append(pxNewListItem, cells, singleton(pxNewListItem));
 285      *      }
 286      *      else
 287      *      {
 288      *          int i = index_of(pxIterator, cells);
 289      *          if (iternext == endprev)
 290      *          {
 291      *              close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
 292      *          }
 293      *          else
 294      *          {
 295      *              assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList);
 296      *              dls_star_item(end, iterprev, iternext);
 297      *              close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList);
 298      *          }
 299      *          drop_drop(1, i, cells);
 300      *          drop_drop(1, i, vals);
 301      *          assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList);
 302      *          assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
 303      *          dls_star_item(iternext, endprev, pxNewListItem);
 304      *          dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells));
 305      *          close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList);
 306      *          close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList);
 307      *          join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals),
 308      *              pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))));
 309      *          list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
 310      *          list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
 311      *          head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
 312      *          take_head(take(i, cells));
 313      *          take_take(1, i, cells);
 314      *          assert( end == head(new_cells) );
 315      *          head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
 316      *          take_head(take(i, vals));
 317      *          take_take(1, i, vals);
 318      *          assert( portMAX_DELAY == head(new_vals) );
 319      *          append_take_drop_n(cells, index_of(pxIterator, cells));
 320      *          close xLIST(pxList, len+1, idx, end, append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))), append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))));
 321      *          mem_take_false(pxNewListItem, i, cells);
 322      *          remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
 323      *      }
 324      *  }
 325      * }@*/
 326 }