Copied modified source and header files to proof subdirectory.

Test/VeriFast/tasks/vTaskSwitchContext/include/list.h

@@ -0,0 +1,453 @@
+/*
+ * FreeRTOS SMP Kernel V202110.00
+ * Copyright (C) 2020 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
+ *
+ */
+
+/*
+ * This is the list implementation used by the scheduler.  While it is tailored
+ * heavily for the schedulers needs, it is also available for use by
+ * application code.
+ *
+ * list_ts can only store pointers to list_item_ts.  Each ListItem_t contains a
+ * numeric value (xItemValue).  Most of the time the lists are sorted in
+ * descending item value order.
+ *
+ * Lists are created already containing one list item.  The value of this
+ * item is the maximum possible that can be stored, it is therefore always at
+ * the end of the list and acts as a marker.  The list member pxHead always
+ * points to this marker - even though it is at the tail of the list.  This
+ * is because the tail contains a wrap back pointer to the true head of
+ * the list.
+ *
+ * In addition to it's value, each list item contains a pointer to the next
+ * item in the list (pxNext), a pointer to the list it is in (pxContainer)
+ * and a pointer to back to the object that contains it.  These later two
+ * pointers are included for efficiency of list manipulation.  There is
+ * effectively a two way link between the object containing the list item and
+ * the list item itself.
+ *
+ *
+ * \page ListIntroduction List Implementation
+ * \ingroup FreeRTOSIntro
+ */
+
+
+#ifndef LIST_H
+#define LIST_H
+
+
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * VeriFast bug:
+     * Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H`
+     * evaluate to true. See minimal example `define_name`.
+     */
+    #define INC_FREERTOS_H
+    /* Remember that this header is included indirectly `tasks.c` after it
+     * includes `FreeRTOS.h`.
+     */
+    // TODO: Remove this work-around once VF has been fixed.
+#endif /* VERIFAST */
+
+#ifndef INC_FREERTOS_H
+    #error "FreeRTOS.h must be included before list.h"
+#endif
+
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * VeriFast's normal and context-free preprocessor consume different
+     * numbers of tokens when expanding `PRIVILEGED_FUNCTION` in this file.
+     */
+    #define PRIVILEGED_FUNCTION
+    // TODO: Figure out why the preprocessors consume different amounts of
+    //       of tokens. This most likely has to do with the path/context
+    //       from which this header is included.
+#endif /* VERIFAST */
+
+/*
+ * The list structure members are modified from within interrupts, and therefore
+ * by rights should be declared volatile.  However, they are only modified in a
+ * functionally atomic way (within critical sections of with the scheduler
+ * suspended) and are either passed by reference into a function or indexed via
+ * a volatile variable.  Therefore, in all use cases tested so far, the volatile
+ * qualifier can be omitted in order to provide a moderate performance
+ * improvement without adversely affecting functional behaviour.  The assembly
+ * instructions generated by the IAR, ARM and GCC compilers when the respective
+ * compiler's options were set for maximum optimisation has been inspected and
+ * deemed to be as intended.  That said, as compiler technology advances, and
+ * especially if aggressive cross module optimisation is used (a use case that
+ * has not been exercised to any great extend) then it is feasible that the
+ * volatile qualifier will be needed for correct optimisation.  It is expected
+ * that a compiler removing essential code because, without the volatile
+ * qualifier on the list structure members and with aggressive cross module
+ * optimisation, the compiler deemed the code unnecessary will result in
+ * complete and obvious failure of the scheduler.  If this is ever experienced
+ * then the volatile qualifier can be inserted in the relevant places within the
+ * list structures by simply defining configLIST_VOLATILE to volatile in
+ * FreeRTOSConfig.h (as per the example at the bottom of this comment block).
+ * If configLIST_VOLATILE is not defined then the preprocessor directives below
+ * will simply #define configLIST_VOLATILE away completely.
+ *
+ * To use volatile list structure members then add the following line to
+ * FreeRTOSConfig.h (without the quotes):
+ * "#define configLIST_VOLATILE volatile"
+ */
+#ifndef configLIST_VOLATILE
+    #define configLIST_VOLATILE
+#endif /* configSUPPORT_CROSS_MODULE_OPTIMISATION */
+
+/* *INDENT-OFF* */
+#ifdef __cplusplus
+    extern "C" {
+#endif
+/* *INDENT-ON* */
+
+/* Macros that can be used to place known values within the list structures,
+ * then check that the known values do not get corrupted during the execution of
+ * the application.   These may catch the list data structures being overwritten in
+ * memory.  They will not catch data errors caused by incorrect configuration or
+ * use of FreeRTOS.*/
+#if ( configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES == 0 )
+    /* Define the macros to do nothing. */
+    #define listFIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE
+    #define listSECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE
+    #define listFIRST_LIST_INTEGRITY_CHECK_VALUE
+    #define listSECOND_LIST_INTEGRITY_CHECK_VALUE
+    #define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem )
+    #define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem )
+    #define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )
+    #define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )
+    #define listTEST_LIST_ITEM_INTEGRITY( pxItem )
+    #define listTEST_LIST_INTEGRITY( pxList )
+#else /* if ( configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES == 0 ) */
+    /* Define macros that add new members into the list structures. */
+    #define listFIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE     TickType_t xListItemIntegrityValue1;
+    #define listSECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE    TickType_t xListItemIntegrityValue2;
+    #define listFIRST_LIST_INTEGRITY_CHECK_VALUE          TickType_t xListIntegrityValue1;
+    #define listSECOND_LIST_INTEGRITY_CHECK_VALUE         TickType_t xListIntegrityValue2;
+
+/* Define macros that set the new structure members to known values. */
+    #define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem )     ( pxItem )->xListItemIntegrityValue1 = pdINTEGRITY_CHECK_VALUE
+    #define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem )    ( pxItem )->xListItemIntegrityValue2 = pdINTEGRITY_CHECK_VALUE
+    #define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )              ( pxList )->xListIntegrityValue1 = pdINTEGRITY_CHECK_VALUE
+    #define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )              ( pxList )->xListIntegrityValue2 = pdINTEGRITY_CHECK_VALUE
+
+/* Define macros that will assert if one of the structure members does not
+ * contain its expected value. */
+    #define listTEST_LIST_ITEM_INTEGRITY( pxItem )                      configASSERT( ( ( pxItem )->xListItemIntegrityValue1 == pdINTEGRITY_CHECK_VALUE ) && ( ( pxItem )->xListItemIntegrityValue2 == pdINTEGRITY_CHECK_VALUE ) )
+    #define listTEST_LIST_INTEGRITY( pxList )                           configASSERT( ( ( pxList )->xListIntegrityValue1 == pdINTEGRITY_CHECK_VALUE ) && ( ( pxList )->xListIntegrityValue2 == pdINTEGRITY_CHECK_VALUE ) )
+#endif /* configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES */
+
+
+/*
+ * Definition of the only type of object that a list can contain.
+ */
+struct xLIST;
+struct xLIST_ITEM
+{
+    listFIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE               /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+    configLIST_VOLATILE TickType_t xItemValue;              /*< The value being listed.  In most cases this is used to sort the list in descending order. */
+    struct xLIST_ITEM * configLIST_VOLATILE pxNext;         /*< Pointer to the next ListItem_t in the list. */
+    struct xLIST_ITEM * configLIST_VOLATILE pxPrevious;     /*< Pointer to the previous ListItem_t in the list. */
+    void * pvOwner;                                         /*< Pointer to the object (normally a TCB) that contains the list item.  There is therefore a two way link between the object containing the list item and the list item itself. */
+    struct xLIST * configLIST_VOLATILE pxContainer;         /*< Pointer to the list in which this list item is placed (if any). */
+    listSECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE              /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+};
+typedef struct xLIST_ITEM ListItem_t;                       /* For some reason lint wants this as two separate definitions. */
+
+struct xMINI_LIST_ITEM
+{
+    listFIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE     /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+    configLIST_VOLATILE TickType_t xItemValue;
+    struct xLIST_ITEM * configLIST_VOLATILE pxNext;
+    struct xLIST_ITEM * configLIST_VOLATILE pxPrevious;
+};
+typedef struct xMINI_LIST_ITEM MiniListItem_t;
+
+/*
+ * Definition of the type of queue used by the scheduler.
+ */
+typedef struct xLIST
+{
+    listFIRST_LIST_INTEGRITY_CHECK_VALUE          /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+    volatile UBaseType_t uxNumberOfItems;
+    ListItem_t * configLIST_VOLATILE pxIndex;     /*< Used to walk through the list.  Points to the last item returned by a call to listGET_OWNER_OF_NEXT_ENTRY (). */
+    #ifdef VERIFAST
+        /* Reason for rewrite:
+         * This change allows us to reuse the existing single-core list proofs,
+         * for which an identical rewrite for assumed.
+         */
+       ListItem_t xListEnd;
+    #else
+        MiniListItem_t xListEnd;                      /*< List item that contains the maximum possible item value meaning it is always at the end of the list and is therefore used as a marker. */
+    #endif /* VERIFAST */
+    listSECOND_LIST_INTEGRITY_CHECK_VALUE         /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+} List_t;
+
+/*
+ * Access macro to set the owner of a list item.  The owner of a list item
+ * is the object (usually a TCB) that contains the list item.
+ *
+ * \page listSET_LIST_ITEM_OWNER listSET_LIST_ITEM_OWNER
+ * \ingroup LinkedList
+ */
+#define listSET_LIST_ITEM_OWNER( pxListItem, pxOwner )    ( ( pxListItem )->pvOwner = ( void * ) ( pxOwner ) )
+
+/*
+ * Access macro to get the owner of a list item.  The owner of a list item
+ * is the object (usually a TCB) that contains the list item.
+ *
+ * \page listGET_LIST_ITEM_OWNER listSET_LIST_ITEM_OWNER
+ * \ingroup LinkedList
+ */
+#define listGET_LIST_ITEM_OWNER( pxListItem )             ( ( pxListItem )->pvOwner )
+
+/*
+ * Access macro to set the value of the list item.  In most cases the value is
+ * used to sort the list in descending order.
+ *
+ * \page listSET_LIST_ITEM_VALUE listSET_LIST_ITEM_VALUE
+ * \ingroup LinkedList
+ */
+#define listSET_LIST_ITEM_VALUE( pxListItem, xValue )     ( ( pxListItem )->xItemValue = ( xValue ) )
+
+/*
+ * Access macro to retrieve the value of the list item.  The value can
+ * represent anything - for example the priority of a task, or the time at
+ * which a task should be unblocked.
+ *
+ * \page listGET_LIST_ITEM_VALUE listGET_LIST_ITEM_VALUE
+ * \ingroup LinkedList
+ */
+#define listGET_LIST_ITEM_VALUE( pxListItem )             ( ( pxListItem )->xItemValue )
+
+/*
+ * Access macro to retrieve the value of the list item at the head of a given
+ * list.
+ *
+ * \page listGET_LIST_ITEM_VALUE listGET_LIST_ITEM_VALUE
+ * \ingroup LinkedList
+ */
+#define listGET_ITEM_VALUE_OF_HEAD_ENTRY( pxList )        ( ( ( pxList )->xListEnd ).pxNext->xItemValue )
+
+/*
+ * Return the list item at the head of the list.
+ *
+ * \page listGET_HEAD_ENTRY listGET_HEAD_ENTRY
+ * \ingroup LinkedList
+ */
+#define listGET_HEAD_ENTRY( pxList )                      ( ( ( pxList )->xListEnd ).pxNext )
+
+/*
+ * Return the next list item.
+ *
+ * \page listGET_NEXT listGET_NEXT
+ * \ingroup LinkedList
+ */
+#define listGET_NEXT( pxListItem )                        ( ( pxListItem )->pxNext )
+
+/*
+ * Return the list item that marks the end of the list
+ *
+ * \page listGET_END_MARKER listGET_END_MARKER
+ * \ingroup LinkedList
+ */
+#define listGET_END_MARKER( pxList )                      ( ( ListItem_t const * ) ( &( ( pxList )->xListEnd ) ) )
+
+/*
+ * Access macro to determine if a list contains any items.  The macro will
+ * only have the value true if the list is empty.
+ *
+ * \page listLIST_IS_EMPTY listLIST_IS_EMPTY
+ * \ingroup LinkedList
+ */
+#define listLIST_IS_EMPTY( pxList )                       ( ( ( pxList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? pdTRUE : pdFALSE )
+
+/*
+ * Access macro to return the number of items in the list.
+ */
+#define listCURRENT_LIST_LENGTH( pxList )                 ( ( pxList )->uxNumberOfItems )
+
+/*
+ * Access function to obtain the owner of the next entry in a list.
+ *
+ * The list member pxIndex is used to walk through a list.  Calling
+ * listGET_OWNER_OF_NEXT_ENTRY increments pxIndex to the next item in the list
+ * and returns that entry's pxOwner parameter.  Using multiple calls to this
+ * function it is therefore possible to move through every item contained in
+ * a list.
+ *
+ * The pxOwner parameter of a list item is a pointer to the object that owns
+ * the list item.  In the scheduler this is normally a task control block.
+ * The pxOwner parameter effectively creates a two way link between the list
+ * item and its owner.
+ *
+ * @param pxTCB pxTCB is set to the address of the owner of the next list item.
+ * @param pxList The list from which the next item owner is to be returned.
+ *
+ * \page listGET_OWNER_OF_NEXT_ENTRY listGET_OWNER_OF_NEXT_ENTRY
+ * \ingroup LinkedList
+ */
+#define listGET_OWNER_OF_NEXT_ENTRY( pxTCB, pxList )                                           \
+    {                                                                                          \
+        List_t * const pxConstList = ( pxList );                                               \
+        /* Increment the index to the next item and return the item, ensuring */               \
+        /* we don't return the marker used at the end of the list.  */                         \
+        ( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext;                           \
+        if( ( void * ) ( pxConstList )->pxIndex == ( void * ) &( ( pxConstList )->xListEnd ) ) \
+        {                                                                                      \
+            ( pxConstList )->pxIndex = ( pxConstList )->pxIndex->pxNext;                       \
+        }                                                                                      \
+        ( pxTCB ) = ( pxConstList )->pxIndex->pvOwner;                                         \
+    }
+
+
+
+/*
+ * Access function to obtain the owner of the first entry in a list.  Lists
+ * are normally sorted in ascending item value order.
+ *
+ * This function returns the pxOwner member of the first item in the list.
+ * The pxOwner parameter of a list item is a pointer to the object that owns
+ * the list item.  In the scheduler this is normally a task control block.
+ * The pxOwner parameter effectively creates a two way link between the list
+ * item and its owner.
+ *
+ * @param pxList The list from which the owner of the head item is to be
+ * returned.
+ *
+ * \page listGET_OWNER_OF_HEAD_ENTRY listGET_OWNER_OF_HEAD_ENTRY
+ * \ingroup LinkedList
+ */
+#define listGET_OWNER_OF_HEAD_ENTRY( pxList )            ( ( &( ( pxList )->xListEnd ) )->pxNext->pvOwner )
+
+/*
+ * Check to see if a list item is within a list.  The list item maintains a
+ * "container" pointer that points to the list it is in.  All this macro does
+ * is check to see if the container and the list match.
+ *
+ * @param pxList The list we want to know if the list item is within.
+ * @param pxListItem The list item we want to know if is in the list.
+ * @return pdTRUE if the list item is in the list, otherwise pdFALSE.
+ */
+#define listIS_CONTAINED_WITHIN( pxList, pxListItem )    ( ( ( pxListItem )->pxContainer == ( pxList ) ) ? ( pdTRUE ) : ( pdFALSE ) )
+
+/*
+ * Return the list a list item is contained within (referenced from).
+ *
+ * @param pxListItem The list item being queried.
+ * @return A pointer to the List_t object that references the pxListItem
+ */
+#define listLIST_ITEM_CONTAINER( pxListItem )            ( ( pxListItem )->pxContainer )
+
+/*
+ * This provides a crude means of knowing if a list has been initialised, as
+ * pxList->xListEnd.xItemValue is set to portMAX_DELAY by the vListInitialise()
+ * function.
+ */
+#define listLIST_IS_INITIALISED( pxList )                ( ( pxList )->xListEnd.xItemValue == portMAX_DELAY )
+
+/*
+ * Must be called before a list is used!  This initialises all the members
+ * of the list structure and inserts the xListEnd item into the list as a
+ * marker to the back of the list.
+ *
+ * @param pxList Pointer to the list being initialised.
+ *
+ * \page vListInitialise vListInitialise
+ * \ingroup LinkedList
+ */
+void vListInitialise( List_t * const pxList ) PRIVILEGED_FUNCTION;
+
+/*
+ * Must be called before a list item is used.  This sets the list container to
+ * null so the item does not think that it is already contained in a list.
+ *
+ * @param pxItem Pointer to the list item being initialised.
+ *
+ * \page vListInitialiseItem vListInitialiseItem
+ * \ingroup LinkedList
+ */
+void vListInitialiseItem( ListItem_t * const pxItem ) PRIVILEGED_FUNCTION;
+//@ requires pxItem->pxContainer |-> _;
+//@ ensures pxItem->pxContainer |-> 0;
+
+/*
+ * Insert a list item into a list.  The item will be inserted into the list in
+ * a position determined by its item value (descending item value order).
+ *
+ * @param pxList The list into which the item is to be inserted.
+ *
+ * @param pxNewListItem The item that is to be placed in the list.
+ *
+ * \page vListInsert vListInsert
+ * \ingroup LinkedList
+ */
+void vListInsert( List_t * const pxList,
+                  ListItem_t * const pxNewListItem ) PRIVILEGED_FUNCTION;
+
+/*
+ * Insert a list item into a list.  The item will be inserted in a position
+ * such that it will be the last item within the list returned by multiple
+ * calls to listGET_OWNER_OF_NEXT_ENTRY.
+ *
+ * The list member pxIndex is used to walk through a list.  Calling
+ * listGET_OWNER_OF_NEXT_ENTRY increments pxIndex to the next item in the list.
+ * Placing an item in a list using vListInsertEnd effectively places the item
+ * in the list position pointed to by pxIndex.  This means that every other
+ * item within the list will be returned by listGET_OWNER_OF_NEXT_ENTRY before
+ * the pxIndex parameter again points to the item being inserted.
+ *
+ * @param pxList The list into which the item is to be inserted.
+ *
+ * @param pxNewListItem The list item to be inserted into the list.
+ *
+ * \page vListInsertEnd vListInsertEnd
+ * \ingroup LinkedList
+ */
+void vListInsertEnd( List_t * const pxList,
+                     ListItem_t * const pxNewListItem ) PRIVILEGED_FUNCTION;
+
+/*
+ * Remove an item from a list.  The list item has a pointer to the list that
+ * it is in, so only the list item need be passed into the function.
+ *
+ * @param uxListRemove The item to be removed.  The item will remove itself from
+ * the list pointed to by it's pxContainer parameter.
+ *
+ * @return The number of items that remain in the list after the list item has
+ * been removed.
+ *
+ * \page uxListRemove uxListRemove
+ * \ingroup LinkedList
+ */
+UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove ) PRIVILEGED_FUNCTION;
+
+/* *INDENT-OFF* */
+#ifdef __cplusplus
+    }
+#endif
+/* *INDENT-ON* */
+
+#endif /* ifndef LIST_H */

Test/VeriFast/tasks/vTaskSwitchContext/include/portable.h

@@ -0,0 +1,245 @@
+/*
+ * FreeRTOS SMP Kernel V202110.00
+ * Copyright (C) 2020 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
+ *
+ */
+
+/*-----------------------------------------------------------
+* Portable layer API.  Each function must be defined for each port.
+*----------------------------------------------------------*/
+
+#ifndef PORTABLE_H
+#define PORTABLE_H
+
+/* Each FreeRTOS port has a unique portmacro.h header file.  Originally a
+ * pre-processor definition was used to ensure the pre-processor found the correct
+ * portmacro.h file for the port being used.  That scheme was deprecated in favour
+ * of setting the compiler's include path such that it found the correct
+ * portmacro.h file - removing the need for the constant and allowing the
+ * portmacro.h file to be located anywhere in relation to the port being used.
+ * Purely for reasons of backward compatibility the old method is still valid, but
+ * to make it clear that new projects should not use it, support for the port
+ * specific constants has been moved into the deprecated_definitions.h header
+ * file. */
+#include "deprecated_definitions.h"
+
+/* If portENTER_CRITICAL is not defined then including deprecated_definitions.h
+ * did not result in a portmacro.h header file being included - and it should be
+ * included here.  In this case the path to the correct portmacro.h header file
+ * must be set in the compiler's include path. */
+#ifndef portENTER_CRITICAL
+    #include "portmacro.h"
+#endif
+
+#if portBYTE_ALIGNMENT == 32
+    #define portBYTE_ALIGNMENT_MASK    ( 0x001f )
+#endif
+
+#if portBYTE_ALIGNMENT == 16
+    #define portBYTE_ALIGNMENT_MASK    ( 0x000f )
+#endif
+
+#if portBYTE_ALIGNMENT == 8
+    #define portBYTE_ALIGNMENT_MASK    ( 0x0007 )
+#endif
+
+#if portBYTE_ALIGNMENT == 4
+    #define portBYTE_ALIGNMENT_MASK    ( 0x0003 )
+#endif
+
+#if portBYTE_ALIGNMENT == 2
+    #define portBYTE_ALIGNMENT_MASK    ( 0x0001 )
+#endif
+
+#if portBYTE_ALIGNMENT == 1
+    #define portBYTE_ALIGNMENT_MASK    ( 0x0000 )
+#endif
+
+#ifndef portBYTE_ALIGNMENT_MASK
+    #error "Invalid portBYTE_ALIGNMENT definition"
+#endif
+
+#ifndef portNUM_CONFIGURABLE_REGIONS
+    #define portNUM_CONFIGURABLE_REGIONS    1
+#endif
+
+#ifndef portHAS_STACK_OVERFLOW_CHECKING
+    #define portHAS_STACK_OVERFLOW_CHECKING    0
+#endif
+
+#ifndef portARCH_NAME
+    #define portARCH_NAME    NULL
+#endif
+
+/* *INDENT-OFF* */
+#ifdef __cplusplus
+    extern "C" {
+#endif
+/* *INDENT-ON* */
+
+#include "mpu_wrappers.h"
+
+/*
+ * Setup the stack of a new task so it is ready to be placed under the
+ * scheduler control.  The registers have to be placed on the stack in
+ * the order that the port expects to find them.
+ *
+ */
+#if ( portUSING_MPU_WRAPPERS == 1 )
+    #if ( portHAS_STACK_OVERFLOW_CHECKING == 1 )
+        StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
+                                             StackType_t * pxEndOfStack,
+                                             TaskFunction_t pxCode,
+                                             void * pvParameters,
+                                             BaseType_t xRunPrivileged ) PRIVILEGED_FUNCTION;
+    #else
+        StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
+                                             TaskFunction_t pxCode,
+                                             void * pvParameters,
+                                             BaseType_t xRunPrivileged ) PRIVILEGED_FUNCTION;
+    #endif
+#else /* if ( portUSING_MPU_WRAPPERS == 1 ) */
+    #if ( portHAS_STACK_OVERFLOW_CHECKING == 1 )
+        StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
+                                             StackType_t * pxEndOfStack,
+                                             TaskFunction_t pxCode,
+                                             void * pvParameters ) PRIVILEGED_FUNCTION;
+    #else
+        StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
+                                             TaskFunction_t pxCode,
+                                             void * pvParameters ) PRIVILEGED_FUNCTION;
+        ///@ requires true;
+        ///@ ensures true;
+    #endif
+#endif /* if ( portUSING_MPU_WRAPPERS == 1 ) */
+
+/* Used by heap_5.c to define the start address and size of each memory region
+ * that together comprise the total FreeRTOS heap space. */
+typedef struct HeapRegion
+{
+    uint8_t * pucStartAddress;
+    size_t xSizeInBytes;
+} HeapRegion_t;
+
+/* Used to pass information about the heap out of vPortGetHeapStats(). */
+typedef struct xHeapStats
+{
+    size_t xAvailableHeapSpaceInBytes;          /* The total heap size currently available - this is the sum of all the free blocks, not the largest block that can be allocated. */
+    size_t xSizeOfLargestFreeBlockInBytes;      /* The maximum size, in bytes, of all the free blocks within the heap at the time vPortGetHeapStats() is called. */
+    size_t xSizeOfSmallestFreeBlockInBytes;     /* The minimum size, in bytes, of all the free blocks within the heap at the time vPortGetHeapStats() is called. */
+    size_t xNumberOfFreeBlocks;                 /* The number of free memory blocks within the heap at the time vPortGetHeapStats() is called. */
+    size_t xMinimumEverFreeBytesRemaining;      /* The minimum amount of total free memory (sum of all free blocks) there has been in the heap since the system booted. */
+    size_t xNumberOfSuccessfulAllocations;      /* The number of calls to pvPortMalloc() that have returned a valid memory block. */
+    size_t xNumberOfSuccessfulFrees;            /* The number of calls to vPortFree() that has successfully freed a block of memory. */
+} HeapStats_t;
+
+/*
+ * Used to define multiple heap regions for use by heap_5.c.  This function
+ * must be called before any calls to pvPortMalloc() - not creating a task,
+ * queue, semaphore, mutex, software timer, event group, etc. will result in
+ * pvPortMalloc being called.
+ *
+ * pxHeapRegions passes in an array of HeapRegion_t structures - each of which
+ * defines a region of memory that can be used as the heap.  The array is
+ * terminated by a HeapRegions_t structure that has a size of 0.  The region
+ * with the lowest start address must appear first in the array.
+ */
+void vPortDefineHeapRegions( const HeapRegion_t * const pxHeapRegions ) PRIVILEGED_FUNCTION;
+
+/*
+ * Returns a HeapStats_t structure filled with information about the current
+ * heap state.
+ */
+void vPortGetHeapStats( HeapStats_t * pxHeapStats );
+
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * VeriFast treats the `malloc` and `free` functions specially,
+     * in a particular built-in way that cannot be axiomatized within
+     * VeriFast's specification language. 
+     * 
+     * When `malloc( sizeof(struct S) )` is called for a user defined
+     * struct `S`, VeriFast instantiates the corresponding
+     * `malloc_block_S(...)` predicate as well as points-to chunks
+     * for its fields.
+     * Reversely, calling `free` cleans up all the predicates instantiated
+     * by `malloc`.
+     */
+    #define pvPortMalloc malloc
+    #define vPortFree(ptr) free( (void*) ptr)
+#else
+    /*
+    * Map to the memory management routines required for the port.
+    */
+    void * pvPortMalloc( size_t xSize ) PRIVILEGED_FUNCTION;
+    void vPortFree( void * pv ) PRIVILEGED_FUNCTION;
+#endif /* VERIFAST */
+
+
+void vPortInitialiseBlocks( void ) PRIVILEGED_FUNCTION;
+size_t xPortGetFreeHeapSize( void ) PRIVILEGED_FUNCTION;
+size_t xPortGetMinimumEverFreeHeapSize( void ) PRIVILEGED_FUNCTION;
+
+#if( configSTACK_ALLOCATION_FROM_SEPARATE_HEAP == 1 )
+    void *pvPortMallocStack( size_t xSize ) PRIVILEGED_FUNCTION;
+    void vPortFreeStack( void *pv ) PRIVILEGED_FUNCTION;
+#else
+    #define pvPortMallocStack pvPortMalloc
+    #define vPortFreeStack vPortFree
+#endif
+
+/*
+ * Setup the hardware ready for the scheduler to take control.  This generally
+ * sets up a tick interrupt and sets timers for the correct tick frequency.
+ */
+BaseType_t xPortStartScheduler( void ) PRIVILEGED_FUNCTION;
+
+/*
+ * Undo any hardware/ISR setup that was performed by xPortStartScheduler() so
+ * the hardware is left in its original condition after the scheduler stops
+ * executing.
+ */
+void vPortEndScheduler( void ) PRIVILEGED_FUNCTION;
+
+/*
+ * The structures and methods of manipulating the MPU are contained within the
+ * port layer.
+ *
+ * Fills the xMPUSettings structure with the memory region information
+ * contained in xRegions.
+ */
+#if ( portUSING_MPU_WRAPPERS == 1 )
+    struct xMEMORY_REGION;
+    void vPortStoreTaskMPUSettings( xMPU_SETTINGS * xMPUSettings,
+                                    const struct xMEMORY_REGION * const xRegions,
+                                    StackType_t * pxBottomOfStack,
+                                    uint32_t ulStackDepth ) PRIVILEGED_FUNCTION;
+#endif
+
+/* *INDENT-OFF* */
+#ifdef __cplusplus
+    }
+#endif
+/* *INDENT-ON* */
+
+#endif /* PORTABLE_H */

Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h

@@ -0,0 +1,208 @@
+/*
+ * FreeRTOS SMP Kernel V202110.00
+ * Copyright (C) 2020 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
+ *
+ */
+
+#ifndef STACK_MACROS_H
+#define STACK_MACROS_H
+
+/*
+ * Call the stack overflow hook function if the stack of the task being swapped
+ * out is currently overflowed, or looks like it might have overflowed in the
+ * past.
+ *
+ * Setting configCHECK_FOR_STACK_OVERFLOW to 1 will cause the macro to check
+ * the current stack state only - comparing the current top of stack value to
+ * the stack limit.  Setting configCHECK_FOR_STACK_OVERFLOW to greater than 1
+ * will also cause the last few stack bytes to be checked to ensure the value
+ * to which the bytes were set when the task was created have not been
+ * overwritten.  Note this second test does not guarantee that an overflowed
+ * stack will always be recognised.
+ */
+
+/*-----------------------------------------------------------*/
+
+/*
+ * portSTACK_LIMIT_PADDING is a number of extra words to consider to be in
+ * use on the stack.
+ */
+#ifndef portSTACK_LIMIT_PADDING
+    #define portSTACK_LIMIT_PADDING 0
+#endif
+
+#if ( ( configCHECK_FOR_STACK_OVERFLOW == 1 ) && ( portSTACK_GROWTH < 0 ) )
+
+/* Only the current stack state is to be checked. */
+    #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
+    {                                                                                                 \
+        /* Is the currently saved stack pointer within the stack limit? */                            \
+        if( pxCurrentTCB->pxTopOfStack <= pxCurrentTCB->pxStack + portSTACK_LIMIT_PADDING )           \
+        {                                                                                             \
+            vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
+        }                                                                                             \
+    }
+
+#endif /* configCHECK_FOR_STACK_OVERFLOW == 1 */
+/*-----------------------------------------------------------*/
+
+#if ( ( configCHECK_FOR_STACK_OVERFLOW == 1 ) && ( portSTACK_GROWTH > 0 ) )
+
+/* Only the current stack state is to be checked. */
+    #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
+    {                                                                                                 \
+                                                                                                      \
+        /* Is the currently saved stack pointer within the stack limit? */                            \
+        if( pxCurrentTCB->pxTopOfStack >= pxCurrentTCB->pxEndOfStack - portSTACK_LIMIT_PADDING )      \
+        {                                                                                             \
+            vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
+        }                                                                                             \
+    }
+
+#endif /* configCHECK_FOR_STACK_OVERFLOW == 1 */
+/*-----------------------------------------------------------*/
+
+#if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH < 0 ) )
+
+    /* TODO: Convert this macro into a function such that we can insert proof annotations.
+    */
+    #ifdef VERIFAST
+        /* Reason for rewrite: 
+         * VeriFast complains about unspecified evaluation order of
+         * - `pxCurrentTCB->pxStack`
+         * - `vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName );`
+         *
+        */
+        #define taskCHECK_FOR_STACK_OVERFLOW()   VF__taskCHECK_FOR_STACK_OVERFLOW()
+
+        void VF__taskCHECK_FOR_STACK_OVERFLOW()
+        /*@ requires prvSeg_TCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*&
+                     coreLocalSeg_TCB_p(gCurrentTCB, ?uxCriticalNesting) &*&
+                    // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
+                        interruptState_p(coreID_f(), ?state) &*&
+                        interruptsDisabled_f(state) == true &*&
+                        pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);
+        @*/
+        /*@ ensures prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack) &*&
+                     coreLocalSeg_TCB_p(gCurrentTCB, uxCriticalNesting) &*&
+                    // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
+                        interruptState_p(coreID_f(), state) &*&
+                        interruptsDisabled_f(state) == true &*&
+                        pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);                                            \
+        @*/                                                                                               \
+        {                                                                                                 \
+            /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                       \
+            /*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack,                                 \
+                        ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) );                                 \
+             @*/                                                                                          \
+            /*@ open stack_p_2(_, _, _, _, _, _); @*/                                                     \
+            /* The detour below allows us to skip proving that `ulFreeBytes`                              \
+             * is a multiple of `sizeof(StackType_t)`.                                                    \
+             */                                                                                           \
+            /*@ integers__to_chars(pxTopOfStack+1); @*/                                                   \
+            /*@ chars_join((char*) pxStack); @*/                                                          \
+            /*@ chars_to_integers_(pxStack, sizeof(StackType_t), false, 4); @*/                           \
+            TCB_t* tcb0 = pxCurrentTCB;                                                                   \
+            const uint32_t * const pulStack = ( uint32_t * ) tcb0->pxStack;                               \
+            const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
+                                                                                                          \
+            /*@ bool gOverflow = false; @*/                                                               \
+            if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
+            {                                                                                             \
+                /*@ gOverflow = true; @*/                                                                 \
+                /*@ integers__to_chars(pxStack); @*/                                                      \
+        	    /*@ chars_join((char*) pxStack); @*/                                                      \
+        	    /*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/                                 \
+        	    /*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                  \
+                                    ulFreeBytes, ulUsedCells, ulUnalignedBytes);                          \
+                @*/                                                                                       \
+        	    /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                  \
+                TCB_t* tcb1 = pxCurrentTCB;                                                               \
+                TCB_t* tcb2 = pxCurrentTCB;                                                               \
+                vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName );                 \
+            }                                                                                             \
+            /*@                                                                                           \
+            if(!gOverflow) {                                                                              \
+                integers__to_chars(pxStack);                                                              \
+        	    chars_join((char*) pxStack);                                                              \
+        	    chars_split((char*) pxStack, ulFreeBytesOnStack);                                         \
+        	    close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                      \
+                                ulFreeBytes, ulUsedCells, ulUnalignedBytes);                              \
+        	    close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack);                                          \
+            }                                                                                             \
+            @*/                                                                                           \
+        }
+    #else
+        #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
+        {                                                                                                 \
+            const uint32_t * const pulStack = ( uint32_t * ) pxCurrentTCB->pxStack;                       \
+            const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
+                                                                                                        \
+            if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
+            {                                                                                             \
+                vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
+            }                                                                                             \
+        }
+    #endif /* VERIFAST */
+
+#endif /* #if( configCHECK_FOR_STACK_OVERFLOW > 1 ) */
+/*-----------------------------------------------------------*/
+
+#if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH > 0 ) )
+
+    #define taskCHECK_FOR_STACK_OVERFLOW()                                                                                                \
+    {                                                                                                                                     \
+        int8_t * pcEndOfStack = ( int8_t * ) pxCurrentTCB->pxEndOfStack;                                                                  \
+        static const uint8_t ucExpectedStackBytes[] = { tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE,   \
+                                                        tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE,   \
+                                                        tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE,   \
+                                                        tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE,   \
+                                                        tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE, tskSTACK_FILL_BYTE }; \
+                                                                                                                                          \
+                                                                                                                                          \
+        pcEndOfStack -= sizeof( ucExpectedStackBytes );                                                                                   \
+                                                                                                                                          \
+        /* Has the extremity of the task stack ever been written over? */                                                                 \
+        if( memcmp( ( void * ) pcEndOfStack, ( void * ) ucExpectedStackBytes, sizeof( ucExpectedStackBytes ) ) != 0 )                     \
+        {                                                                                                                                 \
+            vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName );                                     \
+        }                                                                                                                                 \
+    }
+
+#endif /* #if( configCHECK_FOR_STACK_OVERFLOW > 1 ) */
+/*-----------------------------------------------------------*/
+
+/* Remove stack overflow macro if not being used. */
+#ifndef taskCHECK_FOR_STACK_OVERFLOW
+    #define taskCHECK_FOR_STACK_OVERFLOW()
+#endif
+
+
+
+#endif /* STACK_MACROS_H */