/*
 * FreeRTOS V202111.00
 * 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.
 *
 * https://www.FreeRTOS.org
 * https://github.com/FreeRTOS
 *
 */

#include "proof/list.h"


ListItem_t * choose( List_t * list );
/*@ requires DLS(&(list->xListEnd), ?endprev, &(list->xListEnd), endprev, ?cells, ?vals, ?container);@*/

/*@ ensures DLS(&(list->xListEnd), endprev, &(list->xListEnd), endprev, cells, vals, container) &*&
 *  mem(result, cells) == true;@*/

void vListInsert( List_t * const pxList,
                  ListItem_t * const pxNewListItem )

/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
 *  xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/

/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
 *  remove(pxNewListItem, new_cells) == cells
 * ;@*/
{
    /*@xLIST_star_item(pxList, pxNewListItem);@*/
    /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
    /*@open xLIST(pxList, len, idx, end, cells, vals);@*/
    /*@assert DLS(end, ?endprev, end, endprev, cells, vals, pxList);@*/
    ListItem_t * pxIterator;
    const TickType_t xValueOfInsertion = pxNewListItem->xItemValue;

    /* Only effective when configASSERT() is also defined, these tests may catch
     * the list data structures being overwritten in memory.  They will not catch
     * data errors caused by incorrect configuration or use of FreeRTOS. */
    listTEST_LIST_INTEGRITY( pxList );
    listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );

    /* Insert the new list item into the list, sorted in xItemValue order.
     *
     * If the list already contains a list item with the same item value then the
     * new list item should be placed after it.  This ensures that TCBs which are
     * stored in ready lists (all of which have the same xItemValue value) get a
     * share of the CPU.  However, if the xItemValue is the same as the back marker
     * the iteration loop below will not end.  Therefore the value is checked
     * first, and the algorithm slightly modified if necessary. */
    if( xValueOfInsertion == portMAX_DELAY )
    {
        /*@open DLS(end, endprev, end, endprev, cells, vals, pxList);@*/
        /*@open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);@*/

        /*@
         * if (end != endprev)
         * {
         *  assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
         *  if (endnext == endprev)
         *  {
         *      // done
         *  }
         *  else
         *  {
         *      dls_last_mem(endnext, end, end, endprev, tail(cells));
         *      split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
         *  }
         *  open DLS(endprev, _, _, _, _, _, _);
         *  open xLIST_ITEM(endprev, _, _, _, _);
         * }
         * @*/
        pxIterator = pxList->xListEnd.pxPrevious;
    }
    else
    {
        /* *** NOTE ***********************************************************
        *  If you find your application is crashing here then likely causes are
        *  listed below.  In addition see https://www.FreeRTOS.org/FAQHelp.html for
        *  more tips, and ensure configASSERT() is defined!
        *  https://www.FreeRTOS.org/a00110.html#configASSERT
        *
        *   1) Stack overflow -
        *      see https://www.FreeRTOS.org/Stacks-and-stack-overflow-checking.html
        *   2) Incorrect interrupt priority assignment, especially on Cortex-M
        *      parts where numerically high priority values denote low actual
        *      interrupt priorities, which can seem counter intuitive.  See
        *      https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html and the definition
        *      of configMAX_SYSCALL_INTERRUPT_PRIORITY on
        *      https://www.FreeRTOS.org/a00110.html
        *   3) Calling an API function from within a critical section or when
        *      the scheduler is suspended, or calling an API function that does
        *      not end in "FromISR" from an interrupt.
        *   4) Using a queue or semaphore before it has been initialised or
        *      before the scheduler has been started (are interrupts firing
        *      before vTaskStartScheduler() has been called?).
        **********************************************************************/

        #ifdef VERIFAST /*< ***over-approximate list insert loop*** */
            pxIterator = choose( pxList );
        #else
            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. */
            {
                /* There is nothing to do here, just iterating to the wanted
                 * insertion position. */
            }
        #endif
        /*@int i = index_of(pxIterator, cells);@*/

        /*@
         * if (pxIterator == end)
         * {
         *  open DLS(end, endprev, end, endprev, cells, vals, pxList);
         *  open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
         *  if (end != endprev)
         *  {
         *      assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
         *      open DLS(endnext, _, _, _, _, _, _);
         *      open xLIST_ITEM(endnext, _, _, _, _);
         *  }
         * }
         * else
         * {
         *  assert DLS(end, endprev, end, endprev, cells, vals, pxList);
         *  dls_first_mem(end, endprev, end, endprev, cells);
         *  assert pxIterator != end;
         *  assert index_of(end, cells) == 0;
         *  split(end, endprev, end, endprev, cells, vals, pxIterator, i);
         *  assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList);
         *  assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
         *  open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
         *  open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList);
         *  if (pxIterator == endprev)
         *  {
         *      open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
         *      take_take(1, i, vals);
         *      assert xLIST_ITEM(end, portMAX_DELAY, _, _, _);
         *      open xLIST_ITEM(iternext, _, _, pxIterator, _);
         *  }
         *  else
         *  {
         *      open DLS(iternext, pxIterator, end, endprev, _, _, _);
         *      open xLIST_ITEM(iternext, _, _, pxIterator, _);
         *  }
         * }@*/
    }

    pxNewListItem->pxNext = pxIterator->pxNext;
    pxNewListItem->pxNext->pxPrevious = pxNewListItem;
    pxNewListItem->pxPrevious = pxIterator;
    pxIterator->pxNext = pxNewListItem;

    /* Remember which list the item is in.  This allows fast removal of the
     * item later. */
    pxNewListItem->pxContainer = pxList;

    ( pxList->uxNumberOfItems )++;

    /*@close xLIST_ITEM(pxNewListItem, val, ?iternext, pxIterator, pxList);@*/
    /*@close xLIST_ITEM(pxIterator, ?iterval, pxNewListItem, ?iterprev, pxList);@*/

    /*@
     * if( xValueOfInsertion == portMAX_DELAY )
     * {
     *  assert iternext == end;
     *  assert pxIterator == endprev;
     *  if (end == endprev)
     *  {
     *      close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
     *      close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
     *      join(end, pxNewListItem, pxNewListItem, end, cells, vals,
     *          pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
     *      close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
     *  }
     *  else
     *  {
     *      close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
     *      close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
     *      if (endnext == endprev)
     *      {
     *          assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList);
     *          close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList);
     *          close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList);
     *          join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY),
     *              endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval));
     *          assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList);
     *      }
     *      else
     *      {
     *          assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
     *          assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells));
     *          assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1;
     *          assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells));
     *          assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList);
     *          close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
     *          dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev);
     *          dls_star_item(endnext, endprevprev, end);
     *          close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList);
     *          join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev),
     *              endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
     *          assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
     *
     *      }
     *      join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
     *          pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
     *      remove_append(pxNewListItem, cells, singleton(pxNewListItem));
     *      close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
     *  }
     * }
     * else
     * {
     *  if (pxIterator == end)
     *  {
     *      if (iternext == end)
     *      {
     *          close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
     *          close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
     *          join(end, pxNewListItem, pxNewListItem, end, cells, vals,
     *              pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
     *          close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
     *      }
     *      else
     *      {
     *          close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
     *          if (iternext == endprev)
     *          {
     *              close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
     *              dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext));
     *          }
     *          else
     *          {
     *              assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList);
     *              close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList);
     *              dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev));
     *          }
     *          close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
     *          assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList);
     *          dls_star_item(iternext, endprev, pxNewListItem);
     *          close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList);
     *          join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY),
     *              pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev));
     *          close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev)));
     *      }
     *  }
     *  else
     *  {
     *      close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
     *      if (pxIterator == endprev)
     *      {
     *          if (iterprev == end)
     *          {
     *              close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList);
     *          }
     *          else
     *          {
     *              assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _);
     *              close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList);
     *          }
     *          int i = index_of(pxIterator, cells);
     *          assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
     *          close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList);
     *          close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
     *          join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals),
     *              pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals));
     *          join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals,
     *              pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
     *          close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
     *          remove_append(pxNewListItem, cells, singleton(pxNewListItem));
     *      }
     *      else
     *      {
     *          int i = index_of(pxIterator, cells);
     *          if (iternext == endprev)
     *          {
     *              close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
     *          }
     *          else
     *          {
     *              assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList);
     *              dls_star_item(end, iterprev, iternext);
     *              close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList);
     *          }
     *          drop_drop(1, i, cells);
     *          drop_drop(1, i, vals);
     *          assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList);
     *          assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
     *          dls_star_item(iternext, endprev, pxNewListItem);
     *          dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells));
     *          close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList);
     *          close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList);
     *          join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals),
     *              pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))));
     *          list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
     *          list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
     *          head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
     *          take_head(take(i, cells));
     *          take_take(1, i, cells);
     *          assert( end == head(new_cells) );
     *          head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
     *          take_head(take(i, vals));
     *          take_take(1, i, vals);
     *          assert( portMAX_DELAY == head(new_vals) );
     *          append_take_drop_n(cells, index_of(pxIterator, cells));
     *          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)))));
     *          mem_take_false(pxNewListItem, i, cells);
     *          remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
     *      }
     *  }
     * }@*/
}